Equivalence checking

[Rick Jackson]

Off topic, I know, but hopefully someone can help...

I'm a newbie at EC and have a problem where I have to modify an old
design, and implement it on a new technology with a different vendor.
Before starting, I need to check that I can rebuild the old design,
but without access to the original tools, or the original designers.

I'm hoping to do this with an equivalence checker. Can anyone tell me
if the following requirements are possible and, if so, recommend a
tool? Are there any good references on EC?

1) Compare the original RTL against the original Synopsys netlist.
Note that we don't appear to have the original vendor library, or an
HDL netlist, but we do have a db file for the chip. I need to do this
because it's not obvious that "the original RTL" was actually used for
the final netlist.

2) Resynthesise (with Synplicity, not Synopsys) with a new vendor
library, and compare the new netlist with the original netlist or db
file. Is this possible, given that the libraries have changed?

3) The original includes DesignWare components which won't be in the
new device. Is this a problem?

Thanks -

Rick

[n***@gmail.com]

The Formality from synopsys is good for the job. If you have original
RTL, compre to original netlist is only for experiment. Check
equivalency on the new netlist and RTL is enough to validate new
netlist.
If the DesignWare is in RTL, you have to replace it with something
Synplicity can recognize. If it is in original netlist or db file,
that's fine.

Nandy
www.nandigits.com

[Alvin Andries]

Post by Rick Jackson
Off topic, I know, but hopefully someone can help...
I'm a newbie at EC and have a problem where I have to modify an old
design, and implement it on a new technology with a different vendor.
Before starting, I need to check that I can rebuild the old design,
but without access to the original tools, or the original designers.
I'm hoping to do this with an equivalence checker. Can anyone tell me
if the following requirements are possible and, if so, recommend a
tool? Are there any good references on EC?
1) Compare the original RTL against the original Synopsys netlist.
Note that we don't appear to have the original vendor library, or an
HDL netlist, but we do have a db file for the chip. I need to do this
because it's not obvious that "the original RTL" was actually used for
the final netlist.
2) Resynthesise (with Synplicity, not Synopsys) with a new vendor
library, and compare the new netlist with the original netlist or db
file. Is this possible, given that the libraries have changed?
3) The original includes DesignWare components which won't be in the
new device. Is this a problem?
Thanks -
Rick

Hi,

Quite a challenge!

Some comments (I have some Formality experience):

1) Without vendor technology file, you'll have to code the functionality of
each gate. Easy enough for INV, ND2. This becomes a bit boring when you have
to code INVx2, InVx4, ..., but what if you need to guess AOI34? The least
you'll need is a datasheet. Still, try to get the vendor library. Another
point is how creative the synthesis was done and what was synthesized: if
retiming was applied, you're probably stuck. Also, large arithmetic
structures might prove to be challenging.

2) I would recommend checking versus the RTL. After all, this should be
equivalent and also a lot easier because your new synnthesis might select
different architectures for arithmetic operands. No big deal if an 8 bit
adder changes from ripple to carry-look-ahead, but a 24 by 24
multiplication-addition will most likely turn out to be unverifiable.

3) No real problem: some vendors have DESIGNWARE replacements (Synplicity,
if I'm correct) or something equivalent (AWARITH from Cadence). Generic
arithmetic should preferably be coded as such (+, *) as the tools do a
decent job nowadays. Specialized DW IP will be a problem (you can always
import it from the old netlist and resynthesize it). If you have
instantiated DW components in the original source code, you'll need the DW
directories of the original synthesis tool. Should not be a problem if you
have a Synopsys account. Only difficulty might be the license (I don't know
if FM will grab a DW license when comparing, you'll have to ask). If the DC
version turns out to be too old for your FM version, you might try a more
recent version of DW, but beware of changes.

Regards,
Alvin.

[u***@stanka-web.de]

Post by Rick Jackson
I'm a newbie at EC and have a problem where I have to modify an old
design, and implement it on a new technology with a different vendor.
Before starting, I need to check that I can rebuild the old design,
but without access to the original tools, or the original designers.
I'm hoping to do this with an equivalence checker. Can anyone tell me
if the following requirements are possible and, if so, recommend a
tool? Are there any good references on EC?

You found a very good usage for EC tools :).

I tested four tools ~2 years ago:
- Echeck (Prover)
- Formality (Synopsys)
- Formal Pro (Mentor Graphics)
- LEC (Verplex, now Cadence)

Each of these had major advantages and disadvantages.
- Echeck is good for small designs, but small (unknown) company and
provide less comfort if your EC failed.
- Formality could do FPGAs, but died on designs with more than one
one-hot encoded statemachine per instance (Hah, flat netlist with only
one statemachine supported?)
- Formal Pro was very good for ASICs, but not usable if you have a
FPGA-Library. It provides very good help for manual matching but failed
to often on automatic matching.
- LEC was very good but expensive (and is now sold to Cadence don't
know what the mean to the tool). LEC needs a high training effort. I
found it weak on handling register doubling (often done by Synplify)

Independend of your tool choice you will face problems on:
- "unusually Code" like generics, unconstraint ports, 3D-Arrays
- register mapping (doubling, state encoding, register prunning,
different names)
- statemachines (unused states, one hot, ...)
- internal tristate

Post by Rick Jackson
1) Compare the original RTL against the original Synopsys netlist.
Note that we don't appear to have the original vendor library, or an
HDL netlist, but we do have a db file for the chip. I need to do this
because it's not obvious that "the original RTL" was actually used for
the final netlist.

First Problem: what function has a netlist, if you even don't know what
function has a simple gate? Of course its easy to guess the function of
AND2, but what is AO2B?

Note you need typically a Verilog or VHDL file for the netlist, Edif
and DB are not allways supported.

Post by Rick Jackson
2) Resynthesise (with Synplicity, not Synopsys) with a new vendor
library, and compare the new netlist with the original netlist or db
file. Is this possible, given that the libraries have changed?

It is possible if you have both libraries (I did this task a few
times). You will likely face a lot of problems due to the different
ways the tools do their job. Synplify doubles register for load
balancing, and did some awefull thinks to minimize statemachines. This
will take a lot of time for register matching.

Post by Rick Jackson
3) The original includes DesignWare components which won't be in the
new device. Is this a problem?

No.

bye Thomas