Recovery — Repairing and Changing a Link That Already Exists

SPEED0   "Transmit Electrical Idle Ordered Sets to notify the
          link partner that we are going idle"
 
SPEED1   "Determine to which speed to change"
 
SPEED2   "Wait for remote device to enter electrical idle and
          remain there for required minimum time"
 
SPEED3   "Request PHY change speed and wait for PHY to finish
          changing speed"

step               1     2     3     4     5     6     7     8     9    10
ltssm_recovery     0     1     1     1     1     1     1     1     0     0
rec_causes        --    04    04    04    04    04    04    04    04    04
traffic_enable     1     0     0     0     0     0     0     0     1     1
 
rx_lock            1     0     0     1     1     1     1     1     1     1
rec_qual_count     -     0     0     0     1     2     3     4     4     4
speed_change_req   0     0     0     0     0     0     0     0     0     0
 
cand_valid         0     0     0     0     0     0     0     1     1     0
commit_req         0     0     0     0     0     0     0     0     1     0
active_speed      G3    G3    G3    G3    G3    G3    G3    G3    G3    G3
active_width      x8    x8    x8    x8    x8    x8    x8    x8    x8    x8

step               1     2     3     4     5     6     7     8     9    10    11
ltssm_recovery     0     1     1     1     1     1     1     1     1     1     0
rec_causes        --    08    08    08    08    08    08    08    08    08    08
traffic_enable     1     0     0     0     0     0     0     0     0     0     1
 
eios_tx            0     1     1     0     0     0     0     0     0     0     0
partner_idle       0     0     0     1     1     1     1     1     1     1     0
rate_req_valid     0     0     0     0     1     1     0     0     0     0     0
rate_req_ready     0     0     0     0     0     1     0     0     0     0     0
rate_done          0     0     0     0     0     0     0     1     1     1     1
rate_ok            -     -     -     -     -     -     -     1     1     1     1
 
rx_lock            1     0     0     0     0     0     0     0     1     1     1
cand_speed        --    --    --    --    G4    G4    G4    G4    G4    G4    G4
cand_valid         0     0     0     0     0     0     0     0     0     1     1
commit_req         0     0     0     0     0     0     0     0     0     0     1
active_speed      G3    G3    G3    G3    G3    G3    G3    G3    G3    G3    G4

// SYNTHESIZABLE. Normalized Recovery cause capture.
// THAT CAUSES ARE A STICKY BITMASK rather than an enum follows the
// vendor's own l0_to_rec register (section 1). THE SPECIFIC BITS are this
// chapter's normalization -- exact triggers are generation- and
// implementation-dependent (section 8).
package recovery_pkg;
 
  typedef struct packed {
    logic retrain_req;      // software/management directed
    logic speed_req;        // directed speed change
    logic width_req;        // autonomous width change
    logic lock_loss;        // receiver lost lock / alignment
    logic phy_error;        // PHY error burst
    logic partner_ts;       // partner is directing entry via training sets
    logic replay_exhausted; // repeated replay failure (section 2)
  } rec_cause_t;
 
  localparam int CAUSE_W = $bits(rec_cause_t);
 
  function automatic bit needs_speed_change(input rec_cause_t c);
    return c.speed_req;
  endfunction
 
  // A cause set with NO bits is not a legal Recovery episode. Something
  // asked for this; if nothing did, the entry itself is the bug.
  function automatic bit cause_valid(input rec_cause_t c);
    return (|c);
  endfunction
 
endpackage

import recovery_pkg::*;
 
// SYNTHESIZABLE. Capture ALL causes present at Recovery entry, then freeze.
// THE CAUSE IS THE MOST VALUABLE DEBUG STATE THIS BLOCK OWNS (section 4).
// It must describe why THIS episode started, which means it cannot track
// live events -- section 20 measured what happens when it does.
module recovery_cause_latch (
  input  logic clk,
  input  logic rst_n,
 
  input  logic       rec_entry,      // single-cycle: entering Recovery
  input  rec_cause_t live_causes,    // whatever is asserting right now
 
  // A directed retrain can arrive while Recovery is already running, or
  // while entry is blocked. It must not evaporate.
  input  logic       retrain_pulse,
 
  output rec_cause_t causes,
  output logic       causes_valid,
  output logic       retrain_pending
);
 
  rec_cause_t causes_q;
  logic       valid_q, retrain_q;
 
  assign causes         = causes_q;
  assign causes_valid   = valid_q;
  assign retrain_pending = retrain_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      causes_q <= '0; valid_q <= 1'b0; retrain_q <= 1'b0;
    end else begin
      // ==============================================================
      // A PENDING RETRAIN REQUEST IS A LEVEL, NOT A PULSE.
      //
      // Entry into Recovery can be blocked for a cycle -- the machine may
      // be finishing a previous episode. A one-cycle request wired
      // straight into the entry condition is simply lost, and the
      // software that wrote the Retrain Link register waits forever
      // (section 20, mutation 12).
      // ==============================================================
      if (retrain_pulse)   retrain_q <= 1'b1;
      else if (rec_entry)  retrain_q <= 1'b0;   // consumed EXACTLY ONCE
 
      if (rec_entry) begin
        // CAPTURE EVERYTHING TRUE AT ENTRY, in one assignment. The
        // retrain bit is OR-ed in from the pending flag so a request that
        // arrived while entry was blocked still appears as a cause.
        causes_q             <= live_causes;
        causes_q.retrain_req <= live_causes.retrain_req | retrain_q;
        valid_q              <= 1'b1;
      end
      // ==============================================================
      // AND THEN NOTHING. No arm updates causes_q while the episode runs.
      //
      // This is the point of the block. Live events keep happening during
      // Recovery -- lock drops again, the partner sends more training
      // sets -- and every one of them would overwrite the record of why
      // this episode began. Section 20 measured the damage: 62 of 63
      // cause combinations end up wrong.
      // ==============================================================
    end
  end
 
endmodule

import recovery_pkg::*;
 
// SYNTHESIZABLE. Own exactly one rate-change transaction with the PHY.
// THIS IS SECTION 1'S RECOVERY_SPEED3 MADE CONCRETE: "Request PHY change
// speed and wait for PHY to finish changing speed."
// THE PHY IS A MACRO, not a register. It may stall the request, and it
// takes an unbounded and unknown time to complete.
module phy_rate_owner #(
  parameter int RATE_W = 3
) (
  input  logic clk,
  input  logic rst_n,
 
  // ---- From the Recovery controller --------------------------------------
  input  logic              start,
  input  logic [RATE_W-1:0] requested_rate,
 
  // ---- To the PHY macro ---------------------------------------------------
  output logic              req_valid,
  input  logic              req_ready,
  output logic [RATE_W-1:0] req_rate,
 
  // ---- From the PHY macro. CANNOT BE BACKPRESSURED. -----------------------
  input  logic              done,
  input  logic              success,
 
  // ---- Result -------------------------------------------------------------
  output logic              result_valid,
  output logic [RATE_W-1:0] result_rate,
  output logic              result_success,
  output logic              unowned_done
);
 
  typedef enum logic [1:0] { S_IDLE, S_ISSUE, S_WAIT, S_REPORT } st_e;
  st_e st_q;
 
  logic [RATE_W-1:0] rate_q;
  logic              ok_q, unowned_q;
 
  // ==================================================================
  // req_valid IS TRUE ONLY IN S_ISSUE.
  //
  // The state is left on the HANDSHAKE (req_valid && req_ready), not on
  // `done`. Holding valid until `done` is the classic bug from Chapter
  // 18.2 section 14, and section 20 measured it here: over 2,396,744
  // sequences it produces 452,512 double-accepts and 588,768 results
  // with no accepted request at all.
  // ==================================================================
  assign req_valid      = (st_q == S_ISSUE);
  assign req_rate       = rate_q;              // CAPTURED, never re-read
  assign result_valid   = (st_q == S_REPORT);
  assign result_rate    = rate_q;
  assign result_success = ok_q;
  assign unowned_done   = unowned_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      st_q <= S_IDLE; rate_q <= '0; ok_q <= 1'b0; unowned_q <= 1'b0;
    end else begin
      unique case (st_q)
        S_IDLE : begin
          if (start) begin
            // THE RATE IS CAPTURED AT START. The controller's requested
            // rate may change while the macro stalls -- re-reading it
            // would send the PHY to a rate nobody asked for.
            rate_q <= requested_rate;
            st_q   <= S_ISSUE;
          end
          // A `done` with no outstanding request is REPORTED, never
          // silently consumed. It means a previous transaction completed
          // late, or the macro is signalling something unowned.
          if (done) unowned_q <= 1'b1;
        end
 
        S_ISSUE :
          // LEAVE ON THE HANDSHAKE. One start, one accepted request.
          if (req_ready) st_q <= S_WAIT;
 
        S_WAIT :
          if (done) begin
            ok_q <= success;
            st_q <= S_REPORT;
          end
 
        S_REPORT : st_q <= S_IDLE;
 
        default : st_q <= S_IDLE;
      endcase
    end
  end
 
endmodule

// SYNTHESIZABLE. Qualify re-established training during Recovery.
// SAME CONTRACT AS CHAPTER 18.3's qualifier -- consecutive qualifying
// observations, reset to zero on a bad one, saturating -- because the
// underlying question is the same. THE THRESHOLD IS SEPARATE AND
// PARAMETERISED: this chapter has no source stating that Recovery
// qualification equals Polling qualification, so it does not assume it.
module recovery_qualifier #(
  parameter int THRESH = 4,
  parameter int CNT_W  = (THRESH <= 1) ? 1 : $clog2(THRESH + 1)
) (
  input  logic clk,
  input  logic rst_n,
 
  input  logic restart,          // Recovery entry, or lock lost again
  input  logic qualifying,
  input  logic disqualifying,
 
  output logic [CNT_W-1:0] count,
  output logic             threshold_met
);
 
  generate
    if (THRESH < 1) $error("THRESH must be at least 1");
    if ((1 << CNT_W) < (THRESH + 1)) $error("CNT_W too narrow for THRESH");
  endgenerate
 
  logic [CNT_W-1:0] cnt_q;
  assign count         = cnt_q;
  assign threshold_met = (cnt_q >= CNT_W'(THRESH));
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n)             cnt_q <= '0;
    else if (restart)       cnt_q <= '0;   // priority, declared
    else if (disqualifying) cnt_q <= '0;   // CONSECUTIVE, not cumulative
    else if (qualifying)
      if (cnt_q < CNT_W'(THRESH)) cnt_q <= cnt_q + CNT_W'(1);
  end
 
endmodule

import recovery_pkg::*;
 
// SYNTHESIZABLE. Build the NEW configuration beside the operating one.
// NOTHING HERE IS VISIBLE ABOVE THE PHYSICAL LAYER. This is Chapter 18.4
// section 8's candidate/committed split, applied to a Link that already
// has a committed configuration worth protecting.
module recovery_candidate #(
  parameter int MAX_LANES = 16,
  parameter int LANE_W    = (MAX_LANES <= 1) ? 1 : $clog2(MAX_LANES),
  parameter int WIDTH_W   = 5,
  parameter int RATE_W    = 3
) (
  input  logic clk,
  input  logic rst_n,
 
  input  logic rec_entry,
 
  // ---- The configuration currently in operation --------------------------
  input  logic [RATE_W-1:0]    active_speed,
  input  logic [WIDTH_W-1:0]   active_width,
  input  logic [MAX_LANES-1:0] active_lane_map,
 
  // ---- Results arriving during Recovery ----------------------------------
  input  logic                 rate_result_valid,
  input  logic [RATE_W-1:0]    rate_result,
  input  logic                 rate_result_ok,
 
  input  logic                 width_result_valid,
  input  logic [WIDTH_W-1:0]   width_result,
  input  logic [MAX_LANES-1:0] lane_map_result,
 
  input  logic                 train_ok,
 
  output logic [RATE_W-1:0]    cand_speed,
  output logic [WIDTH_W-1:0]   cand_width,
  output logic [MAX_LANES-1:0] cand_lane_map,
  output logic                 cand_valid
);
 
  logic [RATE_W-1:0]    spd_q;
  logic [WIDTH_W-1:0]   wid_q;
  logic [MAX_LANES-1:0] map_q;
  logic                 spd_bad_q;
 
  assign cand_speed    = spd_q;
  assign cand_width    = wid_q;
  assign cand_lane_map = map_q;
 
  // ==================================================================
  // A CANDIDATE IS VALID ONLY IF TRAINING SUCCEEDED AND NOTHING FAILED.
  //
  // A failed rate change poisons the episode: section 1's speed_change_fail
  // bit exists because the PHY can decline, and committing a configuration
  // that names a rate the PHY never reached is worse than not recovering.
  // ==================================================================
  assign cand_valid = train_ok && !spd_bad_q
                   && (wid_q != '0) && (map_q != '0);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      spd_q <= '0; wid_q <= '0; map_q <= '0; spd_bad_q <= 1'b0;
    end else if (rec_entry) begin
      // ==============================================================
      // SEEDED FROM THE ACTIVE CONFIGURATION, not from zero.
      //
      // Most Recovery episodes change NOTHING -- a retrain after lost
      // lock returns the identical speed, width and lane map. Starting
      // from the operating values means an episode that renegotiates
      // nothing still commits something coherent, and only the fields
      // that were actually re-derived differ.
      //
      // Starting from zero would make every retrain look like a
      // configuration change (section 20, mutation 7).
      // ==============================================================
      spd_q     <= active_speed;
      wid_q     <= active_width;
      map_q     <= active_lane_map;
      spd_bad_q <= 1'b0;
    end else begin
      if (rate_result_valid) begin
        if (rate_result_ok) spd_q     <= rate_result;
        else                spd_bad_q <= 1'b1;   // sticky for the episode
      end
      if (width_result_valid) begin
        wid_q <= width_result;
        map_q <= lane_map_result;   // WIDTH AND MAP TOGETHER, always
      end
    end
  end
 
endmodule

import recovery_pkg::*;
 
// SYNTHESIZABLE. The flagship block: replace the operating configuration
// in ONE cycle or not at all.
// EVERYTHING ABOVE THE PHYSICAL LAYER READS ONLY THESE OUTPUTS. Chapter
// 17.1's lane distributor and Chapter 17.2's recombiner consume them, and
// a Link whose transmitter and receiver disagree about speed or lane map
// corrupts data that no error check can attribute to its cause.
module recovery_commit #(
  parameter int MAX_LANES = 16,
  parameter int WIDTH_W   = 5,
  parameter int RATE_W    = 3
) (
  input  logic clk,
  input  logic rst_n,
 
  input  logic                 cand_valid,
  input  logic [RATE_W-1:0]    cand_speed,
  input  logic [WIDTH_W-1:0]   cand_width,
  input  logic [MAX_LANES-1:0] cand_lane_map,
 
  input  logic recovery_success,   // the Recovery.Idle -> L0 edge
  input  logic link_down,
 
  output logic [RATE_W-1:0]    active_speed,
  output logic [WIDTH_W-1:0]   active_width,
  output logic [MAX_LANES-1:0] active_lane_map,
  output logic                 active_config_valid,
  output logic                 commit_rejected
);
 
  // ONE PACKED STRUCT. Partial commit is not a bug to be avoided here;
  // it is UNCONSTRUCTABLE, because there is no sequence to get wrong.
  typedef struct packed {
    logic                 valid;
    logic [RATE_W-1:0]    speed;
    logic [WIDTH_W-1:0]   width;
    logic [MAX_LANES-1:0] lane_map;
  } link_cfg_t;
 
  link_cfg_t cfg_q;
  logic      rej_q;
 
  assign active_speed        = cfg_q.speed;
  assign active_width        = cfg_q.width;
  assign active_lane_map     = cfg_q.lane_map;
  assign active_config_valid = cfg_q.valid;
  assign commit_rejected     = rej_q;
 
  // Width and map must agree, or the distributor gets an impossible
  // instruction (Chapter 18.4 P6).
  wire commit_ok = cand_valid
                && (cand_width != '0)
                && ($countones(cand_lane_map) == cand_width);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      cfg_q <= '0; rej_q <= 1'b0;
    end else if (link_down) begin
      // ==============================================================
      // LINK-DOWN DOMINATES THE COMMIT. Declared priority.
      //
      // If the Link went down in the same cycle a commit was ready, the
      // configuration being committed describes a Link that no longer
      // exists. Committing it would leave active_config_valid high on a
      // dead Link, and everything above would keep transmitting into it
      // (section 20, mutation 13).
      // ==============================================================
      cfg_q <= '0; rej_q <= 1'b0;
    end else if (recovery_success) begin
      if (commit_ok) begin
        // ============================================================
        // ONE NONBLOCKING ASSIGNMENT. speed, width, lane_map and valid
        // become visible in the SAME cycle.
        //
        // Section 20 measured the alternative across 100,000 random
        // episodes: split registers produced 98,251 cycles in which the
        // active configuration was a combination that was never a
        // coherent candidate. The atomic version produced 0.
        // ============================================================
        cfg_q <= '{ valid    : 1'b1,
                    speed    : cand_speed,
                    width    : cand_width,
                    lane_map : cand_lane_map };
      end else begin
        // A Recovery that "succeeded" without a coherent candidate is a
        // control bug. Expose nothing and say so.
        cfg_q <= '0;
        rej_q <= 1'b1;
      end
    end
    // NOTE THE ABSENCE OF AN ENTRY ARM.
    // Chapter 18.4's cfg_commit clears on state entry because
    // Configuration is reached from Polling with no operational Link to
    // preserve. RECOVERY IS THE OPPOSITE CASE: the old configuration
    // stays active and intact throughout the episode. Copying 18.4's
    // entry arm here would tear down a working configuration in order to
    // renegotiate one that is usually identical (section 23).
  end
 
endmodule

import recovery_pkg::*;
 
// SYNTHESIZABLE. Progress within Recovery only.
// THIS IS NOT THE LTSSM (Chapter 18.1 section 9). It is an
// implementation-facing coordinator whose phases map onto the canonical
// substates verified in section 1 -- it is not their normative encoding,
// and section 1 does not publish the transition criteria it would need
// to be one.
module recovery_progress #(
  parameter int RATE_W = 3
) (
  input  logic clk,
  input  logic rst_n,
 
  input  logic       rec_entry,
  input  rec_cause_t causes,
  input  logic       link_down,
 
  input  logic       rx_lock,
  input  logic       train_threshold_met,
  input  logic       cfg_agreed,
 
  // ---- Rate-change owner (section 12) ------------------------------------
  input  logic       partner_idle,
  output logic       rate_start,
  output logic [RATE_W-1:0] rate_target,
  input  logic       rate_result_valid,
  input  logic       rate_result_ok,
  input  logic [RATE_W-1:0] negotiated_rate,
 
  // ---- Equalization, where applicable (section 17) ------------------------
  input  logic       eq_required,
  input  logic       eq_done,
  input  logic       eq_ok,
 
  input  logic       cand_valid,
  input  logic       timeout_elapsed,
 
  output logic       recovery_success,
  output logic       recovery_fail,
  output logic       traffic_enable,
  output logic       in_speed_phase
);
 
  typedef enum logic [2:0] {
    S_LOCK, S_CFG, S_SPEED_ANNOUNCE, S_SPEED_WAIT, S_SPEED_REQ, S_IDLE,
    S_DONE, S_FAIL
  } st_e;
  st_e st_q;
 
  logic spd_done_q;
 
  assign recovery_success = (st_q == S_DONE);
  assign recovery_fail    = (st_q == S_FAIL);
  assign in_speed_phase   = (st_q inside {S_SPEED_ANNOUNCE, S_SPEED_WAIT,
                                          S_SPEED_REQ});
 
  // ==================================================================
  // NORMAL TRAFFIC IS DISABLED THROUGHOUT RECOVERY, INCLUDING S_DONE.
  //
  // It re-enables only once the commit has happened -- which is the cycle
  // AFTER S_DONE asserts (section 15 registers it). Enabling in S_DONE
  // would let packets out one cycle before the configuration describing
  // how to transmit them became active (section 20, mutation 8).
  // ==================================================================
  assign traffic_enable = 1'b0;   // driven externally from active_config_valid
 
  assign rate_start  = (st_q == S_SPEED_REQ) && !spd_done_q;
  assign rate_target = negotiated_rate;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      st_q <= S_LOCK; spd_done_q <= 1'b0;
    end else if (link_down) begin
      st_q <= S_FAIL;                        // priority over everything
    end else if (rec_entry) begin
      st_q <= S_LOCK; spd_done_q <= 1'b0;
    end else begin
      unique case (st_q)
        S_LOCK :
          if (timeout_elapsed)                    st_q <= S_FAIL;
          else if (rx_lock && train_threshold_met) st_q <= S_CFG;
 
        S_CFG :
          if (timeout_elapsed)      st_q <= S_FAIL;
          else if (!rx_lock)        st_q <= S_LOCK;   // lost it again
          else if (cfg_agreed) begin
            // THE SPEED BRANCH IS TAKEN FROM THE CAPTURED CAUSE, not from
            // a live signal -- and only once per episode.
            if (needs_speed_change(causes) && !spd_done_q)
                                    st_q <= S_SPEED_ANNOUNCE;
            else                    st_q <= S_IDLE;
          end
 
        // ---- Section 1's SPEED0: tell the partner first ------------------
        S_SPEED_ANNOUNCE :
          if (timeout_elapsed) st_q <= S_FAIL;
          else                 st_q <= S_SPEED_WAIT;
 
        // ---- Section 1's SPEED2: BOTH ends must be quiet ----------------
        S_SPEED_WAIT :
          if (timeout_elapsed)   st_q <= S_FAIL;
          else if (partner_idle) st_q <= S_SPEED_REQ;
 
        // ---- Section 1's SPEED3: request the PHY and wait --------------
        S_SPEED_REQ :
          if (rate_result_valid) begin
            spd_done_q <= 1'b1;               // one speed change per episode
            if (rate_result_ok) st_q <= S_LOCK;  // RETRAIN AT THE NEW RATE
            else                st_q <= S_FAIL;
          end else if (timeout_elapsed) st_q <= S_FAIL;
 
        S_IDLE :
          // Equalization, where the generation requires it (section 17).
          if (eq_required && !eq_done)      st_q <= S_IDLE;
          else if (eq_required && !eq_ok)   st_q <= S_FAIL;
          else if (cand_valid)              st_q <= S_DONE;
          else if (timeout_elapsed)         st_q <= S_FAIL;
 
        S_DONE, S_FAIL : ;
        default : st_q <= S_FAIL;
      endcase
    end
  end
 
endmodule

// SVA over the Recovery blocks. These assert the LOCAL contract: what may
// be committed, what the cause record must satisfy, and what the PHY
// transaction owner may do. They assert NOTHING about Recovery succeeding,
// about the partner cooperating, or about any rate being achievable.
 
// ---- ENVIRONMENT ------------------------------------------------------
assume property (@(posedge clk) disable iff (!rst_n)
  rec_entry |=> !rec_entry);
assume property (@(posedge clk) disable iff (!rst_n)
  req_valid |-> !$isunknown(req_rate));
 
// ---- CAUSE OWNERSHIP --------------------------------------------------
 
// P1: the cause is captured on entry and is NEVER recomputed. Section 20
// measured the alternative: wrong for 62 of 63 cause combinations.
property p_cause_frozen;
  @(posedge clk) disable iff (!rst_n)
  (causes_valid && !rec_entry) |=> $stable(causes);
endproperty
a_frozen : assert property (p_cause_frozen);
 
// P2: a Recovery episode always has at least one cause. An entry with no
// cause means something entered Recovery for no represented reason.
property p_cause_nonempty;
  @(posedge clk) disable iff (!rst_n)
  $rose(causes_valid) |-> cause_valid(causes);
endproperty
a_nonempty : assert property (p_cause_nonempty);
 
// P3: A DIRECTED RETRAIN REQUEST IS NEVER LOST. It is held until an entry
// consumes it.
property p_retrain_held;
  @(posedge clk) disable iff (!rst_n)
  (retrain_pending && !rec_entry) |=> retrain_pending;
endproperty
a_retain : assert property (p_retrain_held);
 
// P4: and it is consumed EXACTLY ONCE.
property p_retrain_consumed_once;
  @(posedge clk) disable iff (!rst_n)
  (retrain_pending && rec_entry) |=> !retrain_pending;
endproperty
a_consumed : assert property (p_retrain_consumed_once);
 
// ---- THE PHY RATE TRANSACTION -----------------------------------------
 
// P5: THE REQUEST IS HELD UNDER STALL. The PHY may take any number of
// cycles to become ready.
property p_req_held;
  @(posedge clk) disable iff (!rst_n)
  (req_valid && !req_ready) |=> req_valid;
endproperty
a_held : assert property (p_req_held);
 
// P6: and the requested rate is STABLE while it stalls -- section 12
// captured it at start precisely so this holds.
property p_rate_stable;
  @(posedge clk) disable iff (!rst_n)
  (req_valid && !req_ready) |=> $stable(req_rate);
endproperty
a_rate_stable : assert property (p_rate_stable);
 
// P7: ONE START, AT MOST ONE ACCEPTED REQUEST. This is the property the
// "valid held until done" mutation violates on 452,512 of 2,396,744
// sequences (section 20).
property p_no_double_issue;
  @(posedge clk) disable iff (!rst_n)
  (req_valid && req_ready) |=> !req_valid until_with start;
endproperty
a_single : assert property (p_no_double_issue);
 
// P8: a completion with no outstanding request is REPORTED, never
// consumed as if it belonged to a current transaction.
property p_unowned_done;
  @(posedge clk) disable iff (!rst_n)
  (done && (st_q == S_IDLE)) |=> unowned_done;
endproperty
a_unowned : assert property (p_unowned_done);
 
// P9: A FAILED RATE CHANGE CANNOT BE REPORTED AS SUCCESS. Section 1's
// speed_change_fail bit exists because this outcome is real.
property p_fail_not_success;
  @(posedge clk) disable iff (!rst_n)
  (result_valid && !result_success) |-> !recovery_success;
endproperty
a_spdfail : assert property (p_fail_not_success);
 
// ---- THE COMMIT -------------------------------------------------------
 
// P10: NO COMMIT WITHOUT A VALID CANDIDATE.
property p_no_blind_commit;
  @(posedge clk) disable iff (!rst_n)
  $changed(active_config_valid) && active_config_valid |-> $past(cand_valid);
endproperty
a_guard : assert property (p_no_blind_commit);
 
// P11: ATOMICITY. No field of the active configuration may move alone.
// The property the split-register mutation violates (section 20: 98,251
// incoherent cycles across 100,000 episodes).
property p_atomic;
  @(posedge clk) disable iff (!rst_n)
  ($changed(active_speed) || $changed(active_width)
                          || $changed(active_lane_map))
    |-> ($past(recovery_success) || $past(link_down) || $past(!rst_n));
endproperty
a_atomic : assert property (p_atomic);
 
// P12: THE ACTIVE CONFIGURATION DOES NOT MOVE DURING RECOVERY. The old
// configuration survives the episode intact until the commit.
property p_active_stable_in_recovery;
  @(posedge clk) disable iff (!rst_n)
  (in_recovery && !recovery_success && !link_down)
    |=> ($stable(active_speed) && $stable(active_width)
                               && $stable(active_lane_map));
endproperty
a_stable : assert property (p_active_stable_in_recovery);
 
// P13: candidate state never reaches a consumer. Structurally, the
// distributor's only configuration source is the active outputs.
property p_no_candidate_leak;
  @(posedge clk) disable iff (!rst_n)
  dut_distributor.active_mask ==
    (active_config_valid ? active_lane_map : '0);
endproperty
a_leak : assert property (p_no_candidate_leak);
 
// P14: LINK-DOWN DOMINATES THE COMMIT.
property p_linkdown_priority;
  @(posedge clk) disable iff (!rst_n)
  (link_down && recovery_success) |=> !active_config_valid;
endproperty
a_down : assert property (p_linkdown_priority);
 
// P15: width and lane map always agree in the committed configuration.
property p_width_map_agree;
  @(posedge clk) disable iff (!rst_n)
  active_config_valid |-> ($countones(active_lane_map) == active_width);
endproperty
a_agree : assert property (p_width_map_agree);
 
// ---- TRAFFIC ----------------------------------------------------------
 
// P16: NO NORMAL PACKET TRAFFIC DURING RECOVERY. Note this says nothing
// about the transmitter being silent (section 7).
property p_no_traffic;
  @(posedge clk) disable iff (!rst_n)
  (dut_ltssm.cur_state == ST_RECOVERY) |-> !dut_gate.traffic_enabled;
endproperty
a_no_traffic : assert property (p_no_traffic);
 
// P17: traffic cannot be re-enabled before the configuration is active.
property p_traffic_after_commit;
  @(posedge clk) disable iff (!rst_n)
  dut_gate.traffic_enabled |-> active_config_valid;
endproperty
a_order : assert property (p_traffic_after_commit);
 
// P18: stale training evidence from before this episode cannot qualify it.
property p_no_stale_qual;
  @(posedge clk) disable iff (!rst_n)
  rec_entry |=> (count == '0);
endproperty
a_stale : assert property (p_no_stale_qual);
 
// P19: at most one speed change per Recovery episode.
property p_one_speed_change;
  @(posedge clk) disable iff (!rst_n)
  (result_valid && !rec_entry) |=> !rate_start until_with rec_entry;
endproperty
a_one_speed : assert property (p_one_speed_change);
 
// P20: reset.
property p_reset;
  @(posedge clk)
  !rst_n |=> (!active_config_valid && !causes_valid && !req_valid);
endproperty
a_reset : assert property (p_reset);

rate_start        did the controller ask?          -> §16, cause bits
req_valid/ready   did the macro ACCEPT it?         -> §12, P5
done              did the PHY finish?              -> the macro
success           did it finish SUCCESSFULLY?      -> §1's speed_change_fail
rx_lock           did lock return at the new rate? -> §16 returns to S_LOCK
qual_count        is training being recognised?    -> §13
cand_valid        is there a coherent candidate?   -> §14
commit            did it commit?                   -> §15