( DAC 01 Item 16 ) --------------------------------------------- [ 7/31/01 ]
Subject: Verplex, Formality, Chrysalis, Cadence 'Formal Check'
EMBARRASSING THE BIG BOYS: I feel sort of sorry for the R&D guys at Avanti.
The whole world is raining shit on their company and now customers are
even publically complaining about how old & out-of-date Chrysalis is. Yea,
Synopsys Formality has also had it fair share of abuse from users, too, but
at least the customers seem more willing to give Formality a second look if
the Synopsys guys improve it. I get this sense that users don't forsee
Chrysalis getting 'better' any time soon no matter what Avanti says.
Anyway, as usual, Verplex is mostly doing quite well in the eyes of most EC
users these days, as you'll see from the user comments below. But, if I was
Verplex, I wouldn't sleep too soundly. The Formality people are pissed and
they're busting their butts to correct their product's problems -- and even
Mentor is trying to horn in on the action with its FormalPro product!
"Chrysalis is loosing it, the tool has been around for many years and
I don't think they have kept up with the competition. New front
runner I think is Verplex."
- Anders Nordstrom of Nortel
"First: the days of Chrysalis DesignVerifyer seem to be over.
Second: choosing Verplex or FormalPro is more a less personal taste.
It looked like Verplex focused on improving speed vs. Mentor
improving memeory usage."
- [ An Anon Engineer ]
"We're uncertain about what effect the Avanti trial results will have
on Chrysalis a.k.a. Avanti Formal."
- Howard Landman, Vitesse Semiconductor
"We purchased Formality after evaluating Verplex's Tuxedo and Synopsys
Formality. Throughout the evaluation, Formality completed all of the
test cases using a simple standard setup and the Synopsys sales
support team was always quick to respond and constantly offered their
assistance. Verplex showed no such alacrity and was not able to
complete any of our test cases.
Synopsys's level of support during the evaluation led us to conclude
that they would remain committed to our success even after our
purchase. I'm glad to say, they have!
During our most recent verification Formality wasn't able to match our
RTL code with our Ambit gate-level netlist. The RTL looked good and
we passed it to Synopsys as a bug. After several tests, they were not
able to find any error generated by Formality and netlists which were
synthesized from DC passed verification. We began to look at Ambit
and found a bug in the way it treated a 2-stage adder!
- Dharina Desai, Fast-Chip, Inc. (from ESNUG 375 #4)
"We did a comparison between Verplex, Formality and Chrysalis. Verplex
is extremely easy to use and is blazingly fast. However, in one design
it failed to flag an obvious difference, whereas Chrysalis did point it
out. We also had problems with Verplex handling DW components. The
Verplex AE assured me that they can do it, however when I sent him the
code, he mysteriously disappeared. Chrysalis is a lot harder to use
and its debugging capabilities are horrendous. If everything verifies
then it's beautiful, however if there are differences, you better call
the Chrysalis AE. The Chrysalis equivalence checking engine is really
robust but it lacks good debugging capabilities, whereas Verplex's
engine is not sophisticated enough, however it has good debugging
capabilities.
Formality is just too painful to use. It suffers from long run-times
and is just not friendly enough."
- Himanshu Bhatnagar of Conexant
"Chrysalis - v3.0.1 is good enough for us."
- [ An Anon Engineer ]
"For equivalency checkers I generally use Chrysalis, as a last phase in
the verfication flow. It's pretty easy to use, but you'll want a
really large memory machine for big SOC design runs and make sure to
rebuild the OS with a *JUMBO* size memory kernal..."
- Tom Moxon of Moxon Design
"We own, but don't use Formality. No real need."
- Phil Kuglin, Credence Systems Corp.
"We're quite happy with Formality, but we are still looking at Verplex."
- [ An Anon Engineer ]
"We evaluated Verplex vs Synopsys Formality. Both tools are good with
same results. No decision was done yet."
- [ An Anon Engineer ]
"Verplex is amazingly fast, but never underestimate SNPS. Formality can
now handle designs that have been retimed (ie combi logic moved across
registers). Unfortunately, if EC tools don't know *which* logic was
moved, all combi logic has to be considered together - a significant
runtime hit.
Formality also seems to do far better on datapath."
- [ An Anon Engineer ]
"Synopsys Formality seems okay. It still needs more VHDL-93 support
and improved checking algorithms but they're working on it."
- Menno Spijker, Mitel Semiconductor
"Cadence Formal Check originally came from Bell Labs. As such, they
invented their own language, which looks like a prepositional logic.
If that scares you, don't waste your time with them. The local AE
could not answer what we thought were simple questions, so we got a
demo from the main support center in CO. Nice features are:
1. You write an assertion, which is proven for one block of logic.
You can then use that same assertion as an assumption for the
input of the next block.
2. They do the proofs hierarchically. If an assertion is provable
at the leaf level, it is not retested at any higher level. I'd
like to try them on my current test problem. So far other
vendors have gone "uh....".
I've talked to some folks who have started using Verplex's proof
engine, and seem pretty happy, but I have yet to get there."
- Jeff Deutch, Avici Systems
"We use Verplex (after struggling with Chrysalis). It's relatively
easy to set up and it meets our needs."
- Roger Bethard, Cray Computers
"Verplex is ahead right now in terms of both product and support, but if
the product is easy enough to use, support becomes less important. :-)
Avanti put out a press release in their formal verification newsletter
about a new version of Design VERIFYer, and I'd like to try that. I'm
concerned about the tighter integration to Apollo, though; that's great
for folks using Apollo, but it's not at all compelling to those of us
who aren't."
- Natalie Overstreet Ramsey, Vitesse Semiconductor
"Verplex Blacktie: Functional checker tool. Only saw the first part of
the pitch. Did not see the demo.
- Tool parses your Verilog or VHDL and auto hooks up checkers.
Available now.
- Allows user-defined assertion checkers (Beta) to be added
to the RTL.
- Static checker.
- Uses OVL (open verification library) of checkers. Has about
20 in the library.
Goal of tool is to get to a golden RTL faster so that you can
use it with Verplexes equivilency formal verification tool.
- Peet James, Qualis Design
"Verplex?
A very good tool which seems to be improving. Hopefully they don't
get gobbled up.
Synopsys Formality?
Not bad if the only thing you want to EC is something synthesized by
Design Compiler!
Avanti Chrysalis?
R.I.P. I think their debugging environment couldn't be any more
difficult. Looking stagnant.
Mentor FormalPro?
Still teething. This tool needs some work."
- [ An Anon Engineer ]
"In our eval last year Mentor had problems comparing RTL to gates."
- [ An Anon Engineer ]
"Verplex's BlackTie formal functional checker looks very attractive.
By promoting the Open Verification Library (OVL) assertion checkers
as a free public standard, Verplex is enabling immediate user benefit
in existing Verilog simulation environments. That doesn't require the
purchase of any Verplex tools. But Verplex is also building OVL
assertion checker support (currently in "late beta") into their
BlackTie formal checker. That's potentially a really major win for
designers, if BlackTie works as claimed. HP is a beta site for this
work. Harry Foster (from HP) gave a suite presentation on some of
the results to date, with impressive claims re capacity and overall
results. This is definitely a tool to watch and was (for me) the
surprise of this year's DAC. I also like the fact that BlackTie comes
from a company (Verplex) with real credibility in the related formal
equivalence-checking field."
- Mike Carter of Mosaid Technologies
"Tuxedo seems very easy to use & does full-chip better than Formality."
- Michael Hede, MindSpeed
"We looked at Verplex Tuxedo recently. We can't use for RTL-to-gates
checking on our designs because we use pipeline retiming extensively
and Tuxedo can't check designs in which the registers have moved."
- John Lynch of Pixelworks
"Verplex BlackTie
----------------
Verplex has released their BlackTie model checker, but it only performs
their built-in checks right now. The ability to operate with
user-defined checks through the OVL (Open Verification Library,
www.verificationlib.org) assertion checkers is in beta right now, and
it sounds like they will release it later this year.
As an example of the value of a model checker, consider a 32-bit
comparator. An exhaustive verification via simulation requires 2^64
vectors, and at a rate of 1 M vectors/sec, it requires 500k + years to
simulate. BlackTie can exhaustively verify the logic in 2 sec.
Verplex presented a Ricoh case study in which Ricoh replaced a 150 hr
testbench for an asynchronous design with a 20 minute BlackTie run."
- [ An Anon Engineer ]
"For equivalence checking we continue to be happy with Verplex LEC,
which gets heavily used both for RTL to gates and for VHDL to Verilog
checking. The tool has high capacity - at least high enough for our
designs. Other tools evaluated (in late 1999) - Chrysalis, Synopsys
Formality, Mentor - did not compare, but may have improved this year."
- [ An Anon Engineer ]
"BlackTie(tm) by Verplex
-----------------------
1. Properties are described by assertion statements using a
Verilog-like language. They can be either embedded as Verilog
comments in the design file or kept in a separate file.
2. Supported by a set of powerful diagnostic tools.
3. It is not hierarchical. Results from lower level blocks are not
leveraged off at a higher level.
4. Available on Linux/Intel.
5. The purchase price is in the order of $75K. Leasing program is
available."
- Henry So of Mobilygen, Inc.
"There's no silver bullet here, but in general, Verplex has the faster
and more stable tool. But talking ROI, the picture gets fuzzier."
- [ An Anon Engineer ]
"Verplex Tuxedo is easy-to-use and has great debugging links with
Debussy. This is becoming a "solved problem". The only issue is
with dealing with some new synthesis tools like Synplify ASIC who
say that they've had problems with equivalence checking. Is that
their fault or the checker's fault???"
- Andrew MacCormack, Tality/Cadence
"Verplex is easy to use and works well. Not quite the same can be said
for Chrysalis even though everyone has used it and liked it for what
it does for quite a while."
- John Szetela of AMD
"We use Verplex for equivalence checking. Great tool and great company
to work with. Course in the EDA industry that means they will get
bought within the year and whoever buys them will ruin them but for
the moment they are great."
- Phil Hoppes, Intersil
"We are just about to get rid of our Formality licenses and go with
Verplex. Not that it's a surprise, but Synopsys is totally lying when
they say Formality doesn't use any of the same algorithms that DC does.
Formality missed something in one of our chips that Verplex easily
caught. If formal verification had been done that the module level,
Formality would have caught (we later determined) the problem in this
piece of DesignWare.
On top of this, after a demo at DAC, I was also amazed at how much
easier Verplex is to use than Formality. They OEM Debussy which is
100x better than the schematic tracer that Synopsys has."
- Duncan Halstead, LSI Logic
|
|
