Are are any standard or recommended ways of verifying the functionality of the round-robin arbiter and more specifically checking the fairness?
I’m looking for something that is scalable with the number of requestors.
PS: Assume, the request and grant is asserted on the same cycle
In reply to imajeeth:
Are are any standard or recommended ways of verifying the functionality of the round-robin arbiter and more specifically checking the fairness?
I’m looking for something that is scalable with the number of requestors.
PS: Assume, the request and grant is asserted on the same cycle
I faced this issue before. As far as I know, there is no standard ways to verify round-robin arbiter. Depend on your specification, it would be from simple (using about 3 properties or something like that) to more complicated (I myself used a function with “global” variables).
In reply to hanhha:
This is my solution. Not necessarily the best one. Suggestions for improvements are welcome.
/*
Assume there are 3 requestors namely: A,B and C with reqA, reqB and reqC being the requests
and gntA, gntB and gntC being the grants.
Assumes the request and grant are on the same cycle
Similar sequence and assertions need to be replicated for each requestor. Can concatenate the requests and grants
into a bit vector, in order to save some redundant code
*/
//Denotes there is request and grant for the requestor A. Does not care about other requestors
logic requestorA_req_and_gnt;
//Denotes there is request and grant for requestor A and there is atleast one other requestor active
logic requestorA_req_and_gnt_with_other_requestors_active;
//There are requests other than requestor A
logic other_req_except_requestorA;
//There are grants other than requestor A
logic other_gnt_except_requestorA;
assign other_req_except_requestorA = reqB | reqC; //High when any one of the other requestor's are active
assign other_gnt_except_requestorA = gntB | gntC;
assign requestorA_req_and_gnt = reqA & gntA;
assign requestorA_req_and_gnt_with_other_requestors_active = reqA && other_req_except_requestorA && gntA;
//-----------------------------------------------------------------------------------------------------------------------------------------------
// Covers the case where there is request and grant on one cycle for requestorA, followed by no other requests. And then few cycles later there
// are multiple requests(reqA and atleast one other request). In this case, requestorA should NOT be granted again
//-----------------------------------------------------------------------------------------------------------------------------------------------
sequence requestorA_req_and_gnt_followed_by_other_req_seq;
requestorA_req_and_gnt ##0 (!other_req_except_requestorA)[*1:$] ##1 reqA && other_req_except_requestorA;
endsequence
//-----------------------------------------------------------------------------------------------------------------------------------------------
//Covers the case where there are more than one requestor active(reqA and any one of the other requests) followed by cycles of no other request at all
// and again followed by more than one requestor active. First time during multiple requests, reqA is granted, so, the second time when multiple
// requests are active, gntA should not be asserted again, and one of the other requests should be granted
//-----------------------------------------------------------------------------------------------------------------------------------------------
sequence multiple_requests_with_requestorA_req_and_gnt_followed_by_other_req_seq;
requestorA_req_and_gnt_with_other_requestors_active ##1 (!other_req_except_requestorA)[*0:$] ##1 reqA && other_req_except_requestorA;
endsequence
//-----------------------------------------------------------------------------------------------------------------------------------------------
//Covers the case where there are multiple requestors active in one cycle and next cycle may or may not have reqA, but will have other requests.
// If reqA is granted in the previous cycle, it should not be granted again in the next cycle, rather other requestor should be granted
//-----------------------------------------------------------------------------------------------------------------------------------------------
sequence back_to_back_multiple_requests_active_with_requestorA_gnted_followed_by_other_req_seq;
requestorA_req_and_gnt_with_other_requestors_active ##1 other_req_except_requestorA;
endsequence
//-----------------------------------------------------------------------------------------------------------------------------------------------
//Assertion to check if reqA do not hog the round robin arbiter
//-----------------------------------------------------------------------------------------------------------------------------------------------
assert_fairness_wrt_requestorA: assert property( @(posedge clk) disable iff(!resetn)
(requestorA_req_and_gnt_followed_by_other_req_and_no_bts_seq or
multiple_requests_with_requestorA_req_and_gnt_followed_by_other_req_and_no_bts_seq or
back_to_back_multiple_requests_active_with_requestorA_gnted_followed_by_other_req_and_no_bts_seq
) |-> other_gnt_except_requestorA && !gntA
)
`uvm_info("ARB_ASSERT",$sformatf("Requestor A was previously granted, and not granted again, round robin scheme followed!"),UVM_LOW)
else
`uvm_error("ARB_ASSERT_ERR",$sformatf("Requestor A was previously granted, and gets granted again, round robin scheme not followed"))
In reply to imajeeth:
I think this is not a scalable solution. In my case, there were 16 requestors. Here was my approach:
1 - Assume that req[15:0] and gnt[15:0] is vector of request and grant signals.
2 - Check these properties:
a - $onehot0(gnt)
b - gnt [i] |-> req [i] in which i was generated by “generate” statement from 0 to 15 for all requestors.
c - Developed a function called rr_scheme in which updated the “pivot” (if req[i] & gnt[i] then pivot = i) and returned the expected gnt vector (in my case, expected gnt = the very first req[i] with i > pivot or very first req[i] from req[0] if there was no req[i] with i > pivot). The last assertion compared gnt with rr_scheme returned.
Sorry that I don’t have the code right now.
In reply to imajeeth:
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[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;
)
In reply to MLearner:
If you wanted to formally verify a rr arbiter with any number of requestors, then you don’t need to model it like above.
Instead, you can define ‘fairness’ across any 2 requestors. You let the fv tool choose any 2 random requestors. Intuitively I feel that any fairness bug can be reproduced by a failing trace using 2 requestors. So my simple-minded solution would be to use the assertion as described by Harry Foster
p_fairness: assert property(@(posedge clk) disable iff (reset)
not(req1 ##1(!gnt1 throughout gnt2[->2])));
In reply to MLearner:
Why we need to use genvar her and not simple for loop. what happen if we use simple for loop?
In reply to Himanshu m soni:
The generate-for loop is being used to instantiate multiple assert directives. This is not procedural code.