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