Assertion to check req holds until ack

In reply to lisa.lalice:

You need either a default clocking or a @(posedge clk) in either the property or in the assertion.

 

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);

Ben systemverilog.us