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