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

Until

There are only the unbounded forms of these operators:

￿ Unbounded weak: p1 until p2
￿ Unbounded strong: p1 s_until p2
The operator comes in two forms, weak until and strong s_until . The formal
semantics is covered in Chap. 22 .
The weak until property holds true provided that either p2 is true at the first
clock tick or p1 holds true at all clock ticks as long as p2 is false. If there is no clock
tick at which p2 is ever true, the property evaluates true. The strong form s_until
is similar except when there is no clock tick at which p2 holds true—the strong form
is false in that case.

Example 10.10. Suppose that condition c must hold true between the occurrences
of conditions e1 and e2 but not necessarily including these clock ticks.
a1: assert property (e1 |=> c until e2);
a2: assert property (e1 |=> c s_until e2);

Discussion: Assertion a1 will succeed even if there are not enough clock ticks for
detecting e2 true (provided that c holds till then), while a2 will declare failure in
that situation due to the use of a strong until operator.

t

Always and S_eventually

The following are the unbounded forms of these operators:

￿ Unbounded weak: always p
￿ Unbounded strong: s_eventually p
Property always p is true if p holds true at every clock tick. The operator always
is weak , hence when there are no more clock ticks, the property evaluates to true. It
is equivalent to p until 1'b0 . Recall that 1'b0 is Boolean false in SystemVerilog.
Property s_eventually p is true if there is a sufficient number of clock ticks to
find one at which p is true.
What if we negate an always property as not always p ? According to the
definition this property is true iff always p is false, which means that p is false
at least at one clock tick. This is exactly the property s_eventually not p .Itis
a strong eventuality because there must be a clock tick where p is false (otherwise
always p would be true).
It follows that s_eventually p is equivalent to not always not p . And also
s_eventually p is equivalent to 1'b1 s_until p .
Notice how the negation changes the strength of the resulting property. Negating
a weak always we obtain a strong s_eventually . This is because to falsify