( SNUG 01 Item 15 ) -------------------------------------------- [ 3/28/01 ]
Subject: Verplex Tuxedo & BlackTie, Avanti Chrysalis, Synopsys Formality
EXIT WOUNDS: Out of the 27 e-mails I received on Formality, Verplex or
Chrysalis: 22 were pro-Verplex; 5 were pro-Formality; and none were
pro-Chrysalis. Years ago, Chrysalis owned the Equivalence Checking market.
Then Synopsys, with it's walking talking million man sales army, took this
market away from what was then the new Avanti acquired Chrysalis. Then,
stupidly, Synopsys never built a community of users around Formality.
Formality wasn't under any real pressure to improve, so when Verplex came
along with its better tool, the customers very quickly abandoned Formality.
This 22 to 5 ratio of customer e-mails clearly shows how far ahead Verplex
is over Formality is in this niche.
"We tried Formality vs. Chrysalis vs. Verplex, in fall 1999. Only
Verplex did the job, so we stay with them.
- Paul Schnizlein of Agere Systems
"Formality... let's just say there's a severe pain threshold there.
Unless you're a Unix-god and eat kernal code for breakfast, the
terse-ness of Formality's scripting/setup is out of hand. And,
beyond that, they had trouble in the 2 key areas regarding my
criteria for the evaluation. Those 2 items were image size (how much
memory is used) and performance (how long Formality takes to do the job
in real-time). I had to run a couple of scripts to bump up the
allowable image size from the default 2G to 4G (actually 3.8) on a
Sun-Solaris UNIX box, so I could get Formality to read in the full
RTL-vs-gates. Once I got the tool to read in the design, I found it
to be dog-slow, and produced numerous false discrepencies.
I can not comment on Mentor, as I did not eval their tool.
Now to Verplex. Wow! Day one I was able to read in and do RTL-vs-RTL,
gate-vs-gate, & RTL-vs-gate, all under the 2G image limit. I think I
got up to 1.3G. Performance is another positive for Verplex. What
took Formality 6 hours, Verplex did in 2 hours, it was that obvious.
Verplex scripting is straight forward, and has a familiar feel to
synthesis scripting, so you don't have to bend over backwards to learn
it. Their GUI is solid, easy to navigate, and their use of Debussy
for schematic management is a great choice.
I would seriously urge anyone, even those happy with the formal tools
they have now, to at least evaluate Verplex and see what I'm talking
about. We are using it as I write this, to finalize designs upwards
of 2-3 million gates (and still under the 2G image-ceiling). That's
2-3 million gates vs. RTL fully verified. I'd like to know if anyone
else can do that out of the box."
- Mike Bly of World Wide Packets
"Our chip has roughly 5 million gates and 120,000 flops with lots of
memory. It also contains hundreds of multipliers which range from 9x9
up to 15x15 in size. We use Synopsys DC Ultra with DesignWare for
synthesis. All arithmetic elements are created with DesignWare. This
design takes weeks to run even the most trivial gate-level simulations
with VCS. Verplex Tuxedo LEC helped us eliminate costly simulation
time. LEC handles design hierarchy by performing a bottom up
verification to quickly isolate problem areas in RTL-to-gate
comparisons. Modules are simply black boxed as you move up the
hierarchy. Multipliers were quickly verified against the synthesized
DesignWare multipliers. The tool has a graphical mode that allows
for easy identification of miscompares. Cut points can be inserted
into the design to break up large fanin points."
- Andy Adams of RealTime Visualization
"We've never tried Formality, but switched from Chrysalis to Verplex two
years ago. We have found Verplex to be much easier to learn and use.
We also believe that the LEC runtimes are much better. The engineers
really like the link to the Debussy tools, which we also use. Our
Verplex LEC model of use has primarily been gate-to-gate, but we
recently completed a VHDL/Verilog chip using LEC RTL-to-gate."
- Joe Gilray of Agilent
"We started to use Verplex's Tuxedo from the end of 1999. It has
successfully performed full chip equivalency checking on our
Verilog-RTL vs. Scan-inserted-Gate vs. ClockTree-IPO-Gate ~2M gate
netlists. Our runtime: 2 hrs (RTL-gate), 1 hr (gate-gate) on a
SUN U60."
- Jim Lee of Ishoni Networks
"Again referencing my presentation, Formality saved us a lot of headache
during our hand editing phase. The ability to do a gate-to-gate
compare on a 870 Kgate chip in ~ 4 hours was invaluable to increasing
our turn time."
- Tom Tessier of t2design
"Verplex complains about things that Chrysalis blithely ignores. We
almost got bitten really really bad in the week before tape-out (!)
because of that; I'd run some blocks in Chrysalis and some (the tougher
ones) in Verplex. I ran one block in Verplex sort of on a whim for
the first time and discovered that there were pins that were entirely
disconnected in synthesis that should have been connected. Eek!
Fortunately they turned out to not be used outside the block, but
what a scare. I was so impressed that I went back and ran all the
blocks in Verplex. Nothing like more accurate results to motivate
a person to really learn a new tool, I guess.
The problem with Verplex,and why I dragged my feet on really learning
it, is that IMHO it's harder to debug non-equivalent points than it is
with Chrysalis, which is odd considering how much Verplex touts their
usability. I've heard people complain about the arcane nature of
Verplex mapping rules, but I don't think they're really any worse than
Chrysalis's.
What I really wish Verplex had was the ability to trace a signal back
through the source code, or at the very least a list of signals that
are duplicates of the signal under examination. Chrysalis has both,
which I really like (although of course they have their own goofiness
as well -- I'd like to be able to look at signal correlates while
tracing back, for instance)."
- Natalie Overstreet Ramsey of Vitesse Semiconductor
"Chrysalis used to be the top dog, but doesn't seem to have progressed
much since Avant! bought it. I also think they lost their best support
engineers."
- an anon engineer
"We evaluated Formality, Chrysalis, and Verplex. We chose Formality.
So far we are using it mostly for gate to gate comparisons and it has
found some ECO errors for us. So far we like the tool."
- an anon engineer
"Gates-to-Gates: Verplex is good. RTL-to-Gates with DW components:
Only Formality works. (Verplex couldn't do it.) Chrysalis used to
be good, but now Verplex is much faster and easier to use."
- Himanshu Bhatnagar of Conexant
"We've got Verplex, and it seems easy enough to use. It has certainly
saved our bacon a couple times, and makes us a lot more calm in the
final weeks before tapeout."
- Paul Gerlach of Tektronix
"I've just used Formality because that is what LSI has certified. It
has always done an adequate job, but then again I don't know what I
might be missing with the others since I've never shopped around."
- an anon LSI engineer
"Not sure about other tools but used Chrysalis and Verplex's LEC. I
started Formal Verification with Chrysalis and I used to think 'wow'.
However, that was till I got a copy of LEC. LEC is more easier to use,
with a bunch of simple commands. It doesn't need huge amounts of
memory to do the job. It doesn't keep you waiting for hours to get
the result. Also, debugging is much easier with LEC. Don't know how
much it costs now, but it was less expensive.
I think Verplex is far ahead in the race."
- Prasad Lakamsani of Chartered Semiconductor
"I've never taken to Formality. Who in their right mind would use one
Synopsys tool to check another? Again a straw poll conducted under the
influence revealed quite a larege support for my opinion (or maybe I'm
just remembering things selectively). Verplex's Tuxedo seemed to be
the most popular alternate choice."
- Chris Byham of Philips Semiconductors
"BlackTie (Verplex - http://www.verplex.com)
* Formal Static Verification - no simulation necessary.
* Very large capacity - "Full Chip capacity"
* Assertion monitors used in code or in assertion file.
* Open source assertion monitor library supported (OVL)
(http://www.verificationlib.org)
* User can contribute new assertion to library.
* Leverages same assertions used in simulation (OVL).
* Extracts assertions (properties) and employs formal techniques
to prove properties - diagnosis engine presents counter
example.
* Use assertions as target or constraints for formal
* Advanced linting (bus contention, dead code, set/reset
mutual exclusivity, tri-state, range overflow,...etc.)
* Uses Debussy debug environment to debug failures.
* User can define additional constraints to limit state space.
The big benefit of BlackTie is the ability to use the same assertions
in Formal Verification as with simulation. Plus the tool appeared
very easy to use - same pragmas as simulation and Debussy debug
environment.
Now if Verplex and 0-In would get together and settle on a common
pragma that would be an awesome solution. Write a set of assertions
to use with simulation, semi-formal and formal."
- Jerry Vauk of Sun Microsystems
"We chose the Verplex Tuxedo LEC for following reasons
1. The support for VHDL was better.
2. Provides GUI as well as script based interface to fire the run
and debug problems.
3. Almost all VHDL RTL constructs used by coders are supported.
4. Whatever was not supported in the tool came up afterwards as
part of Verplex support.
5. Excellent support by the Verplex support team for the issues
that came up when we were in our learning stage.
6. Good documentation, though needs many more details.
7. Tool is easier to understand with the kind of documentation
provided.
- Prasanna Shah of Acorn Networks
"We will not look at Formality period, since it's from Synopsys. Why
should I pay for a tool from the same company to check the logic
created by their other tool? Synopsys would say the R&D teams are
totally different for Formality and Design Compiler. I would believe
it only if the Formality team is composed only of Russians, Egyptians,
and Iranians, working in a "safe" site in Turkey, and speaking not
one word of English.
Never seen FormalPro yet. Chrysalis works but is clunky and showing
its age. Verplex is the winner for ease of use, speed, and capacity.
- an anon engineer
|
|
