SVA goto operator

SystemVerilog
1

Is there any logic reason to have a property sequence which ends with the use of the goto operator? [->]?
In my example, as long as “full” asserts once after gi (within 3 cycles), then after that, the property cannot fail. If full never occurs again, the assertion is evaluated forever (right?).

property p_gi;
    disable iff (reset) 
    $rose(gi) |-> gi[*10:20] ##[0:3] full [->3];
  endproperty
  GI_PROTOCOL : assert property (p_gi);
2

In reply to bmorris:
Your are correct.

b[->3] is equivalent to:
!b[*0:$] ##1 b ##1 !b[*0:$] ##1 b  ##1 !b[*0:$] ##1 b
If full never occurs again (after the first (!b[*0:$] ##1 b)), the assertion is evaluated forever.  It is waiting for !b[*0:$] ##1 b  ##1 !b[*0:$] ##1 b

Is there any logic reason to have a property sequence which ends with the use of the goto operator? [->]?

Yes,


ap: assert property(@(posedge clk) a |-> b[->1]); 
// equivalent to: 
ap: assert property(@(posedge clk) a |-> !b[*0:$] ##1 b);   
// after a, assertion passes on the first occurrence of b 
// That would be the same, in this case, as 
ap: assert property(@(posedge clk) a |-> ##[1:$] ##1 b);
The notation of the goto is neat; I read b[->1] as the first occurrence of b, instead of a delay till b. 
Same difference, just a way of seeing things. 
The goto makes a lot of sense in an antecedent 
ap_better: assert property(@(posedge clk) 
                  a ##1 b[->1] |-> c);  // no first_match() needed here
ap_never_passes_can_fail: assert property(@(posedge clk) 
                 (a ##[1:$] b) |-> c); 
// for ap_never_passes_can_fail to pass all sequences of antecedent must be tested 
ap_can_pass_or_fail: assert property(@(posedge clk) 
                  first_match(a ##[1:$] b) |-> c);

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