Hello,
I want to write an assertion to check round robin behavior .
assume we have two require signals : req1 req2__ , and two grant signals : gnt1 , gnt2;
then if req1 and req2__ are high , and as a result gnt1__ is high , then next gnt1__ must occur after gnt2 __is up.
How can i write it in SVA ?
Thanks
In reply to Jad:
For 2 signals, it is easy. However, if you have a large vector, you’ll need to add some supporting logic to keep track as to who next can get the grant if the req is asserted.
module roundrobbin;
bit clk;
bit[1:0] req, grnt;
bit[3:0] r, g, grants;
ap_grnt1_after2: assert property(@(posedge clk)
req[1] && !grnt[1] && $fell(grnt[0]) |=> grnt[1]);
ap_grnt1_no2: assert property(@(posedge clk)
req[1] && $countones(grnt)==0 |=> grnt[1]);
endmodule
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
In reply to ben@SystemVerilog.us:
Need Input !!
I have used following code to verify round robin arbitrator using SystemVerilog Assertions, can anyone of you correct me if I’m wrong, or kindly share if you have an efficient code than the following, thank you!!
I’m particularly looking for a long/lengthy chain of requests/grant
here gnt = Grant of length 16
req = Request of length 16
generate
for (genvar i = 0; i<16; i++)
for (genvar j=i+1; j!=i; j++)
begin
if(j==16)
j=0;
assert property
(
@posedge clk
(gnt[i] && req[j]) |=> (gnt[j] && !req[j]) // Edit: previous error has been correct here
)
end
endgenerate
// Below code is to make sure only one gnt is high at any point of time
assert property
(
@posedge (clk)
$onehot(gnt) ==1;
)
In reply to vvv:
In reply to ben@SystemVerilog.us:…round robin arbitrator.
generate
for (genvar i = 0; i<16; i++)
for (genvar j=i+1; j!=i; j++)
begin
if(j==16)
j=0;
assert property
(
@posedge clk
(gnt[i] && req[j]) |=> (gnt[j] && !req[i])
)
end
endgenerate
// Below code is to make sure only one gnt is high at any point of time
assert property
(
@posedge (clk)
$onehot(gnt) ==1;
)
Your approach in using the generate statement is good, but your implementation is incorrect. For a round robin, you need to add some supporting logic to keep track as to who next can get the grant if the req is asserted. For example, assume that req[4] got the grant. Now req[3] and req[7] both want the grant; who gets it? Next in line to get is #5, but req[5]==0.
Below is a link from my SVA book for an arbiter with 16 bit inputs where there could be multiple requests, but there is a single grant with bits of higher order having higher priority.
http://systemverilog.us/arbiter_cohen.pdf
For your round robin model, you’ll need some supporting logic to hold which grant was previously granted. You may need some additional logic to predict which ones can get the next grant. Below is a model that I started (using 4 bits to ease the verification. It is not fully tested, and may not even do what you want. However, it may be a step in the right direction. Basically, it uses the previous grant along with an arbiter. You’ll need to do the verification. I provided test vectors using constrained-random tests. Let me know how this works for you.
import uvm_pkg::*; `include "uvm_macros.svh"
module top;
bit clk;
bit[3:0] req, gnt, prev_grnt;
default clocking @(posedge clk); endclocking
initial forever #10 clk=!clk;
generate for (genvar i=0; i<=4; i++)
begin
property p_arbiter;
bit[16:0] v;
(req[i]==1'b1, v=prev_grnt, v[i+1]=1'b1) ##0 req < v |->
gnt[i]==1'b1 ##0 $onehot(gnt);
endproperty : p_arbiter
ap_arbiter: assert property(@(posedge clk) p_arbiter);
end
endgenerate
ap_zero_req0: assert property(@(posedge clk) req==0 |-> gnt==0);
initial begin
repeat(200) begin
@(posedge clk);
if (!randomize(req, gnt, prev_grnt) with
{ req inside {0, 1, 2, 4}; // dist {1'b1:=1, 1'b0:=3};
gnt inside {0, 1, 2, 4}; // dist {1'b1:=1, 1'b0:=2};
prev_grnt inside {0, 1, 2, 4};
}) `uvm_error("MYERR", "This is a randomize error")
end
$finish;
end
endmodule
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
Hey Ben thanks for taking time to reply.
Just to make sure we both are in same page and understanding same. I still feel that my code works good for round robin.
To clarify any confusion in the problem, i will write it down below,
Problem statement:
Even though i have considered 16 variables in my solution for understanding purpose lets consider 4 variable round robin arbitrator,
A = req[0], B = req[1], C = req[2], D = req[3]
grant should be cyclic: A → B → C → D → A . . .
if all the request is preset then grant follows above order, if not then it will grant the next available request in the cyclic order i.e if C - request is absent then it will follow this order, A → B → D → A → . .
Here we also assume that we give only 1-grant clk tick to serve the request.
So for the above problem i feel my solution will work and i don’t think we need to keep a track of request and grant sequence in round-robin fashion.
In my solution, variable ‘i’ will keep a track of request in order and ‘j’ will track the grant, i don’t think we need to keep a track of previous grant in this case.
Please correct me if i’m missing out anything.
Or any good example in which my solution fails will be good to get a better solution and cover the corner cases
assert property
(
@posedge clk
(gnt[i] && req[j]) |=> (gnt[j] && !req[j]) // Sorry i had made a mistake !req[j] variable which i have corrected
)
In reply to vvv:
You have not compiled or run your model did you?
With your for (genvar i = 0; i<4; i++)
for (genvar j=i+1; j!=i; j++)
I got error message like
** Error: roundrb.sv(23): (vopt-2134) Evaluation of a generate loop has exceeded the iteration limit of 100000.
# ** Note: roundrb.sv(23): (vopt-2129) Design elaboration has evaluated 100001 loop generated blocks....
To verify your model, get one that compiles and eleborates OK.
Use constrained-random tests to test a small dample, and check it out. Below is an example for a simple driver:
initial begin
repeat(200) begin
@(posedge clk);
if (!randomize(req, gnt, prev_grnt) with
{ req inside {0, 1, 2, 4}; // dist {1'b1:=1, 1'b0:=3};
gnt inside {0, 1, 2, 4}; // dist {1'b1:=1, 1'b0:=2};
prev_grnt inside {0, 1, 2, 4};
}) `uvm_error("MYERR", "This is a randomize error")
end
$finish;
end
endmodule
BTW, add labels to you assertions. The @ posedge(clk) (<<-- incorrect) should be written as @(posedge clk)
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
In reply to ben@SystemVerilog.us:
Analyze and test the following assertion with test case in http://systemverilog.us/roundrb.sv
It makes use of my arbiter. The end case needs adjustment.
bit clk;
bit[3:0] req, gnt;
wire[3:0] prev_grnt;
default clocking @(posedge clk); endclocking
initial forever #10 clk=!clk;
assign prev_grnt=gnt; // <---- NOTICE this per your assumptions
generate for (genvar i=0; i<=4; i++)
begin
property p_arbiter;
bit[16:0] v;
(req[i]==1'b1, v=prev_grnt, v[i+1]=1'b1) ##0 req < v |=>
gnt[i]==1'b1 ##0 $onehot(gnt);
endproperty : p_arbiter
ap_arbiter: assert property(@(posedge clk) p_arbiter);
end
endgenerate
ap_zero_req0: assert property(@(posedge clk) req==0 |-> gnt==0);
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
Hi Ben,
I appreciate your effort in correcting even small errors to give more clarity and guiding all of us towards the solution,
But i was trying to analyze your solution but I’m not getting enough clarity on following 2 things,
v[i+1]=1'b1) ##0 req < v
In addition, i also see that ‘v’ is 16 bit long and all others are 4 bit long, is there any particular reason for this ?
Could you please let me know little more on this sometime when you are free ?
In reply to vvv:
assign prev_grnt=gnt; // <---- NOTICE this per your assumptions
// generate ...
bit[16:0] v;
(req[i]==1'b1, v=prev_grnt, v[i+1]=1'b1) ##0 req < v |=>
gnt[i]==1'b1 ##0 $onehot(gnt);
To better understand this, consider some simple scenarios:
req==4'b0111 (i.e., req==7), gnt==prev_grnt==0001
**[3] for the gen of req[3], v=prev_grnt=0001, v[i+1] i.e., v[4]==1; thus v=10001 (i.e., v==17).
req[3]==0, so assertion is vacuous, req(which is==7) < 17 is true, but req[3]==0
**[2] for the gen of req[2], v=prev_grnt=0001, v[i+1] i.e., v[3]==1; thus v=1001 (i.e., v==9).
req(which is==7) < 9 is true, thus this assertion for req[2] is true, and gnt[2] must be true
** [1]for the gen of req[1], v=prev_grnt=0001, v[i+1] i.e., v[2]==1; thus v=0101 (i.e., v==5).
req(==7] < 5 is false, thus this assertion for req[1] is false, and gnt[1] must be 0
Basically, the v[i+1]is used to set the priority.
The fact that v is 16 bits is immaterial here.
The end condition might be problematic and needs to be considered.
Hopefully, it will get you thinking!!!
Ben SystemVerilog.us
@user49 came across this post today and am trying to understand your code. In case of a 2 signal round-robin arbiter, these are the following scenarios that would arise. Am I missing anything?
Is your code (pasting it below) covering all of these scenarios?
module roundrobbin;
bit clk;
bit[1:0] req, grnt;
bit[3:0] r, g, grants;
ap_grnt1_after2: assert property(@(posedge clk)
req[1] && !grnt[1] && $fell(grnt[0]) |=> grnt[1]);
ap_grnt1_no2: assert property(@(posedge clk)
req[1] && $countones(grnt)==0 |=> grnt[1]);
endmodule