SVA : |-> and ##0 is behaving different. |-> adding one extra cycle

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

In reply to svassert:

Looking at your code:
##[1:100] ($rose(p1) || $rose(p0)) |-> ($rose(p1) && (!p0)) ;
The condition is satisfied only with $rose(p1) because
you cannot have a $rose(p0) and a !p0 in the same cycle. A $rose(p0) means that p0 went to a 1’b1.
Thus, at the endpoint of ($rose(p1) || $rose(p0)) the assertion will fail if you have a
$rose(p0).
Your assertion has multiple matches, you should consider using the first_match and restructure your assertion to consider the endpoint.
To avoid a first_match you could write something like


($fell(p1) && p0) |-> ##1 ($rose(p1) || $rose(p0)[->1] within 1[*100];// |-> ($rose(p1) && (!p0)) ;

Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

or Links_to_papers_books - Google Docs