Hardware Reference
In-Depth Information
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.
Search WWH ::
Custom Search