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

Fig. 6.4 Sequence fusion

s

r

clock ticks

Solution: Since this assertion is continuously monitored (has an implicit outermost
always operator), sequential property a ##1 b must be true in each clock tick.
Hence, a must be true in each clock tick, and b must be true starting form clock
tick 1.

Discussion: This assertion does not mean interleaving of a and b . t

Example 6.11. We want to state that the value of sig toggles every cycle: 0101...or
1010.... The following assertion

a1: assert property (@( posedge clk) sig ##1 !sig);
does not check this condition. Similar to Example 6.10 , it means that sig is true in
each clock tick, and also that sig is false starting from clock tick 1. Therefore,
this assertion is contradictory: it requires that starting from clock tick 1 sig
be simultaneously true and false. Example 7.26 explains how to implement this
assertion correctly. t

6.3.3 Sequence Fusion

Sequence fusion is an overlapping concatenation. The fusion of sequences r and s ,
denoted as r ##0 s , is matched iff for some match of sequence r there is a match of
sequence s starting from the clock tick where the match of r happened (see Fig. 6.4 ).
Note the difference between sequence concatenation r ##1 s and sequence fusion.
For sequence concatenation, we start matching sequence s from the next clock tick
after a match of r has happened, while for sequence fusion we start matching s from
the same clock tick of the match of r .
Example 6.12. What is the meaning of fusion of two Boolean sequences a and b ?
Solution: a ##0 b can have a match iff both a and b are true simultaneously.
Therefore, a ##0 b is semantically equivalent to a&&b . Note, however, that
a ##0 b and a&&b are not syntactically interchangeable. a ##0 b is a sequence,
so it cannot be used as an operand in a Boolean expression. For example,
a&&b||c (where c is a Boolean expression) is legal, whereas (a ##0 b) || c
is syntactically illegal. 3 t

Example 6.13. What is the meaning of (a ##1 b) ##0 (c ##1 d) , where a , b ,
c , and d are Boolean expressions?

3 Also && is not the same as ##0 when match items are attached to the first sequence, see Chap. 16 .