about formal verification

[cnz]

formal verification

Hi all,
usually,we use synopsys formality or cadence verplex-lec to do formal verification.
Formal verification includes two type,one is equivalence checking,another is model checking.
in its most common use,equivalence checking can do a check between RTL and netlist or between netlist and eco netlist without any test vector.
however, I want to know,what is the principle of formal verification?why
formal verification can do this?
Any help is appreciated.
thanks.

 

[jayant]

using formality for formal verification can flag errors when you convet ur design from one stag to another say from rtl to netlist. you can easily find out any problems occured during coversion.

 

[masai_mara]

Formal verification is static verification of the design as opposed to dynamic verification where the design is tested with a number of test vectors. In formal verification no test vectors are involved but the design is verified using formal methods such as theorem proving and model checking. Theorem proving is the most general kind of formal verification where the specifications and the design are reduced to expressions of mathematical logic to be proven as equivalent using some higher order logic. But this is not come out of labs yet, or maybe to some extent in intel or IBM. But model checking is another way in which the design is reduced to a finite state machine and checked for all paths and those leading to an error condition are flagged. Model checking is done using symbolic trajectory evaluation in which Binary decision diagrams(BDDs) play a vital role. Model checking is recently picking up and quite a few commercial tools are out there. Equivalence checking is the simplest version of formal verification where in given two formats of a design(say, rtl Vs gate) their fucntional equivalence is proven using techniques such as structural isomerism, ATPG and some BDDs also. equivalence checking has been around for some time and has seen some good success with formality and verplex being the leading tools. So it basically checks implementation of a design, not the actual design.
So, the basic difference is its static in the sense that you dont have to simulate the design using test vectors and hence is very fast(>10x) compared to dynamic verification but the drawback is uptill now only control logic in a design is amenable for formal verification and so actually cannot replace dynamic verification for large datapath structures.

 

[maxsnail]

actually verplex lec cand do some lint check for rtl

 

[a0000442]

good ,