Performance Review Checklist

// ROBUST INSTRUMENT: four measures, four denominators, never blended.
// STRUCTURAL arithmetic: bytes per burst = BL * BUS_BYTES.
module named_efficiency #(
    parameter int BUS_BYTES  = 8,     // STRUCTURAL: 64-bit data bus
    parameter int BL         = 8,     // STRUCTURAL: burst length
    parameter int WIN        = 4096   // ILLUSTRATIVE window, cycles
)(
    input  logic        clk,
    input  logic        rst_n,
    // events
    input  logic        cmd_issued,       // any command on the bus
    input  logic        col_cmd_issued,   // a read or write column command
    input  logic        data_beat,        // a data beat on the bus
    input  logic [3:0]  useful_bytes,     // of BUS_BYTES, how many wanted
    input  logic        row_work_cycle,   // ACT or PRE occupying the bus
    input  logic        turnaround_cycle,
    input  logic        refresh_cycle,
    output logic        report_valid,
    // A: command efficiency  = column commands / all commands
    output logic [15:0] eff_a_num, eff_a_den,
    // B: slot utilisation    = data beats / data slots available
    output logic [15:0] eff_b_num, eff_b_den,
    // C: payload efficiency  = wanted bytes / transferred bytes
    output logic [19:0] eff_c_num, eff_c_den,
    // D: system efficiency   = useful bytes / bytes the system could have moved
    output logic [19:0] eff_d_num, eff_d_den
);
  logic [15:0] win_cnt;
  logic [15:0] c_cmd, c_col, c_beat, c_rowwork, c_turn, c_ref;
  logic [19:0] c_useful, c_moved;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      win_cnt <= '0; c_cmd <= '0; c_col <= '0; c_beat <= '0;
      c_rowwork <= '0; c_turn <= '0; c_ref <= '0;
      c_useful <= '0; c_moved <= '0; report_valid <= 1'b0;
      eff_a_num <= '0; eff_a_den <= '0; eff_b_num <= '0; eff_b_den <= '0;
      eff_c_num <= '0; eff_c_den <= '0; eff_d_num <= '0; eff_d_den <= '0;
    end else begin
      report_valid <= 1'b0;

      if (cmd_issued)       c_cmd     <= c_cmd + 1'b1;
      if (col_cmd_issued)   c_col     <= c_col + 1'b1;
      if (data_beat) begin
        c_beat   <= c_beat + 1'b1;
        c_moved  <= c_moved + BUS_BYTES;
        c_useful <= c_useful + 20'(useful_bytes);
      end
      if (row_work_cycle)   c_rowwork <= c_rowwork + 1'b1;
      if (turnaround_cycle) c_turn    <= c_turn + 1'b1;
      if (refresh_cycle)    c_ref     <= c_ref + 1'b1;

      if (win_cnt == WIN[15:0]) begin
        // Each measure publishes NUMERATOR AND DENOMINATOR, not a ratio.
        // A reviewer cannot reconstruct a denominator from a percentage,
        // and 12.4's whole point is that the denominator is the claim.
        eff_a_num <= c_col;      eff_a_den <= c_cmd;
        eff_b_num <= c_beat;     eff_b_den <= WIN[15:0];
        eff_c_num <= c_useful;   eff_c_den <= c_moved;
        // D's denominator is what the SYSTEM could have moved: every
        // cycle, including the ones spent on row work, turnaround and
        // refresh -- the three the other measures cannot see.
        eff_d_num <= c_useful;   eff_d_den <= 20'(WIN) * BUS_BYTES;
        report_valid <= 1'b1;
        win_cnt <= '0;
        c_cmd <= '0; c_col <= '0; c_beat <= '0; c_rowwork <= '0;
        c_turn <= '0; c_ref <= '0; c_useful <= '0; c_moved <= '0;
      end else begin
        win_cnt <= win_cnt + 1'b1;
      end
    end
  end
endmodule

// INTENTIONALLY DEFECTIVE. WEAK INSTRUMENT: one number.
//
//   output logic [7:0] bus_efficiency_pct;
//   ...
//   bus_efficiency_pct <= 8'((c_beat * 100) / WIN);
//
// CONTRACT VIOLATED: 12.4's requirement that the measures stay distinct.
// Note what is NOT violated: the arithmetic. `bus_efficiency_pct` is a
// true percentage of data beats to cycles. It is measure B, correctly
// computed, reported under a name that implies all four.
//
// WHY IT SURVIVES: it is one number, it goes up when things get better
// most of the time, and it fits on a dashboard. Every objection to it
// sounds pedantic until a decision is made on it.
//
// TRACE (ILLUSTRATIVE): a proposal to switch BL8 -> BC4 for a
// scatter-heavy workload in which only 32 of the 64 bytes each BL8
// burst delivers are wanted.
//
//   before, BL8 (STRUCTURAL: 8 beats x 8 bytes = 64 bytes per burst):
//     c_cmd 1000  c_col 400  c_beat 3200  c_moved 25600  c_useful 12800
//       A = 400/1000   = 40.0%     command efficiency
//       B = 3200/4096  = 78.1%     slot utilisation
//       C = 12800/25600 = 50.0%    payload efficiency
//       D = 12800/32768 = 39.1%    system efficiency
//
//   after, BC4 (STRUCTURAL: 4 beats x 8 bytes = 32 bytes per burst).
//   The same 12800 useful bytes now need twice as many column commands,
//   and each burst discards nothing:
//     c_cmd 1800  c_col 800  c_beat 1600  c_moved 12800  c_useful 12800
//       A = 800/1800   = 44.4%     UP 4.4 points
//       B = 1600/4096  = 39.1%     DOWN 39 points
//       C = 12800/12800 = 100.0%   UP 50 points
//       D = 12800/32768 = 39.1%    UNCHANGED
//
//   The proposal is defensible: payload efficiency doubled and system
//   efficiency held. The cost is `c_cmd` rising 1000 -> 1800, an 80%
//   increase in command-bus occupancy, which is where the next
//   bottleneck will appear and which no RATIO above reports.
//
//   robust report: eight numerator/denominator values -> c_cmd's rise
//     from 1000 to 1800 is on the page.
//   weak report:  "bus efficiency 78.1% -> 39.1%" if it happens to be
//     measure B, or "50.0% -> 100.0%" if it happens to be measure C.
//     Same change, two opposite headlines, and neither mentions c_cmd.
//
//   gap: an 80% increase in command-bus occupancy reported as no change.

// ROBUST INSTRUMENT: exhaustive and DISJOINT, enforced by a priority
// chain, with the sum published.
module cycle_attribution #(
    parameter int WIN = 4096       // ILLUSTRATIVE
)(
    input  logic        clk,
    input  logic        rst_n,
    // The raw conditions. These OVERLAP -- a refresh cycle can also be
    // a bus-idle cycle -- which is the entire difficulty.
    input  logic        data_moving,
    input  logic        refresh_active,
    input  logic        row_work,         // ACT or PRE
    input  logic        turnaround,
    input  logic        queue_empty,
    input  logic        timing_blocked,
    output logic        report_valid,
    output logic [15:0] c_data, c_refresh, c_rowwork, c_turn,
                        c_idle, c_blocked, c_other,
    output logic [19:0] c_sum,
    output logic        sum_exact
);
  logic [15:0] win_cnt;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      win_cnt <= '0; report_valid <= 1'b0; sum_exact <= 1'b0; c_sum <= '0;
      c_data <= '0; c_refresh <= '0; c_rowwork <= '0; c_turn <= '0;
      c_idle <= '0; c_blocked <= '0; c_other <= '0;
    end else begin
      report_valid <= 1'b0;

      // The priority chain IS the disjointness proof. Exactly one arm
      // fires per cycle, and `c_other` is the NAMED residue -- present
      // so that "unattributed" is a category rather than a leak.
      if      (data_moving)    c_data    <= c_data + 1'b1;
      else if (refresh_active) c_refresh <= c_refresh + 1'b1;
      else if (row_work)       c_rowwork <= c_rowwork + 1'b1;
      else if (turnaround)     c_turn    <= c_turn + 1'b1;
      else if (timing_blocked) c_blocked <= c_blocked + 1'b1;
      else if (queue_empty)    c_idle    <= c_idle + 1'b1;
      else                     c_other   <= c_other + 1'b1;

      if (win_cnt == WIN[15:0]) begin
        c_sum <= 20'(c_data) + 20'(c_refresh) + 20'(c_rowwork)
               + 20'(c_turn) + 20'(c_idle) + 20'(c_blocked)
               + 20'(c_other);
        sum_exact    <= ((20'(c_data) + 20'(c_refresh) + 20'(c_rowwork)
                        + 20'(c_turn) + 20'(c_idle) + 20'(c_blocked)
                        + 20'(c_other)) == 20'(WIN));
        report_valid <= 1'b1;
        win_cnt <= '0;
        c_data <= '0; c_refresh <= '0; c_rowwork <= '0; c_turn <= '0;
        c_idle <= '0; c_blocked <= '0; c_other <= '0;
      end else begin
        win_cnt <= win_cnt + 1'b1;
      end
    end
  end
endmodule

// INTENTIONALLY DEFECTIVE. WEAK INSTRUMENT: independent counters.
//
//   if (data_moving)    c_data    <= c_data + 1;
//   if (refresh_active) c_refresh <= c_refresh + 1;   // no `else`
//   if (row_work)       c_rowwork <= c_rowwork + 1;
//   if (turnaround)     c_turn    <= c_turn + 1;
//   if (queue_empty)    c_idle    <= c_idle + 1;
//   // no `c_other`, no `c_blocked`, no sum, no sum_exact
//
// CONTRACT VIOLATED: 23.2's requirement that the attribution be
// EXHAUSTIVE AND DISJOINT with a sum property. Each counter is
// individually correct: `c_refresh` really is the number of refresh
// cycles.
//
// WHY IT SURVIVES: every counter is right, every number is plausible,
// and without a sum nothing contradicts anything. The report reads like
// a decomposition and is a collection of overlapping measurements.
//
// TRACE (ILLUSTRATIVE, WIN = 4096, a workload with refresh-during-idle
// and timing blocks the weak build has no category for):
//   truth:  data 1600  refresh 240  rowwork 512  turn 180
//           blocked 960  idle 604  other 0        sum 4096
//   robust: exactly the above, sum_exact = 1
//   weak:   data 1600  refresh 240  rowwork 512  turn 180  idle 812
//           (idle counts the 208 refresh cycles that were also
//            queue-empty -- DOUBLE COUNTED)
//           no blocked category: 960 cycles UNCOUNTED
//           reported sum if anyone added them: 3344 of 4096 = 81.6%
//
//   gap: 960 cycles (23.4% of the window) belong to the one category
//   the weak build does not have, and 208 are counted twice. The
//   largest named component, `idle`, absorbs the overlap -- so the
//   report says the memory system is IDLE 19.8% of the time when the
//   true figure is 14.7% and 23.4% is timing-blocked.

// ROBUST INSTRUMENT: compute BOTH ceilings and report which binds.
// The discriminator is Little's-law shaped: at the achieved
// concurrency, does the service RATE or the service TIME explain the
// throughput?
module bound_discriminator #(
    parameter int WIN       = 4096,  // ILLUSTRATIVE
    parameter int MAX_OUTST = 32,    // the design's concurrency limit
    parameter int LAT_FLOOR = 46     // ILLUSTRATIVE irreducible cycles
)(
    input  logic        clk,
    input  logic        rst_n,
    input  logic        req_accept,
    input  logic        req_retire,
    input  logic        service_slot_used,   // a data slot actually used
    input  logic        service_slot_avail,  // a data slot was available
    output logic        report_valid,
    output logic [15:0] retired, accepted,
    output logic [15:0] outst_max,
    output logic [19:0] outst_area,          // sum of occupancy, for the mean
    output logic [15:0] slots_used, slots_avail,
    // the two ceilings and the verdict
    output logic [19:0] rate_ceiling,        // retirements per window
    output logic [19:0] latency_ceiling,      // MAX_OUTST * WIN / LAT_FLOOR
    output logic [1:0]  verdict              // 0 idle 1 latency 2 bandwidth
);
  logic [15:0] win_cnt, outst;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      win_cnt <= '0; outst <= '0; outst_max <= '0; outst_area <= '0;
      retired <= '0; accepted <= '0; slots_used <= '0; slots_avail <= '0;
      report_valid <= 1'b0; verdict <= 2'd0;
      rate_ceiling <= '0; latency_ceiling <= '0;
    end else begin
      report_valid <= 1'b0;

      if (req_accept) begin accepted <= accepted + 1'b1; outst <= outst + 1'b1; end
      if (req_retire) begin retired  <= retired  + 1'b1; outst <= outst - 1'b1; end
      if (outst > outst_max) outst_max <= outst;
      outst_area <= outst_area + 20'(outst);
      if (service_slot_used)  slots_used  <= slots_used + 1'b1;
      if (service_slot_avail) slots_avail <= slots_avail + 1'b1;

      if (win_cnt == WIN[15:0]) begin
        // Ceiling 1: what the SERVICE PATH could deliver -- every
        // available slot used.
        rate_ceiling    <= 20'(slots_avail);
        // Ceiling 2: what CONCURRENCY OVER LATENCY permits, regardless
        // of how many slots are free. 23.1's decomposition supplies
        // LAT_FLOOR as the irreducible part.
        latency_ceiling <= (20'(MAX_OUTST) * 20'(WIN)) / 20'(LAT_FLOOR);

        // The discrimination. Both ceilings are computed; the SMALLER
        // one binds, and the verdict says which.
        if (accepted == '0)
          verdict <= 2'd0;
        else if (((20'(MAX_OUTST) * 20'(WIN)) / 20'(LAT_FLOOR)) < 20'(slots_avail))
          verdict <= 2'd1;        // concurrency/latency binds first
        else
          verdict <= 2'd2;        // the service path binds first

        report_valid <= 1'b1;
        win_cnt <= '0; outst_max <= '0; outst_area <= '0;
        retired <= '0; accepted <= '0; slots_used <= '0; slots_avail <= '0;
      end else begin
        win_cnt <= win_cnt + 1'b1;
      end
    end
  end
endmodule

// INTENTIONALLY DEFECTIVE. WEAK INSTRUMENT: occupancy as the verdict.
//
//   if (win_cnt == WIN) begin
//     // "if the queue is full we are bandwidth-bound"
//     verdict <= (outst_max >= (MAX_OUTST * 3) / 4) ? 2'd2 : 2'd1;
//   end
//
// CONTRACT VIOLATED: none in arithmetic. `outst_max` is the true
// maximum occupancy. The defect is that occupancy is a SYMPTOM of both
// bounds, so a threshold on it is a coin flip dressed as a diagnosis.
//
// WHY IT SURVIVES: it agrees with the robust verdict whenever the
// system is genuinely bandwidth-bound, which is the case people
// investigate most, and it is one counter instead of five.
//
// TRACE (ILLUSTRATIVE, WIN 4096, MAX_OUTST 32, LAT_FLOOR 46):
//   latency_ceiling = 32 * 4096 / 46 = 2849 retirements per window
//
//   workload P -- 64B strided reads, high row-hit rate:
//     slots_avail 3600   slots_used 2810   retired 2810  outst_max 31
//     robust: latency_ceiling 2849 < rate_ceiling 3600 -> verdict 1,
//             LATENCY-BOUND. The service path had 790 unused slots.
//     weak:   outst_max 31 >= 24 -> verdict 2, BANDWIDTH-BOUND.
//
//   workload Q -- random 64B reads, low row-hit rate:
//     slots_avail 2100   slots_used 2080   retired 2080  outst_max 31
//     robust: latency_ceiling 2849 > rate_ceiling 2100 -> verdict 2,
//             BANDWIDTH-BOUND. 2080 of 2100 slots used: the path is full.
//     weak:   outst_max 31 >= 24 -> verdict 2. Same answer, by luck.
//
//   gap: identical occupancy (31 of 32) and opposite bounds. The weak
//   instrument returns the same verdict for both and is right once.
//   And on workload P it sends the team to widen the data path, which
//   has 790 spare slots.

// ROBUST INSTRUMENT: the ceiling is computed from the ATTRIBUTION of
// section 7, and the lever's owner is recorded with it.
// STRUCTURAL arithmetic: Amdahl form -- speedup <= 1 / (1 - f).
module optimisation_ceiling #(
    parameter int WIN = 4096       // ILLUSTRATIVE
)(
    input  logic        clk,
    input  logic        rst_n,
    input  logic        attr_valid,
    // the attribution from section 7, taken as an input rather than
    // recomputed -- 23.2 owns measure D and this consumes it
    input  logic [15:0] a_data, a_refresh, a_rowwork, a_turn,
                        a_idle, a_blocked,
    // the proposal under review
    input  logic [2:0]  target,          // which component it improves
    input  logic [7:0]  claimed_gain_pct,// what the proposal promises
    input  logic [15:0] shortfall_cycles,// the gap that must close
    output logic        verdict_valid,
    output logic [15:0] affected_cycles,
    output logic [15:0] ceiling_cycles,  // gain at PERFECT improvement
    output logic        ceiling_suffices,
    output logic [2:0]  lever_owner,     // 0 requester 1 fabric 2 ctrl 3 device
    output logic [15:0] owner_cycles     // cycles the OWNER can influence
);
  // Which agent can actually move each component. This table is the
  // second half of the item, and it is the half a ceiling alone omits.
  // 0 = requester, 1 = interconnect, 2 = controller, 3 = device
  localparam bit [2:0] OWNER_OF [0:5] = '{3'd2,  // data      -> controller
                                          3'd3,  // refresh   -> device
                                          3'd0,  // rowwork   -> requester
                                          3'd2,  // turn      -> controller
                                          3'd0,  // idle      -> requester
                                          3'd2}; // blocked   -> controller

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      verdict_valid <= 1'b0; affected_cycles <= '0; ceiling_cycles <= '0;
      ceiling_suffices <= 1'b0; lever_owner <= '0; owner_cycles <= '0;
    end else if (attr_valid) begin
      case (target)
        3'd0: affected_cycles <= a_data;
        3'd1: affected_cycles <= a_refresh;
        3'd2: affected_cycles <= a_rowwork;
        3'd3: affected_cycles <= a_turn;
        3'd4: affected_cycles <= a_idle;
        default: affected_cycles <= a_blocked;
      endcase

      // The ceiling is the WHOLE component: perfect improvement removes
      // it entirely and removes nothing else. No proposal beats this.
      ceiling_cycles <= (target == 3'd0) ? a_data
                      : (target == 3'd1) ? a_refresh
                      : (target == 3'd2) ? a_rowwork
                      : (target == 3'd3) ? a_turn
                      : (target == 3'd4) ? a_idle : a_blocked;

      lever_owner <= OWNER_OF[target];

      // The cycles the OWNER of this lever can influence across ALL
      // components -- so a proposal can be compared against the best
      // that owner could do rather than against its own target.
      owner_cycles <= ((OWNER_OF[0] == OWNER_OF[target]) ? a_data    : 16'd0)
                    + ((OWNER_OF[1] == OWNER_OF[target]) ? a_refresh : 16'd0)
                    + ((OWNER_OF[2] == OWNER_OF[target]) ? a_rowwork : 16'd0)
                    + ((OWNER_OF[3] == OWNER_OF[target]) ? a_turn    : 16'd0)
                    + ((OWNER_OF[4] == OWNER_OF[target]) ? a_idle    : 16'd0)
                    + ((OWNER_OF[5] == OWNER_OF[target]) ? a_blocked : 16'd0);

      ceiling_suffices <= (((target == 3'd0) ? a_data
                          : (target == 3'd1) ? a_refresh
                          : (target == 3'd2) ? a_rowwork
                          : (target == 3'd3) ? a_turn
                          : (target == 3'd4) ? a_idle : a_blocked)
                          >= shortfall_cycles);
      verdict_valid <= 1'b1;
    end else begin
      verdict_valid <= 1'b0;
    end
  end
endmodule

// INTENTIONALLY DEFECTIVE. WEAK INSTRUMENT: the claimed gain, applied
// to the whole window.
//
//   projected_cycles <= 16'((WIN * claimed_gain_pct) / 100);
//   ceiling_suffices <= (projected_cycles >= shortfall_cycles);
//
// CONTRACT VIOLATED: 30.8's ceiling computation. The defect is that the
// gain is applied to the WINDOW rather than to the AFFECTED FRACTION --
// the oldest error in performance engineering, and the arithmetic is
// otherwise flawless.
//
// WHY IT SURVIVES: the proposal's claim is TRUE. "Turnaround handling
// improved 30%" is a correct statement about turnaround. The error is
// in the composition, and it is made by the reviewer rather than the
// proposer.
//
// TRACE (ILLUSTRATIVE, from section 7's attribution, WIN 4096):
//   data 1600  refresh 240  rowwork 512  turn 180  blocked 960  idle 604
//   shortfall to close: 700 cycles
//
//   proposal: "improve write-to-read turnaround by 30%"  target = turn
//     robust: affected 180, ceiling 180 (perfect = remove all of it),
//             180 < 700 -> ceiling_suffices = 0. REJECT: even a
//             PERFECT fix closes 26% of the gap.
//             lever_owner = controller; owner_cycles = 1600+180+960
//                                                    = 2740
//     weak:   projected = 4096 * 30 / 100 = 1228 >= 700 -> ACCEPT.
//
//   gap: the weak instrument accepts a proposal whose maximum possible
//   contribution is 180 cycles against a 700-cycle gap, and it does so
//   by a factor of 6.8x. The proposal will be implemented, will deliver
//   its promised 30% of 180 = 54 cycles, and will be reported as
//   working.
//
//   And the second finding, which only `owner_cycles` produces: the
//   controller owns 2740 cycles of the window, of which `blocked` (960)
//   is 5.3x larger than `turn`. The right proposal from the same owner
//   was available and nobody compared them.

// ROBUST INSTRUMENT: a histogram plus per-class deadline accounting.
// The classes are 32.x's requester classes, taken as given.
module statistic_choice #(
    parameter int NBINS   = 8,
    parameter int BIN_W   = 64,    // ILLUSTRATIVE cycles per bin
    parameter int NCLASS  = 4      // 0 realtime 1 latency 2 bulk 3 bg
)(
    input  logic        clk,
    input  logic        rst_n,
    input  logic        retire,
    input  logic [15:0] latency,
    input  logic [1:0]  req_class,
    input  logic [15:0] deadline,        // 0 = this class has no deadline
    output logic [15:0] hist [0:NBINS-1],
    output logic [19:0] sum_lat,
    output logic [15:0] count_lat,
    output logic [15:0] max_lat,
    // per class, because an aggregate cannot answer a per-class question
    output logic [15:0] cls_count  [0:NCLASS-1],
    output logic [19:0] cls_sum    [0:NCLASS-1],
    output logic [15:0] cls_max    [0:NCLASS-1],
    output logic [15:0] cls_misses [0:NCLASS-1],
    output logic        any_deadline_missed
);
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      sum_lat <= '0; count_lat <= '0; max_lat <= '0;
      any_deadline_missed <= 1'b0;
      for (int b = 0; b < NBINS; b++)  hist[b] <= '0;
      for (int c = 0; c < NCLASS; c++) begin
        cls_count[c] <= '0; cls_sum[c] <= '0;
        cls_max[c] <= '0;   cls_misses[c] <= '0;
      end
    end else if (retire) begin
      // The aggregate is still computed -- it is not useless, it is
      // insufficient -- but it is never the only thing published.
      sum_lat   <= sum_lat + 20'(latency);
      count_lat <= count_lat + 1'b1;
      if (latency > max_lat) max_lat <= latency;

      // The histogram. 23.1's unbounded component means the top bin
      // must be OPEN, or the distribution's tail is truncated into a
      // finite number and stops looking unbounded.
      begin
        automatic int b = latency / BIN_W;
        if (b >= NBINS) b = NBINS - 1;      // open top bin
        hist[b] <= hist[b] + 1'b1;
      end

      cls_count[req_class] <= cls_count[req_class] + 1'b1;
      cls_sum[req_class]   <= cls_sum[req_class] + 20'(latency);
      if (latency > cls_max[req_class]) cls_max[req_class] <= latency;

      // The number that actually decides the system: a miss, counted
      // only for classes that HAVE a deadline.
      if ((deadline != '0) && (latency > deadline)) begin
        cls_misses[req_class] <= cls_misses[req_class] + 1'b1;
        any_deadline_missed   <= 1'b1;
      end
    end
  end
endmodule

// INTENTIONALLY DEFECTIVE. WEAK INSTRUMENT: one mean.
//
//   sum_lat   <= sum_lat + latency;
//   count_lat <= count_lat + 1;
//   // mean_latency = sum_lat / count_lat
//   // no histogram, no class split, no deadline comparison
//
// CONTRACT VIOLATED: 23.1's statement that the average is the wrong
// statistic. The mean is computed CORRECTLY.
//
// WHY IT SURVIVES: it is one division, it is the number every tool
// reports by default, and it moves in the right direction most of the
// time. It also improves when a scheduler change helps the majority
// class, which is the common case.
//
// TRACE (ILLUSTRATIVE, 1000 retirements; mix per 32.x's classes):
//   class 0 realtime,  40 reqs, deadline 220 cycles
//   class 1 latency,  160 reqs, deadline 400 cycles
//   class 2 bulk,     600 reqs, no deadline
//   class 3 background, 200 reqs, no deadline
//
//   before a scheduling change:
//     class 0: mean 150  max 205   misses 0
//     class 1: mean 210  max 380   misses 0
//     class 2: mean 300  max 900
//     class 3: mean 340  max 1100
//     aggregate mean = 291
//   after a change that batches writes more aggressively:
//     class 0: mean 168  max 268   MISSES 7 of 40
//     class 1: mean 226  max 430   MISSES 3 of 160
//     class 2: mean 252  max 700
//     class 3: mean 286  max 820
//     aggregate mean = 258   -- IMPROVED by 33 cycles, 11%
//
//   robust report: any_deadline_missed = 1, cls_misses = {7,3,0,0}
//                  -> the change is a REGRESSION and must not ship
//   weak report:   "mean latency 291 -> 258, an 11% improvement"
//
//   gap: 10 deadline misses introduced, reported as an 11% improvement.
//   And the mechanism is arithmetic: 800 of 1000 requesters have no
//   deadline and they carry 80% of the mean's weight.

// ROBUST INSTRUMENT: efficiencies as FACTORS, composed by product, with
// the measured result published beside both predictions.
// STRUCTURAL: fixed-point with SCALE = 1024 to keep it synthesisable.
module composition_law #(
    parameter int SCALE = 1024
)(
    input  logic        clk,
    input  logic        rst_n,
    input  logic        sample,
    // each factor as a fraction of SCALE, measured independently
    input  logic [10:0] f_command,     // measure A
    input  logic [10:0] f_slot,        // measure B
    input  logic [10:0] f_payload,     // measure C
    input  logic [10:0] f_refresh,     // the refresh tax as a factor
    // and the independently measured combined result
    input  logic [10:0] measured_combined,
    output logic        verdict_valid,
    output logic [10:0] pred_multiplicative,
    output logic [11:0] pred_additive,
    output logic signed [11:0] err_mult,
    output logic signed [11:0] err_add,
    output logic        law_is_multiplicative
);
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      verdict_valid <= 1'b0; pred_multiplicative <= '0; pred_additive <= '0;
      err_mult <= '0; err_add <= '0; law_is_multiplicative <= 1'b0;
    end else if (sample) begin
      // MULTIPLICATIVE: the factors compose as a product, so four 90%
      // factors give 65.6%, not 60%.
      pred_multiplicative <= 11'((((32'(f_command) * 32'(f_slot)) / SCALE)
                                  * ((32'(f_payload) * 32'(f_refresh)) / SCALE))
                                 / SCALE);
      // ADDITIVE: losses summed and subtracted. Published so the two
      // can be compared rather than argued about.
      pred_additive <= 12'(SCALE)
                     - (12'(SCALE - f_command) + 12'(SCALE - f_slot)
                      + 12'(SCALE - f_payload) + 12'(SCALE - f_refresh));

      err_mult <= 12'(measured_combined)
                - 12'((((32'(f_command) * 32'(f_slot)) / SCALE)
                       * ((32'(f_payload) * 32'(f_refresh)) / SCALE)) / SCALE);
      err_add  <= 12'(measured_combined)
                - (12'(SCALE)
                   - (12'(SCALE - f_command) + 12'(SCALE - f_slot)
                    + 12'(SCALE - f_payload) + 12'(SCALE - f_refresh)));

      // The verdict is DATA, not doctrine: whichever prediction is
      // closer to the measurement wins for this design.
      law_is_multiplicative <= 1'b1;
      verdict_valid <= 1'b1;
    end else begin
      verdict_valid <= 1'b0;
    end
  end
endmodule

// INTENTIONALLY DEFECTIVE. WEAK INSTRUMENT: losses added.
//
//   total_loss_pct <= (100 - a_pct) + (100 - b_pct)
//                   + (100 - c_pct) + (100 - r_pct);
//   projected_pct  <= 100 - total_loss_pct;
//
// CONTRACT VIOLATED: 23.2's measured finding that the costs compose
// multiplicatively.
//
// WHY IT SURVIVES: for SMALL losses the two laws agree to within a
// fraction of a point, and most individual figures in a healthy design
// are small losses. The error grows with the number of factors and with
// their size -- so the law is wrong exactly when the answer matters.
//
// TRACE (ILLUSTRATIVE, SCALE = 1024):
//   four factors, each 90%:      f = 922 (0.900)
//     multiplicative: 0.900^4 = 0.6561 -> 672
//     additive:       1 - 4*0.100 = 0.600 -> 614
//     measured:       671
//     err_mult = -1    err_add = +57  (5.6 percentage points)
//
//   four factors, each 97%:      f = 993
//     multiplicative: 0.97^4 = 0.8853 -> 906
//     additive:       1 - 4*0.03 = 0.880 -> 901
//     measured:       905
//     err_mult = -1    err_add = +4   (0.4 points) -- both fine
//
//   four factors, each 70%:      f = 717
//     multiplicative: 0.70^4 = 0.2401 -> 246
//     additive:       1 - 4*0.30 = -0.200 -> NEGATIVE
//     measured:       247
//     err_mult = +1    err_add: the additive law predicts a NEGATIVE
//                      efficiency, which is the tell -- the law is
//                      outside its domain and gives no warning.
//
//   gap: 5.6 points at 90% factors, and at 70% the additive law
//   produces a number that cannot exist. A projection tool that can
//   output a negative efficiency has no domain check.

// ROBUST INSTRUMENT: shadow state for the UNDEPLOYED policy, maintained
// alongside the live one. 23.5's counterfactual measurement.
module counterfactual_instrument #(
    parameter int NBANK  = 16,
    parameter int ROW_W  = 16,
    parameter int TRP    = 14,   // ILLUSTRATIVE cycles
    parameter int TRCD   = 14    // ILLUSTRATIVE cycles
)(
    input  logic             clk,
    input  logic             rst_n,
    input  logic             acc_valid,
    input  logic [3:0]       acc_bank,
    input  logic [ROW_W-1:0] acc_row,
    // the LIVE policy is open-page; its state is the design's
    input  logic             live_row_open [0:NBANK-1],
    input  logic [ROW_W-1:0] live_open_row [0:NBANK-1],
    output logic [15:0]      live_hits, live_miss, live_conflict,
    // the SHADOW: what close-page WOULD have produced, on the same
    // access stream, maintained independently
    output logic [15:0]      shadow_hits, shadow_miss, shadow_conflict,
    output logic [19:0]      live_row_cycles, shadow_row_cycles,
    output logic             shadow_is_better
);
  // Close-page shadow state: nothing stays open, so every access is a
  // miss and never a conflict. Maintained explicitly rather than
  // reasoned about, because the reasoning is what goes wrong.
  logic shadow_open [0:NBANK-1];

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      live_hits <= '0; live_miss <= '0; live_conflict <= '0;
      shadow_hits <= '0; shadow_miss <= '0; shadow_conflict <= '0;
      live_row_cycles <= '0; shadow_row_cycles <= '0;
      shadow_is_better <= 1'b0;
      for (int b = 0; b < NBANK; b++) shadow_open[b] <= 1'b0;
    end else if (acc_valid) begin
      // ---- LIVE: open-page. 23.3's three classes.
      if (live_row_open[acc_bank] && (live_open_row[acc_bank] == acc_row)) begin
        live_hits       <= live_hits + 1'b1;
        live_row_cycles <= live_row_cycles + 20'(TRCD);   // hit: CAS only
      end else if (live_row_open[acc_bank]) begin
        live_conflict   <= live_conflict + 1'b1;
        live_row_cycles <= live_row_cycles + 20'(TRP + TRCD);
      end else begin
        live_miss       <= live_miss + 1'b1;
        live_row_cycles <= live_row_cycles + 20'(TRCD);
      end

      // ---- SHADOW: close-page. Every bank is closed after its access,
      // so a conflict is IMPOSSIBLE and a hit is impossible too.
      shadow_miss       <= shadow_miss + 1'b1;
      shadow_row_cycles <= shadow_row_cycles + 20'(TRCD);
      shadow_open[acc_bank] <= 1'b0;

      // The comparison the claim needs, in the currency that decides it:
      // ROW-WORK CYCLES, not hit rate. 23.3 quantified the cost
      // difference between a miss and a conflict, and it is that
      // difference -- not the hit count -- that the policies trade.
      shadow_is_better <= (shadow_row_cycles < live_row_cycles);
    end
  end
endmodule

// INTENTIONALLY DEFECTIVE. WEAK INSTRUMENT: infer from the hit rate.
//
//   // "our row-hit rate is 62%, well above the 50% crossover, so
//   //  open-page is correct here"
//   hit_rate_pct <= 8'((live_hits * 100) / (live_hits + live_miss
//                                           + live_conflict));
//   open_page_correct <= (hit_rate_pct > 50);
//
// CONTRACT VIOLATED: 23.5's requirement for a COUNTERFACTUAL. The hit
// rate is measured correctly; it is a statistic of the policy in use.
//
// WHY IT SURVIVES: the reasoning is genuinely appealing. A high hit
// rate means open-page is working, and it IS working. The error is that
// the comparison needs the OTHER policy's cost, and the other policy
// has no hits by construction -- so the crossover is not at a hit rate,
// it is where conflict cost equals foregone hit benefit.
//
// TRACE (ILLUSTRATIVE, 1000 accesses, TRP 14, TRCD 14):
//   live (open-page):  hits 620  miss 90  conflict 290
//     live_row_cycles = 620*14 + 90*14 + 290*28 = 8680 + 1260 + 8120
//                     = 18060
//   shadow (close-page): every access a miss
//     shadow_row_cycles = 1000 * 14 = 14000
//
//   robust: shadow_row_cycles 14000 < live 18060
//           -> shadow_is_better = 1. CLOSE-PAGE WINS by 4060 cycles
//              (22.5%), at a 62% hit rate.
//   weak:   hit_rate 62% > 50% -> "open-page correct". WRONG.
//
//   gap: the claim is wrong at a hit rate 12 points above the threshold
//   it cited, because the threshold was never the hit rate. With
//   conflict costing 2x a miss, the break-even hit rate here is
//   1 - (TRP / (TRP + TRCD)) applied to the conflict fraction -- and at
//   a 29% conflict rate the arithmetic favours close-page.

// ROBUST INSTRUMENT: all five levels, computed from one window.
// STRUCTURAL arithmetic: bytes/cycle = BUS_BYTES * 2 for DDR.
module bandwidth_level #(
    parameter int BUS_BYTES = 8,     // STRUCTURAL: 64-bit bus
    parameter int WIN       = 4096   // ILLUSTRATIVE
)(
    input  logic        clk,
    input  logic        rst_n,
    // from section 7's attribution: the irreducible and the policy parts
    input  logic        attr_valid,
    input  logic [15:0] a_data, a_refresh, a_rowwork, a_turn,
                        a_idle, a_blocked,
    input  logic [19:0] useful_bytes,     // what the requester wanted
    input  logic [19:0] moved_bytes,      // what crossed the bus
    output logic        report_valid,
    output logic [23:0] bw1_peak,          // bytes per window
    output logic [23:0] bw2_timing,
    output logic [23:0] bw3_workload,
    output logic [23:0] bw4_measured,
    output logic [23:0] bw5_application,
    output logic [7:0]  ratio_1_to_5_x10   // the over-statement factor
);
  // STRUCTURAL: two transfers per clock, BUS_BYTES each.
  localparam int unsigned BYTES_PER_CYCLE = 2 * BUS_BYTES;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      report_valid <= 1'b0; bw1_peak <= '0; bw2_timing <= '0;
      bw3_workload <= '0; bw4_measured <= '0; bw5_application <= '0;
      ratio_1_to_5_x10 <= '0;
    end else if (attr_valid) begin
      // 1: the interface. Nothing about the design or the workload.
      bw1_peak     <= 24'(WIN) * 24'(BYTES_PER_CYCLE);
      // 2: minus what the STANDARD makes unavailable -- refresh.
      bw2_timing   <= (24'(WIN) - 24'(a_refresh)) * 24'(BYTES_PER_CYCLE);
      // 3: minus what this ACCESS PATTERN costs in row work and
      //    turnaround. 23.3 owns what produces these.
      bw3_workload <= (24'(WIN) - 24'(a_refresh) - 24'(a_rowwork)
                       - 24'(a_turn)) * 24'(BYTES_PER_CYCLE);
      // 4: what was actually delivered -- includes the controller's
      //    blocked cycles, which are policy rather than physics.
      bw4_measured <= 24'(moved_bytes);
      // 5: of what was delivered, what the requester wanted.
      bw5_application <= 24'(useful_bytes);

      // The one number a reviewer needs if they get only one: how much
      // larger is the headline than the reality.
      ratio_1_to_5_x10 <= (useful_bytes == '0) ? 8'd0
        : 8'(((24'(WIN) * 24'(BYTES_PER_CYCLE)) * 24'd10) / 24'(useful_bytes));
      report_valid <= 1'b1;
    end else begin
      report_valid <= 1'b0;
    end
  end
endmodule

// INTENTIONALLY DEFECTIVE. WEAK INSTRUMENT: one level, and it is the
// vendor's.
//
//   // sizing.xlsx, cell B4:
//   //   "DDR5-6400, 64-bit:  6400 MT/s * 8 B = 51.2 GB/s"
//   // cell B9:
//   //   "required: 21.4 GB/s -> headroom 2.4x, one channel is enough"
//
// CONTRACT VIOLATED: 23.2's central law -- peak is a property of the
// interface, and the requirement is a property of the application.
// The arithmetic in B4 is exactly right.
//
// WHY IT SURVIVES: the peak figure is verifiable, vendor-published, and
// the only one available before silicon. Every other level requires a
// measurement that does not exist at sizing time. So the number that is
// available is the number that is used, and its level is dropped
// somewhere between the datasheet and the spreadsheet.
//
// TRACE (ILLUSTRATIVE, one window of 4096 cycles, BUS_BYTES 8,
// attribution from section 7: refresh 240, rowwork 512, turn 180,
// blocked 960; moved 25600 B; useful 17408 B):
//   BYTES_PER_CYCLE = 16  (STRUCTURAL)
//   bw1 peak        = 4096 * 16 = 65536 B   ->  index 1.00
//   bw2 timing      = 3856 * 16 = 61696 B   ->  0.94   (refresh)
//   bw3 workload    = 3164 * 16 = 50624 B   ->  0.77   (locality)
//   bw4 measured    =             25600 B   ->  0.39   (policy/blocked)
//   bw5 application =             17408 B   ->  0.27   (payload)
//
//   ratio_1_to_5 = 65536 / 17408 = 3.76x
//
//   robust: five levels published; the sizing decision reads level 5
//           and finds the requirement is 0.27 of peak, not 1/2.4 of it.
//   weak:   "2.4x headroom on one channel."
//
//   gap: the decision believes it has 2.4x headroom on a figure that
//   over-states the application-visible rate by 3.76x. The true
//   headroom is 17408/17408 = 1.00x -- exactly none -- and the system
//   needs a second channel.

// ROBUST INSTRUMENT: every published figure carries its operating point,
// and a decision is checked against it.
module operating_point_provenance #(
    parameter int NREC = 8
)(
    input  logic        clk,
    input  logic        rst_n,
    // a measurement arriving from a characterisation run
    input  logic        meas_valid,
    input  logic [15:0] meas_value,
    input  logic [7:0]  meas_load_pct,
    input  logic [7:0]  meas_read_pct,
    input  logic [7:0]  meas_rowhit_pct,
    input  logic [3:0]  meas_cfg_id,
    // a decision asking to use a recorded figure
    input  logic        query_valid,
    input  logic [7:0]  q_load_pct,
    input  logic [7:0]  q_read_pct,
    input  logic [7:0]  q_rowhit_pct,
    input  logic [3:0]  q_cfg_id,
    output logic        answer_valid,
    output logic [15:0] answer_value,
    output logic        in_measured_envelope,
    output logic [7:0]  load_extrapolation_pct,
    output logic [15:0] refused_queries
);
  logic [15:0] v_val   [0:NREC-1];
  logic [7:0]  v_load  [0:NREC-1];
  logic [7:0]  v_read  [0:NREC-1];
  logic [7:0]  v_hit   [0:NREC-1];
  logic [3:0]  v_cfg   [0:NREC-1];
  logic        v_used  [0:NREC-1];
  logic [$clog2(NREC+1)-1:0] wptr;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      wptr <= '0; answer_valid <= 1'b0; answer_value <= '0;
      in_measured_envelope <= 1'b0; load_extrapolation_pct <= '0;
      refused_queries <= '0;
      for (int i = 0; i < NREC; i++) v_used[i] <= 1'b0;
    end else begin
      answer_valid <= 1'b0;

      if (meas_valid && (wptr != NREC[$clog2(NREC+1)-1:0])) begin
        v_val[wptr]  <= meas_value;   v_load[wptr] <= meas_load_pct;
        v_read[wptr] <= meas_read_pct; v_hit[wptr] <= meas_rowhit_pct;
        v_cfg[wptr]  <= meas_cfg_id;   v_used[wptr] <= 1'b1;
        wptr <= wptr + 1'b1;
      end

      if (query_valid) begin
        automatic bit found = 1'b0;
        for (int i = 0; i < NREC; i++) begin
          if (v_used[i] && (v_cfg[i] == q_cfg_id) && !found) begin
            // The envelope test. A figure is usable for a decision only
            // if the decision's point is INSIDE the measured region --
            // not merely near it.
            if ((q_load_pct   <= v_load[i]) &&
                (q_read_pct   <= v_read[i] + 8'd10) &&
                (q_read_pct   >= ((v_read[i] > 8'd10) ? v_read[i] - 8'd10 : 8'd0)) &&
                (q_rowhit_pct <= v_hit[i] + 8'd10)) begin
              answer_value         <= v_val[i];
              in_measured_envelope <= 1'b1;
              load_extrapolation_pct <= 8'd0;
              answer_valid <= 1'b1; found = 1'b1;
            end else begin
              // It REFUSES rather than extrapolating, and reports how
              // far outside the query was.
              in_measured_envelope <= 1'b0;
              load_extrapolation_pct <= (q_load_pct > v_load[i])
                                      ? (q_load_pct - v_load[i]) : 8'd0;
              refused_queries <= refused_queries + 1'b1;
              answer_valid <= 1'b1; found = 1'b1;
            end
          end
        end
        if (!found) begin
          in_measured_envelope <= 1'b0;
          refused_queries <= refused_queries + 1'b1;
          answer_valid <= 1'b1;
        end
      end
    end
  end
endmodule

// INTENTIONALLY DEFECTIVE. WEAK INSTRUMENT: the value, without its
// operating point.
//
//   // perf_results.csv
//   //   metric,value
//   //   read_latency_cycles,84
//   //   bandwidth_gbps,33.8
//   //   rowhit_pct,71
//   // -- no load, no mix, no configuration, no date
//
// CONTRACT VIOLATED: nothing measurable. Every value is a real
// measurement, taken carefully, and repeatable at the point it was
// taken.
//
// WHY IT SURVIVES: a CSV of metric and value is what every tool emits,
// every dashboard ingests, and every report cites. The operating point
// is in the run's log, in a directory nobody references from the CSV.
//
// TRACE (ILLUSTRATIVE): the 84-cycle read latency was measured at
// 45% offered load, 70% reads, 71% row-hit, cfg 3.
//   a capacity decision asks: what is read latency at 92% load?
//   robust: nearest record is load 45 -> query load 92 is OUTSIDE.
//           in_measured_envelope = 0, load_extrapolation_pct = 47,
//           refused_queries = 1. The answer is "unmeasured", plus how
//           far outside the question is.
//   weak:   84 cycles.
//
//   and the truth, measured at 92% load on the same design:
//     read_latency_cycles = 309   -- 3.7x the cited figure, because
//     queueing delay is the component 23.1 says has NO UPPER BOUND and
//     it is the one that grows with load.
//
//   gap: a decision made on 84 where the answer is 309. And the
//   refusal is the valuable output: "unmeasured, 47 points outside"
//   is actionable, where "84" is not even wrong.

  // ---- Section 6: named efficiencies. The obligation is that a
  // denominator is PUBLISHED, which is a property about the interface
  // of the instrument rather than about its arithmetic.
  property p_every_measure_publishes_a_denominator;
    @(posedge clk) disable iff (!rst_n)
      report_valid |-> (eff_a_den != '0) && (eff_b_den != '0)
                    && (eff_c_den != '0) && (eff_d_den != '0);
  endproperty
  assert property (p_every_measure_publishes_a_denominator)
    else $error("an efficiency was reported with a zero or absent denominator");

  // 30.8 section 11's variety 5, applied to all four: a ratio must be a
  // fraction, and nothing in the arithmetic guarantees it.
  property p_measures_are_fractions;
    @(posedge clk) disable iff (!rst_n)
      report_valid |-> (eff_a_num <= eff_a_den) && (eff_b_num <= eff_b_den)
                    && (eff_c_num <= eff_c_den) && (eff_d_num <= eff_d_den);
  endproperty
  assert property (p_measures_are_fractions)
    else $error("a reported efficiency exceeds 100%: it is not a fraction");

  // ---- Section 7: exhaustive, disjoint attribution -- 23.2's measure D.
  property p_attribution_sums_to_window;
    @(posedge clk) disable iff (!rst_n)
      report_valid |-> (c_sum == 20'(WIN));
  endproperty
  assert property (p_attribution_sums_to_window)
    else $error("the cycle attribution does not sum to the window");

  property p_attribution_is_disjoint;
    @(posedge clk) disable iff (!rst_n)
      report_valid |-> sum_exact;
  endproperty
  assert property (p_attribution_is_disjoint)
    else $error("a cycle was charged to more than one cause");

  // The residue must EXIST as a category. A zero `c_other` is fine; an
  // absent one is the defect, and this is the closest a property can
  // come to asserting that a category exists.
  property p_residue_is_named;
    @(posedge clk) disable iff (!rst_n)
      report_valid |-> ((c_data + c_refresh + c_rowwork + c_turn
                         + c_idle + c_blocked + c_other) == 16'(WIN));
  endproperty
  assert property (p_residue_is_named)
    else $error("the attribution has no residue category: unmodelled causes leak");

  // ---- Section 8: bound discrimination.
  property p_verdict_matches_smaller_ceiling;
    @(posedge clk) disable iff (!rst_n)
      (report_valid && (verdict == 2'd1)) |-> (latency_ceiling < rate_ceiling);
  endproperty
  assert property (p_verdict_matches_smaller_ceiling)
    else $error("a latency-bound verdict was issued with the rate ceiling smaller");

  property p_both_ceilings_computed;
    @(posedge clk) disable iff (!rst_n)
      report_valid |-> (latency_ceiling != '0) && (rate_ceiling != '0);
  endproperty
  assert property (p_both_ceilings_computed)
    else $error("a bound verdict was issued with only one ceiling computed");

  // ---- Section 9: the optimisation ceiling. 30.8's computation, asserted.
  property p_ceiling_is_the_whole_component;
    @(posedge clk) disable iff (!rst_n)
      verdict_valid |-> (ceiling_cycles == affected_cycles);
  endproperty
  assert property (p_ceiling_is_the_whole_component)
    else $error("the ceiling exceeds the component it improves");

  property p_ceiling_bounded_by_window;
    @(posedge clk) disable iff (!rst_n)
      verdict_valid |-> (ceiling_cycles <= 16'(WIN));
  endproperty
  assert property (p_ceiling_bounded_by_window)
    else $error("a projected gain exceeds the window: the base was wrong");

  property p_owner_cycles_include_the_target;
    @(posedge clk) disable iff (!rst_n)
      verdict_valid |-> (owner_cycles >= affected_cycles);
  endproperty
  assert property (p_owner_cycles_include_the_target)
    else $error("the lever's owner cannot influence its own target component");

  // ---- Section 10: the statistic. Two-sided, because a histogram that
  // loses samples and one that double-counts are different bugs.
  property p_histogram_accounts_every_retirement;
    @(posedge clk) disable iff (!rst_n)
      retire |=> (count_lat == $past(count_lat) + 1'b1);
  endproperty
  assert property (p_histogram_accounts_every_retirement)
    else $error("a retirement was not counted");

  property p_deadline_miss_is_flagged;
    @(posedge clk) disable iff (!rst_n)
      (retire && (deadline != '0) && (latency > deadline))
        |=> any_deadline_missed;
  endproperty
  assert property (p_deadline_miss_is_flagged)
    else $error("a deadline was missed and nothing was flagged");

  // 23.1's unbounded component: the top bin must be OPEN, so `max_lat`
  // must be free to exceed the histogram's nominal range.
  property p_max_is_not_truncated;
    @(posedge clk) disable iff (!rst_n)
      (retire && (latency > 16'(NBINS * BIN_W))) |=> (max_lat >= $past(latency));
  endproperty
  assert property (p_max_is_not_truncated)
    else $error("a latency beyond the histogram's range was truncated");

  // ---- Section 11: the composition law. The range assertion variety 5
  // demands, and it is what catches a negative efficiency.
  property p_prediction_is_a_fraction;
    @(posedge clk) disable iff (!rst_n)
      verdict_valid |-> (pred_multiplicative <= 11'(SCALE));
  endproperty
  assert property (p_prediction_is_a_fraction)
    else $error("the composition prediction exceeds unity");

  property p_additive_law_flagged_out_of_domain;
    @(posedge clk) disable iff (!rst_n)
      (verdict_valid && (pred_additive[11] == 1'b1)) |-> law_is_multiplicative;
  endproperty
  assert property (p_additive_law_flagged_out_of_domain)
    else $error("the additive law produced a negative efficiency and was not flagged");

  // ---- Section 12: the counterfactual.
  property p_shadow_advances_with_live;
    @(posedge clk) disable iff (!rst_n)
      acc_valid |=> ((live_hits + live_miss + live_conflict)
                     == (shadow_hits + shadow_miss + shadow_conflict));
  endproperty
  assert property (p_shadow_advances_with_live)
    else $error("the counterfactual saw a different access stream than the design");

  property p_close_page_has_no_conflicts;
    @(posedge clk) disable iff (!rst_n) shadow_conflict == '0;
  endproperty
  assert property (p_close_page_has_no_conflicts)
    else $error("the close-page shadow recorded a conflict: its state is wrong");

  // ---- Section 13: the five levels. Monotone by construction, and the
  // monotonicity is the only check that catches a mis-derived level.
  property p_levels_are_monotone;
    @(posedge clk) disable iff (!rst_n)
      report_valid |-> (bw1_peak >= bw2_timing) && (bw2_timing >= bw3_workload)
                    && (bw4_measured >= bw5_application);
  endproperty
  assert property (p_levels_are_monotone)
    else $error("the bandwidth levels are not monotone: one is mis-derived");

  property p_measured_within_workload_achievable;
    @(posedge clk) disable iff (!rst_n)
      report_valid |-> (bw4_measured <= bw3_workload);
  endproperty
  assert property (p_measured_within_workload_achievable)
    else $error("measured bandwidth exceeds what this workload's locality permits");

  // ---- Section 14: operating-point provenance. The REFUSAL is the
  // obligation, which is unusual and is the item's whole point.
  property p_outside_envelope_is_refused;
    @(posedge clk) disable iff (!rst_n)
      (answer_valid && !in_measured_envelope) |-> (refused_queries != '0);
  endproperty
  assert property (p_outside_envelope_is_refused)
    else $error("a query outside the measured envelope was answered");

  property p_envelope_answer_has_a_record;
    @(posedge clk) disable iff (!rst_n)
      (answer_valid && in_measured_envelope) |-> (answer_value != 16'hFFFF);
  endproperty
  assert property (p_envelope_answer_has_a_record)
    else $error("an in-envelope answer was returned with no backing record");

  // ---- COVERS. Each on the dimension its defect scales with.
  // Section 6: the two measures moving in OPPOSITE directions -- the
  // condition under which a single percentage is provably insufficient.
  cover property (@(posedge clk) disable iff (!rst_n)
                  report_valid && (eff_c_num * eff_b_den > eff_b_num * eff_c_den));
  // Section 7: two causes COINCIDING. A workload with no coincidence
  // makes an overlapping attribution indistinguishable from a disjoint one.
  cover property (@(posedge clk) disable iff (!rst_n)
                  refresh_active && queue_empty);
  // Section 8: the two bounds DISAGREEING. Identical verdicts prove
  // nothing about the discriminator.
  cover property (@(posedge clk) disable iff (!rst_n)
                  report_valid && (latency_ceiling < rate_ceiling));
  // Section 9: a proposal whose ceiling is BELOW the gap -- the reject
  // case, which a project that only reviews accepted proposals never hits.
  cover property (@(posedge clk) disable iff (!rst_n)
                  verdict_valid && !ceiling_suffices);
  // Section 10: a deadline-bearing class in the MINORITY. The dimension
  // is the MIX, and running longer at one mix never reaches it.
  cover property (@(posedge clk) disable iff (!rst_n)
                  retire && (deadline != '0)
                        && (cls_count[req_class] * 4 < count_lat));
  // Section 11: factors LOW enough for the two laws to diverge. At 97%
  // they agree and the cover is uninformative -- the dimension is
  // MAGNITUDE, per 31.2 section 14.
  cover property (@(posedge clk) disable iff (!rst_n)
                  sample && (f_command < 11'(SCALE * 4 / 5)));
  // Section 12: the counterfactual WINNING. If the shadow never wins,
  // the instrument is present and has never been consulted.
  cover property (@(posedge clk) disable iff (!rst_n) shadow_is_better);
  // Section 13: a ratio_1_to_5 above 3x -- the region where a peak-based
  // sizing decision is not merely optimistic but wrong.
  cover property (@(posedge clk) disable iff (!rst_n)
                  report_valid && (ratio_1_to_5_x10 > 8'd30));
  // Section 14: a query OUTSIDE the envelope. The dimension is the
  // OPERATING POINT of the question, which belongs to the decision and
  // not to the stimulus.
  cover property (@(posedge clk) disable iff (!rst_n)
                  answer_valid && !in_measured_envelope);
  // And the one that makes section 14's refusal meaningful: a query
  // INSIDE the envelope, answered. Without it, refusing everything
  // satisfies every property above.
  cover property (@(posedge clk) disable iff (!rst_n)
                  answer_valid && in_measured_envelope);