Using sequence method triggered within Sampled value functions

LRM 16.9.3 Sampled value functions says

Local variables (see 16.10) and the sequence method matched are not allowed in the argument expressions passed to these functions.

Since it doesn’t mention sequence method ‘triggered’ I tried using ::

  sequence seq;
    $rose(a) ##1 b ;   
  endsequence  
  
  property p2;
    $rose(seq.triggered)[->1];
  endproperty
  
  property p1;
    seq.triggered[->1] ;
  endproperty

  ap1:assert property(p1) $display("ap1 passes at %0t",$time);
                    else  $display("ap1 fails at %0t",$time);
    
  ap2:assert property(p2) $display("ap2 passes at %0t",$time);
                    else  $display("ap2 fails at %0t",$time);

However I observe compilation error ::

Error-[SVA-SMNASVF] Sequence method in sampled function
testbench.sv, 37
sva, “$rose(seq.triggered)”
Sequence methods cannot be used as arguments to sampled value functions,
e.g., $past, $fell, $rose, $stable, $changed.
Please remove the use of sequence methods from this context.

Quick answers from my SVA book:
Because triggered it is set in the Observed region, after the Active and NBA region. The endpoint status of of .triggered is set in the Observed region. It persists until the end of the timestep.

Also, you should not use it in an always_ff with an if statement because it will not be seen. For example:
always_ff @(posedge clk) if(seq.triggered) a <= b; // BAD USE
• Triggered may be used in wait statements
• 1800 seem to imply that .triggered cannot be used with the “@” construct, like @(seq.triggered).
Tools do not agree in the compilation of the triggered with the “@”. Many experts believe that this is illegal.
Avoid using such construct. Use the wait instead.

The matched status of the sequence is set in the Observed region and persists
until the Observed region following the arrival of the first clock tick of the destination sequence after the match.
Related links:

Sequence Methods :: ended V/S matched - SystemVerilog - Verification Academy

Link to the list of papers and books that I wrote, many are now donated.

Yes I do understand this part.

Property p1 is true in the observed region on the clock when ‘seq’ ends ,
so shouldn’t $rose( seq.triggered ) work on the same principle ?
i.e in the observed region that ‘seq’ ends $rose(seq.triggered) would be true

But isn’t the issue the sampling?

function f(bit xa); ... endfunction
  f(sig) |-> b; 
the value evaluated by f is ihe sampled value of sig.
Same thing for $rose(seq.triggered). 
the dampled value of seq.triggered is?  Zero? 
I think it would be 0.

Thanks Ben.

As per LRM 16.9.3 Sampled value functions ::

The following functions are called value change functions and are provided to detect changes in sampled
values: $rose, $fell, $stable, and $changed.
A value change function detects a change (or, in the case of $stable, lack of change) in the sampled value
of an expression. The change (or lack of change) is determined by comparing the sampled value of the expression with the sampled value of the expression from the most recent strictly prior time step in which
the clocking event occurred

$rose returns true if the LSB of the sampled value ( preponed value returned by $sampled() ) changed from 0 (in previous clk event) to 1 (in current clk event)

$rose returns true / false based on sampled value i.e value returned by $sampled which is same as pre-poned value, whereas the following operate in Observed region ::

(1) Local variables are assigned in Observed region
(2) seq.triggered returns true in Observed region if the endpoint of the sequence is detected and it remains true for rest of the time step
(3) seq.matched remains true from observed region of source clock till observed region of the destination clock

Also regarding the following ::

1800 seem to imply that .triggered cannot be used with the “@” construct, like @(seq.triggered).
Tools do not agree in the compilation of the triggered with the “@”. Many experts believe that this is illegal.
Avoid using such construct. Use the wait instead.

Instead of @( seq.triggered ) wouldn’t a better approach be @(seq) ?
Since seq.triggered returns boolean value 1’b0/1’b1 and not an event,
I believe it can’t be used as event control i.e @(seq.triggered)

It shall be considered an error to invoke the .triggered method in an @(expression_construct)
or in an if(expression construct). The following examples are illegal:

sequence q1; a[*2] ##1 b; endsequence  
always @(q1.triggered) … // Illegal 
// @(s.triggered) does not make sense because it would have 
// to create two events one when it is set in the Observed region 
// and the other when it is reset in the end of the timestep.
 always @(posedge clk)  if(q1.triggered) … //  illegal  
 // The (s.triggered)would not be seen in the Active region because it is set in the Observed region.  

 /* The triggered method can be used as level-sensitive controls of properties and procedural 
  code as a result of sequence terminations.  Examples of actions taken as a result of termination 
  of sequences include: 
   1. Execution of procedural code delayed until termination of a sequence. 
     This is accomplished using the level-sensitive wait statement in conjunction with the triggered method. 
   2. Disabling a property based on termination of a sequence.   
      The triggered method can be used as a level-sensitive event in a wait statement 
      or in the disable iff component of a property.

Sequence as events  
  Rule: [1] A sequence instance can be used in event expressions to control 
  the execution of procedural statements based on the successful match of the sequence. 
  This allows the successful end point of a named sequence to trigger multiple actions in other processes.  
  When a sequence instance is specified in an event expression, the process executing the event control 
  is blocked until the specified sequence successfully reaches its end-point.   
  A process resumes execution following the Observe region in which the end point is detected. For example: */
     sequence qDoneSetup; @ (posedge clk)   first_match($rose(load_mem) ##[0:5] done);  endsequence : qDoneSetup 
     always @ qDoneSetup begin : a1          
      $info("done memory load" );           
      ready <= 1'b1;         
      @ (posedge clk)  ready <= 1'b0;
     end : a1   
     // In the example above, when the named sequence qDoneSetup reaches its end point, 
     the always block is unblocked.  Thus, the end of the sequence acts as the trigger to unblock the event.  
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.  
https://systemverilog.us/vf/Cohen_Links_to_papers_books.pdf