Hi Forum,
I see weird behavior with |-> operator. Ive below example:
In the below property I’m checking ($rose(p1) && (!p0)) only after ($rose(p1) || $rose(p0)). So using |-> , but this is delaying the check by one cycle. If I use ##0 (below line commented), it does check in the same cycle. But the assertion is evaluated multiple times where it need not to be. I need the |-> working fine in the same cycle. Suggestions appreciated.
property phase_check_p0_streched (dfiClk, dfi_reset, init_complete, p0, p1);
@(negedge dfiClk) disable iff (!dfi_reset ) ($fell(p1) && p0) ##[1:100] ($rose(p1) || $rose(p0)) |-> ($rose(p1) && (!p0)) ;
//@(negedge dfiClk) disable iff (!dfi_reset ) ($fell(p1) && p0) ##[1:100] ($rose(p1) || $rose(p0)) ##0 ($rose(p1) && (!p0)) ;
endproperty
module tb;
bit val, en, reset, clk, en_count, val_count, init_complete, p0, p1;
assert_chk_p0_stretch : assert property (phase_check_p0_streched (clk, reset, init_complete, p0, p1))
else $error("ch$ch$_umc$phy$_dfi_rddata_valid_$ph$ assertion Check", $sformatf("stretch p1 error\n"));
always #5 clk = ~clk;
initial begin
#10 ; p0 = 0; p1 = 0; reset = 0;
#15 ; p0 = 0; p1 = 0; reset = 1;
#10 ; p0 = 0; p1 = 0;
#10 ; p0 = 1; p1 = 1; init_complete = 1;
#10 ; p0 = 0; p1 = 0;
#10 ; p0 = 0; p1 = 0;
#10 ; p0 = 1; p1 = 1;
#10 ; p0 = 1; p1 = 1;
#10 ; p0 = 1; p1 = 1;
#10 ; p0 = 0; p1 = 1;
#10 ; p0 = 0; p1 = 0;
#10 ; p0 = 0; p1 = 0;
#10 ; p0 = 1; p1 = 0;
#10 ; p0 = 1; p1 = 1;
#10 ; p0 = 1; p1 = 1;
#10 ; p0 = 1; p1 = 1;
#10 ; p0 = 1; p1 = 1;
#10 ; p0 = 0; p1 = 0;
#10 ; p0 = 0; p1 = 0;
#10 ; p0 = 0; p1 = 0;
#10 ; p0 = 1; p1 = 1;
#10 ; p0 = 1; p1 = 1;
#10 ; p0 = 1; p1 = 1;
#10 ; p0 = 1; p1 = 1;
#10 ; p0 = 1; p1 = 0;
#10 ; p0 = 0; p1 = 0;
#10 ; p0 = 0; p1 = 0;
#10 ; p0 = 0; p1 = 0;
#10 ; p0 = 1; p1 = 1;
#10 ; p0 = 1; p1 = 1;
#10 ; p0 = 1; p1 = 1;
#10 ; p0 = 1; p1 = 1;
#10 ; p0 = 1; p1 = 0;
#10 ; p0 = 0; p1 = 0;
#10 ; p0 = 0; p1 = 0;
#10 ; p0 = 0; p1 = 1;
#10 ; p0 = 1; p1 = 1;
#10 ; p0 = 1; p1 = 1;
#10 ; p0 = 1; p1 = 1;
#10 ; p0 = 1; p1 = 1;
#10 ; p0 = 0; p1 = 0;
#10 ; p0 = 0; p1 = 0;
#10 ; p0 = 0; p1 = 0;
$finish();
end
initial begin
$fsdbDumpvars(0,"+all");
$fsdbDumpSVA();
end
endmodule