../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: