DDR vs LPDDR

   A1  read destroys the stored value        -- SAME for both
        -> restore is part of the access     -- SAME
        -> a rebuilt row is held somewhere   -- SAME (row buffer)
        -> access cost depends on what is held -- SAME (C2 answered "yes")
        -> completion time is not constant   -- SAME (C1 "neither")
        -> "which row is open" is controller state -- SAME
   charge leaks while idle                   -- SAME
        -> periodic rewrite is mandatory      -- SAME
        -> the memory needs the bus for itself -- SAME (C3 "yes")

   Let D  = duty cycle, the fraction of time the memory is active
       T  = the interval being accounted over
       Pa = active power for the profile
       Pi = idle power for the profile
       W  = the work delivered in the interval (bits)

   average power   =  D x Pa  +  (1 - D) x Pi
   energy per bit  =  ( D x Pa + (1 - D) x Pi ) x T  /  W

   now DIFFERENCE the two profiles. Let

       dPi = Pi(sustained) - Pi(low-power)     the IDLE advantage
       dPa = Pa(low-power) - Pa(sustained)     the ACTIVE penalty
                                               (sign not assumed)

   the low-power profile is ahead when

       (1 - D) x dPi   >   D x dPa

   and the crossover duty cycle is

       D*  =  dPi / ( dPi + dPa )

   D*  =  4 / (4 + 6)  =  0.40

   so at duty cycles below 40% the low-power profile is ahead, and
   above 40% the sustained profile is.

   recompute at dPi = 4, dPa = 2:   D* = 4/6  = 0.667
   recompute at dPi = 1, dPa = 6:   D* = 1/7  = 0.143

   DERIVED, all three. Note the sensitivity: a fourfold change in
   the idle advantage moves the crossover from 14% to 67%. The
   crossover is NOT a robust constant, which is why §16 measures it
   rather than assuming it.

   against §5's ILLUSTRATIVE D* = 0.40 :

     a phone in a pocket                D ~ 0.02   -> far BELOW D*
     a phone sustaining a camera
       or game pipeline                 D ~ 0.5+   -> ABOVE D*
     a server running sustained
       analytics                        D ~ 0.7+   -> far above D*
     an edge node or a burst-scaled
       instance, idle between requests  D ~ 0.05   -> far BELOW D*

   DERIVED reading: two of the four cases sit on the side of the
   crossover their MARKET SEGMENT does not predict.

   DDR legality, one dimension:

       legal(cmd)  =  ( elapsed >= required )  for every applicable rule
                   =  a MAXIMUM over candidates  (13.3, 30.3 §3)

   LPDDR legality, two dimensions:

       legal(cmd)  =  TIMING_LEGAL(cmd)                  -- as above
                 AND  STATE_ADMITS(cmd, device_state)    -- NEW

   and the two are NOT commensurable:

     TIMING_LEGAL  becomes true by WAITING.
     STATE_ADMITS  becomes true only by ACTING -- something must
                   issue an exit, and the exit is itself a command
                   that the current state must admit.

// ---------------------------------------------------------------------
// access_admission -- the parameterised comparative block of §10.
//
// CLASSIFICATION: synthesisable, ILLUSTRATIVE parameter values, and
// CORRECT as written. The intentionally defective block is §11.
//
// WHAT IT IS: the admission gate for one access, under either
// profile. It extends 31.1 §9's frontend along exactly one axis --
// §8's second legality dimension -- and deliberately keeps the first
// dimension identical, because §2 established that the thirteen
// shared obligations do not differ between these technologies.
//
// WHY IT EXISTS HERE: §8 argues that TIMING_LEGAL becomes true by
// WAITING and STATE_ADMITS becomes true only by ACTING, and that a
// scheduler conflating them waits forever. The two output signals
// below are that argument: `blocked_by_timing` and
// `blocked_by_state` are never merged, so 30.5 §3's question "why
// has it not issued" has a distinct answer for each.
//
// HOW TO RUN IT: elaborate with PROFILE_LOW_POWER = 1, drive the
// device into a low-power state, and present an access.
// EXPECTED RESULT: admit is low, blocked_by_state is HIGH and
// blocked_by_timing is LOW -- and `exit_req` is asserted, because
// the state dimension requires an ACTION rather than a wait.
// EXPECTED TRACE: no timing counter is what blocks the access, and
// the block says so on a dedicated output.
//
// SYNTHESIS: a transition-legality ROM plus the shared per-bank
// counters. The sustained profile elaborates neither the ROM nor the
// state register.
//
// LIMITATIONS: models the ADMISSION test, not the policy that chooses
// when to enter a low-power state -- 24.2 §6 owns that selector and
// this block does not duplicate it. It models one outstanding access
// so the two dimensions, rather than concurrency, are what the
// reader compares.
// ---------------------------------------------------------------------
module access_admission #(
  // The profile parameter. Unlike 31.1's DESTRUCTIVE_READ this one
  // does NOT change the access contract -- §1 -- so it is a
  // FEATURE-SET parameter rather than a contract parameter, and
  // 31.1 §12's warning about re-deriving obligations applies with
  // less force. It still changes the INTERFACE, which §14 tests.
  parameter bit PROFILE_LOW_POWER = 1'b1,

  parameter int BANKS   = 8,
  parameter int TRCD    = 14,   // ILLUSTRATIVE
  parameter int TRP     = 14,   // ILLUSTRATIVE
  parameter int TXSR    = 64,   // ILLUSTRATIVE self-refresh exit interval

  // COUNT, not INDEX. Each counter must REPRESENT the threshold it is
  // compared against, so it needs $clog2(threshold + 1) bits. TXSR is
  // the largest, and it is the one that would saturate first -- which
  // would make the exit interval's comparison unreachable and admit
  // an access before the device was ready.
  parameter int CNT_W   = $clog2((TXSR > TRP ? (TXSR > TRCD ? TXSR : TRCD)
                                             : (TRP  > TRCD ? TRP  : TRCD)) + 1),
  parameter int BANK_W  = $clog2(BANKS)
)(
  input  logic               clk,
  input  logic               rst_n,

  input  logic               req_valid,
  input  logic [BANK_W-1:0]  req_bank,

  // Shared dimension: the thirteen obligations of §2, reduced here to
  // the two counters this block needs. 13.3 owns the full taxonomy.
  input  logic               row_open_i,
  input  logic [CNT_W-1:0]   since_act_i,
  input  logic [CNT_W-1:0]   since_pre_i,

  // Low-power dimension. Driven only when the profile has one.
  input  logic [2:0]         dev_state,
  input  logic [CNT_W-1:0]   since_exit_i,

  output logic               admit,
  output logic               blocked_by_timing,
  output logic               blocked_by_state,
  output logic               exit_req,
  output logic [7:0]         obligation_count
);
  // Device power states. 24.2 §1 owns the point that the state set is
  // the DEVICE's and not a textbook's; these five are the shape the
  // admission test needs and the encoding is local to this block.
  localparam logic [2:0] ST_ACTIVE   = 3'd0;
  localparam logic [2:0] ST_IDLE     = 3'd1;
  localparam logic [2:0] ST_PWRDOWN  = 3'd2;
  localparam logic [2:0] ST_SELFREF  = 3'd3;
  localparam logic [2:0] ST_EXITING  = 3'd4;

  initial begin
    if (BANKS < 1) $fatal(1, "access_admission: BANKS must be >= 1");
    if (TRCD < 1 || TRP < 1) $fatal(1, "access_admission: timing must be >= 1");
    if (PROFILE_LOW_POWER && TXSR < 1)
      $fatal(1, "access_admission: low-power profile needs TXSR >= 1");
  end

  // ---- Dimension one: TIMING. Becomes true by WAITING. Identical in
  //      both profiles, because §2 counted thirteen for thirteen.
  logic timing_ok;
  always_comb begin
    if (row_open_i) timing_ok = (since_act_i >= TRCD[CNT_W-1:0]);
    else            timing_ok = (since_pre_i >= TRP[CNT_W-1:0]);
  end

  generate
  if (PROFILE_LOW_POWER) begin : g_low_power

    // ---- Dimension two: STATE. Becomes true only by ACTING. ---------
    logic state_ok;
    always_comb begin
      unique case (dev_state)
        ST_ACTIVE, ST_IDLE : state_ok = 1'b1;
        // 6.2's command-qualification contract: in a gated state the
        // device does not accept commands at all. No counter is
        // blocking this, which is §8's whole point.
        ST_PWRDOWN, ST_SELFREF : state_ok = 1'b0;
        // Exiting: the interval must elapse. This is the ONE part of
        // the state dimension that does become true by waiting, and
        // it is why the state machine needs a distinct EXITING state
        // rather than going straight to ACTIVE.
        ST_EXITING : state_ok = (since_exit_i >= TXSR[CNT_W-1:0]);
        default    : state_ok = 1'b0;   // unknown state admits nothing
      endcase
    end

    // The ACTION the state dimension requires. A scheduler that only
    // waits will wait forever (§8), so the request to leave is an
    // OUTPUT of the admission test rather than somebody else's job.
    assign exit_req = req_valid
                   && (dev_state == ST_PWRDOWN || dev_state == ST_SELFREF);

    assign admit             = req_valid && timing_ok && state_ok;
    // Reported SEPARATELY and never merged. 30.5 §3: an empty result
    // from a combined block is a loop that found nothing; a labelled
    // block is a reportable fact with an attributable cause.
    assign blocked_by_timing = req_valid && !timing_ok;
    assign blocked_by_state  = req_valid && timing_ok && !state_ok;
    assign obligation_count  = 8'd22;   // §7's count

  end else begin : g_sustained

    // No state dimension. Legality is one-dimensional, and that is
    // the ONLY difference this parameter makes -- §1.
    assign exit_req          = 1'b0;
    assign admit             = req_valid && timing_ok;
    assign blocked_by_timing = req_valid && !timing_ok;
    assign blocked_by_state  = 1'b0;
    assign obligation_count  = 8'd13;   // §2's count

  end
  endgenerate
endmodule

// ---------------------------------------------------------------------
// lp_wake_path -- INTENTIONALLY DEFECTIVE, for review (§11).
//
// CLASSIFICATION: synthesisable, ILLUSTRATIVE, and CONTAINS A BUG.
//
// WHAT IT IS MEANT TO DO: the five-clause contract above -- carry the
// refresh obligation across a self-refresh handover in both
// directions, so that the controller resumes with a correct debt.
//
// WHY IT EXISTS HERE: §5 establishes that the deciding quantity is
// energy under the duty cycle, and §7 that "who owns refresh right
// now" is one of the obligations the low-power profile adds. This
// block is what happens when that ownership is tracked for the
// PURPOSE of clause 3 and forgotten for the purpose of clause 2.
//
// HOW TO RUN IT: enter self refresh, remain there for many refresh
// intervals, exit, and watch `debt`.
// EXPECTED RESULT under clause 4: debt on exit equals debt at entry.
// EXPECTED TRACE: `debt` must be STABLE for the whole residency.
//
// SYNTHESIS: one ownership flag, one debt counter, one exit timer.
// LIMITATIONS: this block carries the LEDGER across the handover. It
// does not implement the accrual rule itself -- 15.3 owns the credit
// ledger with its verified postponement and pull-in allowance, and
// this block consumes `interval_tick` from it rather than
// reimplementing the accounting (17.3 §7's one-writer rule). Nor does
// it decide WHEN to enter the state: 24.2 §6 owns that selector.
// ---------------------------------------------------------------------
module lp_wake_path #(
  parameter int TXSR    = 64,      // ILLUSTRATIVE exit interval
  // COUNT, not INDEX: the debt counter must represent the largest
  // debt the verified allowance permits (15.3), and saturating it
  // understates the obligation -- which is the WRONG direction for a
  // correctness obligation, because an understated debt is a refresh
  // that never happens.
  parameter int DEBT_W  = 8,
  parameter int TMR_W   = $clog2(TXSR + 1)
)(
  input  logic               clk,
  input  logic               rst_n,

  input  logic               sre_commit,    // self-refresh entry committed
  input  logic               srx_commit,    // exit committed
  input  logic               interval_tick, // from 15.3's ledger
  input  logic               ref_issued,    // a REF command committed

  output logic               dev_owns_refresh,
  output logic [DEBT_W-1:0]  debt,
  output logic               wake_busy,
  output logic               ctrl_may_refresh
);
  logic [TMR_W-1:0] exit_tmr;

  // Clause 3 is honoured: the controller is forbidden to refresh while
  // the device owns the obligation. This line is CORRECT, and it is
  // the reason the defect is hard to see -- ownership IS tracked, and
  // it IS used.
  assign ctrl_may_refresh = !dev_owns_refresh && !wake_busy;

  always_ff @(posedge clk) begin
    if (!rst_n) begin
      dev_owns_refresh <= 1'b0;      // clause 5
      debt             <= '0;
      wake_busy        <= 1'b0;
      exit_tmr         <= '0;
    end else begin
      // ---- Ownership transfer, both directions. Clauses 1 and 4's
      //      ownership half are correct.
      if (sre_commit) begin
        dev_owns_refresh <= 1'b1;
      end
      if (srx_commit) begin
        dev_owns_refresh <= 1'b0;
        wake_busy        <= 1'b1;
        exit_tmr         <= '0;
      end

      // ---- The exit interval.
      if (wake_busy) begin
        if (exit_tmr >= TXSR[TMR_W-1:0]) wake_busy <= 1'b0;
        else                             exit_tmr  <= exit_tmr + 1'b1;
      end

      // ---- Accrual and discharge.
      if (interval_tick && debt != {DEBT_W{1'b1}})
        debt <= debt + 1'b1;                      // <-- THE DEFECT
      else if (ref_issued && debt != '0)
        debt <= debt - 1'b1;
    end
  end
endmodule

   ILLUSTRATIVE, and the units are refresh intervals rather than any
   published figure -- 15.3 owns tREFI and this block quotes none.

   suppose the device is in self refresh for 4,000 refresh intervals
   (a phone in a pocket; 24.1 §3's 2% duty cycle produces residencies
   of this order routinely).

   contract, clause 2 and 4:
       debt at entry  = 0
       debt during    = 0, STABLE for 4,000 intervals
       debt at exit   = 0
       refreshes owed on wake = 0     -- the device did them all

   this block:
       debt at entry  = 0
       debt during    = 1, 2, 3, ... saturating at 255 (DEBT_W = 8)
       debt at exit   = 255
       refreshes owed on wake = 255

   so on wake the refresh manager:
     1. drains all banks (17.3's DRAIN phase),
     2. issues 255 REF commands the device did not need,
     3. holds the gate closed for the whole occupancy window,
     4. and only then serves the access that caused the wake.

      // CORRECTED. Clause 2: while the device owns the obligation,
      // nothing is accruing for the controller to discharge. The
      // gate is `dev_owns_refresh`, the same flag clause 3 already
      // consumed -- so the fix adds no state, and the bug was never
      // a missing signal. It was a signal used for one of its two
      // obligations.
      //
      // `wake_busy` is included because the exit interval is still
      // the device's: 24.2 §4's handover completes when the exit
      // interval elapses, not when SRX commits.
      if (interval_tick && !dev_owns_refresh && !wake_busy
          && debt != {DEBT_W{1'b1}})
        debt <= debt + 1'b1;
      else if (ref_issued && debt != '0)
        debt <= debt - 1'b1;

// ---------------------------------------------------------------------
// duty_cycle_crossover -- verification/telemetry, CORRECT as written.
//
// CLASSIFICATION: synthesisable telemetry. Drives nothing.
// ILLUSTRATIVE parameter values, ABSTRACT energy units.
//
// WHAT IT DOES: measures the observed duty cycle and the observed
// idle-duration distribution, and reports which side of §5's
// crossover the system is actually on.
//
// WHY IT EXISTS HERE: §6 shows that the market-segment labels are
// proxies which fail at the edges, and §5 shows the crossover is
// sensitive -- a fourfold change in the idle advantage moved it from
// 14% to 67%. An argument that sensitive must be measured on the
// real system, not assumed from the segment.
//
// ENERGY UNITS ARE ABSTRACT, and deliberately. 24.2 §5 is explicit
// that an exit ENERGY cannot be computed from a published exit
// LATENCY and a steady-state CURRENT without knowing the voltage and
// the activity during exit. So D_PI and D_PA are INPUTS supplied by
// whoever characterised the parts, exactly as 24.2 §7's selector
// takes s and e abstractly. Inventing them would be the error this
// module refuses.
//
// HOW TO RUN IT: run the real workload, read `below_crossover` and
// `short_idle_frac` at the end of the window.
// EXPECTED RESULT: a phone-like workload reports below_crossover
// high; a sustained workload reports it low.
//
// SYNTHESIS: three counters, one comparator, one multiply-free
// cross-multiplication. No divider.
//
// LIMITATIONS: reports the ENERGY side of the decision only. §6's
// qualification stands -- availability, capacity per channel, form
// factor and replaceability (axis A7) constrain the choice
// independently, and this block measures none of them.
// ---------------------------------------------------------------------
module duty_cycle_crossover #(
  parameter int WIN     = 1048576,  // accounting window, cycles
  // Abstract energy-rate differences, supplied by characterisation.
  // D_PI = idle advantage of the low-power profile   (>= 0)
  // D_PA = active penalty of the low-power profile   (may be 0)
  parameter int D_PI    = 4,        // ILLUSTRATIVE, abstract units
  parameter int D_PA    = 6,        // ILLUSTRATIVE, abstract units
  // The idle duration below which a deep state cannot pay --
  // 24.2 §5's d* = e/s, supplied rather than computed here.
  parameter int D_STAR  = 512,      // ILLUSTRATIVE, cycles
  // COUNT, not INDEX: every counter below must REPRESENT WIN, so it
  // needs $clog2(WIN + 1) bits. Sized $clog2(WIN) the active counter
  // saturates one short of a fully active window, understating the
  // duty cycle -- the instrument failing in the direction that makes
  // the low-power profile look better than it is.
  parameter int CNT_W   = $clog2(WIN + 1)
)(
  input  logic              clk,
  input  logic              rst_n,

  input  logic              mem_active,   // the memory moved data this cycle
  input  logic              idle_begin,   // an idle interval started
  input  logic              idle_end,     // and ended
  input  logic              win_tick,     // end of the accounting window

  output logic [CNT_W-1:0]  r_active,
  output logic [CNT_W-1:0]  r_idle_events,
  output logic [CNT_W-1:0]  r_short_idles,
  output logic              below_crossover,
  output logic              result_valid
);
  initial begin
    if (WIN  < 2) $fatal(1, "duty_cycle_crossover: WIN must be >= 2");
    if (D_PI < 0 || D_PA < 0)
      $fatal(1, "duty_cycle_crossover: energy differences must be >= 0");
    // §5's degenerate case, made explicit rather than silently
    // dividing by zero: with no idle advantage and no active penalty
    // the crossover is undefined and the comparison is not an energy
    // question at all.
    if (D_PI == 0 && D_PA == 0)
      $fatal(1, "duty_cycle_crossover: D_PI and D_PA both zero -- no crossover exists");
    if (D_STAR < 1) $fatal(1, "duty_cycle_crossover: D_STAR must be >= 1");
  end

  logic [CNT_W-1:0] c_active, c_events, c_short, idle_len;
  logic             in_idle;

  always_ff @(posedge clk) begin
    if (!rst_n) begin
      c_active <= '0;  c_events <= '0;  c_short <= '0;
      idle_len <= '0;  in_idle  <= 1'b0;
      r_active <= '0;  r_idle_events <= '0;  r_short_idles <= '0;
      below_crossover <= 1'b0;  result_valid <= 1'b0;
    end else if (win_tick) begin
      r_active      <= c_active;
      r_idle_events <= c_events;
      r_short_idles <= c_short;
      result_valid  <= 1'b1;

      // §5's test, cross-multiplied so no divider is needed and no
      // fixed-point rounding can move the verdict:
      //
      //     low-power ahead  iff  (1 - D) * D_PI  >  D * D_PA
      //     with D = c_active / WIN, multiply through by WIN:
      //         (WIN - c_active) * D_PI  >  c_active * D_PA
      //
      // DERIVED, and the cross-multiplied form is exact.
      below_crossover <= ((WIN - c_active) * D_PI) > (c_active * D_PA);

      c_active <= '0;  c_events <= '0;  c_short <= '0;
    end else begin
      result_valid <= 1'b0;
      if (mem_active && c_active != {CNT_W{1'b1}}) c_active <= c_active + 1'b1;

      // Idle-duration distribution. §5's closing result: a duty cycle
      // alone is UNDER-SPECIFIED, because the same 2% active fraction
      // reached as one long idle and as ten thousand short ones gives
      // completely different effective idle power. So count the idles
      // that are too short for a deep state to pay (24.2 §5's d*).
      if (idle_begin) begin
        in_idle  <= 1'b1;
        idle_len <= '0;
        if (c_events != {CNT_W{1'b1}}) c_events <= c_events + 1'b1;
      end else if (in_idle) begin
        if (idle_end) begin
          in_idle <= 1'b0;
          if (idle_len < D_STAR[CNT_W-1:0] && c_short != {CNT_W{1'b1}})
            c_short <= c_short + 1'b1;
        end else if (idle_len != {CNT_W{1'b1}}) begin
          idle_len <= idle_len + 1'b1;
        end
      end
    end
  end

  // The fraction of idle intervals too short to pay. Reported as a
  // pair rather than a percentage, because 27.5's closure model and
  // 30.8 §11's range rule both say a derived single number invites a
  // sign-off it cannot support. A consumer that wants a percentage
  // divides the two and owns the rounding.
  //   short_idle_frac = r_short_idles / r_idle_events
endmodule

  // Offered as "proves the refresh handover is correct".
  // P1: clause 3. Correct, and it PASSES on the defective block.
  property p_no_ctrl_refresh_while_device_owns;
    @(posedge clk) disable iff (!rst_n)
      dev_owns_refresh |-> !ctrl_may_refresh;
  endproperty
  assert property (p_no_ctrl_refresh_while_device_owns)
    else $error("controller permitted a refresh while the device owned it");

  // P2: clauses 1 and 5, the ownership transitions. Also correct,
  // also passes.
  property p_ownership_transfers_on_commit;
    @(posedge clk) disable iff (!rst_n)
      sre_commit |=> dev_owns_refresh;
  endproperty
  assert property (p_ownership_transfers_on_commit)
    else $error("ownership did not transfer on self-refresh entry");

  // Clause 2. It names `debt`, so it cannot pass while `debt` moves.
  // $stable is the right operator: the claim is not that debt is
  // zero -- it may be non-zero at entry, and clause 4 requires that
  // value to survive -- but that it does not CHANGE.
  property p_debt_stable_while_device_owns;
    @(posedge clk) disable iff (!rst_n)
      dev_owns_refresh |-> $stable(debt);
  endproperty
  assert property (p_debt_stable_while_device_owns)
    else $error("refresh debt accrued while the device owned the obligation");

  // Clause 4, stated as the end-to-end obligation rather than as a
  // per-cycle one. The debt on exit must equal the debt at entry,
  // which is a claim about a PAIR of events and needs the value
  // sampled at the first.
  property p_debt_survives_the_handover;
    logic [DEBT_W-1:0] entry_debt;
    @(posedge clk) disable iff (!rst_n)
      (sre_commit, entry_debt = debt) |-> (!srx_commit throughout
        (##[1:$] (srx_commit && debt == entry_debt)));
  endproperty
  assert property (p_debt_survives_the_handover)
    else $error("debt on exit differs from debt at entry");

  // The exit interval, which clause 4's correction also gates on --
  // 24.2 §4's handover is not complete until the interval elapses.
  property p_no_accrual_during_wake;
    @(posedge clk) disable iff (!rst_n)
      wake_busy |-> $stable(debt) || ref_issued;
  endproperty
  assert property (p_no_accrual_during_wake)
    else $error("debt accrued during the exit interval");

  // Saturation must never be reached, because a saturated debt
  // UNDERSTATES a correctness obligation -- a refresh that never
  // happens. 30.8 §11's range rule, applied where the direction of
  // the error matters.
  property p_debt_never_saturates;
    @(posedge clk) disable iff (!rst_n)
      debt != {DEBT_W{1'b1}};
  endproperty
  assert property (p_debt_never_saturates)
    else $error("refresh debt saturated: the obligation is now understated");

  // §8's deadlock signature, asserted as a liveness BOUND rather
  // than as unbounded eventuality -- 30.9 §5 Q2, and MAX_WAKE is
  // justified from TXSR plus the drain rather than chosen.
  property p_state_block_resolves;
    @(posedge clk) disable iff (!rst_n)
      blocked_by_state |-> ##[1:MAX_WAKE] (admit || !req_valid);
  endproperty
  assert property (p_state_block_resolves)
    else $error("a state-blocked access did not resolve within the bound");

  // ---- Covers. And this is where §12's refinement bites.
  // The EVENT cover. Non-zero in any bring-up test that enters self
  // refresh at all -- so it proves the antecedent occurred and says
  // NOTHING about whether the defect was observable.
  cover property (@(posedge clk) disable iff (!rst_n) dev_owns_refresh);

  // The DURATION cover. This is the one that finds §11's defect, and
  // it is the instrument §12's refinement demands: for a defect whose
  // magnitude is proportional to a residency, the coverage item must
  // be on the RESIDENCY. LONG_RESIDENCY is chosen so that a correct
  // design's debt would be unchanged and a defective one's would have
  // saturated -- i.e. above 2**DEBT_W intervals.
  cover property (@(posedge clk) disable iff (!rst_n)
                  dev_owns_refresh [*LONG_RESIDENCY]);

  // The handover in both directions, separately, because entry and
  // exit have different bugs.
  cover property (@(posedge clk) disable iff (!rst_n) sre_commit);
  cover property (@(posedge clk) disable iff (!rst_n) srx_commit);

  // A non-zero debt at entry, which is the case clause 4 is actually
  // about. With debt zero at entry, p_debt_survives_the_handover
  // holds trivially on the defective block's saturation as well.
  cover property (@(posedge clk) disable iff (!rst_n)
                  sre_commit && debt != '0);

  // §8's signature, covered so that the deadlock case is known to
  // have been reached rather than merely guarded.
  cover property (@(posedge clk) disable iff (!rst_n)
                  blocked_by_state && !blocked_by_timing);

  // The two dimensions must be MUTUALLY EXCLUSIVE as reported, or
  // §8's signature is unreadable. This is the property that makes
  // the two outputs worth having: if both can be high at once, a
  // report of "blocked by state" no longer means "no rule blocks it".
  property p_block_reasons_are_exclusive;
    @(posedge clk) disable iff (!rst_n)
      $onehot0({blocked_by_timing, blocked_by_state});
  endproperty
  assert property (p_block_reasons_are_exclusive)
    else $error("both block reasons asserted: the signature is ambiguous");

  // Admission and blocking must partition the request. An access is
  // admitted, or blocked for exactly one stated reason -- never
  // neither, which would be an unreported stall.
  property p_request_is_accounted;
    @(posedge clk) disable iff (!rst_n)
      req_valid |-> (admit ^ (blocked_by_timing || blocked_by_state));
  endproperty
  assert property (p_request_is_accounted)
    else $error("a request was neither admitted nor attributed to a cause");

  // The CONTRACT invariant, with the parameter in the ANTECEDENT and
  // not in the claim -- 31.1 §14's test for whether a property may be
  // shared across configurations. It may.
  property p_sustained_never_blocks_on_state;
    @(posedge clk) disable iff (!rst_n)
      (!PROFILE_LOW_POWER) -> (!blocked_by_state && !exit_req);
  endproperty
  assert property (p_sustained_never_blocks_on_state)
    else $error("the sustained profile reported a state block");

  // §8's action requirement: a state block must REQUEST an exit.
  // Waiting cannot clear it, so a block that does not ask is a
  // deadlock by construction.
  property p_state_block_requests_exit;
    @(posedge clk) disable iff (!rst_n)
      blocked_by_state |-> exit_req;
  endproperty
  assert property (p_state_block_requests_exit)
    else $error("state-blocked without requesting an exit: deadlock");

  // The unknown-state case admits nothing. 7.4's three-valued
  // discipline, at the power-state layer rather than the bank layer.
  property p_unknown_state_admits_nothing;
    @(posedge clk) disable iff (!rst_n)
      (PROFILE_LOW_POWER && !(dev_state inside
        {ST_ACTIVE, ST_IDLE, ST_PWRDOWN, ST_SELFREF, ST_EXITING}))
      |-> !admit;
  endproperty
  assert property (p_unknown_state_admits_nothing)
    else $error("an access was admitted with an unrecognised device state");

  // The configuration covers, per 31.1 §14: a parameterised
  // comparison needs a coverage item per configuration, and the
  // regression must be shown to have entered both arms.
  cover property (@(posedge clk) disable iff (!rst_n)
                  obligation_count == 8'd22);   // low-power arm
  cover property (@(posedge clk) disable iff (!rst_n)
                  obligation_count == 8'd13);   // sustained arm