Why Use Formality?


Ok, but why, why do we have to use formal verification.
RTL vs Netlist is used to verify that the synthesis has been ok, i.e the resulting
netlist is functionally equal to the RTL. Well we can always simulate the netlist
to verify that the netlist is ok, but netlist sims take time, they can run for hours
days, and in some cases even weeks. Now suppose that after running days of
simulation, you found a very small bug, you fix it in RTL, synthesize it, produce
netlist. Now without the existence of any formal verification, you would run days
of simulation again. With formal verification, you can quickly verify that the netlist
out of synthesis is corresponding to what the RTL is, thus saving you lot of time.

Netlist vs Netlist is may done to verify
1. Pre layout and Post layout netlists : After PnR, you produce a 'post layout' netlist
To check if this netlist is functionally equivalent to the 'pre layout nelitst', formal verification
is a popular choice.
2. eco changes. Suppose you change a gate or
two for fixing timing or for any other purpose. For example you insert a buffer to fix
a hold violation in the netlist manually, you would then like to be sure that nothing else
has broken as a result. Again using formality, you can easily verify it, without it?? run
days long sims again??

BACK(Introduction)                     NEXT( How To Run Formality)

HOME