Continue to Site

Welcome to

Welcome to our site! is an international Electronics Discussion Forum focused on EDA software, circuits, schematics, books, theory, papers, asic, pld, 8051, DSP, Network, RF, Analog Design, PCB, Service Manuals... and a whole lot more! To participate you need to register. Registration is free. Click here to register now.

what is formal verification

Not open for further replies.


Advanced Member level 2
Nov 7, 2001
Reaction score
Trophy points
Activity points
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

3.RTL Coding
4. Verification
6.Test Insertion
.... and goes on

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



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.

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...

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..)

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... ;(

Not open for further replies.

Part and Inventory Search

Welcome to