Assertion to check req holds until ack

SystemVerilog
, , ,
8

In reply to ben@SystemVerilog.us:

It seems like my assertion only works when I assert it straight away instead of using property/endproperty

This is what I did and it works

rfsh_req_holds_until_ack_a : assert property(@(posedge clk) 
$rose (dcr_usr_rfsh_req) |-> dcr_usr_rfsh_req[*1:$] ##1 !dcr_usr_rfsh_req intersect $rose(dsr_usr_rfsh_ack)[->1] ##0 $fell(dcr_usr_rfsh_req));

This, on the other hand, the code that I did previously and it fails. It’s actually the same code I’m not sure why it fails

property rfsh_req_wait_for_ack_p;
@(posedge clk)
$rose (dcr_usr_rfsh_req) |-> 
  (dcr_usr_rfsh_req[*1:$] ##1 !dcr_usr_rfsh_req  intersect
  ($rose(dsr_usr_rfsh_ack)[->1] ##0 $fell(dcr_usr_rfsh_req)));
endproperty
rfsh_req_wait_for_ack_a : assert property(rfsh_req_wait_for_ack_p);