( ESNUG 285 Item 6 ) ----------------------------------------------- [4/3/98]
Subject: (ESNUG 282 #10 283 #1) Formal Verification, Formality & Chrysalis
> 1) Language synthesis, while not rocket science, isn't trivial. To
> develop one from scratch isn't much fun. Would you write a
> completely new one, if you had the industry-standard version already
> available to you? (This is the basis of the Chrysalis complaint.
> Formality may use the same (or similar) code to do language
> synthesis as did DC, thus, errors introduced in the DC synthesis
> step will be replicated in the Formality synthesis step, and thus
> won't be caught. I don't know whether Synopsys used the same code
> or not.)
From: "Duncan M. (Hank) Walker" <walker@cs.tamu.edu>
John, I think the essential point here is that "low effort" synthesis is
likely to be more bug-free than the heavy-duty optimizations applied later.
Werner von Braun's "too dumb to fail" argument.
> 3) Equivalence checking algorithms: Sadly (or happily, depending on your
> perspective), the time/memory/whatever required for equivalence
> checking is proportional to the SIMILARITY between the designs - not
> on their size or the function they implement. For example, it is not
> hard to compare multipliers, if you know that they are multipliers
> (not buried in logic), and expecially if you know the algorithm they
> use. Similarity comes up in spades, if you try to compare FSMs which
> use a different state encoding (or, equivalently, in pipelined logic,
> if the synthesis tool has done extensive retiming & re-optimization).
> Again, there is no problem if you happen to pick the same encoding as
> DC (but how do you do that, if you are a separate vendor, and don't
> have hooks into DC?), or know how DC did the encoding.
From: "Duncan M. (Hank) Walker" <walker@cs.tamu.edu>
This is only true if you use structural information in your equivalence
checker, such as finding potentially equivalent nodes by random simulation,
recursive learning, etc. A pure functional approach, such as BDDs, depends
only on functional similarity, not structural similarity. Of course all
the really good verification tools, such as IBM Verity, use some structural
similarity to reduce the problem complexity. The author is implying that
algorithms that don't need similarity, e.g. model checkers, can't handle
big designs. True, but they can be used on pieces of the design.
- Duncan M. (Hank) Walker
Texas A&M University
---- ---- ---- ---- ---- ---- ----
From: "Anders Nordstrom" <andersn@nortel.ca>
John,
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
|
|
