( ESNUG 406 Item 10 ) ------------------------------------------- [02/12/03]
Subject: ( ESNUG 405 #11 ) Tomoo Calls Formality An "Arthur Anderson" Tool
> Originally, Formality and Design Compiler *did* use the same front end:
> HDL Compiler. Thus if there was a bug in HDL Compiler then it was
> possible that during the initial parsing of the Verilog code, both Design
> Compiler and Formality would get the same *wrong* answer. And your
> verification tool would be useless. I don't know if this ever actually
> happened, but it was possible.
>
> - Steve Golson
> Trilobyte Systems Carlisle, MA
From: Bart Willems <european=bart cafe=easics.be ouiouioui>
Hi John,
We actually encountered this type of problem. In one of our designs bad
logic was generated due to a bug in Synopsys DC 2000.11-SP2. We found
this via gate-level simulations of the netlist. I thought this was an
interesting test case to check the dependencies (if any) between DC and
Formality.
First I used Formality 2001.08-FM1-SP3. Using this version, the synthesis
bug was not discovered, and verification between the RTL VHDL code and the
buggy Verilog netlist "succeeded"! Formality didn't find the bad logic.
This was not very encouraging. Next I tried Formality 2002.09-FM, which
at that time was the most recent version. Again the verification
"succeeded". Not good. But this time the following message appeared when
the VHDL RTL code was read:
Info: Formality has a new high-performance VHDL reader that can
be enabled by setting the 'hdlin_enable_rtlc_vhdl' variable prior
to reading in any design data.
So I tried again after setting 'hdlin_enable_rtlc_vhdl'. This time the
verification between the RTL code and the buggy netlist failed, so the bug
in DC was caught.
So it looks like, by default, the old front end is still used when VHDL
code is read into Formality. You have to set the
hdlin_enable_rtlc_vhdl = true
in order to use the new VHDL front end. I didn't find anything about this
in the Formality documentation, but maybe I overlooked it.
- Bart Willems
Easics NV Leuven, Belgium
---- ---- ---- ---- ---- ---- ----
> If Verplex wins in my customer benchmarks, that's great! I'll buy the
> tool! But I don't think that being "independent of Synopsys" is a
> legitimate reason to buy Verplex over Formality.
>
> To the Verplex marketing folks out there: Give up the FUD. That dog
> won't hunt any more. And don't belittle your competitor's products. Let
> us users do that for you!
>
> - Steve Golson
> Trilobyte Systems Carlisle, MA
From: Tomoo Taguchi <piranha=tomoo amazonriver=hp sought qualm>
Hi, John,
A few thoughts on Steve's comments. The whole argument against Formality
and DC being developed by the same company reminds me of issues raised about
another industry in the recent past: accounting.
I think one of the main themes of the Arthur Anderson scandals is that an
accounting firm was also providing other services to a company that created
a conflict of interest that compromised the integrity of their accounting.
But let me explain my thinking. For me simulation or formal equivalency
checking is essentially technical accounting. You're checking if synthesis
did it's job right. So for me, the integrity of the checking tool is of
paramount importance. The first pass of Formality didn't pass this test by
using HDL Compiler for both synthesis and formal checks. (In my opinion,
Synopsys deserves any perception problems eminating from originally using
HDL Compiler - they never should have shipped a tool with such a big flaw.)
Since then, Synopsys has done the technical equivalent of putting up (to
borrow another term from the accounting scandals) a Chinese Wall, by buying
an independently developed HDL engine.
Steve mentions using the -hdlc switch to use HDL Compiler get around any
problems with the Formality HDL reader. Although this is convenient to get
around problems, I find even the availability of this switch disturbing
because it essentially breaks down the Chinese Wall, should you use it.
(And I've been told to use -hdlc by Synopsys without getting an explaination
of its implications.)
Now the ease of use issue. Getting both synthesis and formal tools from the
same vendor will make your life easier. But do you really want a checking
(accounting) process to go too smoothly? As an engineer, wouldn't you
question a perfect first-pass result of anything? I think that any kind of
accouting or checking process needs to be adversarial to some extent to
preserve its integrity. Sure, being able to read in the .db file makes life
easier, but in my mind, formal checks replaces simulation, so I'd rather
jump through the hoops of using the simulation libraries instead. (But I
concede that using .dbs after doing formal checks against the simulation
library is OK.)
For me the integrity of an independent check is very important because I
don't know what Design Compiler is doing under the hood and I don't know
what a formal tool is doing under its hood. The only reason I trusted DC
was that I could run a simulation to see the gates I ended up with toggled
the bits in the way that I expected. Now with formal, I don't do much
gate-level simulation and I have to trust that when the tools says its OK,
it's really OK. Using the accouning analogy again, I don't know the exact
details of what's been happening to my money or even where it is, but I
need an accountant that will tell me that I have enough to do what I want.
And to trust the accountant, I need to make sure that he doesn't have any
incentive to lie to me or shade the truth.
Now having said all this, would I use Formality?
YES, I WOULD.
But, I wouldn't use any of the features like -hdlc which Synopsys touts as
selling points. If I used .db files, I would jump through the hoop of
checking it agains the simulation library first. In my mind they constitute
a "conflict of intrest". Basically, I don't think I would use any of the
features that makes Formality "nice to use".
I just used Verplex to check a 2 Mgate design. It wasn't as easy or smooth
as I had hoped. Verplex has its share of warts. My main complaint was that
it doesn't have a native TCL mode. It's TCL is more or less a band-aid
slap-on which limits its usefulness. You have to manually tell the tool
what architecture a multiplier is using (very annoying). It some times gave
false negatives (miscompares) on hierarchical blocks. And it can't deal
with non-synthesizable DesignWare models.
As a result of these frustrations, I did an evaluation of Formality. It was
easier to use. It dealt with multipliers and designware easier (no surprise
since both tools come from the same company). But eventually Formality lost
the evaluation because it was 3X slower than Verplex. For all the
frustrations that I experienced with Verplex, I did find work-arounds, I
just couldn't tolerate a 3X slow down.
Again, would I trust Formality? Yes I would, with the stated restrictions.
But at least with our design, it lost the benchmark.
- Tomoo Taguchi
Hewlett-Packard San Diego, CA
|
|
