( ESNUG 464 Item 14 ) ------------------------------------------- [03/30/07]
Subject: ( DVcon05 #12 ) Conformal saw hierarchy error, Formality didn't
> Mostly Formality, although Verplex does a better job on a few designs.
> Formality has a similar User Interface to other Synopsys tools and SVF
> is a reasonable way of passing "hints" from DC to Formality to speed up
> matching and datapath verification. With all the advanced optimization
> that DC does, like datapath merging and retiming, it is hard for ECs to
> keep up, especially without something like SVF. I think this is a
> challenge for Verplex.
>
> - John Busco of Nvidia
From: [ Don't Ask, Don't Tell ]
Hi, John,
Please keep my name anonymous if this letter gets posted.
I looked at some posts in ESNUG about Formality vs Conformal LEC. I want
to give my 5 cents to it so everybody know our issues with Formality.
1. Long runtime, Formality run never finishes on our design.
2. Usage of SVF/DWSVF is tedious and is not helping in most of
our cases.
We found an issue last year with Formality. Here is the write-up:
We had un-buffered output ports that were connected together at the next
hierarchical level. Here's a little schematic showing the issue:
U1
------------------------
| |
| --------------- |
| | | |
A | - | | Z
--------- mux -- flop ----------
--------- | |
S | | |
------------------------ |
|
U2 |
------------------------ |
| | |
| --------------- | |
| | | | |
A | - | | Z |
--------- mux -- flop ----------
--------- |
S | |
------------------------
Our 'Z' is declared as an output port. Formality respected the port
declaration. Conformal was smarter, treating Z as an inout, which it is,
electrically. Conformal flagged the U1/flop/Q to U2/mux to U2/flop/D and
U2/flop/Q to U1/mux to U1/flop/D paths that we didn't realize existed.
The fixes of course were to insert a buffer between the feedback to MUX
and the output and to remove the multiple-driven net.
U1
----------------------------
| |
| --------------- |
| | | |
A | - | | Z
--------- mux -- flop --- buf ------
--------- |
S | |
----------------------------
U2
----------------------------
| |
| --------------- |
| | | |
A | - | | Z
--------- mux -- flop --- buf ------
--------- |
S | |
----------------------------
This is using
Conformal: Version 05.20-p101 (11-Nov-2005)
Formality: version 2005.06
We haven't run this through a 2006 version of Formality, so this issue might
be gone now.
- [ Don't Ask, Don't Tell ]
Index
|
|
