Equivalence Checking for FPGA Design
As FPGA designs have grown into the millions of gates, the task of verifying such large designs has become increasingly tedious.
Gate-level simulation with a typical design testbench is often not sufficiently exhaustive to provide good coverage, but the effort to create an exhaustive testbench is not only Herculean, but would also result in lengthy simulation times. By adopting ASIC verification techniques, FPGA designers can use equivalence checkers, such as FormalPro™, to quickly verify designs with 100% coverage, thereby keeping projects on schedule and error-free.
Synthesis and equivalence checking tools can work together to accelerate
the verification process, enabling 100% gate-level verification of complex
FPGA designs. Equivalence checking takes a gate-level implementation
of a design and 
compares
its functionality to that of a reference model of the same design.
The reference model is either the RTL model of the design or a known correct gate-level implementation. Formal verification tools, such as the Mentor Graphics® FormalPro equivalence checker, use formal proof algorithms to mathematically prove, or disprove, that the two versions are functionally identical.
View excerpts from Mentor Graphics white paper Equivalence Checking for FPGA Design.
