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

1 module m( input logic clk, a, b, ...);
2 logic c;
3 sequence ab;
4 @( posedge clk) a ##1 b;
5 endsequence
6 always @( posedge clk) begin
7 c <= ab.triggered;
8 //...;
9 end
10 //...
11 endmodule :m

Fig. 11.13 triggered method in procedural code

clear whether these changes in value cause events to trigger the assign statement
evaluations.
If the intent of the assignment statement is to provide a name for the expression
s.triggered || b to be reused in other contexts, for example, in concurrent
assertions, then a better solution is to use let which does not perform any
assignment, but only associates a name with an expression:
let a = s.triggered || b;
Then assertion a1 is internally expanded into
a1: assert property (@( posedge clk) s.triggered || b);
which yields the desired result.
Using the triggered method in procedural code in modules or interfaces is often
meaningless, as shown in the following example.

Example 11.31. In the code in Fig. 11.13 , the value assigned to c in Line 7 is always
0 because the value of ab.triggered is evaluated in the Observed region, while the
nonblocking assignment is evaluated in the NBA region, before the ab.triggered
has been evaluated. Since the sequence match event is not in the sensitivity list of
the event control in Line 6 , there will be no reevaluation of the always procedure in
the same clock tick.

t

triggered method may be safely used in procedural code in programs and
checkers because the procedures are executed after the Observed region. The value
of triggered has the correct value at that moment.

Do not use the triggered sequence method in procedural code in modules
and interfaces outside concurrent assertions. triggered method may be
safely used in procedural code in programs and checkers.
Using the triggered sequence method in let definition with subsequent
let instantiation in concurrent assertions is safe.