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.

Formal verification and conventional verification

Status
Not open for further replies.

steven852

Advanced Member level 4
Joined
Apr 24, 2005
Messages
101
Helped
2
Reputation
4
Reaction score
1
Trophy points
1,298
Activity points
2,040
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

Advanced Member level 1
Joined
Mar 13, 2006
Messages
454
Helped
58
Reputation
116
Reaction score
24
Trophy points
1,298
Activity points
4,415
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

Advanced Member level 4
Joined
Apr 24, 2005
Messages
101
Helped
2
Reputation
4
Reaction score
1
Trophy points
1,298
Activity points
2,040
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

Full Member level 4
Joined
Jun 6, 2004
Messages
229
Helped
16
Reputation
32
Reaction score
2
Trophy points
1,298
Activity points
1,365
The two ways of verification are
1- Formal Verification
2- Functional verifivication

Every one has its own methodologies
 

sree205

Advanced Member level 1
Joined
Mar 13, 2006
Messages
454
Helped
58
Reputation
116
Reaction score
24
Trophy points
1,298
Activity points
4,415
"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

Advanced Member level 4
Joined
Apr 24, 2005
Messages
101
Helped
2
Reputation
4
Reaction score
1
Trophy points
1,298
Activity points
2,040
Well, all you said is true. However, what specific situations are applicable was my question.

Thanks though.
 

eeeraghu

Full Member level 4
Joined
Jun 3, 2005
Messages
222
Helped
26
Reputation
50
Reaction score
9
Trophy points
1,298
Activity points
3,384
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
 
  • Like
Reactions: ivlsi

    ivlsi

    Points: 2
    Helpful Answer Positive Rating

spauls

Advanced Member level 2
Joined
Dec 17, 2002
Messages
524
Helped
26
Reputation
52
Reaction score
9
Trophy points
1,298
Activity points
3,354
Formal verification cant check for the bugs in RTL.
 

haytham

Full Member level 4
Joined
Jun 6, 2004
Messages
229
Helped
16
Reputation
32
Reaction score
2
Trophy points
1,298
Activity points
1,365
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
 
  • Like
Reactions: ivlsi

    ivlsi

    Points: 2
    Helpful Answer Positive Rating

asping

Newbie level 6
Joined
Jan 7, 2006
Messages
12
Helped
0
Reputation
0
Reaction score
0
Trophy points
1,281
Activity points
1,338
Formal verification is to check if it is the same function between your RTL and netlist.
 

hys

Member level 1
Joined
Mar 15, 2006
Messages
41
Helped
5
Reputation
10
Reaction score
3
Trophy points
1,288
Activity points
1,581
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,
http://hdlplanet.tripod.com
http://groups.yahoo.com/group/hdlplanet
 
  • Like
Reactions: ivlsi

    ivlsi

    Points: 2
    Helpful Answer Positive Rating

ivlsi

Advanced Member level 3
Joined
Feb 17, 2012
Messages
880
Helped
17
Reputation
32
Reaction score
16
Trophy points
1,298
Activity points
6,811
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?
 

Status
Not open for further replies.

Part and Inventory Search

Welcome to EDABoard.com

Sponsor

Top