../src/lowrisc_prim_all_0.1/rtl/prim_arbiter_tree.sv Cov: 74.7%
1: // Copyright lowRISC contributors.
2: // Licensed under the Apache License, Version 2.0, see LICENSE for details.
3: // SPDX-License-Identifier: Apache-2.0
4: //
5: // N:1 arbiter module
6: //
7: // Verilog parameter
8: // N: Number of request ports
9: // DW: Data width
10: // Lock: Lock arbiter decision when destination is not ready
11: //
12: // Hand optimized version which implements a binary tree to optimize
13: // timing. In particular, arbitration decisions and data mux steering happen
14: // simultaneously on the corresponding tree level, which leads to improved propagation
15: // delay compared to a solution that arbitrates first, followed by a data mux selection.
16: //
17: // If Lock is turned on, the currently winning request is held if the
18: // data sink is not ready. This behavior is required by some interconnect
19: // protocols (AXI, TL), and hence it is turned on by default.
20: // Note that this implies that an asserted request must stay asserted
21: // until it has been granted.
22: //
23: // See also: prim_arbiter_ppc
24:
25: `include "prim_assert.sv"
26:
27: module prim_arbiter_tree #(
28: parameter int unsigned N = 4,
29: parameter int unsigned DW = 32,
30: // holds the last arbiter decision in case the sink is not ready
31: // this should be enabled when used in AXI or TL protocols.
32: parameter bit Lock = 1'b1
33: ) (
34: input clk_i,
35: input rst_ni,
36:
37: input [ N-1:0] req_i,
38: input [DW-1:0] data_i [N],
39: output logic [ N-1:0] gnt_o,
40: output logic [$clog2(N)-1:0] idx_o,
41:
42: output logic valid_o,
43: output logic [DW-1:0] data_o,
44: input ready_i
45: );
46:
47: `ASSERT_INIT(CheckNGreaterZero_A, N > 0)
48:
49: // this case is basically just a bypass
50: if (N == 1) begin : gen_degenerate_case
51:
52: assign valid_o = req_i[0];
53: assign data_o = data_i[0];
54: assign gnt_o[0] = valid_o & ready_i;
55: assign idx_o = '0;
56:
57: end else begin : gen_normal_case
58:
59: // align to powers of 2 for simplicity
60: // a full binary tree with N levels has 2**N + 2**N-1 nodes
61: localparam int unsigned NumLevels = $clog2(N);
62: logic [N-1:0] req;
63: logic [2**(NumLevels+1)-2:0] req_tree;
64: logic [2**(NumLevels+1)-2:0] gnt_tree;
65: logic [2**(NumLevels+1)-2:0][NumLevels-1:0] idx_tree;
66: logic [2**(NumLevels+1)-2:0][DW-1:0] data_tree;
67: logic [NumLevels-1:0] rr_q;
68:
69: // req_locked
70: if (Lock) begin : gen_lock
71: logic [N-1:0] mask_d, mask_q;
72: // if the request cannot be served, we store the current request bits
73: // and apply it as a mask to the incoming requests in the next cycle.
74: assign mask_d = (valid_o && (!ready_i)) ? req : {N{1'b1}};
75: assign req = mask_q & req_i;
76:
77: always_ff @(posedge clk_i) begin : p_lock_regs
78: if (!rst_ni) begin
79: mask_q <= {N{1'b1}};
80: end else begin
81: mask_q <= mask_d;
82: end
83: end
84: end else begin : gen_no_lock
85: assign req = req_i;
86: end
87:
88: for (genvar level = 0; level < NumLevels+1; level++) begin : gen_tree
89: //
90: // level+1 C0 C1 <- "Base1" points to the first node on "level+1",
91: // \ / these nodes are the children of the nodes one level below
92: // level Pa <- "Base0", points to the first node on "level",
93: // these nodes are the parents of the nodes one level above
94: //
95: // hence we have the following indices for the Pa, C0, C1 nodes:
96: // Pa = 2**level - 1 + offset = Base0 + offset
97: // C0 = 2**(level+1) - 1 + 2*offset = Base1 + 2*offset
98: // C1 = 2**(level+1) - 1 + 2*offset + 1 = Base1 + 2*offset + 1
99: //
100: localparam int unsigned Base0 = (2**level)-1;
101: localparam int unsigned Base1 = (2**(level+1))-1;
102:
103: for (genvar offset = 0; offset < 2**level; offset++) begin : gen_level
104: localparam int unsigned Pa = Base0 + offset;
105: localparam int unsigned C0 = Base1 + 2*offset;
106: localparam int unsigned C1 = Base1 + 2*offset + 1;
107:
108: // this assigns the gated interrupt source signals, their
109: // corresponding IDs and priorities to the tree leafs
110: if (level == NumLevels) begin : gen_leafs
111: if (offset < N) begin : gen_assign
112: // forward path
113: assign req_tree[Pa] = req[offset];
114: assign idx_tree[Pa] = offset;
115: assign data_tree[Pa] = data_i[offset];
116: // backward (grant) path
117: assign gnt_o[offset] = gnt_tree[Pa];
118: end else begin : gen_tie_off
119: // forward path
120: assign req_tree[Pa] = '0;
121: assign idx_tree[Pa] = '0;
122: assign data_tree[Pa] = '0;
123: end
124: // this creates the node assignments
125: end else begin : gen_nodes
126: // NOTE: the code below has been written in this way in order to work
127: // around a synthesis issue in Vivado 2018.3 and 2019.2 where the whole
128: // module would be optimized away if these assign statements contained
129: // ternary statements to implement the muxes.
130: //
131: // TODO: rewrite these lines with ternary statmements onec the problem
132: // has been fixed in the tool.
133: //
134: // See also originating issue:
135: // https://github.com/lowRISC/opentitan/issues/1355
136: // Xilinx issue:
137: // https://forums.xilinx.com/t5/Synthesis/Simulation-Synthesis-Mismatch-with-Vivado-2018-3/m-p/1065923#M33849
138:
139: // forward path
140: logic sel; // local helper variable
141: // this performs a (local) round robin arbitration using the associated rr counter bit
142: assign sel = ~req_tree[C0] | req_tree[C1] & rr_q[NumLevels-1-level];
143: // propagate requests
144: assign req_tree[Pa] = req_tree[C0] | req_tree[C1];
145: // muxes
146: assign idx_tree[Pa] = ({NumLevels{sel}} & idx_tree[C1]) |
147: ({NumLevels{~sel}} & idx_tree[C0]);
148: assign data_tree[Pa] = ({DW{sel}} & data_tree[C1]) |
149: ({DW{~sel}} & data_tree[C0]);
150: // backward (grant) path
151: assign gnt_tree[C0] = gnt_tree[Pa] & ~sel;
152: assign gnt_tree[C1] = gnt_tree[Pa] & sel;
153: end
154: end : gen_level
155: end : gen_tree
156:
157: // the results can be found at the tree root
158: assign idx_o = idx_tree[0];
159: assign data_o = data_tree[0];
160: assign valid_o = req_tree[0];
161: // propagate the grant back to the requestors
162: assign gnt_tree[0] = valid_o & ready_i;
163:
164: // this is the round robin counter
165: always_ff @(posedge clk_i or negedge rst_ni) begin : p_regs
166: if (!rst_ni) begin
167: rr_q <= '0;
168: end else begin
169: if (gnt_tree[0] && (rr_q == N-1)) begin
170: rr_q <= '0;
171: end else if (gnt_tree[0]) begin
172: rr_q <= rr_q + 1'b1;
173: end
174: end
175: end
176:
177: end
178:
179: ////////////////
180: // assertions //
181: ////////////////
182:
183: // we can only grant one requestor at a time
184: `ASSERT(CheckHotOne_A, $onehot0(gnt_o))
185: // A grant implies that the sink is ready
186: `ASSERT(GntImpliesReady_A, |gnt_o |-> ready_i)
187: // A grant implies that the arbiter asserts valid as well
188: `ASSERT(GntImpliesValid_A, |gnt_o |-> valid_o)
189: // A request and a sink that is ready imply a grant
190: `ASSERT(ReqAndReadyImplyGrant_A, |req_i && ready_i |-> |gnt_o)
191: // A request and a sink that is ready imply a grant
192: `ASSERT(ReqImpliesValid_A, |req_i |-> valid_o)
193: // Both conditions above combined and reversed
194: `ASSERT(ReadyAndValidImplyGrant_A, ready_i && valid_o |-> |gnt_o)
195: // Both conditions above combined and reversed
196: `ASSERT(NoReadyValidNoGrant_A, !(ready_i || valid_o) |-> gnt_o == 0)
197: // check index / grant correspond
198: `ASSERT(IndexIsCorrect_A, ready_i && valid_o |-> gnt_o[idx_o] && req_i[idx_o])
199: // data flow
200: `ASSERT(DataFlow_A, ready_i && valid_o |-> data_o == data_i[idx_o])
201: // KNOWN assertions on outputs, except for data as that may be partially X in simulation
202: // e.g. when used on a BUS
203: `ASSERT_KNOWN(ValidKnown_A, valid_o)
204: `ASSERT_KNOWN(GrantKnown_A, gnt_o)
205: `ASSERT_KNOWN(IdxKnown_A, idx_o)
206:
207: `ifndef SYNTHESIS
208: // A grant implies a request
209: int unsigned k; // this is a symbolic variable
210: `ASSUME(KStable_M, ##1 $stable(k), clk_i, !rst_ni)
211: `ASSUME(KRange_M, k < N, clk_i, !rst_ni)
212: `ASSERT(GntImpliesReq_A, gnt_o[k] |-> req_i[k])
213:
214: if (Lock) begin : gen_lock_assertion
215: // requests must stay asserted until they have been granted
216: `ASSUME(ReqStaysHighUntilGranted_M, (|req_i) && !ready_i |=>
217: (req_i & $past(req_i)) == $past(req_i), clk_i, !rst_ni)
218: // check that the arbitration decision is held if the sink is not ready
219: `ASSERT(LockArbDecision_A, |req_i && !ready_i |=> idx_o == $past(idx_o))
220: end
221:
222: `endif
223:
224: endmodule
225: