Formal Verification or EquivalenceChecking

Design verification, must show that the design, expressed at the RTL or structural level, implements the operations described in the data sheet or whatever other specification exists.

Verification at the RTL level can be accomplished by means of simulation, but there is a growing tendency to supplement simulation with formal methods such as model checking. At the structural level the use of equivalence checking is becoming standard procedure. In this operation the RTL model is compared to a structural model, which may have been synthesized by software or created manually. Equivalence checking can determine if the two levels of abstraction are equivalent. If they differ, equivalence checking can identify where they differ and can also identify what logic values cause a difference in response.

Updates: 18th Dec 2008 !
Another series of steps in equivalence checking goes beyond what was described above...

RTL to Pre-Synthesis Netlist!
Pre-Synthesis Netlist Vs Post Synthesis Netlist!