( ESNUG 476 Item 2 ) -------------------------------------------- [10/29/08]
From: Boris Evlampiev <eboris=user domain=cs.niisi.ras.ru>
Subject: Strange equivalance problem with DW02_tree function in Formality
Hi, John,
We have some problem in Formality with the DW02_tree function.
Our design (RTL Verilog) contains DW02_tree and DW01_add functions. We use
DC to make synthesis of the netlist. On the next step we try to make formal
verification with help of Formality. Formality concludes that RTL Verilog
does not correspond to netlist?????
We use flat netlist and hierarchical netlist, but the results are identical.
As recomended in Formality documentation we use the dwroot variable, but
result is the same.
When we investigated report of Formality, we see that non-verified flip-flop
are the flip-flop that stand on the output of DW02_tree.
To test our problem we make simple design that contains only DW02_tree.
Formality shows that two design (RTL Verilog and netlist) are not identical.
On the next start read documentation on DW function and in description of
DW02_multp read the following:
"When using the simulation models for DW02_multp, it is important to
understand that because the simulation architecture differs from the
synthetic architecture and the output is given in a redundant carry-save
representation, the values observed at the out0 and out1 output ports
differ from the values seen when using the gate-level netlist of a
compiled design. The two architectures perform the same function, but
the results only match after they are added together (resolved to
irredundant binary representation). Thus, when comparing results
between pre-synthesis and post-synthesis design, the outputs of
instances of DW02_multp will not match, but the final sums after adding
the DW02_multp outputs will match."
We think that somthing like this is taking place in our DW02_tree component.
We modify our design. We make third output C = A + B. Where A and B are
outputs of DW02_tree. Formality show that "C" outputs of RTL Verilog and
netlist are identical.
We dont know what to do with this problem in our original design. Help!
- Boris Evlampiev
NIISI RAN. Moscow, Russia
Index
Next->Item
|
|
