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

Example 11.26. The following code is legal:

logic a, b, c, d;
// ...
sequence s;
@( posedge clk) a ##[1:3] b;
endsequence :s
sequence t(x);
@( posedge clk) x[ * 5];
endsequence :t
property p( sequence r, untyped y);
a |-> r(y).triggered;
endproperty :p
a1: assert property (@( posedge clk) c |-> s.triggered);
a2: assert property (@( posedge clk) c |-> t(d).triggered);
a3: assert property (@( posedge clk)p(t,d));
s and t(d) are instances of the named sequences. In r(y) , r is a formal argument
and so is y .

t

Example 11.27. The following code is illegal:
logic a, b, c;
// ...
a1_illegal: assert property (@( posedge clk)
c |-> (a ##[1:3] b).triggered);
triggered method is applied to sequence expression a ##[1:3] b which is
neither a named sequence instance nor a formal argument. t

Example 11.28. Consider the following code:

logic a, b, c, d;
sequence s1;
@( posedge clk) a ##1 b;
endsequence :s1
sequence s2;
@( posedge clk1) a ##1 b;
endsequence :s2
sequence s3;
@( posedge clk1) a ##1 @( posedge clk1) b ##1 @( posedge clk) c;
endsequence :s3
a1: assert property (@( posedge clk) d |-> s1.triggered);
a2: assert property (@( posedge clk) d |-> s2.triggered);
a3: assert property (@( posedge clk) d |-> s3.triggered);
The clock for the sequences is governed by the clock flow rules described
in Sect. 12.2.4.1 . Each sequence has its clock explicitly specified, so the clock from
the assertion where they are used does not flow in to the sequence. t

Example 11.29. Table 11.2 contains a trace of a and b , and the values of

s.triggered , where s is defined as
sequence s;
@( posedge clk) a[ * 1:2] ##1 b[ * 1:2];
endsequence :s