Formal verification and conventional verification

[steven852]

Hi,

I wonder when to apply and what the criteria would be in terms of using formal verification tools and conventional verification tools (not sure if this name is right, I mean general tools to do verification: Verilog, VHDL, e, etc). Despite some limitations of formal verification tools (when register retiming, etc), it is pretty powerful, so why do we still need the conventional tools?

Thanks

 

[sree205]

Hi, i have a doubt. i'm new to this concept of formal verication. can u clarify if the functionality can be checked using formal verification ?

 

[steven852]

Sure, formal verification not only can do functional verification but also physical verification (netlist check). In short, 4 combination among RTL and gate-level netlist can be verified as well as library files.

 

[haytham]

The two ways of verification are
1- Formal Verification
2- Functional verifivication

Every one has its own methodologies

 

[sree205]

"formal verification cannot prove that all properties of a design have been enumerated, although for a given property it can prove whether the property is satisfied."

this statement, i got from a book. hope its clear to answer the first question.

 

[steven852]

Well, all you said is true. However, what specific situations are applicable was my question.

Thanks though.

 

[eeeraghu]

Formal verification is used mainly at block level testing, While a designer writes his module to verify whether the module works with respect to all the cases(inputs) according to the assertions given in the design. This can be surely a advantage for verification of the design at an early stage.

thanks & Regards

 

[spauls]

Formal verification cant check for the bugs in RTL.

 

[haytham]

Formal verification cant check for the bugs in RTL.

I think this is not rue. Formal verification is a powerful way to find bugs in your design if you have a well-written assertions and monitors

 

[asping]

Formal verification is to check if it is the same function between your RTL and netlist.

 

[hys]

I feel that some member here do not understand what exactly is "Formal Verification". Lemme try to give a little background....

Formal verification is nothing but trying to solve a problem formally using mathematical approach. There are 3 types involved in it:
1. Model Checking
2. Equivalence Checking
3. Theorem Proving.

"Equivalence Checking" is the most common thing known to everybody but usually referred to a formal verification (Tools: Formality). This is used to check the equivalence between RTL to RTL or RTL to Netlist.

"Model Checking" is where we write formal properties describing the expected behavior and the tools can prove whether that property holds good in all possible conditions. (Tools: Cadence IFV - Incisive Formal Verifier)

Some criteria to look for here are :
- Whenever a design is control intensive it is a very good candidate for model checking.
- If the design is data path intensive it is a best candidate for high level verification languages (e-specman, vera..)


Best Regards,
https://hdlplanet.tripod.com
https://groups.yahoo.com/group/hdlplanet

 

[ivlsi]

So, what's about the Theorem Proving? When used?

- - - Updated - - -

As for the Constraints-driven Random Dynamic Functional Verification, the verification success is measured by the Code Coverage, etc.
How is the Formal Verification success measured?