( ESNUG 465 Item 2 ) -------------------------------------------- [06/28/07]
Subject: ( ESNUG 464 #4 ) Yup, Formality side files are nothing but trouble
> 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: Tom Mannos <tjmanno=user domain=sandia.gov>
Hi, John,
You know, I've always been wary of those SVF files. Yes, I know why they
exist. DC makes so many optimizations that cross hierarchical boundaries,
making checking for functional equivalence a difficult task, particularly
if you have any DesignWare components. Granted. I'm not opposed to the
two tools passing information, as long as I can see what it is. I called
Synopsys tech support, and they said in the future the format will be more
open, but for now it's just a binary file I can't read. It's a little
tough explaining this to my manager:
Q: Who's in charge of logic synthesis for this design?
A: Synopsys.
Q: Are you doing any independent verification of Synopsys's work?
A: Yes, of course.
Q: And who's doing that?
A: Synopsys.
Q: How does that work?
A: Oh, it's a formal process that proves beyond any doubt that the
two designs are equivalent.
Q: Sounds complicated. How are exceptions handled?
A: Well, the two tools kinda pass notes to each other.
Q: What do those notes say?
A: I don't know, I can't read them. They're secret notes.
So, in addition to formal EC, we re-run all our tests on the post-layout
netlist with back-annotated delays. If there are any missing registers, it
would be blatently obvious after a few sims. I recommend doing this anyway,
as it may uncover timing-related issues you didn't catch in PrimeTime.
- Tom Mannos
Sandia National Labs. Albuquerque, NM
---- ---- ---- ---- ---- ---- ----
From: [ One of the Yellow Turbans ]
Hello John,
Please keep me anonymous. I develop CAD flows for a consumer chip company
in Taiwan. I read recent postings on Conformal and Formality.
My experience in using Formality with sidefile is bad.
In my previous company, we had a design with DW02_mult (10X17) istantiated.
For some reason, DC synthesized the multiplier with the 4 LSB PRODUCT bits
tied to 0 and the sidefile declared these bits are sequential constant.
Formality compared the RTL to the synthesized gate as EQ based on the
incorrect information in the sidefile. We didn't know the comparison result
was incorrect until we ran gate-level simulation.
We tried Conformal-LEC and it found the bug right away.
This is one of the reasons that I don't feel comfortable in using Formality
with sidefile.
The current company that I am working with now has been using Conformal for
years. They use it right before delivering netlists to back-end team and
before tape-out. Because of the increase of DC synthesis bugs in DC-0606
and 0612, we run LEC more often and earlier in our design cycle. We also
run Conformal LEC for our ECO cases.
Recently, Synopsys sales recommended to my boss to try the new version of
Formality. Formality failed to complete the comparisons for almost all the
netlists with complex datapath (filters and some sum-of-product) if its
sidefile is not read in! This is bad and dangerous in a verification flow,
because if there is an ECO in the module with datapath, the original
sidefile may not be correct any more. It would be very difficult for the
designer to figure out if his ECO leads to any bug by using Formality.
Also, once the DC synthesized netlist is optimized with a non-Synopsys
backend tool, there is no sidefile generated for Formality to complete
the comparison.
As long as Conformal-LEC is high performance and not use sidefiles and
works with any EDA flow independently, we will keep using LEC as our
sign-off verification tool.
- [ One of the Yellow Turbans ]
Index
Next->Item
|
|
