Advanced Sequences - SVA: The Power of Assertions in SystemVerilog - page 248

Table 11.2 Sequence end points

Clock tick 0 1 2 3 4 5 6 7 8 9 10 11 12

1 1 0 1 1 1 0 1 0 0 0 1 0

a

0 0 1 1 0 0 0 1 1 1 0 0 1

b

s.triggrered 0

0 1 1 0 0 0 0 1 1 0 0 1

Note that s.triggered returns the same value as r.triggered , where r is
defined as

sequence r;
@( posedge clk) a ##1 b[ * 1:2];
endsequence :r
Why? t

Example 11.30. Between request req and acknowledgment ack (inclusive), busy
should be asserted. When both req , ack , and busy are Boolean, the desired
assertion is

a1: assert property (req |-> busy until_with ack);
How should we modify this assertion to allow req and ack be arbitrary
sequences? For instance, these sequences could be defined as follows:

sequence req;
start_req ##1 end_req;
endsequence : req
sequence ack;
enable ##[1:10] end_ack;
endsequence
To make the assertion work, in this case we need to assure that busy is asserted
starting from the last clock tick of req until the last clock tick of ack . There is
no need to make any changes in a1 related to req handling, as the overlapping
implication checks the consequent from the last clock tick of its antecedent.
However, ack handling requires a modification because otherwise the assertion
will check that busy is asserted only until the first clock tick of ack . The required
modification is simple: we need to replace ack with ack.triggered :
a2: assert property (req |-> busy until_with ack.triggered);
Now suppose that we wish to take reset rst into account:
a3: assert property ( disable iff (rst)
req |-> busy until_with ack.triggered);
It should be noted that disable iff does not affect the behavior of the
triggered method, and if sequence ack started before req was asserted and before
rst was deactivated, it will not be aborted. However, in this case it would be natural
to ignore ack . The easiest way to do this is to modify sequence ack to take rst into
account as follows: