Assertion for invalid clock behavior with respect to clock request and acknowledge

In reply to ChChee:
You can write an assertion using the sampling_clock as your main clocking event and use req, ack, and clk as the module variables. The relationship between the clocking event and clk is not clear. Below are 2 solutions. The fork-join_any solution allows you to tune the assertion to your requirements.


module top; 
  timeunit 1ns;  timeprecision 100ps;   
  `include "uvm_macros.svh"
  import uvm_pkg::*;
  bit sampling_clock, clk, req, ack;
  event e0, e1, e2, e3, e4;
    
//assert_b2b_check_missing_ack: assert property (@(posedge sampling_clock) b2b_check_missing_ack);
 
//property b2b_check_missing_ack;  // *** the clocking event  is  @(posedge clk) and not the sampling_clock
    //code here are conceptual only, it's not a working codes
    // @(posedge clk) $past(clk) == 0  |-> (##[0:$] changed(clk)) && req && !ack |-> !( (##[0:$] $stable(clk)) && req && !ack ) 
//endproperty
/* I wanted to screen the condition below (missing ack=1) in a sequence of:
1. clk off && req=1 && ack=0
2. clk active && req=1 && ack=0
3. clk off && req=1 && ack=0 */
/* - after req asserted, followed by at least 3 clk prior to ack assertion
- after req de-asserted, ack should also de-assert and followed by at least 3 clk pulses before clk off
- residue clk from previous req running in current req is allowed */
  let tmax=10; // number of clk cycles after ($rose(req) && !ack)

   // Possible assertion 
  ap: assert property(@ (posedge sampling_clock)  
                         $rose(req) && !ack |-> ##[1:tmax] ack);  

// Solution that can be more finely tuned. 
  task automatic  checkack();
    bit tmax_end, ack_end;
    fork
      fork1: begin 
          -> e0; // for debug 
          repeat(tmax) @(posedge clk);  
          tmax_end = 1'b1;
          -> e1;
          disable fork2;               
      end
      fork2: begin    
          @(ack); 
          ack_end=1'b1;
          -> e2;
          disable fork1;                      
      end
    join_any
  // $display("%t @join %t, err=%b", $realtime, $realtime, err); 
    if(tmax_end && !ack_end) begin 
        a_ackerr: assert (0);
         -> e3; 
    end        
  endtask
  always @(posedge sampling_clock) if($rose(req) && !ack) checkack(); 
  
endmodule
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home.html
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
...
1) SVA Package: Dynamic and range delays and repeats https://rb.gy/a89jlh
2) Free books:  Component Design by Example   https://rb.gy/9tcbhl
                Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
3) Papers: 
- Understanding the SVA Engine,
   https://verificationacademy.com/verification-horizons/july-2020-volume-16-issue-2
 - SVA Alternative for Complex Assertions
   https://verificationacademy.com/news/verification-horizons-march-2018-issue
 - SVA in a UVM Class-based Environment
   https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment