FORMAL EQUIVALENCE CHECKING BETWEEN TWO MODELS OF A CIRCUIT DESIGN USING CHECKPOINTS

Some embodiments of the present invention provide techniques and systems for determining whether a high-level model (HLM) for a circuit design is equivalent to a register-transfer-level (RTL) model for the circuit design. During operation, a system can identify a set of checkpoints. Each checkpoint can be associated with a characteristic function defined over the states of a finite-state-machine (FSM) representation of the HLM, a characteristic function defined over the states of an FSM representation of the RTL model, and an invariant defined over a set of variables in the HLM and a set of registers in the RTL model. Next, the system can generate a set of invariant proof problems, wherein each invariant proof problem corresponds to a transition between two checkpoints in the set of checkpoints. The system can then determine whether the HLM is equivalent to the RTL model by solving the set of invariant proof problems.