Hardware Reference
In-Depth Information
equivalent to .F
:
a/
_
Gb. The latter form explicitly contains an eventuality, and
shows that
a2
is a general liveness assertion. Hence, the combination of
m1
and
a1
introduces liveness condition into the system.
t
Example
21.25
shows that all assumptions of the form
always
q
, that is, the
vast majority of all assumptions, introduce liveness.
10
To understand why, consider
some assertion p and an assumption of the form Ga stating that a is an invariant
of the system. Assume, for simplicity, that p is a safety property. Suppose that at
some time i assertion p fails on trace
w
. In other words, the trace prefix
w
0;i
is
a counterexample of
p:
w
0;i
6ˆ
p. We are ignoring the assumption Ga for a
moment. Assume now that the assumption Ga holds on the trace prefix
w
0;i
, that
is, a holds at each position of
w
from 0 to i (inclusive). Does it mean that
w
0;i
is
a real counterexample of p? Strictly speaking, no: if a
D
false
at some point in
time j>i, then assumption Ga does not hold, and therefore assertion p holds
(vacuously).
In practice, invariant assumptions are always used, which means that the model
checking of safety properties is not relevant at all—if we take assumptions into
account, all our properties become liveness! In spite of this, the FV tools usually
ignore the liveness component introduced by assumptions when checking safety
properties and only check that until the time of an assertion failure no assumptions
have been violated. Some tools even check that the assumptions are not violated
a few more global clock ticks after the assertion violation. Strictly speaking, this
is incorrect, but it is a reasonable compromise. Also, this method is safe: if the
assertion passes then the subsequent behavior of an assumption is not important.
21.4.2.4
Automata of Clocked Properties
In Sect.
21.4.1
, we showed that safety properties may be represented as finite
automata. How will the property automaton change if we take the property's clock
into account?
Consider property
@c a |=> b
. We assume that occurrence of clocking event
@c
has been resolved to testing of a Boolean expression
c
with respect to the global
clock (see Sect.
20.4
). The automaton for the property complement is shown in
Fig.
21.7
(the corresponding unclocked version is shown in Fig.
21.4
).
a
∧
c
¬
b
∧
c
s
1
s
2
s
3
Fig. 21.7
Automaton for
complement of property
@c
always
a |=> b
true
¬
c
10
We are not talking about corner cases such as when the same property is used both as an
assumption and as an assertion.
Search WWH ::
Custom Search