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

Example 6.3. Sequence a ##[1:2] b informally described in Example 6.1 is

bounded.

Solution: This sequence can only have matches of length 2 or 3, and its match upper
bound L D 3: if this sequence does not have a match on a trace fragment of three
clock cycles, it does not have matches at all. t

The definition of sequential properties for bounded sequences may be simplified:

The sequential property corresponding to bounded sequence s is true iff
sequence s has at least one nonempty match.

So, what is the nature of unbounded sequences? They should admit arbitrarily
long matches. Examples of unbounded sequences are provided in Sect. 6.10 .
Another point to be clarified is the notion of empty match . The match is empty
if the trace fragment it defines is empty. We will provide examples of empty match
in Sects. 6.5.1 and 6.8 . Note that a Boolean sequence cannot have an empty match.
It either has a match of size 1 if its Boolean expression is true, or it does not have
matches at all.
Pay attention to the clock tick where the truth value of a sequential property is
defined.

The truth value of sequential property s corresponds to the initial point of
sequence s , and not to the point of its tight satisfaction.

Example 6.4. Let a be true in clock tick 2, and false in all other clock ticks, and b
be true in clock tick 3, and false in all other clock ticks. Then sequential property
a ##[1:2] b is true in clock tick 2 (not 3!), and false in all other clock ticks.

t

Let us apply the definition of a sequential property to a Boolean sequence.
Since Boolean sequences are bounded, Boolean sequential property e is true iff
Boolean sequence e has a match, that is, when e is true. We come to the conclusion
that Boolean sequential properties are exactly Boolean properties we described in
Sect. 5.1 . Therefore, sequential properties generalize Boolean properties, and it is
possible to define all property operators from Chap. 5 independently of the general
sequential properties, as we mentioned in the introduction to that chapter.