( ESNUG 413 Item 2 ) -------------------------------------------- [05/29/03]
Subject: ( ESNUG 406 #10 ) Verplex, Formality, & Those Encrypted DW Parts
> I just used Verplex to check a 2 M gate design. It wasn't as easy or
> smooth as I had hoped. ... 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
> ... but eventually Formality lost the evaluation because it was 3X
> slower than Verplex.
>
> - Tomoo Taguchi
> Hewlett-Packard San Diego, CA
From: [ The Artful Dodger ]
Please keep me anon.
I enjoyed Tomoo's ESNUG 406 #10 letter on Formality vs. Verplex and agree
with his approach to this methodology (e.g. wanting the equivalence check
to be confrontational rather than painless). However, I wanted to comment
on his two snippets above.
I regularly use both Formality and Verplex Conformal LEC, and only trust the
result if both tools show equivalence. I'm glad I have the luxury of this
dual redundancy as it's picked up bugs and methodology issues in both tools,
which I've reported back to Verplex and Synopsys.
Up until 6 months ago, my experience was also that Formality was slower
than Verplex. However, I've noticed big speed ups with Formality since the
2002.09 release, so that now it's as fast as Verplex on our designs
(typically 500 k gates). Formality's debug is also improving and catching
up with Verplex Conformal LEC.
Tomoo also says that Verplex can't deal with non-synthesizable DesignWare
models but Formality can. This is not quite the whole picture -- I'd argue
that neither tool can! In a DesignWare release you get two models under:
dw/src_ver/DW*.v: Verilog simulation model
dw/lib/DW*.syn: Encrypted synthesis model
Both Synopsys DC and Formality use the encrypted synthesisable models. The
good news is that Formality is really checking that DC correctly synthesises
these encrypted models to gates, so it cannot be accussed of being "the fox
that guards the chickens" for this part of the flow. However, the bad news
is that Formality does not equivalence check against the simulation model,
so it's possible that there's a simulation vs synthesis difference in this
flow (i.e. the RTL simulation could be functionally different to the netlist
simulation -- something that equivalence checking is supposed to replace).
Why doesn't Formality compile the simulation model instead? Just like
Verplex, it cannot compile the simulation models! Take a look at the
RTL, it may be efficient for simulation but a synthesis engine will not like
them. Any library qualification that Synopsys does for the simulation and
synthesis views cannot involve equivalence checking with Formality.
Verplex, like Formality, cannot compile the simulation view. It also cannot
compile the synthesis models -- but only because they are encrypted by
Synopsys. What can you do instead:
a) Create your own synthesis models (this is independent but
could be wrong)
b) Black box DW comps in both RTL & netlist (so they are not
checked)
c) If netlist is flattened, have dummy DW comps with all outputs
set as don't-cares (a form of black boxing)
Formality's DW check is certainly better than (b) or (c) above, but the DW
flow that Synopsys tools use still has a possible single-point-failure: a
bug in an encrypted synthesis model that could be missed.
Both Formality and Conformal LEC are good tools and will find bugs in your
design, and my experience is that they are now both fast enough. Formality
has on the whole been developed independently from DC and is becoming more
independent (in June the Interra VHDL Compiler will become the default, with
the DC reader becoming the alternative). However, there are methodology
issues with both tools and Synopsys and Verplex should be open about how
they check the design flow (what is and is not checked). Particular areas
of concern are how X's are modelled and controlled (particularly RTL vs RTL)
and how undriven signals are mapped (floating or don't-care). It may not be
bugs in the tool, but tool usage problems (sometimes with the default
behavior!) that misses design bugs. As engineers, it's our job to ask
difficult questions so that we have confidence in what they are checking
and how much we can rely on them.
Finally, a tip. Equivalence checkers make very good linting tools, warning
about code styles that can throw up important simulation vs synthesis
differences (e.g. use of casex, signal missing in sensitivity list, multiple
drivers) and also report undriven signals and redundant DFFs (termed
"Unreachable" by Verplex and "Unread" by Formality). I've created scripts
that take a Verilog command file then just compile the RTL and report any
issues. For Verplex, I simply run the following checks in my script:
report rule check -Summary >> $LOG
report floating signals >> $LOG
report rule check -Verbose >> $LOG
This typically takes a minute or two to run and has found lots of RTL
problems (sometimes missed by our main linting tool).
- [ The Artful Dodger ]
|
|
