DDR vs SRAM

   the ACCESS CONTRACT, four questions

   C1  Is the completion time a CONSTANT, a BOUND, or neither?
   C2  Does an access depend on the HISTORY of previous accesses?
   C3  Can the memory REFUSE or DEFER an access for its own reasons?
   C4  Does the requester have to participate in MAINTENANCE?

   A1  read destroys the stored value
        |
        +-> the value must be REBUILT after every read
        |     -> the rebuild takes time the requester did not ask for
        |     -> the rebuilt row is now HELD somewhere (the row buffer)
        |          -> so an access's cost DEPENDS ON WHAT IS HELD  (C2)
        |          -> so completion time is not a constant          (C1)
        |          -> so "which row is open" becomes CONTROLLER STATE (A2)
        |
        +-> charge leaks even when NOT read
              -> periodic rewrite is MANDATORY
                   -> the memory needs the bus for its own purposes (C3)
                   -> and somebody must own the schedule for that   (C4)

   ILLUSTRATIVE H = 20, a = 14, p = 14 (units: clock cycles; the real
   values are per-device and per-speed-bin, and 14.1/14.2 own them)

     row hit       20
     row miss      34      = 20 + 14        -> 1.70x the hit
     row conflict  48      = 20 + 14 + 14   -> 2.40x the hit

   DERIVED spread: the SAME access costs between 20 and 48 depending
   only on what previous traffic left behind. Ratio 2.40.

   the equivalent SRAM figure is ONE number, because C2's answer is
   "no" -- there is no history for the cost to depend on.

   ADMISSIBLE(block, technology)  iff

       worst_case_completion(technology)  <=  deadline(block)

   and note what is NOT in that inequality: capacity, cost, area,
   bandwidth. Stage one is a pure feasibility test and it either
   passes or it does not.

   for a destructive-read technology the left-hand side must be
   ARGUED from the obligation set of §5, because §6's component with
   no upper bound means it cannot simply be measured.

   static   total_area  =  N * A_s  +  P_s
   dynamic  total_area  =  N * A_d  +  P_d  +  K

   the crossover capacity N* is where they are equal:

       N* * A_s + P_s  =  N* * A_d + P_d + K

       N*  =  ( P_d + K - P_s )  /  ( A_s - A_d )

   STRUCTURAL, and read the form rather than any value:

   - A_s > A_d, so the denominator is POSITIVE -- 1.3 §4's argument
     that several actively driven transistors cannot be as small as
     the minimum possible number of devices.
   - the numerator is dominated by K for small systems, because a
     controller has a FLOOR: §5's thirteen obligations do not get
     cheaper when the array gets smaller.
   - so N* is NOT near zero. below N* the static contract wins on
     cost as well as on admissibility, and that is why small
     on-chip memories are never dynamic.

// ---------------------------------------------------------------------
// mem_access_frontend -- the parameterised comparative block of §9.
//
// CLASSIFICATION: synthesisable, ILLUSTRATIVE parameter values, and
// CORRECT as written. The intentionally defective block is §11.
//
// WHAT IT IS: one requester-facing frontend that instantiates EITHER
// access contract of §1 under a single causal parameter. The generate
// boundaries below are §5's obligation table expressed as hardware:
// everything inside `if (DESTRUCTIVE_READ)` exists BECAUSE a read
// destroys the stored value (§4), and nothing inside it is an
// optimisation that the static contract merely does without.
//
// WHY IT EXISTS HERE: §5 counts thirteen obligations in prose. Prose
// can be argued with. A generate boundary cannot: the logic either
// elaborates or it does not, and `obligation_count` reports which.
//
// HOW TO RUN IT: elaborate twice, once per contract, and compare the
// synthesised state-element count and `obligation_count`.
// EXPECTED RESULT: the static configuration instantiates no row
// state, no elapsed counters, no rolling window and no refresh
// ledger, and reports obligation_count = 0.
//
// SYNTHESIS: the dynamic configuration is dominated by per-bank
// counters -- BANKS * (3 counters + a row index + 2 state bits).
// The static configuration is a registered address path.
//
// LIMITATIONS: this is a LEGALITY and CONTRACT frontend, not a
// scheduler. It answers "may this access proceed, and when will it
// complete", and deliberately does NOT choose among candidates --
// 17.1 and 17.4 own that, and 30.5 owns why the two must not merge.
// It models one outstanding access so that the contract, rather than
// concurrency, is what the reader compares. §16 states what changes
// when that assumption is relaxed.
// ---------------------------------------------------------------------
module mem_access_frontend #(
  // ---- A1: the causal parameter. Everything else follows. --------
  parameter bit DESTRUCTIVE_READ = 1'b1,

  // ---- Derived, NOT independent. §4's chain forbids the other
  //      combination, and §13 audits it rather than trusting it.
  parameter bit NEEDS_REFRESH    = DESTRUCTIVE_READ,

  // ---- Geometry. Meaningful only for the dynamic contract. -------
  parameter int BANKS            = 16,
  parameter int ROW_W            = 16,

  // ---- ILLUSTRATIVE timing. Real values are per-device and
  //      per-speed-bin; 14.1 to 14.3 own them and this block quotes
  //      none of them as fact.
  parameter int TRCD             = 14,
  parameter int TRP              = 14,
  parameter int TRAS             = 34,

  // ---- The static contract's single completion figure. -----------
  parameter int FIXED_LAT        = 3,

  // ---- COUNT, not INDEX. These counters must REPRESENT their
  //      thresholds, so each needs $clog2(threshold + 1) bits. Sized
  //      $clog2(threshold) a counter saturates one short of the
  //      value it is compared against, and the comparison becomes
  //      unreachable -- the guard is then present in the source and
  //      absent in the silicon.
  parameter int CNT_W            = $clog2((TRAS > TRP ? (TRAS > TRCD ? TRAS : TRCD)
                                                      : (TRP  > TRCD ? TRP  : TRCD)) + 1),
  parameter int BANK_W           = $clog2(BANKS)
)(
  input  logic               clk,
  input  logic               rst_n,

  // ---- Requester side. IDENTICAL for both contracts -- §8's top
  //      layer, and the reason §1's admissibility test is meaningful.
  input  logic               req_valid,
  input  logic [BANK_W-1:0]  req_bank,
  input  logic [ROW_W-1:0]   req_row,
  output logic               req_ready,

  // ---- Device side.
  output logic               cmd_pre,
  output logic               cmd_act,
  output logic               cmd_col,
  output logic [BANK_W-1:0]  cmd_bank,

  // ---- Maintenance. Only the dynamic contract drives this.
  input  logic               refresh_due,
  output logic               refresh_req,

  // ---- Contract reporting, for §13's audit and for the testbench.
  output logic [2:0]         access_outcome,
  output logic [7:0]         obligation_count
);
  // Outcome encoding, shared by both contracts so one scoreboard
  // serves both. OUT_UNKNOWN is a FINDING, not a fourth path --
  // 7.4's three-valued bank-state discipline, and 30.2 §8's point
  // that reporting a confident wrong row is worse than reporting
  // nothing.
  localparam logic [2:0] OUT_IDLE     = 3'd0;
  localparam logic [2:0] OUT_STATIC   = 3'd1;  // non-destructive path
  localparam logic [2:0] OUT_HIT      = 3'd2;
  localparam logic [2:0] OUT_MISS     = 3'd3;
  localparam logic [2:0] OUT_CONFLICT = 3'd4;
  localparam logic [2:0] OUT_UNKNOWN  = 3'd5;

  initial begin
    if (BANKS < 1)
      $fatal(1, "mem_access_frontend: BANKS must be >= 1 (got %0d)", BANKS);
    if (FIXED_LAT < 1)
      $fatal(1, "mem_access_frontend: FIXED_LAT must be >= 1");
    // §4's causal chain, enforced at elaboration. A destructive read
    // without a refresh obligation is not a contract that exists, and
    // a parameterised comparative block that permits the combination
    // can be configured into a memory technology nobody sells.
    if (DESTRUCTIVE_READ && !NEEDS_REFRESH)
      $fatal(1, "mem_access_frontend: DESTRUCTIVE_READ implies NEEDS_REFRESH (§4)");
    // The reverse is also incoherent: charge that does not leak away
    // on a read has no reason to leak away while idle.
    if (!DESTRUCTIVE_READ && NEEDS_REFRESH)
      $fatal(1, "mem_access_frontend: NEEDS_REFRESH without DESTRUCTIVE_READ is incoherent (§4)");
    if (DESTRUCTIVE_READ && (TRAS < TRCD))
      $fatal(1, "mem_access_frontend: TRAS < TRCD leaves no legal column window");
  end

  generate
  // ===================================================================
  // THE DESTRUCTIVE CONTRACT. Everything here exists because of §4.
  // ===================================================================
  if (DESTRUCTIVE_READ) begin : g_dynamic

    // ---- Obligation 1: row state, three-valued. ---------------------
    logic             row_open  [BANKS];
    logic             row_known [BANKS];
    logic [ROW_W-1:0] row_idx   [BANKS];

    // ---- Obligations 2 to 4: per-bank elapsed time. Separate
    //      counters rather than one, because the three thresholds are
    //      measured from DIFFERENT events -- 13.3's scope taxonomy.
    logic [CNT_W-1:0] since_act [BANKS];
    logic [CNT_W-1:0] since_pre [BANKS];

    // ---- Obligation 7: the refresh accrual, held elsewhere. 15.3
    //      owns the ledger with its postponement and pull-in credit
    //      rule; this block CONSUMES `refresh_due` and does not
    //      reimplement the accounting -- 17.3 §7's one-writer rule.
    assign refresh_req = refresh_due;

    // ---- Timekeeping. Saturating, so a long idle period stays legal
    //      rather than wrapping back into illegality.
    always_ff @(posedge clk) begin
      if (!rst_n) begin
        for (int b = 0; b < BANKS; b++) begin
          row_open[b]  <= 1'b0;
          row_known[b] <= 1'b0;
          row_idx[b]   <= '0;
          since_act[b] <= '0;
          since_pre[b] <= '0;
        end
      end else begin
        for (int b = 0; b < BANKS; b++) begin
          if (since_act[b] != {CNT_W{1'b1}}) since_act[b] <= since_act[b] + 1'b1;
          if (since_pre[b] != {CNT_W{1'b1}}) since_pre[b] <= since_pre[b] + 1'b1;
        end
        if (cmd_act) begin
          row_open[cmd_bank]  <= 1'b1;
          row_known[cmd_bank] <= 1'b1;
          row_idx[cmd_bank]   <= req_row;
          since_act[cmd_bank] <= '0;
        end
        if (cmd_pre) begin
          row_open[cmd_bank]  <= 1'b0;
          row_known[cmd_bank] <= 1'b1;
          since_pre[cmd_bank] <= '0;
        end
      end
    end

    // ---- Classification. Against the REGISTERED state, before any
    //      same-cycle command is applied. 30.2 §10 owns why: a
    //      classifier that folds in this cycle's own command reports
    //      the outcome of a state that did not exist when the
    //      requester asked.
    logic [2:0] outcome_c;
    always_comb begin
      outcome_c = OUT_IDLE;
      if (req_valid) begin
        if      (!row_known[req_bank])           outcome_c = OUT_UNKNOWN;
        else if (!row_open[req_bank])            outcome_c = OUT_MISS;
        else if (row_idx[req_bank] == req_row)   outcome_c = OUT_HIT;
        else                                     outcome_c = OUT_CONFLICT;
      end
    end
    assign access_outcome = outcome_c;

    // ---- Obligation 12: legality as a MAXIMUM over every applicable
    //      rule. 13.3 owns the derivation; 30.3 §3 owns why a single
    //      parameter yields only a lower bound. Each term below is
    //      one candidate in that maximum.
    logic legal_col, legal_act, legal_pre;
    assign legal_col = row_open[req_bank] && (since_act[req_bank] >= TRCD[CNT_W-1:0]);
    assign legal_act = !row_open[req_bank] && (since_pre[req_bank] >= TRP[CNT_W-1:0]);
    assign legal_pre = row_open[req_bank]  && (since_act[req_bank] >= TRAS[CNT_W-1:0]);

    // ---- Command emission. One command per cycle: there is one
    //      command bus, and 17.1 owns the commit point as the single
    //      instant architectural state may change.
    always_comb begin
      cmd_pre = 1'b0;
      cmd_act = 1'b0;
      cmd_col = 1'b0;
      cmd_bank = req_bank;
      if (req_valid && refresh_req == 1'b0) begin
        unique case (outcome_c)
          OUT_HIT      : cmd_col = legal_col;
          OUT_MISS     : cmd_act = legal_act;
          OUT_CONFLICT : cmd_pre = legal_pre;
          // OUT_UNKNOWN emits NOTHING. 7.4: an unknown bank state is
          // a finding, and treating it as idle issues an ACT to a
          // bank that may already have a row open -- an ILLEGAL
          // command rather than a slow one.
          default      : ;
        endcase
      end
    end

    // Accept only when the access is COMPLETE, i.e. a column command
    // issued. A miss or conflict re-presents: one request is many
    // commands (17.1 §3), which is §6's variability at its source.
    assign req_ready = cmd_col;

    // §5's count, reported rather than claimed.
    assign obligation_count = 8'd13;

  // ===================================================================
  // THE NON-DESTRUCTIVE CONTRACT. Note what is absent, and that its
  // absence is STRUCTURAL rather than a simplification (§4's
  // inversion): there is no rebuilt copy needing a home, so there is
  // nothing for a row buffer to hold and no state to keep coherent.
  // ===================================================================
  end else begin : g_static

    // No row state. No elapsed counters. No rolling window. No
    // ledger. The access is architecturally one operation -- 1.3 §4.
    assign refresh_req      = 1'b0;
    assign access_outcome   = req_valid ? OUT_STATIC : OUT_IDLE;
    assign obligation_count = 8'd0;

    assign cmd_pre  = 1'b0;
    assign cmd_act  = 1'b0;
    assign cmd_col  = req_valid;
    assign cmd_bank = req_bank;

    // The whole legality question, for this contract. Not "a maximum
    // over every applicable rule" -- there are no rules, because
    // there is no history for a rule to constrain (§4, C2).
    assign req_ready = req_valid;

  end
  endgenerate
endmodule

   ILLUSTRATIVE BANKS = 16, ROW_W = 16, CNT_W = 6 (from TRAS = 34).

   DYNAMIC configuration, per bank:
       row_open     1
       row_known    1
       row_idx     16
       since_act    6
       since_pre    6
                   --
                   30 bits per bank

       x 16 banks           = 480 bits of state
       + the refresh ledger  (15.3, held outside this block)
       + the rolling activate window (14.8, deliberately omitted
         here -- see the block's LIMITATIONS)

   STATIC configuration:
       0 bits.

   DERIVED: 480 bits against 0, for a frontend that presents the
   IDENTICAL requester interface. The comparison is not "how fast"
   -- it is "how much state must agree with something you cannot
   see", and that is the quantity §5 argues is the real cost.

// ---------------------------------------------------------------------
// access_completion_model -- INTENTIONALLY DEFECTIVE, for review (§11).
//
// CLASSIFICATION: synthesisable, ILLUSTRATIVE, and CONTAINS A BUG.
//
// WHAT IT IS MEANT TO DO: the five-clause contract above -- tell the
// requester when its data is usable, under EITHER access contract.
//
// WHY IT EXISTS HERE: §1 claims admissibility must be checked before
// affordability, and that a block which assumes a constant completion
// time is INADMISSIBLE for a destructive-read technology at any
// capacity. This block is that inadmissibility, in hardware, and it
// is the signature bug class of a parameterised comparison: code
// correct under one parameterisation, reused under the other without
// re-deriving the contract.
//
// HOW TO RUN IT: elaborate with DESTRUCTIVE_READ = 1 and present a
// row-conflict access.
// EXPECTED RESULT under clause 4: `done` is asserted only after the
// conflict path's completion time.
// EXPECTED TRACE: done must follow the precharge, the activate and
// the column command -- not a fixed offset from acceptance.
//
// SYNTHESIS: one shift register of depth FIXED_LAT + 1.
// LIMITATIONS: models ONE outstanding access. Association of several
// returns to several requests is 10.5 §9's, and the single-
// outstanding assumption is STATED rather than hidden -- it is not
// what the bug is.
// ---------------------------------------------------------------------
module access_completion_model #(
  parameter bit DESTRUCTIVE_READ = 1'b1,
  parameter int FIXED_LAT        = 3,    // ILLUSTRATIVE
  // ILLUSTRATIVE, and present on the interface for clause 4's use.
  parameter int TRCD             = 14,
  parameter int TRP              = 14
)(
  input  logic       clk,
  input  logic       rst_n,

  input  logic       req_accept,     // a request was accepted this cycle
  input  logic [2:0] access_outcome, // from §9's frontend
  output logic       done
);
  localparam int DEPTH = FIXED_LAT + 1;

  initial begin
    if (FIXED_LAT < 1) $fatal(1, "access_completion_model: FIXED_LAT >= 1");
  end

  // pipe[i] == 1 means "a completion is due i cycles from now".
  logic [DEPTH-1:0] pipe;

  always_ff @(posedge clk) begin
    if (!rst_n) begin
      pipe <= '0;
    end else begin
      logic [DEPTH-1:0] nxt;
      nxt = pipe >> 1;
      if (req_accept)
        nxt[FIXED_LAT] = 1'b1;      // <-- THE DEFECT
      pipe <= nxt;
    end
  end

  // Clause 5 holds: nothing enters the pipe without an acceptance.
  assign done = pipe[0];
endmodule

   ILLUSTRATIVE FIXED_LAT = 3, TRP = 14, TRCD = 14.
   A row CONFLICT access, using §6's path costs.

   cycle   event                                    done
   -----   ------------------------------------     ----
     0     req accepted; outcome = OUT_CONFLICT      0
     1     frontend emits PRE (legal_pre held)       0
     3     this block: pipe[0] -> DONE               1   <-- WRONG
    15     TRP elapsed; frontend emits ACT           0
    29     TRCD elapsed; frontend emits COL          0
    ~34    data actually usable                      0

   the requester was told its data was ready on cycle 3 and the
   column command had not been issued by cycle 29. It reads
   whatever the return path happened to hold.

   and note the DIRECTION: the model is EARLY. An early completion
   is a data-correctness failure. A late one would merely be slow.

  // CORRECTED. Clause 4: under the destructive contract, completion
  // DEPENDS ON THE OUTCOME, so the outcome must be read. The
  // FIXED_LAT path survives only where clause 3 licenses it.
  //
  // Note that `pipe` is gone for the dynamic case rather than being
  // reloaded with a bigger constant: a longer fixed offset would be
  // a WORSE bug, because it would be right on average and wrong per
  // access, and §6's whole point is that the per-access spread is
  // the quantity that decides admissibility.
  generate
  if (DESTRUCTIVE_READ) begin : g_dyn_done
    // Completion is the COLUMN COMMAND's data return, and the column
    // command's timing is the frontend's business. So this block
    // stops predicting and starts OBSERVING: `col_commit` is an
    // input, and done follows it by the device's read latency.
    // 10.2 owns that latency; 30.4 §3 Q4 owns why the observed
    // offset legitimately exceeds it.
    logic [RD_LAT:0] rpipe;
    always_ff @(posedge clk) begin
      if (!rst_n) rpipe <= '0;
      else begin
        logic [RD_LAT:0] nxt;
        nxt = rpipe >> 1;
        if (col_commit) nxt[RD_LAT] = 1'b1;
        rpipe <= nxt;
      end
    end
    assign done = rpipe[0];
  end else begin : g_stat_done
    // Clause 3. Unchanged, and still correct.
    logic [FIXED_LAT:0] pipe;
    always_ff @(posedge clk) begin
      if (!rst_n) pipe <= '0;
      else begin
        logic [FIXED_LAT:0] nxt;
        nxt = pipe >> 1;
        if (req_accept) nxt[FIXED_LAT] = 1'b1;
        pipe <= nxt;
      end
    end
    assign done = pipe[0];
  end
  endgenerate

// ---------------------------------------------------------------------
// contract_consistency_audit -- verification-only, CORRECT as written.
//
// CLASSIFICATION: verification/telemetry. Drives nothing. ILLUSTRATIVE
// parameter values.
//
// WHAT IT DOES: confirms at runtime that the CONTRACT the parameters
// claim is the contract the design actually presents, and records
// which contracts a regression exercised.
//
// WHY IT EXISTS HERE: §12's defect was not a parameter error -- the
// parameters were right. It was a BEHAVIOUR that did not follow its
// parameters, plus a regression that never ran the other
// configuration. An elaboration guard catches the first class and is
// blind to the second. This block catches both, and its
// `contracts_seen` output is the artifact a sign-off review should
// ask for -- 30.9 §11's argument that a green result without a
// coverage artifact is not evidence.
//
// HOW TO RUN IT: bind one instance per frontend instance, in both
// configurations, and read `contracts_seen` at end of test.
// EXPECTED RESULT: contracts_seen == 2'b11 after a regression that
// ran both. Anything less is a STIMULUS finding, not a design one.
//
// SYNTHESIS: none -- verification only.
// LIMITATIONS: audits the CONTRACT, not the data. A scoreboard with
// an independent memory model is 27.4's, and this block deliberately
// does not duplicate it -- 27.3's independence requirement means an
// auditor that recomputed the data would share the design's state.
// ---------------------------------------------------------------------
module contract_consistency_audit #(
  parameter bit DESTRUCTIVE_READ = 1'b1,
  parameter bit NEEDS_REFRESH    = DESTRUCTIVE_READ,
  parameter int FIXED_LAT        = 3,
  parameter int OBS_W            = 16
)(
  input  logic       clk,
  input  logic       rst_n,

  input  logic       req_valid,
  input  logic       req_ready,
  input  logic       done,
  input  logic [2:0] access_outcome,
  input  logic [7:0] obligation_count,
  input  logic       refresh_req,

  // Bit 0 set once a static contract was observed, bit 1 a dynamic
  // one. A regression reporting 2'b01 has proved nothing whatever
  // about the dynamic configuration -- and vice versa.
  output logic [1:0]        contracts_seen,
  // Observed spread between the fastest and slowest completion, in
  // cycles. For a static contract this must stay at zero: it is the
  // RUNTIME evidence for clause 3, and 30.8 §11's rule that a
  // derived statistic needs its range asserted applies to it.
  output logic [OBS_W-1:0]  completion_spread,
  output logic              audit_fail
);
  localparam logic [2:0] OUT_STATIC   = 3'd1;
  localparam logic [2:0] OUT_HIT      = 3'd2;
  localparam logic [2:0] OUT_MISS     = 3'd3;
  localparam logic [2:0] OUT_CONFLICT = 3'd4;
  localparam logic [2:0] OUT_UNKNOWN  = 3'd5;

  // COUNT, not INDEX: these hold elapsed cycle counts up to their
  // saturation value and are COMPARED against each other, so both
  // must be wide enough to represent the worst completion the test
  // can produce. Sized too narrowly, min and max both saturate and
  // the spread reads ZERO -- the instrument reporting the static
  // contract's signature while measuring the dynamic one.
  logic [OBS_W-1:0] elapsed, obs_min, obs_max;
  logic             in_flight, seen_any;

  always_ff @(posedge clk) begin
    if (!rst_n) begin
      contracts_seen    <= 2'b00;
      completion_spread <= '0;
      audit_fail        <= 1'b0;
      elapsed           <= '0;
      obs_min           <= '1;     // AND-accumulator discipline: a
      obs_max           <= '0;     // minimum must start at all-ones,
      in_flight         <= 1'b0;   // or the first sample never wins.
      seen_any          <= 1'b0;
    end else begin
      // ---- Which contract is this instance presenting? -------------
      if (access_outcome == OUT_STATIC) contracts_seen[0] <= 1'b1;
      if (access_outcome inside {OUT_HIT, OUT_MISS, OUT_CONFLICT, OUT_UNKNOWN})
        contracts_seen[1] <= 1'b1;

      // ---- Completion-time observation. -----------------------------
      if (req_valid && req_ready) begin
        elapsed   <= '0;
        in_flight <= 1'b1;
      end else if (in_flight && elapsed != {OBS_W{1'b1}}) begin
        elapsed   <= elapsed + 1'b1;
      end

      if (in_flight && done) begin
        in_flight <= 1'b0;
        seen_any  <= 1'b1;
        if (elapsed < obs_min) obs_min <= elapsed;
        if (elapsed > obs_max) obs_max <= elapsed;
        completion_spread <= (elapsed > obs_max ? elapsed : obs_max)
                           - (elapsed < obs_min ? elapsed : obs_min);
      end

      // ---- The audit itself. ----------------------------------------
      // A1: the obligation count must agree with the contract. §9
      // reports 13 or 0, and any other value means the frontend and
      // the audit disagree about which contract elaborated.
      if (obligation_count != (DESTRUCTIVE_READ ? 8'd13 : 8'd0))
        audit_fail <= 1'b1;

      // A2: a static contract must never request maintenance. §4's
      // causal chain says charge that does not leak on a read has no
      // reason to leak while idle.
      if (!DESTRUCTIVE_READ && refresh_req)
        audit_fail <= 1'b1;

      // A3: a static contract must never report a history-dependent
      // outcome, because there is no history (C2).
      if (!DESTRUCTIVE_READ &&
          access_outcome inside {OUT_HIT, OUT_MISS, OUT_CONFLICT})
        audit_fail <= 1'b1;

      // A4: clause 3, checked at RUNTIME rather than assumed. A
      // static contract's completions must all be the same length.
      // This is the check that would have caught §12's defect from
      // the OTHER direction -- not by finding the dynamic case
      // early, but by proving the static case really is constant and
      // therefore that a constant model is licensed ONLY there.
      if (!DESTRUCTIVE_READ && seen_any && completion_spread != '0)
        audit_fail <= 1'b1;
    end
  end
endmodule

  // Offered as "proves the completion model meets its contract".
  // Correct, non-vacuous, reset-guarded, conventional.
  property p_done_after_fixed_lat;
    @(posedge clk) disable iff (!rst_n)
      req_accept |-> ##FIXED_LAT done;
  endproperty
  assert property (p_done_after_fixed_lat)
    else $error("completion did not arrive at the fixed latency");

  // Clause 2, written so that it is sound under BOTH configurations.
  // The window is derived from the CONTRACT, not from a constant, so
  // the parameter changes the bound rather than the property's
  // meaning. This is the general repair for variety 10: make the
  // parameter an input to the BOUND, never to the CLAIM.
  property p_done_within_contract_window;
    @(posedge clk) disable iff (!rst_n)
      req_accept |-> ##[MIN_COMPLETION:MAX_COMPLETION] done;
  endproperty
  assert property (p_done_within_contract_window)
    else $error("completion outside the contract's stated window");

  // Clause 3, and it is the property that LICENSES the constant
  // model where the constant model is legitimate. An invariant
  // rather than an implication: under a static contract there is no
  // cycle on which a variable completion is acceptable.
  property p_static_completion_is_constant;
    @(posedge clk) disable iff (!rst_n)
      (!DESTRUCTIVE_READ) -> (completion_spread == '0);
  endproperty
  assert property (p_static_completion_is_constant)
    else $error("a static contract produced a variable completion");

  // Clause 4, which is the one §11 violates. It names
  // `access_outcome` -- the signal the defective block declares and
  // never reads -- and so it cannot pass while that signal is
  // ignored. Variety 2's repair, applied here.
  property p_conflict_waits_for_column;
    @(posedge clk) disable iff (!rst_n)
      (req_accept && access_outcome == OUT_CONFLICT) |->
        (!done throughout (##[1:$] col_commit));
  endproperty
  assert property (p_conflict_waits_for_column)
    else $error("completion reported before the column command issued");

  // Clause 5.
  property p_no_unsolicited_done;
    @(posedge clk) disable iff (!rst_n)
      done |-> $past(in_flight, 1);
  endproperty
  assert property (p_no_unsolicited_done)
    else $error("done asserted with no access in flight");

  // ---- The covers. Without these, every assertion above is a
  //      statement about whichever configuration happened to run.
  // The CONFIGURATION cover. This is variety 10's specific
  // instrument: a regression must be shown to have entered BOTH
  // arms, and §13's contracts_seen is the persistent form of it.
  cover property (@(posedge clk) disable iff (!rst_n)
                  access_outcome == OUT_STATIC);
  cover property (@(posedge clk) disable iff (!rst_n)
                  access_outcome == OUT_CONFLICT);
  cover property (@(posedge clk) disable iff (!rst_n)
                  access_outcome == OUT_MISS);
  // The three-valued case, which is a FINDING rather than a path
  // (7.4). A non-zero count here means the frontend was asked about
  // a bank whose state it had never established.
  cover property (@(posedge clk) disable iff (!rst_n)
                  access_outcome == OUT_UNKNOWN);
  // The antecedent of p_conflict_waits_for_column, published
  // separately: a zero here means no conflict was ever accepted, and
  // that is a different fact from the property holding.
  cover property (@(posedge clk) disable iff (!rst_n)
                  req_accept && access_outcome == OUT_CONFLICT);
  // And the boundary: a hit whose elapsed time equals the minimum.
  // 30.3 §10 -- a rule that is respected but never exercised at its
  // boundary has not been tested.
  cover property (@(posedge clk) disable iff (!rst_n)
                  done && elapsed == MIN_COMPLETION);

  // ---- The frontend's contract (§9), asserted. Every property here
  //      names a signal the frontend drives, so none of them can
  //      pass while that signal is ignored -- variety 2's repair.

  // One command bus, so at most one command may commit per cycle.
  // 17.1 owns the commit point as the single instant architectural
  // state may change. An INVARIANT: there is no cycle on which two
  // commands are acceptable, so there is no antecedent.
  property p_one_command_per_cycle;
    @(posedge clk) disable iff (!rst_n)
      $onehot0({cmd_pre, cmd_act, cmd_col});
  endproperty
  assert property (p_one_command_per_cycle)
    else $error("more than one command committed in a cycle");

  // Legality: no column command before the row-to-column separation
  // has elapsed. 30.3 §5's convention is STATED here -- the column
  // command may issue ON act_cycle + TRCD -- so the comparison is
  // >=, and the property encodes the stated reading rather than
  // silently choosing one of the three.
  property p_no_column_before_trcd;
    @(posedge clk) disable iff (!rst_n)
      (cmd_col && DESTRUCTIVE_READ) |->
        (row_open[cmd_bank] && since_act[cmd_bank] >= TRCD);
  endproperty
  assert property (p_no_column_before_trcd)
    else $error("column command issued before TRCD elapsed");

  // The three-valued discipline of 7.4, as a safety property: an
  // unknown bank state must produce NO command. Treating unknown as
  // idle issues an ACT to a bank that may already have a row open,
  // which is an illegal command rather than a slow one.
  property p_unknown_emits_nothing;
    @(posedge clk) disable iff (!rst_n)
      (access_outcome == OUT_UNKNOWN) |->
        (!cmd_pre && !cmd_act && !cmd_col);
  endproperty
  assert property (p_unknown_emits_nothing)
    else $error("a command was emitted for an unknown bank state");

  // Never activate a bank that already has a row open. This is the
  // property that the OUT_UNKNOWN case exists to protect, and it is
  // stated separately because the two failures have different causes.
  property p_no_act_to_open_bank;
    @(posedge clk) disable iff (!rst_n)
      (cmd_act && DESTRUCTIVE_READ) |-> !row_open[cmd_bank];
  endproperty
  assert property (p_no_act_to_open_bank)
    else $error("activate issued to a bank with a row already open");

  // The CONTRACT invariant, and the one property that is sound under
  // BOTH configurations without reinterpretation -- because the
  // parameter appears in the ANTECEDENT as a condition on the
  // configuration, never inside the claim. §14's test, passed.
  property p_static_emits_no_row_commands;
    @(posedge clk) disable iff (!rst_n)
      (!DESTRUCTIVE_READ) -> (!cmd_pre && !cmd_act);
  endproperty
  assert property (p_static_emits_no_row_commands)
    else $error("a static contract emitted a row-state command");

  // §13's audit, asserted rather than merely reported: the frontend's
  // self-declared obligation count must match the contract its
  // parameters claim. An INVARIANT, and it is the cheapest possible
  // check that the configuration that elaborated is the one intended.
  property p_obligation_count_matches;
    @(posedge clk) disable iff (!rst_n)
      obligation_count == (DESTRUCTIVE_READ ? 8'd13 : 8'd0);
  endproperty
  assert property (p_obligation_count_matches)
    else $error("obligation count disagrees with the contract parameters");

  // ---- Two more covers, both antecedents published separately.
  // The legality boundary for the OTHER two rules, so that "the rule
  // was respected" is distinguishable from "the rule was exercised".
  cover property (@(posedge clk) disable iff (!rst_n)
                  cmd_act && since_pre[cmd_bank] == TRP);
  cover property (@(posedge clk) disable iff (!rst_n)
                  cmd_pre && since_act[cmd_bank] == TRAS);