Chapter 4. Verification Algorithms for FSM Models
Combinational Equivalence Checking
Combinational equivalence checking (CEC) of register transfer level (RTL) circuits is the most widely adopted and successful formal validation technology used in modern-day integrated circuit (IC) design flows.
Sequential Equivalence Checking as Combinational Equivalence Checking
RTL circuits arising in the context of IC design flows are usually sequential circuits. There is a often a need to compare two such sequential circuits for equivalence—for example, two copies of the same circuit before and after a sequence of manual or automatic optimization steps, respectively. Several notions of sequential hardware equivalence have been proposed in the literature (e.g ...