Round-Robin Arbiter Architecture from Efficient microarchitecture for network-on-chip

[promach]

I have formally verified a round-robin arbiter code

Could anyone advise about the various methods of minimizing the combinational delay tcomb penalty mentioned at the end of section 2.3 of Efficient microarchitecture for network-on-chip routers ?


arbiter.v

---

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
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
// Credit : [url]https://www.eevblog.com/forum/fpga/understanding-linear-implementation-of-a-round-robin-arbiter/[/url]
 
module arbiter #(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 multiple_requests = (req != 0) && !((req & (req - 1)) == 0);
wire grant_is_one_hot = (grant != 0) && ((grant & (grant - 1)) == 0);
 
always @(*)
begin
    if(reset) assert(grant == 0);
 
    else begin
 
        if (|req) assert(grant_is_one_hot);
 
        else assert(grant == 0);
 
 
        // assertions for round-robin capability
 
        if((req == req_previous) && multiple_requests) 
        // it is possible that the same client files request again after being serviced
            assert((grant & req) != grant_previous); 
    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 != 0);
        end
    end
end
 
`endif
 
endmodule

---

arbiter.sby

[tasks]
proof
cover

[options]
proof: mode prove
proof: depth 10

cover: mode cover
cover: depth 20
cover: append 8

[engines]
smtbmc yices
# smtbmc boolector
# abc pdr
# aiger avy
# aiger suprove

[script]
read_verilog -formal -sv arbiter.v
prep -top arbiter

[files]
arbiter.v

 

[ads-ee]

They author is discussing using parallel pre-fix sum type networks to compute the priority. See this wiki page.

 

[promach]

in practice, the associated delay penalty can be minimized by computing the intermediate grant signals for the block of R -type cells and the block of F -type cells in parallel and conditionally selecting either set of grants based on the value of the first block’s final priority output.

As in the case of fixed-priority arbitration, we can further improve delay by replacing the blocks of R-type and F-type cells with prefix networks.

Thanks for the wikipedia link. However, I am in the dark on how prefix sum could actually replace blocks F and R ?