Assertion property to check for toggle count of a signal between two control signals

In reply to Shubhabrata:


module m;
    bit clk, vld, req, ack, rst_n=1;
    int err1, err2, pass1, pass2; 
    initial forever #10 clk = !clk;
  property p1; // need 2 or more vld in this example
    int count = 0;
    @(posedge clk) disable iff(!rst_n)
    $rose(req) |=> 
    ((vld && $changed(vld)[->1],count++)[*1:$] ##0 (count >= 2)##1 
     $rose(ack) && !vld [->1] );
  endproperty
  assert property (p1) pass1=pass1+1; else err1=err1+1;
// Above assertion misses the condition of a ack and a vld in the same cycle
// particularly if this should be an error 
// The following des check for this. 
// I don;t think you need the first_match here
// but I believe the simulator will not try the other threads
  property p2;
    int count = 0;
    @(posedge clk) disable iff(!rst_n)
    $rose(req) |=> 
    first_match((vld && $changed(vld)[->1],count++)[*1:$] ##0 (count >= 2)) ##1 
    $rose(ack) && !vld [->1];
  endproperty
  assert property (p2) pass2=pass2+1; else err2=err2+1;
  
  ap_ack_vld: assert property(@(posedge clk)  not($rose(ack) && vld)) else err3=err3+1;

Ben