Controller Policies

   open-page   =  h x 0  +  (1-h) x (tRP + tRCD)
               =  (1-h) x (tRP + tRCD)

   close-page  =  tRCD                     -- independent of h

                       tRCD
   h  >  ─────────────────────────
               tRP  +  tRCD

                        same-row access   different-row access
   open-page            0   (best)        22  (worst)
   close-page           11                11
   perfect adaptive     0   (best)        11  (best)
   anti-correlated      11                22  (worst)
                        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
                        worst of both columns

   kept the row open, next access HIT       -> the bet paid. Increment.
   kept the row open, next access CONFLICT  -> the bet lost. Decrement.
   closed the row,    next access MISS      -> no information about
                                               whether keeping it would
                                               have hit. See §8.

// ---------------------------------------------------------------------
// page_policy_engine -- per-bank open / close / adaptive page policy
// with a saturating confidence counter and an observable counterfactual.
//
// CLASSIFICATION: educational, synthesisable.
//
// WHAT IT DOES NOT MODEL:
//   - the device, or tRP / tRCD / tWR enforcement. §2: closing after a
//     write must wait tWR, and 13.4 owns whether a precharge may issue.
//     This block requests; the legality gate decides when.
//   - the scheduler's request choice (23.4 owns it)
//   - the hidden-precharge assumption of §1's callout: whether the
//     precharge actually lands in an idle interval is a scheduling
//     outcome this block cannot see.
//
// THE THREE MODES ARE ONE DESIGN. Open-page and close-page are
// degenerate parameterisations (§9), which is why MODE selects rather
// than switching between implementations.
// ---------------------------------------------------------------------
module page_policy_engine #(
  parameter int NUM_BANKS = 16,
  parameter int ROW_W     = 16,
  // 0 = always open, 1 = always close, 2 = adaptive.
  parameter int MODE      = 2,
  // Saturating counter width per bank. §6's callout: hysteresis is
  // mandatory, and 2 bits is the smallest that provides any.
  parameter int CTR_W     = 2,
  // Decide to hold open when the counter is at or above this. With
  // CTR_W = 2 the counter spans 0..3 and a threshold of 2 means two
  // consecutive wins are needed to switch to holding.
  parameter int HOLD_THRESHOLD = 2,
  // Retain the precharged row's address so the counterfactual of §8 is
  // observable. Costs one register per bank and removes the blindness.
  parameter bit TRACK_COUNTERFACTUAL = 1'b1,
  parameter int BK_W = (NUM_BANKS <= 1) ? 1 : $clog2(NUM_BANKS),
  parameter int CNT_W = 20
) (
  input  logic                clk,
  input  logic                rst_n,

  // ── A burst has completed on this bank: the decision point of §1.
  input  logic                burst_done,
  input  logic [BK_W-1:0]     burst_bank,
  input  logic [ROW_W-1:0]    burst_row,
  // Direction matters for WHEN the precharge may start (§2), not for
  // whether to close. Published onward rather than acted on here.
  input  logic                burst_was_write,

  // ── The next access to a bank, which is the outcome observation.
  input  logic                acc_valid,
  input  logic [BK_W-1:0]     acc_bank,
  input  logic [ROW_W-1:0]    acc_row,

  // ── THE DECISION.
  output logic                close_request,
  output logic [BK_W-1:0]     close_bank,
  // Forwarded so the scheduler applies tWR rather than tRTP (§2).
  output logic                close_after_write,

  // ── Observability: the predictor's own accuracy, which §8 says is
  //    only observable at all because of the retained row address.
  output logic [CNT_W-1:0]    n_held_and_hit,      // the bet paid
  output logic [CNT_W-1:0]    n_held_and_conflict, // the bet lost
  output logic [CNT_W-1:0]    n_closed_and_reused, // closing was WRONG
  output logic [CNT_W-1:0]    n_closed_and_other,  // closing was right
  output logic [CTR_W-1:0]    ctr_of_bank,
  output logic                predict_hold,
  output logic                any_saturated,

  output logic                err_close_unopened,
  output logic                err_mode_invalid
);

  initial begin
    if (NUM_BANKS < 1)
      $fatal(1, "page_policy_engine: NUM_BANKS must be at least 1");
    if (MODE < 0 || MODE > 2)
      $fatal(1, "page_policy_engine: MODE must be 0, 1 or 2");
    if (CTR_W < 2 && MODE == 2)
      // A 1-bit counter has no hysteresis: one observation flips it,
      // which is exactly §6's oscillator.
      $fatal(1, "page_policy_engine: adaptive MODE needs CTR_W >= 2");
    if (HOLD_THRESHOLD < 1 || HOLD_THRESHOLD > (1 << CTR_W) - 1)
      $fatal(1, "page_policy_engine: HOLD_THRESHOLD out of counter range");
  end

  logic [CTR_W-1:0]  ctr      [NUM_BANKS];
  logic              is_open  [NUM_BANKS];
  logic [ROW_W-1:0]  open_row [NUM_BANKS];
  // §8's counterfactual: the row we precharged, kept so a later access
  // can reveal that closing was wrong.
  logic              had_closed [NUM_BANKS];
  logic [ROW_W-1:0]  closed_row [NUM_BANKS];

  // Declared above the assigns that read them.
  logic [CNT_W-1:0] n_hh, n_hc, n_cr, n_co;
  logic             sat, bad_close;

  // ── THE DECISION. Open-page and close-page are the degenerate cases
  //    of the adaptive rule, which is why there is one expression.
  logic hold_now;
  always_comb begin
    unique case (MODE)
      0       : hold_now = 1'b1;    // always open
      1       : hold_now = 1'b0;    // always close
      default : hold_now = burst_done
                         && (ctr[burst_bank] >= CTR_W'(HOLD_THRESHOLD));
    endcase
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (int b = 0; b < NUM_BANKS; b++) begin
        // Start at the threshold: neither biased toward holding nor
        // toward closing, so the first few observations decide. Biasing
        // it either way makes the policy's warm-up a hidden default.
        ctr[b]        <= CTR_W'(HOLD_THRESHOLD);
        is_open[b]    <= 1'b0;
        open_row[b]   <= '0;
        had_closed[b] <= 1'b0;
        closed_row[b] <= '0;
      end
      n_hh <= '0; n_hc <= '0; n_cr <= '0; n_co <= '0;
      sat <= 1'b0; bad_close <= 1'b0;
    end else begin
      bad_close <= 1'b0;

      // ── The outcome observation, BEFORE the new decision, so an
      //    access and a burst completion in the same cycle are ordered
      //    correctly: the access reports on the PREVIOUS decision.
      if (acc_valid) begin
        if (is_open[acc_bank]) begin
          // The row was held. Did the bet pay?
          if (open_row[acc_bank] == acc_row) begin
            if (n_hh != {CNT_W{1'b1}}) n_hh <= n_hh + CNT_W'(1); else sat <= 1'b1;
            if (ctr[acc_bank] != {CTR_W{1'b1}})
              ctr[acc_bank] <= ctr[acc_bank] + CTR_W'(1);
          end else begin
            if (n_hc != {CNT_W{1'b1}}) n_hc <= n_hc + CNT_W'(1); else sat <= 1'b1;
            if (ctr[acc_bank] != '0)
              ctr[acc_bank] <= ctr[acc_bank] - CTR_W'(1);
          end
        end else if (TRACK_COUNTERFACTUAL && had_closed[acc_bank]) begin
          // §8: the row was closed. The retained address reveals
          // whether closing was wrong -- the ONLY way this state
          // produces a learning signal at all.
          if (closed_row[acc_bank] == acc_row) begin
            // Closing was WRONG: this would have been a hit.
            if (n_cr != {CNT_W{1'b1}}) n_cr <= n_cr + CNT_W'(1); else sat <= 1'b1;
            if (ctr[acc_bank] != {CTR_W{1'b1}})
              ctr[acc_bank] <= ctr[acc_bank] + CTR_W'(1);
          end else begin
            if (n_co != {CNT_W{1'b1}}) n_co <= n_co + CNT_W'(1); else sat <= 1'b1;
            if (ctr[acc_bank] != '0)
              ctr[acc_bank] <= ctr[acc_bank] - CTR_W'(1);
          end
        end
        // The access opens its row either way.
        is_open[acc_bank]    <= 1'b1;
        open_row[acc_bank]   <= acc_row;
        had_closed[acc_bank] <= 1'b0;
      end

      // ── The decision, at the burst-completion point of §1.
      if (burst_done) begin
        if (!is_open[burst_bank] && !acc_valid) bad_close <= 1'b1;
        if (!hold_now) begin
          is_open[burst_bank]    <= 1'b0;
          had_closed[burst_bank] <= 1'b1;
          closed_row[burst_bank] <= burst_row;
        end
      end
    end
  end

  assign close_request     = burst_done && !hold_now;
  assign close_bank        = burst_bank;
  assign close_after_write = burst_done && !hold_now && burst_was_write;

  assign n_held_and_hit      = n_hh;
  assign n_held_and_conflict = n_hc;
  assign n_closed_and_reused = n_cr;
  assign n_closed_and_other  = n_co;
  assign ctr_of_bank         = ctr[acc_valid ? acc_bank : burst_bank];
  assign predict_hold        = hold_now;
  assign any_saturated       = sat;
  assign err_close_unopened  = bad_close;
  assign err_mode_invalid    = 1'b0;   // MODE is checked at elaboration

endmodule

// ---------------------------------------------------------------------
// policy_counterfactual -- what would open-page, close-page and a
// perfect predictor each have cost on THIS access stream?
//
// CLASSIFICATION: educational, synthesisable.
//
// WHY IT EXISTS: §4 shows the winner depends on the workload's hit
// probability, and §3 gives the crossover in closed form. A design can
// therefore decide which policy to use IF it knows h -- and this block
// measures the three costs directly instead, which is stronger because
// it needs no distributional assumption at all.
//
// WHAT IT DOES NOT MODEL:
//   - the device, the deployed policy, or the scheduler
//   - the hidden-precharge assumption (§1's callout). Close-page's
//     cost here assumes the precharge lands in an idle interval; if it
//     does not, the real cost is higher and this understates it.
// ---------------------------------------------------------------------
module policy_counterfactual #(
  parameter int NUM_BANKS = 16,
  parameter int ROW_W     = 16,
  // VERIFIED weights from 23.3 §2 / 23.1 §2.
  parameter int T_RCD = 11,
  parameter int T_RP  = 11,
  parameter int BK_W  = (NUM_BANKS <= 1) ? 1 : $clog2(NUM_BANKS),
  parameter int ACC_W = 32
) (
  input  logic                clk,
  input  logic                rst_n,

  input  logic                acc_valid,
  input  logic [BK_W-1:0]     acc_bank,
  input  logic [ROW_W-1:0]    acc_row,
  // The NEXT access's row for this bank, if known. A perfect predictor
  // needs it, which is exactly why a perfect predictor is not
  // implementable -- this input exists only to compute the CEILING.
  input  logic                lookahead_valid,
  input  logic [ROW_W-1:0]    lookahead_row,

  // ── The three costs, in cycles, on the observed stream.
  output logic [ACC_W-1:0]    cost_open,
  output logic [ACC_W-1:0]    cost_close,
  output logic [ACC_W-1:0]    cost_perfect,
  output logic [ACC_W-1:0]    n_accesses,

  // ── The crossover, evaluated: is the stream's behaviour above or
  //    below tRCD/(tRP+tRCD)? Reported as the comparison rather than
  //    as a ratio, so nothing divides.
  output logic                open_is_better,
  output logic                counts_valid,

  output logic                err_weights_invalid
);

  initial begin
    if (T_RCD < 1 || T_RP < 1)
      $fatal(1, "policy_counterfactual: weights must be positive");
    if (ACC_W < 16)
      $fatal(1, "policy_counterfactual: ACC_W too small to accumulate");
  end

  logic [ROW_W-1:0] open_row [NUM_BANKS];
  logic             valid_r  [NUM_BANKS];

  logic [ACC_W-1:0] c_open, c_close, c_perf, n_acc;
  logic             sat;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (int b = 0; b < NUM_BANKS; b++) begin
        open_row[b] <= '0;
        valid_r[b]  <= 1'b0;
      end
      c_open <= '0; c_close <= '0; c_perf <= '0; n_acc <= '0; sat <= 1'b0;
    end else if (acc_valid) begin
      if (n_acc == {ACC_W{1'b1}}) begin
        sat <= 1'b1;
      end else begin
        n_acc <= n_acc + ACC_W'(1);

        // ── OPEN-PAGE: hit if the row matches, else a conflict.
        if (!valid_r[acc_bank])
          c_open <= c_open + ACC_W'(T_RCD);                 // first touch
        else if (open_row[acc_bank] == acc_row)
          c_open <= c_open;                                  // hit: zero
        else
          c_open <= c_open + ACC_W'(T_RP + T_RCD);           // conflict

        // ── CLOSE-PAGE: always a miss. Constant, independent of the
        //    stream -- which is §3's whole point, in one line.
        c_close <= c_close + ACC_W'(T_RCD);

        // ── PERFECT: a hit costs nothing; anything else costs a miss,
        //    because the row was closed in advance. §5's ceiling.
        if (valid_r[acc_bank] && (open_row[acc_bank] == acc_row))
          c_perf <= c_perf;
        else
          c_perf <= c_perf + ACC_W'(T_RCD);

        open_row[acc_bank] <= acc_row;
        valid_r[acc_bank]  <= 1'b1;
      end
    end
  end

  assign cost_open    = c_open;
  assign cost_close   = c_close;
  assign cost_perfect = c_perf;
  assign n_accesses   = n_acc;
  // The crossover test, as a comparison rather than a ratio.
  assign open_is_better = (c_open < c_close);
  assign counts_valid   = !sat && (n_acc != '0);
  assign err_weights_invalid = 1'b0;   // checked at elaboration

endmodule

// ---------------------------------------------------------------------
// precharge_timing_gate -- applies tRTP after a read and tWR after a
// write before a requested precharge becomes eligible.
//
// CLASSIFICATION: educational, synthesisable. Supplies the timing
// page_policy_engine requests and deliberately does not own.
//
// WHAT IT DOES NOT MODEL:
//   - the device, or command-bus arbitration
//   - LEGALITY (13.4) or the commit point (17.1). Eligible is not
//     issued, and this block never claims otherwise.
//   - whether the precharge lands in an idle interval, which is §1's
//     callout's assumption and a scheduling outcome.
//
// §2: the two delays differ by 2x, so a gate applying one value to
// both would either violate tWR after writes or needlessly delay
// precharges after reads.
// ---------------------------------------------------------------------
module precharge_timing_gate #(
  parameter int NUM_BANKS = 16,
  // VERIFIED at DDR4-1600K: tRTP = 6 nCK, tWR = 15 ns = 12 nCK.
  parameter int T_RTP = 6,
  parameter int T_WR  = 12,
  parameter int BK_W  = (NUM_BANKS <= 1) ? 1 : $clog2(NUM_BANKS),
  parameter int D_W   = (T_WR > T_RTP)
                          ? ((T_WR   <= 1) ? 1 : $clog2(T_WR + 1))
                          : ((T_RTP  <= 1) ? 1 : $clog2(T_RTP + 1)),
  parameter int OCC_W = $clog2(NUM_BANKS + 1)
) (
  input  logic                 clk,
  input  logic                 rst_n,

  // -- A close request from page_policy_engine, with its direction.
  input  logic                 close_request,
  input  logic [BK_W-1:0]      close_bank,
  input  logic                 close_after_write,

  // -- Eligibility, per bank. NOT an issue signal.
  output logic [NUM_BANKS-1:0] pre_eligible,
  output logic [D_W-1:0]       wait_of_bank,
  output logic [OCC_W-1:0]     n_waiting,

  // -- Observability: cycles spent waiting, split by direction, so the
  //    §2 asymmetry's real cost on this workload is visible.
  output logic [23:0]          cy_waiting_read,
  output logic [23:0]          cy_waiting_write,
  output logic                 any_saturated,

  output logic                 err_request_while_waiting
);

  initial begin
    if (NUM_BANKS < 1)
      $fatal(1, "precharge_timing_gate: NUM_BANKS must be at least 1");
    if (T_RTP < 1 || T_WR < 1)
      $fatal(1, "precharge_timing_gate: delays must be positive");
    if (T_WR < T_RTP)
      // §2: write recovery is the LONGER of the two. A parameterisation
      // claiming otherwise inverts the asymmetry the block exists for.
      $fatal(1, "precharge_timing_gate: T_WR (%0d) below T_RTP (%0d)",
             T_WR, T_RTP);
  end

  logic [D_W-1:0] cnt    [NUM_BANKS];
  logic           pend   [NUM_BANKS];
  logic           was_wr [NUM_BANKS];

  // Declared above the assigns that read them.
  logic [23:0] cy_rd, cy_wr;
  logic        sat, bad_req;

  logic [OCC_W-1:0] n_wait;
  always_comb begin
    n_wait = '0;
    for (int b = 0; b < NUM_BANKS; b++)
      if (pend[b] && (cnt[b] != '0)) n_wait = n_wait + OCC_W'(1);
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (int b = 0; b < NUM_BANKS; b++) begin
        cnt[b]    <= '0;
        pend[b]   <= 1'b0;
        was_wr[b] <= 1'b0;
      end
      cy_rd <= '0; cy_wr <= '0; sat <= 1'b0; bad_req <= 1'b0;
    end else begin
      bad_req <= 1'b0;

      // -- Age every pending bank, charging the wait to the right
      //    direction so §2's asymmetry is measurable rather than
      //    merely asserted.
      for (int b = 0; b < NUM_BANKS; b++) begin
        if (pend[b] && (cnt[b] != '0)) begin
          cnt[b] <= cnt[b] - D_W'(1);
          if (was_wr[b]) begin
            if (cy_wr == 24'hFFFFFF) sat <= 1'b1; else cy_wr <= cy_wr + 24'd1;
          end else begin
            if (cy_rd == 24'hFFFFFF) sat <= 1'b1; else cy_rd <= cy_rd + 24'd1;
          end
        end
      end

      // -- A new request loads the direction-appropriate delay.
      if (close_request) begin
        if (pend[close_bank] && (cnt[close_bank] != '0)) bad_req <= 1'b1;
        pend[close_bank]   <= 1'b1;
        was_wr[close_bank] <= close_after_write;
        cnt[close_bank]    <= close_after_write ? D_W'(T_WR) : D_W'(T_RTP);
      end
    end
  end

  always_comb
    for (int b = 0; b < NUM_BANKS; b++)
      pre_eligible[b] = pend[b] && (cnt[b] == '0);

  assign wait_of_bank     = cnt[close_bank];
  assign n_waiting        = n_wait;
  assign cy_waiting_read  = cy_rd;
  assign cy_waiting_write = cy_wr;
  assign any_saturated    = sat;
  assign err_request_while_waiting = bad_req;

endmodule

// P11 -- the loaded delay matches the direction. §2's asymmetry, and
// the check that a single value is not being applied to both.
property p_delay_matches_direction;
  @(posedge clk) disable iff (!rst_n)
    close_request
      |=> (wait_of_bank == ($past(close_after_write, 1)
                              ? D_W'(T_WR) : D_W'(T_RTP)));
endproperty
assert property (p_delay_matches_direction);

// P12 -- eligibility requires the counter to have expired. A gate that
// asserted early would violate tWR, which is a device rule and not a
// policy preference.
property p_eligible_only_when_expired;
  @(posedge clk) disable iff (!rst_n)
    pre_eligible[close_bank] |-> (wait_of_bank == '0);
endproperty
assert property (p_eligible_only_when_expired);

// -- Cover: a write-direction wait, which a read-only trace never
// exercises and which is the longer of the two.
cover property (@(posedge clk) disable iff (!rst_n)
                  close_request && close_after_write);
// Several banks waiting at once -- the multi-bank case.
cover property (@(posedge clk) disable iff (!rst_n) n_waiting > OCC_W'(1));

// Bind unit note: P1-P7 reference page_policy_engine's internals,
// P8-P10 policy_counterfactual's; both are written as though bound
// into their module, so clk and rst_n are visible directly.

// P1 -- MODE 0 never closes. Open-page as a degenerate case (§9), and
// the check that the mode parameter is real rather than decorative.
property p_open_mode_never_closes;
  @(posedge clk) disable iff (!rst_n)
    (MODE == 0) |-> !close_request;
endproperty
assert property (p_open_mode_never_closes);

// P2 -- MODE 1 closes on every burst completion. Close-page, likewise.
property p_close_mode_always_closes;
  @(posedge clk) disable iff (!rst_n)
    ((MODE == 1) && burst_done) |-> close_request;
endproperty
assert property (p_close_mode_always_closes);

// P3 -- a close is requested only at a burst completion. §1: the
// decision has one moment, and closing at any other point would
// precharge a row that may still be carrying a transfer.
property p_close_only_at_burst_end;
  @(posedge clk) disable iff (!rst_n)
    close_request |-> burst_done;
endproperty
assert property (p_close_only_at_burst_end);

// P4 -- the adaptive decision follows the counter and the threshold.
property p_adaptive_follows_counter;
  @(posedge clk) disable iff (!rst_n)
    ((MODE == 2) && burst_done)
      |-> (predict_hold == (ctr[burst_bank] >= CTR_W'(HOLD_THRESHOLD)));
endproperty
assert property (p_adaptive_follows_counter);

// P5 -- a held row that hit increments; a held row that conflicted
// decrements. The update rule of §7, checkable.
property p_counter_update_direction;
  @(posedge clk) disable iff (!rst_n)
    (acc_valid && is_open[acc_bank] && (open_row[acc_bank] == acc_row)
       && (ctr[acc_bank] != {CTR_W{1'b1}}))
      |=> (ctr[$past(acc_bank, 1)] == $past(ctr[acc_bank], 1) + 1);
endproperty
assert property (p_counter_update_direction);

// P6 -- THE hysteresis property of §6's callout. A single observation
// cannot move the counter across the threshold when it starts more
// than one step away. Without this the policy is an oscillator.
property p_single_observation_cannot_flip;
  @(posedge clk) disable iff (!rst_n)
    ((MODE == 2) && acc_valid
       && (ctr[acc_bank] >= CTR_W'(HOLD_THRESHOLD) + CTR_W'(1)))
      |=> (ctr[$past(acc_bank, 1)] >= CTR_W'(HOLD_THRESHOLD));
endproperty
assert property (p_single_observation_cannot_flip);

// P7 -- the counterfactual counter only moves when tracking is
// enabled. §8: without it the predictor is blind in close mode, and
// that blindness must be visible rather than silently absent.
property p_counterfactual_requires_tracking;
  @(posedge clk) disable iff (!rst_n)
    (n_closed_and_reused != $past(n_closed_and_reused, 1))
      |-> (TRACK_COUNTERFACTUAL == 1'b1);
endproperty
assert property (p_counterfactual_requires_tracking);

// P8 -- close-page's cost is exactly tRCD per access. §3's "independent
// of h", as an invariant rather than an observation.
property p_close_cost_is_linear;
  @(posedge clk) disable iff (!rst_n)
    counts_valid |-> (cost_close == n_accesses * ACC_W'(T_RCD));
endproperty
assert property (p_close_cost_is_linear);

// P9 -- a perfect predictor is never worse than either fixed policy.
// §5's ceiling, and the check that the ceiling is computed correctly.
property p_perfect_bounds_both;
  @(posedge clk) disable iff (!rst_n)
    counts_valid |-> ((cost_perfect <= cost_open)
                   && (cost_perfect <= cost_close));
endproperty
assert property (p_perfect_bounds_both);

// P10 -- open-page's cost never exceeds (tRP+tRCD) per access, and
// close-page's never falls below tRCD. The two bounds of §4's table.
property p_costs_within_bounds;
  @(posedge clk) disable iff (!rst_n)
    counts_valid |-> (cost_open <= n_accesses * ACC_W'(T_RP + T_RCD));
endproperty
assert property (p_costs_within_bounds);

// ── Cover.
cover property (@(posedge clk) disable iff (!rst_n) close_request);
cover property (@(posedge clk) disable iff (!rst_n)
                  burst_done && predict_hold && (MODE == 2));
// The counterfactual fired: closing was WRONG and the predictor learned
// it. §8's mechanism actually exercised -- without this cover, the
// retained row address is untested.
cover property (@(posedge clk) disable iff (!rst_n)
                  n_closed_and_reused != $past(n_closed_and_reused, 1));
// The counter saturated at each end -- the hysteresis limits.
cover property (@(posedge clk) disable iff (!rst_n)
                  (MODE == 2) && acc_valid && (ctr[acc_bank] == '0));
cover property (@(posedge clk) disable iff (!rst_n)
                  (MODE == 2) && acc_valid && (ctr[acc_bank] == {CTR_W{1'b1}}));
// Open-page better, and close-page better, on the same instance across
// two runs -- §4's flip actually observed.
cover property (@(posedge clk) disable iff (!rst_n)
                  counts_valid && open_is_better);
cover property (@(posedge clk) disable iff (!rst_n)
                  counts_valid && !open_is_better);
// A close after a write: §2's tWR path, which a read-only trace misses.
cover property (@(posedge clk) disable iff (!rst_n) close_after_write);

// Independent policy cost reference. Computes each policy's cost from
// CLASS COUNTS by closed form, rather than by per-access accumulation
// -- a different method, so agreement is evidence.
// SIMULATION-ONLY.
class policy_ref;
  int unsigned t_rcd, t_rp;
  int unsigned n_hit, n_other;     // over the observed stream

  function int unsigned cost_open();
    return n_other * (t_rp + t_rcd);
  endfunction
  function int unsigned cost_close();
    return (n_hit + n_other) * t_rcd;
  endfunction
  function int unsigned cost_perfect();
    return n_other * t_rcd;
  endfunction
  // §3's crossover, as a comparison with no division.
  function bit open_better();
    return cost_open() < cost_close();
  endfunction
  // The crossover hit rate, as a numerator/denominator pair.
  function void crossover(output int unsigned num, output int unsigned den);
    num = t_rcd; den = t_rp + t_rcd;
  endfunction
endclass

  THE PREDICTOR THAT CANNOT LEARN ITS WAY OUT
    MODE = 2, CTR_W = 2, HOLD_THRESHOLD = 2, counter starts at 2.
    TRACK_COUNTERFACTUAL = 0.

    workload: h = 90% -- open-page would cost 2200 cy per 1000 accesses.
    but the stream BEGINS with a burst of 3 different-row accesses.

    access 1-3 : row held, conflict each time -> counter 2,1,0
    access 4   : counter 0 < threshold 2      -> CLOSE
    access 5+  : every access is a MISS. The row is closed before each
                 one, so the access never reveals that it WANTED the
                 row that was just precharged.
                 with TRACK_COUNTERFACTUAL = 0 there is no observation
                 at all -> the counter NEVER MOVES.

    outcome over 1000 accesses:
      actual cost      : 3 conflicts x 22 + 997 misses x 11 = 11033 cy
      open-page would  : 2200 cy
      close-page would : 11000 cy
      perfect would    : 1100 cy

    the adaptive policy performed WORSE THAN BOTH fixed policies
    (11033 > 11000 > 2200) on a workload with 90% locality.

    diagnosis : three unrepresentative accesses drove the counter to
      zero, and §8's blindness meant no subsequent evidence could ever
      contradict it. The policy is stuck, correctly by its own rules.
    what still passes : P1-P6 all hold. P4 holds -- the decision
      follows the counter. P6 holds -- no single observation flipped
      anything. The engine is working exactly as specified.
    caught by : this check, and by n_closed_and_reused being
      permanently zero -- which P7 explains is expected when tracking
      is disabled, and which is therefore the signature rather than
      the bug.
    the fix : TRACK_COUNTERFACTUAL = 1. With it, access 5 reveals that
      the precharged row was wanted, the counter rises, and the policy
      returns to holding within CTR_W observations.