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

Of course, in a real system there is always an upper bound on the request service
time, but if the system implementation changes or if the upper bound is large, then
a liveness property can be more appropriate.
For example, suppose we know that the request service time is bounded by 600
clock ticks, and also that the system implementation may be modified in which case
the upper bound may grow to 700. To make it a safety property, we could have
written the property as

always req |-> ##[1:701] gnt
However, we are not really interested in the exact time bound, and the efficiency of
this bounded safety property in FV is very poor. We thus have a tradeoff between
the safety property, with an automaton comprising more than 700 states and with
about twice as many edges, and the liveness property, with only a couple of states.
Checking the liveness property is likely to be more efficient in this case.

21.4.2.2 Counterexamples for Liveness Properties

There is an important question about liveness property checking: How can infinite
counterexamples be found and reported? Obviously, tools and humans can deal with
finite representations only. Fortunately, it can be shown [ 29 ] that if a property has
an infinite counterexample, then it also has a lasso-shaped counterexample, that is, a
counterexample of the form w 1 w 2 . Here, w 1 and w 2 are finite words, w 1 is a prefix,
and w 2 is an infinitely repeated part. For instance, .a ^ b/ba.ab/ ! has the form w 1 w 2
for w 1 D .a ^ b/ba and w 2 D ab. The lasso-shaped counterexample stems from the
fact that the model has a finite number of states, hence it must in a bounded number
of transitions enter some previously visited state thus forming the lasso loop.

21.4.2.3 Assumptions and Liveness

So far we have considered property classification into safety and liveness from the
point of view of assertions. It turns out that even the simplest assumptions introduce
liveness into the system.

Example 21.25. Given assertion a1 and assumption m1 not in the scope of an
initial procedure, they are equivalent to the assertion a2
m1: assume property (a);
a1: assert property (b);
initial a2: assert property (( always a) implies ( always b));
as explained in Example 22.1 .
For conciseness, we switch now to the notation of the research literature, where
operator always is designated as G, and operator s_eventually as F .Using
this notation, the property corresponding to the assertion a2 may be written as
Ga ! Gb. This property is equivalent to . : Ga/ _ Gb, which is, in its turn,