In reply to svq:
Thanks for the explanation . This makes sense. Last question, is it all right to use |=> in place of #=# ?
// You are suggesting changing this:
$rose(req)|->##[1:10]ack #=# always @(posedge clk) !ack);
// To
$rose(req)|->##[1:10]ack |=> always @(posedge clk) !ack);
// The issues here are VACUITY and meeting requirements
// If ack==0 for all 10 cycles, then the assertion is vacuously true.
The followed-by operator in the consequent concatenates a sequence and a property.
In this example, if ack==0 for all 10 cycles then the assertion fails.