( ESNUG 322 Item 8 ) ---------------------------------------------- [6/15/99]
Subject: ( ESNUG 320 #3 321 #4 ) We Found Equivalency Checking Useful
> Equivalence checkers work hierarchically, so large designs aren't
> a problem if they have matching hierarchy. The main problems are:
> ... RTL to gates if there is not matching hierarchy. But flow can solve
> this. Use an RTL to hierarchical-gates proof, then a hierarchical to
> flat gates proof,...
>
> - Mike Bartley
> STMicroelectronics Bristol, UK
From: damianf@s3two.ie (Damian Finnerty)
I'm evaluating Chrysalis at the moment and I've just come across this
problem. I'm awaiting a response from a Chrysalis AE but I'd like to hear
from somebody who is actually using one of these tools.
I'm trying to compare RTL to Flattened-Gates.
Usually when doing an RTL to Gate comparison, I break the design up into
sub-blocks and do the equivalency check hierarchically. But, with a
flattened netlist this does not seem to be possible. You have to compile
and compare the whole design. This is not viable when working with a
1+ million gate design as I am. The ONLY solution appears to be to do
what you said above...
RTL to Hier-Gates
Hier-Gates to Flattened-Gates
Is this correct?
- Damian Finnerty
S3 Dublin, Ireland
---- ---- ---- ---- ---- ---- ----
From: Mike Bartley <bartley@bristol.st.com>
Damian
Yes - I would say that the only way to really do this is
RTL to Hier-Gates
Hier-Gates to Flattened-Gates
But that shouldn't be too much of a problem.
- Mike Bartley
STMicroelectronics Bristol, UK
---- ---- ---- ---- ---- ---- ----
From: Chrystian Roy <croy@lsil.com>
Hi John,
I was very surprised about Don Mills' assertion that equivalence checking
is useless. We have had quite a different experience at LSI Logic.
Just as an illustration, my latest project was to help on the formal
verification of a design in a RTL signoff (this was a "give us your RTL
and we will fab you a chip" deal). The specs were:
- G10 technology (0.35 um)
- flip chip package, close to 1000 leads
- 100 MHz clock frequency
- 460 Kgates (whole chip, not counting rams)
- 230 Kgates (without cores)
- 200 Kgates (without cores and pads)
The synthesized logic (200 Kgates) was verified against the RTL in one
block in 1.25 hour (including reading in the designs). Memory usage was
615 Mb. The memory limit under Solaris 2.6 is around 3.7 Gb. We were not
even close to that.
Gate-to-gate verification required 0.35 hour and 695 Mb (this was for the
final netlist against the synthesized gates, with scan chain disabled and
wihtout cores). Two bugs were caught using equivalence checking. One of
them would have been quite difficult to find using other methods. The run
time of the full gate level simulations on a compute farm was 2 weeks.
This is compared to 21 minutes for equivalence checking on a single CPU.
All benchmark data is from a dual CPU (200 MHz) Ultra 2 with 2 Gb of RAM
and is very design dependent of course. Every equivalence checker is
going to choke on a large multiplier for example.
We found formal verification to be very useful to check that any
transformation performed on a netlist (scan, JTAG, and BCT insertion,
IPO, hand edits, scan reorder, place and route, etc.) does not introduce
errors. Some of those comparisons (e.g. edits in layout) can be totally
push-button.
It took 6 weeks to go from final RTL to tape out for that design.
Equivalence checking saved us at least 1 to 2 weeks.
- Chrystian Roy
LSI Logic
---- ---- ---- ---- ---- ---- ----
From: Mohammad Imam <mimam@micro.ti.com>
John,
I also do not agree with Don Mills. We have used Chrysalis a lot for past
year and half or so.
We have found it out very useful, in many respect. RTL-> GATE comparision
is no problem for us now, as we have automated it almost compeltely. Of
course due to hierachy problems some times we have difficulties, but with
open eyes writing correct rules is easy. :-)
We have used it for different purposes too. In multiple instances, we were
very close to PG and bugs were discovered, and there was no time to
resynthesize the block, we made changes in RTL, and corresponding gates
changes were done, and using Chrysalis, we were able to fix and prove
the netlist very fast.
- Shahid Imam
Texas Instruments
---- ---- ---- ---- ---- ---- ----
From: Tom David <tomd@silogix.com>
Hi John,
With respect to the equivalency checking thread on ESNUG 321, folks should
check out Verplex's tuxedo suite of tools... I understand they're much
faster than Chrysalis and can handle things like precharge-evaluate logic
and hierarchy mismatches between RTL and gates, etc.
- Tom David
SiLogiX, LLC.
|
|
