Always, s_always property examples

In reply to ben@SystemVerilog.us:

Hi Ben,

Thanks for the reply.


    assert property ( always [4:5] a ##[1:4] b |=> c );
   

    //Assertion isn't failing for this case. I don't understand why it isn't failing? 
initial begin
       a=0; b=0; c=0;
       @(negedge clk); a = 0; b=0; c=0;
       @(negedge clk); a = 1; b=0; c=0;
       @(negedge clk); a = 1; b=0; c=0;
       @(negedge clk); a = 0; b=0; c=0;
       @(negedge clk); a = 0; b=1; c=0;
       @(negedge clk); a = 0; b=0; c=0;
       @(negedge clk); a = 0; b=0; c=0;
end
   

//Assertion is failing for this case where same sequence is happening but it is 1 clock delayed.  
initial begin
       a=0; b=0; c=0;
       @(negedge clk); a = 0; b=0; c=0;
       @(negedge clk); a = 0; b=0; c=0;
       @(negedge clk); a = 1; b=0; c=0;
       @(negedge clk); a = 1; b=0; c=0;
       @(negedge clk); a = 0; b=0; c=0;
       @(negedge clk); a = 0; b=1; c=0;
       @(negedge clk); a = 0; b=0; c=0;
       @(negedge clk); a = 0; b=0; c=0;
end