Understanding SVA failure for hold_req_until_grant property

SystemVerilog
, , ,
1

Hi,

I have following property definition for checking that req should be held until grant is given. Grant can come in same cycle.

property p_hold_req_until_grant(clk,rst,req,gnt);
@(posedge clk) disable iff (rst)
rose(req) |=> req[*0:] ##0 $rose(gnt);
endproperty

This property fails when I get the grant in same cycle. I am not sure why though as *0 and ##0 is present. Please help me understand the failure and suggest correct implementation.

Thanks,
Vivek

2

In reply to vivek3016:

Figured out that it is because I am using non-overlapping operator for an arbiter which can give grant in same cycle.

property p_req_to_grant(clk,rst,req,gnt);
@(posedge clk) disable iff (rst)
req |-> ##[0:$] gnt;
endproperty

This code works fine.