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