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

Discussion: If a new request can start immediately at the clock tick following gnt ,
the assertion would have to be modified as follows because there is no rising edge
on req in that situation.
a2: assert property (
(!req || gnt) ##1 req |-> req s_until_with gnt);
The sequence in the antecedent matches when either !req ##1 req happens
(i.e., rising transition of req )or gnt ##1 req happens which is the case of a
continuing request. Note that another assertion should verify that gnt does not occur
without a req .
How should we modify the assertions if it is not required that gnt ever happens
after asserting req ? The answer is similar to the preceding example, Example 10.11 ,
namely, replace the strong form s_until_with by the weak one until_with .
Then, even if gnt never happens after being requested the property will evaluate
true. t

10.5 Bounded Linear Temporal Operators

Bounded operators are useful when the property to be verified must be satisfied
within some specified range of clock ticks. There is the fixed delay property
operator nexttime , which is similar to ##m in sequences. The operators always
and eventually are provided with ranges in both strong and weak forms.
The behavior of the bounded operators is as follows.

Nexttime

￿ nexttime p
￿ s_nexttime p
￿ nexttime [m] p
￿ s_nexttime [m] p

The semantics are split according to the value of argument m , which must be an
elaboration constant, and according to the strength of the operator:

1. Weak form: nexttime p is true at tick t if p is true at tick t C 1 or if there is no
tick t C 1 or if there are no clock ticks at all. nexttime [0] p has no delay, p has
to be true at tick t or there is no tick t . In that sense it is equivalent to 1 |-> p .
Property nexttime [m] p for some m >0is true if p is true at tick t C m or if
there are not enough ticks.
2. Strong form: s_nexttime [m] p , m >0is similar to the weak form except that
it does require having a sufficient number of clock ticks, i.e., at least m .Itisthus
equivalent to not nexttime [m] not p .