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

Table 10.2 Comparison of suffix implication and followed-by

Operator Antecedent match Antecedent no match

|-> |=> Each must yield consequent true

Vacuous success

#-# #=# At least one must yield consequent true

Failure

Suffix Implication

The suffix implications have been discussed in Chap. 6 . We summarize them here
because we need them to describe the followed-by operators.
A suffix implication operator takes a sequence as the left-hand operand and a
property as the right-hand operand: s |-> p and s |=> p . Whenever s matches,
property p must hold. When s has no match then a suffix implication is vacuously
true.
The difference between the two forms is that in the case of |-> the evaluation of
property p starts at the clock tick that occurs at or after the tick when s matches.
In the case of |=> the evaluation of p starts at the clock tick that occurs strictly
after the clock tick when s matches. When the ending clock of s (meaning the
clock of the latest evaluated expression of s ) is the same as the leading clock of
p , then in the case of s |-> p property p starts at the same clock tick when s
matches, while in the case of s |=> p , property p starts at the clock tick following
the match of s .Thisiswhy |-> is called an overlapping suffix implication, and |=>
is a nonoverlapping one.

Suffix Conjunction (Followed-By)

The followed-by operators #-# and #=# also have a sequence as the left-hand
operand and a property as the right-hand operand: s #-# p and s #=# p .If s
has no match, then followed-by evaluates to false. If s has one or more matches
for a given evaluation attempt, then for the property to evaluate to true, at least
one match of s must result in p evaluating to true (see Table 10.2 ). In this sense,
the behavior is similar to sequence concatenation with ##0 and ##1 cycle delays.
The difference is that sequence concatenation requires a sequence as the right-hand
side operand, while followed-by accepts a property there. This is also the reason
that followed-by is sometimes called a suffix conjunction or suffix concatenation .If
property p is in fact a strong sequential property (e.g., if s1 #-# s2 appears in a
cover), then s1 #-# strong (s2) is the same as strong (s1 ##0 s2) . Similarly,
s1 #=# strong (s2) is the same as strong (s1 ##1 s2) . As to when p starts its
evaluation relative to the match of s , the difference between #-# and #=# is the same
as between the two forms of the suffix implication. The former is overlapping and
the latter is nonoverlapping.