CPU Memory Controllers

   for each platform class, in this order:

     1  WHICH CONSTRAINT dominates that did not dominate elsewhere
     2  WHAT DECISION that constraint forces on the controller
     3  WHAT GRADE of evidence we have for any of it

   and the answer to (1) is, in every chapter of this module,
   a property of the REQUESTER MIX rather than of the DRAM.

   AXIS 1 -- DEADLINE
     does something stall until this completes?
       yes -> latency is observable, and delay has a cost upstream
       no  -> latency is invisible; only throughput matters

   AXIS 2 -- DROPPABILITY
     may the controller discard this request entirely?
       yes -> it is a HINT. Correctness does not depend on it.
       no  -> it is an OBLIGATION. Discarding it loses data or hangs
              the requester.

   the two axes are INDEPENDENT, and all four combinations occur.

   1  identify which of §5's three source situations applies
   2  if a mechanism is documented -> READ THE CONFIGURATION
   3  if only research exists -> treat it as grade C: a finding
      about those machines, and design a measurement for yours
   4  state the category with every number you then quote

   and note what step 2 requires that step 3 does not: ACCESS to
   the running machine's registers. A grade-B answer is only
   actionable if you can read the configuration, which is an
   observability requirement rather than a documentation one.

   GRADE D. A representative mix, per 100 requests reaching the
   controller. Proportions are invented; the RANKING they produce
   is the transferable part.

     class         share   deadline  droppable
     -----------   -----   --------  ---------
     demand          40      yes        no
     prefetch        35      no         YES
     writeback       20      no         no
     translation      5      yes+       no      (+ blocks another)

   DERIVED observations, recomputed:

   (1) DEADLINE-BEARING share  = 40 + 5 = 45%
       so 55% of arriving traffic has NO deadline at all.

   (2) DROPPABLE share = 35%
       more than a third of the queue is work the controller is
       free to abandon -- and Module 17's queue has no field for it.

   (3) the class with the STRONGEST obligation has the SMALLEST
       share: translation, at 5%.

// ---------------------------------------------------------------------
// request_class_admission -- the platform-profile block of §9.
//
// CLASSIFICATION: synthesisable, grade-D parameter values, CORRECT as
// written. The intentionally defective block is §12.
//
// WHAT IT IS: the controller's admission boundary, class-aware. It is
// the ONLY place a drop may legally occur, because after 17.5's
// handshake the controller owes a completion (§4).
//
// WHY IT EXISTS HERE: §3 establishes two independent axes -- deadline
// and droppability -- and §4 that Module 17's queue has no field for
// the second. This block adds that field at the only boundary where
// it can be acted on, and its generate boundaries show what a
// single-requester platform does NOT need.
//
// HOW TO RUN IT: offer a mix at or above capacity with all four
// classes present.
// EXPECTED RESULT: prefetches are DROPPED (not deferred), writebacks
// are DEFERRED (never dropped), and deadline classes are admitted.
// EXPECTED TRACE: on pressure, drop_count rises and no
// deadline-bearing or non-droppable request is ever refused.
//
// SYNTHESIS: one occupancy counter per class plus a small decode. No
// memory; the queue itself is 17.2's.
//
// LIMITATIONS: models ADMISSION. It does not schedule -- 17.1 owns
// the pipeline, 17.4 the layered mask, and 23.4 the heuristic, and
// §7's argument is precisely that the class ranking belongs in
// 17.4's LAYERS rather than in a weight here. Nor does it model
// coherence itself: COHERENT only selects whether a remote class
// exists, and CHI/AXI semantics are 29.1's.
// ---------------------------------------------------------------------
module request_class_admission #(
  // Platform properties. These are the CONSTRAINT of §1 step 1
  // expressed as parameters, not sizes -- so 31.1 §12's warning
  // applies: an obligation must be re-derived when they change.
  parameter bit COHERENT     = 1'b1,
  parameter bit HAS_PREFETCH = 1'b1,
  parameter int NUM_CORES    = 8,

  parameter int QDEPTH       = 32,
  // Grade D. The share at which the droppable class starts being
  // shed. §4: dropping is a policy with a threshold somebody must
  // justify -- the same shape as 17.4 §9's age threshold.
  parameter int DROP_AT_PCT  = 75,

  // COUNT, not INDEX: occupancy ranges 0 .. QDEPTH inclusive, so it
  // needs $clog2(QDEPTH + 1) bits. Sized $clog2(QDEPTH) a full queue
  // wraps to empty and admission would accept without limit --
  // the counter failing inside the pressure case it exists to detect.
  parameter int OCC_W        = $clog2(QDEPTH + 1),
  parameter int CNT_W        = 32
)(
  input  logic              clk,
  input  logic              rst_n,

  // Upstream. 17.5 owns the ready/valid contract; this block supplies
  // `req_ready` and must hold 17.5's one-handshake-one-entry rule.
  input  logic              req_valid,
  input  logic [2:0]        req_class,
  output logic              req_ready,

  // Queue state, from 17.2's pool.
  input  logic [OCC_W-1:0]  q_occupancy,
  input  logic              q_free,

  // Outputs.
  output logic              admit,
  output logic              drop,
  output logic              defer_hint,
  output logic [CNT_W-1:0]  drop_count,
  output logic [CNT_W-1:0]  admit_count,
  output logic              class_unknown,
  output logic [7:0]        classes_present
);
  // The class codes. Translation is a CODE rather than a diagram node
  // (§8) and it carries the strongest obligation in §3's table.
  localparam logic [2:0] CL_DEMAND = 3'd0;  // deadline, not droppable
  localparam logic [2:0] CL_PREF   = 3'd1;  // no deadline, DROPPABLE
  localparam logic [2:0] CL_WB     = 3'd2;  // no deadline, never drop
  localparam logic [2:0] CL_XLATE  = 3'd3;  // deadline, and BLOCKS
  localparam logic [2:0] CL_REMOTE = 3'd4;  // coherent platforms only

  initial begin
    if (QDEPTH < 2) $fatal(1, "request_class_admission: QDEPTH must be >= 2");
    if (DROP_AT_PCT < 1 || DROP_AT_PCT > 100)
      $fatal(1, "request_class_admission: DROP_AT_PCT must be 1..100");
    // §4's third consequence, enforced: a threshold of 100 means the
    // droppable class is only shed when the queue is completely full,
    // which is indistinguishable from not having the mechanism. Flag
    // it rather than let a configuration silently disable the feature
    // -- 31.2 §7's "present in the source, absent in the silicon".
    if (HAS_PREFETCH && DROP_AT_PCT == 100)
      $warning("request_class_admission: DROP_AT_PCT = 100 disables shedding in all but the full case (§4)");
  end

  // The drop threshold in entries, DERIVED at elaboration so the
  // percentage and the depth cannot disagree at runtime.
  localparam int DROP_THRESH = (QDEPTH * DROP_AT_PCT) / 100;

  logic deadline_bearing, droppable, recognised;

  always_comb begin
    // §3's two axes, decoded independently -- they are INDEPENDENT,
    // so they are two expressions rather than one priority number.
    // Collapsing them into a single "priority" is the error §3's
    // second and third rows are about.
    unique case (req_class)
      CL_DEMAND : begin deadline_bearing = 1'b1; droppable = 1'b0; recognised = 1'b1; end
      CL_PREF   : begin deadline_bearing = 1'b0; droppable = 1'b1; recognised = HAS_PREFETCH; end
      CL_WB     : begin deadline_bearing = 1'b0; droppable = 1'b0; recognised = 1'b1; end
      CL_XLATE  : begin deadline_bearing = 1'b1; droppable = 1'b0; recognised = 1'b1; end
      CL_REMOTE : begin deadline_bearing = 1'b1; droppable = 1'b0; recognised = COHERENT; end
      default   : begin deadline_bearing = 1'b1; droppable = 1'b0; recognised = 1'b0; end
    endcase
  end

  // An unrecognised class is treated as deadline-bearing and
  // NON-droppable, and reported. 7.4's three-valued discipline
  // applied to a class code: the safe default for an unknown
  // obligation is the STRONGEST obligation, because the cost of
  // over-serving is performance and the cost of under-serving is
  // correctness.
  assign class_unknown = req_valid && !recognised;

  generate
  if (HAS_PREFETCH) begin : g_shedding

    logic under_pressure;
    assign under_pressure = (q_occupancy >= DROP_THRESH[OCC_W-1:0]);

    // The drop decision. It happens BEFORE acceptance -- §4's first
    // consequence -- so `drop` and `admit` are mutually exclusive and
    // together they account for every valid request.
    assign drop  = req_valid && recognised && droppable && under_pressure;
    assign admit = req_valid && !drop && q_free;

    // Deferral is a HINT to 17.4's policy layers, not an action here.
    // A writeback under pressure is deferred by the SCHEDULER; this
    // block only says which class it is. Acting on it here would put
    // policy in the admission stage, which 17.4 §3 forbids.
    assign defer_hint = req_valid && recognised && !droppable && !deadline_bearing;

  end else begin : g_no_shedding

    // A platform with no prefetcher has no droppable class, so the
    // mechanism does not exist -- it is not disabled, it is absent.
    assign drop       = 1'b0;
    assign admit      = req_valid && q_free;
    assign defer_hint = req_valid && recognised && !deadline_bearing;

  end
  endgenerate

  assign req_ready = admit || drop;   // a dropped request is ANSWERED

  always_ff @(posedge clk) begin
    if (!rst_n) begin
      drop_count      <= '0;
      admit_count     <= '0;
      classes_present <= '0;
    end else begin
      // §4's second consequence: a drop must be COUNTED. A drop that
      // is not counted is indistinguishable from a prefetcher that
      // never issued, and the two have opposite fixes.
      if (drop  && drop_count  != {CNT_W{1'b1}}) drop_count  <= drop_count  + 1'b1;
      if (admit && admit_count != {CNT_W{1'b1}}) admit_count <= admit_count + 1'b1;
      // Which classes this platform actually presented, so §14's mix
      // report can be checked against the platform's claims.
      if (req_valid && recognised) classes_present[req_class[2:0]] <= 1'b1;
    end
  end
endmodule

// ---------------------------------------------------------------------
// class_policy_layers -- CORRECT as written. Grade-D thresholds.
//
// CLASSIFICATION: synthesisable policy. It chooses among LEGAL
// candidates only, and never re-checks legality -- 17.4 §3 owns why
// that separation is mandatory rather than tidy.
//
// WHAT IT IS: §7's class ranking expressed as 17.4's LAYERED MASK.
// Each layer NARROWS the legal set; a layer that would empty it
// passes the set through unchanged. That narrowing rule is what lets
// a 5%-share class be served first without a weight its rarity
// would dilute.
//
// WHY IT EXISTS HERE: §7's result is that share and obligation are
// anti-correlated, so any share-proportional policy under-serves the
// hardest obligation. The claim that layers fix it is structural,
// and a generate-free mask chain is how a structural claim is made
// checkable.
//
// HOW TO RUN IT: present a legal set containing one translation
// request and many prefetches.
// EXPECTED RESULT: the translation request is granted, and its 5%
// share is irrelevant to that outcome.
// EXPECTED TRACE: grant must be one-hot and a subset of legal_mask
// on every cycle.
//
// SYNTHESIS: four mask ANDs, four zero-detects, one priority encoder.
//
// LIMITATIONS: implements the CLASS layer and a rotation below it. It
// does not implement locality preference (23.3), direction batching
// (30.5 §7) or the age-based bounded bypass -- 17.4 §9 owns that and
// §6 of this block's discussion states why age must sit ABOVE class.
// ---------------------------------------------------------------------
module class_policy_layers #(
  parameter int NUM_ENTRIES = 16,
  // COUNT, not INDEX: the age counter must REPRESENT the threshold it
  // is compared against, so it needs $clog2(AGE_MAX + 1) bits. Sized
  // $clog2(AGE_MAX) the comparison is unreachable and the fairness
  // layer is present in the source and absent in the silicon --
  // 31.2 §7's hazard, and 17.4 §9 owns the original argument.
  parameter int AGE_MAX      = 255,
  parameter int AGE_W        = $clog2(AGE_MAX + 1),
  // Grade D. The age at which fairness outranks class. It must sit
  // ABOVE the class layer or a starved low-class entry is
  // unreachable -- 17.4 §9's "the override must be reachable".
  parameter int AGE_URGENT   = 192
)(
  input  logic                    clk,
  input  logic                    rst_n,

  // From the legality filter. Consumed, NEVER recomputed (17.4 §3).
  input  logic [NUM_ENTRIES-1:0]  legal_mask,
  input  logic [NUM_ENTRIES-1:0]  is_xlate,
  input  logic [NUM_ENTRIES-1:0]  is_demand,
  input  logic [NUM_ENTRIES-1:0]  is_wb,
  input  logic [AGE_W-1:0]        age [NUM_ENTRIES],

  input  logic                    commit,

  output logic [NUM_ENTRIES-1:0]  grant,
  output logic [2:0]              binding_layer,
  output logic                    fairness_active
);
  initial begin
    if (AGE_URGENT > AGE_MAX)
      $fatal(1, "class_policy_layers: AGE_URGENT exceeds AGE_MAX -- the layer is unreachable");
    if (NUM_ENTRIES < 2) $fatal(1, "class_policy_layers: NUM_ENTRIES >= 2");
  end

  function automatic logic [NUM_ENTRIES-1:0] lowest(input logic [NUM_ENTRIES-1:0] m);
    return m & (~m + 1'b1);
  endfunction

  // A layer NARROWS, or passes through. This helper is the whole
  // mechanism of 17.4 §4, and writing it once makes each layer one
  // line -- which is the point: the structure is simple and the
  // ORDER is the design decision.
  function automatic logic [NUM_ENTRIES-1:0] narrow(
      input logic [NUM_ENTRIES-1:0] set,
      input logic [NUM_ENTRIES-1:0] pref);
    return (|(set & pref)) ? (set & pref) : set;
  endfunction

  logic [NUM_ENTRIES-1:0] aged, l0, l1, l2, l3;
  logic [$clog2(NUM_ENTRIES > 1 ? NUM_ENTRIES : 2)-1:0] rot_ptr;

  always_comb begin
    aged = '0;
    for (int i = 0; i < NUM_ENTRIES; i++)
      // The aged set is intersected with LEGAL, not with valid.
      // 31.1's module established that an override placed above
      // legality issues illegal commands; 30.5 §10 is the defect.
      if (legal_mask[i] && age[i] >= AGE_URGENT[AGE_W-1:0]) aged[i] = 1'b1;
  end

  always_comb begin
    // Layer 0 -- the legal set. Never widened.
    l0 = legal_mask;
    // Layer 1 -- FAIRNESS, above class so a starved entry of any
    // class is reachable (17.4 §9).
    l1 = narrow(l0, aged);
    // Layer 2 -- translation. §3's strongest obligation: a deadline
    // AND it blocks another access. Its 5% share is irrelevant here,
    // which is exactly what a weight could not achieve.
    l2 = narrow(l1, is_xlate);
    // Layer 3 -- demand. A deadline, nothing blocked behind it.
    l3 = narrow(l2, is_demand);
    // Writebacks and prefetches fall through to the rotation below,
    // which is correct: neither has a deadline, and §3 says the
    // response to pressure for the droppable one already happened at
    // admission (§9).
  end

  // Rotation, advanced on COMMIT rather than on grant -- 17.4 §7,
  // because a grant that does not commit must not move the pointer.
  always_ff @(posedge clk) begin
    if (!rst_n) rot_ptr <= '0;
    else if (commit) rot_ptr <= rot_ptr + 1'b1;
  end

  assign grant = lowest(l3);

  // Which layer actually narrowed the set. Reported so that "why did
  // this entry win" has an answer -- 30.5 §3's attribution argument,
  // applied to policy instead of to legality.
  always_comb begin
    if      (|aged && (l1 != l0))                binding_layer = 3'd1;
    else if (|(l1 & is_xlate)  && (l2 != l1))    binding_layer = 3'd2;
    else if (|(l2 & is_demand) && (l3 != l2))    binding_layer = 3'd3;
    else                                          binding_layer = 3'd4;  // rotation
  end
  assign fairness_active = |aged;
endmodule

   GRADE D geometry: QDEPTH = 32, so OCC_W = 6; CNT_W = 32.

   WITH the class mechanism (COHERENT = 1, HAS_PREFETCH = 1):
       drop_count           32
       admit_count          32
       classes_present       8
                            --
                            72 bits, plus a combinational decode

   WITHOUT it (HAS_PREFETCH = 0, COHERENT = 0):
       admit_count          32     (still worth having)
       classes_present       8
                            --
                            40 bits, and no drop path at all

   DERIVED: 72 bits against 40. The mechanism is CHEAP.

// ---------------------------------------------------------------------
// platform_address_decode -- INTENTIONALLY DEFECTIVE, for review (§12).
//
// CLASSIFICATION: synthesisable, grade-D values, and CONTAINS A BUG.
//
// WHAT IT IS MEANT TO DO: the five-clause contract above -- decode a
// physical address into channel, bank and row using field positions
// the PLATFORM supplies, because 18.4 §2 establishes that those
// positions are a grade-B fact and 18.4 §5 that "the" map is often a
// category error.
//
// WHY IT EXISTS HERE: §5's callout owns CATEGORY DRIFT -- a grade-C
// measurement loses its qualification through a slide and a wiki and
// is eventually consumed as grade A. This block is that drift in
// hardware, and it is the only defect in this module that could not
// have appeared in any earlier one.
//
// HOW TO RUN IT: bring the block up on a platform whose configured
// channel-field position differs from the compiled one.
// EXPECTED RESULT under clause 1: the decode follows the CONFIGURED
// position.
// EXPECTED TRACE: changing cfg_ch_bit must change sel_ch for the
// same address. It does not.
//
// SYNTHESIS: a variable bit-extract plus a validity gate.
//
// LIMITATIONS: decodes three fields. The complete field set, the
// inversion and the hashing options are 8.6's and 18.1's, and
// omitting them is STATED rather than hidden -- it is not the bug.
// ---------------------------------------------------------------------
module platform_address_decode #(
  parameter int ADDR_W  = 46,
  parameter int NUM_CH  = 4,
  parameter int NUM_BK  = 16,
  parameter int ROW_W   = 16,
  parameter int CH_W    = $clog2(NUM_CH),
  parameter int BK_W    = $clog2(NUM_BK),

  // GRADE D, and this is the whole problem. The value came from a
  // measurement on the first platform this block was brought up on
  // -- honest grade C at the moment it was taken (18.4 §1), written
  // here as a localparam-in-all-but-name and consumed below as
  // though it were grade A.
  parameter int CH_BIT_DEFAULT = 8
)(
  input  logic               clk,
  input  logic               rst_n,

  // The CONFIGURATION, from the platform's registers at
  // initialisation. Clause 1 says these are the answer.
  input  logic               cfg_valid,
  input  logic [5:0]         cfg_ch_bit,
  input  logic [5:0]         cfg_bk_bit,
  input  logic [5:0]         cfg_row_bit,

  input  logic               req_valid,
  input  logic [ADDR_W-1:0]  req_addr,

  output logic [CH_W-1:0]    sel_ch,
  output logic [BK_W-1:0]    sel_bk,
  output logic [ROW_W-1:0]   sel_row,
  output logic               decode_invalid,
  output logic [5:0]         cfg_in_use_ch
);
  initial begin
    if (CH_BIT_DEFAULT + CH_W > ADDR_W)
      $fatal(1, "platform_address_decode: channel field falls outside the address");
  end

  // Clause 2 and 5, HONOURED. The block refuses to decode before the
  // configuration is valid, and a reviewer checking "does it wait for
  // configuration?" finds that it does. This line is CORRECT, and it
  // is what conceals the defect.
  assign decode_invalid = req_valid && !cfg_valid;

  always_comb begin
    sel_ch  = '0;
    sel_bk  = '0;
    sel_row = '0;
    if (req_valid && cfg_valid) begin
      // <-- THE DEFECT: the compiled-in position is used, and
      //     cfg_ch_bit is never read.
      sel_ch  = req_addr[CH_BIT_DEFAULT +: CH_W];
      sel_bk  = req_addr[cfg_bk_bit  +: BK_W];
      sel_row = req_addr[cfg_row_bit +: ROW_W];
    end
  end

  // Clause 4, and it makes the bug FINDABLE rather than fixing it:
  // the block reports what it believes it is using.
  assign cfg_in_use_ch = CH_BIT_DEFAULT[5:0];
endmodule

   GRADE D throughout. NUM_CH = 4 so CH_W = 2.

   platform A, brought up first:
       cfg_ch_bit = 8   == CH_BIT_DEFAULT
       decode is CORRECT. every test passes. the constant is now
       "validated by bring-up".

   platform B, a different population and interleave granularity:
       cfg_ch_bit = 13
       the block still extracts addr[9:8].

   consequence, and it is NOT corruption:
       addr[9:8] is still a bijection onto 4 channels, so every
       address still maps to exactly one channel and every read
       still returns what was written there. NO DATA IS WRONG.

   what IS wrong: the INTERLEAVE GRANULARITY.
       intended  : channel changes every 2^13 = 8192 bytes
       actual    : channel changes every 2^8  =  256 bytes

   DERIVED: a stride-8192 access pattern that was designed to
   spread across all four channels now lands entirely on one,
   because bits [9:8] are constant across that stride. Four
   channels of hardware deliver the throughput of one.

      // CORRECTED. Clause 1: all three positions come from the
      // configuration. The compiled default is DELETED rather than
      // kept as a fallback -- a fallback recreates the bug on any
      // platform whose firmware did not write the register, and
      // clause 2 already says the correct behaviour there is to
      // REFUSE rather than to guess. 30.7 §9: an untrained value is
      // unknown, and unknown is not a default.
      sel_ch  = req_addr[cfg_ch_bit  +: CH_W];
      sel_bk  = req_addr[cfg_bk_bit  +: BK_W];
      sel_row = req_addr[cfg_row_bit +: ROW_W];

  // And clause 4 must report the CONFIGURED value, not the compiled
  // one -- otherwise the block's own traceability output confirms
  // the wrong answer, which is worse than having no output.
  assign cfg_in_use_ch = cfg_ch_bit;

// ---------------------------------------------------------------------
// class_mix_monitor -- verification/telemetry, CORRECT as written.
//
// CLASSIFICATION: synthesisable telemetry. Drives nothing. Grade-D
// parameter values.
//
// WHAT IT DOES: counts requests per class and per channel over a
// window, and reports both mixes plus the drop count.
//
// WHY IT EXISTS HERE: §7's proportions are grade D, so the ranking
// they produce is transferable and the numbers are not. This block
// replaces them with measurements. And §13's defect produces a
// signature only a CHANNEL mix can show -- extreme imbalance with no
// correctness failure -- so the two mixes are reported together.
//
// HOW TO RUN IT: run the real workload and read both mixes.
// EXPECTED RESULT: a stride-based pattern designed to interleave
// should show a near-uniform channel mix. Extreme concentration with
// zero errors is §13's signature.
//
// SYNTHESIS: NUM_CLASS + NUM_CH counters plus a max/min tracker.
// No divider.
//
// LIMITATIONS: measures DISTRIBUTION. It cannot see a decode that is
// wrong but uniform, and it cannot see a class the upstream protocol
// never labelled (§6). Both are STATED rather than implied --
// 27.3's independence discipline requires a monitor to say what it
// does not cover.
// ---------------------------------------------------------------------
module class_mix_monitor #(
  parameter int NUM_CLASS = 5,
  parameter int NUM_CH    = 4,
  parameter int WIN       = 1048576,
  // COUNT, not INDEX: a window in which EVERY request went to one
  // class or one channel must be representable, so each counter needs
  // $clog2(WIN + 1) bits. Sized to the "fair share" WIN / NUM_CH it
  // would saturate in exactly the concentrated case it exists to
  // detect, and report balance.
  parameter int CNT_W     = $clog2(WIN + 1),
  parameter int CL_W      = $clog2(NUM_CLASS > 1 ? NUM_CLASS : 2),
  parameter int CH_W      = $clog2(NUM_CH > 1 ? NUM_CH : 2)
)(
  input  logic              clk,
  input  logic              rst_n,

  input  logic              admit,
  input  logic              drop,
  input  logic [CL_W-1:0]   req_class,
  input  logic [CH_W-1:0]   sel_ch,
  input  logic              win_tick,

  output logic [CNT_W-1:0]  r_class   [NUM_CLASS],
  output logic [CNT_W-1:0]  r_ch_max,
  output logic [CNT_W-1:0]  r_ch_min,
  output logic [CNT_W-1:0]  r_drops,
  output logic [CNT_W-1:0]  r_total,
  output logic              concentrated,
  output logic              result_valid
);
  initial begin
    if (WIN < NUM_CH)
      $fatal(1, "class_mix_monitor: WIN must be >= NUM_CH or the channel mix is meaningless");
    if (NUM_CLASS < 1) $fatal(1, "class_mix_monitor: NUM_CLASS >= 1");
  end

  logic [CNT_W-1:0] c_class [NUM_CLASS];
  logic [CNT_W-1:0] c_ch    [NUM_CH];
  logic [CNT_W-1:0] c_drop, c_total;

  always_ff @(posedge clk) begin
    if (!rst_n) begin
      for (int i = 0; i < NUM_CLASS; i++) begin c_class[i] <= '0; r_class[i] <= '0; end
      for (int i = 0; i < NUM_CH;    i++) c_ch[i] <= '0;
      c_drop <= '0;  c_total <= '0;
      r_ch_max <= '0;
      // AND-accumulator discipline: a minimum tracker must start at
      // all-ones, or the first sample never wins and the reported
      // minimum stays zero -- which would report maximum
      // concentration on every window regardless of the traffic.
      r_ch_min <= '1;
      r_drops <= '0;  r_total <= '0;
      concentrated <= 1'b0;  result_valid <= 1'b0;
    end else if (win_tick) begin
      begin
        logic [CNT_W-1:0] mx, mn;
        mx = '0;
        mn = '1;
        for (int i = 0; i < NUM_CH; i++) begin
          if (c_ch[i] > mx) mx = c_ch[i];
          if (c_ch[i] < mn) mn = c_ch[i];
        end
        r_ch_max <= mx;
        r_ch_min <= mn;
        // §13's signature, cross-multiplied so no divider is needed:
        // a channel received more than three quarters of a window's
        // traffic while another received almost none. Reported as a
        // FLAG plus both endpoints rather than as a single ratio --
        // 27.5 refuses a lone percentage and 30.8 §11 requires a
        // derived statistic's range to be visible.
        concentrated <= (mx * 4 > c_total * 3) && (mn * NUM_CH * 4 < c_total);
      end
      for (int i = 0; i < NUM_CLASS; i++) begin
        r_class[i] <= c_class[i];
        c_class[i] <= '0;
      end
      for (int i = 0; i < NUM_CH; i++) c_ch[i] <= '0;
      r_drops      <= c_drop;
      r_total      <= c_total;
      c_drop       <= '0;
      c_total      <= '0;
      result_valid <= 1'b1;
    end else begin
      result_valid <= 1'b0;
      if (admit) begin
        if (c_class[req_class] != {CNT_W{1'b1}}) c_class[req_class] <= c_class[req_class] + 1'b1;
        if (c_ch[sel_ch]       != {CNT_W{1'b1}}) c_ch[sel_ch]       <= c_ch[sel_ch]       + 1'b1;
        if (c_total            != {CNT_W{1'b1}}) c_total            <= c_total            + 1'b1;
      end
      // Drops are counted SEPARATELY and are not in c_total, because
      // a dropped request never reached a channel. Folding them in
      // would make the channel mix's denominator disagree with its
      // numerators -- 30.8 §10's denominator error, avoided by
      // construction.
      if (drop && c_drop != {CNT_W{1'b1}}) c_drop <= c_drop + 1'b1;
    end
  end
endmodule

  // Offered as "proves the decode respects the platform configuration".
  // Clause 2 and 5. Correct, non-vacuous, and PASSES on the
  // defective block.
  property p_no_decode_before_config;
    @(posedge clk) disable iff (!rst_n)
      (req_valid && !cfg_valid) |-> decode_invalid;
  endproperty
  assert property (p_no_decode_before_config)
    else $error("a decode was attempted before the configuration was valid");

  // And the field-extraction property, which was written from the
  // same mental model as the design.
  property p_channel_from_default_position;
    @(posedge clk) disable iff (!rst_n)
      (req_valid && cfg_valid) |->
        (sel_ch == req_addr[CH_BIT_DEFAULT +: CH_W]);
  endproperty
  assert property (p_channel_from_default_position)
    else $error("channel select did not match the expected field");

  // Clause 1. It names cfg_ch_bit -- the signal the defective block
  // declares and never reads -- so it cannot pass while that signal
  // is ignored. Variety 2's and variety 4's repair together: the
  // property's reference is the CONFIGURATION, not a constant the
  // design also holds.
  property p_channel_follows_configuration;
    @(posedge clk) disable iff (!rst_n)
      (req_valid && cfg_valid) |->
        (sel_ch == ((req_addr >> cfg_ch_bit) & ((1 << CH_W) - 1)));
  endproperty
  assert property (p_channel_follows_configuration)
    else $error("channel select does not follow the configured field position");

  // Clause 3. A configuration change must take effect. This is the
  // property that catches a design which LATCHES the first
  // configuration it saw -- a different bug in the same family, and
  // one the defective block above would also exhibit.
  property p_config_change_takes_effect;
    @(posedge clk) disable iff (!rst_n)
      (req_valid && cfg_valid && !$stable(cfg_ch_bit)) |->
        (sel_ch == ((req_addr >> cfg_ch_bit) & ((1 << CH_W) - 1)));
  endproperty
  assert property (p_config_change_takes_effect)
    else $error("a configuration change did not take effect");

  // Clause 4, and it is the property that makes the block's own
  // traceability trustworthy. Reporting the compiled value would
  // CONFIRM the wrong answer, which §13 argues is worse than
  // reporting nothing.
  property p_reported_config_is_the_used_config;
    @(posedge clk) disable iff (!rst_n)
      cfg_valid |-> (cfg_in_use_ch == cfg_ch_bit);
  endproperty
  assert property (p_reported_config_is_the_used_config)
    else $error("the block reports a configuration it is not using");

  // And the runtime guard the correction creates (§13): a configured
  // position that does not fit must be REFUSED, not wrapped.
  property p_out_of_range_config_refused;
    @(posedge clk) disable iff (!rst_n)
      (req_valid && cfg_valid && (cfg_ch_bit + CH_W > ADDR_W)) |-> decode_invalid;
  endproperty
  assert property (p_out_of_range_config_refused)
    else $error("an out-of-range configured field position was used");

  // ---- Covers. The dimension this defect scales with is the
  //      CONFIGURATION VALUE, so per 31.3 §15's rule the cover must
  //      be on that value -- and specifically on it DIFFERING from
  //      the compiled default, which is the only case that separates
  //      the two designs.
  cover property (@(posedge clk) disable iff (!rst_n)
                  req_valid && cfg_valid && (cfg_ch_bit == CH_BIT_DEFAULT));
  cover property (@(posedge clk) disable iff (!rst_n)
                  req_valid && cfg_valid && (cfg_ch_bit != CH_BIT_DEFAULT));
  // A configuration CHANGE while running, for clause 3.
  cover property (@(posedge clk) disable iff (!rst_n)
                  cfg_valid && !$stable(cfg_ch_bit));
  // The refusal path, so clause 2 is known to have been exercised.
  cover property (@(posedge clk) disable iff (!rst_n) decode_invalid);

  // ---- The safety property of the whole class mechanism. A
  //      deadline-bearing or non-droppable request must NEVER be
  //      dropped, whatever the pressure. This is the one obligation
  //      the mechanism could violate catastrophically, and it names
  //      both axes of §3 rather than a priority number.
  property p_never_drop_an_obligation;
    @(posedge clk) disable iff (!rst_n)
      drop |-> (droppable && !deadline_bearing);
  endproperty
  assert property (p_never_drop_an_obligation)
    else $error("a non-droppable or deadline-bearing request was dropped");

  // Admission and drop must PARTITION the accepted requests: a valid
  // request is admitted, or dropped, or back-pressured -- never two
  // of those and never none silently. 17.5's contract depends on it.
  property p_request_is_accounted;
    @(posedge clk) disable iff (!rst_n)
      req_valid |-> ((admit ^ drop) || (!admit && !drop && !req_ready));
  endproperty
  assert property (p_request_is_accounted)
    else $error("a valid request was neither admitted, dropped, nor stalled");

  // 17.5's one-handshake-one-entry rule, at this boundary: a DROP
  // completes the handshake and must NOT create a queue entry. This
  // is the property that catches §4's forbidden design -- accept,
  // then discard -- which would leave the requester waiting forever.
  property p_drop_creates_no_entry;
    @(posedge clk) disable iff (!rst_n)
      (drop && req_ready) |=> $stable(q_occupancy) || admit_count != $past(admit_count);
  endproperty
  assert property (p_drop_creates_no_entry)
    else $error("a dropped request occupied a queue entry");

  // An unrecognised class must be treated as the STRONGEST
  // obligation, never dropped. 7.4's three-valued discipline: the
  // safe default for an unknown obligation is the strictest one.
  property p_unknown_class_never_dropped;
    @(posedge clk) disable iff (!rst_n)
      class_unknown |-> !drop;
  endproperty
  assert property (p_unknown_class_never_dropped)
    else $error("a request of unrecognised class was dropped");

  // The PLATFORM invariant, with the parameter in the ANTECEDENT and
  // not inside the claim -- 31.1 §14's test for whether a property
  // may be shared across configurations. It may.
  property p_no_shedding_without_prefetch;
    @(posedge clk) disable iff (!rst_n)
      (!HAS_PREFETCH) -> !drop;
  endproperty
  assert property (p_no_shedding_without_prefetch)
    else $error("a platform without a droppable class performed a drop");

  // Shedding must be BOUNDED in the other direction too (§4's third
  // consequence): below the threshold, nothing is dropped. Without
  // this, a design that drops every prefetch always satisfies the
  // safety property above and has silently disabled prefetching.
  property p_no_drop_below_threshold;
    @(posedge clk) disable iff (!rst_n)
      (q_occupancy < DROP_THRESH) |-> !drop;
  endproperty
  assert property (p_no_drop_below_threshold)
    else $error("a drop occurred below the pressure threshold");

  // ---- Covers: per class, per platform arm, and at the threshold.
  // Per CLASS, because the isolation of §3's axes holds only for the
  // classes the stimulus presented -- 31.3 §15's per-index rule,
  // applied to a class code.
  cover property (@(posedge clk) disable iff (!rst_n) admit && req_class == CL_DEMAND);
  cover property (@(posedge clk) disable iff (!rst_n) admit && req_class == CL_WB);
  cover property (@(posedge clk) disable iff (!rst_n) admit && req_class == CL_XLATE);
  cover property (@(posedge clk) disable iff (!rst_n) drop  && req_class == CL_PREF);
  // The BOUNDARY of the shedding threshold, so "the rule was
  // respected" is distinguishable from "the rule was exercised" --
  // 30.3 §10.
  cover property (@(posedge clk) disable iff (!rst_n)
                  req_valid && (q_occupancy == DROP_THRESH));
  // And the unrecognised-class path, which is a FINDING rather than a
  // fifth class: a non-zero count means the platform presented a
  // class this controller was not integrated to understand (§6).
  cover property (@(posedge clk) disable iff (!rst_n) class_unknown);