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.

Register Log in

functional and formal verification

Status
Not open for further replies.

santumevce1412

Junior Member level 2
Joined
Jan 8, 2008
Messages
24
Helped
0
Reputation
0
Reaction score
0
Trophy points
1,281
Activity points
1,445
functional vs. formal verification

what is the difference between functional and formal verifcation? What r the tools that support these verifications?

Hi
Here i am uploading the verilog pdf...
 

VitalyM4

Junior Member level 3
Joined
Jan 18, 2008
Messages
28
Helped
1
Reputation
2
Reaction score
0
Trophy points
1,281
Activity points
1,459
functional verification vs formal verification

Functional verification means check correspondence of your RTL desciption to your specification. Usually it done by Modelsim, NC-Sim and similar tools.

Formal verification. It is comparing of RTL description (referrence design) with different implementation- after synthesis, scan-chain insertion and so on. Tools Formality, Conformal and others.

Rgds
 

madhavisai

Member level 2
Joined
Feb 3, 2008
Messages
43
Helped
2
Reputation
4
Reaction score
2
Trophy points
1,288
Activity points
1,482
+functional verification is +rtl +vs. formal

functional verification means verifying whether the chdl functionality is correct or not
but formal verification means by using some assertions u can verify without test bench
go for modelsim
 

vizpal

Member level 2
Joined
Apr 26, 2007
Messages
44
Helped
1
Reputation
2
Reaction score
0
Trophy points
1,286
Activity points
1,519
+functional verification is +rtl

Functional Verification is checking your DUT's behaviour on different inputs combinations...
Formal Verification is checking different possible States covered by you DUT...
 

salma ali bakr

Advanced Member level 3
Joined
Jan 27, 2006
Messages
971
Helped
104
Reputation
206
Reaction score
21
Trophy points
1,298
Activity points
7,491
functional verification formal

the difference is the approach of the verification itself

in formal verification for instance, you can use mathematical proof to make sure your design is going to function okay...it can be by: theorem proofing, model checking, equivalence checking...and other different methods....

tools: conformal, formality, etc


functional verification is the big umbrella...it's when you verify that your design works fine compared to its specs....formal verification comes under it...along with dynamic verification (simulation)...emulation...linting for HDL...and other ways..

tools: modelsim, ncverilog, etc
 

delay

Full Member level 4
Joined
Jun 11, 2004
Messages
207
Helped
6
Reputation
12
Reaction score
3
Trophy points
1,298
Location
Van Allen Belt
Activity points
2,221
formal verification

Functional verification is usually exhaustive, checking all boundary conditions to get a golden RTL, it is prior to synthesis. It is generally done using a tool that does timing verification such as NCSIM/SimVision and ModelSim.

Formal verifcation tools compare RTL golden netlist with mapped/gate level/synthesized netlist using formal techniques and algorithms such as bounded model checking, SMV, CTL, or temporal methods by representing the circuit as canonical binary decision diagrams, Kripke structures or even perhaps Petri nets. Bottomline is to determine whether two circuit structures are mathematically equal i.e. they would produce same boolean outputs. This is a rather quick way of verification as opposed to functional.
 

delay

Full Member level 4
Joined
Jun 11, 2004
Messages
207
Helped
6
Reputation
12
Reaction score
3
Trophy points
1,298
Location
Van Allen Belt
Activity points
2,221
formal and functional verification

In EDA industry a subset of formal verification known as logic equivalence check is used mostly for digital designs although formal techniques are being applied to analog designs and mixed signal circuits as well but BDDs and Kirpke graphs are treated as discrete automata having finite states and transitions/paths.

Examples of tools are:
Quartz Formal (Magma)
0-In (Mentor Graphics)
Formal Pro (Mentor Graphics)
Conformal LEC (Cadence)
SLEC (Claypto)
Design Verifyer (Chrysalis/Avant!)
Solidify (Averant)
Formality (Synopsys)

Keep in mind some of these tools are for logic and others are for property checking.
 

Status
Not open for further replies.
Toggle Sidebar

Part and Inventory Search

Welcome to EDABoard.com

Sponsor

Top