Incisive Conformal ASIC

With thousands of Tapeouts, Conformal ASIC is the most widely-supported equivalency checking tool in the industry. It's also production-proven with more physical design closure tools, advanced synthesis tools, ASIC libraries, and IP cores than any other formal verification tool. Many EDA tool vendors rely on Conformal ASIC as an independent standard within their regression suites to verify the results that their own tools produce.

Key Features:
    * Minimizes re-spin risk by providing complete verification coverage
    * Reduces verification time significantly by verifying multi-million gate designs by orders of magnitude faster than traditional gate-level simulation
    * Independent verification technology decreases the risk of missing critical bugs
    * Faster, more accurate bug detection and correction throughout the entire design flow
    * Provides capacity to handle designs of tens of millions of gates
    * Eliminates functional clock domain crossing problems before simulation
    * Easy to learn and easy to use
    * Structural checks perform bus checks for data conflicts, set-reset exclusivity checks, and multi-port latch contention checks
    * Clock domain checks perform synchronization validation and data stability checks
    * Full cross-highlighting between debug, schematic, and RTL source code windows

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!