Sva: once req asserted, 1-5 cycles later ack should be asserted

SystemVerilog
,
2

In reply to Jeff_Li_90:

2.without a req, ack should not be asserted. In other words, every ack should have its corresponding req from past 1-5 cycles, “uniquely”. note there could be multiple outstanding req/ack pair

This was answered without the uniqueness at


sequence s_ack; @(posedge clk)  ##[1:5] ack; endsequence 
ap_grant2: assert property(@(posedge clk) $rose(req) |-> ! s_ack.triggered);

For your issue, addressing your 2nd concern see code below: Key elements:

  • // Keep track of the number of request counts, +1 if req, -1 if ack
  • // Define a sequence to create endpoints in the last 5 cycles if rose(req)
  • // At new ack, then req count>0 and there was a req in the previous 5 cycles.

I believe that this would work, but I could have missed something.
Let me know if that is the case, but this is my current train of thoughts.


module top;
    timeunit 1ns;  timeprecision 100ps;    
    `include "uvm_macros.svh"   import uvm_pkg::*;
    bit clk, req, ack; 
    initial forever #10 clk = !clk; 
    int req_count; 
    // Keep track of the number of request counts, +1 if req, -1 if ack 
    always @(posedge clk) begin
        if(req)   req_count <= req_count + 1'b1;
        if(ack)  req_count <= req_count - 1'b1;
    end
    // Define a sequence to create endpoints in the last 5 cycles if rose(req) 
    sequence s_req; @(posedge clk) $rose(req)  ##[0:5] 1'b1; endsequence // endpoints at 0, 1, ..5 cycles after req
    // At new ack, then req count>0 and there was a req in the previous 5 cycles. 
    ap_ack2req: assert property(@(posedge clk) $rose(ack) |-> req_count > 0 && s_req.triggered);   
  
  
    initial begin
        bit v; 
      repeat (200) begin
        @(posedge clk);
        req <= 1'b1; @(posedge clk); req <= 1'b0; 
        repeat(3) @(posedge clk); 
        ack <= 1'b1; @(posedge clk); ack <= 1'b0; 
        // 
        req <= 1'b1; @(posedge clk); req <= 1'b0; 
        repeat(8) @(posedge clk); 
        ack <= 1'b1; @(posedge clk); ack <= 1'b0; 
        // 
        req <= 1'b1; @(posedge clk); req <= 1'b0; 
        repeat(2) @(posedge clk); 
        ack <= 1'b1; @(posedge clk); ack <= 1'b0; 
        // 
        req <= 1'b1; @(posedge clk); req <= 1'b0; 
        repeat(1) @(posedge clk); 
        ack <= 1'b1; @(posedge clk); ack <= 1'b0; 
        // 
        req <= 1'b1; @(posedge clk); req <= 1'b0; 
        repeat(9) @(posedge clk); 
        ack <= 1'b1; @(posedge clk); ack <= 1'b0; 
        // 

        if (!randomize(req, ack) with {
          req  dist {1'b1 := 1, 1'b0 := 1};
          ack  dist {1'b1 := 1, 1'b0 := 3};
          v    dist {1'b1 := 1, 1'b0 := 5};
        }) `uvm_error("MYERR", "This is a randomize error");
        if(v) begin @(posedge clk)  req <= 1'b1; repeat(6) @(posedge clk); end 
      end
      $finish;
    end
  endmodule

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
  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:

Udemy courses by Srinivasan Venkataramanan (http://cvcblr.com/home.html)
https://www.udemy.com/course/sva-basic/
https://www.udemy.com/course/sv-pre-uvm/