( SNUG 02 Item 10 ) -------------------------------------------- [ 5/15/02 ]
Subject: Verplex, Chrysalis, Synopsys Formality, Mentor FormalPro
THE EMPIRE STRIKES BACK: Last year users crucified Formality in the SNUG'01
Trip Report. It was brutal. Out of the 27 e-mails I received then, 22 were
pro-Verplex and only 5 were pro-Formality. (See SNUG 01 #15.) Users took
great joy in praising Verplex while trashing Formality. But it appears that
at least some of the Synopsys Formality R&D staff noticed this and spent the
last 12 months fixing things. This year, there were 28 e-mails; 14 were
pro-Verplex; 12 were pro-Formality; 2 pro-Chrysalis; and 1 pro-FormalPro.
Formality hasn't 'won', but it's definitely now a viable rival to Verplex.
Dataquest FY 2000 Formal Verification Market (in $ Millions)
Synopsys Formality ############## $14.0 (44%)
Verplex ########### $10.5 (33%)
Avanti/Chrysalis #### $4.1 (13%)
others ### $3.2 (10%)
"Gee whiz, I didn't even realize that Mentor *had* an equivalence
checker, despite the fact that we have other Mentor products
in-house. They're definitely behind on mindshare, then. :-)
With Formality and Chrysalis, I can't see Synopsys continuing to
support two equivalence checkers, and I'm not sure which one will
win. Formality has the Synopsys in-house advantage, but with
formal verification, Chrysalis might be the right choice. It
might be the way for Synopsys to alleviate concerns about inbreeding
with Design Compiler.
Verplex hasn't made debugging any easier with its new versions
(disclaimer: I haven't played with version 3.3 yet). But it
continues to be powerful enough to handle all the designs that
get thrown at it here, and it's straightforward to set up and
run. And it's surprisingly fast. So, all things considered, I'd
say they're still ahead. They're definitely ahead politically,
and I have no complaints about the technology."
- Natalie Overstreet Ramsey of Vitesse
"We received a Verilog RTL design and a Verilog netlist that was suppose
to partially match. The design had 50 modules. We started with
Formality. Some of the Verilog files couldn't be read in. At that
point the guy that worked on this specific module tried to run
Verplex - and it passes smoothly. This happened on several modules.
To be fair with Formality, many of the modules caused Verplex to just
hang up and not finish. We tried them in Formality and they passed.
My conclusion is that there is no absolute 'best tool'. We are lucky
to have both so we can easily switch between the two and have the
best from both worlds. If someone would ask me which tool to use if
he can afford only one, I would probably say Verplex but definitely
recommend using both."
- Shimon Gur of Conexant
"Chrysalis and Formality have worked fine for me. Results are all
that count. Never heard of the other two. How many equiv checkers
do we need?"
- Brent Lawson of Texas Instruments
"We recently evaluated Verplex vs. Formality. Our conclusion was that
both tools are equivalent, and we decided to go with Synopsys mostly
for business reasons. We already taped out two designs with Formality
and although we found some bugs and some limitations (mostly in the
hierarchical RTL-to-flat-gates domain), we are very happy."
- Nir Sever of Zoran
"I have not tried Mentor's FormalPro. I feel Verplex is simple and best
for most of the ASIC designs. It works faster than others. It lacks
the TCL interface which Synopsys tools provide. We gave up Chrysalis
since it makes life complicated without providing any benefits."
- an anon engineer
"We consider Verplex the market leader with Formality a close
second. We expect to go with one of the two within the next
6 months."
- Scott Campbell of Motorola
"After 3 years, Formality still has problems verifying RTL vs gates for
multiple instanciated multipliers."
- an anon engineer
"Verplex, Verplex, Verplex. We did a benchmark on a DSP based block,
letting the FAE's of Verplex and Formality grunt it out. Verplex took
5 minutes on our block, Formality 55 minutes. Also taking advantage
of FAE's, Verplex was able to handle our whole chip (1M gates with a
lot of DSP). Formality struggled and was newver able to complete.
Currently we're running a gate-to-gate Verplex comparison on the same
design and it completes in 10 minutes on a 2.2GHz Linux box. Amazing."
- Scott Vincelette of Flarion
"In the middle of a tapeout, we were using Formality and Verplex LEC
to help verify our backend transformations. It turns out Formality
showed a failed verification, while Verplex showed a successful
verification. I was worried about the discrepancy, so I called our
Synopsys ACs to ask for their help. Quickly, they determined that
our design did indeed have real errors and isolated the errors down
to the faulty module.
It turns out our backend tools actually swapped port directions on
several lower level modules. While I could've reproduced this result
with Verplex, given the information from the Synopsys ACs, I'm glad
we were able to automatically identify the problem in time with
Formality. It's nice to avoid problems downstream. I'm glad that I
didn't trust the Verplex alone, and double checked with Formality."
- an anon engineer
"We tried Formality and got memory segmentation faults. Then we tried
Verplex and it was able to do a better job. The tool is simple enough
and quite fast. However we also found issues with arithmetic elements
like multipliers which forced us to recode some of our design to
satisfy Verplex. But Verplex Inc. was quite supportive helping us to
resolve the issues."
- Karl Kaiser of Resonext
"We use Formality (again 'short vendor list'). Only did gates to gates
comparisons."
- Curt Beckmann of Rhapsody Networks
"I've only used Chrysalis, no experience with the others. It does the
job, but you'd better have a big memory machine."
- Tom Moxon of Moxon Design
"Six months ago we started to use Formality as a equivalence checker
between the RTL and the final routed gate netlist. During out final
verification, our testbenches passed the netlist but Formality flagged
a difference between the RTL and gates. Initially we though that
Formality was incorrect, but as we looked into the problem more, we saw
that the testbenches actually did not cover all tests and there was a
difference.
From that moment on, Formality has become a important part of the
verification flow for us."
- Paul Kelleher of Motorola
"We did some evaluation and Verplex was the best overall. I can't
give any details."
- Hemant Kumar of Morphics
"Verplex is #1, Formality is #2, Chrysalis is at #3 and falling, and
FormalPro looks like another Mentor pipe dream at the moment. I got
on board with Verplex last year, and though we hit the 'hidden switch
nightmare' with this tool (which Synopsys customers are very familiar
with) overall it worked. Note that a big part of any formal
verification tool is a very good support structure. The ASICs I put
through the tool actually resulted Verplex support spending a day
with us to get the designs through."
- David Bishop of Kodak
"I had a chance to test Formality 2002.03 on our 1.3 M gate design that
we split into 3 partitions. There were several levels of hierarchy
under each partition. For this evaluation, we did an equivalence check
of our design's taped out netlist (scan+clktree+PhysOpt+ECO+etc.) to its
corresponding RTL (VHDL) source code.
Runtime Memory Usage Diskspace Gate Count
(min) (max) (bytes) (instances)
Par1 123 2,234 MB 21,829,047 499,240
Par2 64 1,431 MB 12,577,337 329,912
Par3 138 2,386 MB 18,853,207 533,912
With some mapping rules, we were able to verify all units successfully.
Most of our verification was done using bottom-up approach except for
Par2. Once a design was compiled into a container at the partition
level, it can be reused for comparison and debugging purpose. This
reduced compilation times when we worked on same designs. This version
of Formality has a hierarchical write script available to propagate
constraints down to lower modules for bottom-up compares. It also
picks up IEEE libraries and other Synopsys libraries automatically.
Formality can also read in libraries in db format for faster runtime."
- an anon Intel engineer
"Chrysalis is not in competition anywhere. It is an interesting fight
between Verplex and Formality. We recently did an eval on Formality
and found it quite useful. A design that was not even able to read
into Chrysalis passed RTL -> Gate in 4 hours using Formality."
- an anon engineer
"I don't see formal verification as cost justifiable for RTL designers.
If your RTL doesn't match your synthesized gates, chances are your
Formal Verifier is going to have problems, too, (or your RTL is cr*p)
and report lots of false negatives, etc. I do see a need for Formal
Verification on scan insertion, but I don't mess with that."
- Kevin Hubbard of Siemens
"Formality: It seems like Synopsys had to play in the FV market so they
just came out with something! Very limited, you can not do half the
things you can do in Verplex such as black-box pin mapping. Crashes
constantly and we saw some dangerous assumptions that were being made
during HDL read. The TPT was too much on Formality!
Chrysalis: I think when this tool was written, it was meant to do
EVERYTHING in the world! This is why it is very hard to use, too many
concepts to learn just for simple verification. The messages are not
clear, the same message can be in multiple places. The TPT for designs
that were easier to run thru Formality was large for Chrysalis. It was
good with aborted points but lack of other capabilities made it too
difficult to use.
Mentor FormalPro: Isn't this very old tool? Heard the name from some
of my co-workers, did not hear many good things!
Verplex's Tuxedo: If all above tools are 'og', then Verplex is
'EXCELLENT'. Two things top the chart, TPT i.e. it is lot faster than
any of the above tools, secondly the capabilties in the tool are very
impressive i.e. name mapping, black-box pin mapping, port mapping,
capability to save maps and re-use later, capability to write Verilog
for anything that goes in the tool (.lib, .spice, .vhdl), plus very
good logic-transistor-extraction capability. The switch b/w LEC/SETUP
mode is sometime a nuisance especially when some commands only work in
one mode and not the other, but this is very very minor compared to
other things we get from Tuxedo. The TCL interface moving forward is
a big plus, too."
- an anon engineer
"Verplex is still the king. This year, there's only one paper that
talks about Synopsys Formality. Furthermore, that paper talks about
using Formality in FPGA design, not ASIC design. I think Synopsys will
never have success in Formality. After using Synopsys DC for
synthesis, why on earth do we want to use another Synopsys tool to do
the equivalence checking? People would rather use the not-so-user-
friendly 'Chrysalis' to avoid using Formality."
- Andrew Cheng of Cisco
"One thing I can say about Formality 2002.03 is: no more MainWin!
Hooray! I can't be the only EDA user fed up with installing the
constant stream of O/S patches and deleting endless ~/.wind*
hidden directories.
Oh, and the new debug features in Formality are pretty cool, too :-)"
- Tom Fairbairn of 3Com Europe Ltd.
"We used to use FormalPro but found it pretty painful. We beat up
Mentor pretty hard and they started putting in some more useability
features which made significant improvement, and I believe they will
roll these into future releases. They were hierarchical block-by-block
hierarchical FV of RTL-RTL.
We evaluated Formality and found it a lot easier to use out of the box.
We now use Formality for RTL-RTL (VHDL to Verilog; as we supply both
flavors of IP) as well as RTL-gates. Formality has some very nice
debug features. We decided to buy it, and now support it to our IP
customers.
We also evaluated Verplex and liked it a lot but their business model
made no sense. They would not do Global WAN licenses. I also didn't
like the way they throw FUD about the Formality logic synthesis being
related to DC; even though Synopsys license the synth engine for
Formality from Interra."
- an anon engineer
"In one case, I inserted a bug in a design with a multiplier. Formality
can verify it (the previous version could not). But, with four bugs
added to the original design, even the current version cannot complete.
In both cases (with one and four bugs), Verplex LEC caught all the bugs
with almost the same runtime as when no bug is inserted."
- Hiroshi Furukawa of NEC
"I had a chance of using new Formality 2002.03 for my 15 million gate
design. I have been using 64 bit Formality because 32 bit version was
failed before. Now I have no problem to use 32 bit version and 64
bit version. In some cases, 32 bit version was faster. And the new
GUI become faster to be coming up. Most verification for such a
huge design could be done in 5 ~ 7 hours."
- an anon engineer
"We are using both Verplex and Formality. Verplex is winning now.
Verplex has a better GUI and better debugging tools, but has somewhat
of a bigger learning curve than Formality. Formality seems to be able
to do simple jobs quickly but is hard to work with when debugging
larger designs. Verplex is MUCH faster in run time. Synopsys is
putting more support into Formality so it should improve."
- an anon engineer
"I think that Verplex is more mature, but is not enough user friendly.
Mentor FormalPro is much more user friendly, easy to use, and gives
faster results but it's not enough mature."
- Gideon Paul of TeraChip
"I have about two years of experience with Formality and Verplex LEC.
We use them for block-level RTL2gate and full-chip gate2gate
equivalence check. For our million gate design, I tried to set
up both tools but finally integrated Formality into our flow.
The problems I saw problems with LEC were when some blocks ended up
with aborted points even if I set compare effort high and some blocks
rely on specific Verplex version to pass. Formality also needed some
workarounds like using an earlier version to read in the design. But
other than that, all 11 blocks went through 2001.08-FM1-SP2.
Runtime for each block in Formality was less than half hour on Solaris
and even less on Linux machines. Generally I saw 2-3X speed-up on
Linux machines. LEC used to be faster than Formality. Not any more."
- an anon engineer
"We began using Verplex after an eval that had also looked at Formality.
We'd found Verplex to be significantly easy to come up to speed on, and
it had better debugging capabilities."
- Neel Das of Corrent Corp.
|
|
