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:

  golden:                  revised:

         ------                   ------
    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:

        -----------
       |A          |
       |B---buf---Z|
       |C          |
        -----------

i.e. A and C had no effect on output Z. Hence the 2 designs are equivalent, based on that incorrect library.

Lesson 1: use Verilog libraries. Running synthesis and verification of the synthesis using the same Liberty or .db library can cause inconsistencies to be missed

Lesson 2: only use Liberty if you validated it against the Verilog*

Lesson 3: leaving a cell black-boxed is better than reading in an incorrect model**

Lesson 4: 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

** we do have an AE-ware script to do strict equivalence checking, where any changes to the connections and/or cell names get flagged.