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

always we require that the operand property p be false somewhere in the future. It
must happen, hence the eventuality is strong. always and s_eventually are dual
properties.
In

case of a Boolean property e , not always e may be rewritten as

s_eventually !e .

Until_with

There are only the unbounded forms of these operators:

￿ Unbounded weak: p1 until_with p2
￿ Unbounded strong: p1 s_until_with p2
The weak until_with property holds true provided that either p1 and p2 is
true at the first clock tick or p1 holds true at all clock ticks until a clock tick when
both p1 and p2 hold true. If there is no clock tick at which p1 and p2 is true,
the weak property evaluates true. The strong form s_until_with is similar except
when there is no clock tick at which p1 and p2 holds true—the strong form is false
in that case.
As in the case of the dual operators always and s_eventually , until and
s_until_with are dual operators, as are s_until and until_with . The following
equivalences hold:

p s_until q not (( not q) until_with ( not p))
p until q not (( not q) s_until_with ( not p))

Example 10.11. Write an assertion that verifies the following situation: When
Boolean trig is true, property p2 must hold at some clock tick strictly before a
clock tick at which property p1 holds.
Solution:

a1: assert property (
if (trig) ( not p1) until_with p2);
The specification is missing one important point, namely, must p2 ever occur? If
not, then the above assertion is correct. If yes, then we should require p2 to be true
at some clock tick by using the strong form

a2: assert property (
if (trig) ( not p1) s_until_with p2);

t

Example 10.12. When req becomes true it must hold until and including gnt .In
addition, gnt must happen.
Solution:
a1: assert property (
!req ##1 req |-> req s_until_with gnt);