In reply to ben@SystemVerilog.us:
Hi Ben,
( (1, v_t=v_t+1’b1)[*0:$] ##0 $rose(PORESET_B)) |-> (v_t >= 32);
// IS SAME as
( (1, v_t=v_t+1’b1)[*0] ##0 rose(PORESET_B) or // This is a NO match, meaningless (1, v_t=v_t+1'b1)[*1:] ##0 rose(PORESET_B) or (1, v_t=v_t+1'b1)[*2:] ##0 rose(PORESET_B) or ... (1, v_t=v_t+1'b1)[*n:] ##0 $rose(PORESET_B) |-> (v_t >= 32);
// For a success, ALL, really ALL terms of the antecedent must be tested for this property to succeed. If any antecedent is a no match, the property for that match is vacuously true. However, since this property can fail on another antecedent match, all terms of this infinite antecedent must be tested. That is why you need the first_match.
It seems that the assertion will work as the antecedent will be true, however it is not written accurately.