( DAC 03 Item 19 ) ----------------------------------------------- [ 01/20/04 ]
Subject: Cadence Verplex, Synopsys Formality, Mentor FormalPro, Prover
GOOD BUY! Cadence bought Verplex this year. From the business perspective
Cadence got a first class company & tool. Now the question most Verplex
users have is whether being part of Cadence will mess up Verplex or not.
Only time will tell. In the rivals department, Synopsys Formality has lost
it's "laughing stock" image of a few years back. Most of Formality's users
are conscripts, though -- they're using Formality because it was part of
a larger Synopsys package deal (just like those Cadence PKS users of the
tape-out counting days.) Mentor FormalPro is still trying to get beyond
beach head status in its attempted invasion of the EC market.
Verplex believes they now have 70%-75% of the equivalence checker
market, which is quite an impressive expansion in that market. They
are supposedly making their numbers and threw one hell of a DAC party
(again). Their tool has a library of the types of multipliers that
Synopsys uses and hence doesn't get stuck on those, and also has a
special version for datapaths (like Ambit or Module Compiler). They have
a new FPGA version where they are sort of teaming with Synplicity.
They also has a tool which can compare SPICE netlists to RTL or gate
level. It has a library of SPICE netlists for basic cell types and does
pattern matching (a competing tool would be Innologic but it works
entirely differently).
If they don't screw up Verplex this seems like a good move on the part
of Cadence. Verplex was talking about adding a free model checker to
Incisive (their NC-Sim upgrade) - my guess is that may change.
Prover Technologies sells tools to other tool vendors. Their model
checker is available for other vendors, but this year they are selling
their equivalence checker to end users. They say their tool is fast,
their GUI is very easy and they have a number of small customers.
Avery Design made an interesting comment on equivalence checkers.
Multipliers have always been a big problem for these tools, but of late
many can do 32 bit multipliers. Avery said they all cheat. They know
the three algorithms that Synopsys uses and if anyone uses a fourth
algorithm the tools would never work.
- John Weiland of Intrinsix
Verplex Formal Verification - LEC
Verplex Logic Equivalence Checker (LEC) for formal verification is
basically unchanged from the previous version I used. The biggest
difference (enhancement?) was a new Verplex debug environment
instead of Debussy. The Verplex schematic viewer supports annotation
of logic levels onto both the schematic and the RTL code. From the
brief demo, the Verplex environment appeared acceptable, relative
to the debug capabilities of Debussy. Tcl scripting capability is
also supported. Some enhancements have also been made for comparison
point mapping. Another new feature is the ability to perform LVR:
layout vs RTL, which may be useful for those individuals who don't
ever want to generate or view schematics.
- [ An Anon Engineer ]
Verplex is doing well. The new tool we heard is 'Prover Check'.
- Gangadhar of DigiPro Design
Cadence's "Heck"? What the heck is that? Haven't heard much besides
Verplex and Formality.
- [ An Anon Engineer ]
We use Formality with good results. Can't speak for the others.
- [ An Anon Engineer ]
We are using Formality. My company decided that they want to go single
set of tools. It seems to work fine.
- [ An Anon Engineer ]
We've done an evaluation of Verplex, Formality and FormalPro recently.
Of the three, Verplex has still the lead when the datapath modules are
big and flattened in the netlist. But Formality and FormalPro are very
close behind. The only issue with FormalPro was the fact that it
performed only flat verification even if there is a hierarchy in your
design. It cannot take advantage of the hierarchy to ease the process so
if you are stuck with a design that is too big, there is no way out
except to split it manually. Mentor is apparently planning to support
hierarchical verification soon.
We ended up buying Formality and are quite happy with it so far.
On a more general point of view, we are still quite annoyed by the very
slow support of Verilog 2001 by most EDA vendors and by the high level of
bugs in their Verilog reader once it supports part of Verilog 2001. It
seems that either nobody is interested in it or the vendors haven't
received enough complaints about it.
- Laurent Claudel
For LEC, we use Formality. We had Verplex before and people liked it
better than Formality (especially Debussy) but now we have only
Formality. They are still happy after all.
- [ An Anon Engineer ]
This is what I think is 'OK' and 'not OK' about Mentor FormalPro.
OK-I use FormalPro on both Solaris and Linux.
NOT OK- We use LSF for all our jobs -- it does not work here. If you
like to use the multi tasking you need to allocate all CPU´s you need
during the run. This means that LSF could not be used here.
OK- I do like the debugging possibilities FormalPro offers like the
what-if-analysis together with all good reports.
OK- I do not know if FormalPro is the fastest on the market today but
over the years I have only seen one tool that been faster and that is a
tool from Abstract Hardware which does not exist anymore. If a tool
manages to both compile and verify a design (rtl-gate 1.5M gate) within
a couple of hours I am more than satisfied.
OK- Earlier I was only using FormalPro in batch mode but that is not the
case today. I have slowly moved from setting up, starting the
compilation and verification, checking the result and doing the
debugging in a textual way to only using the graphical user interface.
This is because it is so easy to use and it is also very convenient to
have everything in front of you. Not long ago this was not possible,
but today the tool can handle the whole design so we do not need to
divide the verification into several parts. As with all EDA tools you
need to have good communication with the vendor so your problems will be
quickly solved. The support from several vendors after they have sold
their tool to you will not be the same.
- Jorgen Lundgren of Ericsson
I believe FormalPro is the best tool out there. We looked at tools from
Synopsys, Verplex, and Mentor. Based on what I had read, I expected to
see Verplex win. This did not happen. My opinion of the tools is that
Formality is the hardest to use. Some of our test circuits were never
able to verify and crashed the tool. Verplex was easy to use, but when
we started digging into the reports we found that it had thrown out much
of the circuit. I was amazed to see that we had only about half as many
compare points as registers. This gave me an uneasy feeling. They had
some reasoning for this but I didn't it. It makes me nervous so much
was thrown out. FormalPro on the other hand was easy to use, worked
quickly and gave excellent reports. They didn't throw anything away.
This was a big plus to me.
We have used the tool in many ways. We have used it to do equivalency
checking on our last two chips. All worked well except some Module
Compiler blocks that had merged multipliers and adders. (Large
multipliers are validated if we tell FormalPro the type of construction
used). Our last chip was ~12.5 Million gates--around 15 to 20% of this
was memories/analog. The rest was digital circuitry.
FormalPro verified all but ~1500 of 1,039,155 compare points. These
unverified endpoints were in the MC blocks I mentioned above. If we
black-boxed these, we were able to compare and verify everything. It
takes 30 minutes to compile the reference circuit and 30 minutes to
compile the final circuit. It takes another 30 minutes to do matching.
The final solve takes about 1.5 hours. Overall it takes 3 hours to
compare our chip.
We recently needed to do an ECO to one of the large blocks in this chip.
The code is written in VHDL and uses many libraries. FormalPro is able
to verify the gates (RTL-to-gates) in about 30 minutes. This block has
about 110,000 endpoints. It takes less time to verify than it does to
synthesize the circuitry!
I have been rewriting a processor core. I have been doing RTL-to-RTL
comparisons. FormalPro works extremely well for this. It has been able
to prove my new design is equivalent. One bug I have found is that the
GUI version of the tool sometimes takes two licenses.
We periodically looked at verification tools over the years. We always
found them hard to use and unable to solve things without telling them
exactly how to match up test points, which made the tools almost
useless. Once we evaluated the FormalPro tool, a large part of our group
found ways to use it. We fight over the licenses now -- I think this
says a lot. It is fully integrated into our flow. It does what it
promises to do.
- Maynard Hammond of Scientific-Atlanta
|
|
