FormalVerification-and-FunctionalVerification

[reddy]

formal verification gate vs gate

What is the difference between 'Formal Verification' and 'Funtional Verification'?
Please through some light on this topic. If you could know any links/references, it would be of great help for me.

thanks,
-pradeep reddy

 

[yuzhicai]

scan-inserted netlist lec

Formal verification is to conform that the RTL code and the netlist have the same logic.
The functionalverification is to check the function of the design is what you want.

 

[zhangpengyu]

See the book <<writing testbenches>>
You could find the book in Ebook download/upload
forum.

 

[patrickli]

formalVerification use lec, formality tools to check the logic.
functional verification use NC or vcs to run your function pattern.

Sometimes formalVerification can pass, but functional verification will fail.
for example, timing, reset problem...

 

[linuxluo]

hi,
in short ,formal verification is static verification, it does not need any input vector but need more computation power.
on the other hand, func. veri. is dynamic verificatio, need input vectors .

 

[kermit]

Now the main formal verification is equivalence check.that is this tool is to check whether the two things is equivalence,such as RTL code and netlist.

 

[reddy]

Hi Friends,
ThankYou for your reply. but I need detailed information. So, please suggest me some links/documents to get the clear picture of this topic.

thanks,
reddy

 

[kermit]

This is formality user guide.pls enjoy it!

 

[gold_kiss]

hi reddy,

basically formal verification is signoff once you get your netlist and have run few gate level simulations.

Now wht is formal verification?
Basically formal verification is parted down into two
a) Model Checking
b) Equivalence checking

It is nothing else but checking the transformation ...i.e in case of equivalence check you check whether the netlist generated after synthesis (scan inserted) is equivalent to the RTL. You need to specfy few rules. Can check formality manual to get to know more.

Model checking is nothing but specifying some mathematical expression that matches you rtl implementation.

Functional verification is actually running RTL simulations ...post generation and pre generation of stimulus.

Check for the book mentioned above...or even few websites from google.

Cheers,
Gold_kiss

 

[ram]

Functional verification is mainly used to verify what ever specified in Design specifications is corrctly implemented or the RTL codning is done as per specs or not. For this they may bulied a verification enviornment using languages like SystemC or e - language (specman). In simple format functional verification is done by using testbench.

Formal verification is as explained by gold_kiss...



Bye

 

[allanweee]

'Funtional Verification' use the simulator NC or VCS, then have golden RTL.
When you translate into netlist which compare with golden RTL using 'Formal Verification' tool.
That's all

 

[AlexWan]

'Funtional Verification' use the simulator NC or VCS, then have golden RTL.
When you translate into netlist which compare with golden RTL using 'Formal Verification' tool.
That's all

Functional verification not only is done before the synthesis, but is done during pre-simulation and post-simulation. Use the test patterns as the input vectors.

Formal verification is noly compare the function between different design vision. So the formal tool is also used as vision control tool.

 

[claint]

formal verification compares the netlists of different design phase

 

[beta0]

Formal verification and function verification are two different but related categories.
Formal verification sometimes can be used as a kind of static function verification.
function verification is used to check whether your design implement is satisfied with your specification or not.

 

[jayakumarjay]

will the formal verification does full functional verification, is it enough to do formal verification b/w (rtl , netlist) (netlist , netlist)

magma is also releasing formal verification tool and they says it does full functional comparison b/w {rtl,netlist) (netlist , layout netlist)

 

[jayakumarjay]

formal verification is signoff once you get your netlist and have run few gate level simulations.

Now wht is formal verification?


Basically formal verification is parted down into two

a) Model Checking

b) Equivalence checking


It is nothing else but checking the transformation ...i.e in case of

equivalence check you check whether the netlist generated after

synthesis (scan inserted) is equivalent to the RTL. You need to specfy few

rules. Can check formality manual to get to know more.

Model checking is nothing but specifying some mathematical expression

that matches you rtl implementation.

Functional verification is actually running RTL simulations ...post

generation and pre generation of stimulus.

 

[foster_cn]

Could we say formal verification is static verification, while fucntional verification is dynamic verification.

 

[aji_vlsi]

Could we say formal verification is static verification, while fucntional verification is dynamic verification.

Certainly not. Formal Verif. (FV) is part of "functional verification" (FunV). As others mentioned there are mainly 2 classifications to FV:

1. Equivalence Checking
2. Model Checking

(1) - makes sure your RTL matches Gate Level (Or Gate vs. Gate) - so that the "functionality" is intact - hence it is FunV
(2) Mathematically proves that your RTL matches a set of properties, see http://www.noveldv.com for PSL & FV and also do google search on Model Checking.

HTH
Ajeetha
http://www.noveldv.com

 

[AlexWan]

Could we say formal verification is static verification, while fucntional verification is dynamic verification.

Ye,
Normal, functional verification is for functionality completeness. It needs vectors for each path in design.
Formal verification is for functionality equality. It not needs vectors.

Like STA vs. dynamic simulation.

Good Luck

 

[krishna31]

In Functional verfication , we test the completed functionality of the module, but in formal verfication just use for pipecleaning the flow.