Welcome to EDAboard.com

Welcome to our site! EDAboard.com is an international Electronic 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.

Register Log in

what is formal verification

Status
Not open for further replies.

eda_wiz

Advanced Member level 2
Joined
Nov 7, 2001
Messages
654
Helped
57
Reputation
114
Reaction score
29
Trophy points
1,308
Activity points
6,195
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

Member level 5
Joined
Sep 13, 2002
Messages
86
Helped
0
Reputation
0
Reaction score
0
Trophy points
1,286
Activity points
616
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

Member level 5
Joined
Sep 13, 2002
Messages
86
Helped
0
Reputation
0
Reaction score
0
Trophy points
1,286
Activity points
616
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

Member level 5
Joined
Sep 13, 2002
Messages
86
Helped
0
Reputation
0
Reaction score
0
Trophy points
1,286
Activity points
616
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

Member level 5
Joined
Apr 19, 2004
Messages
89
Helped
3
Reputation
6
Reaction score
1
Trophy points
1,288
Activity points
910
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... ;(
 

Status
Not open for further replies.
Toggle Sidebar

Part and Inventory Search

Welcome to EDABoard.com

Sponsor

Top