Understanding Linear implementation of a round-robin arbiter

[promach]

Sorry , I will need to study figure 2.3 on my own then.

I am not doing any trolling here. Sorry again.
I am actually doing a personal research study on round-robin arbiter, hence what you meant by performance art.

[hamster_nz]

Sorry , I will need to study figure 2.3 on my own then.

I am not doing any trolling here. Sorry again.
I am actually doing a personal research study on round-robin arbiter, hence what you meant by performance art.

Sorry if I was a bit short - just wanted to say thanks because it got me to do my first FPGA project for a while, a 4-input Arbiter with two different modes:

http://hamsterworks.co.nz/mediawiki/index.php/Arbiter

[promach]

I have just formally verified the arbiter architecture (Figure 2.3) given in the thesis.

TODO :
1. Add more assert() formal coding for round-robin capability check
2. Investigate ways to reduce t_comb delay as described at the end of section 2.3 of the thesis
3. Includes the core ideas from Fast Arbiters for On-Chip Network Switches

Code: [Select]

// Credit : [url]https://www.eevblog.com/forum/fpga/understanding-linear-implementation-of-a-round-robin-arbiter/[/url]

module arbiter2 #(parameter WIDTH = 4) (clk, reset, req, grant);

input clk, reset;
input [WIDTH-1:0] req;
output [WIDTH-1:0] grant;

// 'grant' is one-hot vector, which means only one client request is granted/given green light to proceed
// note that 'base' is one-hot vector,
// 'base' signal helps round-robin arbiter to decide which 'req' to start servicing
reg [WIDTH-1:0] base;

always @(posedge clk)
begin
if(reset) base <= 1;

else base <= (grant[WIDTH-1]) ? 1 : (grant == 0) ? base : ( grant << 1 );
end

wire [WIDTH-1:0] priority_in;
wire [(WIDTH << 1)-1:0] priority_out; // the two leftmost significant bit are left unused

wire [WIDTH-1:0] granting = req & priority_in;
wire [WIDTH-2:0] approval; // we only have (WIDTH-1) block F

genvar index;
generate
for(index = 0; index < WIDTH; index = index + 1)
begin
if(index == WIDTH-1) assign grant[index] = (reset) ? 0 : granting[index];

else assign grant[index] = (reset) ? 0 : ( granting[index] | approval[index] );


if(index < (WIDTH-1)) assign approval[index] = ( priority_out[index+WIDTH-1] & req[index] );

if(index > 0) assign priority_in[index] = ( base[index] | priority_out[index-1] );

else assign priority_in[index] = base[index];
end
endgenerate


genvar priority_index;
generate
for(priority_index = 0; priority_index < (WIDTH << 1); priority_index = priority_index + 1)
begin : out_priority

if(priority_index < (WIDTH))
assign priority_out[priority_index] = (~req[priority_index]) & priority_in[priority_index];

else assign priority_out[priority_index] = (~req[priority_index-WIDTH]) & priority_out[priority_index-1];
end
endgenerate


`ifdef FORMAL

initial assume(reset);
initial assume(req == 0);  // only enable this assume() to test the cover() at line 100 properly

genvar grant_num;

generate
for(grant_num = 0; grant_num < WIDTH; grant_num = grant_num + 1)

always @(*) cover(first_clock_had_passed && grant[grant_num]);  // covers grants to each of the clients' request

endgenerate


reg [WIDTH-1:0] req_previous;
always @(posedge clk) req_previous <= req;

always @(posedge clk) cover(!$past(reset) && (grant == 0)); // covers the ability to go to an idle state

// covers the ability to handle requests properly even with ALL requests ON
always @(posedge clk) cover((&$past(req_previous)) && (&$past(req)) && (&req) && first_clock_had_passed && $past(first_clock_had_passed) && ((grant & $past(req)) == grant));


reg [WIDTH-1:0] grant_previous;
always @(posedge clk) grant_previous <= grant;

always @(posedge clk) cover(grant != grant_previous); // covers the ability to switch grants to any other requests

always @(posedge clk) cover(first_clock_had_passed && $past(first_clock_had_passed) && (&req) && (req_previous == 4'b1100) && ($past(req_previous) == 4'b1011)); // covers round-robin ability
`endif

`ifdef FORMAL

reg first_clock_had_passed;
initial first_clock_had_passed = 0;

always @(posedge clk) first_clock_had_passed <= 1;

// [url]https://graphics.stanford.edu/~seander/bithacks.html#DetermineIfPowerOf2[/url]
wire grant_is_one_hot = (grant != 0) && ((grant & (grant - 1)) == 0);
wire base_is_one_hot = (base != 0) && ((base & (base - 1)) == 0);

// assertions for round-robin capability
always @(*)
begin
if(reset) assert(grant == 0);

else begin
if (|req) assert(grant_is_one_hot);

else assert(grant == 0);
end
end

always @(posedge clk)
begin
if(first_clock_had_passed)
begin
// starts round-robin arbiter with req #0 getting prioritized first
if($past(reset)) assert(base == 1);

// 'grant' is a one-hot signal, but 'req' is not a one-hot signal
// 'base' is a one-hot signal which rotates
//  after the corresponding 'req' had been granted/given permission to proceed)
//  Rotation wraps around upon reaching MSB

else begin
assert(base == $past(grant[WIDTH-1]) ? 1 : ($past(grant) == 0) ? $past(base) : ($past(grant) << 1) );
assert(base_is_one_hot);
end
end
end

genvar f_index;
generate

for(f_index = 0; f_index < WIDTH; f_index = f_index + 1)
begin
always @(*)
begin
if(reset) assert( grant[f_index] == 0 );

else begin
if(f_index == WIDTH-1) assert( grant[f_index] == granting[f_index] );

else assert( grant[f_index] == ( granting[f_index] | approval[f_index] ) );
end

if(f_index < (WIDTH-1)) assert( approval[f_index] == ( priority_out[f_index+WIDTH-1] & req[f_index] ));

if(f_index > 0) assert( priority_in[f_index] == (base[f_index] | priority_out[f_index-1] ));

else assert( priority_in[f_index] == base[f_index] );
end
end

endgenerate


genvar f_priority_index;
generate

for(f_priority_index = 0; f_priority_index < (WIDTH << 1); f_priority_index = f_priority_index + 1)
begin : out_priority
always @(*)
begin
if(f_priority_index < (WIDTH))
assert( priority_out[f_priority_index] ==
((~req[f_priority_index]) & priority_in[f_priority_index]) );

else assert( priority_out[f_priority_index] ==
((~req[f_priority_index-WIDTH]) & priority_out[f_priority_index-1]) );
end
end

endgenerate

`endif

endmodule


[promach]

For Fast Arbiters for On-Chip Network Switches , what do you guys understand by GP and GR ?