Understanding Linear implementation of a round-robin arbiter

Code Verilog - [expand]
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
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 <= (base[WIDTH-1]) ? 1 : (grant == 0) ? 1 : (grant << 1);
end
 
wire [WIDTH-1:0] priority_in;
reg [WIDTH-1:0] priority_out;
 
genvar index;
generate
    for(index = 0; index < WIDTH; index = index + 1)
    begin
        if(index > 0) assign priority_in[index] = base[index] | priority_out[index-1];
 
        else assign priority_in[index] = base[index] | priority_out[WIDTH-1];
    end
endgenerate
 
assign grant = (reset) ? 1 : req & priority_in;
 
always @(posedge clk) priority_out <= (~req) & priority_in;
 
`ifdef FORMAL
initial assume(reset);
 
reg first_clock_had_passed;
initial first_clock_had_passed = 0;
 
always @(posedge clk) first_clock_had_passed <= 1;
always @(posedge clk) if(first_clock_had_passed && $past(first_clock_had_passed) && $past(first_clock_had_passed, 2) && $past(first_clock_had_passed, 3)) assume(&req); // ALL requests ON
 
// covers the ability to handle requests properly even with ALL requests ON
always @(posedge clk) cover(first_clock_had_passed); 
`endif
 
endmodule