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?