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

For singly clocked properties nexttime [0] p means “either the clock does not
tick anymore, or p ”, and s_nexttime [0] p means “the clock ticks at least once,
and p ”.
For example,

initial a: assert property (
nexttime [0] s_eventually e);
means that either the clock does not tick at all, or e holds in some finite number
of clock ticks. However,

initial a: assert property (
s_nexttime [0] always e);
means that the clock ticks at least once and e happens at each clock tick.
When m >0the weak form can be defined recursively. This results in a repetitive
application m times of nexttime on p :
nexttime nexttime ... nexttime nexttime p
As mentioned above, the strong form is defined by double negation: Therefore,
for m==1 , nexttime not p says that p does not hold at the next clock tick and
it is a weak form. By negating it, a strong property is obtained saying that “it is not
true that p does not hold at the next clock tick”. That is, it must hold and there must
be at least one clock tick.

Example 10.13. When initial reset rst is deasserted, property p must eventually
hold after 2 clock ticks, and there must be enough clock ticks:

Solution:

initial a: assert property (
rst ##1 !rst |-> s_nexttime [2] s_eventually p);

t

Efficiency Tip. In general, it is recommended to use s_nexttime with strong
operators, and nexttime with weak ones. For instance, nexttime always p
and s_nexttime s_eventually p . It is important to note that p is a property.
This situation is common and important for assertion libraries, where there are
restrictions on the argument type.

Example 10.14. There cannot be two consecutive requests where req is a Boolean
expression. One could be tempted to write the following assertion:

a1: assert property (req and nexttime !req);
but this is wrong. Assertion a1 is contradictory: req and nexttime !req must
be true at every clock tick, i.e., req must be true at each clock tick and !req must
be true starting from the second clock tick. Already at the second clock tick it thus
requires that both req and !req are true!
To write this assertion correctly, we can formulate it as “if there is a request, there
should be no request at the next clock tick”:

a2: assert property (req implies nexttime !req);