Assertions

sequence seq1;
a##1b;
endsequence

sequence seq2;
##2 c;
endsequence

property prop;
@(posedge clk) seq1.triggered |-> seq2.triggered;
endproperty

for the above code the checker is started at end of sequence of ‘seq1’ that I understand but what I dont understand is ‘seq2’ is also finishing in the same cycle for the triggered method why is happening I do not get it.I mean ‘seq2’ contains ‘c’ which should be evaluated after 2 clock cycles because there is 2 cycle delay but it is getting checked and evaluated at the end of ‘seq1’ even after having ##2 in ‘seq2’.

In reply to Shiv_coder:
Using pseudocode


cycle                          1     2     3     4   
start point name               q     r     s     t                       
seq1: (a##1b).triggered              q     r     s   
seq2: (##2 c).triggered                    q     r  
seq1.triggered with sequence called 'q' that started at cycle 1 has an end point at cycle 2
seq2.triggered with sequence called 'q' that started at cycle 1 has an end point at cycle 3

thus seq1.triggered |-> seq2.triggered evaluated only end points. 
At cycle 3 you evaluate the end point of seq1 that started at cycle 2 with the
                            end point of seq2 that started at cycle 1


Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
  2. Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
    Real Chip Design and Verification Using Verilog and VHDL($3) Amazon.com
  3. Papers:

Udemy courses by Srinivasan Venkataramanan (http://cvcblr.com/home.html)
https://www.udemy.com/course/sva-basic/
https://www.udemy.com/course/sv-pre-uvm/

In reply to ben@SystemVerilog.us:

Hi Ben,

I have some query with triggered. can you help to resolve it.
As,seq1 started at cycle and end at cycle 2.
And seq2 start at cycle 1 and end at cycle 3.
Can you explain more about below statement.



thus seq1.triggered |-> seq2.triggered evaluated only end points. 
At cycle 3 you evaluate the end point of seq1 that started at cycle 2 with the
                            end point of seq2 that started at cycle 1

As, seq1 completed at cycle 2 and we have used overlapping implication ( |-> ).
How it’s start evaluation at clock 3 and not at clock 2?

Also, I have tried example available below.


case 1:- ##1 c // As, seq2 is completed it get match at end.
case 2:- ##2 c // As, we used |-> why it take next clock (3).
case 3:- ##3 c // Fail expected. Pass with |=>

Thanks!

In reply to harsh pandya:

Two comments:
Coding error:

sequence seq1;
  a##1b;
endsequence
 
sequence seq2;
  ##2 c;
endsequence
 
property prop;
  @(posedge clk) disable iff(rst)
  seq1.triggered |-> seq2.triggered;
endproperty
ERROR SVAREAD2667 "triggered method call on unclocked sequence is forbidden." "testbench.sv" 21  7
ERROR SVAREAD2667 "triggered method call on unclocked sequence is forbidden." "testbench.sv" 21  26
ERROR SVAREAD2671 "Invalid property 'prop' definition. " "testbench.sv" 24  23

Your rational:

As, seq1 completed at cycle 2 and we have used overlapping implication ( |-> ).
How it’s start evaluation at clock 3 and not at clock 2?


sequence seq1; @(posedge clk) a##1b; endsequence // the clocking event is needed because you
                    // you use the end points, and those are started at every ce 
sequence seq2; @(posedge clk) ##2 c; endsequence
// At every clocking event the simulator srts the computation of the needed end points. 
//  seq1 that started at cycle 1 (let's call this cycle 'q') completed at cycle 2
//  seq1 that started at cycle 2 (let's call this cycle 'r') completed at cycle 3
//  seq2 that started at cycle 0 (let's call this cycle 'p') completed at cycle 2
//  seq1 that started at cycle 1 (let's call this cycle 'q') completed at cycle 3
cycle                      0    1     2     3     4   
start point name           p    q     r     s     t                       
seq1: (a##1b).triggered               q     r     s   
seq2: (##2 c).triggered                     q     r  
// THUS, with seq1.triggered |-> seq2.triggered; 
// at every clocking event you are evaluating the endpoints, 
// ***************  regardless of when they started  **************************
// At cycle 2 you compare the endpoints only
//  seq1 that started at cycle 1 (let's call this cycle 'q') completed at cycle 2
//  seq2 that started at cycle 0 (let's call this cycle 'p') completed at cycle 2
// At cycle 3
//  seq1 that started at cycle 2 (let's call this cycle 'r') completed at cycle 3
//  seq2 that started at cycle 1 (let's call this cycle 'q') completed at cycle 3

Ben

In reply to ben@SystemVerilog.us:
Hi Ben,

Thanks for your feedback. I got it.
Btw, sorry for compilation error.
I have checked my example with xrun only and in which it works without compilation error.

Harsh!