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

Chapter 6
Basic Sequences
A sequence works in a way a collection never can.
— George Murray
In Chap. 5 , we showed how to build complex properties from the elementary
building blocks. We considered Boolean properties as the simplest building block.
SVA provides sequences as more elaborate building blocks for properties. Since the
simplest sequence is a Boolean expression, we could say that properties are built not
from Boolean expressions, but from sequences.
A sequence is a rule defining a series of values in time. A sequence does
not have a truth value, it has one initial point and zero or more match ,or tight
satisfaction points. Like properties, sequences are clocked. If the clock is not written
explicitly, we assume that the sequence inherits this clock from the property to
which it belongs. Starting from a specific initial point in a trace, a sequence defines
zero or more finite fragments on this trace, each beginning at the initial point and
ending at a tight satisfaction point. We will call the length of a trace fragment defined
by a sequence match simply the length of the sequence match. In the following
sections, we define the sequence match separately for each kind of a sequence.
Before we proceed to the accurate definitions, we informally illustrate the notion
of a sequence on the following example.
Example 6.1. Sequence a ##[1:2] b defines the following scenario: a is followed
by b in one or two clock ticks. Let the initial point of this sequence be clock tick 2.
Then this sequence has a match if a is true in clock tick 2 and either b is true in
clock tick 3 or b is true in clock tick 4. Thus, the following matching outcomes are
possible: