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