Logic Formal Verification -> how does it work?

Hi All,

Could someone explain me what is Logic Formal Verification and how it works?

I don't mean LEC (Logic Equivalent Check), but Formal Verification, which check the design against a Spec, not against Gates .

Thank you!

You sent a link for SV Assertions, but I asked about Formal Verification.

Are Formal Verification test written using SystemVerilog Assertions?

ivlsi said:

Are Formal Verification test written using SystemVerilog Assertions?

Click to expand...

Yes. That is the way you write the 'Spec' that checks the design.
You can use either dynamic simulation or static formal tools to perform the checks,

static formal tools -> how does it work with? Shouldn't I create testbenches like for dynamic simulation?

if you are asking how Formal verification tools basically work, here is a general idea.
First of all, as dave_59 said, you have to "tell" the Formal tool your design SPEC, such as bus protocol, constraints, what is expected, or what is not expected, etc.
After you specify your design in a format that formal tool understands, the tool would usually take your design, and enumerate ALL possible "legal" inputs per your "SPEC", then check if the result is legal. If it is not, the tools will usually provide you some information to debug.
Formal verification is very useful on clearly-defined interface, like connections, or AXI bus. But it is limited in high demand of CPU/memory resources for a medium-complexity design, as well as proving scenarios involving long-loop feedback logic, let alone system behavior.

So, then how is Formal Verification different from Constraints-Driven Dynamic Random Verification (like creation testbenches with Specman or SystemVerilog or SystemVerilog Assertions)? Not understood...

Formal verification is a very complex subject that a few people fully understand, and I have to admit I am not one of them.

You can take the simple example of trying to prove the commutative property that A + B == B + A. A constraint driven dynamic random simulation will generate a subset of all possible combinations of A and B with constraints like A != B; to reduce unnecessary patterns. You cannot prove this property this way without exhaustively providing all combinations that meet the constraints. You can take your knowledge from other properties to add more constraints and further reduce the set of required patterns, like A != 0; B != 0;.

Formal verification tries to prove a property without any stimulus by using deductive reasoning logic. (I don't need to get into the entire proof here, but if you can prove A+1 == 1+A, you can easily prove A will work for any number). A formal tool will construct a mathematical proof from a set of axioms to prove a property, and can provide a counter-example if the property turns out to be false.

Dave

Formal verification is a very complex subject that a few people fully understand, and I have to admit I am not one of them.

Click to expand...

Fishing for compliments? Anyway, thanks for the profound explanation.

if you can prove A+1 == 1+A, you can easily prove A will work for any number

Click to expand...

So, in terms of time, should the Formal Verification be "shorter" than dynamic random simulations?

Why is it needed? What gap should it cover? Should it replace the dynamic random verification?

There's no good answer for this. It will depend on the design and the type of assertions you are trying to prove. Static or formal verification many be better as specific applications, so both are needed. static formal tools are much better for checking unreachable states or reset checking.