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

6.3 Sequence Concatenation

From two sequences r and s , one can build a new sequence r ##1 s by concate-
nating these two sequences: there is a match of sequence r ##1 s if there is a
match of sequence r and there is a match of sequence s starting from the clock tick
immediately following the match of r , as shown in Fig. 6.2 .
In other words, a finite trace matches r ##1 s iff it can be split into two adjacent
fragments, the first one matching r , and the second one matching s . If both operands
of sequence concatenation are bounded sequences, its result is also bounded.

Example 6.5. What is the meaning of a ##1 b , where a and b are Boolean

expressions?

Solution: Let the initial point be clock tick i . Sequence a ##1 b has a match iff a
is true in clock tick i and b is true in clock tick i C 1. Sequence a ##1 b may have
only one tight satisfaction point, in clock tick i C 1. Therefore, this sequence means
that b immediately follows a .
Discussion: Tight satisfaction of sequence a ##1 b depends neither on the value
of b in clock tick i nor on the value of a in clock tick i C 1. Although this looks
obvious, this is a source of confusion for many people who erroneously believe that
for this sequence match b must become true for the first time in clock tick i C 1. t
Example 6.6. Write a sequence capturing the following scenario: request req ,
immediately followed by retry rtry , immediately followed by acknowledgment
ack .
Solution: req ##1 rtry ##1 ack . t

6.3.1 Multiple Delays

We will begin this section with a motivational example.

Example 6.7. Write the following sequence: request req followed by acknowledg-
ment ack in two cycles.
Solution: This description is equivalent to “request, immediately followed by
anything, immediately followed by acknowledgment”. “Anything in a given clock
tick” means a Boolean sequence that has a match in this clock regardless of the
values of req and ack . To match, the corresponding Boolean expression should be
true. Recall (Sect. 5.1 ) that true may be expressed with any nonzero known value, for
example, value 1. So, the desired sequence may be written as req ##1 1 ##1 ack .
t

r s

Fig. 6.2 Sequence

concatenation