Formal Verification

Formal Verification refers to the process of establishing functional
equivalence of two designs generally represented as HDL models without running simulations.
Most common use of formal verification is to establish functional equivalence of
RTL model which is called the reference design(ref) and a corresponding netlist which is
called the implemented design(Impl).
RTL vs Netlist equivalence checking using formal verification is relatively
a new step added to the ASIC design process.

The following combinations are normally acceptable
Ref             Impl
RTL            RTL
RTL            Netlist
Netlist        Netlist
 
Normally the functional equivalence of two HDL designs is established by simulation
of the the two using the same test vectors, and observing the response from the two.
But Formal verification does it without running simulations, making the verification process
checking very fast.

Why Formal Verification?
1. As the ASICs are becoming larger and complex, the netlist simulation is
becoming a very time consuming process, and its not worth running weeks
of netlist simulations corresponding to a very small change in RTL just
to establish that the netlist is good. Formal verification is an answer to such
a problem
2. Often the late fixes also called ECOs, need to be verified quickly without
running lengthy simulations. Formal verification is an answer to it.
3. Formal verification is also a double check on your synthesis tool, that it
is doing the right job.

Examples of EDA tools for formal verification.
Formality from Synopsys
Co-formal from Cadence