Low-Power Features

   entering is worth it   when   s x d  >  e
   the break-even duration is    d*  =  e / s

   3d - 2  =  10d - 16
       14  =  7d
        d  =  2          the crossover, exactly

// ---------------------------------------------------------------------
// lp_state_selector -- given a predicted idle duration and the cost
// and saving of two states, choose between them, or neither.
//
// CLASSIFICATION: educational, synthesisable.
//
// ALL UNITS ARE ABSTRACT. No energy, no current, no voltage, no real
// exit latency. §5's callout: datasheets publish exit LATENCY and
// steady-state CURRENT, which cannot be combined into an energy
// without information they do not give.
//
// WHAT IT DOES NOT MODEL:
//   - the prediction. d_pred is an INPUT. §4: the idle duration is a
//     system property the memory cannot know, and guessing it here
//     would invent the hardest part of the problem.
//   - legality. §10's machine owns whether the transition is even
//     permitted, and this block can recommend a state the machine
//     will refuse. That separation is deliberate.
//   - what actually happens if the prediction is wrong, beyond
//     reporting the regret (§13's oscillation case).
//
// NO DIVISION. The break-even comparison is done by cross-multiplying
// (s x d vs e), the same no-divide discipline as 24.1 §10.
// ---------------------------------------------------------------------
module lp_state_selector #(
  parameter int RATE_W = 12,        // saving per tick
  parameter int COST_W = 16,        // cost to leave the state
  parameter int DUR_W  = 16,        // predicted idle duration, ticks
  parameter int NET_W  = RATE_W + DUR_W + 2   // signed headroom
) (
  input  logic                    clk,
  input  logic                    rst_n,

  input  logic                    eval,
  input  logic [DUR_W-1:0]        d_pred,

  // Shallow state (power down) and deep state (self refresh).
  input  logic [RATE_W-1:0]       s_shallow,
  input  logic [COST_W-1:0]       e_shallow,
  input  logic [RATE_W-1:0]       s_deep,
  input  logic [COST_W-1:0]       e_deep,

  // ── Verdict. Three outcomes, not two -- "neither" is a real answer
  //    and §6's d=1 row is why.
  output logic                    pick_shallow,
  output logic                    pick_deep,
  output logic                    pick_none,

  // Net savings, SIGNED, so a state that loses reports a negative
  // figure rather than a clamped zero. §6: at d=1 the deep state
  // spends 6 units to save nothing, and that must be visible.
  output logic signed [NET_W-1:0] net_shallow,
  output logic signed [NET_W-1:0] net_deep,
  output logic signed [NET_W-1:0] net_chosen,

  // The regret of the choice not taken -- always >= 0 by construction.
  output logic signed [NET_W-1:0] regret,

  // §6's second reading: a state can be past its own break-even and
  // still be the worse of the two. Reported separately because a
  // policy that conflates them picks wrongly in that window.
  output logic                    deep_past_own_breakeven,
  output logic                    deep_beats_shallow,

  output logic                    err_deep_cheaper_to_exit,
  output logic                    err_no_saving_either_state
);

  initial begin
    if (NET_W <= RATE_W + DUR_W)
      $fatal(1, "lp_state_selector: NET_W needs sign and carry headroom");
    if (COST_W > NET_W - 1)
      $fatal(1, "lp_state_selector: COST_W exceeds signed net range");
  end

  logic signed [NET_W-1:0] n_sh, n_dp;
  logic                    v_sh, v_dp, v_no, bad_cost, bad_zero;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      n_sh <= '0; n_dp <= '0;
      v_sh <= 1'b0; v_dp <= 1'b0; v_no <= 1'b1;
      bad_cost <= 1'b0; bad_zero <= 1'b0;
    end else if (eval) begin
      begin : decide
        logic signed [NET_W-1:0] a, b;
        // s x d - e, by multiplication only. Zero-extend the unsigned
        // operands into the signed width before the subtract, so the
        // result can legitimately go negative.
        a = NET_W'($signed({1'b0, s_shallow}) * $signed({1'b0, d_pred}))
            - NET_W'($signed({1'b0, e_shallow}));
        b = NET_W'($signed({1'b0, s_deep})    * $signed({1'b0, d_pred}))
            - NET_W'($signed({1'b0, e_deep}));
        n_sh <= a;
        n_dp <= b;

        // Three-way. A state is only picked if its net saving is
        // POSITIVE -- "neither" wins when both lose.
        if ((a <= 0) && (b <= 0)) begin
          v_sh <= 1'b0; v_dp <= 1'b0; v_no <= 1'b1;
        end else if (b > a) begin
          v_sh <= 1'b0; v_dp <= 1'b1; v_no <= 1'b0;
        end else begin
          // Ties go to the SHALLOW state. At the crossover both save
          // the same, and the shallow state carries less risk if the
          // prediction was optimistic -- §5's asymmetry.
          v_sh <= 1'b1; v_dp <= 1'b0; v_no <= 1'b0;
        end

        bad_zero <= (a <= 0) && (b <= 0);
      end

      // §5's trade, checked at runtime rather than at elaboration
      // because here the costs are inputs rather than parameters.
      bad_cost <= (e_deep <= e_shallow);
    end
  end

  assign pick_shallow = v_sh;
  assign pick_deep    = v_dp;
  assign pick_none    = v_no;
  assign net_shallow  = n_sh;
  assign net_deep     = n_dp;
  assign net_chosen   = v_dp ? n_dp : (v_sh ? n_sh : '0);
  // Regret of the alternative. Zero when nothing was entered, since
  // there was nothing better to have done.
  assign regret = v_dp ? ((n_dp > n_sh) ? (n_dp - n_sh) : '0)
                : v_sh ? ((n_sh > n_dp) ? (n_sh - n_dp) : '0)
                : '0;
  assign deep_past_own_breakeven = (n_dp > 0);
  assign deep_beats_shallow      = (n_dp > n_sh);
  assign err_deep_cheaper_to_exit  = bad_cost;
  assign err_no_saving_either_state = bad_zero;
endmodule

// ---------------------------------------------------------------------
// lp_state_machine -- the LPDDR interface state set read from a named
// device's own bus-interface state diagram, with the illegal
// transitions of §3 explicitly forbidden.
//
// CLASSIFICATION: educational, synthesisable.
//
// RELATION TO 4.7 §7: that chapter's dram_power_state_ctrl owns the
// POLICY question -- is entering a deeper state worth its exit cost.
// This block owns the LEGALITY question -- is the transition even
// permitted. Both are needed and they are different.
//
// WHAT IT DOES NOT MODEL:
//   - the device, any timing parameter (tRFCpb/tRFCab/exit latency),
//     any current or energy, the array, or refresh itself
//   - the POLICY of when to enter a state (4.7 §7; §5's break-even)
//   - what the device actually does if an illegal command arrives,
//     which is not defined to be a clean rejection (§3's callout)
//
// THE STATE SET IS THE DEVICE'S. It is not a generic hierarchy, and
// the two power-down states are separate because their obligations
// differ (§1).
// ---------------------------------------------------------------------
module lp_state_machine #(
  // Exit latency per deep state, in abstract ticks. Published by
  // datasheets as a LATENCY (not an energy), so that is what this
  // takes -- §5's callout on why no energy figure is invented.
  parameter int EXIT_PD = 2,
  parameter int EXIT_SR = 16,
  parameter int LAT_W   = (EXIT_SR <= 1) ? 1 : $clog2(EXIT_SR + 1),
  parameter int CNT_W   = 20
) (
  input  logic              clk,
  input  logic              rst_n,

  // ── Device reset, which the diagram makes a state rather than an
  //    input condition.
  input  logic              dev_reset_n,

  // ── The commands and signals that drive transitions.
  input  logic              cke,            // low requests power down
  input  logic              cmd_act,
  input  logic              cmd_pre,
  input  logic              cmd_ref,
  input  logic              ref_all_bank,   // scope of cmd_ref (§2)
  input  logic              cmd_sre,        // enter self refresh
  input  logic              cmd_srx,        // exit self refresh
  input  logic              cmd_rdwr,
  // Set while any bank holds an open row. §3: this is what makes
  // refresh and self refresh illegal.
  input  logic              any_bank_open,
  // Timing completions, supplied by whoever owns the parameters.
  input  logic              rfc_pb_done,
  input  logic              rfc_ab_done,

  // ── State, as the device names it.
  output logic [3:0]        state,
  output logic              in_low_power,
  output logic              refresh_obligation_is_ours,

  // ── Exit accounting. §5: a deeper state costs more to leave.
  output logic [LAT_W-1:0]  exit_countdown,
  output logic              exiting,
  output logic [CNT_W-1:0]  cy_in_pd,
  output logic [CNT_W-1:0]  cy_in_sr,
  output logic [CNT_W-1:0]  cnt_entries_pd,
  output logic [CNT_W-1:0]  cnt_entries_sr,

  // ── §3's forbidden set, each reported separately so a debug session
  //    learns WHICH rule was broken rather than that one was.
  output logic              err_refresh_with_bank_open,
  output logic              err_sre_with_bank_open,
  output logic              err_cmd_during_power_down,
  output logic              err_cmd_during_self_refresh,
  output logic              err_srx_without_sre,
  output logic              any_illegal
);

  localparam logic [3:0] S_RESET   = 4'd0;
  localparam logic [3:0] S_IDLE    = 4'd1;
  localparam logic [3:0] S_IDLE_PD = 4'd2;
  localparam logic [3:0] S_ACTING  = 4'd3;
  localparam logic [3:0] S_ACTIVE  = 4'd4;
  localparam logic [3:0] S_ACT_PD  = 4'd5;
  localparam logic [3:0] S_PRE     = 4'd6;
  localparam logic [3:0] S_REF_PB  = 4'd7;
  localparam logic [3:0] S_REF_AB  = 4'd8;
  localparam logic [3:0] S_SREF    = 4'd9;
  localparam logic [3:0] S_SR_PD   = 4'd10;

  initial begin
    if (EXIT_PD < 1 || EXIT_SR < 1)
      $fatal(1, "lp_state_machine: exit latencies must be at least 1");
    if (EXIT_SR <= EXIT_PD)
      // §5: a deeper state costs MORE to leave. A parameterisation
      // claiming otherwise inverts the trade the machine exists to
      // represent, and every conclusion drawn from it would be wrong.
      $fatal(1, "lp_state_machine: EXIT_SR (%0d) must exceed EXIT_PD (%0d)",
             EXIT_SR, EXIT_PD);
  end

  logic [3:0]       st;
  logic [LAT_W-1:0] exit_cnt;
  logic [CNT_W-1:0] pd_cy, sr_cy, pd_n, sr_n;
  logic             e_ref_open, e_sre_open, e_cmd_pd, e_cmd_sr, e_srx;

  // Any command at all, for the "commands are not accepted here"
  // checks. Declared above the assigns that read it.
  logic any_cmd;
  assign any_cmd = cmd_act | cmd_pre | cmd_ref | cmd_sre | cmd_rdwr;

  logic is_pd, is_sr;
  assign is_pd = (st == S_IDLE_PD) || (st == S_ACT_PD);
  assign is_sr = (st == S_SREF)    || (st == S_SR_PD);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      st <= S_RESET; exit_cnt <= '0;
      pd_cy <= '0; sr_cy <= '0; pd_n <= '0; sr_n <= '0;
      e_ref_open <= 1'b0; e_sre_open <= 1'b0;
      e_cmd_pd <= 1'b0; e_cmd_sr <= 1'b0; e_srx <= 1'b0;
    end else begin
      e_ref_open <= 1'b0; e_sre_open <= 1'b0;
      e_cmd_pd   <= 1'b0; e_cmd_sr   <= 1'b0; e_srx <= 1'b0;

      if (!dev_reset_n) begin
        st <= S_RESET;
      end else begin
        // ── Occupancy accounting, charged before any transition so a
        //    state's final tick is counted in that state.
        if (is_pd && (pd_cy != {CNT_W{1'b1}})) pd_cy <= pd_cy + CNT_W'(1);
        if (is_sr && (sr_cy != {CNT_W{1'b1}})) sr_cy <= sr_cy + CNT_W'(1);

        // ── Exit latency. A deep state is left over several ticks, and
        //    commands are not accepted during them.
        if (exit_cnt != '0) begin
          exit_cnt <= exit_cnt - LAT_W'(1);
        end else begin
          unique case (st)
            S_RESET : if (dev_reset_n) st <= S_IDLE;

            S_IDLE : begin
              // §3: refresh and self refresh require closed banks. The
              // check is on any_bank_open rather than on the state,
              // because a bank can be open while the interface state
              // is Idle in a multi-bank device.
              if (cmd_ref && any_bank_open)      e_ref_open <= 1'b1;
              else if (cmd_ref)                  st <= ref_all_bank ? S_REF_AB : S_REF_PB;
              else if (cmd_sre && any_bank_open) e_sre_open <= 1'b1;
              else if (cmd_sre) begin
                st <= S_SREF;
                if (sr_n != {CNT_W{1'b1}}) sr_n <= sr_n + CNT_W'(1);
              end
              else if (cmd_act)                  st <= S_ACTING;
              else if (!cke) begin
                st <= S_IDLE_PD;
                if (pd_n != {CNT_W{1'b1}}) pd_n <= pd_n + CNT_W'(1);
              end
              else if (cmd_srx)                  e_srx <= 1'b1;
            end

            S_ACTING : st <= S_ACTIVE;

            S_ACTIVE : begin
              // §3: refresh and self refresh from an active state are
              // illegal. Reported, and the state does NOT change --
              // pretending the transition happened would hide the bug.
              if (cmd_ref)      e_ref_open <= 1'b1;
              else if (cmd_sre) e_sre_open <= 1'b1;
              else if (cmd_pre) st <= S_PRE;
              else if (!cke) begin
                st <= S_ACT_PD;
                if (pd_n != {CNT_W{1'b1}}) pd_n <= pd_n + CNT_W'(1);
              end
            end

            S_PRE : st <= S_IDLE;

            // §3: a state is left the way it was entered. Raising CKE
            // starts an exit that takes EXIT_PD ticks, and commands
            // arriving during those ticks are not accepted.
            S_IDLE_PD : begin
              if (any_cmd) e_cmd_pd <= 1'b1;
              if (cke) begin st <= S_IDLE;   exit_cnt <= LAT_W'(EXIT_PD); end
            end
            S_ACT_PD : begin
              if (any_cmd) e_cmd_pd <= 1'b1;
              if (cke) begin st <= S_ACTIVE; exit_cnt <= LAT_W'(EXIT_PD); end
            end

            S_REF_PB : if (rfc_pb_done) st <= S_IDLE;
            S_REF_AB : if (rfc_ab_done) st <= S_IDLE;

            S_SREF : begin
              // Only SRX leaves self refresh, and it returns to IDLE
              // rather than to an active row (§3).
              if (any_cmd) e_cmd_sr <= 1'b1;
              if (cmd_srx) begin st <= S_IDLE; exit_cnt <= LAT_W'(EXIT_SR); end
              else if (!cke) st <= S_SR_PD;
            end
            S_SR_PD : begin
              if (any_cmd) e_cmd_sr <= 1'b1;
              if (cke)     st <= S_SREF;
            end

            default : st <= S_RESET;
          endcase
        end
      end
    end
  end

  assign state           = st;
  assign in_low_power    = is_pd || is_sr;
  // §4's third row: in power down the obligation is still the
  // controller's; in self refresh it is not.
  assign refresh_obligation_is_ours = !is_sr;
  assign exit_countdown  = exit_cnt;
  assign exiting         = (exit_cnt != '0);
  assign cy_in_pd        = pd_cy;
  assign cy_in_sr        = sr_cy;
  assign cnt_entries_pd  = pd_n;
  assign cnt_entries_sr  = sr_n;

  assign err_refresh_with_bank_open  = e_ref_open;
  assign err_sre_with_bank_open      = e_sre_open;
  assign err_cmd_during_power_down   = e_cmd_pd;
  assign err_cmd_during_self_refresh = e_cmd_sr;
  assign err_srx_without_sre         = e_srx;
  assign any_illegal = e_ref_open | e_sre_open | e_cmd_pd | e_cmd_sr | e_srx;
endmodule

// ---------------------------------------------------------------------
// pasr_segment_mask -- which array segments are maintained, and
// detection of accesses to ones that are not.
//
// CLASSIFICATION: educational, synthesisable.
//
// WHAT IT DOES NOT MODEL:
//   - retention time, temperature, or decay. It CANNOT say when an
//     abandoned segment's contents become wrong (§9: gradual and
//     unpredictable). A block predicting that would be inventing the
//     property that makes the mechanism dangerous.
//   - the software contract itself. 4.7 §4 owns the argument that
//     correctness here depends on the operating system keeping a
//     promise, and no hardware can verify it.
//
// WHAT IT ADDS: the device cannot refuse a bad mask (§9), so the
// CONTROLLER can at least NOTICE an access to an abandoned segment.
// That detection does not make the mechanism safe -- it makes a
// violation visible instead of silent, which is the difference
// between a diagnosable failure and arbitrary corruption.
// ---------------------------------------------------------------------
module pasr_segment_mask #(
  parameter int SEGMENTS = 8,
  parameter int ADDR_W   = 32,
  // Address bits that select the segment. The segment granularity is
  // COARSE (§9): one live byte in a segment requires the whole
  // segment, and this parameter is where that coarseness lives.
  parameter int SEG_LSB  = 26,
  parameter int SEG_W    = (SEGMENTS <= 1) ? 1 : $clog2(SEGMENTS),
  // A COUNT of segments up to SEGMENTS needs clog2(SEGMENTS+1).
  parameter int SEGC_W   = $clog2(SEGMENTS + 1),
  parameter int CNT_W    = 20
) (
  input  logic                clk,
  input  logic                rst_n,

  // ── Mask programming. Bit set = segment is MAINTAINED.
  input  logic                mask_write,
  input  logic [SEGMENTS-1:0] mask_in,

  // ── Accesses, for the detection of §12's header.
  input  logic                acc_valid,
  input  logic [ADDR_W-1:0]   acc_addr,

  // ── Whether the device is in a state where the mask applies. PASR
  //    governs SELF refresh; PAAR governs controller-issued refresh.
  //    Both are inputs because which exists is generation-specific
  //    (§9's table) and this block does not decide it.
  input  logic                in_self_refresh,
  input  logic                paar_enabled,

  // ── State.
  output logic [SEGMENTS-1:0] mask,
  output logic [SEGC_W-1:0]   n_maintained,
  output logic [SEGC_W-1:0]   n_abandoned,
  // Fraction maintained, as a PAIR. No division: the caller states
  // its denominator, as every accountant in this module does.
  output logic [SEGC_W-1:0]   maintained_num,
  output logic [SEGC_W-1:0]   maintained_den,

  // ── Detection. The whole point of the block.
  output logic                acc_to_abandoned,
  output logic [SEG_W-1:0]    abandoned_seg,
  output logic [CNT_W-1:0]    cnt_abandoned_acc,
  // Sticky: once an abandoned segment has been read, the data
  // returned from it is untrustworthy FOREVER after, because §9 says
  // decay is progressive rather than instantaneous.
  output logic                trust_lost,

  output logic                err_mask_all_zero,
  output logic                err_mask_changed_in_sr
);

  initial begin
    if (SEGMENTS < 2)
      $fatal(1, "pasr_segment_mask: SEGMENTS must be at least 2");
    if (SEG_LSB + SEG_W > ADDR_W)
      $fatal(1, "pasr_segment_mask: segment field exceeds ADDR_W");
  end

  logic [SEGMENTS-1:0] mask_q;
  logic [CNT_W-1:0]    n_bad;
  logic                lost, bad_zero, changed_sr, hit_bad;
  logic [SEG_W-1:0]    bad_seg;

  // Declared above the assigns that read it.
  logic [SEG_W-1:0] seg_of_acc;
  assign seg_of_acc = acc_addr[SEG_LSB +: SEG_W];

  logic [SEGC_W-1:0] n_keep;
  always_comb begin
    n_keep = '0;
    for (int s = 0; s < SEGMENTS; s++)
      if (mask_q[s]) n_keep = n_keep + SEGC_W'(1);
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      // SAFE STATE: everything maintained. A reset that abandoned
      // segments would lose data before software had said anything.
      mask_q     <= {SEGMENTS{1'b1}};
      n_bad      <= '0;
      lost       <= 1'b0;
      bad_zero   <= 1'b0;
      changed_sr <= 1'b0;
      hit_bad    <= 1'b0;
      bad_seg    <= '0;
    end else begin
      hit_bad    <= 1'b0;
      changed_sr <= 1'b0;

      if (mask_write) begin
        mask_q <= mask_in;
        // An all-zero mask maintains nothing. Legal to program and
        // never intended: it abandons the entire array.
        bad_zero <= (mask_in == '0);
        // Changing the mask while the device is self-refreshing means
        // segments change maintenance status mid-interval, so what was
        // retained is no longer knowable.
        if (in_self_refresh) changed_sr <= 1'b1;
      end

      if (acc_valid && !mask_q[seg_of_acc]) begin
        hit_bad <= 1'b1;
        bad_seg <= seg_of_acc;
        lost    <= 1'b1;            // sticky, per §12's header
        if (n_bad != {CNT_W{1'b1}}) n_bad <= n_bad + CNT_W'(1);
      end
    end
  end

  assign mask             = mask_q;
  assign n_maintained     = n_keep;
  assign n_abandoned      = SEGC_W'(SEGMENTS) - n_keep;
  assign maintained_num   = n_keep;
  assign maintained_den   = SEGC_W'(SEGMENTS);
  assign acc_to_abandoned = hit_bad;
  assign abandoned_seg    = bad_seg;
  assign cnt_abandoned_acc = n_bad;
  assign trust_lost       = lost;
  assign err_mask_all_zero = bad_zero;
  // Reported whenever the mask changes in self refresh, regardless of
  // whether PAAR is also enabled -- the hazard is the mid-interval
  // change, not which mechanism was active.
  assign err_mask_changed_in_sr = changed_sr;
endmodule

// Bind unit note: P1-P7 reference lp_state_machine's internal state
// and P8-P11 pasr_segment_mask's; both are written as though bound
// into their module, so clk and rst_n are visible directly.

// P1 -- FORBIDDEN TRANSITION. Refresh is never entered with a bank
// open. §3, and §15 names this property class the highest-value one
// in this module.
property p_no_refresh_with_bank_open;
  @(posedge clk) disable iff (!rst_n)
    (any_bank_open && cmd_ref) |=> ((state != 4'd7) && (state != 4'd8));
endproperty
assert property (p_no_refresh_with_bank_open);

// P2 -- FORBIDDEN TRANSITION. Self refresh is never entered from an
// active state or with a bank open.
property p_no_self_refresh_from_active;
  @(posedge clk) disable iff (!rst_n)
    ((state == 4'd4) && cmd_sre) |=> (state != 4'd9);
endproperty
assert property (p_no_self_refresh_from_active);

// P3 -- FORBIDDEN TRANSITION. Self refresh exits to Idle, never
// directly to an active row.
property p_srx_exits_to_idle;
  @(posedge clk) disable iff (!rst_n)
    ((state == 4'd9) && cmd_srx) |=> ((state == 4'd1) || (state == 4'd9));
endproperty
assert property (p_srx_exits_to_idle);

// P4 -- FORBIDDEN TRANSITION. A power-down state is never left
// directly into an activation; the exit is a step (§3).
property p_no_activate_from_power_down;
  @(posedge clk) disable iff (!rst_n)
    (((state == 4'd2) || (state == 4'd5)) && cmd_act) |=> (state != 4'd3);
endproperty
assert property (p_no_activate_from_power_down);

// P5 -- an illegal request is reported AND the state holds. Reporting
// without holding would let the model diverge from the device;
// holding without reporting would hide the controller's bug (§11).
property p_illegal_reported_and_held;
  @(posedge clk) disable iff (!rst_n)
    (err_refresh_with_bank_open || err_sre_with_bank_open)
      |-> (state == $past(state, 1));
endproperty
assert property (p_illegal_reported_and_held);

// P6 -- §4's third row, as an invariant. The refresh obligation is the
// controller's in every state except self refresh.
property p_obligation_matches_state;
  @(posedge clk) disable iff (!rst_n)
    refresh_obligation_is_ours == !((state == 4'd9) || (state == 4'd10));
endproperty
assert property (p_obligation_matches_state);

// P7 -- no command is accepted while an exit is in progress. §5: a
// deeper state is left over several ticks, and this is what makes the
// exit cost real rather than notional.
property p_no_transition_while_exiting;
  @(posedge clk) disable iff (!rst_n)
    exiting |=> (state == $past(state, 1));
endproperty
assert property (p_no_transition_while_exiting);

// P8 -- the maintained and abandoned counts partition the segments.
property p_segments_partition;
  @(posedge clk) disable iff (!rst_n)
    ((n_maintained + n_abandoned) == SEGC_W'(SEGMENTS));
endproperty
assert property (p_segments_partition);

// P9 -- an access to an unmaintained segment is always detected. The
// block's entire purpose: a violation must be visible rather than
// silent (§12's header).
property p_abandoned_access_detected;
  @(posedge clk) disable iff (!rst_n)
    (acc_valid && !mask[acc_addr[SEG_LSB +: SEG_W]]) |=> acc_to_abandoned;
endproperty
assert property (p_abandoned_access_detected);

// P10 -- trust, once lost, is never regained. §12: decay is
// progressive, so a plausible read proves nothing.
property p_trust_loss_is_sticky;
  @(posedge clk) disable iff (!rst_n)
    $past(trust_lost, 1) |-> trust_lost;
endproperty
assert property (p_trust_loss_is_sticky);

// P11 -- the mask comes out of reset maintaining everything. A reset
// that abandoned segments would lose data before software spoke.
property p_reset_maintains_all;
  @(posedge clk)
    $rose(rst_n) |-> (mask == {SEGMENTS{1'b1}});
endproperty
assert property (p_reset_maintains_all);

// P12 -- the three verdicts are mutually exclusive and one always
// holds. "Neither" is a real answer (§6's d=1 row), so the verdict is
// a genuine three-way partition rather than two flags.
property p_verdict_is_a_partition;
  @(posedge clk) disable iff (!rst_n)
    ($onehot({pick_shallow, pick_deep, pick_none}));
endproperty
assert property (p_verdict_is_a_partition);

// P13 -- a state is never entered at a loss. The whole point of §6:
// at short durations the deep state SPENDS to save nothing, and the
// selector must decline rather than pick the better loser.
property p_never_enter_at_a_loss;
  @(posedge clk) disable iff (!rst_n)
    (pick_shallow || pick_deep) |-> (net_chosen > 0);
endproperty
assert property (p_never_enter_at_a_loss);

// P14 -- the chosen state is the better of the two whenever either
// is worth entering. Rules out a selector that declines a profitable
// choice or takes the worse one.
property p_choice_is_maximal;
  @(posedge clk) disable iff (!rst_n)
    pick_deep    |-> (net_deep    >= net_shallow) and
    pick_shallow |-> (net_shallow >= net_deep);
endproperty
assert property (p_choice_is_maximal);

// P15 -- §6's second reading, as a property. Being past one's own
// break-even does NOT imply being the better choice, so the two
// outputs must be allowed to disagree -- and when they do, the
// shallow state is the one picked.
property p_breakeven_does_not_imply_better;
  @(posedge clk) disable iff (!rst_n)
    (deep_past_own_breakeven && !deep_beats_shallow) |-> !pick_deep;
endproperty
assert property (p_breakeven_does_not_imply_better);

// P16 -- regret is never negative. It measures the choice not taken,
// and a negative regret would mean the selector knew it chose badly.
property p_regret_non_negative;
  @(posedge clk) disable iff (!rst_n) (regret >= 0);
endproperty
assert property (p_regret_non_negative);

// ── Cover.
cover property (@(posedge clk) disable iff (!rst_n) state == 4'd9);   // self refresh
cover property (@(posedge clk) disable iff (!rst_n) state == 4'd10);  // SR power down
cover property (@(posedge clk) disable iff (!rst_n) state == 4'd2);   // idle PD
cover property (@(posedge clk) disable iff (!rst_n) state == 4'd5);   // active PD
// Both refresh scopes exercised -- §2's distinction.
cover property (@(posedge clk) disable iff (!rst_n) state == 4'd7);
cover property (@(posedge clk) disable iff (!rst_n) state == 4'd8);
// Each forbidden transition ATTEMPTED. A suite that never attempts one
// has not tested the property that forbids it.
cover property (@(posedge clk) disable iff (!rst_n) err_refresh_with_bank_open);
cover property (@(posedge clk) disable iff (!rst_n) err_sre_with_bank_open);
cover property (@(posedge clk) disable iff (!rst_n) err_cmd_during_self_refresh);
// A partial mask actually in force, and an access to an abandoned
// segment actually detected.
cover property (@(posedge clk) disable iff (!rst_n)
                  (n_abandoned != '0) && (n_maintained != '0));
cover property (@(posedge clk) disable iff (!rst_n) acc_to_abandoned);
// All three selector verdicts reached. "None" is the one a suite is
// likeliest to miss, and §6's d=1 row is exactly when it happens.
cover property (@(posedge clk) disable iff (!rst_n) pick_shallow);
cover property (@(posedge clk) disable iff (!rst_n) pick_deep);
cover property (@(posedge clk) disable iff (!rst_n) pick_none);
// The window §6 names: past the deep state's own break-even and still
// the worse choice. A suite that never enters it has not tested P15.
cover property (@(posedge clk) disable iff (!rst_n)
                  deep_past_own_breakeven && !deep_beats_shallow);
// The deep state evaluated at an outright loss -- the negative net.
cover property (@(posedge clk) disable iff (!rst_n) net_deep < 0);

// Independent legality reference. Holds the permitted transitions as
// an explicit adjacency table read from the device's state diagram,
// rather than as a case statement -- a different representation, so
// agreement is evidence rather than a restatement.
// SIMULATION-ONLY.
class lp_legality_ref;
  // legal[from][to] = 1 if the diagram has that edge.
  bit legal [11][11];

  function void build();
    foreach (legal[i,j]) legal[i][j] = 0;
    legal[0][1]  = 1;                          // RESET  -> IDLE
    legal[1][2]  = 1; legal[1][3] = 1;         // IDLE   -> IDLE_PD, ACTING
    legal[1][7]  = 1; legal[1][8] = 1;         // IDLE   -> REF_PB, REF_AB
    legal[1][9]  = 1;                          // IDLE   -> SREF
    legal[3][4]  = 1;                          // ACTING -> ACTIVE
    legal[4][5]  = 1; legal[4][6] = 1;         // ACTIVE -> ACT_PD, PRE
    legal[6][1]  = 1;                          // PRE    -> IDLE
    legal[2][1]  = 1;                          // IDLE_PD-> IDLE
    legal[5][4]  = 1;                          // ACT_PD -> ACTIVE
    legal[7][1]  = 1; legal[8][1] = 1;         // REF_*  -> IDLE
    legal[9][1]  = 1; legal[9][10] = 1;        // SREF   -> IDLE, SR_PD
    legal[10][9] = 1;                          // SR_PD  -> SREF
  endfunction

  function bit permitted(int f, int t);
    return (f == t) || legal[f][t];
  endfunction
endclass

  THE LEGAL-ONLY TESTBENCH THAT PROVES NOTHING
    A suite that drives only permitted sequences.

    result: every assertion PASSES.
            P1  no refresh with bank open      PASS (never attempted)
            P2  no self refresh from active    PASS (never attempted)
            P3  srx exits to idle              PASS
            P4  no activate from power down    PASS (never attempted)
            coverage: err_refresh_with_bank_open  NEVER HIT
                      err_sre_with_bank_open      NEVER HIT
                      err_cmd_during_self_refresh NEVER HIT

    diagnosis : P1, P2 and P4 are VACUOUS. Their antecedents never
      became true, so they held trivially and constrained nothing.
      The design could permit every illegal transition and this suite
      would still be green.

    what makes it dangerous : the pass is not a weak signal, it is a
      MISLEADING one. Three properties reported success while
      verifying nothing, and the only evidence of the problem is in
      the coverage report rather than in the results.

    the fix : the three "forbidden transition attempted" covers of
      §13 are the guard. A suite that does not hit them has not
      exercised the property class §15 calls the most valuable here,
      and the covers turn that from a judgement into a measurement.