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

6.7.1.1 Finite Repetition Range

Consider an example of a finite repetition range first. What is the meaning
of sequence s[ * 2:4] ? Intuitively, it means that sequence s is repeated from
2to4 imes.Moreforma ly, s[ * 2:4] has a match iff either s[ * 2] has a
match, or s[ * 3] ,or s[ * 4] has a match. That is, s[ * 2:4] is equivalent to
s[ * 2] or s[ * 3] or s[ * 4] . This leads us to the following recursive definition:
s[ * n:n] s[ * n] .
s[ * m:n] s[ * m:n-1] or s[ * n] , m < n .

Efficiency Tip. Big repetition factors, and ranges with big finite upper bounds, are
inefficient both in simulation and in formal verification.

6.7.1.2 Infinite Repetition Range

Consider now an example of an infinite repetition range: intuitively s[ * 1:$] means
that s happens one or more times. Following the definition of finite repetition range
we would like to define s[ * 1:$] as s or s[ * 2] or s[ * 3] ....Unfortunately, such
a definition does not work as it produces an infinite formula. Therefore, we need to
define s[ * 1:$] directly.
Let the initial point of sequence s[ * 1:$] be clock tick i . Sequence s[ * 1:$]
has a tight satisfaction point (match) j i iff there is some number n >0such
that j is the tight satisfaction point of sequence s[ * n] . In other words, sequence
s[ * 1:$] is tightly satisfied on trace fragment i W j if it is possible to divide this
trace fragment into one or more consecutive fragments so that each such fragment
tightly satisfies s .
After we have defined infinite repetition range [ * 1:$] we can define any infinite
repetition range as follows:

s[ * 0:$] s[ * 0] or s[ * 1:$] .
s[ * n:$] s[ * n-1] ##1 s[ * 1:$] , n >1.

s[ * n:$] does not mean that sequence s is repeated infinitely many times, but
that it is repeated n or more (finite) number of times.

There are shortcuts s[ * ] provided for s[ * 0:$] (zero or more times), and s[+] for
s[ * 1:$] (one or more times) that we will widely use.
Example 6.32. Describe a transaction as a sequence. A transaction starts with
Beginning Of Transaction signal ( bot ) and ends with End Of Transaction signal
( eot ). Each transaction is at least two cycles long, and transactions cannot overlap.