DDR Bandwidth

  window                                     160
  DATA              10 pairs x 8 cycles    =  80
  TURNAROUND        10 x 2  (read-to-write) =  20
  TURNAROUND        10 x 6  (tWTR_L)        =  60
  everything else                           =   0
                                              ---
  SUM                                         160

  SUM CHECK : 80 + 20 + 60 + 0 = 160 == window  ->  HOLDS
  turnaround total = 80 cycles = 50.0% of the window

// ---------------------------------------------------------------------
// turnaround_tracker -- determines when the shared data bus must change
// direction, and for how long it is unusable.
//
// CLASSIFICATION: educational, synthesisable. Produces the
// c_turnaround input that cycle_attributor consumes.
//
// WHAT IT DOES NOT MODEL:
//   - the bus or its electrical handover (22.1 owns termination)
//   - the READ-TO-WRITE interval. DDR4 publishes no single parameter
//     for it: the real value is derived from CL, CWL and burst length
//     together. It is therefore a PARAMETER here, not a constant, and
//     §7's callout says why a default would be an invention.
//   - whether a turnaround was avoidable. §7: batching avoids it, and
//     23.4 owns that decision.
// ---------------------------------------------------------------------
module turnaround_tracker #(
  // VERIFIED at DDR4-1600: write-to-read, same and different bank group.
  parameter int TWTR_L = 6,
  parameter int TWTR_S = 2,
  // NOT VERIFIED as a single value -- see the header and §7's callout.
  parameter int T_RTW  = 2,
  parameter int GAP_W  = $clog2((TWTR_L > T_RTW ? TWTR_L : T_RTW) + 2)
) (
  input  logic              clk,
  input  logic              rst_n,

  // ── A burst's last data cycle, with its direction and bank group.
  input  logic              burst_end,
  input  logic              burst_is_write,
  input  logic              burst_same_bg,

  // ── The next burst the scheduler wants to issue.
  input  logic              next_pending,
  input  logic              next_is_write,

  // ── To cycle_attributor.
  output logic              c_turnaround,
  output logic [GAP_W-1:0]  gap_remaining,
  output logic              direction_change,

  // ── Observability. Counting turnarounds separately from the cycles
  //    they cost is what distinguishes "how often" from "how much".
  output logic [15:0]       cnt_turnarounds,
  output logic [15:0]       cnt_turnaround_cycles,
  output logic              last_dir_was_write,

  output logic              err_gap_violated
);

  initial begin
    if (TWTR_L < 1 || TWTR_S < 1)
      $fatal(1, "turnaround_tracker: write-to-read intervals must be >= 1");
    if (T_RTW < 0)
      $fatal(1, "turnaround_tracker: T_RTW must not be negative");
    if (TWTR_S > TWTR_L)
      $fatal(1, "turnaround_tracker: TWTR_S (%0d) exceeds TWTR_L (%0d)",
             TWTR_S, TWTR_L);
  end

  logic             prev_write, have_prev;
  logic [GAP_W-1:0] gap;
  logic [15:0]      n_ta, n_ta_cy;

  // A direction change is needed when the pending burst's direction
  // differs from the last one completed. Declared above the assigns.
  logic change_needed;
  assign change_needed = have_prev && next_pending
                      && (next_is_write != prev_write);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      prev_write <= 1'b0;
      have_prev  <= 1'b0;
      gap        <= '0;
      n_ta       <= '0;
      n_ta_cy    <= '0;
    end else begin
      if (burst_end) begin
        // Load the gap this direction change requires. Write-to-read
        // uses the VERIFIED tWTR value for the bank-group relationship;
        // read-to-write uses the caller's parameter.
        if (have_prev && (prev_write != burst_is_write)) begin
          n_ta <= (n_ta == 16'hFFFF) ? n_ta : n_ta + 16'd1;
        end
        prev_write <= burst_is_write;
        have_prev  <= 1'b1;
        gap        <= burst_is_write
                        ? (burst_same_bg ? GAP_W'(TWTR_L) : GAP_W'(TWTR_S))
                        : GAP_W'(T_RTW);
      end else if (gap != '0) begin
        gap     <= gap - GAP_W'(1);
        n_ta_cy <= (n_ta_cy == 16'hFFFF) ? n_ta_cy : n_ta_cy + 16'd1;
      end
    end
  end

  assign c_turnaround      = (gap != '0);
  assign gap_remaining     = gap;
  assign direction_change  = change_needed;
  assign cnt_turnarounds   = n_ta;
  assign cnt_turnaround_cycles = n_ta_cy;
  assign last_dir_was_write    = prev_write;

  // A burst starting while a gap is still outstanding is a scheduling
  // violation: the bus had not finished changing hands.
  assign err_gap_violated = burst_end && (gap != '0);

endmodule

// P11 -- the gap is loaded from the VERIFIED parameter matching the
// bank-group relationship. Getting tWTR_S and tWTR_L the wrong way
// round understates the cost on the common case.
property p_gap_matches_relationship;
  @(posedge clk) disable iff (!rst_n)
    (burst_end && burst_is_write)
      |=> (gap_remaining == (($past(burst_same_bg, 1))
                               ? GAP_W'(TWTR_L) : GAP_W'(TWTR_S)));
endproperty
assert property (p_gap_matches_relationship);

// P12 -- turnaround COUNT and turnaround CYCLES are tracked
// separately. One turnaround costing six cycles and six costing one
// each are different problems, and a single counter conflates them.
property p_cycles_at_least_count;
  @(posedge clk) disable iff (!rst_n)
    (cnt_turnarounds != '0) |-> (cnt_turnaround_cycles >= cnt_turnarounds);
endproperty
assert property (p_cycles_at_least_count);

// ── Cover: a write-to-read turnaround within a bank group -- the
// expensive case, and the one tWTR_L governs.
cover property (@(posedge clk) disable iff (!rst_n)
                  burst_end && burst_is_write && burst_same_bg);
// A read-to-write turnaround: the case whose interval is not a
// published parameter.
cover property (@(posedge clk) disable iff (!rst_n)
                  burst_end && !burst_is_write && next_pending && next_is_write);

   1. DATA           a beat is on the bus. Nothing else matters --
                     the cycle was USED.
   2. REFRESH        the device is unavailable. Dominates every
                     controller-side cause, because no decision
                     could have used this cycle.
   3. TURNAROUND     the bus is changing direction.
   4. ROW WORK       a PRE or ACT is occupying the path to data.
   5. tFAW STALL     an activate was wanted and the window forbade it.
   6. tCCD GAP       a column command was ready and spacing forbade it.
   7. IDLE           no demand. The requester had nothing.

// ---------------------------------------------------------------------
// cycle_attributor -- charges every cycle in an observation window to
// exactly ONE named cause, exhaustively.
//
// CLASSIFICATION: educational, synthesisable. Builds measure D of
// Chapter 12.4, which that chapter defined and did not construct.
//
// WHAT IT DOES NOT MODEL:
//   - the device, the workload, or the scheduler
//   - whether a charged cycle was AVOIDABLE. §8: attribution is not
//     blame, and no counter can separate irreducible from avoidable.
//   - absolute time. Cycles only; the ns conversion needs tCK.
//
// THE TWO INVARIANTS:
//   DISJOINT    -- exactly one category charged per cycle (P2)
//   EXHAUSTIVE  -- the categories sum to the window length (P1)
// Both are asserted, and P1 is the single most valuable property in
// this module: an attribution whose parts do not sum is not one.
// ---------------------------------------------------------------------
module cycle_attributor #(
  // Observation window in cycles. A window is REQUIRED: a utilisation
  // without a stated denominator is not a quantity (12.4 §2).
  parameter int WINDOW  = 1024,
  parameter int CNT_W   = 24,
  parameter int WIN_W   = (WINDOW <= 1) ? 1 : $clog2(WINDOW + 1),
  // Seven categories, fixed by §9's priority order. Not configurable:
  // changing the set changes what the block claims to measure.
  parameter int NCAT    = 7
) (
  input  logic              clk,
  input  logic              rst_n,

  input  logic              enable,

  // ── Condition inputs, one per cause. These may be simultaneously
  //    true -- that is the whole difficulty (§9), and resolving it is
  //    this block's job rather than its caller's.
  input  logic              c_data_beat,     // a beat is on the bus
  input  logic              c_refresh,       // device unavailable
  input  logic              c_turnaround,    // bus changing direction
  input  logic              c_row_work,      // PRE or ACT occupying
  input  logic              c_faw_block,     // an ACT wanted, tFAW said no
  input  logic              c_ccd_block,     // a CAS ready, tCCD said no
  input  logic              c_demand,        // the requester wants something

  // ── Per-category counts, valid when window_done.
  output logic [CNT_W-1:0]  n_data,
  output logic [CNT_W-1:0]  n_refresh,
  output logic [CNT_W-1:0]  n_turnaround,
  output logic [CNT_W-1:0]  n_row_work,
  output logic [CNT_W-1:0]  n_faw,
  output logic [CNT_W-1:0]  n_ccd,
  output logic [CNT_W-1:0]  n_idle,

  // ── Observability.
  output logic [2:0]        charged,         // which category, this cycle
  output logic [WIN_W-1:0]  cycles_elapsed,
  output logic              window_done,
  // The invariants, published so a checker requires rather than
  // recomputes them.
  output logic              sum_ok,
  output logic              exactly_one,
  output logic [2:0]        dominant_loss,   // largest NON-data category

  output logic              err_saturated,
  output logic              err_overlap_seen  // two causes coincided
);

  initial begin
    if (WINDOW < 8)
      $fatal(1, "cycle_attributor: WINDOW (%0d) too small to be meaningful", WINDOW);
    if (NCAT != 7)
      $fatal(1, "cycle_attributor: NCAT is fixed at 7 by the priority order");
    // Every cycle of the window could fall in one category, so a
    // counter must be able to hold WINDOW. A narrower counter would
    // saturate on a perfectly ordinary trace.
    if ((CNT_W < WIN_W))
      $fatal(1, "cycle_attributor: CNT_W (%0d) cannot hold WINDOW", CNT_W);
  end

  localparam logic [2:0] K_DATA = 3'd0;
  localparam logic [2:0] K_REF  = 3'd1;
  localparam logic [2:0] K_TURN = 3'd2;
  localparam logic [2:0] K_ROW  = 3'd3;
  localparam logic [2:0] K_FAW  = 3'd4;
  localparam logic [2:0] K_CCD  = 3'd5;
  localparam logic [2:0] K_IDLE = 3'd6;

  // ── THE DECODER. §9's priority order, in one place, as a priority
  //    chain. This is the only classification in the block, which is
  //    what makes the categories disjoint BY CONSTRUCTION rather than
  //    by a check applied afterwards.
  logic [2:0] sel;
  always_comb begin
    if      (c_data_beat)  sel = K_DATA;   // used -- nothing else matters
    else if (c_refresh)    sel = K_REF;    // irreducible, dominates policy
    else if (c_turnaround) sel = K_TURN;
    else if (c_row_work)   sel = K_ROW;
    else if (c_faw_block)  sel = K_FAW;
    else if (c_ccd_block)  sel = K_CCD;
    else                   sel = K_IDLE;   // catch-all: exhaustive
  end

  // ── How many causes were simultaneously true. Not used for
  //    classification -- published so the undercount §9's callout
  //    admits to is observable rather than hidden.
  logic [3:0] n_true;
  always_comb
    n_true = 4'($countones({c_data_beat, c_refresh, c_turnaround,
                            c_row_work, c_faw_block, c_ccd_block}));

  logic [CNT_W-1:0] cnt [7];
  logic [WIN_W-1:0] elapsed;
  logic             sat, wdone, ovl;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (int k = 0; k < 7; k++) cnt[k] <= '0;
      elapsed <= '0;
      sat     <= 1'b0;
      wdone   <= 1'b0;
      ovl     <= 1'b0;
    end else begin
      wdone <= 1'b0;

      if (enable) begin
        if (elapsed == WIN_W'(WINDOW)) begin
          // Window complete: report and restart. Counters clear here
          // rather than on the first cycle of the next window, so a
          // consumer reading on window_done sees a complete set.
          wdone   <= 1'b1;
          elapsed <= WIN_W'(1);
          for (int k = 0; k < 7; k++) cnt[k] <= '0;
          cnt[sel] <= CNT_W'(1);
          ovl <= (n_true > 4'd1);
        end else begin
          elapsed <= elapsed + WIN_W'(1);
          if (cnt[sel] == {CNT_W{1'b1}}) sat <= 1'b1;
          else                           cnt[sel] <= cnt[sel] + CNT_W'(1);
          if (n_true > 4'd1) ovl <= 1'b1;
        end
      end
    end
  end

  assign n_data       = cnt[K_DATA];
  assign n_refresh    = cnt[K_REF];
  assign n_turnaround = cnt[K_TURN];
  assign n_row_work   = cnt[K_ROW];
  assign n_faw        = cnt[K_FAW];
  assign n_ccd        = cnt[K_CCD];
  assign n_idle       = cnt[K_IDLE];

  assign charged        = sel;
  assign cycles_elapsed = elapsed;
  assign window_done    = wdone;

  // ── EXHAUSTIVENESS. Summed in a wider accumulator so the comparison
  //    cannot itself overflow and report a false pass.
  logic [CNT_W+3:0] tally;
  always_comb begin
    tally = '0;
    for (int k = 0; k < 7; k++) tally = tally + {4'b0, cnt[k]};
  end
  assign sum_ok = (tally == {{(CNT_W+4-WIN_W){1'b0}}, elapsed});

  // ── DISJOINTNESS. The decoder guarantees it structurally; this makes
  //    the guarantee checkable.
  assign exactly_one = 1'b1;   // one `sel` per cycle, by construction

  // ── Largest non-data category: the binding constraint, and the only
  //    question anyone asks of an attribution.
  always_comb begin
    dominant_loss = K_REF;
    for (int k = 2; k < 7; k++)
      if (cnt[k] > cnt[dominant_loss]) dominant_loss = 3'(k);
  end

  assign err_saturated    = sat;
  assign err_overlap_seen = ovl;

endmodule

  Model B: row hits, same bank group. tCCD_L = 5, burst = 4 cycles.
  Window = 200 cycles.

  bursts issued        = 200 / 5          = 40
  DATA cycles          = 40 x 4           = 160
  tCCD GAP cycles      = 40 x (5 - 4)     =  40
  REFRESH              =                     0   (none in this window)
  TURNAROUND           =                     0   (reads only)
  ROW WORK             =                     0   (all hits)
  tFAW STALL           =                     0   (no activates)
  IDLE                 =                     0   (demand always present)
                                            ----
  SUM                                        200

  SUM CHECK : 160 + 40 + 0 + 0 + 0 + 0 + 0 = 200 == window  ->  HOLDS

  slot utilisation  = 160 / 200 = 80.0%
  achieved          = 40 bursts x 64 B / 200 cycles = 12.800 B/cycle
                    = 10.240 GB/s of 12.8 GB/s peak = 80.0%
  dominant_loss     = tCCD GAP (40 cycles)

// ---------------------------------------------------------------------
// bandwidth_reporter -- turns an attribution into byte counts and
// explicit ratio numerator/denominator pairs.
//
// CLASSIFICATION: educational, synthesisable.
//
// WHAT IT DOES NOT MODEL:
//   - causes, avoidability, or time. Cycles and bytes only.
//   - a percentage. IT DOES NOT DIVIDE (12.4 §2): every ratio is
//     published as a numerator and a denominator so the consumer is
//     forced to state what it divided by.
//
// WHY NO DIVISION: 12.4 established that "efficiency" as a single
// number is not a quantity. A block that produced one would be
// endorsing exactly the trap that chapter named.
// ---------------------------------------------------------------------
module bandwidth_reporter #(
  // Bytes carried by one fully-used cycle. DERIVED from the interface:
  // beats per cycle times bytes per beat (§2 -- 2 x 8 = 16).
  parameter int BYTES_PER_CYCLE = 16,
  parameter int CNT_W  = 24,
  parameter int BYT_W  = CNT_W + 5,
  parameter int BPC_W  = (BYTES_PER_CYCLE <= 1) ? 1 : $clog2(BYTES_PER_CYCLE + 1)
) (
  input  logic              clk,
  input  logic              rst_n,

  // ── From cycle_attributor, on window_done.
  input  logic              window_done,
  input  logic [CNT_W-1:0]  n_data,
  input  logic [CNT_W-1:0]  n_refresh,
  input  logic [CNT_W-1:0]  n_window,      // total cycles observed
  input  logic              attrib_sum_ok,

  // ── Byte counts.
  output logic [BYT_W-1:0]  bytes_moved,
  output logic [BYT_W-1:0]  bytes_peak,        // if every cycle carried
  // Bytes the device could have carried given refresh alone -- the
  // TRUE ceiling of §6, which is below peak and is the honest
  // denominator for a controller-efficiency claim.
  output logic [BYT_W-1:0]  bytes_ceiling,

  // ── Ratio PAIRS. Never a quotient.
  output logic [CNT_W-1:0]  util_num,          // n_data
  output logic [CNT_W-1:0]  util_den,          // n_window
  output logic [CNT_W-1:0]  ctrl_num,          // n_data
  output logic [CNT_W-1:0]  ctrl_den,          // n_window - n_refresh
  output logic              ratios_valid,

  output logic              err_data_exceeds_window,
  output logic              err_reported_without_sum
);

  initial begin
    if (BYTES_PER_CYCLE < 1)
      $fatal(1, "bandwidth_reporter: BYTES_PER_CYCLE must be >= 1");
    if (BYT_W <= CNT_W)
      $fatal(1, "bandwidth_reporter: BYT_W must exceed CNT_W to hold a product");
  end

  logic [BYT_W-1:0] mv, pk, cl;
  logic [CNT_W-1:0] un, ud, cn, cd;
  logic             vld, bad, nosum;

  // Available cycles after refresh: the denominator a CONTROLLER should
  // be judged against, because refresh is not its decision (§6, §8).
  logic [CNT_W-1:0] avail;
  always_comb begin
    avail = (n_window >= n_refresh) ? (n_window - n_refresh) : '0;
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      mv <= '0; pk <= '0; cl <= '0;
      un <= '0; ud <= '0; cn <= '0; cd <= '0;
      vld <= 1'b0; bad <= 1'b0; nosum <= 1'b0;
    end else if (window_done) begin
      // Products are computed into BYT_W, which the elaboration guard
      // requires to be wider than CNT_W -- a same-width multiply would
      // silently truncate on a large window.
      mv <= {{(BYT_W-CNT_W){1'b0}}, n_data}  * BYT_W'(BYTES_PER_CYCLE);
      pk <= {{(BYT_W-CNT_W){1'b0}}, n_window} * BYT_W'(BYTES_PER_CYCLE);
      cl <= {{(BYT_W-CNT_W){1'b0}}, avail}   * BYT_W'(BYTES_PER_CYCLE);

      un <= n_data;   ud <= n_window;
      cn <= n_data;   cd <= avail;

      // A report is only trustworthy if the attribution it came from
      // was exhaustive. Reporting from a broken attribution is worse
      // than not reporting.
      vld   <= attrib_sum_ok && (n_window != '0);
      bad   <= (n_data > n_window);
      nosum <= !attrib_sum_ok;
    end
  end

  assign bytes_moved   = mv;
  assign bytes_peak    = pk;
  assign bytes_ceiling = cl;
  assign util_num = un; assign util_den = ud;
  assign ctrl_num = cn; assign ctrl_den = cd;
  assign ratios_valid = vld;

  assign err_data_exceeds_window   = bad;
  assign err_reported_without_sum  = nosum;

endmodule

// Bind unit note: P1-P7 reference cycle_attributor's internals and are
// written as though bound into it. P8-P10 reference bandwidth_reporter
// likewise. Both see clk and rst_n directly.

// P1 -- THE property of this chapter, and of this module. The
// categories sum to the cycles elapsed. If it holds, the attribution
// is a partition; if not, it is seven counters.
property p_categories_sum_to_window;
  @(posedge clk) disable iff (!rst_n)
    enable |-> sum_ok;
endproperty
assert property (p_categories_sum_to_window);

// P2 -- exactly one category is charged per enabled cycle. §9's
// disjointness, and the guard against the seven-independent-ifs design.
property p_one_category_per_cycle;
  @(posedge clk) disable iff (!rst_n)
    (enable && !err_saturated && !window_done)
      |=> ($countones({n_data       != $past(n_data, 1),
                       n_refresh    != $past(n_refresh, 1),
                       n_turnaround != $past(n_turnaround, 1),
                       n_row_work   != $past(n_row_work, 1),
                       n_faw        != $past(n_faw, 1),
                       n_ccd        != $past(n_ccd, 1),
                       n_idle       != $past(n_idle, 1)}) == 1);
endproperty
assert property (p_one_category_per_cycle);

// P3 -- a data beat is ALWAYS charged to DATA. §9's priority order at
// its top: a used cycle is never charged to a loss category, which
// would understate achieved bandwidth.
property p_data_beat_charged_to_data;
  @(posedge clk) disable iff (!rst_n)
    (enable && c_data_beat) |-> (charged == 3'd0);
endproperty
assert property (p_data_beat_charged_to_data);

// P4 -- refresh outranks every controller-side cause. §8's claim that
// an irreducible cycle is never charged to a policy category.
property p_refresh_outranks_policy;
  @(posedge clk) disable iff (!rst_n)
    (enable && !c_data_beat && c_refresh) |-> (charged == 3'd1);
endproperty
assert property (p_refresh_outranks_policy);

// P5 -- IDLE is only charged when nothing else holds. The flattering
// error -- charging real stalls to "no demand" -- forbidden.
property p_idle_is_last_resort;
  @(posedge clk) disable iff (!rst_n)
    (enable && (charged == 3'd6))
      |-> !(c_data_beat || c_refresh || c_turnaround
            || c_row_work || c_faw_block || c_ccd_block);
endproperty
assert property (p_idle_is_last_resort);

// P6 -- elapsed never exceeds the window.
property p_window_bounded;
  @(posedge clk) disable iff (!rst_n)
    (cycles_elapsed <= WIN_W'(WINDOW));
endproperty
assert property (p_window_bounded);

// P7 -- no category can exceed the cycles elapsed.
property p_no_category_exceeds_elapsed;
  @(posedge clk) disable iff (!rst_n)
    enable |-> ((n_data <= {{(CNT_W-WIN_W){1'b0}}, cycles_elapsed})
             && (n_idle <= {{(CNT_W-WIN_W){1'b0}}, cycles_elapsed}));
endproperty
assert property (p_no_category_exceeds_elapsed);

// P8 -- a report is never issued from a non-exhaustive attribution.
property p_no_report_without_sum;
  @(posedge clk) disable iff (!rst_n)
    ratios_valid |-> !err_reported_without_sum;
endproperty
assert property (p_no_report_without_sum);

// P9 -- the controller denominator never exceeds the peak denominator,
// because refresh cycles are subtracted rather than added.
property p_ceiling_below_peak;
  @(posedge clk) disable iff (!rst_n)
    ratios_valid |-> (bytes_ceiling <= bytes_peak);
endproperty
assert property (p_ceiling_below_peak);

// P10 -- bytes moved never exceeds the ceiling. A controller cannot
// move data during a refresh, so exceeding it means refresh cycles
// were also counted as data.
property p_moved_within_ceiling;
  @(posedge clk) disable iff (!rst_n)
    ratios_valid |-> (bytes_moved <= bytes_ceiling);
endproperty
assert property (p_moved_within_ceiling);

// ── Cover.
cover property (@(posedge clk) disable iff (!rst_n) window_done);
// 100% utilisation -- §4's model A, which a suite that never hits it
// has not tested against the actual ceiling.
cover property (@(posedge clk) disable iff (!rst_n)
                  window_done && (n_data == n_window));
// Zero data in a whole window: the pathological case.
cover property (@(posedge clk) disable iff (!rst_n)
                  window_done && (n_data == '0));
// Each loss category was dominant at least once.
cover property (@(posedge clk) disable iff (!rst_n)
                  window_done && (dominant_loss == 3'd5));   // tCCD
cover property (@(posedge clk) disable iff (!rst_n)
                  window_done && (dominant_loss == 3'd3));   // row work
cover property (@(posedge clk) disable iff (!rst_n)
                  window_done && (dominant_loss == 3'd1));   // refresh
// Two causes coincided -- the projection case of §9's callout.
cover property (@(posedge clk) disable iff (!rst_n) err_overlap_seen);
// A window with demand present and everything idle: the hole that a
// demand-gated IDLE category would have created.
cover property (@(posedge clk) disable iff (!rst_n)
                  enable && c_demand && (charged == 3'd6));

// Independent tally. Records the condition vector every cycle and
// classifies afterwards, from the recorded history, rather than
// live -- a different method from the DUT's priority chain.
// SIMULATION-ONLY.
class attrib_tally;
  int unsigned tot[7];
  int unsigned cycles;
  // How many cycles had N causes simultaneously true, for N = 0..6.
  int unsigned coincidence[7];

  function void observe(bit d, bit rf, bit tn, bit rw, bit fw, bit cd);
    int unsigned n; int unsigned k;
    n = d + rf + tn + rw + fw + cd;
    coincidence[n]++;
    cycles++;
    // Same ORDER as the DUT, but applied to a recorded vector rather
    // than to live signals -- so a live-signal timing bug shows up as
    // a disagreement instead of being reproduced.
    if      (d)  k = 0;
    else if (rf) k = 1;
    else if (tn) k = 2;
    else if (rw) k = 3;
    else if (fw) k = 4;
    else if (cd) k = 5;
    else         k = 6;
    tot[k]++;
  endfunction

  function bit partitions();
    int unsigned s; s = 0;
    for (int i = 0; i < 7; i++) s += tot[i];
    return s == cycles;
  endfunction

  // The undercount: cycles where a lower-priority cause was true but
  // not charged. This is what §9's callout admits to, quantified.
  function int unsigned masked_cycles();
    int unsigned m; m = 0;
    for (int n = 2; n < 7; n++) m += coincidence[n] * (n - 1);
    return m;
  endfunction
endclass

  THE PRIORITY ORDER'S UNDERCOUNT, QUANTIFIED
    Model B, 200 cycles, with a refresh inserted over cycles 100-119
    (20 cycles, ILLUSTRATIVE -- a real tRFC is 280 cycles).

    reference tally                     DUT
      DATA        144                     144
      REFRESH      20                      20
      tCCD GAP     36                      36
      others        0                       0
      SUM         200                     200      partition HOLDS

    coincidence histogram from the reference:
      1 cause  true : 180 cycles
      2 causes true :  20 cycles   <- the refresh window
      masked_cycles() = 20 x (2-1) = 20

    reading it : during the 20 refresh cycles, tCCD_L was ALSO
      forbidding a column command. Those cycles are charged to
      REFRESH, correctly by §9's order -- and tCCD GAP is therefore
      UNDERCOUNTED by 20 relative to "cycles on which tCCD_L was
      binding", which was 56, not 36.

    diagnosis : NOT A BUG. It is the projection §9's callout describes,
      and the two readings answer different questions:
        "what bounded this cycle"      -> tCCD GAP = 36  (the DUT)
        "when was tCCD_L binding"      -> 56 cycles      (the tally)
    why it matters : a report of 36 tCCD cycles understates how often
      that constraint was active. A design deciding whether to change
      bank-group interleaving wants the second number; a design
      deciding where the cycles WENT wants the first.
    what would be wrong : charging those 20 cycles to both, which
      sums to 220 over a 200-cycle window and fails P1.