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

10.1 Sequential Property

In addition to the property operators listed in Table 10.1 , sequences are promoted
to properties when used in a property context. We call them sequential properties,
or sequence properties (see also Sect. 6.2 ). This happens when a sequence is used
as the only expression in an assertion or as an operand to a property operator that
requires the operand to be a property. Sequential properties can be weak or strong .
A sequence becomes a strong property when it is the argument to a strong (...)
qualifier, e.g., strong (a ##1 b) . A strong sequential property holds if and only if
the underlying sequence has a match. Without this strong qualifier, a sequential
property is weak (see Sect. 6.2 , the definition given there corresponds to the week
sequential property) in the assertion or assumption context, and strong in the cover
context. As we shall see, in situations where a sequence is strong by default, it can
be made weak by using the qualifier weak (...) . The distinction between strong and
weak sequential properties is reflected in their truth value when there are not enough
clock ticks to complete the evaluation of the sequence: If there are not enough clock
ticks the weak sequence property succeeds, while the strong one fails.

Example 10.1. Consider the following assertions:

initial a1: assert property (a ##[+] b);
initial a2: assert property ( strong (a ##[+] b));

a3: assert property (!a ##1 a |-> b[ * ] ##1 c);
a4: assert property (!a ##1 a |-> strong (b[ * ] ##1 c));

c1: cover property (a ##[+] b);
c2: cover property ( weak (a ##[+] b));

Table 10.1 Property

Operator Associativity
not -
nexttime , s_nexttime -
and Left
or Left
iff Right
until , s_until Right
until_with , s_until_with Right
implies Right
|-> , |=> Right
#-# , #=# Right
always , s_always -
eventually , s_eventually -
if else , case -
accept_on , sync_accept_on -
reject_on , sync_reject_on -

operators