In reply to ben@SystemVerilog.us:
Thanks Ben…
Actually by mistake I have added [3:0] a . It is 1 bit only. Your first solution is working. But I had to add one condition in that.
($rose(a), v=delay+1'b1) |-> (**v>0****, v=v-1'b1)[*0:$] ##1 v==0 ##0 b == 1;