General Terms Verification, Algorithms

Abstract

We present a novel technique for Sequential Equivalence Checking (SEC) between non-cycle-accurate designs. The problem is rou-tinely encountered in verifying the correctness of a system-level model versus an RTL design which has been derived from the for-mer either manually or through high-level synthesis. The existing state-of-the-art in formal verification/SEC does not provide an effi-cient mechanism to perform such an equivalence check. Our tech-nique 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.