Advanced Properties - SVA: The Power of Assertions in SystemVerilog - page 230

To define the strong form s_eventually [2:4] p ,use s_nexttime .
3. Let m 0. always [m:m] p is the same as writing nexttime [m] p . Since
the extent where always should hold is only one clock tick, always [m:m] is
the same as eventually [m:m] p as well. The strong forms are defined using
s_nexttime .
4. Let n > m . always [m:n] p is the same as always [m:n-1] p and nexttime
[n] p . The expansion is similar to the expansion of ( eventually [m:n] p) ,but
the series of nexttime properties is formed using conjunctions. For example,
always [2:4] p is equivalent to nexttime [2] p and nexttime [3] p and
nexttime [4] p . The strong form is again defined using s_nexttime .
5. Let m 0. always [m:$] p is equivalent to nexttime [m] always p .Thelower
bound m just shifts the check for property p to hold forever after m clock ticks.
There is no strong form in this case due to the open-ended upper bound, which
requires always p .
6. Let m 0. s_eventually [m:$] p is equivalent to s_nexttime [m] s_event-
ually p . As in the preceding case, the check for the property p to eventually
hold is just shifted by m clock ticks. As a dual property to always [m:$] p ,
there is no weak form.
Like the unbounded case, the form s_eventually [m:n] p can also be defined
using duality with always as not always [m:n] not p . The strong eventuality
requires that p is true within m to n clock ticks and that there are enough clock
ticks to cover this range. In the formulation using always , always [m:n] not p
will succeed when p fails at each clock tick in the range (there need not be
enough clock ticks to cover the range). Again, due to the top-level negation
in not always [m:n] not p , that property will succeed provided p is true at
some clock tick in the range. It is thus equivalent to the strong eventuality
( s_eventually [m:n] p) .
Similarly, we can see that ( s_always [m:n] p) is equivalent to ( not eventu-
ally[m:n] not p) . Again, the negation of a weak property becomes a strong
property and vice versa.
One may ask the question why there is the weak eventually [m:n] p with a
fixed range, while the open-ended range is only strong s_eventually [m:$] p .
It works out that if the latter were weak, the property would be in some sense
meaningless because in an assertion it cannot ever fail. If there are not enough clock
ticks before p is true, then the weak form succeeds. Only the strong form can declare
failure in that case. This distinction between open and bounded ranges carries over
by duality to the always operator. Namely,
not eventually [m:n] not p s_always [m:n] p
not s_eventually [m:$] not p always [m:$] p .
In the final section of this chapter, we explain how vacuous successes of a property
are determined depending on the type of the operator.