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