Basic Sequences - SVA: The Power of Assertions in SystemVerilog - page 120

r ##1 s does not mean “skip one clock tick after match of r and then match
s ”, but “start matching s after match of r ”.

6.5.1.2 Fusion with Empty Sequence

In this section, we will clarify the meaning of sequence r[ * 0] ##0 s . According to
the definition of sequence fusion (Sect. 6.3.3 ), the match of sequence r[ * 0] ##0 s
requires the clock tick of the match of r[ * 0] be the first clock tick of sequence s .
Since r[ * 0] does not match any positive number of clock ticks, a match of sequence
r[ * 0] ##0 s is impossible. Similarly, sequence r ##0 s[ * 0] cannot be matched,
either. Therefore, a fusion with an empty sequence does not have a match.
This result reveals a very important fact:

Sequence fusion never admits an empty match.

6.5.1.3 Empty Sequence in Antecedent

What happens when the antecedent of a suffix implication is an empty sequence?
In case of the overlapping implication s[ * 0] |-> p , its antecedent does not have
nonempty matches, and according to the definition of the overlapping implication,
s[ * 0] |-> p trivially holds (is a tautology).
The situation with the nonoverlapping implication is completely different.
According to its definition, s[ * 0] |=> p is equivalent to s[ * 0] ##1 1 |-> p ,
which is, in its turn, equivalent to 1 |-> p (see Sect. 6.5.1.1 ). The latter is
equivalent to p .
Although it is rarely used in its pure form, this seemingly pathological behavior
of the empty sequence in antecedents is important to understand the semantics of
more complex antecedents admitting empty matches, described in Sect. 6.8.1 .

6.6 Sequence Disjunction

Sequence disjunction r or s is a sequence which has a match whenever either r or
s (or both) have a match.
Boolean Disjunction. For Boolean expressions a and b sequence a or b has
a match iff a||b is true. Therefore, in case of Boolean values, a sequence
disjunction behaves as a logical disjunction.