Equivalent expression for b[=0]

SystemVerilog
,
7

In reply to ben@SystemVerilog.us:

I don’t think that your approach with simulatn_ends = 1; will work because of sampling.
I think that you need to set the simulatn_ends = 1; before the end of sim

Thanks Ben for the pointer. Will have to work on some alternative logic

The max range cannot use the $, but you can use a 2^31 (syntax? forgot it)

I believe you meant 2**31


Later I was trying a variation of the consequent 

  property ab2;
   @(posedge clk) a |=> b[->0]; // consequent changed from b[=0]
  endproperty

As you have already explained above , *b[=0] is equivalent to !b[0:$]

What would the equivalent expression for b[->0] be ?

I am aware that :

b[->1] is equivalent to !b[*0:$] ##1 b[*1]


Shouldn't b[->0] be equivalent to !b[*0:$] ##1 b[*0] i.e !b[*0:$] ?

However I observe different results with consequent as b[->0] compared to b[=0] for following stimulus


always #5 clk = ~clk;
initial begin
  #4; a = 1;
 #10; a = 0;
 #30; b = 1;
end

With b[=0] the assertion passes at T:15 whereas the assertion fails at T:15 with b[->0]