differnce between by formal verification and Logic equivalence checking

Is formal verification is same as Logic equivalence checking (LEC) for which the tools are formality by Synopsys and Conformal LEC by cadence.

Logic Equivalence checking(LEC) is a Formal verifcation tool

dcreaddy1980

So formal verification can be accomplished by LEC tools. But some persons say formal verification is something different than LEC. That was even in contradiction to my earlier idea THAT "Logic Equivalence checking(LEC) is a Formal verifcation tool". I FIND U ALSO THINKS THE SAME.

Some people thinks formal verification is related to functional verification. I do not understand how this is true. Do u have any idea of this?

Do you think formal verification can mean something elec othe than equivalence checking of two circuits/systems.

Regards

Property checking is also a part of Formal Verification.

Your statement : Formal verification is related to Functional Veriifcation

This can be true, but will give you a scenario where the above statement can be true.

Lets take you have implemented an algorithm for certain functionality and you have completely verified the functionallity with gate level simulation and good coverage of tests are done this algorithm written in RTL. But there was a change in requirement w.r.t Area/Speed. Now you implemented different algorithm keeping in mind of the same functionality.

Instead of running your new algorithm through Simulation, you can simply perform LEC on these oldd agorithm and new algorith. This way you have done functional verification of your new algorithm.

I hope you agree with my statements.

dcreddy1980 said:

Property checking is also a part of Formal Verification.

Click to expand...

What do you mean by property here?


You were talking of verification of algorithm. But people talks of formal verification of designs by Synopsys vcs !!!!

Here is a good document : http://www.jasper-da.com/newsevents/formal prop checking what users say.pdf

In simple words, Property is identical to Assertion. The properties can be simulated or Formally verified.

Can you provide some docs which support your statement : But people talks of formal verification of designs by Synopsys vcs !!!!

LEC is for RTL vs NETLIST comparion! Formal verification is for property check !

ljxpjpjljx said:

LEC is for RTL vs NETLIST comparion! Formal verification is for property check !

Click to expand...

disagree, but don't angry.

formal verification can be classified into 2 types:
1. logic equivalent.
2. property check.