Unbounded delay vs goto repetition

SystemVerilog
1

Hi, I am trying to understand the difference between unbounded delay operator and go-to repetition operator. Is there a case of success where these two will give different results ?

// Option-1
assert property (@(posedge clk) $rose(b) |-> (##[1:$] (a)))
 
// Option-2 
assert property (@(posedge clk)  $rose(b) |-> ##1 a[->1])
2

NO. However, if your consequent is an antecedent instead, then it’s a different situation.

 (##[1:$] (a)) |-> b // can never succeed, but can fail because 
                                // ALL threads of antecedent must succeed
a[->1] |-> b // is same as 
a |-> b; 
// the go is better use in something like 
cond1 ##1 a[->1] |-> b
// if cond1==1, then all threads where a==0 cause vacuous passes. 
// when a==1 then b is evaluated and the assertion is pass or a fail
1 Like