Triggered in SVA "request for more clarification"

i’m a beginner in studying SVA using SystemVerilog Assertions and Functional Coverage Guide to Language, Methodology and Applications book.

i did not understand the triggered concept, i used the below code to underestand the different between using it or not.

the triggered property give pass at time 130 and the non triggered one give pass at time 150.
i thought that both must give pass at time 130 when the readEndstate is stable.
also in the triggered one, it give me FAIL at time 10, which is not have meaning for me.

code:
module state_transition;
int readStartState, readIDState, readDataState, readEndState;
logic clk, read_enb;

sequence readSt;@(posedge clk) read_enb ##1 readStartState; endsequence
sequence readID;@(posedge clk) readStartState ##1 readIDState; endsequence
sequence readData;@(posedge clk) readIDState ##1 readDataState; endsequence
sequence readEnd;@(posedge clk) readDataState ##1 readEndState; endsequence
//property checkReadStates; //non triggered property
//@(posedge clk)
// readSt ##[1:] // readID ##[1:]
// readData ##[1:] // readEnd; //endproperty property checkReadStates; **//triggered property** @(posedge clk) readSt.triggered ##[1:]
readID.triggered ##[1:] readData.triggered ##[1:]
readEnd;
endproperty
sCheck: assert property(checkReadStates) else $display($stime,“FAIL”);
cCheck: cover property(checkReadStates) $display($stime,“PASS”);

initial begin
clk = 0;
read_enb = 1;
@(posedge clk) readStartState = 1;
@(posedge clk) readIDState = 1;
@(posedge clk)@(posedge clk); readDataState = 1;
@(posedge clk)@(posedge clk); readEndState = 1;
end

initial $monitor($stime,"clk= ",clk,“RE=”,read_enb,“RSS=%0b”,readStartState,“RIDS=%0b”,readIDState,“RDS=%0b”,readDataState,“RES=%0b”,readEndState);
always #10 clk = !clk;
endmodule

In reply to moustafaali:
I am providing a link of 2 pages from my SVA Handbook 4th Edition, 2016 ISBN 978-1518681448 that explains the .triggered Hopefully, it will give a better understanding of this method.


Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us


In reply to ben@SystemVerilog.us:

sequence q_ab; @ (posedge clk) a ##[1:3] b; endsequence
assert property(@ (posedge clk)(q_ab.triggered ) |=> 1)

In the above sequence let say we have three endpoints at clock tick 2,3,4 since it is multi thread and we are not using first operator in the declaration of sequence.
As per my understanding q_ab.triggered needs to return true at all these endpoints 2,3,4.

2.If we use the .triggered in the consequent side does it required first_match in the sequence declaration.

3.for example if a is asserted at clock tick 1,2,3 and b is asserted at clock tick 2,3,4.
How the above mentioned property will behave.

Please let me know.
Thanks

In reply to sudharshan:

In reply to ben@SystemVerilog.us:
sequence q_ab; @ (posedge clk) a ##[1:3] b; endsequence
assert property(@ (posedge clk)(q_ab.triggered ) |=> 1)
In the above sequence let say we have three endpoints at clock tick 2,3,4 since it is multi thread and we are not using first operator in the declaration of sequence.
As per my understanding q_ab.triggered needs to return true at all these endpoints 2,3,4.

q_ab.triggered may (not need) return true at all these endpoints 2,3,4.
It is false if b==0 at that time tick.

2.If we use the .triggered in the consequent side does it required first_match in the sequence declaration.
3.for example if a is asserted at clock tick 1,2,3 and b is asserted at clock tick 2,3,4.
How the above mentioned property will behave.

From my book, I referenced http://systemverilog.us/vf/triggered_cohen_book.pdf
Thus, an end point of a sequence is a Boolean expression (True/False) that represents the
evaluation of a thread of a sequence at its last cycle. Every time a thread of sequence completes it represents an endpoint for that thread. Thus, a multi-threaded sequence can have multiple endpoints. The value of sequence method (triggered) would be true at these endpoints. Applying a first_match method on a sequence_instance.triggered does not make sense, and is equivalent to sequence_instance (see guidelines below for an example).


@(posedge clk)  c |-> (q_ab.triggered ; 
// At every clocking event  (the @(posedge clk)) you have an attempt at the property. 
// If c==1, you test and see if there is an enpoint of q_ab at that tick.  
// If q_ab.triggered==1, then assertion is true, else false. 
// q_ab.triggered is a "SINGLE POINT", it is not a sequence and it has NO RANGE. 

@(posedge clk)  (q_ab.triggered |-> c ; 
// Same as above, 
// At every clocking event  (the @(posedge clk)) you have an attempt at the property. 
// q_ab.triggered is a "SINGLE POINT", it is not a sequence and it has NO RANGE. 
// q_ab.triggered may be true at tick 2, tick 3, tick 4; but those are at separate ticks. 
// Simularly, if I declare 
bit w; 
// w can be true at at tick 2, tick 3, tick 4; but those are at separate ticks. 
// Where is the range for w? 
 

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr


  1. SVA Alternative for Complex Assertions
    https://verificationacademy.com/news/verification-horizons-march-2018-issue
  2. SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
  3. SVA in a UVM Class-based Environment
    https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment