Assertion to check req holds until ack

SystemVerilog
, , ,
4

In reply to yourcheers:

In reply to ben@SystemVerilog.us:

$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))); // without the $rose
//vs 
$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))); // with the $rose
// COMMENTS
a |-> b[->1] // If b==1 in cycle a==1 the property is true 
             // If b==0 in cycle a==1,  then b[->1] is equivalent to $rose(b)[->1]
             // because when b==1 you do get a $rose(b).
a |-> $rose(b)[->1] // If b==1 in cycle a==1, then you have to wait till 
             // b==0 and then rises back to b==1 
// Bottom line: Little difference if you know that b==0 when a==1

Ben SystemVerilog.us