Recursive property call

SystemVerilog
,
1

Hi,
I saw this example in the book I am currently referring :


  sequence seq;
    c ##1 d ##1 e;  
  endsequence
  
  property rc1(ra,rb);    
    rb or ( ra and ( 1 |=> rc1( a, b ) ) ); // recursive property call
  endproperty  
  
  property s_rc1(c_seq,sra,srb);    
    c_seq |=> rc1( sra, srb ) ;
  endproperty  
  
  assert property( @(posedge clk) s_rc1( seq,a,b ) );

Unfortunately the book doesn’t elaborate on the working of the code.
What does it take for the assertion to pass ?

2

In reply to Have_A_Doubt:

Explanation:

The sequence seq models a sequence of events c, d, and e occurring consecutively.
The property rc1 is a recursive property that allows rb to be true, or if ra is true, it recursively checks the property after a one-clock delay.
The property s_rc1 calls rc1 with the sequence c_seq and states that if c_seq is satisfied, then rc1(sra, srb) should be true.
The assertion checks this property at every positive clock edge.
To make the assertion pass:

The sequence seq needs to be satisfied, meaning that c, d, and e occur in sequence.
The properties rc1 and s_rc1 must hold recursively based on the values of a and b.
For example, if the sequence seq occurs, and the properties rc1(a, b) and s_rc1(seq, a, b) hold true, the assertion will pass. The recursive property allows for a chain of events (c_seq in this case) and their associated conditions to be verified.

rahulvala@gmail.com
Freelancer/verification engineer
https://www.linkedin.com/in/rahulvala/