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

A followed-by operator is a dual operator of suffix implication. The following
equivalences hold:
s #-# p not (s |-> not p) , and s #=# p not (s |=> not p)
This means that even without the availability of the followed-by operators,
the same behaviors could be obtained using the right-hand sides of the above
equivalences. The intent is, however, more clearly conveyed by the shorter notation
when a followed-by operator is used.
The question is where the use of followed-by is appropriate. Its principal usage
is in cover property statements when the right-hand side argument cannot be
restricted to a sequence. This often occurs in properties that are used in checker
libraries, where the arguments of the checker are not restricted to be Boolean
expressions or sequences only.

Example 10.8. Consider the coverage property: When a “pattern” x is detected it is
followed by a “pattern” y . We may have to restrict x to be a sequence, but y could
be nonrestricted and be any property.
property p( sequence x, untyped y);
x #-# y;
endproperty
Its usage could be
cov: cover property (p((req[ * 2]), ( s_eventually ack)));

t

Example 10.9. Ascertain that a reset condition is true for some m initial clock ticks
and then it remains false forever. Such a property is often used as an assumption on
reset in formal verification.

Solution:
initial a: assume property (reset[ * m] #=# always !reset);

t

We now examine the temporal operators inspired by Linear Temporal Logic.

10.4 Unbounded Linear Temporal Operators

Linear temporal logic (LTL) is a modal temporal logic with modalities referring
to time, which in SVA means as measured by the occurrence of clock ticks. In
LTL, it is possible to write formulae about the future of behaviors following a linear
progression of time, such as that a property will eventually be true, that a property
will be true until another property becomes true, and so on. The operators can be
bounded with some specific ranges or unbounded. The following are linear temporal
unbounded property operators available in SVA:
￿ Weak until and until_with ,

and their strong forms s_until and

s_until_with .
￿ Unbounded weak always .
￿ Unbounded strong s_eventually .