Verification Techniques for System-Level Design

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 ...