RTL verification remains the bottleneck in digital hardware design. Industry surveys show that functional verification accounts for 70% of the total design effort. Yet despite the emphasis on verification, over 60% of all design tape-outs require a re-spin. The predominated cause for re-spins is logic or functional flaws. That is, defects that could have been caught by functional verification. Clearly improved verification techniques are needed.

Design teams commonly use system models for verification. System models have many advantages over RTL for verification, namely ease of development and runtime performance. The challenge is bridging the gap between system-level verification and creating functionally correct RTL. Sequential Logic Equivalence Checking (SLEC) has the unique capability to bridge this gap by formally verifying RTL implementations against a specification written in C/C++ or SystemC.