( ESNUG 283 Item 1 ) ------------------------------------------------ [3/5/98]
Subject: ( ESNUG 282 #10 ) Formality's Independence From Design Compiler
> I need your insights on Formality, Synopsys's new equivalence checker.
> Questions have been raised by Synopsys competitor Chrysalis about the
> independence or lack thereof of Formality from Synopsys's Design Compiler
> synthesis tool. How much of an issue is Formality's reliance on DC? Is
> Formality going to allow the same faults to slip through that DC allows?
>
> - Chad Fasca
> Associate Editor
> Electronic News
From: [ Someone Who Knows A Little Something About FV Tools ]
John,
Please keep my name in confidence - in a former life, I worked on [ All
Sorts Of Great Yet Identifying Creditials Deleted ].
With respect to Formality's dependence or independence from DC: if you want
to compare RTL to gate-level designs, you must synthesize the RTL to gates,
then check those gates to the user's gates. (Got that? -- you start with
RTL and gate1 -- you synthesize RTL *to* gate2, *then* compare your gate2 to
the user's gate1. There may be other ways to do the comparison in theory,
but they all break down pretty quickly.)
Given the above scheme, you have a couple of problems:
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.)
2) If you do choose the "let's write one" language synthesis route, you
have a bunch of new problems. Amongst them:
- language interpretation: some corners of the language are
ambiguous (or, at least DC takes an "interesting" interpretation).
Do you match DC, or the simulator? Folks will complain, either
way. (Let me know, if you want specific examples.)
- worse, interpretation can depend on compiler directives (pragmas),
which can (and do) affect the systhesized result. ("synopsys
full_case" and "parallel_case" are the most obvious examples).
Now, not only do you have to match [relatively standard]
languages/language subsets, but also completely non-standard
(and potentially copyrighted) compiler directives -- not all of
which are well documented.
- More interpretation: FSMs - what do you do when/if DC re-encodes
the FSMs? (...and, for an implicit FSM, where there is no explicit
encoding.) How do you find the state variable flops, if the
synthesis tool doesn't tell you where it put them, in the gate1
netlist?
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.
Hmm... this is getting long. Lets change gears for a minute:
Last issue is really a marketing one: why do customers purchase Formal
Verification tools? If it is just to check whether Synopsys did the right
thing, how many do you think you can sell? If you find Synopsys bugs,
great -- then Synopsys fixes the bug (maybe)....eventually, you turn into
a Synopsys QA tool -- and only Synopsys really needs to buy one. (i.e.,
your value tends to decrease over time).
Next issue: given that your sales as Chrysalis may be limited, how many
resources do you really want to pour into development? As described above,
keeping up to DC may or may not be so straightforward. Synopsys has a much
larger market, and thus can afford to but a lot more people into developing
DC than you can afford to put into yours to keep up. And if you don't keep
up, your tool is going to give more "can't solve" messages - thus becoming
less valuable, over time. So you need to customers to have another set of
reasons (aside from Synopsys QA) to buy. And those reasons would be... ?
Do I think that there are viable FV product opportunities? Yes. But I'm
not sure how many equivalence checking products can actually make money.
And I have real doubts about the viability of (real) RTL->gate Equivalence
Checking and even more doubts about RTL->RTL comparison (both of which
are probably more valuable than gate->gate. Unfortunately, less feasible
technically). On that front, I'd be curious to hear, if you find a customer
who used anybody's RTL->gate or an RTL->RTL EC tool, and was happy with it.
(I'm not really interested if the user had to hack the code to get EC to eat
it, or if there were severe limits on block size, design methodology, etc.)
Again, you didn't hear any of this from me.
- [ Someone Who Knows A Little Something About FV Tools ]
---- ---- ---- ---- ---- ---- ----
From: rajen@jaxom.eng.pko.dec.com ( Rajen Ramchandani )
Hi John,
As someone who has used Formality on a 2 million gate ASIC to check the RTL
to gates, I feel that I should comment.
Our design flow used DC 97.08 for compiling the designs and one of the
significant changes in this release was a new hdl reader and like all new
code this had significant bugs. There were cases in which this reader would
incorrectly read our verilog code and produce bad gates. These were being
detected by gate-level simulation.
In one instance a whole else branch of if statement was ignored. We couldn't
migrate back to 1997.01 since there were instances in which this release was
producing incorrect logic for us & these bugs had been fixed in the 1997.08
release. Also we were getting much better quality of results with 1997.08
while using the large design compile strategy as detailed in the white paper.
We asked Synopsys for a pre-release version of Formality to check the RTL to
gates, since the simulations would not be able to check all cases of errors.
After a lot of arm-twisting on our part (which I couldn't understand, since
we were going through hell out here trying to synthesize this design), we
were given a temporary liscence to use Formality and used this tool to
check the RTL to gates for equivalence. We used this to check the RTL to
gates for most blocks on the design. A couple of blocks had to be sent off
to the Formality R&D folks for further investigation of miscomparisons.
Formality did detect errors in Design Compiler when comparing the RTL to the
gates and in most cases the solution to the problem was to say:
hdlin_turbo_sequential = false
(i.e just use the old hdl reader, one more hidden swich to be added to the
list out there :-).
I feel that Synopsys has taken the trouble to address the issue of
independence of Formality and Design Compiler. I must add that in the past
I have detected the problems with the BK adders for certain bit-widths
( see ESNUG 261 #1 ) using compare_design which is within Design Compiler
itself. I think the issue is not whether both tools come from the same
company but whether they were developed by the same team. If different
teams implement the tools independently then the likelyhood of making the
same assumptions and the same mistakes are minimized.
I hope Synopsys makes this independence formal and glass walls the two
divisions to prevent common mode mistakes from entering the system. I don't
know the extent of shared code in the two tools but my experience has shown
that Formality can be used to check the results of Design Compiler. We have
taped out the design and are waiting for prototypes back from IBM. Lets see
what the lab results have to show when we get the prototypes back and power
up the system.
- Rajen Ramchandani
Digital Equipment Corporation
---- ---- ---- ---- ---- ---- ----
From: Dyson.Wilkes@swi055.ericsson.se (Dyson Wilkes)
John
Chad Fasca asked about the indepenedence of Formality from DC. A good
question that was raised at seminar I attended. The answer was that
Formality contains a number of equivalence engines of which, I think, only
one is the same as that used in DC.
The issue I have is with the RTL front-end. The interpretation of RTL into
the logical equivalent is one most frought with danger. (Maybe it is not so
bad now assuming a higher level of education in how to code good RTL.) Even
so I would would like to have any RTL checked by two independent front-ends
if I was to rely on formal tools to do away with gate level simulation.
I got the feeling that Synopsys was playing down the use of Formality in the
early stages and advocating that users start with gate-gate comparisons and
only then work back to RTL-gate comparisons as they gained experience in the
these new tools.
The big downside so far with any tool of this kind (equivalence checkers) is
that they get more tricky to use as the topology (or logic) of the compared
codes become more different. I advise Chad to take a close look at the
debugging capabilities in the tools under consideration: watch out for that
old "Not proven" problem!
I am also interesed in some figures for the scaling of performance of these
tools with circuit size. Unless the algorithms are cleaver the runtime goes
through the roof as the size increases. A good tool would be nearer linear
if at all possible.
What would be most useful is a tool that can tell me that circuit A is the
same as circuit B except that it has XYZ additional functionality! That
would be such a useful tool in this age of design re-use. Oh, yes, and it
has to cope with all sorts of nasty asych. features in the circuits, too!
- Dyson Wilkes
Ericsson
|
|
