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!
Your comments will be moderated before it appears here.