( ESNUG 286 Item 4 ) ---------------------------------------------- [4/13/98]
Subject: (ESNUG 283 #1 285 #6 ) Formal Verification, Formality & Chrysalis
> I have used both Chrysalis and Formality to do RTL to gate comparisons
> on a 850k gate chip. Both tools had their successes and their
> failures but I think that Chrysalis has a more mature tool without
> going into technical details about algorithms. The Chrysalis tool
> was available on the market long before Formality and I did pretty
> much all work with Chrysalis.
>
> One of the most critical issue I have with Formality is that it is
> using Synopsys synthesis libraries. If there is a bug in the synthesis
> library the resulting gatelevel netlist will not be functionally
> equivalent to the RTL and you would not be able to find this with
> Formality since your reference was incorrect.
>
> Chrysalis uses the ASIC vendors library which is also the one used
> for ASIC sign-off. If the synthesis library is different from the sign-
> off library this will today only be found with Chrysalis.
>
> I did find a bug in our vendors synthesis library. One type of flip
> flop had an asynchroneous reset but it was modelled as a synchroneous
> reset flip flop in the synthesis library. This bug would have been
> pretty hard to find in the lab.
>
> - Anders Nordstrom
> Nortel Ottawa, Ontario
From: "Frank J. Rich" <fjrmrt@snet.net>
OK, John. What's your take on Formality's current capability? Is it the
usual 'trust us, we'll take care of the problems', or does the approach
Synopsys has taken -- same compiler for DC and Formality, use of .db file
to represent logic elements, switching DC versions to find differences, the
same mapper, parser, synthesizer, etc., etc.
Are the comments above meaning to say: We'll work w/ the tool, hacking away
until it does the job; because of the investment in Syn (dare to interpret
that as a double entendre). If so, we're in the same boat, and should plan
on added time and cost in solving the verifications we do.
Or, should designers looking to Formality to chase arduous regression
simulations at the gate level consider it a reasonable alternative? Is
any user going to understand the risk in using Formality also going to be
working on real silicon? Or the issues he (and Chrysalis) raises significant
enough to bother about? Some clear and conclusive answers would be helpful!
- Frank J. Rich
MRT
---- ---- ---- ---- ---- ---- ----
Hi John,
I am a Formality CAE and would like to respond to Anders' post. Please
don't use my name directly. [ A Synopsys Formality CAE ] would be fine.
Formality provides support for both Synopsys db libraries and verilog
simulation libraries. The support for verilog libraries was added after
our early pre-production releases and is currently available for use if you
have installed any release newer than 1997.10-3. The verilog library
support was used successfully by a number of customers during a beta test
that was recently conducted.
Since Formality can read db libraries and verilog simulation libraries,
it is possible to verify a db library against a verilog simulation library
directly within the tool. If a db library has been verified against a
golden verilog simulation library, it should make no difference to the
user which format of library to use in Formality when verifying a design.
- [ A Synopsys Formality CAE ]
|
|
