CXL Link Training

module training_fsm #(
  parameter int unsigned MAX_RECOVERY  = 3,
  parameter int unsigned REC_DWELL     = 4,     // bound on ONE recovery attempt
  parameter bit          RETRY_FOREVER = 1'b0   // 1 = the unbounded shape
) (
  input  logic       clk, rst_n, start,
  input  logic       train_ok,       // base training reached a usable state
  input  logic       cxl_agreed,     // negotiation resolved to CXL
  input  logic       link_error, recovered,
  output logic [2:0] state_q,
  output logic       operational, failed, in_recovery,
  output logic [7:0] n_recovery_q, rec_dwell_q,
  output logic       cxl_before_base_err, op_without_training_err,
  output logic       unbounded_recovery_err
);
  localparam logic [2:0] S_DOWN = 3'd0, S_TRAIN = 3'd1, S_BASE = 3'd2,
                         S_SETUP = 3'd3, S_OP = 3'd4, S_REC = 3'd5, S_FAIL = 3'd6;
  logic [2:0] nxt;
  logic       may_retry, dwell_done;
 
  assign may_retry   = RETRY_FOREVER || (n_recovery_q < MAX_RECOVERY[7:0]);
  // An ATTEMPT COUNTER IS NOT A BOUND if the attempt itself can hang. Counting
  // entries into recovery bounds nothing while the machine sits in recovery,
  // so one attempt needs its own dwell bound before the attempt count can
  // advance at all.
  assign dwell_done  = (rec_dwell_q >= REC_DWELL[7:0]);
  assign operational = (state_q == S_OP);
  assign failed      = (state_q == S_FAIL);
  assign in_recovery = (state_q == S_REC);
 
  always_comb begin
    nxt = state_q;
    case (state_q)
      S_DOWN  : if (start)      nxt = S_TRAIN;
      // Base training is PCIe's. Nothing CXL happens here.
      S_TRAIN : if (train_ok)   nxt = S_BASE;
      // The base link exists. CXL setup rides on top of it, never beside it.
      S_BASE  : nxt = cxl_agreed ? S_SETUP : S_OP;
      S_SETUP : nxt = S_OP;
      S_OP    : if (link_error) nxt = S_REC;
      // Recovery re-enters training. It is bounded, and exhausting the bound
      // is a FAILURE, not a silent forever-retry.
      S_REC   : if (recovered)       nxt = S_TRAIN;
                else if (dwell_done) nxt = may_retry ? S_TRAIN : S_FAIL;
      S_FAIL  : ;
      default : nxt = S_FAIL;
    endcase
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      state_q <= S_DOWN; n_recovery_q <= 8'd0; rec_dwell_q <= 8'd0;
      cxl_before_base_err <= 1'b0; op_without_training_err <= 1'b0;
      unbounded_recovery_err <= 1'b0;
    end else begin
      state_q     <= nxt;
      rec_dwell_q <= (nxt == S_REC) ? (rec_dwell_q + 8'd1) : 8'd0;
      if ((state_q != S_REC) && (nxt == S_REC)) n_recovery_q <= n_recovery_q + 8'd1;
 
      if ((nxt == S_SETUP) && (state_q != S_BASE)) cxl_before_base_err <= 1'b1;
      if ((nxt == S_OP) &&
          !((state_q == S_BASE) || (state_q == S_SETUP) || (state_q == S_OP)))
        op_without_training_err <= 1'b1;
      // Stated about the DWELL, which is what actually advances. A check
      // written against n_recovery_q cannot fail while the machine is stuck,
      // because the thing it counts is exactly what has stopped happening.
      if (in_recovery && (rec_dwell_q > REC_DWELL[7:0] + 8'd2))
        unbounded_recovery_err <= 1'b1;
    end
  end
endmodule

module rate_ladder #(
  parameter bit ALLOW_BELOW_FLOOR = 1'b0   // 1 = the broken shape
) (
  input  logic       clk, rst_n,
  input  logic       negotiated,     // alternate protocol negotiation done
  input  logic [2:0] rate_code,      // 0:2.5 1:5 2:8 3:16 4:32 5:64
  input  logic       rate_valid,
  output logic       rate_legal, is_native_rate,
  output logic       below_floor_err, start_rate_err
);
  localparam logic [2:0] START_RATE = 3'd0;   // 2.5 GT/s
  localparam logic [2:0] FLOOR      = 3'd2;   // 8.0 GT/s
 
  assign is_native_rate = rate_valid && (rate_code >= 3'd4);
  // Before negotiation the link is at the start rate. After it, the rate must
  // be at or above the floor.
  assign rate_legal     = rate_valid &&
                          (negotiated ? (ALLOW_BELOW_FLOOR ? 1'b1
                                                           : (rate_code >= FLOOR))
                                      : (rate_code == START_RATE));
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      below_floor_err <= 1'b0; start_rate_err <= 1'b0;
    end else if (rate_valid) begin
      if (negotiated && rate_legal && (rate_code < FLOOR)) below_floor_err <= 1'b1;
      if (!negotiated && (rate_code != START_RATE))        start_rate_err  <= 1'b1;
    end
  end
endmodule

  pre-negotiation  2.5 GT/s : legal=1
  post-negotiation rate[0]  : legal=0 native=0 | allow-below-floor legal=1
  post-negotiation rate[1]  : legal=0 native=0 | allow-below-floor legal=1
  post-negotiation rate[2]  : legal=1 native=0 | allow-below-floor legal=1
  post-negotiation rate[3]  : legal=1 native=0 | allow-below-floor legal=1
  post-negotiation rate[4]  : legal=1 native=1 | allow-below-floor legal=1
  post-negotiation rate[5]  : legal=1 native=1 | allow-below-floor legal=1

module width_negotiate #(
  parameter bit DEGRADED_IS_FAILURE = 1'b0   // 1 = the broken shape
) (
  input  logic       clk, rst_n,
  input  logic [4:0] lanes_requested, lanes_trained,
  input  logic       valid,
  output logic [4:0] width_out,
  output logic       width_legal, is_native_width, degraded, train_ok,
  output logic       overclaim_err, degraded_rejected_err
);
  // You cannot operate wider than the lanes that actually trained.
  assign width_out       = (lanes_trained < lanes_requested) ? lanes_trained
                                                             : lanes_requested;
  assign is_native_width = valid && (width_out >= 5'd4);   // x4, x8, x16
  assign degraded        = valid && (width_out >= 5'd1) && (width_out < 5'd4);
  assign width_legal     = valid && (width_out >= 5'd1);
  // The broken shape refuses to come up narrow at all.
  assign train_ok        = width_legal &&
                           (DEGRADED_IS_FAILURE ? is_native_width : 1'b1);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      overclaim_err <= 1'b0; degraded_rejected_err <= 1'b0;
    end else if (valid) begin
      if (width_out > lanes_trained) overclaim_err <= 1'b1;
      // Diagnostic on the broken variant: a usable narrow link was refused.
      if (DEGRADED_IS_FAILURE && degraded && !train_ok) degraded_rejected_err <= 1'b1;
    end
  end
endmodule

  request x16 trained 16 : width=16 native=1 degraded=0 train_ok=1
  request x16 trained  8 : width=8 native=1 degraded=0 train_ok=1
  request x16 trained  2 : width=2 native=0 degraded=1 train_ok=1 | reject-degraded train_ok=0
  request  x4 trained 16 : width=4  <-- never wider than requested

module recovery_policy #(
  parameter int unsigned MAX_AT_POINT  = 2,
  parameter bit          NEVER_DEGRADE = 1'b0   // 1 = the broken shape
) (
  input  logic       clk, rst_n, error_seen, retrain_ok,
  input  logic [2:0] rate_in,
  output logic [2:0] rate_out,
  output logic [7:0] tries_at_point_q, n_degrade_q,
  output logic       give_up, stuck_err, degraded_past_floor_err
);
  localparam logic [2:0] FLOOR = 3'd2;   // 8.0 GT/s
  logic [2:0] rate_q;
  logic       exhausted;
 
  assign exhausted = (tries_at_point_q >= MAX_AT_POINT[7:0]);
  assign rate_out  = rate_q;
  // Give up only when the operating point cannot be narrowed any further.
  // NEVER_DEGRADE models the real bug shape: retry at the SAME point forever,
  // neither narrowing nor concluding.
  assign give_up   = exhausted && !NEVER_DEGRADE && (rate_q <= FLOOR);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      rate_q <= 3'd5; tries_at_point_q <= 8'd0; n_degrade_q <= 8'd0;
      stuck_err <= 1'b0; degraded_past_floor_err <= 1'b0;
    end else begin
      if (retrain_ok) begin
        tries_at_point_q <= 8'd0;
      end else if (error_seen) begin
        if (exhausted && !NEVER_DEGRADE && (rate_q > FLOOR)) begin
          // Narrow the operating point and reset the attempt count.
          rate_q           <= rate_q - 3'd1;
          n_degrade_q      <= n_degrade_q + 8'd1;
          tries_at_point_q <= 8'd0;
        end else begin
          tries_at_point_q <= tries_at_point_q + 8'd1;
        end
      end
 
      if ((tries_at_point_q > MAX_AT_POINT[7:0] + 8'd1) && !give_up) stuck_err <= 1'b1;
      if (rate_q < FLOOR) degraded_past_floor_err <= 1'b1;
    end
  end
endmodule

  step  error  rate_out  tries  degrades  give_up | never-degrade rate  give_up
  2      1      4        0      1         0       | 5              0
  5      1      3        0      2         0       | 5              0
  8      1      2        0      3         0       | 5              0
  11     1      2        3      3         1       | 5              0
  14     1      2        6      3         1       | 5              0
  correct policy : rate reached 2 after 3 degrades, give_up=1
  never-degrade  : rate still 5, tries=16, give_up=0

module operating_point (
  input  logic        clk, rst_n,
  input  logic [4:0]  width,
  input  logic [2:0]  rate_code,
  input  logic        valid,
  output logic [15:0] bw_proxy,
  output logic        point_native, point_legal,
  output logic        illegal_point_used_err, bw_mismatch_err
);
  logic [15:0] rate_units;
  logic        w_ok, r_ok, w_native, r_native;
 
  // Teaching proxy: 2.5/5/8/16/32/64 -> 1/2/3/6/13/26 units.
  always_comb begin
    case (rate_code)
      3'd0: rate_units = 16'd1;  3'd1: rate_units = 16'd2;
      3'd2: rate_units = 16'd3;  3'd3: rate_units = 16'd6;
      3'd4: rate_units = 16'd13; 3'd5: rate_units = 16'd26;
      default: rate_units = 16'd0;
    endcase
  end
 
  assign w_ok     = (width >= 5'd1) && (width <= 5'd16);
  assign r_ok     = (rate_code >= 3'd2);           // at or above the 8 GT/s floor
  assign w_native = (width >= 5'd4);
  assign r_native = (rate_code >= 3'd4);
 
  assign point_legal  = valid && w_ok && r_ok;
  // Native requires BOTH axes native -- the same AND as Chapter 5.2.
  assign point_native = point_legal && w_native && r_native;
  assign bw_proxy     = point_legal ? ({11'd0, width} * rate_units) : 16'd0;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      illegal_point_used_err <= 1'b0; bw_mismatch_err <= 1'b0;
    end else if (valid) begin
      if (!point_legal && (bw_proxy != 16'd0)) illegal_point_used_err <= 1'b1;
      // Independent restatement: bandwidth is the product, always.
      if (point_legal && (bw_proxy != ({11'd0, width} * rate_units)))
        bw_mismatch_err <= 1'b1;
    end
  end
endmodule

  over 4 widths x 4 rates: native=6 legal-but-degraded=10 illegal=0
  x16 @ rate5 : bw=416  <-- the reference point
  x8  @ rate5 : bw=208  (half the width)
  x16 @ rate4 : bw=208  (one rate step down)

module training_residency (
  input  logic        clk, rst_n, tick,
  input  logic        in_train, in_setup, in_op, in_rec,
  output logic [15:0] t_total_q, t_train_q, t_setup_q, t_op_q, t_rec_q,
  output logic        accounting_err, multi_state_err
);
  logic [2:0] hot;
  assign hot = 3'd0 + in_train + in_setup + in_op + in_rec;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      t_total_q <= '0; t_train_q <= '0; t_setup_q <= '0; t_op_q <= '0; t_rec_q <= '0;
      accounting_err <= 1'b0; multi_state_err <= 1'b0;
    end else begin
      if (tick) begin
        t_total_q <= t_total_q + 16'd1;
        if (in_train) t_train_q <= t_train_q + 16'd1;
        if (in_setup) t_setup_q <= t_setup_q + 16'd1;
        if (in_op)    t_op_q    <= t_op_q    + 16'd1;
        if (in_rec)   t_rec_q   <= t_rec_q   + 16'd1;
      end
      if (t_total_q != t_train_q + t_setup_q + t_op_q + t_rec_q) accounting_err <= 1'b1;
      if (hot > 3'd1) multi_state_err <= 1'b1;
    end
  end
endmodule

  total=100 train=30 setup=8 op=50 recovery=12
  conservation total == train+setup+op+recovery : 100 == 100
  fraction of link life actually operational: 50%

// SAFETY -------------------------------------------------------------------
// V1 — CXL setup is entered only from the base link state.
a_setup_on_base: assert property (@(posedge clk) disable iff (!rst_n)
  (state_q == S_SETUP) |-> ($past(state_q) == S_BASE));
 
// V2 — the base state is never entered before training succeeded.
a_base_needs_trainok: assert property (@(posedge clk) disable iff (!rst_n)
  (state_q == S_BASE) |-> $past(train_ok));
 
// V3 — operational is reached only from base, setup, or itself.
a_op_route: assert property (@(posedge clk) disable iff (!rst_n)
  operational |-> $past(state_q) inside {S_BASE, S_SETUP, S_OP});
 
// V4 — after negotiation the rate is at or above the floor.
a_rate_floor: assert property (@(posedge clk) disable iff (!rst_n)
  (rate_valid && negotiated && rate_legal) |-> (rate_code >= FLOOR));
 
// V5 — before negotiation the link is at the start rate.
a_start_rate: assert property (@(posedge clk) disable iff (!rst_n)
  (rate_valid && !negotiated) |-> (rate_code == START_RATE));
 
// V6 — the operating width never exceeds the lanes that trained.
a_width_bounded: assert property (@(posedge clk) disable iff (!rst_n)
  valid |-> (width_out <= lanes_trained));
 
// V7 — a point is native only if BOTH axes are native.
a_native_both: assert property (@(posedge clk) disable iff (!rst_n)
  point_native |-> (w_native && r_native));
 
// V8 — the rate never degrades below the floor.
a_never_below_floor: assert property (@(posedge clk) disable iff (!rst_n)
  rate_q >= FLOOR);
 
// V9 — CONSERVATION: every tick is in exactly one training state.
a_residency_conserved: assert property (@(posedge clk) disable iff (!rst_n)
  t_total_q == t_train_q + t_setup_q + t_op_q + t_rec_q);
 
// V10 — one recovery attempt is bounded by its dwell.
a_dwell_bounded: assert property (@(posedge clk) disable iff (!rst_n)
  in_recovery |-> (rec_dwell_q <= REC_DWELL + 1));
 
// LIVENESS ------------------------------------------------------------------
// V11 — recovery always terminates: retrain or fail, never neither.
//       Provable BECAUSE of V10. Without the dwell bound this needs an
//       environment assumption that the link eventually recovers, which is
//       exactly the assumption a failing link violates.
a_recovery_terminates: assert property (@(posedge clk) disable iff (!rst_n)
  in_recovery |-> s_eventually (operational || failed));

13/13 killed, 0 escaped