Welcome to EDAboard.com

Welcome to our site! EDAboard.com is an international Electronics 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.

Property checkers can mathematically prove/disprove assertions, do we still simulate?

Status
Not open for further replies.

matrixofdynamism

Advanced Member level 2
Joined
Apr 17, 2011
Messages
565
Helped
24
Reputation
48
Reaction score
23
Trophy points
1,298
Activity points
7,369
Formal tools called property checkers can mathematically prove that, given an RTL design and some assumptions about the relationships of the input signals, an assertion will always hold true. If a counter example is found, the formal tool will provide details on the sequence of events that leads to the assertion violation.

If this is true, do we still need to carry out simulation with all those assertions? Can you give me example of an actual property (also known as assertion prover) checker as I think this funtionality is not present in ModelSim and Formal verification tools are quite expensive.

I must say, I am quite intrigued by these formal verification tools! Does Static Timing Analyzer form part of Formal verification tools as it also uses mathematics to verify that the design has no timing violations and does not need input stimulus or simulation to do this.
 

K-J

Advanced Member level 2
Joined
Jan 26, 2012
Messages
658
Helped
308
Reputation
620
Reaction score
301
Trophy points
1,343
Activity points
7,053
Formal tools called property checkers can mathematically prove that, given an RTL design and some assumptions about the relationships of the input signals, an assertion will always hold true.
'Some assumptions' potentially being not valid would be a reason to not totally rely on this method.

If this is true, do we still need to carry out simulation with all those assertions?
Do you really think that every functional requirement of a design can be expressed as the input to a formal property checker (Examples: MPEG or JPEG encoder; USB or Ethernet interface; interface to some microprocessor)? How do you verify that the input to the formal property checker is accurate?

I must say, I am quite intrigued by these formal verification tools!
They would be a neat addition to a verification toolkit...but not all by themselves.
Does Static Timing Analyzer form part of Formal verification tools as it also uses mathematics to verify that the design has no timing violations and does not need input stimulus or simulation to do this.
No, static timing analysis doesn't formally 'prove' anything. What it does is to compute min and max arrival times of signals and validate whether a given signal violates any constraint with some other signals min/max arrival time.

Kevin Jennings
 
Status
Not open for further replies.

Part and Inventory Search

Welcome to EDABoard.com

Sponsor

Top