AI Accelerators

   1  WHICH CONSTRAINT
        both halves of 26.4 §8's co-design are SILICON, so both are
        committed before the workload exists (§3)

   2  WHAT DECISION
        provision against the COST ASYMMETRY rather than the
        expectation (§5, §6), and instrument for the NEXT decision (§7)

   3  WHAT GRADE
        D for every cost and workload figure. 26.4's stream and
        stack arithmetic is A/CURRICULUM-DERIVED and is the only
        firm ground available (§9)

   the joint decision, stated as what it needs and what it has

     needs :  the workload's arithmetic intensity
              the workload's achievable outstanding-request count
              the workload's address distribution

     has   :  an estimate of each, from workloads that exist NOW
              and a design lifetime over which they will change

   so the decision is a bet, and §5 costs the two ways to lose it.

   DEFINITIONS
     V       the value of the system running at full workload speed
     c       the cost of the memory subsystem at the NOMINAL
             provisioning point
     f       the misprovisioning factor, f > 1

   OVER-provisioning by f  (M2):
     extra memory cost   =  (f - 1) * c
     performance         =  FULL
     cost per unit of delivered performance rises by
         (1 + (f-1)*c/V_total)   where V_total is the whole system's
                                 cost -- a small number when memory
                                 is a fraction of the system.

   UNDER-provisioning by f  (M1 or M3):
     memory cost saved   =  (1 - 1/f) * c
     performance         =  1/f of achievable  (26.4 §3's mechanism)
     value delivered     =  V / f
     cost per unit of delivered performance rises by
         f * (1 - (1 - 1/f)*c/V_total)  ~  f   for small c/V_total

   DERIVED, and this is the asymmetry:

       over-provision by f   -> cost/performance x (1 + (f-1)*c/V)
       under-provision by f  -> cost/performance x  approximately f

   the two are equal only when  c/V  is close to 1, i.e. when the
   memory IS the system. Whenever memory is a fraction of the
   system's cost, UNDER-provisioning is far worse.

   GRADE D.  memory subsystem = 30% of system cost, so c/V = 0.30.
   misprovisioning factor f = 2.

     over-provision 2x :  cost/perf x (1 + 1.0 * 0.30) = 1.30
     under-provision 2x:  cost/perf x  2.00 * (1 - 0.15) = 1.70

   DERIVED ratio of penalties: 1.70 / 1.30 = 1.31x worse to
   under-provision, at this cost share and this factor.

   recompute at c/V = 0.10 (memory a tenth of the system):
     over  : 1 + 1.0*0.10           = 1.10
     under : 2.00 * (1 - 0.05)      = 1.90
     DERIVED ratio: 1.73x worse to under-provision.

   recompute at c/V = 0.60 (memory the dominant cost):
     over  : 1 + 1.0*0.60           = 1.60
     under : 2.00 * (1 - 0.30)      = 1.40
     DERIVED ratio: 0.88 -- now OVER-provisioning is worse.

   the decision, as a procedure

   1  ESTIMATE the workload's arithmetic intensity, and the
      probability it is bandwidth-bound (26.4 §5)

   2  COMPUTE the memory's share of system cost, c/V

   3  IF c/V < ~0.5 AND the workload is likely bandwidth-bound
         -> bias the provisioning UP. The cheaper error is M2.
      IF c/V > ~0.5
         -> bias DOWN. The cheaper error is M1/M3.

   4  COMPUTE THE CEILING of the bias, because provisioning up has
      one: 26.4 §8's table gives the minimum outstanding requests
      to fill a given stack count, and a requester that cannot
      supply them converts M2 into M3.

   DERIVED from that table. Suppose the requester was designed for
   128 concurrent outstanding accesses.

     provisioning up to 8 stacks  : needs 128.  EXACTLY met.
     provisioning up to 12 stacks : needs 192.  NOT met.

   so provisioning the 12-stack configuration against a 128-request
   requester does not buy 12 stacks of bandwidth. It buys 8 stacks
   of bandwidth and 12 stacks of cost -- which is M2 and M3 at the
   same time, and 26.4 §9 says both produce working systems.

   CEILING: the provisioning bias is bounded by the requester's
   own parallelism, and 26.4 §8 is explicit that the requester's
   parallelism is silicon too.

   a third cause of "a fraction of the bandwidth"

     M5 (this section) : one stack degraded or partially repaired,
                         so its streams deliver less than the others

   and why it presents identically to M4:

     M4 : streams idle because ADDRESSES did not reach them
     M5 : streams slow because that STACK cannot deliver

   both show: outstanding count high, aggregate bandwidth low,
   some streams under-delivering. A monitor that reports only
   "streams occupied" cannot tell them apart.

// ---------------------------------------------------------------------
// provisioning_counterfactual -- the platform-profile block of §11.
//
// CLASSIFICATION: synthesisable telemetry. Drives nothing. Grade-D
// parameter values except where noted CURRICULUM-DERIVED.
//
// WHAT IT IS: §7's four counterfactual questions, answered from the
// JOINT history of the outstanding-request count and the stream
// occupancy. 26.4 §12's monitor reports the two requirements
// separately; this block additionally records WHICH ONE WAS BINDING
// over time, which is what a provisioning decision needs and a
// point-in-time report does not supply.
//
// WHY IT EXISTS HERE: §3 establishes that both halves are silicon and
// committed before the workload exists, so the current decision is
// closed. §7 concludes the controller's most valuable output is
// evidence for the next one, and 23.5 owns the counterfactual
// technique this applies.
//
// HOW TO RUN IT: run the real workload for a full window and read
// bound_by_requester against bound_by_streams.
// EXPECTED RESULT: exactly one of the two dominates, or both are low
// and the workload was not bandwidth-bound at all -- which is §5's
// most important input and the one nothing else reports.
//
// SYNTHESIS: three counters, two comparators, one min/max tracker.
// No divider: every ratio is reported as a pair.
//
// LIMITATIONS: it reports which half was BINDING, not what a
// different provisioning would have delivered numerically -- that
// requires a model of the alternative, and 23.5's counterfactual is
// explicit that a replay against an alternative is how such a number
// is obtained. Stating the boundary rather than implying a
// prediction. It also cannot see M5: per-stack throughput is §12's,
// and 27.3's independence discipline requires saying so.
// ---------------------------------------------------------------------
module provisioning_counterfactual #(
  // The MEMORY half of the joint decision. CURRICULUM-DERIVED from
  // 26.4 §6: sixteen streams per stack.
  parameter int NUM_STACKS      = 8,
  parameter int STREAMS_PER_STK = 16,
  parameter int TOTAL_STREAMS   = NUM_STACKS * STREAMS_PER_STK,

  // The REQUESTER half. CURRICULUM-DERIVED from 26.4 §8: an
  // accelerator cannot choose this at runtime, so it is a parameter
  // here in the same sense that it is silicon there.
  parameter int REQ_CEILING     = 128,

  parameter int WIN             = 1048576,
  // COUNT, not INDEX: each counter must represent a full window, so
  // $clog2(WIN + 1). Sized for an expected rate it would saturate at
  // exactly the saturated operating point the counterfactual is
  // about, and report the system as unbound when it was bound.
  parameter int CNT_W           = $clog2(WIN + 1),
  parameter int OCC_W           = $clog2(REQ_CEILING + 1),
  parameter int STR_W           = $clog2(TOTAL_STREAMS + 1)
)(
  input  logic               clk,
  input  logic               rst_n,

  input  logic [OCC_W-1:0]   outstanding,      // requests in flight
  input  logic [STR_W-1:0]   streams_busy,     // streams with work
  input  logic               demand_pending,   // somebody wants memory
  input  logic               win_tick,

  output logic [CNT_W-1:0]   c_bound_requester,
  output logic [CNT_W-1:0]   c_bound_streams,
  output logic [CNT_W-1:0]   c_bound_neither,
  output logic [CNT_W-1:0]   c_demand_cycles,
  output logic [STR_W-1:0]   streams_busy_max,
  output logic [OCC_W-1:0]   outstanding_max,
  output logic               result_valid,
  output logic               counter_saturated
);
  initial begin
    if (NUM_STACKS < 1)  $fatal(1, "provisioning_counterfactual: NUM_STACKS >= 1");
    if (REQ_CEILING < 1) $fatal(1, "provisioning_counterfactual: REQ_CEILING >= 1");
    // 26.4 §8's table, as an elaboration WARNING rather than a
    // fatal: a requester that cannot supply one access per stream
    // converts an over-provisioned memory (M2) into M3 as well, and
    // §6 step 4 is exactly this check. It is a warning because the
    // configuration is legal and merely unwise, and saying which is
    // part of the contract.
    if (REQ_CEILING < TOTAL_STREAMS)
      $warning("provisioning_counterfactual: REQ_CEILING %0d < TOTAL_STREAMS %0d -- cannot touch every stream once (26.4 §8, §6 step 4)",
               REQ_CEILING, TOTAL_STREAMS);
  end

  logic [CNT_W-1:0] br, bs, bn, dc;
  logic [STR_W-1:0] smax;
  logic [OCC_W-1:0] omax;

  // The three attributions. They are MUTUALLY EXCLUSIVE and jointly
  // exhaustive over demand cycles, which is what makes the report a
  // partition rather than three loosely related counters -- 23.2 §9's
  // exhaustive-and-disjoint standard, applied to provisioning.
  logic at_req_ceiling, streams_saturated;
  assign at_req_ceiling    = (outstanding  >= REQ_CEILING[OCC_W-1:0]);
  assign streams_saturated = (streams_busy >= TOTAL_STREAMS[STR_W-1:0]);

  always_ff @(posedge clk) begin
    if (!rst_n) begin
      br <= '0;  bs <= '0;  bn <= '0;  dc <= '0;
      smax <= '0;  omax <= '0;
      c_bound_requester <= '0;  c_bound_streams <= '0;
      c_bound_neither   <= '0;  c_demand_cycles <= '0;
      streams_busy_max  <= '0;  outstanding_max <= '0;
      result_valid <= 1'b0;  counter_saturated <= 1'b0;
    end else if (win_tick) begin
      c_bound_requester <= br;
      c_bound_streams   <= bs;
      c_bound_neither   <= bn;
      c_demand_cycles   <= dc;
      streams_busy_max  <= smax;
      outstanding_max   <= omax;
      result_valid      <= 1'b1;
      br <= '0;  bs <= '0;  bn <= '0;  dc <= '0;
      smax <= '0;  omax <= '0;
    end else begin
      result_valid <= 1'b0;

      // The denominator is DEMAND cycles, not window cycles. 30.8
      // §10's denominator error: counting idle cycles would conflate
      // "the provisioning was adequate" with "nobody asked", and
      // §5's model needs the second case reported SEPARATELY because
      // it means the workload was not bandwidth-bound at all.
      if (demand_pending) begin
        if (dc != {CNT_W{1'b1}}) dc <= dc + 1'b1;
        else counter_saturated <= 1'b1;

        // §7's rows two and three, as a partition. The joint test is
        // the whole point: 26.4 §12 reports the two requirements
        // separately and 26.4 §9 says they share a symptom, so only
        // the CONJUNCTION attributes a cycle.
        if (at_req_ceiling && !streams_saturated) begin
          // Requests are the ceiling and streams are idle -> MORE
          // OUTSTANDING REQUESTS would have helped. This is M3.
          if (br != {CNT_W{1'b1}}) br <= br + 1'b1;
          else counter_saturated <= 1'b1;
        end else if (streams_saturated) begin
          // Streams are full -> MORE STACKS would have helped. M1.
          if (bs != {CNT_W{1'b1}}) bs <= bs + 1'b1;
          else counter_saturated <= 1'b1;
        end else begin
          // Neither is at its limit and demand is pending. The
          // binding constraint is elsewhere -- distribution (M4),
          // degradation (M5, §12), or the workload simply is not
          // bandwidth-bound. §5's most important input.
          if (bn != {CNT_W{1'b1}}) bn <= bn + 1'b1;
          else counter_saturated <= 1'b1;
        end
      end

      if (streams_busy > smax) smax <= streams_busy;
      if (outstanding  > omax) omax <= outstanding;
    end
  end
endmodule

// ---------------------------------------------------------------------
// per_stack_throughput -- verification/telemetry, CORRECT as written.
//
// CLASSIFICATION: synthesisable telemetry. Drives nothing. Grade D.
//
// WHAT IT DOES: counts delivered beats per stack over a window and
// reports the spread, plus whether the under-delivering set is
// CONTIGUOUS within one stack.
//
// WHY IT EXISTS HERE: §8's table shows M4 and M5 differ in exactly
// one observable -- whether the under-delivering streams align with
// a stack boundary -- because 26.1 §3 and §6 establish that streams
// are grouped into channels within a stack while an address
// distribution has no reason to follow that grouping. And §8 row
// five is why it matters commercially: M4 is a software fix, M5 is
// scrap (31.3 §16).
//
// HOW TO RUN IT: run the workload and compare per-stack delivery.
// EXPECTED RESULT: a healthy system's stacks deliver within a narrow
// spread. One stack low is M5; a scattered pattern is M4.
//
// SYNTHESIS: one counter per stack plus a min/max tracker.
//
// LIMITATIONS: attributes to a STACK, not to a via or a group --
// 26.3 §6 owns that repair is per group rather than per via, and
// this block cannot see inside a stack. Nor can it prove degradation:
// a stack serving a cold address range legitimately delivers less.
// §18's row five is the disambiguation, and stating that this block
// does not perform it is 27.3's independence discipline.
// ---------------------------------------------------------------------
module per_stack_throughput #(
  parameter int NUM_STACKS = 8,
  parameter int WIN        = 1048576,
  // COUNT, not INDEX: a window in which ONE stack served every beat
  // must be representable, so $clog2(WIN + 1). Sized to the fair
  // share WIN / NUM_STACKS it would saturate in exactly the skewed
  // case it exists to detect, and report balance.
  parameter int CNT_W      = $clog2(WIN + 1),
  parameter int SID_W      = $clog2(NUM_STACKS > 1 ? NUM_STACKS : 2)
)(
  input  logic               clk,
  input  logic               rst_n,

  input  logic               beat_delivered,
  input  logic [SID_W-1:0]   beat_stack,
  input  logic               win_tick,

  output logic [CNT_W-1:0]   r_stack [NUM_STACKS],
  output logic [CNT_W-1:0]   r_max,
  output logic [CNT_W-1:0]   r_min,
  output logic [SID_W-1:0]   r_min_stack,
  output logic               single_stack_low,
  output logic               result_valid
);
  initial begin
    if (NUM_STACKS < 1) $fatal(1, "per_stack_throughput: NUM_STACKS >= 1");
    if (WIN < NUM_STACKS)
      $fatal(1, "per_stack_throughput: WIN < NUM_STACKS makes the spread meaningless");
  end

  logic [CNT_W-1:0] c [NUM_STACKS];

  always_ff @(posedge clk) begin
    if (!rst_n) begin
      for (int i = 0; i < NUM_STACKS; i++) begin c[i] <= '0; r_stack[i] <= '0; end
      r_max <= '0;
      // AND-accumulator discipline: a minimum tracker starts at
      // all-ones, or the first sample never wins and the reported
      // minimum stays zero -- which would flag every window as
      // having a dead stack.
      r_min <= '1;
      r_min_stack <= '0;
      single_stack_low <= 1'b0;  result_valid <= 1'b0;
    end else if (win_tick) begin
      begin
        logic [CNT_W-1:0] mx, mn;
        logic [SID_W-1:0] mni;
        logic [31:0]      n_low;
        mx = '0;  mn = '1;  mni = '0;  n_low = 0;
        for (int i = 0; i < NUM_STACKS; i++) begin
          if (c[i] > mx) mx = c[i];
          if (c[i] < mn) begin mn = c[i]; mni = i[SID_W-1:0]; end
        end
        // How many stacks are materially below the maximum? §8's
        // discriminator: ONE low stack is M5; SEVERAL scattered is
        // more consistent with M4, because a distribution failure has
        // no reason to spare all but one stack.
        for (int i = 0; i < NUM_STACKS; i++)
          if ((c[i] * 4) < (mx * 3)) n_low = n_low + 1;

        r_max <= mx;  r_min <= mn;  r_min_stack <= mni;
        // Reported as a FLAG plus both endpoints and the index, never
        // as a lone ratio -- 27.5 refuses a single percentage and
        // 30.8 §11 requires a derived statistic's range to be visible.
        single_stack_low <= (n_low == 1) && (NUM_STACKS > 1);
      end
      for (int i = 0; i < NUM_STACKS; i++) begin
        r_stack[i] <= c[i];
        c[i]       <= '0;
      end
      result_valid <= 1'b1;
    end else begin
      result_valid <= 1'b0;
      if (beat_delivered && c[beat_stack] != {CNT_W{1'b1}})
        c[beat_stack] <= c[beat_stack] + 1'b1;
    end
  end
endmodule

// ---------------------------------------------------------------------
// provisioning_ceiling -- CORRECT as written. Grade-D inputs except
// where noted CURRICULUM-DERIVED.
//
// CLASSIFICATION: synthesisable, but intended as an elaboration-time
// and design-review artifact. It drives nothing.
//
// WHAT IT DOES: given the requester's outstanding-request ceiling,
// reports the largest stack count that ceiling can actually fill,
// and flags a configuration that provisions beyond it.
//
// WHY IT EXISTS HERE: §6 step 4 bounds §5's provisioning bias by the
// requester's own parallelism, and 26.4 §8 supplies the arithmetic:
// sixteen streams per stack, and one outstanding access per stream
// merely to touch each once. A provisioning decision taken without
// this number converts M2 into M2-and-M3 simultaneously (§6), and
// 26.4 §9 says both produce working systems.
//
// HOW TO RUN IT: set REQ_CEILING to the requester's designed
// parallelism and sweep NUM_STACKS.
// EXPECTED RESULT: max_useful_stacks = floor(REQ_CEILING / 16), and
// over_provisioned rises once NUM_STACKS exceeds it.
//
// SYNTHESIS: a shift and two comparators. No divider -- the streams
// per stack is a power of two, which is CURRICULUM-DERIVED from
// 26.4 §6 rather than assumed.
//
// LIMITATIONS: reports the ceiling to TOUCH every stream once. 26.4
// §8 is explicit that KEEPING them busy needs "considerably more,
// since each must be re-issued as it completes" -- so this is a
// LOWER bound on the requirement and an UPPER bound on the useful
// stack count. Saying which direction each bound runs is the point;
// a single number here would be read as the answer.
// ---------------------------------------------------------------------
module provisioning_ceiling #(
  // CURRICULUM-DERIVED from 26.4 §6. A power of two, which is why no
  // divider is needed below.
  parameter int STREAMS_PER_STK = 16,
  // The requester half of 26.4 §8's joint decision. Silicon.
  parameter int REQ_CEILING     = 128,
  // The memory half, as proposed.
  parameter int NUM_STACKS      = 8,
  // §6 step 4's honest margin: 26.4 §8 says touching every stream
  // once is not enough to keep them busy. This is the multiplier a
  // design review must argue for, and it is grade D here because the
  // real value depends on the round-trip and the re-issue rate.
  parameter int REISSUE_FACTOR  = 2,

  parameter int LOG_SPS         = $clog2(STREAMS_PER_STK),
  // COUNT, not INDEX: the reported stack count must represent
  // NUM_STACKS inclusive, so $clog2(NUM_STACKS + 1). Sized
  // $clog2(NUM_STACKS) the ceiling can never equal the proposal and
  // over_provisioned would be unreachable at the exact boundary --
  // the guard failing on the one configuration it is for.
  parameter int STK_W           = $clog2(NUM_STACKS + 1)
)(
  input  logic                clk,
  input  logic                rst_n,

  // Runtime versions, so a platform whose requester ceiling is
  // discoverable can evaluate this without re-elaborating.
  input  logic [15:0]         cfg_req_ceiling,
  input  logic [7:0]          cfg_num_stacks,
  input  logic                cfg_valid,

  output logic [STK_W-1:0]    max_useful_stacks,
  output logic [STK_W-1:0]    max_useful_stacks_busy,
  output logic                over_provisioned,
  output logic                under_requested,
  output logic                cfg_out_of_range
);
  initial begin
    if (STREAMS_PER_STK < 1 || (STREAMS_PER_STK & (STREAMS_PER_STK - 1)) != 0)
      $fatal(1, "provisioning_ceiling: STREAMS_PER_STK must be a power of two (26.4 §6)");
    if (REQ_CEILING < 1) $fatal(1, "provisioning_ceiling: REQ_CEILING >= 1");
    if (REISSUE_FACTOR < 1)
      $fatal(1, "provisioning_ceiling: REISSUE_FACTOR >= 1");
  end

  // A configured ceiling of zero, or a stack count of zero, is not a
  // configuration -- it is an absent one, and 30.7 §9's discipline
  // says unknown is not a default.
  assign cfg_out_of_range = cfg_valid &&
                            ((cfg_req_ceiling == '0) || (cfg_num_stacks == '0));

  always_comb begin
    if (!cfg_valid || cfg_out_of_range) begin
      max_useful_stacks      = '0;
      max_useful_stacks_busy = '0;
      over_provisioned       = 1'b0;
      under_requested        = 1'b0;
    end else begin
      // 26.4 §8's table, computed. A shift rather than a divide,
      // because STREAMS_PER_STK is a power of two.
      max_useful_stacks      = STK_W'(cfg_req_ceiling >> LOG_SPS);
      // And the honest version, per this block's LIMITATIONS: 26.4
      // §8 says touching every stream once is not enough. Reported
      // SEPARATELY rather than replacing the first number, so a
      // reviewer sees both bounds and cannot mistake one for the
      // other.
      max_useful_stacks_busy = STK_W'((cfg_req_ceiling / REISSUE_FACTOR) >> LOG_SPS);

      // The two directions of §6's bound. Both are flagged, because
      // §4 establishes M2 and M3 are different errors with different
      // costs and a single "mismatch" flag would conflate them.
      over_provisioned = (cfg_num_stacks > max_useful_stacks);
      under_requested  = (cfg_num_stacks < max_useful_stacks_busy);
    end
  end
endmodule

   max_useful_stacks       = 128 >> 4        =  8 stacks
   max_useful_stacks_busy  = (128/2) >> 4    =  4 stacks

   so a 128-request requester can TOUCH 8 stacks' streams and
   realistically KEEP 4 stacks busy at a grade-D re-issue factor
   of 2. A 12-stack proposal is over-provisioned against both.

  // ---- The ceiling block's own contract.
  // The relationship 26.4 §8's table encodes, as an invariant. If
  // this fails, the block and the table disagree and the table wins.
  property p_ceiling_matches_table;
    @(posedge clk) disable iff (!rst_n)
      (cfg_valid && !cfg_out_of_range) |->
        (max_useful_stacks == (cfg_req_ceiling >> LOG_SPS));
  endproperty
  assert property (p_ceiling_matches_table)
    else $error("the computed ceiling disagrees with 26.4 §8's arithmetic");

  // The realistic ceiling must never EXCEED the touch-once ceiling,
  // because a re-issue factor of at least one cannot increase the
  // number of stacks a fixed request budget can fill. A derived
  // statistic whose range follows from its definition -- 30.8 §11.
  property p_busy_ceiling_not_above_touch_ceiling;
    @(posedge clk) disable iff (!rst_n)
      (cfg_valid && !cfg_out_of_range) |->
        (max_useful_stacks_busy <= max_useful_stacks);
  endproperty
  assert property (p_busy_ceiling_not_above_touch_ceiling)
    else $error("the realistic ceiling exceeded the touch-once ceiling");

  // An absent configuration produces no verdict rather than a
  // default one -- the same discipline 32.2 §15's filter applies,
  // and 30.7 §9's "unknown is not a default".
  property p_no_verdict_without_config;
    @(posedge clk) disable iff (!rst_n)
      (!cfg_valid || cfg_out_of_range) |-> (!over_provisioned && !under_requested);
  endproperty
  assert property (p_no_verdict_without_config)
    else $error("a provisioning verdict was issued with no valid configuration");

  // ---- Covers: both verdicts and the balanced case, per 31.1 §14's
  //      configuration rule. A block that has only ever reported one
  //      verdict has been exercised in one configuration.
  cover property (@(posedge clk) disable iff (!rst_n) over_provisioned);
  cover property (@(posedge clk) disable iff (!rst_n) under_requested);
  cover property (@(posedge clk) disable iff (!rst_n)
                  cfg_valid && !over_provisioned && !under_requested);

// ---------------------------------------------------------------------
// stream_utilisation -- INTENTIONALLY DEFECTIVE, for review (§14).
//
// CLASSIFICATION: synthesisable telemetry, grade-D values, CONTAINS
// A BUG.
//
// WHAT IT IS MEANT TO DO: the five-clause contract above -- report
// whether the provisioned stream space was used, so §7's
// counterfactual question is answerable.
//
// WHY IT EXISTS HERE: §7 argues the controller's most valuable output
// is evidence for the NEXT provisioning decision. This block is that
// evidence, computed against the wrong denominator -- and because
// the number it produces is plausible and high, it argues for
// exactly the wrong conclusion.
//
// HOW TO RUN IT: run a workload whose addresses concentrate on a
// quarter of the stream space (M4).
// EXPECTED RESULT under clause 2: utilisation is LOW, because three
// quarters of the provisioned streams delivered nothing.
// EXPECTED TRACE: the denominator must be TOTAL_STREAMS x window,
// independent of how many streams were busy.
//
// SYNTHESIS: two counters and a compare.
//
// LIMITATIONS: reports utilisation only; per-stack attribution is
// §12's. That is STATED and is not the bug.
// ---------------------------------------------------------------------
module stream_utilisation #(
  parameter int NUM_STACKS      = 8,
  parameter int STREAMS_PER_STK = 16,          // CURRICULUM-DERIVED, 26.4 §6
  parameter int TOTAL_STREAMS   = NUM_STACKS * STREAMS_PER_STK,
  parameter int WIN             = 1048576,
  parameter int CNT_W           = $clog2(WIN + 1),
  parameter int STR_W           = $clog2(TOTAL_STREAMS + 1),
  // COUNT, not INDEX: the capacity accumulator must represent
  // TOTAL_STREAMS x WIN, so it needs STR_W + CNT_W bits. One short
  // and it wraps on a fully busy window -- reporting a LOW
  // utilisation at exactly the saturated point the report is for.
  parameter int CAP_W           = STR_W + CNT_W
)(
  input  logic               clk,
  input  logic               rst_n,

  input  logic               beat_delivered,
  input  logic [STR_W-1:0]   streams_busy,     // on the interface, and...
  input  logic               demand_pending,
  input  logic               win_tick,

  output logic [CNT_W-1:0]   r_beats,
  output logic [CAP_W-1:0]   r_capacity,
  output logic [CNT_W-1:0]   r_demand_cycles,
  output logic               over_unity,
  output logic               result_valid
);
  logic [CNT_W-1:0] beats, dem;
  logic [CAP_W-1:0] cap;

  initial begin
    if (NUM_STACKS < 1) $fatal(1, "stream_utilisation: NUM_STACKS >= 1");
  end

  always_ff @(posedge clk) begin
    if (!rst_n) begin
      beats <= '0;  dem <= '0;  cap <= '0;
      r_beats <= '0;  r_capacity <= '0;  r_demand_cycles <= '0;
      over_unity <= 1'b0;  result_valid <= 1'b0;
    end else if (win_tick) begin
      r_beats         <= beats;
      r_capacity      <= cap;
      // Clause 4 is HONOURED: the demand denominator is reported
      // separately, so a reviewer checking "can this distinguish
      // adequate provisioning from an idle system?" finds that it
      // can. That is what conceals the defect.
      r_demand_cycles <= dem;
      // Clause 5 is HONOURED: an impossible utilisation is flagged.
      over_unity      <= (beats > cap[CNT_W-1:0]);
      result_valid    <= 1'b1;
      beats <= '0;  dem <= '0;  cap <= '0;
    end else begin
      result_valid <= 1'b0;
      if (beat_delivered && beats != {CNT_W{1'b1}}) beats <= beats + 1'b1;
      if (demand_pending && dem   != {CNT_W{1'b1}}) dem   <= dem   + 1'b1;
      // The capacity accumulator.
      cap <= cap + {{(CAP_W-STR_W){1'b0}}, streams_busy};   // <-- THE DEFECT
    end
  end
endmodule

   GRADE D. NUM_STACKS = 8, STREAMS_PER_STK = 16, so
   TOTAL_STREAMS = 128 (CURRICULUM-DERIVED structure, 26.4 §6).

   a workload whose addresses concentrate on 32 streams (M4):

     beats delivered over the window : 32 streams x W beats
     contract denominator (clause 2) : 128 x W
         DERIVED utilisation = 32/128 = 25.0%   <- the TRUTH

     this block's denominator        :  32 x W   (streams_busy)
         DERIVED utilisation = 32/32  = 100.0%  <- what it reports

   and clause 5's over-unity flag never fires, because the two
   quantities move together and the ratio is exactly 1.

   DERIVED consequence, and it is the worst outcome in this module:

     actual problem  : M4, fixable after shipping, costs nothing
     reported problem: M1, fixable only in silicon
     action taken    : provision more stacks next generation

     result: the new silicon has MORE streams, the addresses still
     concentrate on the same fraction, and the utilisation report
     still reads 100%. The next decision buys stacks again.

   the defect is self-confirming: the action it recommends does
   not change the number it produces.

      // CORRECTED. Clause 2: the denominator is the PROVISIONED
      // capacity, which is a constant per cycle and independent of
      // what was busy. The question is whether the provisioning was
      // adequate, so the provisioning must be the denominator.
      //
      // streams_busy remains on the interface and is now genuinely
      // unused HERE -- it belongs to §11's block, which needs it for
      // the attribution partition. A signal that is right for one
      // block and wrong for another is not a signal to delete; it is
      // one to route correctly.
      cap <= cap + TOTAL_STREAMS[CAP_W-1:0];

  // Offered as "proves the utilisation report is sound". All PASS on
  // the defective block.
  property p_utilisation_never_over_unity;
    @(posedge clk) disable iff (!rst_n)
      result_valid |-> (r_beats <= r_capacity);
  endproperty
  assert property (p_utilisation_never_over_unity)
    else $error("delivered beats exceeded the reported capacity");

  property p_demand_reported_separately;
    @(posedge clk) disable iff (!rst_n)
      result_valid |-> (r_demand_cycles <= WIN);
  endproperty
  assert property (p_demand_reported_separately)
    else $error("demand cycles exceeded the window");

  property p_counters_cleared_each_window;
    @(posedge clk) disable iff (!rst_n)
      result_valid |=> (r_beats == $past(r_beats));
  endproperty
  assert property (p_counters_cleared_each_window)
    else $error("a latched result changed outside a window tick");

  // Clause 2. It names the PROVISIONED constant, so a denominator
  // derived from streams_busy cannot satisfy it. Variety 2's repair,
  // and note that the property is an equality rather than a bound --
  // a capacity accumulator has exactly one correct value per cycle.
  property p_capacity_is_provisioned_not_observed;
    @(posedge clk) disable iff (!rst_n)
      result_valid |-> (r_capacity == (TOTAL_STREAMS * $past(WIN_ELAPSED)));
  endproperty
  assert property (p_capacity_is_provisioned_not_observed)
    else $error("the capacity denominator was not the provisioned capacity");

  // The INDEPENDENCE property, which is the general form and the one
  // worth carrying: the denominator must not move when only the
  // numerator's driver moves. This is the property that catches the
  // whole class §15 names, not just this instance.
  property p_denominator_independent_of_numerator;
    @(posedge clk) disable iff (!rst_n)
      ($changed(streams_busy) && !win_tick) |=> $stable(cap_delta);
  endproperty
  assert property (p_denominator_independent_of_numerator)
    else $error("the capacity denominator moved with the busy-stream count");

  // §11's partition, asserted as exhaustive and disjoint -- 23.2 §9's
  // standard. Without this the three attribution counters are three
  // loosely related numbers rather than a partition, and §7's
  // counterfactual cannot be read off them.
  property p_attribution_is_a_partition;
    @(posedge clk) disable iff (!rst_n)
      result_valid |->
        ((c_bound_requester + c_bound_streams + c_bound_neither) == c_demand_cycles);
  endproperty
  assert property (p_attribution_is_a_partition)
    else $error("the provisioning attribution does not sum to the demand cycles");

  // Clause 3's mutual exclusion, stated separately because a
  // partition needs both properties: they sum correctly AND no cycle
  // is charged twice.
  property p_attribution_is_disjoint;
    @(posedge clk) disable iff (!rst_n)
      demand_pending |-> $onehot({at_req_ceiling && !streams_saturated,
                                  streams_saturated,
                                  !at_req_ceiling && !streams_saturated});
  endproperty
  assert property (p_attribution_is_disjoint)
    else $error("a demand cycle was attributed to more than one cause");

  // Saturation must never be reached, because a saturated
  // attribution counter understates a cause -- and §15 shows the
  // action taken depends on WHICH cause dominates, so an
  // understatement changes a silicon decision. 30.8 §11's range
  // rule, with the consequence named.
  property p_no_attribution_saturation;
    @(posedge clk) disable iff (!rst_n)
      result_valid |-> !counter_saturated;
  endproperty
  assert property (p_no_attribution_saturation)
    else $error("an attribution counter saturated: a provisioning conclusion is understated");

  // ---- Covers. The dimension this defect scales with is the
  //      ADDRESS DISTRIBUTION, and 31.3 §15's rule says the cover
  //      must be on that dimension.
  // A CONCENTRATED distribution -- the case that separates the
  // correct denominator from the defective one. A uniform-address
  // testbench never produces it, and the defect is invisible under
  // uniform traffic because busy == provisioned.
  cover property (@(posedge clk) disable iff (!rst_n)
                  demand_pending && (streams_busy * 4 < TOTAL_STREAMS));
  // A UNIFORM distribution, so both regimes are known to have run.
  cover property (@(posedge clk) disable iff (!rst_n)
                  demand_pending && (streams_busy >= TOTAL_STREAMS));
  // Each of §11's three attributions reached, per the per-dimension
  // rule -- an attribution counter that never incremented proves
  // nothing about the cause it represents.
  cover property (@(posedge clk) disable iff (!rst_n)
                  demand_pending && at_req_ceiling && !streams_saturated);
  cover property (@(posedge clk) disable iff (!rst_n)
                  demand_pending && streams_saturated);
  // The "neither" case, which §11 argues is the strongest available
  // argument for provisioning DOWN and which a bandwidth-focused
  // report would never produce.
  cover property (@(posedge clk) disable iff (!rst_n)
                  demand_pending && !at_req_ceiling && !streams_saturated);
  // And §12's discriminator: exactly one stack materially low.
  cover property (@(posedge clk) disable iff (!rst_n) single_stack_low);

  // The partition, from both directions. §11's whole value is that
  // the three counters partition the demand cycles -- 23.2 §9's
  // exhaustive-and-disjoint standard -- so a reader can attribute
  // every demand cycle to one named cause.
  property p_partition_sums_to_demand;
    @(posedge clk) disable iff (!rst_n)
      result_valid |->
        ((c_bound_requester + c_bound_streams + c_bound_neither) == c_demand_cycles);
  endproperty
  assert property (p_partition_sums_to_demand)
    else $error("the attribution counters do not sum to the demand cycles");

  // Nothing may be attributed on a cycle with no demand. This is the
  // property that keeps §11's denominator honest: 30.8 §10's
  // denominator error was counting the wrong cycles, and this
  // forbids the same mistake here.
  property p_no_attribution_without_demand;
    @(posedge clk) disable iff (!rst_n)
      (!demand_pending) |=> ($stable(c_bound_requester) &&
                             $stable(c_bound_streams)   &&
                             $stable(c_bound_neither));
  endproperty
  assert property (p_no_attribution_without_demand)
    else $error("a cycle with no demand was attributed to a provisioning cause");

  // The two observed maxima must respect their provisioned ceilings,
  // or the block is reporting a state the configuration forbids --
  // 30.8 §11's range rule, and here an out-of-range maximum means
  // the ceiling parameter disagrees with the hardware.
  property p_maxima_within_provisioning;
    @(posedge clk) disable iff (!rst_n)
      result_valid |-> ((outstanding_max <= REQ_CEILING) &&
                        (streams_busy_max <= TOTAL_STREAMS));
  endproperty
  assert property (p_maxima_within_provisioning)
    else $error("an observed maximum exceeded its provisioned ceiling");

  // 26.4 §8's table as a runtime invariant: if the requester ceiling
  // cannot touch every stream once, the streams can never ALL be
  // busy. A design reporting otherwise has a counter or a parameter
  // that disagrees with the hardware.
  property p_ceiling_bounds_stream_occupancy;
    @(posedge clk) disable iff (!rst_n)
      (REQ_CEILING < TOTAL_STREAMS) |-> (streams_busy <= REQ_CEILING);
  endproperty
  assert property (p_ceiling_bounds_stream_occupancy)
    else $error("more streams were busy than the requester can have outstanding");

  // And the invariant that makes the counterfactual TRUSTWORTHY
  // rather than merely present: the block must never attribute to
  // BOTH halves at once, because §7's whole use of it is to decide
  // which half to buy next time.
  property p_never_bound_by_both;
    @(posedge clk) disable iff (!rst_n)
      !(at_req_ceiling && streams_saturated && demand_pending) ||
       ((c_bound_requester == $past(c_bound_requester)) ||
        (c_bound_streams   == $past(c_bound_streams)));
  endproperty
  assert property (p_never_bound_by_both)
    else $error("a cycle was attributed to both provisioning halves");

  // ---- Covers: the configuration arms, per 31.1 §14's rule, since
  //      REQ_CEILING versus TOTAL_STREAMS is exactly the
  //      configuration 26.4 §8's table is about.
  cover property (@(posedge clk) disable iff (!rst_n)
                  result_valid && (REQ_CEILING >= TOTAL_STREAMS));
  cover property (@(posedge clk) disable iff (!rst_n)
                  result_valid && (REQ_CEILING < TOTAL_STREAMS));
  // A window in which the requester half dominated, and one in which
  // the memory half did -- both must occur or the counterfactual has
  // only ever produced one answer.
  cover property (@(posedge clk) disable iff (!rst_n)
                  result_valid && (c_bound_requester > c_bound_streams));
  cover property (@(posedge clk) disable iff (!rst_n)
                  result_valid && (c_bound_streams > c_bound_requester));