SystemVerilog checker function/task for two input arbiter

Hi,

I need help in writing a checker task to verify the following scenario:

Suppose we have a arbiter with two inputs(request) and outputs(grants). All are one bit wide. If a request goes high then it’s corresponding grant can come in 1-4 clock cycles. Also I have to match the grant with it’s corresponding request.

cycle | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 |
request| 1 | 0 | 1 | 0 | 0 | 0 | 0 | 0 | 0 |
grant | 0 | 0 | 0 | 1 | 0 | 1 | 0 | 0 | 0 |

So my req in Cycle 1 should match with grant in Cycle 4. Req in cycle 3 should only match with grant in cycle 6 but not with grant in cycle 4.

My initial approach is to write a automatic task and call that task whenever a req is asserted. But I am stuck at coming with a code.
Any help on this,please?

In reply to Alonso14:

A simplistic model (for 1 bit req/gnt, and not fully tested for all cases) is below:

 
  always @(posedge req) req_id++;
  always @(posedge gnt) gnt_id++;

  property p_uniq_req_gnt;
    int v_req_id;
    ($rose(req), v_req_id = req_id) |-> 
      ##[1:4] (gnt && (v_req_id == gnt_id ));
  endproperty : p_uniq_req_gnt

  a_p_uniq_req_gnt : assert property (p_uniq_req_gnt);


Idea - you will need tags/IDs to mark requests and grants.

// Edited - removed use of $sampled for local variables
// But will be needed for subroutine calls in some cases
// Thanks Ben Cohen for pointing this out.

Regards
Srini
www.go2uvm.org

In reply to Srini @ CVCblr.com:

  • The $sampled is not needed here, but is needed in an action block.
  • Because local variables (the IDs) are needed to support the assertions, it is recommended that you put your assertions inside a SystemVerilog checker and either instantiate that checker directly into your DUT, or bind it to your DUT. Below is such an example. You could, of course declare a module instead of a checker.
  • Putting assertions outside the DUT is a good idea.

checker reqack1to1 (bit req, gnt, clk);
  int req_id, gnt_id; 
  always_ff @(posedge req) req_id <= req_id + 1'b1; 
  always_ff @(posedge gnt) gnt_id <= gnt_id + 1'b1;
  default clocking @(posedge clk); endclocking
  property p_uniq_req_gnt;
	int v_req_id;
	($rose(req), v_req_id = req_id) |-> 
		##[1:4] (gnt && v_req_id == gnt_id);
  endproperty : p_uniq_req_gnt
  a_p_uniq_req_gnt : assert property (p_uniq_req_gnt);
endchecker  
	
module dut(input bit req, gnt, clk);  
   	reqack1to1 reqack1to1_i(req, gnt, clk); // checker instantiation 
endmodule 

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us

  • SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
  • A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
  • Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
  • Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 0-9705394-2-8
  • Component Design by Example ", 2001 ISBN 0-9705394-0-1
  • VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
  • VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115

Without assertion , this can be achieved through the following snippet of code .
Logic is not fully tested


int unsigned req_cnt =0;
int unsigned gnt_cnt =0;
int unsigned req_clk_cnt =0 ;
int unsigned gnt_clk_cnt =0;
      forever begin 
           @(posedge clk)
           if(req) begin
                  req_cnt++;
                   req_clk_cnt=0;
             end 
           else req_clk_cnt++;
           if (gnt) begin 
                if(req_cnt !=0) req_cnt--;
                if(req_cnt ==0) $error ("Gnt is asserted without Req");
                if((req_clk_cnt < gnt_clk_cnt) && (gnt_clk_cnt >4)) gnt_clk_cnt -=req_clk_cnt;
              end 
            else begin 
                  if(req_cnt !=0) gnt_clk_cnt++;
              end 
         if (gnt_clk_cnt >4) $error ("gnt is not asserted within [1:4] cycles");  
      end 

In reply to kddholak:

Without assertion , this can be achieved through the following snippet of code

… Which proves the point that using SVA is by far simpler to write and read.
Ben SystemVerilog.us

In reply to ben@SystemVerilog.us:

Yes I agree. Its gonna be simpler and clean

In reply to kddholak:

Because the assertion and the Id’s rely on edges of req and gnt you should write an assume statement.

am_no2reqs: assume property( req |=>!req) ;
am_no2gnts: assume property (gnt |=> !gnt) ;

Ben SystemVerilog.us