SVA: How to solve false pass of same consequent condition used for back to back antecedent?

Below is the concurrent SVA for req/gnt protocol, won’t be same “gnt” meet requirement for back to back “req” (T1 & T2)?
Would implicit first_match operator takes cares of it? If not, any recommendation or suggestion to solve this?

property p1
@(posedge clk) req → ##[1:5] gnt;
endproperty

Timing Diagram:

clk |0|1|2|3|4|5|6|7|8|9|10|
req |-|__________________
T1
req |-|______________
T2
gnt |-|__
T1 Pass
T2 Pass?

In reply to ns27:

With @(posedge clk) req → ##[1:5] gnt;, your example shows 2 successful attempts:
One attempt at T1 and another at T2. Each attempt starts a new thread and it is looking for a gnt at any cycle with 5 cycles from the req.
For the T1 req, we’re looking a=for a gnt at cycle 2, 3, 4, 5. or 6
For the T2 req, we’re looking a=for a gnt at cycle 3, 4, 5. 6, or 7
You now have 2 concurrent independent threads, and each looking for a gnt within a number of cycles from their starts. Since you have a gnt at cycle 6, both threads will suceed.

I strongly urge you to read my paper Understanding the SVA Engine,
Verification Horizons - July 2020 | Verification Academy

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 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:

In reply to ben@SystemVerilog.us:

Thank you Ben for detail explanation.
With reference to your paper on Understanding SVA Engine for above example I could model below,

For T1 → On antecedent match → t_consequent → separate 5 threads → On any thread match it will succeed
For T2 → On antecedent match → t_consequent → separate 5 threads → On any thread match it will succeed

But same gnt is succeeding for 2 independent threads (req) which is potentially incorrect for a system in which there has to be a “gnt” for every “req”. Is there any operator/construct or re-code SVA we need to overcome this problem? Apology if I have overlooked your paper which talks about solution, can you please point me to the relevant section?

In reply to ns27:

Add external counter to count number of req and gnt
Below is the simple code how to resolve this
bit[1:0] req_num,gn_num;
always @(posedge clk) begin
if(rst) begin
req_num=0;gnt_num=0;
end
else begin
if(req) req_num++;
if(gnt) gnt_num++;
end
end

property p1
bit [1:0] num;
(req,num = req_num)-> ##[1:5](gnt && (num == gnt_num));
endproperty

Hope this helps.

In reply to kalva:

With reference to your paper on Understanding SVA Engine for above example I could model below,
For T1 → On antecedent match → t_consequent → separate 5 threads → On any thread match it will succeed
For T2 → On antecedent match → t_consequent → separate 5 threads → On any thread match it will succeed

Your understanding of SVA is correct; this is how it works.

But same gnt is succeeding for 2 independent threads (req) which is potentially incorrect for a system in which there has to be a “gnt” for every “req”. Is there any operator/construct or re-code SVA we need to overcome this problem? Apology if I have overlooked your paper which talks about solution, can you please point me to the relevant section?

To accomplish uniqueness, you need supporting logic. Below are 2 solutions: mine and a modified version of the one suggested by the previous post. The previous post made the error of not incrementing the gnt_num when the property failed (i.e., when no gnt was received within the 1:5 clk periods.


/*You are correct that if you have 5 req pulse came with single gnt (on say 6th cycle) then you have 5 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, gnt, rst;  
    int ticket, now_serving; 
    int req_num,gnt_num;
    initial forever #10 clk=!clk;  
    always @(posedge clk) begin
      if(rst) begin
         req_num<=0; gnt_num<=0;
      end 
      else begin
       if(req) req_num<= req_num +1'b1;
       // if(gnt) gnt_num<= gnt_num + 1'b1;
      end
    end

    function void inc_gnt_num(); 
        gnt_num<= gnt_num + 1'b1;
    endfunction 

    property p_not_working;
      int num;
      (req, num=req_num) |-> ##[1:5](gnt && (num == gnt_num));
    endproperty
    ap_not_working: assert property(@ (posedge clk) p_not_working );  

    property p1;
        int num;
        (req, num=req_num) |-> ##[1:5](gnt && (num == gnt_num), inc_gnt_num());
      endproperty
      ap_1: assert property(@ (posedge clk) p1 ) else inc_gnt_num();  

    ///////////////////////
 
    function void inc_ticket(); 
        ticket = ticket + 1'b1; 
    endfunction 
 
    property reqgnt_unique;
        int v_serving_ticket;
        @(posedge clk) (req,  v_serving_ticket=ticket, inc_ticket()) |-> 
              ##[1:5] now_serving==v_serving_ticket ##0 gnt; 
    endproperty
    ap_reqgnt_unique: assert property(reqgnt_unique) 
         now_serving =now_serving+1; else now_serving =now_serving+1; 
 
 
    initial begin 
        repeat(100) begin 
            @(posedge clk); #1;  
            if (!randomize(req, gnt)  with 
            { req dist {1'b1:=1, 1'b0:=3};
            gnt 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, gnt)  with 
        { req dist {1'b1:=1, 1'b0:=3};
        gnt 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 http://cvcblr.com/home.html
** 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:

In reply to ben@SystemVerilog.us:

Got it. Thank you Ben!

In reply to kalva:

Thank you Kalva!