Refresh Scheduling

Chapter 15.1 established that refresh is specified as an average interval, and drew a distinction it could not yet quantify: due is not late. Chapter 15.2 counted service without ever deciding when to deliver it.

This chapter makes both concrete, and it starts from something that surprises most people the first time they read it:

The specification does not require a refresh command at every nominal interval. It publishes an explicit allowance for postponing and for pulling in refresh, with hard limits — and it states that each pulled-in command reduces the number required later by one.

That last sentence describes a credit ledger, and it is in the datasheet rather than in a controller design paper. Once you have it, “refresh debt” stops being a design metaphor and becomes arithmetic with published bounds.

1. What the Specification Actually Permits

Four things worth extracting before going further, because each becomes a section.

The allowance is a specification feature, not a controller liberty. A controller that postpones refresh is not bending a rule; it is using something the device explicitly offers “to allow for improved efficiency in scheduling.” Chapter 15.1 §2's MIN = N/A was the first half of this; the postponement allowance is the second.

The limits are counts, not durations. Eight commands, not eight microseconds. That makes the natural controller state a counter, and it makes the ledger integer arithmetic rather than a timer comparison.

The bounds scale with the mode, and not proportionally to the count. 8 postponed gives 9 × tREFI; 16 gives 17 × tREFI2. The multiplier is count + 1 in each case, which §3 derives — but note that tREFI2 is itself half of tREFI, so the absolute worst-case gap is not the same across modes. §3 does that arithmetic.

Pull-in and postponement are two directions of one quantity. “Reduces the number required later by one” is a credit. Postponement is a debt. One signed counter represents both, which is §6's design.

2. The Boundary With the Refresh Manager

This chapter and Module 17 both concern refresh scheduling, so the split needs stating plainly before anything else.

  THIS CHAPTER — what the device permits
      the allowance:      8 / 16 / 32 postponed, by mode
      the gap bound:      9 × tREFI  /  17 × tREFI2  /  33 × tREFI4
      the credit rule:    each pull-in reduces later requirement by one
      the state needed:   a signed ledger, and due/urgent/overdue
      → NORMATIVE.  Identical for every controller on that device.

  MODULE 17 — what the controller chooses
      when to defer within the allowance
      how to arbitrate refresh against read/write/activate traffic
      queue structure, admission control, urgency thresholds
      → POLICY.  Different for every controller, and no single answer.

3. Due, Urgent, Overdue — And the Gap Bound

Chapter 15.1 §5 distinguished due from late. §1's allowance lets us name three states precisely, and add a fourth boundary that is easy to miss.

  ON SCHEDULE   debt ≤ 0        service delivered at least as often
                                as nominal; possibly ahead (credit)

  DUE           debt ≥ 1        a nominal interval has elapsed without
                                service. NOT a violation.

  URGENT        debt near the   the allowance is nearly exhausted;
                allowance       further deferral risks the bound

  OVERDUE       debt > allowance   the specification is violated

The allowance in the verified 1X case is 8, so debt may legally reach 8 and a ninth postponement is a violation.

Now the arithmetic the multiplier hides. The bound is (count + 1) × tREFI, which is intuitive — 8 skipped intervals plus the one you are in. But tREFI itself changes with the mode, so the absolute worst-case gap does not stay fixed:

  mode  interval   allowance   multiplier   worst-case gap
  ────────────────────────────────────────────────────────────
   1X    7.8 µs        8          9 ×        70.2 µs
   2X    3.9 µs       16         17 ×        66.3 µs
   4X    1.95 µs      32         33 ×        64.35 µs

The worst-case gap shrinks as the mode gets finer, from 70.2 µs down to 64.35 µs — using the verified tREFI values from Chapter 15.1 §2 and the verified multipliers from §1. That is a genuinely useful and non-obvious result: the finer modes offer proportionally more postponement headroom in commands while permitting a slightly shorter absolute gap. A designer who assumed the modes were equivalent in deferral freedom would be wrong in both directions at once.

4. The Credit Ledger

§1's closing sentence — each pulled-in command reduces the number required later by one — is a conservation statement, and it makes the ledger simple.

Let D be debt: service owed but not delivered. Then:

  every nominal interval elapsing         D  ←  D + 1
  every refresh command accepted          D  ←  D − 1

  D >  0   behind  (postponed commands outstanding)
  D == 0   exactly on schedule
  D <  0   ahead   (credit from pulled-in commands)

One signed counter represents both directions, and the specification bounds it on both sides:

  D  ≤  +8     postponement limit   (1X mode, verified)
  D  ≥  −8     pull-in limit        (1X mode, verified)

Two properties of the ledger worth stating before building it.

It must saturate, not wrap. A debt that wraps from 9 to a small number reports a compliant controller that is violating. Chapter 15.2 §7 made the same argument for ages, and the reasoning is identical: a monitor that makes severe failure look mild is worse than no monitor.

Credit and debt are not symmetric in consequence. Exceeding the debt bound is a correctness violation — data may be lost. Exceeding the credit bound is a specification violation of a different kind: the device says no more than 8 may be issued in advance, and a controller that issues more has done something the standard does not sanction, but nothing decays as a result. §6's block reports both and §13's fourth misconception is about conflating them.

5. The Exact Boundary

Three conventions, because this chapter has three distinct events.

Debt increments on the nominal interval boundary.

  last service accepted at cycle  S
  interval                        I  cycles

  debt increments at  S + I,  S + 2I,  S + 3I, …
  counted from the SERVICE, not from the previous increment

Counting from the service rather than from the last increment is what makes the ledger track the average: a service that arrives late does not shift the schedule forward, so the deficit is preserved. Chapter 15.1 §5's average bound depends on this.

Debt decrements on service acceptance, dated by the cycle the refresh command is accepted — Chapter 15.1 §5's convention, unchanged.

Simultaneous increment and service. If a nominal boundary and an acceptance fall on the same cycle, both apply and the debt is unchanged. Ordering them would be arbitrary and would make the ledger depend on a tie-break that has no architectural meaning.

  candidate refresh at cycle M is COMPLIANT  ⟺  debt_before_service ≤ ALLOWANCE

  and the gap requirement, separately:
       M − S  ≤  (ALLOWANCE + 1) × I

Both must hold. §3's callout is the reason there are two.

6. RTL — A Signed Refresh Ledger

Collision check. Chapter 2.3 §4's refresh_deadline_tracker holds one interval and a MAX_OWED bound, and applies backpressure to traffic. Chapter 15.1 §6's refresh_rate_obligation measures an average over a window. Chapter 15.2 §7's refresh_scope_ledger holds per-resource ages. Chapter 7.5's ref_precondition_check owns the precondition and occupancy.

refresh_deadline_tracker is the closest, and the gap is specific: it has no credit side and no gap bound. Its owed count is unsigned, so pull-in cannot be represented at all, and it bounds the count without bounding the interval — which §3 established are two different requirements.

The new responsibility is the signed ledger with both verified bounds plus the independent gap check. That is not a generic counter; it is the specification's own accounting model, and §1 is the citation for every bound in it.

The engineering problem. Track service owed or credited as a signed quantity, bound it on both sides, separately bound the interval since the last service, and classify urgency so a policy layer has something to act on.

Classification: controller-side service accounting. Counts cycles and events; compares integers. No physical modelling.

// ─────────────────────────────────────────────────────────────────────
//  refresh_credit_ledger
//
//  CLASSIFICATION
//    Controller-side service accounting. Counts cycles and events and
//    compares signed integers. No physical modelling whatsoever.
//
//  WHAT IT MODELS
//    §4's ledger and §1's VERIFIED bounds:
//      debt++ on every nominal interval boundary
//      debt-- on every accepted refresh command
//      debt <= +ALLOWANCE      postponement limit
//      debt >= -CREDIT_LIMIT   pull-in limit
//    plus §3's SEPARATE gap requirement:
//      cycles since last service <= (ALLOWANCE + 1) * INTERVAL
//    and the due / urgent / overdue classification of §3.
//
//  WHAT IT DOES NOT MODEL
//    Charge, leakage, retention, cells or rows -- Chapter 2.2 owns the
//    physics and a controller observes none of it. Nor the refresh
//    precondition or occupancy (Chapter 7.5's ref_precondition_check,
//    reused). Nor per-resource scope (Chapter 15.2's
//    refresh_scope_ledger). And deliberately NOT any POLICY: it
//    reports urgency and never decides, gates, or arbitrates.
//    Module 17 owns the deciding.
//
//  RELATIONSHIP TO EXISTING RTL
//    Chapter 2.3's refresh_deadline_tracker is the single-sided
//    ancestor: it bounds an UNSIGNED owed count and applies
//    backpressure. This block adds the CREDIT side, which the
//    specification explicitly permits and which an unsigned counter
//    cannot represent, and adds the GAP bound, which §3 shows is a
//    separate requirement the count does not imply.
//
//  WHY SIGNED
//    §1's verified sentence -- "each of these REFRESH commands reduces
//    the number of regular REFRESH commands required later by one" --
//    is a conservation statement over a signed quantity. Postponement
//    and pull-in are two directions of one number, and representing
//    them as two unsigned counters would require reconciling them on
//    every event.
//
//  CONVENTION (§5)
//    Interval boundaries are counted FROM THE LAST SERVICE, not from
//    the last boundary, so a late service does not shift the schedule
//    and the deficit is preserved.
//    Service is dated by the cycle the refresh command is ACCEPTED.
//    Simultaneous boundary and service -> BOTH apply, debt unchanged.
//
//  SATURATION
//    Debt saturates at one past each bound rather than wrapping. A
//    wrapped debt reports a compliant controller that is violating,
//    which is the failure mode Chapter 15.2 §7 argued is worse than
//    having no monitor. The saturated value is still distinguishable
//    from the legal maximum, so overdue remains detectable.
//
//  GENERATION SCOPE
//    The BOUNDS are DDR4-verified (§1) and mode-dependent: 8/16/32 by
//    refresh mode. They are parameters, not constants, because
//    Chapter 15.4 shows the mode and the interval both change.
// ─────────────────────────────────────────────────────────────────────
module refresh_credit_ledger #(
  // Nominal interval, in cycles. EDUCATIONAL sizes expected in
  // simulation: Chapter 15.1 §7 explains why a real tREFI must not be
  // simulated directly.
  parameter int INTERVAL     = 8,
  // §1's VERIFIED postponement limit: 8 in 1X mode, 16 in 2X, 32 in 4X.
  parameter int ALLOWANCE    = 8,
  // §1's VERIFIED pull-in limit: 8 in 1X and 2X modes, 32 in 4X.
  parameter int CREDIT_LIMIT = 8,
  // Threshold at which the ledger reports URGENT, so a policy layer
  // has warning before the bound. A POLICY input, not a specification
  // value -- see §2. Must be at or below ALLOWANCE.
  parameter int URGENT_AT    = 6,
  // Signed debt width. Must hold -(CREDIT_LIMIT+1) .. +(ALLOWANCE+1)
  // so that saturation lands one past each bound and stays
  // distinguishable from the legal extreme.
  parameter int DEBT_W = 2 + ((ALLOWANCE > CREDIT_LIMIT)
                                ? $clog2(ALLOWANCE + 2)
                                : $clog2(CREDIT_LIMIT + 2)),
  // Interval counter, and the gap counter which must reach
  // (ALLOWANCE+1)*INTERVAL.
  parameter int ICNT_W = (INTERVAL <= 1) ? 1 : $clog2(INTERVAL + 1),
  parameter int GAP_W  = $clog2(((ALLOWANCE + 1) * INTERVAL) + 2)
) (
  input  logic                    clk,
  input  logic                    rst_n,

  // ── A refresh command was ACCEPTED this cycle.
  input  logic                    service_accepted,

  // ── §4's signed ledger. Positive = behind, negative = ahead.
  output logic signed [DEBT_W-1:0] debt,

  // ── §3's four states. Mutually exclusive by construction.
  output logic                    on_schedule,
  output logic                    due,
  output logic                    urgent,
  output logic                    overdue,

  // ── §3's SEPARATE gap requirement. Cycles since the last service,
  //    and whether the verified bound has been exceeded. This is NOT
  //    implied by the debt bound -- see §3's callout.
  output logic [GAP_W-1:0]        cycles_since_service,
  output logic                    gap_exceeded,

  // ── Bound violations, reported separately because §4 explains they
  //    have different consequences: debt overflow risks DATA, credit
  //    overflow does not.
  output logic                    debt_bound_violated,
  output logic                    credit_bound_violated,

  // ── A nominal boundary occurred this cycle. Published so §8's trace
  //    and §11's checker can align against it.
  output logic                    interval_tick
);

  // ── Elaboration guards.
  if (INTERVAL < 1) begin : g_int
    initial $fatal(1, "refresh_credit_ledger: INTERVAL must be >= 1");
  end
  if (ALLOWANCE < 0) begin : g_allow
    initial $fatal(1, "refresh_credit_ledger: ALLOWANCE must be >= 0");
  end
  if (CREDIT_LIMIT < 0) begin : g_credit
    initial $fatal(1, "refresh_credit_ledger: CREDIT_LIMIT must be >= 0");
  end
  // An urgent threshold above the allowance could never fire before
  // the bound, defeating its purpose. Refused at elaboration.
  if (URGENT_AT > ALLOWANCE) begin : g_urgent
    initial $fatal(1, "refresh_credit_ledger: URGENT_AT must be <= ALLOWANCE");
  end

  localparam int DEBT_MAX = ALLOWANCE    + 1;   // saturation, one past
  localparam int DEBT_MIN = -(CREDIT_LIMIT + 1);
  localparam int GAP_MAX  = ((ALLOWANCE + 1) * INTERVAL) + 1;

  logic signed [DEBT_W-1:0] debt_q;
  logic [ICNT_W-1:0]        icnt;
  logic [GAP_W-1:0]         gap_q;
  logic                     tick;

  always_comb begin
    // §5: the boundary is counted from the last SERVICE. icnt is reset
    // by service, so a boundary occurs when it completes one interval.
    tick          = (icnt == ICNT_W'(INTERVAL - 1));
    interval_tick = tick;

    debt                 = debt_q;
    cycles_since_service = gap_q;

    // §3's classification. Ordered so exactly one is high.
    overdue     = (debt_q >  DEBT_W'(ALLOWANCE));
    urgent      = !overdue && (debt_q >= DEBT_W'(URGENT_AT))
                           && (DEBT_W'(URGENT_AT) > DEBT_W'(0));
    due         = !overdue && !urgent && (debt_q >= DEBT_W'(1));
    on_schedule = !overdue && !urgent && !due;

    // §3's separate gap check, against the VERIFIED bound.
    gap_exceeded = (gap_q > GAP_W'((ALLOWANCE + 1) * INTERVAL));

    // §4: different consequences, reported separately.
    debt_bound_violated   = (debt_q >  DEBT_W'(ALLOWANCE));
    credit_bound_violated = (debt_q <  -DEBT_W'(CREDIT_LIMIT));
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      // Reset asserts on-schedule with no history. Chapter 15.2 §7's
      // reset note applies: this is an optimistic convenience, and the
      // device's own initialisation sequence is what actually
      // establishes a known refresh state.
      debt_q <= '0;
      icnt   <= '0;
      gap_q  <= '0;
    end else begin
      // ── Interval counter. Reset by service per §5, so boundaries
      //    are measured from the service and a late service does not
      //    shift the schedule.
      if (service_accepted) begin
        icnt <= '0;
      end else if (tick) begin
        icnt <= '0;
      end else begin
        icnt <= icnt + 1'b1;
      end

      // ── Gap counter. Reset only by service; saturating so a long
      //    neglect reports truthfully instead of wrapping.
      if (service_accepted) begin
        gap_q <= '0;
      end else if (gap_q != GAP_W'(GAP_MAX)) begin
        gap_q <= gap_q + 1'b1;
      end

      // ── §4's ledger, with §5's simultaneity rule: a boundary and a
      //    service on the same cycle both apply and cancel, so the
      //    debt is unchanged. Written as one case over both events so
      //    the two updates cannot disagree.
      case ({tick, service_accepted})
        2'b10: if (debt_q < DEBT_W'(DEBT_MAX)) debt_q <= debt_q + DEBT_W'(1);
        2'b01: if (debt_q > DEBT_W'(DEBT_MIN)) debt_q <= debt_q - DEBT_W'(1);
        default: debt_q <= debt_q;     // 2'b00 idle, 2'b11 cancels
      endcase
    end
  end

endmodule

Interface contract. debt is signed — a consumer treating it as unsigned reads credit as a very large debt and will force refresh when the controller is ahead. The four state outputs are mutually exclusive by construction. gap_exceeded is deliberately not folded into overdue, because §3 established they are separate requirements and a report that conflates them cannot say which was violated.

Parameter contract. ALLOWANCE and CREDIT_LIMIT carry §1's verified values and are mode-dependent — 8/16/32 and 8/8/32 respectively — which is why they are parameters. URGENT_AT is a policy input, must be at or below ALLOWANCE, and is enforced at elaboration: a threshold above the bound could never fire in time to be useful. DEBT_W is sized for −(CREDIT_LIMIT+1) … +(ALLOWANCE+1) so saturation lands one past each bound and stays distinguishable from the legal extreme — a saturation at the bound would make a violating ledger read as exactly compliant.

Why the interval counter is reset by service. §5's convention, and it is the subtle part. Resetting on the boundary instead would make each interval run from the previous boundary, so a service arriving late would silently re-phase the schedule and the deficit would vanish. Resetting on service preserves the deficit, which is what makes the ledger track an average rather than a rolling timer.

Corner cases. ALLOWANCE == 0: no postponement permitted, so any debt is immediately overdue — a legal configuration representing a strict policy, and the degenerate case §2 calls out. CREDIT_LIMIT == 0: pull-in forbidden; debt cannot go negative. URGENT_AT == 0: the urgent term is guarded so it does not swallow on_schedule, which is why the comparison includes URGENT_AT > 0. Simultaneous tick and service: both apply, debt unchanged, and icnt resets from the service path. Debt at saturation: stops moving and keeps reporting, so overdue stays high.

Synthesis implications. One signed counter, two unsigned counters, four comparators. The gap counter is the widest — (ALLOWANCE+1) × INTERVAL is thousands of cycles at a real interval, so about 17 bits for 1X DDR4 at a typical clock. Still trivial.

Failure modes. Treating debt as unsigned — credit reads as enormous debt and the controller force-refreshes while ahead. Resetting icnt on the tick rather than on service — the schedule re-phases and the deficit disappears, so a persistently late controller reports on-schedule. Wrapping instead of saturating — a violating ledger reads compliant. Omitting the gap check — §3's separate requirement goes unverified, and a controller sitting at the allowance for a long stretch passes the count bound while exceeding the interval bound. Saturating at the bound rather than one past it — overdue becomes indistinguishable from exactly-compliant.

7. The Ledger, in Cycles

Cycles 4 through 7 are the point. The debt is 1, the state is DUE, and nothing is wrong — the specification permits it and §1 is the citation. A controller that treated this as a violation would preempt traffic for no reason.

The gap counter climbs to 8 and the bound is 12. So there were four cycles of headroom left at the moment of service. That number is the one a policy layer wants, and it is the reason cycles_since_service is published rather than only gap_exceeded.

8. Worked Trace — Refresh Becoming Due Under Load

Now the trace §34 of this module's brief requires: normal traffic, refresh becoming due, in-flight work blocking preparation, and service resuming.

The command stream. Last refresh service at cycle 0, so debt increments at 8, 16, 24 and the gap bound expires at cycle 24.

  cycle  0   REF accepted                    (given)
  cycle  2   WRITE bank 1                    admitted
  cycle  8   interval boundary               debt → 1   (DUE)
  cycle 10   candidate: PRECHARGE all        analyse
  cycle 13   candidate: REF                  analyse
  cycle 16   interval boundary               debt → ...

Candidate 1 — PRECHARGE all at cycle 10

Refresh state: debt 1, DUE. Gap 10 of 24 — comfortable. Blocker: the write at cycle 2 has its last data at cycle 5, so tWR permits precharge from 5 + 5 = 10. Verdict: 10 >= 10 — legal, issue. The preparation can begin exactly now.

Candidate 2 — REF at cycle 13

Refresh state: debt 1, DUE. Blocker: precharge accepted at 10, so tRP permits refresh from 10 + 3 = 13. Verdict: 13 >= 13 — legal, issue. Debt drops to 0. Gap resets. Occupancy: the resource is unavailable for 4 cycles; the first legal conflicting command is cycle 13 + 4 = 17 (Chapter 15.5 owns that boundary).

The whole trace

Three things this trace demonstrates that a definition cannot.

Being DUE at cycle 8 was not a failure and required no panic. The controller had 16 cycles of gap headroom left. It spent 2 waiting for tWR, 3 on tRP, and serviced at 13 — comfortably inside the allowance. §7's point, in a real sequence.

The blocker was a Module 14 obligation, not a refresh one. tWR from a write admitted six cycles before the boundary is what determined when preparation could start. Refresh scheduling is mostly about other people's timing obligations, which is why §9's failure trace is about admission rather than about refresh.

The preparation cost is deterministic and computable in advance. W + 11. A controller that knows this can answer a question §9 makes central: given the deadline, what is the last cycle at which I may admit a write?

9. Worked Trace — The Deadline Failure, and Where the Bug Began

Now the trace §35 requires, and the question it exists to answer.

Same constraints as §8. Last service at cycle 0, so the gap bound expires at cycle 24. The controller keeps admitting writes.

  cycle  0   REF accepted                       gap bound → 24
  cycle  6   WRITE admitted      → refresh possible from  6 + 11 = 17
  cycle 10   WRITE admitted      → refresh possible from 10 + 11 = 21
  cycle 14   WRITE admitted      → refresh possible from 14 + 11 = 25   ← past 24
  cycle 18   WRITE admitted      → refresh possible from 18 + 11 = 29
  cycle 24   GAP BOUND EXPIRES   — refresh still not issuable
  cycle 29   REF finally accepted                        5 cycles late

This is the central controller-design lesson of the module, and it generalises past refresh.

The check that would have prevented it is an admission check, not a refresh check. Before admitting work, ask whether the deadline remains reachable afterwards:

  admit new work at cycle C  only if
      C + preparation_cost  ≤  deadline

  here:  C + 11 ≤ 24   →   C ≤ 13

Cycle 13 is the last safe admission, and the controller admitted at 14. One cycle past a limit it never computed.

10. Five Assertions Worth Writing

// ── P1. SAFETY-shaped: debt never exceeds the verified allowance
//    without overdue being reported. The count bound of §1.
property p_debt_bound_is_reported;
  @(posedge clk) disable iff (!rst_n)
    (debt > DEBT_W'(ALLOWANCE)) |-> (overdue && debt_bound_violated);
endproperty
a_debt_bound_is_reported: assert property (p_debt_bound_is_reported);

// ── P2. §3's SEPARATE requirement: the interval bound. Catches the
//    design that bounds the COUNT and believes it has bounded the GAP.
//    A controller sitting at the allowance for a long stretch passes
//    P1 continuously and fails this.
property p_gap_bound_is_reported;
  @(posedge clk) disable iff (!rst_n)
    (cycles_since_service > GAP_W'((ALLOWANCE + 1) * INTERVAL))
      |-> gap_exceeded;
endproperty
a_gap_bound_is_reported: assert property (p_gap_bound_is_reported);

// ── P3. §4's conservation: debt moves by exactly one per event, in
//    the right direction, and a simultaneous tick and service cancel.
//    Catches an ordering that drops one of the two, which makes a
//    persistently-late controller report on-schedule.
property p_ledger_conserves;
  @(posedge clk) disable iff (!rst_n)
    ( ($past(interval_tick, 1) && !$past(service_accepted, 1)
       && ($past(debt, 1) < DEBT_W'(ALLOWANCE + 1)))
        |-> (debt == $past(debt, 1) + DEBT_W'(1)) )
    and ( (!$past(interval_tick, 1) && $past(service_accepted, 1)
           && ($past(debt, 1) > -DEBT_W'(CREDIT_LIMIT + 1)))
            |-> (debt == $past(debt, 1) - DEBT_W'(1)) )
    and ( ($past(interval_tick, 1) && $past(service_accepted, 1))
            |-> (debt == $past(debt, 1)) );
endproperty
a_ledger_conserves: assert property (p_ledger_conserves);

// ── P4. The four states are mutually exclusive and exhaustive.
//    Catches overlapping thresholds, which would let a consumer read
//    two contradictory states and act on whichever it sampled.
property p_states_are_exclusive;
  @(posedge clk) disable iff (!rst_n)
    ($countones({on_schedule, due, urgent, overdue}) == 1);
endproperty
a_states_are_exclusive: assert property (p_states_are_exclusive);

// ── P5. Debt saturates ONE PAST each bound, not at it. Catches the
//    subtle failure where saturation lands on the legal maximum and
//    a violating ledger becomes indistinguishable from an exactly
//    compliant one.
property p_saturation_stays_distinguishable;
  @(posedge clk) disable iff (!rst_n)
    (debt == DEBT_W'(ALLOWANCE + 1)) |-> overdue;
endproperty
a_saturation_stays_distinguishable:
  assert property (p_saturation_stays_distinguishable);

// ── C1. BOUNDED-SERVICE coverage. Chapter 15.1 §9's distinction: the
//    interesting states must be REACHED or the properties above are
//    vacuous. The overdue cover is the one people omit -- a ledger
//    never observed to report a violation is not known able to.
c_reached_due:     cover property (@(posedge clk) disable iff (!rst_n) due);
c_reached_urgent:  cover property (@(posedge clk) disable iff (!rst_n) urgent);
c_reached_overdue: cover property (@(posedge clk) disable iff (!rst_n) overdue);
c_reached_credit:  cover property (@(posedge clk) disable iff (!rst_n)
                                     (debt < DEBT_W'(0)));

What these prove. That both of §1's bounds are reported, separately; that the ledger conserves and handles simultaneity as documented; that the states are well-formed; and that saturation stays distinguishable from compliance.

What these do not prove. Three gaps, and the second is the chapter's.

Nothing proves INTERVAL, ALLOWANCE or CREDIT_LIMIT are right for the device and mode. They are parameters, and §1's verified values are mode-dependent — 8, 16 or 32. A ledger configured with the 4X allowance on a device in 1X mode permits four times the legal postponement with every property passing. Chapter 15.4 owns the mode and interval selection, and this is a configuration check no simulation discharges.

Nothing proves the deadline was reachable. §9's entire lesson is that the violation is determined by an admission decision many cycles before the bound expires, and this block cannot see admissions. It reports the state and the remaining gap; the guard that matters — deadline − preparation_cost — needs a scheduler's knowledge and belongs to Module 17.

Nothing proves the data survived. Chapter 15.1 §8's boundary, unchanged.

Vacuity. P3's three conjuncts each need their antecedent; the simultaneous case in particular requires a tick and a service to coincide, which random stimulus produces rarely. C1's four covers exist for that reason, and the overdue and credit ones are the commonly missing pair.

11. DV — An Independent Service Ledger

Invert the representation. The design holds a signed counter driven by events. A checker should hold a service timestamp list and compute the expected debt as floor((now − first_service) / INTERVAL) − services_delivered. That is a completely different computation from an incrementing counter, so it cannot reproduce an increment-ordering or a simultaneity bug.

Check both bounds independently. §3 established the count and the gap are separate requirements, and a checker that derives one from the other has collapsed them.

Recompute the allowance from the mode. This is the chapter-specific obligation. §1's limits depend on the refresh mode, and the mode is set by a mode-register write. A checker should decode the mode from the observed MRS traffic and select the allowance from it, rather than reading the design's ALLOWANCE parameter — because §10's first limitation is that a mis-configured allowance passes every property.

  REFRESH DEADLINE VIOLATION
    generation        : DDR4, 1X refresh mode        [mode decoded from MRS]
    resource          : rank 0
    last service      : cycle 1200
    nominal interval  : 200 cycles     (educational)
    allowance         : 2 commands     [1X mode → verified limit]
    gap bound         : 600 cycles     = (2+1) × 200
    observed service  : cycle 1829
    gap               : 629 cycles     → EXCEEDED by 29
    debt at violation : 3              → exceeded allowance by 1
    ─────────────────────────────────────────────────────────────────
    blocker at bound  : write recovery on bank 5, precharge legal 1831
    LAST SAFE ADMIT   : cycle 1789     = deadline − preparation cost
    admitted anyway   : cycle 1794     ← THE BUG, 35 cycles before
                                          the bound expired
    root question     : why was work admitted after the deadline
                        became unreachable?

The two lines to steal are LAST SAFE ADMIT and admitted anyway. Every other line describes the violation; those two describe the cause, and they place it 35 cycles earlier than the timestamp the violation carries. §9 is the argument for why that is the number a debugging engineer actually needs.

And reporting both bound checks separately matters. A report saying only “deadline violation” cannot distinguish a controller that exceeded the count from one that exceeded the interval, and §3 established those are different failures with different fixes.

12. Debugging

Symptom. Refresh deadlines missed, and only under heavy write traffic.

The discriminator that defines this chapter is whether an admission followed the last-safe-admit cycle. It is a one-line computation per violation, it needs no rerun if the admission log exists, and it distinguishes a scheduling-policy bug from a ledger bug — which are in different modules and different files.

The second discriminator is which bound was exceeded. Count versus gap, per §3. A count violation means too much cumulative deferral; a gap violation means one stretch ran too long. Different causes, and a report that says only “late” distinguishes neither.

Responsible layer. If the ledger's bounds are correct for the mode, no admission followed the safe line, and refresh is still late, then the preparation cost itself is the problem — the in-flight work takes longer to drain than the allowance can absorb, which is a capacity question for Module 17 rather than a bug.

13. Common Misconceptions

“Every tREFI cycles, issue refresh immediately.” Tempting because it is trivially compliant, simple, and feels safe. Why it is wrong: §1 verified that the specification explicitly provides postponement “to allow for improved efficiency in scheduling”. Immediate service is a policy and a conservative one. Consequence: refresh preempts traffic at moments when deferral was legal, so latency spikes are self-inflicted. Replacement model: the allowance is a specification feature to be used deliberately. Debugging clue: refresh always issues at a fixed phase, never deferred, and adding a smarter scheduler changes nothing.

“The controller can postpone refresh indefinitely if traffic is busy.” Tempting because the allowance exists and busy traffic is a real pressure. Why it is wrong: the allowance is bounded — §1's verified 8/16/32 commands by mode, and a gap bound on top. Consequence: a controller that defers under load until data is lost, with the loss appearing far from the deferral. Replacement model: bounded flexibility, with two separate bounds. Debugging clue: deadline misses that correlate with traffic density.

“Refresh debt is the same thing as the refresh cycle time.” Tempting because both are “refresh numbers” and both grow the amount of refresh work outstanding in some loose sense. Why it is wrong: Chapter 15.1 §3 — debt is a count of service owed, and cycle time is how long the resource is unavailable once service starts. Different units, different axes, different owners. Consequence: a design that sizes a debt counter from a duration, or that treats occupancy as if it discharged debt. Replacement model: debt is an integer count; occupancy is a duration. Debugging clue: a debt counter whose width was chosen from a time value.

“Exceeding the credit limit is as dangerous as exceeding the debt limit.” Tempting because both are bounds in the same sentence of the same datasheet. Why it is wrong: §4 — exceeding debt risks data, because service was not delivered in time. Exceeding credit means issuing more refresh in advance than the device sanctions, and nothing decays as a result. Both are specification violations; only one loses data. Consequence: a design that treats them with equal urgency, or worse, one that treats debt with the mildness appropriate to credit. Replacement model: two bounds, two very different consequences. Debugging clue: a report that does not say which bound was crossed.

“Bounding the postponement count bounds the gap.” Tempting because the count and the gap are both in §1's allowance and the multiplier count + 1 connects them. Why it is wrong: §3 — the count limits how far behind you are, and a controller can sit at the limit for a long stretch while servicing just often enough to avoid exceeding it. The specification bounds the interval separately. Consequence: a design and a monitor that both check the count and neither checks the gap. Replacement model: two requirements, two checks. Debugging clue: debt never exceeds the allowance and deadline violations still occur.

“An urgency threshold prevents deadline misses.” Tempting because stopping admission when urgent is obviously better than not doing so, and it does help. Why it is wrong: §9 — urgency is computed from the debt, and the quantity that determines reachability is the preparation cost of in-flight work. Urgency arrived two cycles after the violation was already unavoidable. Consequence: a controller with a correct-looking guard that still misses deadlines under write-heavy load. Replacement model: guard on deadline − preparation_cost, which needs a scheduler's knowledge. Debugging clue: the last admission before a violation precedes the urgency assertion.

“A late deadline means the bug happened at the deadline.” Tempting because that is where the violation is detected and where the timestamp points. Why it is wrong: §9's trace — the violation became unavoidable eleven cycles earlier, at an admission that looked entirely unremarkable. Consequence: debugging starts at the wrong cycle and examines the refresh path, which is working correctly, instead of the admission path, which is not. Replacement model: find the last cycle at which the deadline was still reachable. Debugging clue: everything in the refresh path looks correct at the moment of violation, because it is.

14. Interview Reasoning

“Why can a controller not always issue refresh the instant it becomes due?” Because refresh has a precondition — the affected resources must be prepared — and preparing them means draining in-flight work and honouring its timing obligations first. A write in flight arms write recovery, which delays precharge, which delays refresh. So the earliest possible refresh is set by other people's obligations, not by the refresh logic. And the good news is that it does not need to: the specification explicitly permits postponement, bounded at 8 commands in 1X mode, precisely so the controller has room to finish what it started.

“What is refresh debt?” The count of refresh service owed but not yet delivered — incremented at each nominal interval and decremented by each accepted command. It is signed, because the device also permits pulling in refresh, and the datasheet states that each pulled-in command reduces the number required later by one. That is a conservation statement, which makes one signed counter the natural representation: positive is behind, negative is ahead, and both directions are bounded.

“What does it mean for refresh to be due but not late?” Due means a nominal interval elapsed without service, so the debt is at least one. Late means the allowance is exhausted. The gap between them is a specification feature rather than slack a designer invented — verified at 8 postponed commands in 1X mode, with the resulting worst-case interval bounded at nine times the nominal. A controller that treats due as a violation throws that away and preempts traffic for no correctness benefit.

“Does bounding the debt bound the worst-case gap?” No, and this is the subtlety worth volunteering. The count limits how far behind you are; a controller can hold the debt at the limit for a long stretch while servicing just often enough never to exceed it, producing an interval far longer than intended. The specification bounds the two separately — a count limit and an explicit interval limit — so a design needs two checks, and a monitor that derives one from the other has collapsed them.

“Why can continuing to admit writes after refresh becomes due cause a deadline miss?” Because each admitted write extends the preparation cost. A write accepted at cycle C pushes the earliest possible refresh to roughly C plus write latency plus burst plus write recovery plus precharge time. Once that sum passes the deadline, the violation is unavoidable no matter what happens next. The uncomfortable part is that the controller's refresh state can look entirely healthy at that moment — merely due, with plenty of gap left — so nothing signals the mistake.

“A refresh deadline was missed at cycle 1829. When did the bug happen?” Almost certainly well before. Compute the deadline, subtract the preparation cost of the work in flight, and find the last admission after that line — that is the cycle the deadline became unreachable, and everything afterwards is consequence. In a realistic case that can be tens of cycles earlier than the violation timestamp. The practical consequence is that debugging should start in the admission path, which is broken, rather than the refresh path, which is working.

“Why is an urgency signal not sufficient to guard admission?” Because urgency is derived from the debt, and the debt says how far behind you are rather than how long recovery will take. The binding quantity is the preparation cost of in-flight work, which depends on writes, bursts and Module 14's obligations — none of which the debt reflects. So urgency is a lagging indicator, and in a write-heavy trace it can assert after the deadline has already become unreachable.

15. Engineering Exercises

1. Compute the verified bounds. Using §1's rules and Chapter 15.1 §2's verified intervals, give the worst-case gap in microseconds for 1X, 2X and 4X modes. Which mode permits the longest absolute gap?

Worked: 1X is 9 × 7.8 = 70.2 µs; 2X is 17 × 3.9 = 66.3 µs; 4X is 33 × 1.95 = 64.35 µs. 1X permits the longest absolute gap, which is the opposite of what the command counts suggest — 4X allows four times as many postponed commands and a slightly shorter absolute stretch. Noticing that the two measures disagree is the point.

2. Build the ledger by hand. Interval 10 cycles, allowance 2. Service at cycle 0. Then service at 35, 42 and 44. Give the debt after each event and say whether anything was violated.

Worked: boundaries from the last service. From 0: boundaries at 10, 20, 30 → debt 1, 2, 3. Debt 3 exceeds the allowance of 2 at cycle 30 — violated. Service at 35 → debt 2; gap was 35 against a bound of 3 × 10 = 30, so the gap was also exceeded. Service at 42 → after the 35 service, a boundary at 45 has not arrived, so debt goes to 1. Service at 44 → debt 0. Both bounds were violated and by different amounts, which is §3's argument in numbers.

3. Find the last safe admission. Using §8's constraints — preparation cost 11 cycles — and a deadline at cycle 60, give the last cycle at which a write may be admitted. Then recompute if tWR were 8 instead of 5.

Worked: C + 11 ≤ 60 → C ≤ 49. With tWR of 8 the cost becomes 3 + 8 + 3 = 14, so C ≤ 46 — three cycles earlier. The instructive part: a Module 14 parameter the refresh logic never mentions moved the refresh admission limit. That is why §9's guard cannot live in the ledger.

4. Locate the causal cycle. A controller with a deadline at 100 and a preparation cost of 15 admits writes at cycles 70, 78, 86 and 94. At which cycle did the deadline become unreachable, and what does the controller's debt look like there?

Worked: last safe admission is 100 − 15 = 85. Admissions at 70 (→85, exactly reachable) and 78 (→93) are fine; the admission at 86 is the bug, giving an earliest refresh of 101. Its debt at cycle 86 depends on the interval but will be small and unalarming — which is the whole lesson. The admission at 94 makes it worse and is not the cause.

5. Break the interval convention. Modify §6's block to reset icnt on the tick rather than on service. Construct a stimulus where a persistently late controller then reports on_schedule, and say which property catches it.

Worked: with icnt reset on the tick, boundaries occur every INTERVAL cycles regardless of service, so a service arriving just before each boundary decrements the debt as fast as it increments and the debt hovers near zero — even though the actual service interval is nearly twice nominal. P3 still passes, because the ledger conserves correctly against the ticks it sees. What catches it is P2's gap check, which measures cycles since service and is unaffected by the re-phasing. That makes P2 doubly important: it catches both the omitted-gap-check design and this one.

6. Distinguish the bounds. Construct two failing scenarios: one that exceeds the count bound without exceeding the gap bound, and one that does the reverse. Is the second possible?

Worked: exceeding the count without the gap requires many small deferrals with frequent service — take interval 10, allowance 2: boundaries at 10, 20, 30 with no service reaches debt 3 at cycle 30, and the gap bound of 30 is met exactly but not exceeded, so count violated, gap not (just barely). The reverse is harder: since the gap bound is (allowance + 1) × interval, exceeding the gap means at least allowance + 1 boundaries elapsed without service, which also exceeds the count. So a gap violation implies a count violation, but not conversely — which is a genuinely useful asymmetry and a better answer than assuming independence.

7. Write the admission guard. Sketch the check §9 says belongs in Module 17, name every input it needs, and say which of those the ledger of §6 does not have.

16. Summary

The specification does not require refresh at every nominal interval. Verified from Micron's 16Gb DDR4 datasheet: flexibility is explicitly provided “for postponing and pulling in” the command, with a maximum of 8 postponed in 1X mode, 16 in 2X and 32 in 4X, and the resulting interval bounded at 9 × tREFI, 17 × tREFI2 and 33 × tREFI4 respectively. Pull-in is permitted and bounded too, and the datasheet states that each pulled-in command reduces the number required later by one — a conservation statement that makes refresh debt a signed ledger rather than a metaphor.

This chapter owns what the device permits; Module 17 owns what the controller chooses. A stricter policy is always legal, and confusing a policy limit with the standard's limit fails in both directions.

Four states, not two. On schedule, due (debt at least one, and not a violation), urgent (allowance nearly exhausted), and overdue. And two bounds, not one: the count limits how far behind you may be, and the gap separately limits how long one stretch may run — a controller can hold the debt at the allowance indefinitely and pass the count check while exceeding the interval. §15's sixth exercise shows the asymmetry: a gap violation implies a count violation, not the reverse.

The mode arithmetic is non-obvious. Because tREFI itself halves with the mode, the absolute worst-case gap shrinks as the mode gets finer — 70.2, 66.3, 64.35 µs — even though the command allowance quadruples. The two measures of deferral freedom disagree.

refresh_credit_ledger holds the signed debt with both verified bounds, checks the gap separately, saturates one past each bound so a violation stays distinguishable from exact compliance, and counts intervals from the last service so a late service cannot silently re-phase the schedule. It reports urgency and decides nothing.

And §9 is the module's most transferable lesson. A deadline missed at cycle 24 became unavoidable at cycle 14, when the controller admitted a write whose preparation cost pushed the earliest possible refresh past a deadline that was already fixed. At that moment the ledger read debt 1, state DUE, with ten cycles of gap left — nothing looked wrong. Urgency arrived two cycles too late, because urgency is derived from how far behind you are and the binding quantity is how long recovery will take. The correct guard is deadline − preparation_cost, it needs a scheduler's knowledge, and a controller watching only its debt is watching the wrong variable.

17. What Comes Next

Every interval in this chapter has been a parameter supplied from somewhere, and Chapter 15.1 §4 derived it as a retention window divided by a command count while admitting it could verify neither factor.

Chapter 15.4 takes up the interval itself: how a distribution of per-cell retention times — which Chapter 2.2 established is what physically exists — becomes a single specification number that a controller can count against. And it takes up the variable this chapter has quietly treated as fixed: temperature, where the verified table halves the interval twice across the operating range, and where §1's allowance is measured in a tREFI that is itself a function of the operating condition.

That has a consequence worth anticipating. A controller configured for one temperature band and operated in another is not merely refreshing at the wrong rate — its entire postponement allowance is denominated in the wrong unit.