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

[matrixofdynamism]

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]

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