hw/ip/prim/rtl/prim_arbiter_ppc.sv Cov: 89.4%

   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: module prim_arbiter_ppc #(
  24:   parameter int unsigned N  = 4,
  25:   parameter int unsigned DW = 32
  26: ) (
  27:   input clk_i,
  28:   input rst_ni,
  29: 
  30:   input        [ N-1:0]        req_i,
  31:   input        [DW-1:0]        data_i [N],
  32:   output logic [ N-1:0]        gnt_o,
  33:   output logic [$clog2(N)-1:0] idx_o,
  34: 
  35:   output logic          valid_o,
  36:   output logic [DW-1:0] data_o,
  37:   input                 ready_i
  38: );
  39: 
  40:   `ASSERT_INIT(CheckNGreaterZero_A, N > 0)
  41: 
  42:   // this case is basically just a bypass
  43:   if (N == 1) begin : gen_degenerate_case
  44: 
  45:     assign valid_o  = req_i[0];
  46:     assign data_o   = data_i[0];
  47:     assign gnt_o[0] = valid_o & ready_i;
  48:     assign idx_o    = '0;
  49: 
  50:   end else begin : gen_normal_case
  51: 
  52:     logic [N-1:0] masked_req;
  53:     logic [N-1:0] ppc_out;
  54:     logic [N-1:0] arb_req;
  55:     logic [N-1:0] mask, mask_next;
  56:     logic [N-1:0] winner;
  57: 
  58:     assign masked_req = mask & req_i;
  59:     assign arb_req = (|masked_req) ? masked_req : req_i;
  60: 
  61:     // PPC
  62:     //   Even below code looks O(n) but DC optimizes it to O(log(N))
  63:     //   Using Parallel Prefix Computation
  64:     always_comb begin
  65:       ppc_out[0] = arb_req[0];
  66:       for (int i = 1 ; i < N ; i++) begin
  67:         ppc_out[i] = ppc_out[i-1] | arb_req[i];
  68:       end
  69:     end
  70: 
  71:     // Grant Generation: Leading-One detector
  72:     assign winner = ppc_out ^ {ppc_out[N-2:0], 1'b0};
  73:     assign gnt_o    = (ready_i) ? winner : '0;
  74: 
  75:     assign valid_o = |req_i;
  76:     // Mask Generation
  77:     assign mask_next = {ppc_out[N-2:0], 1'b0};
  78:     always_ff @(posedge clk_i or negedge rst_ni) begin
  79:       if (!rst_ni) begin
  80:         mask <= '0;
  81:       end else if (valid_o && ready_i) begin
  82:         // Latch only when requests accepted
  83:         mask <= mask_next;
  84:       end else if (valid_o && !ready_i) begin
  85:         // Downstream isn't yet ready so, keep current request alive. (First come first serve)
  86:         mask <= ppc_out;
  87:       end
  88:     end
  89: 
  90:     always_comb begin
  91:       data_o = '0;
  92:       idx_o  = '0;
  93:       for (int i = 0 ; i < N ; i++) begin
  94:         if (winner[i]) begin
  95:           data_o = data_i[i];
  96:           idx_o  = i;
  97:         end
  98:       end
  99:     end
 100: 
 101:   end
 102: 
 103:   ////////////////
 104:   // assertions //
 105:   ////////////////
 106: 
 107:   // we can only grant one requestor at a time
 108:   `ASSERT(CheckHotOne_A, $onehot0(gnt_o), clk_i, !rst_ni)
 109:   // A grant implies that the sink is ready
 110:   `ASSERT(GntImpliesReady_A, |gnt_o |-> ready_i, clk_i, !rst_ni)
 111:   // A grant implies that the arbiter asserts valid as well
 112:   `ASSERT(GntImpliesValid_A, |gnt_o |-> valid_o, clk_i, !rst_ni)
 113:   // A request and a sink that is ready imply a grant
 114:   `ASSERT(ReqAndReadyImplyGrant_A, |req_i && ready_i |-> |gnt_o, clk_i, !rst_ni)
 115:   // A request and a sink that is ready imply a grant
 116:   `ASSERT(ReqImpliesValid_A, |req_i |-> valid_o, clk_i, !rst_ni)
 117:   // Both conditions above combined and reversed
 118:   `ASSERT(ReadyAndValidImplyGrant_A, ready_i && valid_o |-> |gnt_o, clk_i, !rst_ni)
 119:   // Both conditions above combined and reversed
 120:   `ASSERT(NoReadyValidNoGrant_A, !(ready_i || valid_o) |-> gnt_o == 0, clk_i, !rst_ni)
 121:   // check index / grant correspond
 122:   `ASSERT(IndexIsCorrect_A, ready_i && valid_o |-> gnt_o[idx_o] && req_i[idx_o], clk_i, !rst_ni)
 123:   // data flow
 124:   `ASSERT(DataFlow_A, ready_i && valid_o |-> data_o == data_i[idx_o], clk_i, !rst_ni)
 125:   // KNOWN assertions on outputs, except for data as that may be partially X in simulation
 126:   // e.g. when used on a BUS
 127:   `ASSERT_KNOWN(ValidKnown_A, valid_o, clk_i, !rst_ni)
 128:   `ASSERT_KNOWN(GrantKnown_A, gnt_o, clk_i, !rst_ni)
 129:   `ASSERT_KNOWN(IdxKnown_A, idx_o, clk_i, !rst_ni)
 130: 
 131: `ifndef SYNTHESIS
 132:   // A grant implies a request
 133:   int unsigned k; // this is a symbolic variable
 134:   `ASSUME(KStable_M, ##1 $stable(k), clk_i, !rst_ni)
 135:   `ASSUME(KRange_M, k < N, clk_i, !rst_ni)
 136:   `ASSERT(GntImpliesReq_A, gnt_o[k] |-> req_i[k], clk_i, !rst_ni)
 137: 
 138:   // requests must stay asserted until they have been granted
 139:   `ASSUME(ReqStaysHighUntilGranted_M, (|req_i) && !ready_i |=>
 140:       (req_i & $past(req_i)) == $past(req_i), clk_i, !rst_ni)
 141:   // check that the arbitration decision is held if the sink is not ready
 142:   `ASSERT(LockArbDecision_A, |req_i && !ready_i |=> idx_o == $past(idx_o), clk_i, !rst_ni)
 143: 
 144: `endif
 145: 
 146: endmodule
 147: