../src/lowrisc_prim_all_0.1/rtl/prim_arbiter_ppc.sv Cov: 87.5%
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: //
11: // This is the original implementation of the arbiter which relies on parallel prefix
12: // computing optimization to optimize the request / arbiter tree. Not all synthesis tools
13: // may support this.
14: //
15: // Note that the currently winning request is held if the data sink is not ready.
16: // This behavior is required by some interconnect protocols (AXI, TL). Note that
17: // this implies that an asserted request must stay asserted
18: // until it has been granted. Note that for PPC, this option cannot
19: // be disabled.
20: //
21: // See also: prim_arbiter_tree
22:
23: `include "prim_assert.sv"
24:
25: module prim_arbiter_ppc #(
26: parameter int unsigned N = 4,
27: parameter int unsigned DW = 32,
28:
29: // Configurations
30: // EnDataPort: {0, 1}, if 0, input data will be ignored
31: parameter int EnDataPort = 1,
32:
33: // Derived parameters
34: localparam int unsigned IdxW = $clog2(N)
35: ) (
36: input clk_i,
37: input rst_ni,
38:
39: input [ N-1:0] req_i,
40: input [DW-1:0] data_i [N],
41: output logic [ N-1:0] gnt_o,
42: output logic [IdxW-1:0] idx_o,
43:
44: output logic valid_o,
45: output logic [DW-1:0] data_o,
46: input ready_i
47: );
48:
49: `ASSERT_INIT(CheckNGreaterZero_A, N > 0)
50:
51: // this case is basically just a bypass
52: if (N == 1) begin : gen_degenerate_case
53:
54: assign valid_o = req_i[0];
55: assign data_o = data_i[0];
56: assign gnt_o[0] = valid_o & ready_i;
57: assign idx_o = '0;
58:
59: end else begin : gen_normal_case
60:
61: logic [N-1:0] masked_req;
62: logic [N-1:0] ppc_out;
63: logic [N-1:0] arb_req;
64: logic [N-1:0] mask, mask_next;
65: logic [N-1:0] winner;
66:
67: assign masked_req = mask & req_i;
68: assign arb_req = (|masked_req) ? masked_req : req_i;
69:
70: // PPC
71: // Even below code looks O(n) but DC optimizes it to O(log(N))
72: // Using Parallel Prefix Computation
73: always_comb begin
74: ppc_out[0] = arb_req[0];
75: for (int i = 1 ; i < N ; i++) begin
76: ppc_out[i] = ppc_out[i-1] | arb_req[i];
77: end
78: end
79:
80: // Grant Generation: Leading-One detector
81: assign winner = ppc_out ^ {ppc_out[N-2:0], 1'b0};
82: assign gnt_o = (ready_i) ? winner : '0;
83:
84: assign valid_o = |req_i;
85: // Mask Generation
86: assign mask_next = {ppc_out[N-2:0], 1'b0};
87: always_ff @(posedge clk_i or negedge rst_ni) begin
88: if (!rst_ni) begin
89: mask <= '0;
90: end else if (valid_o && ready_i) begin
91: // Latch only when requests accepted
92: mask <= mask_next;
93: end else if (valid_o && !ready_i) begin
94: // Downstream isn't yet ready so, keep current request alive. (First come first serve)
95: mask <= ppc_out;
96: end
97: end
98:
99: if (EnDataPort == 1) begin: gen_datapath
100: always_comb begin
101: data_o = '0;
102: for (int i = 0 ; i < N ; i++) begin
103: if (winner[i]) begin
104: data_o = data_i[i];
105: end
106: end
107: end
108: end else begin: gen_nodatapath
109: assign data_o = '1;
110: // TODO: waive data_i from NOT_READ error
111: end
112:
113: always_comb begin
114: idx_o = '0;
115: for (int i = 0 ; i < N ; i++) begin
116: if (winner[i]) begin
117: idx_o = i[IdxW-1:0];
118: end
119: end
120: end
121:
122: ////////////////
123: // assertions //
124: ////////////////
125: // grant shall be higher index than prev. unless no higher requests exist
126: `ASSERT(RoundRobin_A, valid_o && ready_i && $past(ready_i) && $past(valid_o) &&
127: |(masked_req) |-> idx_o > $past(idx_o))
128:
129: end
130:
131: ////////////////
132: // assertions //
133: ////////////////
134:
135: // we can only grant one requestor at a time
136: `ASSERT(CheckHotOne_A, $onehot0(gnt_o))
137: // A grant implies that the sink is ready
138: `ASSERT(GntImpliesReady_A, |gnt_o |-> ready_i)
139: // A grant implies that the arbiter asserts valid as well
140: `ASSERT(GntImpliesValid_A, |gnt_o |-> valid_o)
141: // A request and a sink that is ready imply a grant
142: `ASSERT(ReqAndReadyImplyGrant_A, |req_i && ready_i |-> |gnt_o)
143: // A request and a sink that is ready imply a grant
144: `ASSERT(ReqImpliesValid_A, |req_i |-> valid_o)
145: // Both conditions above combined and reversed
146: `ASSERT(ReadyAndValidImplyGrant_A, ready_i && valid_o |-> |gnt_o)
147: // Both conditions above combined and reversed
148: `ASSERT(NoReadyValidNoGrant_A, !(ready_i || valid_o) |-> gnt_o == 0)
149: // check index / grant correspond
150: `ASSERT(IndexIsCorrect_A, ready_i && valid_o |-> gnt_o[idx_o] && req_i[idx_o])
151: // data flow
152: `ASSERT(DataFlow_A, ready_i && valid_o |-> data_o == data_i[idx_o])
153: // KNOWN assertions on outputs, except for data as that may be partially X in simulation
154: // e.g. when used on a BUS
155: `ASSERT_KNOWN(ValidKnown_A, valid_o)
156: `ASSERT_KNOWN(GrantKnown_A, gnt_o)
157: `ASSERT_KNOWN(IdxKnown_A, idx_o)
158:
159: `ifndef SYNTHESIS
160: // A grant implies a request
161: int unsigned k; // this is a symbolic variable
162: `ASSUME(KStable_M, ##1 $stable(k), clk_i, !rst_ni)
163: `ASSUME(KRange_M, k < N, clk_i, !rst_ni)
164: `ASSERT(GntImpliesReq_A, gnt_o[k] |-> req_i[k])
165:
166: // requests must stay asserted until they have been granted
167: `ASSUME(ReqStaysHighUntilGranted_M, (|req_i) && !ready_i |=>
168: (req_i & $past(req_i)) == $past(req_i))
169: // check that the arbitration decision is held if the sink is not ready
170: `ASSERT(LockArbDecision_A, |req_i && !ready_i |=> idx_o == $past(idx_o))
171:
172: `endif
173:
174: endmodule
175: