Formal Verification - what is the meaning?

[vlsi_freak]

Formal Verification

Hi All,

What is the meaning and help of Formal Verification ?
In which stage FV is done ? Is there any relation with Functional Verification. ?

regards,
freak

 

[mailsrikanth007]

Re: Formal Verification

FV does equivalence checking between two designs. If a design is functionally verified then any further modifications to that design is formally verified with original design. This avoids multiple functional verification.

FV is generally done after DFT, BIST insertion to avoid functional verification again. The DFT,BIST logic is disabled and the netlist without DFT, BIST is formally verified with DFT,BIST inserted netlist.

FV takes less time compared to functional verification and is extensively used in industries.

 

[koggestone]

Re: Formal Verification

note that the term "formal verification" (FV) is used for 2 things
- Equivalency checking
- Property checking

"equivalency checking" (aka EC) is used compare one RTL model matches another RTL model 100% . eg. Cadence LEC , Synopsys Formality.


"Property checking" is used to verify that your assertions are valid 100%.
eg. Jasper Design Tool , Synopsys Magellan , Real Intent tool , etc ...

Functional Verification is not 100%
Formal Verification is 100% Match .

 

[Nandy]

Formal Verification

Formal verification is to check if DesignA==DesignB, but they may have wrong functions even they are equal. So functional verification (VCS/ModelSim) has to be run to verify one of them has correct functions. And run formal verification again to check the other one equals the function-correct one.
Functional verification is not practical to run on huge size netlist. So you run functional verification on the RTL and use fomal verification to check RTL=Netlist

 

[vmittal]

Re: Formal Verification

Just do a little googling on 'formal verification' and you will find that it's broadly categorized as:
1. Equivalence checking (tools like formality) - generally used for checking equivalence between RTL & corresponding netlist
2. Model checking (tools like Magellan) - generally used for RTL functional verification
3. Theorem proving