( ESNUG 402 Item 8 ) --------------------------------------------- [10/23/02]
Subject: ( ESNUG 400 #15 ) Formality vs. Chrysalis & What About FormalPro?
> We started out using Chrysalis Design VERIFYer, which was subsequently
> acquired by Avanti and recently by Synopsys. I was able to use Synopsys'
> Formality to re-run some of this work. What follows is a summary of my
> experience with the two tools.
>
> - Steve Golson
> Trilobyte Systems Carlisle, MA
From: Mahesh Siddappa <msiddapp@atmel.com>
Hi John,
Thanks for publishing the comparison of Formality and Chrysalis in
ESNUG 400 #15. I wonder if any user of both Mentor's FormalPro and
Formality has published such a report? I would be interested in
looking at it.
- Mahesh Siddappa
Atmel
---- ---- ---- ---- ---- ---- ----
From: Maremanda Rao <mrao@amplecomm.com>
Hi John,
Here's my experience going from Design-Verifyer to Formality. Actually
there isn't much to write about in terms of training, ramp-up curve, etc.
because Formality itself was very easy to use, and rarely we had to rely
on the advanced commands like inv_push, etc. We just tried Formality
RTL-to-post-layout flat on our 300K instance design. It took 37 mins
on Linux machines. Design-Verifyer couldn't do this, even RTL-to-
pre-scan-gates (hier) due to capcity issues. Our traditional flow with
Chrysalis used to be bottom-up RTL-to-gates (same hierarchy that we
used for Synthesis), excising the instances as we go up. This was was
painful, because we had to add module/scripts and modify 'make' files,
etc. Overall, our runtimes have come down from a full day to 9 hours
plus no need to do that excising business anymore.
Thanks for the support from both the Synopsys & Chrysalis teams, especially
from the field specialist who was there for us on site resolving some
critical issues (turned out to be bugs) with painless work-arounds.
Also the shared key (for Formality and Design-Verifyer) helped us debug
the failures fairly easily, and report the bugs to the Formality team.
To make the story short, this was the easiest transition I haver ever had.
- Rao Maremanda
Ample Communication, Inc.
---- ---- ---- ---- ---- ---- ----
> The way Formality used to work and the way I think Design VERIFYer works
> today, if you need to give the tool some help once you matched again the
> tool would start the entire matching process from scratch. A waste of
> CPU cycles
>
> - Steve Golson
> Trilobyte Systems Carlisle, MA
From: Howard Landman <howard@riverrock.org>
Not exactly. You do need to rerun Design VERIFYer, but you can read in an
output file from the previous run to re-establish all the matchings and
equivalences already proved. This doesn't take very long compared to
the overall runtime.
> 15. Formality allows you to quickly and easily check just one output, and
> ignore all the rest. Design VERIFYer can do this, but it's painful.
Steve, go into the debugger ("chrys_explore -gui"), select the matched
output, and verify it there. Not too painful unless it takes a long
time. (Yeah I know, you'd rather script it ... which does require
setting an ignore on every ouput EXCEPT the one you want ...)
As you discovered, DV is starting to show capacity and speed limits for
big designs in RTL mode. From your number it looks like Formality may
be better in those domains. From my experience (I haven't used
Formality much), Verplex's LEC is also much better at handling large
designs than DV. I'm a long time DV user and have taped out multiple
chips using it, and I like many aspects of the tool, but if I was doing
something large today I would be more likely to go with Verplex because
of capacity and speed concerns. LEC also does a somewhat better job of
pruning the logic cone feeding into a difference when it reports the
difference back to you, which can make debugging a little easier.
I'd like to also mention that library model verification should be taken
very seriously. Many people think that library cells are so simple that
nothing can go wrong, or that if something was wrong, it would be so
obvious that it would be caught by simulation. Think again. I've seen
at least two tapeouts (at different companies) fail because of library
bugs that would have been caught by any reasonable verification process.
Setting it all up may be slightly painful, but the runtimes (except for
Spice on 32-bit registers :-) are trivial. On one project I worked on,
we had up to 5 Verilog models of each cell. Formally verifying all 5
libraries against each other took less than one CPU-minute, once it was
set up, and we ran it routinely on every library release, and we
occasionally found problems and fixed them. Using formal verification
tools designed for million gate chips to verify a standard cell library
may seem like using a sledgehammer to kill a mosquito, but it does the
job, and it's better than simulation (although you want to do that too,
if only to verify that the models work with each simulator).
- Howard A. Landman
Riverrock Consulting Fort Collins, CO
============================================================================
Trying to figure out a Synopsys bug? Want to hear how 14,488 other users
dealt with it? Then join the E-Mail Synopsys Users Group (ESNUG)!
!!! "It's not a BUG, jcooley@TheWorld.com
/o o\ / it's a FEATURE!" (508) 429-4357
( > )
\ - / - John Cooley, EDA & ASIC Design Consultant in Synopsys,
_] [_ Verilog, VHDL and numerous Design Methodologies.
Holliston Poor Farm, P.O. Box 6222, Holliston, MA 01746-6222
Legal Disclaimer: "As always, anything said here is only opinion."
The complete, searchable ESNUG Archive Site is at http://www.DeepChip.com
|
|
