( DVcon 04 Item 9 ) ---------------------------------------------- [ 05/26/04 ]
Subject: Cadence Verplex, Synopsys Formality, Mentor FormalPro, Prover eCheck
IT'S NOW A BUSINESS DEAL Long story short, Verplex used to rule the EC biz.
They would repeatedly embarrass Synopsys Formality again and again in the
user surveys. A humiliated Synopsys goes back and reworks Formality while
Cadence aquires Verplex.
"What tool do you use for equivalence checking?"
don't use : ########################## 26%
Cadence Verplex : ###################################### 38%
Synopsys Formality : ############################### 31%
Mentor FormalPro : #### 4%
Prover eCheck : # 1%
homebrew EC : #### 4%
This is bad news for Verplex because users are now seeing that's its roughly
equivalent to Formality and vice vera. Instead of EC tools being a fiery
technology battle, it's now just a business deal. Whoever has the best
saleman talking to you wins the business. Not a good situation for a tool
that used to rule this realm.
We are using Cadence Verplex. I think all the three tools seems OK. It
was just a preference of who is cheaper.
- Jithendra Madala of QuickSilver Technology
I've used both Verplex and Formality. No problem with either.
- [ An Anon Engineer ]
Both Verplex and Formality. Depends on the team.
- [ An Anon Engineer ]
Have used Verplex when it wasn't Cadence yet. It was okay then, but I
would not touch it now, because of bad experiences with Cadence tools
and support (lack thereof). Only use Cadence simulators because they
haven't needed support. We're currently using Formality. It performs
similarly to what I remember of Verplex. I think it is six of one,
half a dozen of the other.
- Michiel Vandenbroek of China Core Technology Ltd.
We use both Synopsys Formality and Cadence Verplex. I think they are
roughly equivalent now. No preference.
- [ An Anon Engineer ]
Cadence Verplex. It's sufficient and runs well, easily to use. I think
it has equal capabilities to Formality and FormalPro.
- [ An Anon Engineer ]
It's Verplex or Formality. I can't remember which right now.
- Jerry Roletter of ATI
We use Verplex and Formality. We've found that using only one is
dangerous. You must use both to check each other.
- [ An Anon Engineer ]
Verplex. Each vendor's tools have about the same pluses and minuses.
It's a wash.
- Terry Doherty of Emulex Corporation
Verplex is the only one we have seen that can perform RTL to gates on
large multipliers. It is still the leader.
- [ An Anon Engineer ]
Synopsys Formality. Mostly just used it because we had it handy.
Haven't really checked out the competition.
- [ An Anon Engineer ]
Formality. I think maybe Verplex is more aggresive.
- Luo Min of Northwestern Polytechnical University, China
We use Verplex.
- Scott Runner of Qualcomm
We recently changed from Formality to Verplex, due to better Verilog 2000
support at a given critical time.
- Yuval Itkin of Metalink Broadband, Ltd.
Synopsys Formality. I'm reasonably happy RTL to Gates. Gate to Gate
is fine.
- [ An Anon Engineer ]
We use Formality. However now that we do many more FPGAs we have not
been able to use Formality as it is not supported by the EDA tools. This
is a huge problem for our large FPGA designs. We have found bad logic
caused by Synplify and Quartus and the only way to hunt these down is to
s....i..m...u...l....a..t....e..... Argh. Both companies claim to be
working on formal verification support.
- Jay Adams of Marconi Corp.
Verplex: straightforward to use and powerful. I haven't explored the
others.
- Aviva Starkman of Northrop Grumman
Cadence Verplex.
- [ An Anon Engineer ]
We use Verplex. Good tool but the documentation is really poor. Most of
our problems could be fixed with some undocumented tool options. Verplex
always wanted to send us to classes instead of fixing the documentation.
It also had quite some issues with RTL vs. Netlist on complicated RTL
coding. Particular with datapath elements (mult,add...). As far as I
know they addressed this shortcoming with a new datapath extension but
they expected us to send them some $$$$.
We did a eval of FormalPro and could not observe similar issues. It
was clearly superior. Unfortunately Mentor does such a good job not to
tell anyone about some of their great tools that it was too late by the
time we got aware of FormalPro through Deepchip/ESNUG.
- Karl Kaiser of EcoLogic GmbH
Verplex. But it has not been updated to keep it competitive.
Considering Mentor's FormalPro.
- Winston Worrell of Microsoft
We use Formality to verify truncated/internally rounded arrays and adders
written as RTL against hand-crafted gate instantiated netlists.
18 months ago we looked at FormalPro, at the time it could only manage
to do a 12 by 12 multiplier (I think this was with generic BDD type
solvers) and in order to verify a 17x17 multiplier we had to run a 12x12
type multiplier verification 1024 times - i.e. exhaustive/formal mix.
Their R&D team had it for a while & that was the best they came up with.
Then we heard that one of our customers had verified a 24x24 multiplier
with Formality!
We evaluated it and found it could anything up to 64x64 quite happily
(we stopped there only because of requirements not because of tool
limits - using BMDs I think). There is however an issue that a
multiplier whose first few rows do not use Booth encoding but then the
rest does is proving tricky in Formality. I think sometimes it works,
sometimes it doesn't. (We haven't worked out why yet.) We then found
a way to do truncated arrays (that is make an array and get rid of
columns before the reduction.)
We are now using Formality to do any reductions of partial products
(e.g. a+b+c+d etc.) This is slightly tricky and not fully working yet.
Formality does retiming very well.
We don't use these tools to debug, we don't use the GUI, we don't care
too much about memory -- it's about verification not too much about
resources.
Then we heard that Verplex had improved leaps and bounds. It doesn't
do retiming well at all.
Currently we use Verplex and Formality.
Formality for retiming and if it can find a multiplier or a reduction to
gets its teeth into we let it and it works well. Verplex we don't use
for retiming, if Formality can't find some pre-verification to do then
we usually resort to Verplex. Verplex seems better at generic BDD type
verifications even if some datapath blocks get lost in the netlist. You
have to tell Formality where the datapath blocks are and if it finds
them it works. Verplex can be given a netlist and it can find them for
itself, but once found, it is less powerful.
- Theo Drane of Arithmatica
We use Verplex for long time and we are very happy with it.
- [ An Anon Engineer ]
I'm pretty happy with Formality. If you're used to DC and PrimeTime,
Formality is quite easy to pick up and be productive with. (Though
I wish Synopsys had made commands identical to those tools, rather
than just "similar" -- get_cells vs. find_cells and collections vs.
lists, anyone?)
I just can't get used to the reporting from Verplex. The messages don't
seem consistent or give me the level of detail I'm looking for, and
Verplex refuses to come right out and say verification "succeeded" or
"failed", like Formality does.
- John Busco of Nvidia
Synopsys Formality. We haven't compared it with anything else. It does
our job fine. Can be difficult to debug when failures happen though.
- Samuel Russell of Ceva, Inc.
We use Formality and I don't know its rivals. So I can't tell who is
ahead or behind.
- Frank Lier of PACT XPP Technologies
We use Formality. Short term Verplex is ahead, mid-term I see Formality
technically reaching Verplex. FormalPro is out of the play for the
moment.
- Umberto Rossi of STMicroelectronics
Formality is the most popular equivalence checker in our company.
Although some groups in our company use other tools such as Verplex,
mostly we rely on Formality for design sign-off. For example, recently
we were having problems in verifying RTL vs. Gates for an ARM9 micro-
controller. We solved the problem by using SVF (Setup Verification
for Formality), which is a composite log file generated by Design
Compiler during synthesis to log all setup information including
register and net name changes, register duplication, etc. (Our attempts
to enter the information manually or in semi-automatic ways in Verplex
proved to be tedious and error-prone. Formality solved this problem.
Another reason why we like Formality over Verplex is its capability to
understand DesignWare components in a design and treating them
appropriately.
- Mohammed Zaman of Analog Devices, Inc.
Formality for the moment, we might go for Verplex if necessary. I think
Verplex is ahead, but Formality is not that bad.
- Remi Francard of STmicroelectronics
Verplex, but I use it rarely.
- Stefan Rohrer of Micronas GmbH
Synopsys Formality is no doubt is ahead. Using Formality.
- Ajit Madhekar of ControlNet India Pvt Ltd.
We are using an internal tool that was developed in IBM. I'm not
familiar with rivals' tools.
- Dorit Moshe of IBM Israel
We are in the process of switching from Formality to Verplex. We have
not yet obtained the licenses for Verplex, so I can't say which one
I think is better.
- Greg Arena of Intel Corp.
We use Verplex, it worked well for some of the team in a past life.
- Pete Cumming of Icera Semiconductor
Verplex. We compared them 3 years ago, and Verplex won hands down.
Support for the tool has gone down since Cadence purchased them though.
We have found lots of other uses for Verplex (converting Verilog to VHDL
is one) and would not do another design without it.
- [ Kenny from Southpark ]
Verplex. Verplex.
- Carl Harvey of Cirrus Logic
Cadence Verplex. We also evaluated Formality at time of purchase (about
a year ago). Formality was not able to handle our 2 million gate VHDL
netlist. Both tools were able to check the Verilog version.
- Tim Ma of Mykotronx
I have played with Prover eCheck -- it is very easy to use and runs on
a PC which is very convenient. But I think formal verification tools
are overpriced and hope that they can be bundled into other tools in
the near future.
- John Dean of Philips Research USA
Our design house performs synthesis and for equivalence checking they
use Synopsys Formality.
- Willem Sloof of Philips Microdisplay Systems
We use Formality - it's a pain to set up, but it's no worse than what we
used to struggle with (Chrysalis).
- [ An Anon Engineer ]
We use Formality.
- Dan Steinberg of Integrated Device Technology
We are using Mentor FormalPro. We were satisfied with the gate level
equivalence checking. It is fast, easy to learn, easy to script. We
had once some problem with RTL-to-gate equivalence checking but for the
rest of the circuit worked again very well. We have not performed any
comparison with other equ check tools. I have heard that eCheck from
Prover Technology is also good.
- Premysl Vaclavik of On Demand GmbH
Mentor FormalPro. Haven't used the rival ones.
- Rainer Mueller of Oasis Silicon Systems
Currently Verplex. System Verilog support may push us towards
Formality.
- Mark Curry of Texas Instruments
We use Formality and DesignVerifyer. Formality compare point matching
is problematic for optimized designs and not able to handle transistor
design. DesignVerifyer is used by the processor team design. Will
look into Cadence equivalence tool solution.
- [ An Anon Engineer ]
Verplex was recently acquired by Cadence, and their bread and butter was
formal verification. Verplex is a rock solid formal verification tool.
Its fast, intuitive, and you don't have to be a "power user" with 5 years
experience of doing nothing but running that specific tool to get the
job done. That's the biggest reason Verplex is so popular, and powerful.
Unlike some of its competition, you don't have to be able to read
Sanskrit to use it.
As far as enhancements go, I would like Verplex to have the ability to
"black-box" modules up front. I requested this type of enhancement a
while ago, but have not seen it yet. Case in point, our last design had
a wrapper for each RAM. The RTL versions were clean, but the
gate-versions had BIST logic, etc. that our vendor inserted (they owned
the BIST insertion). It would have been great to have been able to add
a section to our scripts that black-boxed the wrappers upfront, rather
than having to weed through all the warnings that popped on the BIST
logic. And, it would have been even nicer, because you would not have
FV checking the two memory arrays against each other, which would
have sped up the FV run.
Having said that, Cadence did buy them, and we all know what tends to
happen to acquired tools... My hope is that Cadence can avoid the
classic pitfalls as they "assimilate" the Verplex product line.
- Mike Bly of World Wide Packets, Inc.
Started using Formality but found several design bugs while Verplex was
demoing their tool to us that Formality missed. Formality is still not
to be trusted although we use it for block level checks. Final checks
must run through the Verplex tool.
- [ An Anon Engineer ]
Verplex and FormalPro. Depending on the application one has advantages
over the other. None of the tools do it all.
- [ An Anon Engineer ]
We use Verplex for RTL-to-Gate checks. Haven't used the other tools.
- Brad Hollister of NetSilicon, Inc.
We would like to be able to compare FPGA netlists (that we use for
prototyping) against ASIC netlists -- taking into account where we
know they should be different and where we know they should be the same.
So far we have spent some time evaluating Formality, but were unable to
achieve this ASIC-to-FPGA comparison. On the positive side, Formality
was extremely easy to setup and use, and did find some differences
between the results of different synthesis runs that where meant to be
based on the same RTL.
We are yet to evaluate any of the other offerings.
- [ An Anon Engineer ]
We use Formality for equivalence checking. We've had it choke on some
of our larger designs as of late, but our AE helped us get around the
problems. I don't think we've looked at the competition for a while,
so I can't really comment on how things rate.
- Jonathan Craft of McData Corp.
Synopsys Formality. Recent eval showed Formality & Verplex essentialy
even in capability, although Verplex currently has better support for
Verilog 2001. Synopsys ESP-CV add-on was a big plus in the eval for
behavioral verification.
- [ An Anon Engineer ]
Verplex is the standard in equivalence checking.
- Subbu Muddappa of Woodside Networks
We tried Mentor FormalPro as a rental/extended evaluation on a
3 million gate ASIC with marginal results.
- Brien Anderson of Siemens Medical
Most of the company uses Synopsys Formality. Full custom designs still
use Synopsys Chrysalis due to handling of transistors, but will be
moving to Formality.
- [ An Anon Engineer ]
We use Mentor's FormalPro. We did an evaluation with the two others
mentioned a couple of years ago. Mentor was found to be easy to use and
it didn't throw away a good chunk of the circuit. It made me nervous
when one of its competitors threw away a significant number of compare
points. It was able to complete circuits that its competitors had
problems with. I think one of the most compelling facts about it is
that our foundry who uses one of the other two, has started having us
verify the final circuits with ours because they couldn't get their
tool to do it in a reasonable time.
- Maynard Hammond of Scientific Atlanta
I have a design (actually an SHA-1 hashing algorithm) that I first
started to try to verify with Formality mid-last year. With a straight
through run it proved too hard to verify and gave up after a couple of
days, in particular a large adder tree that had had name changes in some
parts. It required recourse to a Formality expert and a raft of
set_user_matches in order to get a successful verification.
Having just upgraded to Formality 2004.03, I get a successful
verification after around an hour without any manual matches required!
This version seems to be a big improvement over others, as I have tried
2003.06, .09 and .12 and the verif would not complete on any of these
without manual intervention.
I'm hoping that run time might be improved with their introduction
of svf datapath info from DC, which I believe is in the June release.
- Tom Thomas of STMicroelectronics
Verplex
- [ An Anon Engineer ]
We're using Formality. We never got stuck with it so far. Verplex is
probably still ahead though.
- Laurent Claudel of Wavecom
We have an in-house formal tool for this. It is currently at least as
good as anything else out there.
- [ An Anon Engineer ]
We use Formality. FormalPro is behind. Verplex is good as well.
- Boaz Ben-Nun of Starcore DSP
Synopsys Formality for equivalent checking.
- Gao Peng of Tongji University, China
Cadence's Verplex. Faced no problem in using it and it also has great
technical support. We will stick with Verplex.
- Inder Singh of iVivity, Inc.
We use Cadence Verplex.
- [ An Anon Engineer ]
Currently evaluating equivalency checking tools.
- [ An Anon Engineer ]
We use Synopsys Formality, the 2002.03 release was much improved over
earlier releases with a new graphical debugger. Keeps getting better.
We have done dozens of metal-fix ECO's by hand, comparing verified RTL
against the hand-fixed netlist, and formal verification is the only way
to get good confidence in our fixes. Another best "bang for the buck"
tool, we've gotten our money's worth.
- Nathan Dohm of StarGen, Inc.
Not used.
- Chandresh Patel of Ciena Corp.
We use Formality with major unhappiness over their slow support for new
language constructs (first Verilog 2001, now System Verilog). Is
Verplex still being updated by Cadence? I haven't seen any sign of that
happening. I liked Verplex a lot but I think they're toast under
Cadence's ownership. For anyone who's using DC the new SVF scripting
mechanism to guide Formality is both useful and a real block (because
it's so useful) to using anything other than Formality.
- [ An Anon Engineer ]
We have been using Verplex for several years and recently started to use
Formality as a second source. In comparison, the run time for both are
more or less the same. Verplex is better in verifying mulipliers, while
Formality is good at automatic loop breaking (takes a long time, though)
supports Verilog models better, and easier to verify designs with extra
ports, caused by clock tree synthesis, or scan insertion. Overall, both
have good quality.
- Haizhou Chen of Marvell Semiconductor
When we bought Verplex, it replaced Chrysalis and beat Formality, but
that was 3 years ago. Don't know who's ahead now.
- Mark Andrews of EFI, Inc.
We use Verplex for equivalence checking.
- Hsing Hsieh of Hitachi
Nothing yet, under consideration...
- Sandro Pintz of Precision IO, Inc.
Don't use equivalence checking for FPGA designs.
- Don Monroe of Enterasys Networks
We use Verplex. It still runs twice as fast as Formality. Never
tried FormalPro.
- Edmond Tam of Global Locate, Inc.
We used Verplex. Seemed to do a good job.
- [ An Anon Engineer ]
Verplex. No basis to compare since no evals lately.
- [ An Anon Engineer ]
We use Formality. It works. No opinions on rivals.
- Christine Gerveshi of Agere Systems
Verplex.
- [ An Anon Engineer ]
Just starting to use Formality, not much experience yet.
- Greg Schmidt of General Dynamics
We use Verplex, I believe, but I'm a little removed from this tool usage.
- Jim Lear of Legerity
We havent done equivalency checking on our own, our partner has done it
for us. We will probably buy a tool next year.
- Bill Dittenhofer of Starkey
|
|
