hw/ip/prim/rtl/prim_arbiter_tree.sv Cov: 82.9%

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