Assertion to check req holds until ack

SystemVerilog
, , ,
3

In reply to ben@SystemVerilog.us:

$rose(dsr_usr_rfsh_ack)[->1]

As there is a $rose, isn’t the above assertion successful only in the first clock when ack==1 ?

Should we change the above assertion to as follows:

$rose (dcr_usr_rfsh_req) |-> 
  (dcr_usr_rfsh_req[*1:$] ##1 !dcr_usr_rfsh_req  intersect
  (dsr_usr_rfsh_ack[->1] ##0 $fell(dcr_usr_rfsh_req)));