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

11.2.2 The triggered Method in Checkers

In Sect. 11.2.1.2 we stated that using triggered sequence method on the right-
hand side of a nonblocking assignment in modules is meaningless because the
nonblocking assignment is performed in the NBA region, while the triggered
method is evaluated only later in the Observed region.
This is not true for checkers: the triggered sequence method may be safely
used in checker variable assignments, because checker variables are assigned in the
Re-NBA queue of the Reactive region, after the evaluation of triggered .

It is safe to use the triggered sequence method in checker variable
assignments.

Example 11.32. Disable checking assertions in a checker between the match points
of sequences stop_check and start_check .
Solution:

checker toggle_check( sequence stop_check, start_check,
event clk = $inferred_clock);
bit rst = 1;
default clocking @clk; endclocking
default disable iff rst;

always @clk begin
if (stop_check.triggered) rst <= 1'b1;
else if (start_check.triggered) rst <= 1'b0;
end

a1: assert property (...);
// More assertions here ...
endchecker : toggle_check

Discussion: We defined a checker variable rst which is 1 between the match point
of sequence stop_check until the match point of sequence start_check .For
example, if the stop sequence consists of two consecutive stop signals, and the
start sequence consists of two consecutive start signals, then the actual checker
arguments would be stop[ * 2] and start[ * 2] .

t

11.2.3 Matched

The method matched returns the status of sequence termination but in the strictly
subsequent clock tick. Therefore, in the case of single clock, s.matched is
equivalent to s1.triggered , where s1 is defined as follows: