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

Sequence Disjunction versus Property Disjunction. Sequence disjunction and
property disjunction have exactly the same syntax. The following rule shows how
they are distinguished: if both r and s are sequences then r or s is a sequence
disjunction, otherwise, it is a property disjunction. For example, the formula
(a ##1 b) or ##1 c is a sequence disjunction, and (a ##1 b) or nexttime c is
a property disjunction. In the context where both sequences and properties may
appear, the exact decision is not important since in this case both definitions yield
equivalent results. Why?

Example 6.30. There are two types of transactions: the read transaction, in which
read request read is followed by data_ready in three cycles, and the write
transaction, in which write request write is followed by done . Write a sequence
representing a generic transaction.

Solution: The sequence representing the read transaction is read ##3 data_ready ;
the sequence representing the write transaction is write ##1 done . The generic
transaction is their disjunction, read ##3 data_ready or write ##1 done . t
Multiple Matches. All sequences we considered until now could have at most one
match. Sequence disjunction introduces sequences that can have multiple matches.

Example 6.31. Sequence a[ * 2] or b[ * 3] may have 0, 1, or 2 matches. t

6.7 Consecutive Repetition Revisited

In Sect. 6.5 , we introduced consecutive repetition with factors n 0.Therulesof
building consecutive repetition may be summarized as follows:

￿ s[ * 0] is an empty sequence.
￿ s[ * n] , where n >0is defined recursively:

s[ * n] s[ * n-1] ##1 s .

In this section, we will define repetition ranges.

6.7.1 Repetition Range

Instead of a fixed number of repetitions one can specify a repetition range: finite
s[ * m:n] and infinite s[ * n:$] . m and n should be elaboration time integral constants,
m n , and $ stands for an “infinite number”.