What would you do to solve non-equivalence in timing ECO?

[Nandy]

This is a real case. A timing ECO iteration added an extra inverter somewhere in the design. Hundreds of inverters/buffers have been added, it's impossible to check one by one to see which inverter is the extra one. Debugging with Formal tools shows lots of support points causing the mismatches, but it doesn't help too much. What would you do if it happens in your timing closure? Well, revert back the database can solve the problem, but the flow still needs to be checked how the extra inverter is introduced.
Check the following link to see how Gates On the Fly solve the issue by the built-in Logic Equivalence Check feature.
https://www.nandigits.com/use_case_find_extra_inv.htm

 

[RCircuit]

There is one problem, the link shows flipflop equivalence is done on data pin only, clock pin should also involve in equal check, especially when driven by gated clock, the clock enable is essentially a MUX select.

 

[Nandy]

Thanks for pointing out. Actually for timing ECO case, it's enough to compare D pins. In full function comparing mode, two flop instances should be selected and compared. Check the image for flop to flop equivalence check.