( DAC 00 Item 23 ) --------------------------------------------- [ 7/13/00 ]
Subject: Verplex, Synopsys Formality, Avanti Chrysalis, & Mentor FormalPro
DOG EAT DOG WORLD: For the past 18 months, Verplex has been embarassing the
hell out of the Synopsys Formality and Avanti (Chrysalis) DesignVerifyer in
the equivalency checking business. It now seems that out of left field,
Mentor is sporting a new EC tool that might unsettle Verplex, too!
"As long as we use DC of Synopsys I would not use Formality (problem:
same vendor, same software). Chrysalis we use right now - not easy to
use but some interestung features coming up. FormalPro (Mentor) and
TuxedoLEC (Verplex) promise much and seem to be worth a benchmark test.
At least they have a much better user interface than Chrysalis."
- an anon engineer
"I have been using Verplex LEC for the last few months to completely
verify a 3.5 Mgate SoC ASIC.
I have done RTL to gates, gates to gates, and prescan to postscan
comparisons. Once I became familiar with the best debug methodology,
I was able to debug problems on my own. Initially I needed some input
from the AEs.
I had problems verifying Synopsys DW multiplier and divider modules;
divider extraction is currently available in a pre-release form only,
but did successfully compare an 8 bit divider. The multiplier compared
once the wallace type was set before reading in the design.
The scripting is very easy in Verplex. I have used Mentor Fastscan for
the last 6 years, and the style is similar, with add, set, delete,
report commands.
My favorite feature is the automated hierarchical compare commands.
With one command, LEC analyzes the design, and writes out a dofile
script which goes into each sub-block in turn, making it a black box
when complete, and working up the hierarchy. Then the "dofile" command
is used to execute the script which was written out. A few days ago I
wanted to compare the top level, having completed the major sub-blocks.
The compare got stuck at 83% for an hour, so I used the hierarchical
compare command. It took 30 minutes to analyze the complete RTL and
gates, and a further hour to run the compares up the hierarchy.
Although we ran some gate level simulations (which hardly fit the 4 Gbit
address space limit in 32-bit Solaris) no problems were found. RTL to
gates comparison did find some problems, and they would have been very
hard to find in simulation. They were mainly related to optimizations
made for timing.
Although the idea of learning a new tool takes time and effort, I have
found Verplex LEC to be powerful and simple in design, and helpful in
debugging a complex ocean of gates!
- Guy Harriman of Cisco (VG 1.13)
"We've been evaluating Avanti DesignVerifyer, Synopsys Formality, Verplex
Tuxedo LEC and Mentor FormalPro. The first two have been on the market
for some time and seem to be architectured in a non-state of the art
way. They consume a lot of memory and have long compile times. The
latter two (LEC & FormalPro) are rather new and seem to be better
architectured. Their run times are over 3 times faster than Formality
and over 6 times faster than DesignVerifyer (in our test case: ~2M Gates
gate2gate equiv. check). Tuxedo's memory consumption is 3-4 times less
than the first two. FormalPro even 2 times better than Tuxedo.
Both Synopsys and Avanti have come up with improvement plans, but these
plans do not come close to current performance of Tuxedo & FormalPro.
Interesting to hear at DAC is that Verplex continuously indicated their
performance benefit compared to Synopsys and Avanti but 'failed' to name
Mentor. It seems that Mentor is even outperforming Verplex.
We're going for Mentor FormalPro."
- an anon engineer
"Verplex looked really good - I think they very well may kill Chrysalis,
now that Avanti will ruin it."
- an anon engineer
"Formality numbers on multipliers are becoming pretty impressive 256x256
RTL to Gates (wallace, booth, csa you name it) in less than 20 minutes!
Take that Verplex, you EE Times number dropping fools! I'd be
interested if anyone has any feedback here as far as what Verplex was
saying, however they now have momemtum.. not sure if it is too late for
Formality the TAM for equivalence checking at $100,000 per copy may not
be there?"
- an anon Synopsys employee
"We have also tried out formal verification with the Chrysalis tool last
year. We found that the approach is promising but immature for larger
designs. Especially arithmitical blocks was hard to verify."
- an anon engineer
"Didn't really look into this much. Chrysalis (Avanti) and Formality
(Synopsys) are still the big ones. Verplex had a booth again this year,
but Formalized Design and Verysys didn't this year - don't know if
they're still in business."
- an anon engineer
"Verplex LEC: have used it - Problem: the VHDL is so low level that you
and synthesis can't read it anymore - but it's absolutely equivalent."
- an anon engineer
|
|
