( ESNUG 483 Item 1 ) -------------------------------------------- [11/30/09]
From: Laurent Besson <laurent.besson=user domain=stericsson.com>
Subject: Formality messes up if any non-DC-generated UPF code is used
Hi John,
My name is Laurent Besson. I work at ST-Ericsson. I have near 15 years of
experience in the field of synthesis, equivalence checking but I have also
worked on P&R, DRC/LVS tools, etc....
I recently put in place a UPF-based synthesis flow using Design-Compiler for
synthesis and Formality as the equivalent checking tool. Formality in UPF
mode is very simple to use. Compared to a standard Synopsys flow, you just
have to load a UPF in the "reference" container and another one in the
"implementation" container. That's it!
But this is too simple and can lead to a real false positive! I have filled
two SolvNet cases (8000281573 & 8000347291) on this but Formality R&D seems
not convinced and did not comment further on this problem. This is why I
want to warn the Formality community about this possible verification hole.
To give you more technical detail, here is what happens: As I said, the UPF
flow inside Formality is very simple (load_upf en both containers) but the
treatment of this UPF is not the same between the RTL and the gate netlist.
When applying to the RTL, Formality needs to infer by itself the low-power
feature. In the gate netlist, Formality must "verify" without any
modification. So by using the same command (load_upf), Formality has two
behaviors. This is done thanks to a simple comment on the first line of
the UPF file written by DC as in this example:
#Generated by Design Compiler(B-2008.09-SP5) on Oct 13 20:13 2009
create_power_domain PD_top
...
This is where there is a potential false positive in Formality. If a user
reads a UPF file that DOES NOT contain this pseudo-comment line in the
"implementation", Formality will infer the low-power cells and THUS WILL
NOT VERIFY ANYTHING!!!
The funny thing in this is the following trick: I just used one simple
Ctrl-T in emacs on the first line to change it this way:
#Generated by Desing Compiler(B-2008.09-SP5) on Oct 13 20:13 2009
create_power_domain PD_top
...
(Note: It's "Desing" instead of "Design" Compiler here.) And this also
succeeded in creating a false positive!!!!!
Or I could have also done this:
#Generated by Design Compiler(B-2008.09-SP5) on Oct 13 20:13 2009
create_power_domain PD_top
...
(Note: There are 2 blank spaces between "Design" and "Compiler" here.)
Formality R&D is refusing to take care of this problem because they say I'm
out of the flow. Their supposition is that every gate-netlist UPF file is
obviously coming from Design Compiler. But today DC is not the only tool
to write a UPF file (Mentor Olympus is another example) and moreover,
Formality should not, in any way, rely on a comment in the first line of
a UPF file whether or not to infer the low-power cells.
John, could you inform Formality users about this gap in the equivalence
checking flow? I think having a false positive is too dangerous to keep
this information just between Synopsys R&D and myself.
- Laurent Besson
ST-Ericsson Grenoble, France
Join
Index
Next->Item
|
|
