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

Logic Formal Verification -> how does it work?

Status
Not open for further replies.

ivlsi

Advanced Member level 3
Joined
Feb 17, 2012
Messages
879
Helped
17
Reputation
32
Reaction score
16
Trophy points
1,298
Activity points
6,806
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!
 

ivlsi

Advanced Member level 3
Joined
Feb 17, 2012
Messages
879
Helped
17
Reputation
32
Reaction score
16
Trophy points
1,298
Activity points
6,806
You sent a link for SV Assertions, but I asked about Formal Verification.

Are Formal Verification test written using SystemVerilog Assertions?
 

dave_59

Advanced Member level 3
Joined
Dec 15, 2011
Messages
813
Helped
361
Reputation
726
Reaction score
354
Trophy points
1,353
Location
Fremont, CA, USA
Activity points
6,364
Are Formal Verification test written using SystemVerilog Assertions?
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,
 

ivlsi

Advanced Member level 3
Joined
Feb 17, 2012
Messages
879
Helped
17
Reputation
32
Reaction score
16
Trophy points
1,298
Activity points
6,806
static formal tools -> how does it work with? Shouldn't I create testbenches like for dynamic simulation?
 

layowblue

Advanced Member level 4
Joined
Mar 21, 2014
Messages
115
Helped
19
Reputation
38
Reaction score
18
Trophy points
18
Activity points
791
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.
 

ivlsi

Advanced Member level 3
Joined
Feb 17, 2012
Messages
879
Helped
17
Reputation
32
Reaction score
16
Trophy points
1,298
Activity points
6,806
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...
 

dave_59

Advanced Member level 3
Joined
Dec 15, 2011
Messages
813
Helped
361
Reputation
726
Reaction score
354
Trophy points
1,353
Location
Fremont, CA, USA
Activity points
6,364
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
 
  • Like
Reactions: FvM

    FvM

    points: 2
    Helpful Answer Positive Rating

FvM

Super Moderator
Staff member
Joined
Jan 22, 2008
Messages
47,502
Helped
14,052
Reputation
28,359
Reaction score
12,711
Trophy points
1,393
Location
Bochum, Germany
Activity points
276,222
Formal verification is a very complex subject that a few people fully understand, and I have to admit I am not one of them.
Fishing for compliments? Anyway, thanks for the profound explanation.
 

ivlsi

Advanced Member level 3
Joined
Feb 17, 2012
Messages
879
Helped
17
Reputation
32
Reaction score
16
Trophy points
1,298
Activity points
6,806
if you can prove A+1 == 1+A, you can easily prove A will work for any number
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?
 

dave_59

Advanced Member level 3
Joined
Dec 15, 2011
Messages
813
Helped
361
Reputation
726
Reaction score
354
Trophy points
1,353
Location
Fremont, CA, USA
Activity points
6,364
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.
 

Status
Not open for further replies.
Toggle Sidebar

Part and Inventory Search

Welcome to EDABoard.com

Sponsor

Top