Not operator used with [*]

module test;
  
  logic a, b;
  logic clk;
  
  initial begin
    	  a = 0; b = 0; clk =0;
    #5    a = 0; b = 1;
    #10   a = 1; b = 1;
    #10   a = 0; b = 0;
    #10   a = 0; b = 1;
    #10   a = 0; b = 1;
    #50
    $finish;
  end
  
  always #5 clk = ~clk;
  
  property p1;
    @(posedge clk)
    $rose(a) |-> not (b[*2]);
  endproperty 
  
  assert property (p1) $display("%0d, assertion is pass", $time); else $error("%0t, assertion is failed", $time);
    
endmodule

here is a very simple example for not operator. if the a and b change like above, the assertion will be pass.

if they change like the way below, it won’t be failed or pass.

  initial begin
    	  a = 0; b = 0; clk =0;
    #5    a = 0; b = 1;
    #10   a = 1; b = 0;
    #10   a = 0; b = 1;
    #10   a = 0; b = 1;
    #10   a = 0; b = 1;
    #50
    $finish;
  end

can anyone explain this?

The changed code works correctly on 3 out of the 4 tools on EDA playground. You have run into a tool specific bug.

This Siemens sponsored public forum is not for discussing tool specific issues. Please read your tool’s User Manual or contact your tool vendor for support.