Configuration — Lanes Become a Link

Downstream Port  (toward the Endpoint)      Upstream Port  (toward the Root)
  CONFIGURATION_DS_LW_START                   CONFIGURATION_US_LW_START
  CONFIGURATION_DS_LW_ACCEPT                  CONFIGURATION_US_LW_ACCEPT
  CONFIGURATION_DS_LN_WAIT                    CONFIGURATION_US_LN_WAIT
  CONFIGURATION_DS_LN_ACCEPT                  CONFIGURATION_US_LN_ACCEPT
                    both converge at
              CONFIGURATION_COMPLETE → CONFIGURATION_IDLE

physical lane (pins, routing)
    → training
        → logical lane number (position within this Link)

routed         x8      lanes 0-7 present on the board
candidate    0x3F      lanes 0-5 detected and trained  (6 lanes)
configured     x4      lanes 0-3

step             1     2     3     4     5     6     7     8     9
obs_valid        0     1     1     1     1     1     0     0     0
obs_lane         -     0     1     2     1     3     -     -     -
obs_link         -    0A    0A    0A    0A    0A     -     -     -
 
cand_mask       00    01    03    07    07    0F    0F    0F    0F
dup_error        0     0     0     0     1     1     1     1     1
cand_consistent  1     1     1     1     0     0     0     0     0
 
commit_req       0     0     0     0     0     0     0     1     0
config_valid     0     0     0     0     0     0     0     0     0
active_width     -     -     -     -     -     -     -     -     -
l0_handoff       0     0     0     0     0     0     0     0     0

// SYNTHESIZABLE. Normalized Configuration types.
// LEGAL LINK WIDTHS are canonical: x1, x2, x4, x8, x16. Everything else
// here -- field widths, the contiguity policy, the encoding -- is this
// chapter's internal normalization (section 1).
package config_pkg;
 
  parameter int MAX_LANES = 16;
  // GUARDED. Never zero-width, even at MAX_LANES == 1.
  parameter int LANE_W    = (MAX_LANES <= 1) ? 1 : $clog2(MAX_LANES);
  parameter int LINK_W    = 9;   // section 1: the vendor link_num field is 9 bits
  parameter int WIDTH_W   = 5;   // holds 0..16
 
  typedef struct packed {
    logic                valid;
    logic [LANE_W-1:0]   lane_num;   // LOGICAL lane number, not a pad index
    logic [LINK_W-1:0]   link_num;   // NOT a bus number (section 3)
  } cfg_obs_t;
 
  // THE COMMITTED CONFIGURATION. One struct, so section 15 can assign it
  // in a single nonblocking statement and partial commit is unconstructable.
  typedef struct packed {
    logic                   valid;
    logic [WIDTH_W-1:0]     width;       // 0, 1, 2, 4, 8 or 16
    logic [MAX_LANES-1:0]   lane_mask;   // exactly `width` bits set
    logic [LINK_W-1:0]      link_num;
  } link_config_t;
 
  function automatic bit is_legal_width(input logic [WIDTH_W-1:0] w);
    return (w inside {5'd1, 5'd2, 5'd4, 5'd8, 5'd16});
  endfunction
 
endpackage

import config_pkg::*;
 
// SYNTHESIZABLE. Accumulate the set of logical lanes claimed during this
// Configuration attempt.
// THIS BUILDS A CANDIDATE, NOT A CONFIGURATION (section 8). Nothing here
// is visible above the Physical Layer.
module cfg_candidate_collect (
  input  logic clk,
  input  logic rst_n,
 
  input  logic     state_entry,   // entering Configuration: start over
  input  cfg_obs_t obs,
 
  output logic [MAX_LANES-1:0] cand_mask,
  output logic [LINK_W-1:0]    cand_link,
  output logic                 cand_link_seen
);
 
  logic [MAX_LANES-1:0] mask_q;
  logic [LINK_W-1:0]    link_q;
  logic                 seen_q;
 
  assign cand_mask      = mask_q;
  assign cand_link      = link_q;
  assign cand_link_seen = seen_q;
 
  wire in_range = (MAX_LANES == 1) ? (obs.lane_num == '0)
                                   : (obs.lane_num < LANE_W'(MAX_LANES));
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      mask_q <= '0; link_q <= '0; seen_q <= 1'b0;
    end else if (state_entry) begin
      // ==============================================================
      // CHECKED FIRST. A candidate set inherited from a previous attempt
      // would let lanes that trained under different conditions join this
      // Link -- Chapter 18.3 section 12's rule, one layer up.
      // ==============================================================
      mask_q <= '0; link_q <= '0; seen_q <= 1'b0;
    end else if (obs.valid && in_range) begin
      // ONE BIT PER OBSERVATION. Setting a range of bits from a width
      // would assume contiguity that has not been established yet --
      // that is section 14's job, on the finished set.
      mask_q[obs.lane_num] <= 1'b1;
      if (!seen_q) begin
        link_q <= obs.link_num;
        seen_q <= 1'b1;
      end
    end
  end
 
endmodule

import config_pkg::*;
 
// SYNTHESIZABLE. Detect a candidate set that cannot describe a Link.
// TWO LANES CLAIMING THE SAME LOGICAL NUMBER is not a width problem and
// not recoverable by choosing a smaller width -- the set is incoherent,
// and section 15 refuses to commit it at all.
module cfg_consistency (
  input  logic clk,
  input  logic rst_n,
 
  input  logic     state_entry,
  input  cfg_obs_t obs,
 
  input  logic [MAX_LANES-1:0] cand_mask,      // set BEFORE this observation
  input  logic [LINK_W-1:0]    cand_link,
  input  logic                 cand_link_seen,
 
  output logic dup_error,
  output logic range_error,
  output logic link_mismatch,
  output logic cand_consistent
);
 
  logic dup_q, rng_q, lnk_q;
 
  assign dup_error     = dup_q;
  assign range_error   = rng_q;
  assign link_mismatch = lnk_q;
 
  // CONSISTENCY IS A PROPERTY OF THE WHOLE SET, not a verdict on the
  // latest observation -- so these are STICKY until the next attempt.
  // A design that recomputed it per observation would report the set
  // consistent again as soon as a clean observation arrived after a bad
  // one (section 18, mutation 5).
  assign cand_consistent = !dup_q && !rng_q && !lnk_q;
 
  wire in_range = (MAX_LANES == 1) ? (obs.lane_num == '0)
                                   : (obs.lane_num < LANE_W'(MAX_LANES));
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      dup_q <= 1'b0; rng_q <= 1'b0; lnk_q <= 1'b0;
    end else if (state_entry) begin
      // Cleared only on a NEW ATTEMPT. Checked first.
      dup_q <= 1'b0; rng_q <= 1'b0; lnk_q <= 1'b0;
    end else if (obs.valid) begin
      if (!in_range) begin
        rng_q <= 1'b1;
      end else begin
        // THE DUPLICATE TEST. Note it reads cand_mask BEFORE this
        // observation is applied -- comparing against the post-update
        // mask would find every observation to be a duplicate of itself.
        if (cand_mask[obs.lane_num]) dup_q <= 1'b1;
      end
      // A SECOND LINK NUMBER means two different negotiations are being
      // observed on one candidate set. Not a width problem either.
      if (cand_link_seen && (obs.link_num != cand_link)) lnk_q <= 1'b1;
    end
  end
 
endmodule

import config_pkg::*;
 
// SYNTHESIZABLE. Reduce a candidate lane set to a LEGAL Link width.
// WIDTH IS NOT POPCOUNT (section 7). This is combinational and pure --
// it holds no state, so it can be reasoned about and exhaustively checked
// as a function, which section 18 did over all 65,536 masks.
module cfg_width_class (
  input  logic [MAX_LANES-1:0] cand_mask,
  output logic [WIDTH_W-1:0]   width,
  output logic [MAX_LANES-1:0] width_mask
);
 
  // Step 1: the CONTIGUOUS RUN FROM LANE 0.
  // A gap terminates the run. Lanes beyond a gap are good lanes that this
  // Link cannot use (section 7) -- 0x000D has three good lanes and a run
  // of one.
  logic [MAX_LANES:0] run_ok;
  logic [WIDTH_W-1:0] run_len;
 
  always_comb begin
    run_ok[0] = 1'b1;
    for (int i = 0; i < MAX_LANES; i++)
      run_ok[i+1] = run_ok[i] && cand_mask[i];
 
    run_len = '0;
    for (int i = 0; i < MAX_LANES; i++)
      if (run_ok[i+1]) run_len = WIDTH_W'(i + 1);
  end
 
  // Step 2: REDUCE THE RUN TO A LEGAL WIDTH, largest first.
  // A run of 6 is not x6. It is x4, and two working lanes go unused.
  always_comb begin
    if      (run_len >= 5'd16) width = 5'd16;
    else if (run_len >= 5'd8)  width = 5'd8;
    else if (run_len >= 5'd4)  width = 5'd4;
    else if (run_len >= 5'd2)  width = 5'd2;
    else if (run_len >= 5'd1)  width = 5'd1;
    else                       width = 5'd0;   // no usable width
  end
 
  // Step 3: the mask of exactly the lanes the Link will use.
  // BUILT FROM THE WIDTH, never passed through from cand_mask -- so the
  // two can never disagree, and Chapter 17.1's distributor cannot be
  // handed a lane outside the configured width.
  always_comb begin
    width_mask = '0;
    for (int i = 0; i < MAX_LANES; i++)
      if (WIDTH_W'(i) < width) width_mask[i] = 1'b1;
  end
 
endmodule

import config_pkg::*;
 
// SYNTHESIZABLE. The commit boundary (section 8).
// EVERYTHING ABOVE THE PHYSICAL LAYER READS ONLY `cfg` -- the provisional
// values are not brought out. Chapter 17.1's lane distributor and Chapter
// 17.2's recombiner consume this struct, and a half-updated version makes
// them disagree about the shape of the Link.
module cfg_commit (
  input  logic clk,
  input  logic rst_n,
 
  input  logic state_entry,
 
  // ---- Provisional, from sections 12-14 ---------------------------------
  input  logic [WIDTH_W-1:0]   prov_width,
  input  logic [MAX_LANES-1:0] prov_mask,
  input  logic [LINK_W-1:0]    prov_link,
  input  logic                 prov_link_seen,
  input  logic                 cand_consistent,
 
  input  logic commit_req,       // the Complete -> Idle edge (section 1)
 
  // ---- Committed. The ONLY outputs anything above may use. --------------
  output link_config_t cfg,
  output logic         commit_rejected
);
 
  link_config_t cfg_q;
  logic         rej_q;
 
  assign cfg             = cfg_q;
  assign commit_rejected = rej_q;
 
  // ==================================================================
  // THE COMMIT GUARD. Every condition must hold; there is no arm that
  // commits a partial or incoherent result.
  //
  //   consistent   -- no duplicate, no range error, no link mismatch (13)
  //   legal width  -- x0 is not a Link (section 14 returns 0 for an
  //                   unusable set, and that must be refused, not
  //                   committed as a zero-wide Link)
  //   link seen    -- a Link number was actually observed
  // ==================================================================
  wire commit_ok = cand_consistent
                && is_legal_width(prov_width)
                && prov_link_seen;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      cfg_q <= '0; rej_q <= 1'b0;
    end else if (state_entry) begin
      // ENTERING CONFIGURATION INVALIDATES THE COMMITTED CONFIGURATION.
      // Checked first. Configuration is reached from Polling, so there is
      // no operational Link to preserve -- there is nothing above that may
      // legally act on a configuration right now, and a stale width left
      // exposed could only mislead.
      //
      // RECOVERY IS THE OPPOSITE CASE and must not copy this arm. A Link
      // entering Recovery already HAS a coherent operational configuration
      // that stays active until a new one commits (Chapter 18.5). Clearing
      // on entry there would tear down a working configuration to
      // renegotiate one that may end up identical.
      cfg_q <= '0; rej_q <= 1'b0;
    end else if (commit_req) begin
      if (commit_ok) begin
        // ============================================================
        // ONE NONBLOCKING ASSIGNMENT TO ONE PACKED STRUCT.
        //
        // width, lane_mask, link_num and valid become visible in the SAME
        // CYCLE. There is no ordering between them because there is no
        // sequence -- partial commit is not a bug to be avoided here, it
        // is UNCONSTRUCTABLE (section 8).
        // ============================================================
        cfg_q <= '{ valid     : 1'b1,
                    width     : prov_width,
                    lane_mask : prov_mask,
                    link_num  : prov_link };
      end else begin
        // A REFUSED COMMIT LEAVES NOTHING EXPOSED and says so. Committing
        // a "best effort" configuration would hand the distributor a lane
        // map that the receiver is not using.
        cfg_q <= '0;
        rej_q <= 1'b1;
      end
    end
  end
 
endmodule

import config_pkg::*;
 
// SYNTHESIZABLE. Progress within Configuration only.
// THIS IS NOT THE LTSSM (Chapter 18.1 section 9), and it is not Chapter
// 18.5's Recovery -- speed changes, Up/Down-configure and autonomous width
// changes are NOT modelled here (section 1). It sequences one thing:
// collect, check, classify, commit, hand off.
module cfg_progress #(
  parameter int CNT_W = 24
) (
  input  logic clk,
  input  logic rst_n,
 
  input  logic state_entry,
 
  input  logic cand_consistent,
  input  logic prov_link_seen,
  input  logic [WIDTH_W-1:0] prov_width,
  input  logic settle_done,        // enough observation to stop collecting
  input  logic timeout_elapsed,
 
  input  link_config_t cfg,
 
  output logic commit_req,
  output logic config_done,
  output logic config_fail,
  output logic l0_handoff
);
 
  typedef enum logic [2:0] {
    S_WIDTH, S_LANENUM, S_COMPLETE, S_IDLE, S_FAIL
  } st_e;
  st_e st_q;
 
  // COMMIT IS AN EDGE, not a level -- section 1 places it at the
  // Complete -> Idle transition. A level would re-commit every cycle.
  assign commit_req  = (st_q == S_COMPLETE) && settle_done;
  assign config_done = (st_q == S_IDLE);
  assign config_fail = (st_q == S_FAIL);
 
  // ==================================================================
  // THE HANDOFF IS GATED ON THE COMMITTED STRUCT, not on reaching Idle.
  //
  // Reading `cfg.valid` rather than the state means the Link cannot be
  // handed to normal operation unless a configuration was actually
  // committed -- so a refused commit (section 15) cannot be followed by
  // traffic (section 18, mutation 12).
  // ==================================================================
  assign l0_handoff = (st_q == S_IDLE) && cfg.valid;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      st_q <= S_WIDTH;
    end else if (state_entry) begin
      st_q <= S_WIDTH;
    end else begin
      unique case (st_q)
        S_WIDTH :
          // A CANDIDATE THAT IS ALREADY INCOHERENT FAILS IMMEDIATELY.
          // Continuing to collect lanes onto a set with a duplicate wastes
          // the rest of the timeout for a result that cannot commit.
          if (!cand_consistent)          st_q <= S_FAIL;
          else if (timeout_elapsed)      st_q <= S_FAIL;
          else if (settle_done && is_legal_width(prov_width))
                                         st_q <= S_LANENUM;
 
        S_LANENUM :
          if (!cand_consistent)          st_q <= S_FAIL;
          else if (timeout_elapsed)      st_q <= S_FAIL;
          else if (prov_link_seen)       st_q <= S_COMPLETE;
 
        S_COMPLETE :
          // The commit fires on the way out, and the result is checked on
          // arrival: if it was refused, Idle exposes nothing and the
          // handoff does not happen.
          if (!cand_consistent)          st_q <= S_FAIL;
          else if (settle_done)          st_q <= S_IDLE;
          else if (timeout_elapsed)      st_q <= S_FAIL;
 
        S_IDLE, S_FAIL : ;
 
        default : st_q <= S_WIDTH;
      endcase
    end
  end
 
endmodule

// SVA over the Configuration blocks. These assert the LOCAL contract:
// what may be committed, and what the committed result must satisfy.
// They assert NOTHING about the partner agreeing, about any particular
// width being achievable, or about Configuration succeeding.
 
// ---- ENVIRONMENT ------------------------------------------------------
assume property (@(posedge clk) disable iff (!rst_n)
  obs.valid |-> !$isunknown({obs.lane_num, obs.link_num}));
assume property (@(posedge clk) disable iff (!rst_n)
  state_entry |=> !state_entry);
 
// ---- THE CANDIDATE ----------------------------------------------------
 
// P1: entering Configuration starts from an empty candidate -- lanes from
// a previous attempt must not join this Link.
property p_entry_clears;
  @(posedge clk) disable iff (!rst_n)
  state_entry |=> ((cand_mask == '0) && cand_consistent && !cfg.valid);
endproperty
a_entry : assert property (p_entry_clears);
 
// P2: a lane bit is set ONLY by an in-range observation of that lane.
property p_mask_growth;
  @(posedge clk) disable iff (!rst_n)
  ((cand_mask & ~$past(cand_mask)) != '0)
    |-> ($past(obs.valid) && (cand_mask & ~$past(cand_mask))
                          == (MAX_LANES'(1) << $past(obs.lane_num)));
endproperty
a_growth : assert property (p_mask_growth);
 
// P3: A DUPLICATE LOGICAL LANE IS DETECTED. Two lanes cannot occupy one
// position (section 13).
property p_dup_detected;
  @(posedge clk) disable iff (!rst_n)
  (obs.valid && cand_mask[obs.lane_num]) |=> dup_error;
endproperty
a_dup : assert property (p_dup_detected);
 
// P4: inconsistency is STICKY until the next attempt -- a clean
// observation after a bad one does not repair the set.
property p_sticky;
  @(posedge clk) disable iff (!rst_n)
  (!cand_consistent && !state_entry) |=> !cand_consistent;
endproperty
a_sticky : assert property (p_sticky);
 
// ---- THE WIDTH --------------------------------------------------------
 
// P5: THE COMMITTED WIDTH IS ALWAYS LEGAL. x6 is not a Link.
property p_legal_width;
  @(posedge clk) disable iff (!rst_n)
  cfg.valid |-> is_legal_width(cfg.width);
endproperty
a_legal : assert property (p_legal_width);
 
// P6: WIDTH AND MASK AGREE, and the mask uses only candidate lanes.
// The property that keeps Chapter 17.1's distributor safe.
property p_mask_matches_width;
  @(posedge clk) disable iff (!rst_n)
  cfg.valid |-> (($countones(cfg.lane_mask) == cfg.width)
              && ((cfg.lane_mask & ~cand_mask) == '0));
endproperty
a_match : assert property (p_mask_matches_width);
 
// ---- THE COMMIT -------------------------------------------------------
 
// P7: AN INCONSISTENT CANDIDATE IS NEVER COMMITTED.
property p_no_bad_commit;
  @(posedge clk) disable iff (!rst_n)
  $rose(cfg.valid) |-> $past(cand_consistent);
endproperty
a_guard : assert property (p_no_bad_commit);
 
// P8: ATOMICITY. Every field of the committed configuration changes in the
// SAME cycle -- no field may move while the others are stable.
// The counterexample in section 18 is exactly the violation of this.
property p_atomic;
  @(posedge clk) disable iff (!rst_n)
  ($changed(cfg.width) || $changed(cfg.lane_mask) || $changed(cfg.link_num))
    |-> $changed(cfg.valid) || $rose(state_entry) || $rose(commit_req);
endproperty
a_atomic : assert property (p_atomic);
 
// P9: the committed configuration is STABLE between commits -- consumers
// may not see it drift.
property p_stable;
  @(posedge clk) disable iff (!rst_n)
  (cfg.valid && !commit_req && !state_entry) |=> $stable(cfg);
endproperty
a_stable : assert property (p_stable);
 
// P10: A REFUSED COMMIT EXPOSES NOTHING and reports itself.
property p_reject;
  @(posedge clk) disable iff (!rst_n)
  (commit_req && !cand_consistent) |=> (!cfg.valid && commit_rejected);
endproperty
a_reject : assert property (p_reject);
 
// P11: a zero width is never committed as a valid Link.
property p_no_zero_link;
  @(posedge clk) disable iff (!rst_n)
  cfg.valid |-> (cfg.width != '0);
endproperty
a_nonzero : assert property (p_no_zero_link);
 
// ---- THE HANDOFF ------------------------------------------------------
 
// P12: NO HANDOFF TO NORMAL OPERATION WITHOUT A COMMITTED CONFIGURATION.
// The property that connects this chapter to Chapter 18.6.
property p_handoff_needs_commit;
  @(posedge clk) disable iff (!rst_n)
  l0_handoff |-> cfg.valid;
endproperty
a_handoff : assert property (p_handoff_needs_commit);
 
// P13: NO NORMAL TRAFFIC DURING CONFIGURATION. Bound against Chapter
// 18.1's gate -- the Link is not a Link yet.
property p_no_traffic;
  @(posedge clk) disable iff (!rst_n)
  (dut_ltssm.cur_state == ST_CONFIGURATION) |-> !dut_gate.traffic_enabled;
endproperty
a_no_traffic : assert property (p_no_traffic);
 
// P14: the provisional values never reach a consumer -- structurally, the
// only configuration port is `cfg`.
property p_consumer_uses_committed;
  @(posedge clk) disable iff (!rst_n)
  dut_distributor.active_mask == (cfg.valid ? cfg.lane_mask : '0);
endproperty
a_consumer : assert property (p_consumer_uses_committed);
 
// P15: reset.
property p_reset;
  @(posedge clk)
  !rst_n |=> (!cfg.valid && (cand_mask == '0) && !l0_handoff);
endproperty
a_reset : assert property (p_reset);