( ESNUG 465 Item 3 ) -------------------------------------------- [06/28/07]
Subject: ( ESNUG 464 #4 ) Questioning the 40 missing DFFs Verplex "found"
> We ran Verplex (Cadence Conformal) against a netlist that was generated
> from Synopsys DC and optimized by PhysOpt, and found a non-matching number
> of end points between our Golden RTL and our revised netlist.
>
> We couldn't find why around 40 DFFs disappeared from our netlist?! They
> were right there in our RTL. Using Verplex we proved that those 40 DFFs
> shouldn't have been optimized out. Looking at the constants we traced
> the issue to wrong/bad optimization by PhysOpt/DC.
>
> By setting a switch in PhysOpt/DC that avoids constant propagation through
> sequential cells, we were able to prove that the design is passing EC;
> which meant that there was a bug in the synthesis tool.
>
> - [ Seek And Ye Shall Find ]
From: [ The Silver Surfer ]
Hi John,
Please keep me anonymous.
In ESNUG 464 #4, an anonymous user shares an experience in which DC/PhysOpt
removed 40 DFFs that it should not have done. ConFormal caught the error;
the equivalence checker doing its job, exactly as it should.
But this post appears to be arriving at two conclusions that are just not
supported by the results:
1. "This DC/PhysOpt bug may not be detected if there is side information
provided between DC and Formality."
2. "It's our belief that it is best to avoid passing info directly
from your synthesis tool to EC as it may create assumptions that
may prove wrong."
CALL IN THE MYTHBUSTERS!!!!
This user is trying to conclude guidance files of any kind are always a bad
idea -- but it seems that his experiment did NOT include comparing "with
guidance" to "without guidance." That's the essential comparison, and this
poster doesn't seem to have even tried it in the tool he uses (ConFormal),
let alone the tool he is drawing a conclusion about Formality.
Any Formality user can try the experiment: Remove a flop from your netlist
as if the Design Compiler had mistakenly removed it. Then hand-edit the SVF
to wrongly instruct Formality that this flop was removed because it is a
constant register. When I tried it, Formality rejected the wrong guidance,
said it was doing so, then went on to fail the netlist as non-equivalent.
With guidance, without guidance, or with incorrect guidance, Formality
arrived at the right result every time. I haven't tried it using ConFormal
(with guidance vs. without), so perhaps another poster can provide results
for that.
The statements in ESNUG 464 #4 are still not wrong, but only because of safe
phrasing like "may not be detected" and "It's our belief that..." Without
those weasel-words, I think we would all be looking at a big steel sign
still white-hot from the welding torch, that says:
BUSTED!
- [ The Silver Surfer ]
---- ---- ---- ---- ---- ---- ----
From: [ The Artful Dodger ]
Hi John,
Please keep me anonymous.
I have fox-guarding-the-chickens concerns myself with Synopsys Formality
checking Synopsys DC -- in particular the fact that DW synth views are
common between DC and Formality but are not available to other tools (as
they are encrypted) as described years ago in ESNUG 413 #2.
The SVF hints file is also encrypted, so this info is also not open to
other tools. :-(
However, I'm not sure about the details of this particular item:
"We couldn't find why around 40 DFFs disappeared from our netlist?"
Is he talking about constant DFFs removed by DC?
LEC tools can also try to find constant flops, but will generally find less
or more than DC. If you find *different* numbers of constant DFFs between
DC and LEC, even if all really are constant, you'll get non-equivalences.
Formality can take the constant DFF list from the SVF file, but I believe
that it will verify that these really are constant before relying on these
constraints.
Conformal (Verplex) cannot read the SVF hints file (it's encrypted). You
can ask Conformal to find constant DFFs for the whole design, but it tends
to find a different set -- so gives it differences. You can work around
this problem by getting Conformal to only look for constant DFFs after
mapping; and only in DFFs that are left "Not-Mapped" in the RTL.
Here's the new Conformal command to do this that I use in my LEC scripts:
set system mode lec
remodel -seq_constant -repeat -golden // <-- NEW command for constant
// detection of extra DFFs
// in RTL
add compare points -all
compare
This means Conformal can automatically handle constant DFF optimization
without any hints from DC (and avoids the workaround of disabling this
feature in DC). Oddly, I've not been able to find a sequence to automate
this in Formality (so it has to use the SVF hints file).
I wonder if this fixes his original problem, and gets Conformal to prove
equivalence between RTL and the original optimized netlist.
If there is a real issue (not solved by the above) I'd be interested in
more details.
- [ The Artful Dodger ]
Index
Next->Item
|
|
