Non-cycle-accurate sequential equivalence checking

We present a novel technique for Sequential Equivalence Checking (SEC) between non-cycle-accurate designs. The problem is routinely encountered in verifying the correctness of a system-level model versus an RTL design which has been derived from the former either manually or through high-level synthesis. The existing state-of-the-art in formal verification/SEC does not provide an efficient mechanism to perform such an equivalence check. Our technique reduces the SEC problem to a cycle-accurate equivalencechecking problem by constructing a pair of normalized cycle-accurate designs from the original designs, on which standard equivalencechecking techniques can then be deployed. We report the results of deploying our techniques on several industrial examples. Categories and Subject Descriptors B.2.2 [Performance Analysis and Design Aids]: Verification; B.5.2, B.6.3, B.7.2 [Design Aids]: Verification General Terms Verification, Algorithms Keywords Sequential Equivalence Checking, Mod...

• Type: Conference
• Year: 2009
• Where: DAC
• Authors: Pankaj Chauhan, Deepak Goyal, Gagan Hasteer, Anmol Mathur, Nikhil Sharma
• Keywords: DAC 2009, Keywords Sequential Equivalence, Normalized Cycle-accurate Designs, Sequential Equivalence