forked from ChokaThenappan/Formal-Project
-
Notifications
You must be signed in to change notification settings - Fork 0
/
router_arbiter.sv
182 lines (154 loc) · 5.6 KB
/
router_arbiter.sv
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
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
// 4 inputs to 1 output router arbiter
//
// There is no delay from request to grant.
// The abriter assumes that the request remains stable while the entire
// packet is forwarded. Hence, priority is updated whenever a tail flit
// is forwarded. Grant is locked between a head flit and the corresponding
// tail flit.
//
// Interface
//
// * Inputs
// - clk: clock.
// - rst: active-high reset.
// - request: each bit should be set to 1 if there is a valid flit coming from the corresponding
// input port that needs to be routed to the output port arbitrated by this module.
// - forwarding_head: set to 1 to indicate the head flit of a new packet is being routed this cycle.
// The current grant gets locked until the tail flit is forwarded (wormhole routing)
// - forwarding_tail: set to 1 to indicate the tail flit of a packet is being routed this cycle.
// Priority is updated and grant is unlocked.
//
// * Outputs
// - grant: one-hot or zero. When grant[i] is set, request[i] is granted and the packet from the
// corresponding input port i can be routed.
// and the packet from the input
// - grant_valid: this flag indicates whether the current grant output is valid. When at least one
// request bit is set, the arbiter grants the next higher priority request with zero-cycles delay,
// unless grant is locked.
//
module router_arbiter
(
input logic clk,
input logic rst,
input logic [3:0] request,
input logic forwarding_head,
input logic forwarding_tail,
output logic [3:0] grant,
output logic grant_valid
);
logic grant_locked;
// Lock current grant for flit between head and tail, tail included
always_ff @(posedge clk) begin
if (rst) begin
grant_locked <= 1'b0;
end else begin
if (forwarding_tail) begin
grant_locked <= 1'b0;
end else if (forwarding_head) begin
grant_locked <= 1'b1;
end
end
end
assign grant_valid = |request & ~grant_locked;
// Update priority
typedef logic [3:0][3:0] priority_t;
priority_t priority_mask, priority_mask_next;
priority_t grant_stage1;
logic [3:0][1:0] grant_stage2;
// Higher priority is given to request[0] at reset
localparam priority_t InitialPriority = { 4'b0000, // request[3]
4'b1000, // request[2]
4'b1100, // request[1]
4'b1110 }; // request[0]
always_ff @(posedge clk) begin
if (rst) begin
priority_mask <= InitialPriority;
end else if (forwarding_tail) begin
priority_mask <= priority_mask_next;
end
end
always_comb begin
priority_mask_next = priority_mask;
unique case (grant)
4'b0001 : begin
priority_mask_next[0] = '0;
priority_mask_next[1][0] = 1'b1;
priority_mask_next[2][0] = 1'b1;
priority_mask_next[3][0] = 1'b1;
end
4'b0010 : begin
priority_mask_next[1] = '0;
priority_mask_next[0][1] = 1'b1;
priority_mask_next[2][1] = 1'b1;
priority_mask_next[3][1] = 1'b1;
end
4'b0100 : begin
priority_mask_next[2] = '0;
priority_mask_next[0][2] = 1'b1;
priority_mask_next[1][2] = 1'b1;
priority_mask_next[3][2] = 1'b1;
end
4'b1000 : begin
priority_mask_next[3] = '0;
priority_mask_next[0][3] = 1'b1;
priority_mask_next[1][3] = 1'b1;
priority_mask_next[2][3] = 1'b1;
end
default begin
end
endcase
end
genvar g_i, g_j;
for (g_i = 0; g_i < 4; g_i++) begin : gen_grant
for (g_j = 0; g_j < 4; g_j++) begin : gen_grant_stage1
assign grant_stage1[g_i][g_j] = request[g_j] & priority_mask[g_j][g_i];
end
for (g_j = 0; g_j < 2; g_j++) begin : gen_grant_stage2
assign grant_stage2[g_i][g_j] = ~(grant_stage1[g_i][2*g_j] | grant_stage1[g_i][2*g_j + 1]);
end
assign grant[g_i] = &grant_stage2[g_i] & request[g_i];
end // gen_grant
//
// Assertions
//
`ifndef SYNTHESIS
// pragma coverage off
//VCS coverage off
a_grant_onehot: assert property (@(posedge clk) disable iff(rst) $onehot0(grant))
else $error("Fail: a_grant_onehot"); // Proven in JG
//1
a_no_request_no_grant: assert property (@(posedge clk) disable iff(rst)
(request == 4'b000) |-> (grant == 4'b0000))
else $error("Fail: a_no_request_no_grant"); // Proven in JG
//2
a_grant_lock_zero: assert property (@(posedge clk) disable iff(rst)
(grant_locked == 0) |-> ($onehot0(grant)))
else $error("Fail: a_grant_lock_zero"); // Proven in JG
//3
a_stable_priority: assert property (@(posedge clk) disable iff(rst)
(grant_locked == 0) |-> $stable(priority_mask))
else $error("Fail: a_stable_priority"); // Fails
//4
a_grant_valid: assert property (@(posedge clk) disable iff(rst)
(!grant_locked && |request |-> grant_valid))
else $error("Fail: a_grant_valid"); // Proven in JG
//5
a_grant_unlocked: assert property (@(posedge clk) disable iff(rst)
(!grant_locked && forwarding_head |=> grant_locked))
else $error("Fail: a_grant_unlocked"); //Fails
//6
a_grant_locked: assert property (@(posedge clk) disable iff(rst)
(grant_locked && forwarding_tail |=> !grant_locked))
else $error("Fail: a_grant_locked"); //Proven in JG
//7
a_priority_changed: assert property (@(posedge clk) disable iff(rst)
(grant_locked |=> $changed(priority_mask)))
else $error("Fail: a_priority_changed"); //Fails
//8
a_one_input_one_output: assert property (@(posedge clk) disable iff(rst)
($countones(grant) <= 1))
else $error("Fail: a_one_input_one_output"); //Proven in JG
// pragma coverage on
//VCS coverage on
`endif // ~SYNTHESIS
endmodule