( SNUG 03 Item 14 ) ---------------------------------------------- [05/14/03]
Subject: Synopsys Formality, Verplex LEC, Mentor FormalPro
THE EVIL EMPIRE WINS: Over the past 3 years I've been tracking how users
viewed the infamous Formality vs. Verplex war. To recap the story, back in
SNUG 01 #15, I saw 82% of the user letters at pro-Verplex vs. 18% of them
being pro-Formality. That was 2 years ago. Last year, it was a 54% to 46%
Verplex to Formality split. (See SNUG 02 #10.) This year, I'm seeing a
30% pro-Verplex to a surprizing 70% pro-Formality split in the user survey
responses! Whoa! That's 14 pro-Formality to 6 pro-Verplex letters. (I'm
disregarding the added 6 "both tools are equivalent" letters here because
they're neutral.) The Evil Empire wins this round.
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%)
Dataquest FY 2001 Formal Verification Market (in $ Millions)
Synopsys Formality ###################### $22.4 (47%)
Verplex ##################### $21.5 (45%)
others #### $3.8 (8%)
"I think everyone likes Verplex. We decided to go with Formality."
- [ An Anon Engineer ]
"Other group uses Verplex and their feedback indicates they like it."
- Ross Swanson of Flextronics
"Only used Formality and it's getting better."
- Bengt-Erik Embretsen of Zarlink Semiconductor
"No idea on the other tools - we use Formality."
- Lance Flake of Maxtor
"We are using Formality and Verplex (and Chrysalis DesignVerifyer for
legacy modules.) Our decision was Formality as our prime tool.
No question Verplex is the more performant tool and based on our
experience and the reports from other design centers Formality seems
to fail more often on complex designs. However none of the tools are
perfect and we found bugs in both, all of them are solved. Currently
we do not have any issues with Formality on our projects.
The Synopsys guys did a very good job in improving the usability of
Formality. Their debugging process is very intuitive and cuts down the
debugging time. Something I really like is that you can connect at any
point the GUI to the Formality engine.
License cost: advantage - Synopsys Formality."
- Christian Glassner of National Semiconductor
"We use Formality. I don't use it myself but the people who use it seem
satisfied. I can't compare it with the other products though."
- Amar Guettaf of Broadcom
"We committed to Formality, and it is a vital part of our flow. We've
used gates-to-gates on more than one project, and gates-to-RTL on one
project. We actually tried using it to limit the amount of gate
simulation this latest project, but we then chickened out and ran lots
of gate sims anyway."
- Curtis Jones of Hewlett-Packard
"We used Formality, and I believe it was effective. We haven't looked
at the competition in quite a while."
- [ An Anon Engineer ]
"I chose Formality because our customer was using Formality, so I wanted
to make sure I used the same tool as them. Having made this choice, I
found the support from Synopsys to be prompt and helpful. I have not
come across any major problems in applying the took that Synopsys could
not resolve."
- Alan Duffy of Motorola
"Formality is not user friendly, crash each time almost, but we use it."
- Rex Tung of InProComm
"Formality is the leader, Verplex has a great product (we evaluated them
as essentially equal), but they would have to beat Synopsys on price to
win because we already buy everything else from Synopsys."
- Patrick Allen of Infiniswitch
"With the Formality vs Verplex one there's a real issue about the
confusion over DW components. Synopsys encrypts the original RTL
(actually VHDL I think) and so Verplex doesn't have a chance to compare
them. Synopsys publishes non-synthesizable RTL versions that are
efficient for simulation, but Formality doesn't use these to check
against the netlist. Formality is checking that DC doesn't synthesize
DW parts incorrectly (because DC uses the same encrypted source) but
there's no formal verification against the VCS simulation model - which
you use to pass your functional tests!
Having any simulation vs synthesis differences is an integrity issue
for an equivalency checker. Thing is, only Verplex gets bad press on
this because it does not handle DesignWare components (note that
Formality and DC cannot read in the VCS simulation descriptions of
DW - even something as simple as the barrell shifter.)
BTW, I thought that your recent article had the best EETimes headline
I've ever seen - "VHDL, the new Latin" made me chuckle for days."
- [ An Anon Engineer ]
"I recently did an evaluation of Synopsys Formality, Verplex LEC, and
Mentor FormalPro. The design that I used was very large: it had 70
RAMs, 30 k flops, and 200 k gates. It's logic is predominantly
control logic and contains CRC generation. The logic also has hand
instantiated DesignWare components. I did this comparison 2 months
ago and used the following
versions: Formality 2002.12, LEC 3.3.2.a, FormalPro v4-4_2-8
setup:
* Formality was clearly the easiest to setup. The VCS style read is
still a little buggy, so I was not able to use it cleanly.
* LEC was not too hard to setup. The VCS style read of RTL worked
well. The LINT checking built into LEC was helpful. The instantiated
DesignWare presented a problem, since ECC components were used, I
could not just blackbox them. My solution was to write a gate
netlist version of the ECC block and compare it in formality, and
then read the gate ECC with the RTL.
* FormalPro took a little more work to setup. FormalPro uses five
input files (rules, match, constraint, blackbox, formalpro.ini) to
setup the verification environment. They were not hard to setup,
but took more effort than LEC and Formality. I needed to do the
same DesignWare ECC trick as in LEC.
match & verify:
* Formality worked pretty well. I did need to use set_constraint to
declare some case statements as 1hot. The verify also left some
"Not Compared: Unread" points, which turned out to be self fed
spares.
* LEC took some effort in this stage. I needed to experiment with the
Mapping Method to get the most matches, "Name Guide" seemed to work
the best, but I still needed to use the GUI to match a few unmatched
flops. I needed to add 1hot directives in an earlier version of LEC,
but not in the most recent version. The verify reported that 'every'
flop (including the scans) were checked. A big problem was that the
match and verify took nearly 3 times longer than Formality or
FormalPro. LEC also required stepping through compare strengths
to complete, I needed to use to the undocumented "ULTRA" effort to
complete the verify. NOTE: I ran LEC on many other designs as well,
they all had more minor problems in matching comapre points, but none
required higher than medium compare effort.
* FormalPro was not able to complete this stage with every flop
defined. One problem was that some self-fed spare flops in the
design were discarded somewhere between the reading of the design
and matching. A second problem was that some of the unmapped points
could not be found in any report. Specifically, benign points were
reported in the log, but not found in a report. Another problem was
that it was hard to find a report that correlated to all of the
categories in the log file, the Target Display in the GUI was really
the only way to understand what happened to every compare point. I
also needed to declare some state machines as 1hot. I did not put
much credibility into the results of FormalPro since I could not
account for every flop.
debug:
* Formality is very limited in it's ability to debug problems. The
error candidate generation is completely useless. I broke a single
cell in the design, and got over 6000 nets as error candidates (over
500 are 100%), including all clk tree nets and scan nets. Tracing
through the logic on the GUI was also difficult, case statements
were confusing to follow with the don't care generate blocks, and
since the entire module was displayed it was hard and took a lot of
time to trace problems. The pattern display was really the only way
to debug a problem, but was cumbersome to use without being able to
trace the logic easily.
* LEC was clearly the best in debug, for the change I forced, I got
2 100% error candidates, and a total of 10 error candidates. One
of the 2 100% error candidate was the cell that I changed. The
Debussy tracing was never necessary (due to the accuracy of error
candidates), but I found it much easier to trace the logic, mainly
because it was easier to close entire cones to leave only relevant
logic.
* FormalPro. I did not use the debug features in FormalPro since I
could not account for all flops in the design. When I take the
number of target points generated, the pins and BBpins matched,
but the DFF was only 95% of the flops in the design (not counting
spares).
Overall, Formality was the easiest tool to setup and run, but useless
on netlists with an verify error. For netlists with problems, it was
much much faster to take the time to setup LEC, match the compare
points the tool couldn't finish by hand, wait the 3x verify run time
and easily find the problem than to use Formality to debug. FormalPro
seemed to work really well, but could not close this design because it
did not verify all compare points in the design."
- Joe Hasting of Agere Systems
"This is very dependant on what version of who's tool you're using. In
general, Verplex gave Synopsys a kick in the pants, and Synopsys
responded aggressively to close the gap. I've had no exposure to
Mentor's FormalPro, but it is definitely not garnering user's mind
share. Perhaps it's just my Mentor salesman, but it definitely does
not jump to mind when talking about formal verification. And Cadence's
entry? Yet another hole in their line. I'd put good odds on them
buying Verplex to plug this hole."
- [ An Anon Engineer ]
"Formality vs Verplex. About the same. I used both (last year), now I
only use Formality. I guess Formality will always be ahead for DC
designs. They just fix it to cope with every new tweak to DC.
What I'd really like to see is a formal verification tool that can deal
with Synplicity's optimized designs."
- Santiago Fernandez-Gomez of Pixim, Inc.
"Despite Formality has done really good progresses in the past 2 years,
Verplex Conformal LEC is still a step ahead. Verplex has a really
powerful HDL reader and a very good and reactive user interface
reducing the setup and debug time, which requires the designer in front
of the tool. The runtime and memory consumption are also much better
and LEC is able to handle more complex logic cones on which Formality
remains inconclusive. However Formality remains usable in most of the
cases and gives acceptable performance."
- [ An Anon Engineer ]
"We like Verplex and are looking for funds to buy it. Formality failed
us on a medium complex design. No time to look at FormalPro."
- [ An Anon Engineer ]
"Verplex is very good. Runtime and accuracy are very good. Formality
is so-so."
- Tie Li of Applause Technolgy
"Who cares? I've yet to do a single design in which formal verification
was a requirement or a necessity. In my opinion, equivalence checking
is a crutch tool to catch bad coding habits."
- [ An Anon Engineer ]
"I would say that Formality and Verplex are on par for performance, but
Formality has problems having too much access to under-the-hood
information Synopsys' synthesis. Refer to my ESNUG 406 #10 letter.
I'd like to play around with Mentor's FormalPro but haven't had the
chance."
- Tomoo Taguchi of Hewlett-Packard
"Used both Formality and Verplex. I prefer Verplex. Easier to use.
Faster results. Less memory (1 year old data). Formality is not
keeping up with DC and VCS, which has been a real pain. Try using some
Verilog-2001 constructs: VCS and DC are OK, but Formality doesn't
support them. I'll bet the same thing will happen with System Verilog.
The lack of consistency between the product lines is shocking."
- [ An Anon Engineer ]
"Verplex by far blows away Formality in speed and capacity. Formality
was recently improved in those areas, but Verplex is still ahead. We
ran Formality for our chip in 6 blocks, from 15 minutes to 8 hours for
the different blocks. When we put the *whole* device into 64-bit
Verplex, we were able to run the whole thing in about 24 hours. (That
was using 1 generation of Sun workstation ago on a SUN Ultra 80's). I
would not even contemplate trying that in Formality. By the way, for
all of this I was talking RTL-to-gates. Gates-to-gates (for example
pre-scan to post-scan) is approx 4 times faster.
Formality is better for debugging, since Verplex breaks down the logic
to its constituent AND and OR gates, at least with the libraries that
Agere provides. So we use Formality at times when we have a small
block identified that we cannot see why there is a Compare Failure in
Verplex.
Formality is also better at mapping (matching) endpoints which is an
effort in the Verplex setup, although Formality's automatic methods can
sometimes match the wrong points. Then you are totally stuck.
Our layout team (Agere Allentown+NewJersey) uses Formality for
gate-to-gate runs on a block basis (approx 1 million gates) to verify
that any cell changes, power-up, buffering, etc. has maintained the
logic correctly, because of the ease of setup (endpoint matching, etc),
and the ease of diagnosis in Formality.
Looked at Mentor, did not have the capacity to match Verplex, so why
add another company to our mix?"
- Bob Lawrence of Agere Systems
"Verplex is definitely ahead in the market. FormalPro is catching up
fast. It has the speed offered by Verplex, but doesn't quite have the
robustness of Verplex."
- [ An Anon Engineer ]
"We used Verplex. Their tool works, it's fairly easy to use, and fairly
easy to debug. Have not evaluated Formality & FormalPro. One worry
with Formality is using a checker from the same tool vendor as our
synthesis tool. Just no reason to switch. Have other pressing
problems to solve."
- Tom Thatcher, ex-Agilent and looking
"The only problem is Synopsys phasing out Chrysalis and replacing it
with Formality. We had macros that worked perfectly with Chrysalis
but simply did not work with Formality. Synopsys couldn't figure
out why either."
- [ An Anon Engineer ]
"Chrysalis is a lousy tool and it should die. Verplex is the best but
we will move to Formality because we are trying to buy all the tools
from the same vendor as a part of a package deal. I'm not familiar
with Mentor FormalPro."
- [ An Anon Engineer ]
"We migrated from Chrysalis to Formality. Our experience has been good
so far. We have seen designs which were taking 3 days to verify using
the old Design Verifyer getting verified within couple of hours using
Formality. Also the number of matching points we have to give manually
to Design Verifyer was much more than that required by Formality."
- Srinivas Jammula of Procket Networks
|
|
