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

SystemVerilog
,
1

came across with this question online and have no good idea about requirement #2:

requirements:
1.once req asserted, ack should be asserted within 1-5 cycles, uniqueness here is required.
2.with out 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

for 1st requirements, it’s easy to implement with the “now serving, tkt X” style from assertion handbook

int tkt, now_serving;
function void inc_tck();
tkt = tkt + 1'b1;
endfunction

property p_req_ack;
int v_serving_tkt;
(req, v_serving_tkt = tkt, inc_tkt()) |=> ##[1:5] ack && now_serving == v_serving_tkt;
endproperty

assert property(p_req_ack) now_serving = now_serving+1;
else now_serving = now_serving+1;

But I’m now sure what’s the best way to implement 2nd requirement which is basically the reverse direction of uniqueness;

Thanks,
Jeff

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/

3

In reply to ben@SystemVerilog.us:
OOPS! Need to correct the counters
Note: if req and ack are both true you get 2 NBA assignments to the same variable with different values; the simulator may accept the last one, and it will not function as intended.
NEW CHANGE:


always @(posedge clk) begin
        if(req && !ack)  req_count <= req_count + 1; // was if(req) ... * 1'b1
        if(ack && !req)  req_count <= req_count - 1; // was if(ack) ... - 1'b1
    end

Updated code at http://systemverilog.us/vf/unique_ack.sv

4

In reply to ben@SystemVerilog.us:

This is a clever solution to workaroud the uniqueness requirement! Thank you Ben.