Patent ID: 8201119

Claim:
A method 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, the method comprising: identifying a set of checkpoints, wherein each checkpoint is associated with: a first component which specifies a first characteristic function using one or more states of a finite-state-machine (FSM) representation of the HLM; a second component which specifies a second characteristic function using one or more states of an FSM representation of the RTL model; and a third component which describes an invariant using a set of variables in the HLM and a set of registers in the RTL model; generating a set of invariant proof problems, wherein each invariant proof problem corresponds to a transition between two checkpoints in the set of checkpoints; and determining, using a computer, whether the HLM is equivalent to the RTL model by solving the set of invariant proof problems.