VERISEC: VERIfying Equivalence of SEquential Circuits using SAT

In this paper we propose a novel framework to verify equivalence of sequential circuits using Boolean Satisfiability (SAT). We tackle a problem that is harder than the traditional sequential hardware equivalence; specifically, we address the uninvestigated problem of verifiying delay replaceability [1] of two sequential designs. This notion of sequential equivalence does not make any assumptions either about the design-environment or about the design's steady state behavior. Thus, verifying delay replaceability is considered as hard as verifying safe replaceability [1] of sequential circuits (conjectured as EXPSPACE complete). Our SAT-based framework has the following salient features: (a) a methodology to inductively prove equivalence (delay replaceability) of sequential circuits with no assumptions about any initial state; (b) a scheme to include sequential logic implications into the framework; and (c) a low-cost scheme to identify equivalent flip-flop pairs on the fly. We used our tool to successfully verify several sequential benchmark circuits. Low execution times make our framework practical and scalable.