Hardware Reference
In-Depth Information
Property (
1
) is a liveness property, as it checks that
clk
ticks at least twice.
Property (
2
) is a safety property even though it has a strong operator. As the global
clock is fair
11
according to its definition, the operators
nexttime
and
s_nexttime
mean the same thing when they are controlled by the global clock.
Property (
3
) is a liveness property as it checks that
b
eventually happens and that
clk
ticks enough times to witness the occurrence of
b
. Property (
4
) is also liveness,
even though it is controlled by the global clock, as it checks that
b
eventually
happens. Property (
5
) is a safety property since it is equivalent to
a
until
b
.
However, it is likely that most FV tools will not recognize it as safety, as it contains
a
s_until
operator, and it looks syntactically like a general liveness property.
t
Most property operators have both weak and strong versions, such as
until
and
s_until
. However, the unbounded operator
always
has only a weak form, and
the unbounded operator
s_eventually
has only a strong form. When we say that
eventually
a
happens, our intent is that
a
happens in some clock tick, and therefore
the clock cannot stop ticking before
a
has been detected. When we say that
a
always
happens, our intent is that
a
happens at each clock tick. If there are no clock ticks,
the value of
a
is not checked. Therefore, in this case there is no requirement that the
clock ticks.
Suffix Implication
Why is suffix implication a weak operator? Suffix implication requires its conse-
quent to be true for each match of its antecedent. There is no requirement that the
antecedent match, and therefore there is no requirement that the clock ticks enough
times to witness a match of the antecedent.
Negation
Negation reverses the strength of an operator.
Example 21.27.
Property
@clk
not weak
(a)
is equivalent to
@clk
strong
(!a)
.
Indeed, according to the clock rewriting rules, explained in Sect.
20.4
,
@clk
not
weak
(a)
is equivalent to
not weak
(@clk a)
. The latter property holds iff property
weak
(@clk a)
fails. This property fails iff either
clk
does not tick at least once or
a
is false at the first clock tick
clk
. This is in its turn equivalent to
@clk
strong
(!a)
.
t
11
I.e., the clock never stops.
Search WWH ::
Custom Search