DDR5 New Capabilities

   tDRFM  =  (2 x tRRF) x BRC
          =  (2 x BRC)  x tRRF
             \________/    \__/
              rows          per-row
              refreshed     duration

   32 ms / 8192  =  3.906 us  per refresh interval   (up to 85 C)
   16 ms / 8192  =  1.953 us  per refresh interval   (85-95 C)
                                    exactly 2x shorter when hot

// ---------------------------------------------------------------------
// drfm_bounded_refresh -- the DEVICE-VERIFIED BRC configuration, with
// tDRFM computed as (rows x per-row duration) and checked against the
// published equation's own form.
//
// CLASSIFICATION: educational, synthesisable.
//
// VERIFIED IDENTITY (§9): tDRFM = (2 x tRRF) x BRC, which regroups to
// (2 x BRC) rows x tRRF per row. All six published values reproduce
// under both readings. This block computes the ROW-COUNT form and
// asserts it equals the published form, so the regrouping is enforced
// rather than merely asserted in prose.
//
// WHAT IT DOES NOT MODEL:
//   - the array, disturbance physics, or what a neighbour row IS
//   - refresh scope or scheduling (Module 15 owns both, with
//     refresh_scope_ledger and refresh_credit_ledger)
//   - whether RFM is REQUIRED, which is MR58:OP[0] and an input here
//
// tRRF IS DENSITY-INDEPENDENT on this device (§8): 70 all-bank and 60
// same-bank at 8, 16, 24 and 32 Gb. So density is NOT a parameter,
// and adding one would imply a dependence the table denies.
// ---------------------------------------------------------------------
module drfm_bounded_refresh #(
  // DEVICE-VERIFIED per-row durations, in nanoseconds.
  parameter int TRRF_AB = 70,
  parameter int TRRF_SB = 60,
  // DEVICE-VERIFIED BRC range: 2, 3 or 4.
  parameter int BRC_MIN = 2,
  parameter int BRC_MAX = 4,
  parameter int BRC_W   = 3,
  parameter int DUR_W   = 12,
  parameter int CNT_W   = 24
) (
  input  logic              clk,
  input  logic              rst_n,

  // ── Configuration. MR59:OP[2:1] carries BRC; MR58:OP[0] says
  //    whether RFM is required at all (§7).
  input  logic              cfg_valid,
  input  logic [BRC_W-1:0]  cfg_brc,
  input  logic              rfm_required,
  input  logic              cfg_same_bank,     // DRFMsb vs DRFMab

  // ── A DRFM command issued.
  input  logic              drfm_issue,

  // ── Configuration state.
  output logic [BRC_W-1:0]  brc_in_force,
  output logic              brc_valid,
  // §9: 2 x BRC neighbour rows, one on each side at each distance.
  output logic [BRC_W:0]    rows_refreshed,
  output logic [DUR_W-1:0]  t_drfm_ns,
  output logic [DUR_W-1:0]  t_rrf_ns,

  // ── Accounting.
  output logic [CNT_W-1:0]  cnt_drfm,
  output logic [CNT_W-1:0]  ns_spent_in_drfm,

  output logic              err_brc_unsupported,
  output logic              err_issue_without_config,
  output logic              err_issue_when_not_required,
  output logic              any_error
);

  initial begin
    if (TRRF_AB < 1 || TRRF_SB < 1)
      $fatal(1, "drfm_bounded_refresh: per-row durations must be positive");
    if (TRRF_SB > TRRF_AB)
      // §9's callout: same-bank is the cheaper per-row scope, 60
      // against 70, uniformly at every BRC level. A parameterisation
      // reversing that inverts the only saving the scope offers.
      $fatal(1, "drfm_bounded_refresh: same-bank per-row cost (%0d) must not exceed all-bank (%0d)",
             TRRF_SB, TRRF_AB);
    if (BRC_MIN != 2 || BRC_MAX != 4)
      $fatal(1, "drfm_bounded_refresh: BRC range is 2..4 (device-verified)");
    if (BRC_W < 3)
      $fatal(1, "drfm_bounded_refresh: BRC_W too narrow for BRC_MAX");
    // The verified identity, checked at elaboration for every legal
    // BRC and both scopes: the row-count form must equal the
    // published (2 x tRRF) x BRC form, and must fit DUR_W.
    for (int b = BRC_MIN; b <= BRC_MAX; b++) begin
      if (((2 * b) * TRRF_AB) != ((2 * TRRF_AB) * b))
        $fatal(1, "drfm_bounded_refresh: row-count form disagrees at BRC%0d ab", b);
      if (((2 * b) * TRRF_SB) != ((2 * TRRF_SB) * b))
        $fatal(1, "drfm_bounded_refresh: row-count form disagrees at BRC%0d sb", b);
      if (((2 * b) * TRRF_AB) > ((1 << DUR_W) - 1))
        $fatal(1, "drfm_bounded_refresh: DUR_W too narrow for BRC%0d (%0d ns)",
               b, (2 * b) * TRRF_AB);
    end
  end

  logic [BRC_W-1:0]  brc_q;
  logic              have_q, sb_q, required_q;
  logic [CNT_W-1:0]  n_drfm, ns_acc;
  logic              e_brc, e_nocfg, e_notreq;

  // Declared above the continuous assigns that read it.
  logic brc_ok;
  assign brc_ok = (cfg_brc >= BRC_W'(BRC_MIN)) && (cfg_brc <= BRC_W'(BRC_MAX));

  // §9's regrouping, computed rather than tabulated.
  logic [BRC_W:0]   rows_c;
  logic [DUR_W-1:0] per_row_c, tdrfm_c;
  assign rows_c    = have_q ? ((BRC_W+1)'(brc_q) << 1) : '0;
  assign per_row_c = sb_q ? DUR_W'(TRRF_SB) : DUR_W'(TRRF_AB);
  assign tdrfm_c   = have_q ? DUR_W'(rows_c * per_row_c) : '0;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      brc_q <= '0; have_q <= 1'b0; sb_q <= 1'b0; required_q <= 1'b0;
      n_drfm <= '0; ns_acc <= '0;
      e_brc <= 1'b0; e_nocfg <= 1'b0; e_notreq <= 1'b0;
    end else begin
      e_brc <= 1'b0; e_nocfg <= 1'b0; e_notreq <= 1'b0;

      if (cfg_valid) begin
        if (!brc_ok) begin
          // An unsupported BRC is REJECTED, not clamped. Clamping
          // would leave the controller budgeting a tDRFM the device
          // does not use, and every availability figure after that
          // would be wrong by a known factor.
          e_brc <= 1'b1;
        end else begin
          brc_q      <= cfg_brc;
          sb_q       <= cfg_same_bank;
          required_q <= rfm_required;
          have_q     <= 1'b1;
        end
      end

      if (drfm_issue) begin
        if (!have_q) begin
          e_nocfg <= 1'b1;
        end else begin
          // §7: the specifications apply when RFM is required. A DRFM
          // issued when it is not is reported -- it is not illegal,
          // but it spends availability for no obligation.
          if (!required_q) e_notreq <= 1'b1;
          if (n_drfm != {CNT_W{1'b1}}) n_drfm <= n_drfm + CNT_W'(1);
          if (ns_acc < ({CNT_W{1'b1}} - CNT_W'(tdrfm_c)))
            ns_acc <= ns_acc + CNT_W'(tdrfm_c);
        end
      end
    end
  end

  assign brc_in_force   = brc_q;
  assign brc_valid      = have_q;
  assign rows_refreshed = rows_c;
  assign t_drfm_ns      = tdrfm_c;
  assign t_rrf_ns       = per_row_c;
  assign cnt_drfm       = n_drfm;
  assign ns_spent_in_drfm = ns_acc;
  assign err_brc_unsupported        = e_brc;
  assign err_issue_without_config   = e_nocfg;
  assign err_issue_when_not_required = e_notreq;
  assign any_error = e_brc | e_nocfg | e_notreq;
endmodule

// ---------------------------------------------------------------------
// rfm_activation_tracker -- counts activations per bank since that
// bank's last DRFM, and raises the obligation when a count crosses a
// threshold.
//
// CLASSIFICATION: educational, synthesisable.
//
// COLLISION NOTE: 17.1's activate_concurrency_budget governs how many
// activations may be IN FLIGHT within a rolling window (tFAW's
// subject). This block counts how many have OCCURRED since the last
// DRFM to a bank, which has a different reset condition and a
// different purpose. Both are activation counters and they are not
// the same counter.
//
// WHAT IT DOES NOT MODEL:
//   - disturbance physics, or which rows are physically adjacent.
//     §7: DRFM refreshes +/-1..+/-4 NEIGHBOURS, and physical
//     adjacency is a device-internal mapping this block cannot see.
//   - any real threshold. The threshold is an INPUT, because the
//     device-verified material gives BRC and tDRFM but no activation
//     count at which RFM becomes due.
//   - the device's own internal counters, which exist and are not
//     visible at the interface.
// ---------------------------------------------------------------------
module rfm_activation_tracker #(
  parameter int BANKS     = 32,          // 25.1: x4/x8 verified count
  parameter int BANK_W    = $clog2(BANKS),
  parameter int ACT_W     = 16,
  // A COUNT of banks up to BANKS needs clog2(BANKS+1).
  parameter int BANKCNT_W = $clog2(BANKS + 1),
  parameter int CNT_W     = 24
) (
  input  logic                 clk,
  input  logic                 rst_n,

  input  logic                 rfm_required,
  // Threshold at which a bank's accumulation raises the obligation.
  input  logic [ACT_W-1:0]     act_threshold,
  input  logic                 threshold_valid,

  // ── Activity.
  input  logic                 act_valid,
  input  logic [BANK_W-1:0]    act_bank,

  // ── A DRFM discharging the obligation. All-bank clears every
  //    bank's count; same-bank clears one.
  input  logic                 drfm_valid,
  input  logic                 drfm_all_bank,
  input  logic [BANK_W-1:0]    drfm_bank,

  // ── Obligation.
  output logic                 obligation_due,
  output logic [BANKCNT_W-1:0] n_banks_due,
  output logic [BANK_W-1:0]    worst_bank,
  output logic [ACT_W-1:0]     worst_count,

  // ── Accounting.
  output logic [CNT_W-1:0]     cnt_drfm_ab,
  output logic [CNT_W-1:0]     cnt_drfm_sb,
  output logic [CNT_W-1:0]     cnt_threshold_crossings,
  // Sticky: an obligation that went unserved is evidence even after
  // a later DRFM clears the count.
  output logic                 ever_exceeded_unserved,

  output logic                 err_act_bank_out_of_range,
  output logic                 err_no_threshold,
  output logic                 err_saturated,
  output logic                 any_error
);

  initial begin
    if (BANKS < 2 || (BANKS & (BANKS - 1)) != 0)
      // The lower bound matters: a power-of-two test alone accepts 0
      // and 1, either of which makes BANK_W zero and the bank index
      // meaningless.
      $fatal(1, "rfm_activation_tracker: BANKS must be a power of two >= 2");
    if (BANK_W != $clog2(BANKS))
      $fatal(1, "rfm_activation_tracker: BANK_W must address BANKS");
    if (BANKCNT_W <= BANK_W)
      // A count up to BANKS needs one more bit than an index into it.
      // Too narrow and n_banks_due cannot represent "all of them".
      $fatal(1, "rfm_activation_tracker: BANKCNT_W too narrow to count BANKS");
  end

  logic [ACT_W-1:0] acc [BANKS];
  logic             e_rng, e_thr, e_sat, ever_uns;
  logic [CNT_W-1:0] n_ab, n_sb, n_cross;

  // Declared above the continuous assigns that read them.
  logic bank_ok;
  assign bank_ok = ({{(32-BANK_W){1'b0}}, act_bank} < 32'(BANKS));

  logic [BANKCNT_W-1:0] n_due;
  logic [BANK_W-1:0]    w_bank;
  logic [ACT_W-1:0]     w_cnt;
  always_comb begin
    n_due  = '0;
    w_bank = '0;
    w_cnt  = '0;
    for (int b = 0; b < BANKS; b++) begin
      if (threshold_valid && (acc[b] >= act_threshold))
        n_due = n_due + BANKCNT_W'(1);
      if (acc[b] > w_cnt) begin
        w_cnt  = acc[b];
        w_bank = BANK_W'(b);
      end
    end
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (int b = 0; b < BANKS; b++) acc[b] <= '0;
      e_rng <= 1'b0; e_thr <= 1'b0; e_sat <= 1'b0; ever_uns <= 1'b0;
      n_ab <= '0; n_sb <= '0; n_cross <= '0;
    end else begin
      e_rng <= 1'b0; e_thr <= 1'b0; e_sat <= 1'b0;

      if (act_valid && !bank_ok) e_rng <= 1'b1;
      if (act_valid && rfm_required && !threshold_valid) e_thr <= 1'b1;

      // ── Accumulate. A DRFM arriving in the same cycle clears
      //    AFTER this activation is counted, so an activation is
      //    never lost to a coincident discharge.
      if (act_valid && bank_ok) begin
        if (acc[act_bank] == {ACT_W{1'b1}}) e_sat <= 1'b1;
        else begin
          acc[act_bank] <= acc[act_bank] + ACT_W'(1);
          if (threshold_valid && ((acc[act_bank] + ACT_W'(1)) == act_threshold))
            if (n_cross != {CNT_W{1'b1}}) n_cross <= n_cross + CNT_W'(1);
        end
      end

      // ── Discharge.
      if (drfm_valid) begin
        if (drfm_all_bank) begin
          for (int b = 0; b < BANKS; b++) acc[b] <= '0;
          if (n_ab != {CNT_W{1'b1}}) n_ab <= n_ab + CNT_W'(1);
        end else begin
          acc[drfm_bank] <= '0;
          if (n_sb != {CNT_W{1'b1}}) n_sb <= n_sb + CNT_W'(1);
        end
      end

      // Sticky evidence: a threshold was crossed and the cycle ended
      // without a DRFM discharging it.
      if (threshold_valid && (n_due != '0) && !drfm_valid) ever_uns <= 1'b1;
    end
  end

  assign obligation_due = threshold_valid && (n_due != '0);
  assign n_banks_due    = n_due;
  assign worst_bank     = w_bank;
  assign worst_count    = w_cnt;
  assign cnt_drfm_ab    = n_ab;
  assign cnt_drfm_sb    = n_sb;
  assign cnt_threshold_crossings = n_cross;
  assign ever_exceeded_unserved  = ever_uns;
  assign err_act_bank_out_of_range = e_rng;
  assign err_no_threshold          = e_thr;
  assign err_saturated             = e_sat;
  assign any_error = e_rng | e_thr | e_sat;
endmodule

// ---------------------------------------------------------------------
// integrity_layer_arbiter -- which of four mechanisms owns a fault,
// and whether the host finds out.
//
// CLASSIFICATION: educational, synthesisable.
//
// WHY THIS BLOCK EXISTS: §1 establishes four mechanisms with four
// different verbs -- reshapes, detects, corrects, prevents -- at four
// layers. They do NOT compose into one guarantee, and the question a
// controller actually faces is "who handles this, and do I hear about
// it". That question has an answer and it is not in any datasheet
// because it depends on system choices (§6).
//
// WHAT IT DOES NOT MODEL:
//   - any code, polynomial, or actual correction. 22.4 owns the CRC
//     and proved its properties from the polynomial; on-die ECC's
//     code is not published (§2's callout).
//   - DFE's EFFECT. §11: it changes the probability of an error
//     existing, which is not computable here, and 22.3 established
//     that a synthesisable block must not fake physics.
//   - any fault RATE. This routes a fault that has occurred.
// ---------------------------------------------------------------------
module integrity_layer_arbiter #(
  parameter int CNT_W = 24
) (
  input  logic       clk,
  input  logic       rst_n,

  // ── Which layers exist and are usable. §6: ALERT_n's usage is
  //    "system-dependent", so reachability is a system property and
  //    must be an input rather than an assumption.
  input  logic       dfe_enabled,
  input  logic       crc_enabled,
  input  logic       alert_connected,
  input  logic       ondie_ecc_enabled,
  input  logic       ecc_transparency_enabled,
  input  logic       scrub_enabled,
  input  logic       rfm_enabled,

  // ── A fault, by origin. Exactly one may be asserted.
  input  logic       fault_link,          // corrupted in transit
  input  logic       fault_cell_bounded,  // within on-die ECC's bound
  input  logic       fault_cell_beyond,   // beyond it
  input  logic       fault_disturb,       // a neighbour degraded

  // ── Verdict: which layer handles it.
  output logic       handled_by_crc,
  output logic       handled_by_ondie_ecc,
  output logic       prevented_by_rfm,
  output logic       handled_by_nobody,

  // ── Visibility: does the host learn?
  output logic       host_informed,
  output logic       silently_corrected,
  output logic       silently_lost,

  // ── Accounting.
  output logic [CNT_W-1:0] cnt_informed,
  output logic [CNT_W-1:0] cnt_silent_correct,
  output logic [CNT_W-1:0] cnt_silent_loss,

  output logic       err_multiple_fault_origins,
  output logic       err_crc_without_alert,
  output logic       err_ecc_without_visibility,
  output logic       any_error
);

  logic [CNT_W-1:0] n_inf, n_sc, n_sl;
  logic             e_multi, e_crc, e_ecc;

  // Declared above the continuous assigns that read them.
  logic any_fault;
  assign any_fault = fault_link | fault_cell_bounded |
                     fault_cell_beyond | fault_disturb;

  logic one_fault;
  assign one_fault = $onehot({fault_link, fault_cell_bounded,
                              fault_cell_beyond, fault_disturb});

  // ── Routing. Each verb of §1 handles exactly its own fault class.
  logic h_crc, h_ecc, p_rfm, h_none;
  assign h_crc  = one_fault && fault_link && crc_enabled;
  assign h_ecc  = one_fault && fault_cell_bounded && ondie_ecc_enabled;
  assign p_rfm  = one_fault && fault_disturb && rfm_enabled;
  // Nobody handles it: a link fault with CRC off, a bounded cell
  // fault with ECC off, a disturbance with RFM off, or ANY fault
  // beyond on-die ECC's bound -- which no layer here repairs.
  assign h_none = one_fault && !h_crc && !h_ecc && !p_rfm;

  // ── Visibility, which is the chapter's subject.
  //    CRC informs only if ALERT_n is actually connected (§6).
  //    On-die ECC informs only through transparency or scrub (§4).
  logic informed, silent_ok, silent_bad;
  assign informed   = (h_crc && alert_connected) ||
                      (h_ecc && (ecc_transparency_enabled || scrub_enabled)) ||
                      (fault_cell_beyond && one_fault);
  // Corrected, and the host never learns: the §4 visibility problem.
  assign silent_ok  = h_ecc && !ecc_transparency_enabled && !scrub_enabled;
  // Detected or unhandled, and the host never learns: the §6 hazard.
  assign silent_bad = one_fault && !informed && !silent_ok;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      n_inf <= '0; n_sc <= '0; n_sl <= '0;
      e_multi <= 1'b0; e_crc <= 1'b0; e_ecc <= 1'b0;
    end else begin
      e_multi <= 1'b0; e_crc <= 1'b0; e_ecc <= 1'b0;

      if (any_fault && !one_fault) e_multi <= 1'b1;
      // §6's hazard, as a configuration error rather than a fault:
      // CRC enabled with no path for its report.
      if (crc_enabled && !alert_connected) e_crc <= 1'b1;
      // §4's hazard: correction with no visibility path at all.
      if (ondie_ecc_enabled && !ecc_transparency_enabled && !scrub_enabled)
        e_ecc <= 1'b1;

      if (one_fault) begin
        if (informed   && (n_inf != {CNT_W{1'b1}})) n_inf <= n_inf + CNT_W'(1);
        if (silent_ok  && (n_sc  != {CNT_W{1'b1}})) n_sc  <= n_sc  + CNT_W'(1);
        if (silent_bad && (n_sl  != {CNT_W{1'b1}})) n_sl  <= n_sl  + CNT_W'(1);
      end
    end
  end

  assign handled_by_crc       = h_crc;
  assign handled_by_ondie_ecc = h_ecc;
  assign prevented_by_rfm     = p_rfm;
  assign handled_by_nobody    = h_none;
  assign host_informed       = informed;
  assign silently_corrected  = silent_ok;
  assign silently_lost       = silent_bad;
  assign cnt_informed       = n_inf;
  assign cnt_silent_correct = n_sc;
  assign cnt_silent_loss    = n_sl;
  assign err_multiple_fault_origins = e_multi;
  assign err_crc_without_alert      = e_crc;
  assign err_ecc_without_visibility = e_ecc;
  assign any_error = e_multi | e_crc | e_ecc;
endmodule

// Bind unit note: P1-P5 reference drfm_bounded_refresh's internals,
// P6-P10 rfm_activation_tracker's, P11-P15 integrity_layer_arbiter's.

// P1 -- §9's identity, as a runtime invariant as well as an
// elaboration check: tDRFM is the row count times the per-row cost.
property p_tdrfm_is_rows_times_per_row;
  @(posedge clk) disable iff (!rst_n)
    brc_valid |-> (t_drfm_ns == DUR_W'(rows_refreshed * t_rrf_ns));
endproperty
assert property (p_tdrfm_is_rows_times_per_row);

// P2 -- §9: the row count is two per BRC level, because neighbours
// come in pairs.
property p_rows_is_two_per_brc;
  @(posedge clk) disable iff (!rst_n)
    brc_valid |-> (rows_refreshed == ((BRC_W+1)'(brc_in_force) << 1));
endproperty
assert property (p_rows_is_two_per_brc);

// P3 -- FORBIDDEN. An unsupported BRC never enters force. Clamping
// would leave the controller budgeting a tDRFM the device never uses.
property p_bad_brc_never_in_force;
  @(posedge clk) disable iff (!rst_n)
    brc_valid |-> ((brc_in_force >= BRC_W'(BRC_MIN)) &&
                   (brc_in_force <= BRC_W'(BRC_MAX)));
endproperty
assert property (p_bad_brc_never_in_force);

// P4 -- the same-bank scope is never more expensive per row than
// all-bank. §9's callout: 60 against 70, uniformly.
property p_same_bank_is_never_costlier;
  @(posedge clk) disable iff (!rst_n)
    (t_rrf_ns <= DUR_W'(TRRF_AB));
endproperty
assert property (p_same_bank_is_never_costlier);

// P5 -- FORBIDDEN. A DRFM before configuration is reported and never
// accounted, so the availability figures cannot be polluted.
property p_no_accounting_before_config;
  @(posedge clk) disable iff (!rst_n)
    (drfm_issue && !brc_valid)
      |=> (err_issue_without_config && (cnt_drfm == $past(cnt_drfm, 1)));
endproperty
assert property (p_no_accounting_before_config);

// P6 -- an all-bank DRFM discharges EVERY bank. §14: that is what
// distinguishes it from the same-bank form.
property p_all_bank_clears_everything;
  @(posedge clk) disable iff (!rst_n)
    (drfm_valid && drfm_all_bank && !act_valid) |=> (n_banks_due == '0);
endproperty
assert property (p_all_bank_clears_everything);

// P7 -- FORBIDDEN. An activation coincident with a DRFM is never
// lost. §14: an activation that happened cannot be un-happened.
property p_activation_never_lost_to_discharge;
  @(posedge clk) disable iff (!rst_n)
    (act_valid && drfm_valid && !drfm_all_bank && (act_bank == drfm_bank)
     && (worst_count != {ACT_W{1'b1}}))
      |=> (worst_count <= $past(worst_count, 1) + ACT_W'(1));
endproperty
assert property (p_activation_never_lost_to_discharge);

// P8 -- the obligation is never raised without a threshold. An
// obligation against an unknown threshold is an opinion.
property p_no_obligation_without_threshold;
  @(posedge clk) disable iff (!rst_n)
    (!threshold_valid |-> !obligation_due);
endproperty
assert property (p_no_obligation_without_threshold);

// P9 -- the due-bank count never exceeds the bank count. Guards the
// COUNT-vs-INDEX trap: a too-narrow BANKCNT_W would wrap at BANKS.
property p_due_count_bounded;
  @(posedge clk) disable iff (!rst_n)
    (n_banks_due <= BANKCNT_W'(BANKS));
endproperty
assert property (p_due_count_bounded);

// P10 -- an unserved obligation is never forgotten. A later DRFM
// clears the count and must not clear the record of lateness.
property p_unserved_record_is_sticky;
  @(posedge clk) disable iff (!rst_n)
    ($past(ever_exceeded_unserved, 1) |-> ever_exceeded_unserved);
endproperty
assert property (p_unserved_record_is_sticky);

// P11 -- FORBIDDEN. At most one layer handles a fault. §1: four
// verbs, and a fault has one origin, so two owners is a routing bug.
property p_at_most_one_handler;
  @(posedge clk) disable iff (!rst_n)
    $onehot0({handled_by_crc, handled_by_ondie_ecc,
              prevented_by_rfm, handled_by_nobody});
endproperty
assert property (p_at_most_one_handler);

// P12 -- FORBIDDEN. CRC never informs the host when ALERT_n is not
// connected. §6: a detection nobody listens to is not a detection.
property p_crc_cannot_inform_without_alert;
  @(posedge clk) disable iff (!rst_n)
    (handled_by_crc && !alert_connected && !fault_cell_beyond)
      |-> !host_informed;
endproperty
assert property (p_crc_cannot_inform_without_alert);

// P13 -- FORBIDDEN. On-die ECC never informs the host without a
// visibility path. §4's problem, as a property.
property p_ecc_cannot_inform_without_visibility;
  @(posedge clk) disable iff (!rst_n)
    (handled_by_ondie_ecc && !ecc_transparency_enabled && !scrub_enabled)
      |-> (silently_corrected && !host_informed);
endproperty
assert property (p_ecc_cannot_inform_without_visibility);

// P14 -- the three visibility outcomes are mutually exclusive, and
// exactly one holds for a single fault. Merging "corrected but
// invisible" with "lost" would hide the distinction §15 exists for.
property p_visibility_is_a_partition;
  @(posedge clk) disable iff (!rst_n)
    ($onehot({fault_link, fault_cell_bounded, fault_cell_beyond, fault_disturb})
      |-> $onehot({host_informed, silently_corrected, silently_lost}));
endproperty
assert property (p_visibility_is_a_partition);

// P15 -- a fault beyond on-die ECC's bound always reaches the host.
// §2: "bounded fault" is a scope statement, and beyond the bound
// there is nothing to hide the failure.
property p_beyond_bound_always_visible;
  @(posedge clk) disable iff (!rst_n)
    (fault_cell_beyond && $onehot({fault_link, fault_cell_bounded,
                                   fault_cell_beyond, fault_disturb}))
      |-> host_informed;
endproperty
assert property (p_beyond_bound_always_visible);

// ── Cover.
// Every BRC level in force, at both scopes.
cover property (@(posedge clk) disable iff (!rst_n)
                  brc_valid && (brc_in_force == BRC_W'(2)));
cover property (@(posedge clk) disable iff (!rst_n)
                  brc_valid && (brc_in_force == BRC_W'(4)));
cover property (@(posedge clk) disable iff (!rst_n)
                  brc_valid && (t_rrf_ns == DUR_W'(TRRF_SB)));
cover property (@(posedge clk) disable iff (!rst_n)
                  brc_valid && (t_rrf_ns == DUR_W'(TRRF_AB)));
// Each forbidden condition ATTEMPTED -- vacuous otherwise.
cover property (@(posedge clk) disable iff (!rst_n) err_brc_unsupported);
cover property (@(posedge clk) disable iff (!rst_n) err_issue_without_config);
cover property (@(posedge clk) disable iff (!rst_n) err_issue_when_not_required);
// Both DRFM scopes discharging, and an activation coincident with one.
cover property (@(posedge clk) disable iff (!rst_n) drfm_valid && drfm_all_bank);
cover property (@(posedge clk) disable iff (!rst_n) drfm_valid && !drfm_all_bank);
cover property (@(posedge clk) disable iff (!rst_n) act_valid && drfm_valid);
// An obligation raised, and one left unserved.
cover property (@(posedge clk) disable iff (!rst_n) obligation_due);
cover property (@(posedge clk) disable iff (!rst_n) ever_exceeded_unserved);
cover property (@(posedge clk) disable iff (!rst_n) n_banks_due == BANKCNT_W'(BANKS));
// EVERY fault class routed, and every visibility outcome reached.
cover property (@(posedge clk) disable iff (!rst_n) handled_by_crc);
cover property (@(posedge clk) disable iff (!rst_n) handled_by_ondie_ecc);
cover property (@(posedge clk) disable iff (!rst_n) prevented_by_rfm);
cover property (@(posedge clk) disable iff (!rst_n) handled_by_nobody);
// THE TWO SILENT OUTCOMES, separately. §15: one is acceptable and
// one is data loss, and a suite that cannot tell them apart has not
// tested the distinction the block exists for.
cover property (@(posedge clk) disable iff (!rst_n) silently_corrected);
cover property (@(posedge clk) disable iff (!rst_n) silently_lost);
cover property (@(posedge clk) disable iff (!rst_n) err_crc_without_alert);
cover property (@(posedge clk) disable iff (!rst_n) err_ecc_without_visibility);

// Independent DRFM duration reference. Holds the published Table 5
// values as an explicit lookup rather than computing them, so
// agreement with the DUT's computed form is evidence that the
// equation and the table agree — which is §9's whole claim.
// SIMULATION-ONLY.
class drfm_duration_ref;
  // Published tDRFM in ns, indexed [scope][brc]: scope 0 = ab, 1 = sb.
  int published_ns [2][5];

  function void build();
    foreach (published_ns[s,b]) published_ns[s][b] = -1;
    published_ns[0][2] = 280; published_ns[0][3] = 420; published_ns[0][4] = 560;
    published_ns[1][2] = 240; published_ns[1][3] = 360; published_ns[1][4] = 480;
  endfunction

  function int lookup(bit same_bank, int brc);
    if (brc < 2 || brc > 4) return -1;
    return published_ns[same_bank][brc];
  endfunction

  // The row-count reading of §9, computed independently.
  function int by_row_count(bit same_bank, int brc);
    int per_row = same_bank ? 60 : 70;
    return (2 * brc) * per_row;
  endfunction

  function bit forms_agree(bit same_bank, int brc);
    return lookup(same_bank, brc) == by_row_count(same_bank, brc);
  endfunction
endclass

  THE TWO SILENCES, WHICH ARE NOT THE SAME SILENCE
    Same stimulus count, two configurations.

  (A) bounded cell fault, on-die ECC ON, transparency OFF, scrub OFF
        handled_by_ondie_ecc   1
        host_informed          0
        silently_corrected     1     <-- data is CORRECT
        silently_lost          0
        err_ecc_without_visibility   asserted

      the data was repaired. The host does not know a cell is
      marginal, so it cannot predict the part's decline (§4) -- but
      nothing was lost.

  (B) link fault, CRC ON, ALERT_n NOT CONNECTED
        handled_by_crc         1
        host_informed          0
        silently_corrected     0
        silently_lost          1     <-- data is WRONG
        err_crc_without_alert        asserted

      the device detected the corrupted write and pulsed a pin
      nobody is listening to. 22.4 established CRC recovery is a
      RETRY, and the retry lives in the controller -- so no retry
      happens, and the corrupted write completes "successfully".

    a design logging one "silent events" counter sees 2 and cannot
    tell these apart. One is the acceptable cost of on-die ECC; the
    other is undetected data corruption on a system that paid for
    the check bits and the bandwidth to send them.

    the fix : silently_corrected and silently_lost are SEPARATE
      outputs and separate required covers (§16). And the two
      configuration errors -- err_ecc_without_visibility and
      err_crc_without_alert -- fire at BUILD-CONFIGURATION time
      rather than waiting for a fault, which is the only point at
      which either is cheap to fix.