Formal Verification and Models - SVA: The Power of Assertions in SystemVerilog - page 465

21.4.2 Liveness Properties

Model checking of liveness properties is significantly more complex than model
checking of safety properties. Liveness properties cannot be verified using direct
reachability analysis. This is because for safety properties any path to a bad state
is finite, and all counterexamples found this way are necessarily finite, while liveness
properties have infinite counterexamples. Checking liveness properties is much less
efficient than checking safety properties because the tool must search (explicitly or
implicitly) for infinite cycles in the model that do not satisfy the property.

Efficiency Tip. Avoid writing liveness properties unless they are absolutely neces-
sary.

Example 21.23. To check that some condition c holds between two events ev1 and
ev2 implemented as Boolean expressions, we can write the following property:
always ev1 |-> c s_until_with ev2 . Before we proceed further, we should
ask ourselves whether this property is one that we really need to check. It verifies
two things:
1. c holds between ev1 and ev2 , and
2. Each time that ev1 holds, ev2 also eventually holds.
Do we really want to check the second condition which is liveness?
Usually, the answer is “no”. If not, we should rewrite the property as
always ev1 |-> c until_with ev2 . This property is safety, and it only checks
for the first condition. 9 t

Example 21.24. To check that each request is granted, we can write the following
property: always req |=> s_eventually gnt . This property is liveness, and in
this case liveness is what we actually want. Although this property is expensive, we
are prepared to pay for it. t

21.4.2.1 Why Write Liveness Properties?

Why should we write liveness properties if they are expensive? There may be several
reasons for doing so. One common reason is to check that there is no starvation in
the system. For example, if a CPU needs to access some resource, this resource
should be eventually available.
Another common reason to use liveness properties is specification abstraction.
For example, we might need to ensure that each request is eventually granted. The
following liveness property is suitable for this purpose:
always req |-> s_eventually gnt

9 By a chance the operator s_until_with has a clumsier syntax in SVA than the operator
until_with : this was done to make the safety property until_with a natural choice.