In reply to Ankit Bhange:
An until property of the non-overlapping form (i.e., until, s_until) evaluates to true if property_expr1 evaluates to true at every clock tick beginning with the starting clock tick of the evaluation attempt and continuing until at least one tick before a clock tick where property_expr2 (called the terminating property) evaluates to true. The until, s_until operators have an implicit repetition until the terminating condition (i.e., property_expr2) occurs. Specifically, with a strong until (e.g., s_until), if the simulation completes but the terminating condition is pending, the assertion fails, unlike the weak until where the assertion is evaluated as vacuously true.
$rose(req) |=> busy until ready); // Enhanced readability, and Identical to
// $rose(req) |=> busy[*0:$] ##1 ready ; // equivalent property expression
// Thus,
ap_until_sig1_stable_throughout_sig2: assert property(@(posedge clk)
$rose(sig2) |=> $stable(sig1) until !sig2);
// can be written as
ap_until_sig1_stable_throughout_sig2: assert property(@(posedge clk)
$rose(sig2) |=> $stable(sig1)[*0:$] ##1 !sig2);
// When sig2==0, sig1 need not be stable