TIP OF THE MONTH: gate to gate EC, with different synthesis engines
I have netlist A and netlist B from the same RTL. Can I compare equivalency of the two netlists?
This question often comes up when a customer has RTL to netlist A that has passed previous EC run, but decides to produce a netlist B from the same RTL due to change in synthesis strategy.
Comparison between gate netlists is usually faster to perform than RTL to netlist. However if the two netlists are produced from different synthesis runs, user typically cannot use equivalency checking to prove equivalency.
The main reason for this is the usage of X in RTL. RTL almost always contains X's, which creates a Don't Care (DC) space in implementation. Synthesis has freedom on how these Don't Cares are optimized away - and it often is the case that two netlists from same RTL differs in DC optimizations.
Common ways to introduce X in RTL are:
1) case default X assignment,
2) else clause X assignment, and
3) parallel case/full case directive.
From past experiences, X optimizations don't seem to have deterministic results, although all the factors stay constant (same OS, version of the tool, script).
A secondary reason for gate-gate difficulties would be differing datapath optimizations. If the structures of the 2 netlists were implemented differently, EC could result in aborts. Then the best course of action is to do 2 RTL vs gate runs, where 'analyze multiplier' and 'analyze datapath' can make use of the word-level information in the RTL (e.g. '*' or '+') to understand the datapath transforms.
Note that, if the design you are verifying is completely free from X assignments or datapath elements, comparing two netlists from different synthesis runs should be possible. Also, any subsequent netlist produced from the seed netlist can be compared to each other. |