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

Table 6.3 Initial trace
fragment in Example 6.34

Clock tick a b c
0 1 0 0

1 1 1 0

2 0 0 1

Solution: Since the transaction is at least two cycles long, bot and eot of the same
transaction cannot be asserted in the same clock cycle. The fact that transactions
cannot overlap means that between bot and the next eot there are no other
occurrences of bot . We allow bot of the next transaction to occur in the same
clock cycle with eot of the previous transactions. Transactions should also be well
formed; therefore no two eot should occur without a bot occurrence between them.
Therefore, the sequence describing the transaction is

t

bot ##1 (!bot && !eot)[ * ] ##1 eot .

Example 6.33. Write the following assertion: rdy becomes asserted the first time
when the reset sequence is over. The reset sequence is represented by the high value
of rst .
Solution:

initial a1: assert property (@( posedge clk)
rst && !rdy [ * ] ##1 !rst && rdy);

Discussion: The same assertion may be more intuitively rewritten using property
operator until :
initial a2: assert property (@( posedge clk)
rst && !rdy until !rst && rdy);

t

Example 6.34. We revisit Example 5.21 : ready should be low until rst becomes
inactive for the first time.

Solution: This time we are going to implement this assertion using sequences:

initial assert property (@( posedge clk) !ready[ * ] ##1 !rst);

Discussion: In this case, the property operator until may be implemented as a
sequential property (see also Example 6.33 ). If a is a Boolean and s is a sequence,
a until s is equivalent to sequential property a[ * ] ##1 s in the assertion or
assumption context. However, for a general sequence r , r until s and the
sequential property r[ * ] ##1 s are not equivalent . To understand this, compare
(a ##1 b)[ * ] ##1 c and a ##1 b until c for values of a , b , and c shown in
Table 6.3 . Sequence (a ##1 b)[ * ] has a match in clock tick 1, therefore sequence
(a ##1 b)[ * ] ##1 c has a match in clock tick 2, and the corresponding sequential