I recently encountered a testcase that confirmed the old saying: "garbage in, garbage out".
The customer was running a gate-gate verification using an incorrect Liberty library (source for .db) and that caused a difference to be missed. Here are the details:
A --|A | C --|A |
B --|B Z|-- Z B --|B Z|-- Z
C --|C | A --|C |
Note the swapped connections for pins A and C. The problem was that the cell was incorrectly described as:
i.e. A and C had no effect on output Z. Hence the 2 designs are equivalent, based on that incorrect, incomplete library.
- use Verilog libraries. Running synthesis and verification of the synthesis using the same Liberty or .db library can cause inconsistencies to be missed
- only use Liberty if you validated it against the Verilog*
- leaving a cell black-boxed is better than reading in an incorrect model**
- consider using Conformal GXL to validate the Verilog libraries against the Spice
Again, remember: "garbage in, garbage out"
* on Sourcelink, search for "library qualification" under Conformal for details on how to run it. It should be the first solution search returns
** we do have an AE-ware script to do strict equivalence checking, where any changes to the connections and/or cell names get flaggedOriginally posted in cdnusers.org by croy