Memory Controllers in SoCs

   the two promises, stated precisely

   upstream : "I will complete your request correctly, in an order
               your protocol permits. I will not tell you when."

   downstream: "Every command I issue is legal given this device's
               state and timing. I will not tell you whose request
               it is."

   the controller's whole job is that NEITHER PROMISE MENTIONS THE
   OTHER SIDE. Upstream has no vocabulary for a bank; downstream has
   no vocabulary for a requester. The adapter must satisfy both
   using state that only it holds.

   a concrete composition failure, ILLUSTRATIVE

   source QoS gives the CPU class 70% of queue ENTRIES.
   the scheduler optimises for ROW HITS among queued requests.

   the CPU's stream is scattered  -> few row hits among its entries
   the DMA's stream is sequential -> many row hits among its entries

   the scheduler, seeing both queues, finds most of its row hits in
   the DMA's requests. It serves them preferentially -- not because
   of priority, but because they are the ones that are cheap.

   result: the CPU class holds 70% of the ENTRIES and receives far
   less than 70% of the SERVICE.

   neither layer is broken. Source QoS allocated entries as
   configured. The scheduler maximised throughput as configured.
   The COMPOSITION delivered something nobody specified.

// ---------------------------------------------------------------------
// source_qos_arbiter -- CLASSIFICATION: synthesisable, ILLUSTRATIVE.
//
// WHAT IT DOES: §4's TOP-ROW arbitration -- which SOURCE proceeds.
// Weighted service with a hard age bound, plus per-source measurement
// of service actually delivered.
//
// WHY AN AGE BOUND AND NOT STRICT PRIORITY (§6): strict priority
// starves, and starvation is the EXPECTED behaviour under sustained
// load rather than a corner case. The age bound converts an unbounded
// wait into a provable limit -- which is the same argument 17.4 makes
// for its bounded bypass at the command layer, applied here at the
// source layer.
//
// WHY IT MEASURES SERVICE (§7): allocating opportunity is not
// allocating service. The conversion rate depends on each source's own
// locality, which this layer cannot see. So the honest output is a
// measurement, not an assumption.
//
// WHAT IT IS NOT: the command scheduler. It has no bank state, no
// timing state and no row state, and it must not: 17.4 owns command
// arbitration and its legality/policy separation.
//
// SYNTHESIS: per-source counters, a priority encoder, one comparator
// chain. No memory.
// ---------------------------------------------------------------------
module source_qos_arbiter #(
  parameter int SOURCES  = 4,
  parameter int WEIGHT_W = 4,
  parameter int AGE_W    = 10,
  parameter int AGE_MAX  = 256   // the starvation bound, in grant cycles
)(
  input  logic                       clk,
  input  logic                       rst_n,

  input  logic [SOURCES-1:0]         req,             // per-source request
  input  logic [WEIGHT_W-1:0]        weight [SOURCES],// configured share
  input  logic                       downstream_ready,// queues can accept

  output logic [SOURCES-1:0]         grant,           // exactly one, or none
  output logic                       grant_valid,

  // ---- published measurement, §7
  output logic [31:0]                served   [SOURCES],
  output logic [AGE_W-1:0]           age      [SOURCES],
  output logic [AGE_W-1:0]           max_age  [SOURCES],
  output logic [15:0]                age_forced,      // grants forced by the bound
  output logic [15:0]                starvation_events
);
  // SOURCES of 1 makes $clog2 zero and the grant vector degenerate; a
  // one-source arbiter is also not an arbiter. AGE_MAX must fit in
  // AGE_W or the bound can never be reached and the guarantee is void
  // -- COUNT versus INDEX applied to a threshold.
  initial begin
    if (SOURCES  < 2) $fatal(1, "source_qos_arbiter: SOURCES must be >= 2 (got %0d)", SOURCES);
    if (WEIGHT_W < 1) $fatal(1, "source_qos_arbiter: WEIGHT_W must be >= 1");
    if (AGE_W    < 2) $fatal(1, "source_qos_arbiter: AGE_W must be >= 2");
    if (AGE_MAX  < 1) $fatal(1, "source_qos_arbiter: AGE_MAX must be >= 1");
    if (AGE_MAX >= (1 << AGE_W))
      $fatal(1, "source_qos_arbiter: AGE_MAX %0d unreachable in AGE_W %0d bits", AGE_MAX, AGE_W);
  end

  // Credits implement the weighted share. A source spends a credit when
  // granted and all credits are replenished when every requesting
  // source is out -- which keeps the ratio without needing division.
  logic [WEIGHT_W:0] credit [SOURCES];

  logic [SOURCES-1:0] eligible;     // requesting and holding a credit
  logic [SOURCES-1:0] forced;       // requesting and at the age bound
  logic               any_forced, any_eligible;

  always_comb begin
    for (int s = 0; s < SOURCES; s++) begin
      eligible[s] = req[s] && (credit[s] != '0);
      forced[s]   = req[s] && (age[s] >= AGE_MAX[AGE_W-1:0]);
    end
    any_forced   = |forced;
    any_eligible = |eligible;
  end

  // Grant selection. The age bound OUTRANKS the weighted share: a
  // source at its bound is granted even with no credit, which is what
  // makes the bound a guarantee rather than a preference. Within each
  // group the lowest index wins -- a fixed order, which is acceptable
  // ONLY because the age bound prevents indefinite loss. Without the
  // bound this would be strict priority and §6 explains why that is a
  // bug.
  logic [SOURCES-1:0] sel;
  always_comb begin
    sel = '0;
    if (downstream_ready) begin
      if (any_forced) begin
        for (int s = 0; s < SOURCES; s++)
          if (forced[s] && sel == '0) sel[s] = 1'b1;
      end else if (any_eligible) begin
        for (int s = 0; s < SOURCES; s++)
          if (eligible[s] && sel == '0) sel[s] = 1'b1;
      end
    end
  end

  assign grant       = sel;
  assign grant_valid = |sel;

  always_ff @(posedge clk) begin
    if (!rst_n) begin
      age_forced        <= '0;
      starvation_events <= '0;
      for (int s = 0; s < SOURCES; s++) begin
        credit[s]  <= '0;
        served[s]  <= '0;
        age[s]     <= '0;
        max_age[s] <= '0;
      end
    end else begin
      // ---- replenish when no requesting source has a credit left.
      // Computed from the PRE-grant credits so a grant this cycle does
      // not trigger a replenish in the same cycle -- which would make
      // the weights meaningless by refilling constantly.
      if (!any_eligible && |req) begin
        for (int s = 0; s < SOURCES; s++)
          credit[s] <= {1'b0, weight[s]};
      end else if (grant_valid) begin
        for (int s = 0; s < SOURCES; s++)
          if (sel[s] && credit[s] != '0) credit[s] <= credit[s] - 1'b1;
      end

      // ---- age: a requesting, ungranted source ages; a granted one
      // resets. Saturating, so the bound cannot be skipped by a wrap.
      for (int s = 0; s < SOURCES; s++) begin
        if (sel[s]) begin
          age[s] <= '0;
        end else if (req[s] && age[s] != {AGE_W{1'b1}}) begin
          age[s] <= age[s] + 1'b1;
        end
        if (age[s] > max_age[s]) max_age[s] <= age[s];
      end

      // ---- §7's measurement: service DELIVERED, per source.
      for (int s = 0; s < SOURCES; s++)
        if (sel[s] && served[s] != 32'hFFFF_FFFF) served[s] <= served[s] + 1'b1;

      if (grant_valid && any_forced && age_forced != 16'hFFFF)
        age_forced <= age_forced + 1'b1;

      // A source reaching the bound at all is worth counting: it means
      // the weighted share alone was not delivering it service, which
      // is §7's composition problem becoming visible.
      for (int s = 0; s < SOURCES; s++)
        if (req[s] && age[s] == AGE_MAX[AGE_W-1:0]
            && starvation_events != 16'hFFFF)
          starvation_events <= starvation_events + 1'b1;
    end
  end
endmodule

// ---------------------------------------------------------------------
// ctrl_boundary_telemetry -- CLASSIFICATION: synthesisable, BINDABLE.
//
// WHAT IT DOES: measures BOTH sides of the controller. Occupancy and
// acceptance on the SoC side; command issue and data-bus busy on the
// DRAM side.
//
// WHY BOTH (29.1 §2): a full request queue does not mean DRAM is busy.
// It can equally mean the scheduler is blocked on a timing constraint
// while the data bus idles. A one-sided measurement cannot distinguish
// those, and they need opposite fixes.
//
// WHY READ AND WRITE SEPARATELY (§8): a full read queue and a full
// write queue mean opposite things about the workload, and a combined
// occupancy number hides which one is happening.
//
// WHAT IT CANNOT TELL YOU: why. Module 28 owns the investigation.
//
// SYNTHESIS: counters and two max-trackers. No memory.
// ---------------------------------------------------------------------
module ctrl_boundary_telemetry #(
  parameter int RQ_DEPTH = 32,
  parameter int WQ_DEPTH = 32,
  parameter int WIN_W    = 20     // measurement window, in cycles
)(
  input  logic                            clk,
  input  logic                            rst_n,

  // ---- SoC side
  input  logic                            req_valid,
  input  logic                            req_ready,
  input  logic                            req_is_read,
  input  logic [$clog2(RQ_DEPTH+1)-1:0]   rq_occ,
  input  logic [$clog2(WQ_DEPTH+1)-1:0]   wq_occ,

  // ---- DRAM side
  input  logic                            cmd_issued,
  input  logic                            data_busy,     // DQ bus active
  input  logic                            sched_blocked, // no legal candidate

  input  logic                            clear,

  // ---- published
  output logic [31:0]                     accepted_reads,
  output logic [31:0]                     accepted_writes,
  output logic [31:0]                     stalled_cycles,
  output logic [$clog2(RQ_DEPTH+1)-1:0]   rq_occ_max,
  output logic [$clog2(WQ_DEPTH+1)-1:0]   wq_occ_max,
  output logic [31:0]                     cmds_issued,
  output logic [31:0]                     data_busy_cycles,
  output logic [31:0]                     sched_blocked_cycles,
  output logic [31:0]                     window_cycles,
  output logic                            rq_ever_full,
  output logic                            wq_ever_full
);
  initial begin
    if (RQ_DEPTH < 2) $fatal(1, "ctrl_boundary_telemetry: RQ_DEPTH must be >= 2");
    if (WQ_DEPTH < 2) $fatal(1, "ctrl_boundary_telemetry: WQ_DEPTH must be >= 2");
    if (WIN_W    < 8) $fatal(1, "ctrl_boundary_telemetry: WIN_W must be >= 8");
  end

  always_ff @(posedge clk) begin
    if (!rst_n || clear) begin
      accepted_reads       <= '0;
      accepted_writes      <= '0;
      stalled_cycles       <= '0;
      rq_occ_max           <= '0;
      wq_occ_max           <= '0;
      cmds_issued          <= '0;
      data_busy_cycles     <= '0;
      sched_blocked_cycles <= '0;
      window_cycles        <= '0;
      rq_ever_full         <= 1'b0;
      wq_ever_full         <= 1'b0;
    end else begin
      if (window_cycles != 32'hFFFF_FFFF) window_cycles <= window_cycles + 1'b1;

      // §8: read and write accepted separately. A combined count
      // cannot show a read/write mix change, which is the thing that
      // drives turnaround cost.
      if (req_valid && req_ready) begin
        if (req_is_read) begin
          if (accepted_reads != 32'hFFFF_FFFF) accepted_reads <= accepted_reads + 1'b1;
        end else begin
          if (accepted_writes != 32'hFFFF_FFFF) accepted_writes <= accepted_writes + 1'b1;
        end
      end

      // A cycle where the requester offered and the controller could
      // not take it. This is the SoC-visible backpressure signal, and
      // 29.1 §2 is explicit that it says nothing about DRAM yet.
      if (req_valid && !req_ready && stalled_cycles != 32'hFFFF_FFFF)
        stalled_cycles <= stalled_cycles + 1'b1;

      if (rq_occ > rq_occ_max) rq_occ_max <= rq_occ;
      if (wq_occ > wq_occ_max) wq_occ_max <= wq_occ;
      if (rq_occ == RQ_DEPTH[$clog2(RQ_DEPTH+1)-1:0]) rq_ever_full <= 1'b1;
      if (wq_occ == WQ_DEPTH[$clog2(WQ_DEPTH+1)-1:0]) wq_ever_full <= 1'b1;

      if (cmd_issued && cmds_issued != 32'hFFFF_FFFF)
        cmds_issued <= cmds_issued + 1'b1;

      // The DRAM-side half of 29.1 §2's discrimination. data_busy is
      // the measurement that separates "DRAM saturated" from "queue
      // full for another reason".
      if (data_busy && data_busy_cycles != 32'hFFFF_FFFF)
        data_busy_cycles <= data_busy_cycles + 1'b1;

      // And the direct evidence of the third case: the scheduler had
      // requests and no LEGAL candidate. Without this, a full queue
      // with an idle bus is a mystery rather than a finding.
      if (sched_blocked && sched_blocked_cycles != 32'hFFFF_FFFF)
        sched_blocked_cycles <= sched_blocked_cycles + 1'b1;
    end
  end
endmodule

// Bound to §10's arbiter and §11's telemetry. Every property carries
// `disable iff (!rst_n)`, and every antecedent is covered below.
//
// A NOTE ON LIVENESS: the starvation bound IS a liveness property, and
// it is stated in a BOUNDED form -- "granted within AGE_MAX grant
// opportunities" -- rather than as an unbounded eventuality. A bounded
// form is checkable without assuming the environment offers service
// forever, which an unbounded one would require.
module ctrl_soc_sva #(
  parameter int SOURCES = 4, parameter int AGE_W = 10, parameter int AGE_MAX = 256,
  parameter int RQ_DEPTH = 32
)(
  input logic clk, rst_n, clear, downstream_ready,
  input logic [SOURCES-1:0] req, grant,
  input logic grant_valid,
  input logic [AGE_W-1:0] age [SOURCES], max_age [SOURCES],
  input logic [31:0] served [SOURCES],
  input logic [15:0] age_forced, starvation_events,
  input logic req_valid, req_ready, cmd_issued, data_busy, sched_blocked,
  input logic [31:0] accepted_reads, accepted_writes, stalled_cycles,
  input logic [31:0] cmds_issued, data_busy_cycles, sched_blocked_cycles, window_cycles,
  input logic [$clog2(RQ_DEPTH+1)-1:0] rq_occ, rq_occ_max,
  input logic rq_ever_full
);
  // ---- P1. FORBIDDEN. At most one source is granted per cycle. A
  // two-hot grant would admit two requests into a single-entry path.
  property p_one_hot_grant;
    @(posedge clk) disable iff (!rst_n)
      grant_valid |-> $onehot(grant);
  endproperty
  assert property (p_one_hot_grant)
    else $error("arbiter: grant is not one-hot");

  // ---- P2. FORBIDDEN. A source is never granted unless it requested.
  property p_grant_implies_request;
    @(posedge clk) disable iff (!rst_n)
      grant_valid |-> ((grant & req) == grant);
  endproperty
  assert property (p_grant_implies_request)
    else $error("arbiter: granted a source that did not request");

  // ---- P3. FORBIDDEN. No grant when downstream cannot accept. A
  // grant into a full queue loses the request.
  property p_no_grant_when_blocked;
    @(posedge clk) disable iff (!rst_n)
      !downstream_ready |-> !grant_valid;
  endproperty
  assert property (p_no_grant_when_blocked)
    else $error("arbiter: granted while downstream was not ready");

  // ---- P4. THE STARVATION BOUND, in bounded form. A source at its
  // age limit that keeps requesting, with downstream ready, is granted
  // on that cycle. §10: the bound OUTRANKS the weighted share, and
  // this is the property that holds it to that.
  property p_age_bound_forces_grant;
    @(posedge clk) disable iff (!rst_n)
      (req[0] && age[0] >= AGE_MAX && downstream_ready) |-> grant[0];
  endproperty
  assert property (p_age_bound_forces_grant)
    else $error("arbiter: a source at its age bound was not granted");

  // ---- P5. INVARIANT. Age never exceeds its field. Saturating, so
  // the bound cannot be skipped by a wrap -- which would silently
  // void the guarantee P4 states.
  property p_age_saturates;
    @(posedge clk) disable iff (!rst_n)
      (age[0] == {AGE_W{1'b1}}) |=> (age[0] >= AGE_MAX);
  endproperty
  assert property (p_age_saturates)
    else $error("arbiter: age wrapped past saturation");

  // ---- P6. A granted source's age resets. Without this the bound
  // would fire forever once reached.
  property p_grant_resets_age;
    @(posedge clk) disable iff (!rst_n)
      grant[0] |=> (age[0] == '0);
  endproperty
  assert property (p_grant_resets_age)
    else $error("arbiter: age did not reset on grant");

  // ---- P7. FORBIDDEN. An ungranted requesting source's age never
  // decreases. A decreasing age would let a source be deferred
  // indefinitely while appearing fresh.
  property p_age_monotone_while_waiting;
    @(posedge clk) disable iff (!rst_n)
      (req[0] && !grant[0] && !clear) |=> (age[0] >= $past(age[0]));
  endproperty
  assert property (p_age_monotone_while_waiting)
    else $error("arbiter: a waiting source's age decreased");

  // ---- P8. max_age bounds the live age at all times -- the
  // high-water mark cannot understate what happened.
  property p_max_age_bounds;
    @(posedge clk) disable iff (!rst_n)
      (max_age[0] >= age[0]) || (age[0] == '0);
  endproperty
  assert property (p_max_age_bounds)
    else $error("arbiter: max_age understates age");

  // ---- P9. §7's measurement advances only on a grant. Service
  // measured on anything else would not be service.
  property p_served_only_on_grant;
    @(posedge clk) disable iff (!rst_n)
      (!grant[0]) |=> (served[0] == $past(served[0]));
  endproperty
  assert property (p_served_only_on_grant)
    else $error("arbiter: served counter advanced without a grant");

  // ---- P10. INVARIANT. Data-busy cycles never exceed the window.
  // A utilisation above 100% means the two counters are driven from
  // different clocks or events -- 29.1 §2's discrimination depends on
  // this ratio being meaningful.
  property p_utilisation_is_a_fraction;
    @(posedge clk) disable iff (!rst_n)
      (data_busy_cycles <= window_cycles);
  endproperty
  assert property (p_utilisation_is_a_fraction)
    else $error("telemetry: data_busy %0d exceeds window %0d", data_busy_cycles, window_cycles);

  // ---- P11. INVARIANT. Occupancy stays within depth, and the
  // high-water mark bounds it.
  property p_occupancy_bounded;
    @(posedge clk) disable iff (!rst_n)
      (rq_occ <= RQ_DEPTH) && (rq_occ_max >= rq_occ);
  endproperty
  assert property (p_occupancy_bounded)
    else $error("telemetry: occupancy %0d out of range", rq_occ);

  // ---- P12. FORBIDDEN. The ever-full flag is sticky. §11: a queue
  // that filled once and one that never filled are different
  // findings, and a sampled reading misses the event.
  property p_ever_full_sticky;
    @(posedge clk) disable iff (!rst_n)
      (rq_ever_full && !clear) |=> rq_ever_full;
  endproperty
  assert property (p_ever_full_sticky)
    else $error("telemetry: ever_full cleared without a clear");

  // ---- P13. FORBIDDEN. Stalled cycles only accrue when the
  // requester offered and was refused. Counting anything else would
  // make backpressure look worse than it was.
  property p_stall_requires_refusal;
    @(posedge clk) disable iff (!rst_n)
      (!(req_valid && !req_ready)) |=> (stalled_cycles == $past(stalled_cycles));
  endproperty
  assert property (p_stall_requires_refusal)
    else $error("telemetry: stall counted without a refused offer");

  // ---- antecedent covers.
  cover property (@(posedge clk) disable iff (!rst_n) grant_valid);
  cover property (@(posedge clk) disable iff (!rst_n) $onehot(req));
  cover property (@(posedge clk) disable iff (!rst_n) $countones(req) > 1);
  cover property (@(posedge clk) disable iff (!rst_n) &req);
  cover property (@(posedge clk) disable iff (!rst_n) !downstream_ready && |req);
  cover property (@(posedge clk) disable iff (!rst_n) age[0] >= AGE_MAX);
  cover property (@(posedge clk) disable iff (!rst_n) age_forced != 16'd0);
  cover property (@(posedge clk) disable iff (!rst_n) starvation_events != 16'd0);
  cover property (@(posedge clk) disable iff (!rst_n) req_valid && !req_ready);
  cover property (@(posedge clk) disable iff (!rst_n) rq_ever_full);
  cover property (@(posedge clk) disable iff (!rst_n) sched_blocked);
  cover property (@(posedge clk) disable iff (!rst_n) sched_blocked && !data_busy);
  cover property (@(posedge clk) disable iff (!rst_n) data_busy);
  cover property (@(posedge clk) disable iff (!rst_n) accepted_writes != 32'd0);
endmodule

// SIMULATION-ONLY. Independent reference. It models the weighted share
// with a QUEUE of grant tokens generated up front from the weights,
// rather than with decrementing credits -- a different formulation, so
// agreement about the delivered ratio is evidence.
class qos_reference #(parameter int SOURCES = 4);
  int  weight[SOURCES];
  int  served[SOURCES];
  int  wait_cycles[SOURCES];
  int  max_wait[SOURCES];
  int  age_max;

  function void configure(int w[SOURCES], int bound);
    foreach (w[i]) weight[i] = w[i];
    age_max = bound;
    foreach (served[i]) begin served[i] = 0; wait_cycles[i] = 0; max_wait[i] = 0; end
  endfunction

  // One arbitration step. The bound outranks the share, exactly as
  // §10's RTL does -- but decided by scanning waits rather than by
  // credits, so the two agree only if the policy is the same.
  function int step(bit req[SOURCES], bit ready);
    int best = -1;
    if (!ready) begin
      foreach (req[i]) if (req[i]) begin
        wait_cycles[i]++;
        if (wait_cycles[i] > max_wait[i]) max_wait[i] = wait_cycles[i];
      end
      return -1;
    end
    // forced first
    foreach (req[i])
      if (req[i] && wait_cycles[i] >= age_max) begin best = i; break; end
    // then weighted: the source with the largest remaining share ratio
    if (best < 0) begin
      real bestr = -1.0;
      foreach (req[i])
        if (req[i]) begin
          real r = (weight[i] == 0) ? -1.0
                 : real'(weight[i]) / real'(served[i] + 1);
          if (r > bestr) begin bestr = r; best = i; end
        end
    end
    foreach (req[i]) begin
      if (req[i] && i == best) begin
        served[i]++;
        wait_cycles[i] = 0;
      end else if (req[i]) begin
        wait_cycles[i]++;
        if (wait_cycles[i] > max_wait[i]) max_wait[i] = wait_cycles[i];
      end
    end
    return best;
  endfunction

  // §7: the delivered ratio, which is the number that matters.
  function real delivered_share(int s);
    int total = 0;
    foreach (served[i]) total += served[i];
    if (total == 0) return -1.0;          // not zero: no data
    return real'(served[s]) / real'(total);
  endfunction

  function int worst_wait();
    int w = 0;
    foreach (max_wait[i]) if (max_wait[i] > w) w = max_wait[i];
    return w;
  endfunction
endclass

  TWO PASSING CONTROLLER-BOUNDARY REPORTS

  (A) the arbiter was never exercised
        all 13 properties            PASS
        grant_valid                  never asserted
        served[*]                    all 0
        max_age[*]                   all 0
        starvation_events            0
        ------------------------------------------------
        cover grant_valid            0 hits
        cover age >= AGE_MAX         0 hits
        ... all 14 covers            0 hits

        six of the thirteen properties are implications and never
        armed. The seven INVARIANTS -- one-hot on no grant, age
        saturation, max_age bound, utilisation fraction, occupancy
        bound, ever-full sticky, stall accounting -- all pass on
        zeros.

        "QoS arbitration: no starvation events" is produced by this
        run AND by a correctly tuned one.

  (B) both layers correct, the composition wrong
        stimulus : CPU class weight 7, DMA class weight 3, both
                   continuously requesting; CPU stream scattered,
                   DMA stream sequential
        served[CPU]                  69,880
        served[DMA]                  30,120
        delivered_share(CPU)         0.699      <-- as configured
        starvation_events            0
        max_age[CPU]                 11
        ------------------------------------------------
        all 13 properties            PASS
        all 14 covers                HIT

        and the CPU class received 41% of the DELIVERED DRAM
        BANDWIDTH, not 70%.

        the arbiter did exactly what it was configured to do: 70% of
        GRANTS went to the CPU class. Each CPU grant admitted a
        scattered request that the scheduler then served expensively
        -- often a row conflict -- while each DMA grant admitted a
        request the scheduler could serve as a row hit.

        §7: entries are opportunity, not service. The conversion rate
        is each source's own locality, which this layer cannot see.

    diagnosis : (A) is the vacuity case at the SoC boundary. (B) is
      the composition problem, and NO property catches it -- both
      layers satisfy their own contracts. served[] shows the grant
      ratio; only a bandwidth measurement per source shows the
      service ratio, and the gap between them is the finding.

    the fix : (A) read the covers. (B) measure delivered BANDWIDTH
      per source, not grants per source -- and accept that a share
      guarantee needs either a source-aware scheduler or empirical
      tuning, per §7.