CXL Link Initialisation

module init_fsm #(
  parameter int unsigned TIMEOUT    = 8,
  parameter bit          NO_TIMEOUT = 1'b0   // 1 = the hanging shape
) (
  input  logic       clk, rst_n,
  input  logic       base_link_up,     // link reached the base operating state
  input  logic       local_cxl,
  input  logic       peer_advert_seen, // partner's advertisement observed
  input  logic       peer_cxl, link_error,
  output logic [2:0] state_q,
  output logic       cxl_ready, pcie_fallback, in_error, decided,
  output logic [7:0] wait_q,
  output logic       used_before_decided_err, both_outcomes_err, hung_err
);
  localparam logic [2:0] S_RESET = 3'd0, S_BASE = 3'd1, S_EXCH = 3'd2,
                         S_DECIDE = 3'd3, S_CXL = 3'd4, S_PCIE = 3'd5, S_ERR = 3'd6;
  logic [2:0] nxt;
  logic       timed_out;
 
  assign timed_out     = !NO_TIMEOUT && (wait_q >= TIMEOUT[7:0]);
  assign cxl_ready     = (state_q == S_CXL);
  assign pcie_fallback = (state_q == S_PCIE);
  assign in_error      = (state_q == S_ERR);
  assign decided       = cxl_ready || pcie_fallback;
 
  always_comb begin
    nxt = state_q;
    case (state_q)
      S_RESET : if (base_link_up) nxt = S_BASE;
      // The link is up. It is a PCIe link. Nothing CXL has happened yet.
      S_BASE  : nxt = S_EXCH;
      // Wait to HEAR the partner. A timeout converts waiting into a decision.
      S_EXCH  : if (peer_advert_seen) nxt = S_DECIDE;
                else if (timed_out)   nxt = S_PCIE;
      // Both keys, or fall back. This state cannot loop.
      S_DECIDE: nxt = (local_cxl && peer_cxl) ? S_CXL : S_PCIE;
      S_CXL   : if (link_error) nxt = S_PCIE;   // fall back, never forward
      S_PCIE  : ;                               // terminal for this bring-up
      S_ERR   : ;
      default : nxt = S_ERR;
    endcase
    if (state_q != S_RESET && !base_link_up) nxt = S_ERR;
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      state_q <= S_RESET; wait_q <= 8'd0;
      used_before_decided_err <= 1'b0; both_outcomes_err <= 1'b0; hung_err <= 1'b0;
    end else begin
      state_q <= nxt;
      wait_q  <= (nxt == S_EXCH) ? (wait_q + 8'd1) : 8'd0;
 
      if (cxl_ready && !decided)      used_before_decided_err <= 1'b1;
      if (cxl_ready && pcie_fallback) both_outcomes_err       <= 1'b1;
      // Liveness made checkable: waiting past the bound is a detected fault.
      if ((state_q == S_EXCH) && (wait_q > TIMEOUT[7:0] + 8'd2)) hung_err <= 1'b1;
    end
  end
endmodule

module two_phase_negotiate #(
  parameter bit RESPOND_EARLY = 1'b0    // 1 = the broken shape
) (
  input  logic       clk, rst_n, start,
  input  logic [3:0] host_offer,
  input  logic       host_offer_valid,
  input  logic [3:0] dev_wants,
  input  logic       dev_reply_valid,
  output logic [1:0] phase_q,
  output logic [3:0] enabled_q,
  output logic       complete,
  output logic       replied_before_offer_err, enabled_not_offered_err
);
  localparam logic [1:0] P_IDLE = 2'd0, P_OFFER = 2'd1, P_REPLY = 2'd2, P_DONE = 2'd3;
  logic [3:0] offer_q;
  logic       may_reply, reply_now;
 
  // The guard must be evaluated OUTSIDE the P_REPLY branch, or it is
  // tautological -- inside that branch phase_q == P_REPLY by construction, so
  // the term can never be false and mutating it away changes nothing.
  assign may_reply = RESPOND_EARLY ? (phase_q != P_DONE) : (phase_q == P_REPLY);
  assign reply_now = dev_reply_valid && may_reply;
  assign complete  = (phase_q == P_DONE);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      phase_q <= P_IDLE; offer_q <= 4'h0; enabled_q <= 4'h0;
      replied_before_offer_err <= 1'b0; enabled_not_offered_err <= 1'b0;
    end else begin
      if (reply_now) begin
        // What is enabled is the INTERSECTION, never the request.
        enabled_q <= offer_q & dev_wants;
        phase_q   <= P_DONE;
      end else begin
        case (phase_q)
          P_IDLE  : if (start) phase_q <= P_OFFER;
          P_OFFER : if (host_offer_valid) begin
                      offer_q <= host_offer; phase_q <= P_REPLY;
                    end
          default : ;
        endcase
      end
 
      if (reply_now && (phase_q != P_REPLY)) replied_before_offer_err <= 1'b1;
      // Nothing may be enabled that the host did not offer.
      if (complete && ((enabled_q & ~offer_q) != 4'h0)) enabled_not_offered_err <= 1'b1;
    end
  end
endmodule

  after start        : correct phase=1 | respond-early phase=1
  device replies EARLY: correct enabled=0x0 complete=0 | early enabled=0x0 complete=0
  host offers 0xf    : correct phase=2
  device wants 0x6   : correct enabled=0x6 complete=1
  respond-early replied_before_offer_err=1
  partial offer 0x3, wants 0x6 : enabled=0x2 (expected 0x2)

module capability_intersect #(
  parameter bit USE_UNION = 1'b0        // 1 = the broken shape
) (
  input  logic       clk, rst_n,
  input  logic [3:0] host_caps, dev_caps,
  input  logic       valid,
  output logic [3:0] enabled,
  output logic       any_enabled,
  output logic       not_subset_host_err, not_subset_dev_err, empty_but_claimed_err
);
  assign enabled     = valid ? (USE_UNION ? (host_caps | dev_caps)
                                          : (host_caps & dev_caps)) : 4'h0;
  assign any_enabled = |enabled;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      not_subset_host_err <= 1'b0; not_subset_dev_err <= 1'b0;
      empty_but_claimed_err <= 1'b0;
    end else if (valid) begin
      // Subset of each side, stated separately: a union breaks both, and a
      // one-sided bug breaks exactly one.
      if ((enabled & ~host_caps) != 4'h0) not_subset_host_err <= 1'b1;
      if ((enabled & ~dev_caps)  != 4'h0) not_subset_dev_err  <= 1'b1;
      if (any_enabled && ((host_caps & dev_caps) == 4'h0)) empty_but_claimed_err <= 1'b1;
    end
  end
endmodule

  host=0xF dev=0x6 : correct=0x6 | union-bug=0xf
  host=0x9 dev=0x6 : correct=0x0 any=0 | union-bug=0xf any=1  <-- disjoint
  host=0x3 dev=0x7 : correct=0x3 | union-bug=0x7
  union-bug not_subset_host_err=1 not_subset_dev_err=1

module negotiation_window #(
  parameter bit IGNORE_WINDOW = 1'b0    // 1 = the broken shape
) (
  input  logic       clk, rst_n, os_valid, os_modified,
  input  logic       in_window,        // one of the permitted config states
  input  logic [3:0] adv_field,
  output logic       adv_accepted,
  output logic [3:0] adv_q,
  output logic       accepted_outside_window_err, accepted_unmodified_err
);
  logic gate;
  assign gate         = os_valid && os_modified && (IGNORE_WINDOW ? 1'b1 : in_window);
  assign adv_accepted = gate;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      adv_q <= 4'h0;
      accepted_outside_window_err <= 1'b0; accepted_unmodified_err <= 1'b0;
    end else begin
      if (adv_accepted) adv_q <= adv_field;
      if (adv_accepted && !in_window)   accepted_outside_window_err <= 1'b1;
      if (adv_accepted && !os_modified) accepted_unmodified_err     <= 1'b1;
    end
  end
endmodule

  modified OS, in window     : accepted=1 adv=0x5
  modified OS, OUTSIDE window: accepted=0 adv=0x5 | ignore-window accepted=1
  standard OS, in window     : accepted=0
  ignore-window accepted_outside_window_err=1

module retimer_path #(
  parameter bit ASSUME_UNMODIFIED = 1'b0   // 1 = the broken shape
) (
  input  logic       clk, rst_n, valid,
  input  logic [3:0] far_end_caps, rt1_caps, rt2_caps,
  input  logic       rt1_present, rt2_present,
  output logic [3:0] received_caps, path_caps,
  output logic       path_overclaim_err, silently_narrowed_err
);
  logic [3:0] m1, m2;
  assign m1 = rt1_present ? rt1_caps : 4'hF;
  assign m2 = rt2_present ? rt2_caps : 4'hF;
 
  // What actually arrives has already been narrowed by the path.
  assign received_caps = valid ? (far_end_caps & m1 & m2) : 4'h0;
  // The broken shape ignores the path and trusts the far end's own claim.
  assign path_caps     = valid ? (ASSUME_UNMODIFIED ? far_end_caps : received_caps) : 4'h0;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      path_overclaim_err <= 1'b0; silently_narrowed_err <= 1'b0;
    end else if (valid) begin
      if ((path_caps & ~received_caps) != 4'h0) path_overclaim_err <= 1'b1;
      // Diagnostic, not a fault: the path removed something the far end offered.
      if ((far_end_caps & ~received_caps) != 4'h0) silently_narrowed_err <= 1'b1;
    end
  end
endmodule

  no retimers        : received=0xf correct path=0xf | assume-unmodified=0xf
  one retimer (0x7)  : received=0x7 correct path=0x7 | assume-unmodified=0xf
  two retimers       : received=0x3 correct path=0x3 | assume-unmodified=0xf  <-- overclaim
  far end offered 0xf, path carries 0x3
  assume-unmodified path_overclaim_err=1 | correct silently_narrowed_err=1

module init_outcome_counters (
  input  logic        clk, rst_n, attempt,
  input  logic        got_cxl, got_pcie, got_timeout, got_error,
  output logic [15:0] n_attempt_q, n_cxl_q, n_pcie_q, n_timeout_q, n_error_q,
  output logic        accounting_err, multi_outcome_err
);
  logic [2:0] hot;
  assign hot = {1'b0, 1'b0, 1'b0} + got_cxl + got_pcie + got_error;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      n_attempt_q <= '0; n_cxl_q <= '0; n_pcie_q <= '0;
      n_timeout_q <= '0; n_error_q <= '0;
      accounting_err <= 1'b0; multi_outcome_err <= 1'b0;
    end else begin
      if (attempt)     n_attempt_q <= n_attempt_q + 16'd1;
      if (got_cxl)     n_cxl_q     <= n_cxl_q     + 16'd1;
      if (got_pcie)    n_pcie_q    <= n_pcie_q    + 16'd1;
      if (got_timeout) n_timeout_q <= n_timeout_q + 16'd1;
      if (got_error)   n_error_q   <= n_error_q   + 16'd1;
 
      // Every attempt reaches exactly one terminal outcome. Timeouts are NOT a
      // fourth outcome -- a timeout resolves to PCIe, so it is counted twice
      // on purpose and must not appear in the conservation sum.
      if (n_attempt_q != n_cxl_q + n_pcie_q + n_error_q) accounting_err <= 1'b1;
      if (hot > 3'd1) multi_outcome_err <= 1'b1;
    end
  end
endmodule

  attempts=40 cxl=8 pcie=29 timeout=12 error=3
  conservation attempts == cxl+pcie+error : 40 == 40
  timeouts are a REASON, not an outcome: 12 of 29 PCIe results

// SAFETY -------------------------------------------------------------------
// V1 — CXL is never in use before a decision was reached.
a_decide_then_use: assert property (@(posedge clk) disable iff (!rst_n)
  cxl_ready |-> decided);
 
// V2 — the two outcomes are mutually exclusive.
a_one_outcome: assert property (@(posedge clk) disable iff (!rst_n)
  !(cxl_ready && pcie_fallback));
 
// V3 — CXL is entered only from the decision state, never from BASE.
a_no_shortcut: assert property (@(posedge clk) disable iff (!rst_n)
  (state_q == S_CXL) |-> $past(state_q) inside {S_DECIDE, S_CXL});
 
// V4 — an error in CXL falls back by the next cycle.
a_error_falls_back: assert property (@(posedge clk) disable iff (!rst_n)
  (cxl_ready && link_error) |=> pcie_fallback);
 
// V5 — nothing is enabled that the host did not offer.
a_subset_of_offer: assert property (@(posedge clk) disable iff (!rst_n)
  complete |-> ((enabled_q & ~offer_q) == '0));
 
// V6 — the enabled set is a subset of BOTH advertisements.
a_subset_both: assert property (@(posedge clk) disable iff (!rst_n)
  valid |-> (((enabled & ~host_caps) == '0) && ((enabled & ~dev_caps) == '0)));
 
// V7 — an advertisement is accepted only in the window, and only modified.
a_window_and_variant: assert property (@(posedge clk) disable iff (!rst_n)
  adv_accepted |-> (in_window && os_modified));
 
// V8 — nothing is claimed that the path cannot carry.
a_path_bounds_claim: assert property (@(posedge clk) disable iff (!rst_n)
  valid |-> ((path_caps & ~received_caps) == '0));
 
// V9 — CONSERVATION: every attempt reaches exactly one terminal outcome.
a_outcomes_conserved: assert property (@(posedge clk) disable iff (!rst_n)
  n_attempt_q == n_cxl_q + n_pcie_q + n_error_q);
 
// V10 — a reply is never acted on before the offer has been recorded.
a_reply_after_offer: assert property (@(posedge clk) disable iff (!rst_n)
  reply_now |-> (phase_q == P_REPLY));
 
// SAFETY, formerly LIVENESS -------------------------------------------------
// V11 — the machine leaves EXCH within the bound, UNCONDITIONALLY.
//       This was a liveness property in Chapter 5.1 with an environment
//       assumption about the peer. The timeout discharges the assumption and
//       makes it a safety property of the design alone.
a_bounded_wait: assert property (@(posedge clk) disable iff (!rst_n)
  (state_q == S_EXCH) |-> (wait_q <= TIMEOUT + 1));
 
// LIVENESS ------------------------------------------------------------------
// V12 — a link that comes up eventually decides.
//       With the timeout present this is IMPLIED BY V11 and needs no
//       environment assumption. Stated separately because it is the property
//       anyone actually cares about, and V11 is how it is discharged.
a_eventually_decides: assert property (@(posedge clk) disable iff (!rst_n)
  base_link_up |-> s_eventually decided);

12/12 killed, 0 escaped