Assertion on req and gnt signals

SystemVerilog
,
6

In reply to pk_94:

You are correct that if you have 10 req pulse came with single gnt (on say 11th cycle) then you have 10 separate attempts all waiting for that ONE gnt. When the gnt arrives, it satisfies each of those 10 attempts.
(From my book) What is desired for this assertion is the exclusivity or uniqueness of each attempted thread sequences, meaning that one successful consequent does not terminate all concurrent attempts waiting for that consequent.
To accomplish this, one could use concepts of a familiar model seen in hardware stores in the paint department. There, the store provides a spool of tickets, each with a number. As a customer comes in, he takes a ticket. The clerk serving the customers has a sign that reads “NOW SERVING, TICKET x”. The customer that has the ticket gets served, the others have to wait. When done, the number X in incremented, and the next in-line customer gets served.
The assertion code could then be written as follows:


import uvm_pkg::*; `include "uvm_macros.svh" 
module top; 
    timeunit 1ns;     timeprecision 100ps;    
    bit clk,req, ack;  
    int ticket, now_serving; 
    default clocking @(posedge clk); 
    endclocking
    initial forever #10 clk=!clk;  
    
    function void inc_ticket(); 
        ticket = ticket + 1'b1; 
    endfunction 

    property reqack_unique;
        int v_serving_ticket;
        @(posedge clk) ($rose(req),  v_serving_ticket=ticket, inc_ticket()) |-> 
             ##[1:10] now_serving==v_serving_ticket ##0 ack; 
    endproperty
    ap_reqack_unique: assert property(reqack_unique) 
         now_serving =now_serving+1; else now_serving =now_serving+1; 
    
    
    initial begin 
        repeat(100) begin 
            @(posedge clk); #1;  
            if (!randomize(req, ack)  with 
            { req dist {1'b1:=1, 1'b0:=3};
            ack dist {1'b1:=1, 1'b0:=5};       
        }) `uvm_error("MYERR", "This is a randomize error")
    end 
    repeat(200) begin
        @(posedge clk); #1
        if (!randomize(req, ack)  with 
        { req dist {1'b1:=1, 1'b0:=3};
        ack dist {1'b1:=0, 1'b0:=1};       
    }) `uvm_error("MYERR", "This is a randomize error")
end
$stop; 
end 
endmodule

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

** 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 | Verification Academy
  2. Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
    Real Chip Design and Verification Using Verilog and VHDL($3) Amazon.com
  3. Papers: