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 equivalence-checking problem by constructing a pair of normalized cycle-accurate designs from the original designs, on which standard equivalence-checking techniques can then be deployed. We report the results of deploying our techniques on several industrial examples.