Debugging non-detected faults using sequential equivalence checking

摘要

Techniques and systems for classifying non-detected faults (NDFs) in a formal verification test-bench are described. A sequential equivalence checking formulation can be constructed based on an integrated circuit (IC) design and a set of NDFs, wherein the set of NDFs do not falsify a first set of properties of the IC design, wherein said constructing the sequential equivalence checking formulation comprises creating a second set of properties based on the set of NDFs, wherein each property in the second set of properties corresponds to an NDF in the set of NDFs. A formal sequential equivalence checking tool can be used to prove the second set of properties in the sequential equivalence checking formulation. Next, for each property in the second set of properties that is disproven by the formal sequential equivalence checking tool, some embodiments can classify a corresponding NDF in the set of NDFs as an observable NDF.