functional and formal verification

[santumevce1412]

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]

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]

+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]

+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]

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]

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]

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.