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

Fig. 6.9 r[ * 2]

r r

clock ticks

Example 6.29. Signal sig remains high during five cycles.

Solution:

a1: assert property (@( posedge clk) !sig ##1 sig |=> sig[ * 4]);

Discussion: This assertion states that once the signal goes high it remains high
during four additional clock ticks. It does not forbid the signal to stay high for
longer time. See Exercise 6.6 for an alternative interpretation.

t

6.5.1 Zero Repetition

It is possible to define zero repetition of sequences: sequence s[ * 0] is a sequence
admitting only an empty match. In other words, sequence s[ * 0] matches on any
trace, but the trace fragment it defines is empty—it does not contain any clock tick.
Because of this characteristic of zero repetition, it is also called empty sequence .
Empty sequence is a strange creature, its behavior significantly differs from the
behavior of “normal” sequences. It is rarely written explicitly, but its implicit use in
delay and repetition ranges is rather common, therefore it is extremely important to
understand its behavior. The meaning of empty sequence concatenation and fusion
is not obvious, and it is clarified below.
The empty sequence cannot be promoted to a sequential property, as the
definition of sequential property in Sect. 6.2 excludes sequences admitting an empty
match. Thus, assertion assert property (@( posedge clk)s[ * 0]); is illegal .

6.5.1.1 Concatenation with Empty Sequence

In this section, we will clarify the meaning of sequence r[ * 0] ##1 s .Letthe
initial point of the resulting sequence be clock tick i . According to the definition of
sequence concatenation (Sect. 6.3 ), r[ * 0] ##1 s has a match in clock tick j i iff
the interval i W j may be split into two consecutive parts, the interval where sequence
r[ * 0] has a match and the interval where sequence s has a match. Since r[ * 0]
matches an empty trace fragment, the match of sequence r[ * 0] ##1 s coincides
with the match of sequence s . In other words, r[ * 0] ##1 s is equivalent to s .
Similarly, r ##1 s[ * 0] is equivalent to r .
Concatenation with an empty sequence clarifies the semantics of sequence
concatenation operator ##1 .