what is formal verification

[eda_wiz]

hi all, I have heard a lot about this.. but dont really know what it is and why do we need this tool....

My concept of RTL2GDSII flow

1.specification
2.Design
3.RTL Coding
4. Verification
5.Synthesis
6.Test Insertion
.... and goes on


where in this flow will formal verification come into picture
And also what is equivalence checkers?

Thanks

 

[asterix91]

Hi

Here is what little i know...

Formal verification techniques come under the Verification stage as per your flow..

The usual standard verification techniques involve providing a test vector ( or a wave form) to the Design and observing the out put for any failures. So one can say the Correctness of the design is proportional to the coverage of your test vector.

In Formal verification techniques, instead of test vectors the tool checks that if certain basic conditions defined by the user are met ( or not voilated ) under all circumstances. Mind you this is not a explorative procedure but a exhuative procedure as thing like binary decision trees , state space explosion etc are used to check the correctness of the circuit mathematically.

 

[asterix91]

There are a couple of techniques such as static assertion based verification, and dynamic assertion based verification in which the user can define assertions such as "A should always be 1", or "A'B = 0" then the engine check that such assertion should never fail...

 

[asterix91]

eqivalence checkers are just tools which check if the two different format representations of the same design is exactly equal or not ..

It may also be used to check eqivalence between same format representation coming from different sources..

Currently this is a area in which some very good and efficient tools are avialable (must be easy to make..)

 

[sandusty]

HI, Wizkid:

You would like to use formal verification:

1. after the buffer insertion, cts... compared the generated netlist is functionally the same as data-in
2. after eco
3. last check before tapeout

of course you can check your rtl code is same with the gate level too... but I don't use it often.
Sometimes, we used it for re-writing codes... but it's not very useful... ;(