Hi,
I have a following code and TB:
module eventually_chk( input logic resetn, input logic reg_clk, input logic a, input logic b, input logic c);
property eventually_chk;
disable iff (!resetn) @(posedge reg_clk) ($rose (a) |=> s_eventually($rose (b) |=> c));
endproperty
eventually_chk_prop: assert property(eventually_chk)
$info("Success_eventually_chk @ %0t",$time);
else
$info("failure_eventually_chk @ %0t",$time);
endmodule
module tb_top;
logic resetn, reg_clk;
logic a, b, c;
initial begin
resetn = 1'b0;
#2
resetn = 1'b1;
end
initial begin
reg_clk = 1'b1;
forever reg_clk = #5 ~reg_clk;
end
initial begin
a=1'b0;
b= 1'b0;
c= 1'b0;
#41
a = 1'b1;
#10
a = 1'b0;
#80
b = 1'b1;
#10
b = 1'b0;
c = 1'b0;
#10
c = 1'b0;
end
initial begin
$dumpfile("dump.vcd");
$dumpvars;
#4000;
$finish();
end
eventually_chk eventuall_chkinst(resetn, reg_clk, a, b, c);
endmodule
Now I am expecting s_eventually($rose (b) |=> c to fail as c never goes to 1. However, if I run this on edaplayground mentor simulator, it shows the property success at 60ns.
I am not clear about behaviour of s_eventually. can someone explain please.
thanks,
-sunil puranik