Link Establishment

// SYNTHESIZABLE. The bring-up sequencer.
//
// It sequences; it does not implement. Every input here is produced by a
// block an earlier chapter owns:
//
//   signal_ok      <- PMD             (Chapter 3.2)
//   clock_locked   <- PMA             (Chapter 2.6)
//   block_locked   <- PCS aligner     (Chapters 3.4, 3.5)
//   markers_locked <- Section 6
//   deskew_ok      <- Section 7
//
// The design rule this module exists to enforce: EACH LOSS FALLS BACK
// EXACTLY AS FAR AS ITS OWN PRECONDITION. A sequencer that returns to DOWN
// on any loss converts every brief search into a full outage, and upper
// layers see a link flap where the PHY saw a two-microsecond re-lock.
package bringup_pkg;
  typedef enum logic [2:0] {
    LS_DOWN    = 3'd0,   // nothing arriving
    LS_SIGNAL  = 3'd1,   // energy present, no timing
    LS_CLOCKED = 3'd2,   // timing recovered, no block boundaries
    LS_BLOCKED = 3'd3,   // blocks parse, lane identity unknown
    LS_MARKED  = 3'd4,   // lanes identified, skew not yet removed
    LS_UP      = 3'd5
  } link_state_e;
endpackage
 
module bringup_sequencer
  import bringup_pkg::*;
#(
  // Per-stage watchdogs. A stage that has not completed within its budget
  // is STALLED, which is a different report from "still progressing" and
  // must be distinguishable -- Section 11 depends on it.
  parameter int unsigned T_SIGNAL = 1_000_000,
  parameter int unsigned T_CLOCK  = 2_000_000,
  parameter int unsigned T_BLOCK  = 8_000_000,
  parameter int unsigned T_MARKER = 4_000_000,
  parameter int unsigned T_DESKEW = 1_000_000,
  parameter int unsigned TMR_W    = 24
) (
  input  logic clk,
  input  logic rst_n,
 
  input  logic negotiated,     // Section 8: both ends agreed what to try
  input  logic signal_ok,
  input  logic clock_locked,
  input  logic block_locked,
  input  logic markers_locked,
  input  logic deskew_ok,
 
  output link_state_e state,
  output logic        link_up,
 
  // How long the current stage has been running. Exposed continuously, not
  // only on failure -- a stage that usually takes 2 ms and today takes 40
  // is a finding even though it eventually succeeded.
  output logic [TMR_W-1:0] stage_elapsed,
  output logic             stage_stalled,
 
  // Pulses, for the timeline recorder of Section 9.
  output logic advanced,
  output logic regressed
);
 
  link_state_e       state_q, state_d;
  logic [TMR_W-1:0]  timer_q;
  logic [TMR_W-1:0]  budget_c;
 
  always_comb begin
    unique case (state_q)
      LS_DOWN:    budget_c = TMR_W'(T_SIGNAL);
      LS_SIGNAL:  budget_c = TMR_W'(T_CLOCK);
      LS_CLOCKED: budget_c = TMR_W'(T_BLOCK);
      LS_BLOCKED: budget_c = TMR_W'(T_MARKER);
      LS_MARKED:  budget_c = TMR_W'(T_DESKEW);
      default:    budget_c = '1;      // LS_UP has no budget
    endcase
  end
 
  always_comb begin
    state_d = state_q;
 
    // Signal loss beats everything. Evaluated FIRST so no later branch can
    // advance a stage on stale evidence after the signal has gone -- the
    // same priority rule Chapter 3.1 §7 asserted for pair training.
    if (!signal_ok && (state_q != LS_DOWN)) begin
      state_d = LS_DOWN;
    end else begin
      unique case (state_q)
        LS_DOWN:
          // Negotiation must complete before the ladder starts. Without
          // this term the ladder can begin against a mode the far end is
          // not using, which fails at clock lock with a healthy channel.
          if (signal_ok && negotiated) state_d = LS_SIGNAL;
 
        LS_SIGNAL:
          if (clock_locked) state_d = LS_CLOCKED;
 
        LS_CLOCKED:
          if (block_locked) state_d = LS_BLOCKED;
 
        LS_BLOCKED: begin
          if      (!block_locked)  state_d = LS_CLOCKED;  // fall back one rung
          else if (markers_locked) state_d = LS_MARKED;
        end
 
        LS_MARKED: begin
          if      (!block_locked)   state_d = LS_CLOCKED;
          else if (!markers_locked) state_d = LS_BLOCKED; // one rung, not two
          else if (deskew_ok)       state_d = LS_UP;
        end
 
        LS_UP: begin
          if      (!block_locked)   state_d = LS_CLOCKED;
          else if (!markers_locked) state_d = LS_BLOCKED;
          else if (!deskew_ok)      state_d = LS_MARKED;
        end
 
        default: state_d = LS_DOWN;
      endcase
    end
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      state_q   <= LS_DOWN;
      timer_q   <= '0;
      advanced  <= 1'b0;
      regressed <= 1'b0;
    end else begin
      state_q <= state_d;
 
      // The timer measures time IN A STAGE, so it resets on any change.
      if (state_d != state_q) timer_q <= '0;
      else if (timer_q != '1) timer_q <= timer_q + 1'b1;
 
      advanced  <= (state_d > state_q);
      regressed <= (state_d < state_q);
    end
  end
 
  assign state         = state_q;
  assign link_up       = (state_q == LS_UP);
  assign stage_elapsed = timer_q;
  assign stage_stalled = (state_q != LS_UP) && (timer_q >= budget_c);
 
endmodule

// SYNTHESIZABLE. Alignment marker insertion and detection.
//
// NO CLAUSE'S MARKER FORMAT IS ENCODED HERE. The three properties that
// matter architecturally are:
//
//   RECOGNISABLE    -- distinguishable from data, so a receiver can find one
//   LANE-IDENTIFYING-- carries which logical lane this physical lane is
//   PERIODIC        -- inserted on a fixed interval, forever
//
// The third is what bounds marker-lock time and what makes Section 7's
// skew measurement possible: the SAME marker goes into every lane at the
// SAME moment, so arrival-time differences ARE the skew.
package marker_pkg;
  parameter int unsigned LANES = 4;
  parameter int unsigned LANE_W = $clog2(LANES);
endpackage
 
module marker_inserter
  import marker_pkg::*;
#(
  // Blocks between markers. The worst-case marker-lock time is exactly this
  // many block times, which is a DESIGNED bound rather than a search that
  // depends on data content.
  parameter int unsigned MARKER_PERIOD = 16384,
  parameter int unsigned PER_W = $clog2(MARKER_PERIOD)
) (
  input  logic clk,
  input  logic rst_n,
 
  input  logic [LANE_W-1:0] lane_id,
 
  input  logic       blk_valid,
  input  logic [65:0] blk_in,
  output logic       blk_ready,
 
  output logic       out_valid,
  output logic [65:0] out_blk,
  output logic       out_is_marker,
 
  // Pulses when a marker is inserted. All lanes must pulse on the SAME
  // cycle -- Section 7's measurement is meaningless otherwise, and
  // Section 13 asserts it.
  output logic       marker_inserted
);
 
  logic [PER_W-1:0] count_q;
  logic             insert_c;
 
  assign insert_c  = (count_q == PER_W'(MARKER_PERIOD - 1));
  // A marker displaces a data block rather than being squeezed between
  // them, so the upstream must be held for exactly one cycle.
  assign blk_ready = !insert_c;
 
  // The marker carries the lane identity and a recognisable body. The body
  // pattern here is illustrative; what matters is that it is distinguishable
  // from data and that the identity field exists.
  function automatic logic [65:0] make_marker(input logic [LANE_W-1:0] id);
    make_marker = {2'b10, 8'hA5, 46'h2A2A_2A2A_2A2A, {(10-LANE_W){1'b0}}, id};
  endfunction
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      count_q         <= '0;
      out_valid       <= 1'b0;
      out_blk         <= '0;
      out_is_marker   <= 1'b0;
      marker_inserted <= 1'b0;
    end else begin
      out_valid       <= 1'b1;      // the PCS never goes silent
      marker_inserted <= insert_c;
 
      if (insert_c) begin
        out_blk       <= make_marker(lane_id);
        out_is_marker <= 1'b1;
        count_q       <= '0;
      end else begin
        out_blk       <= blk_valid ? blk_in : 66'0;
        out_is_marker <= 1'b0;
        count_q       <= count_q + 1'b1;
      end
    end
  end
 
endmodule
 
 
// SYNTHESIZABLE. Detection, on the receive side of one lane.
//
// Marker lock is UNLIKE every other gate on the ladder: its duration is
// bounded by when the transmitter next sends a marker, not by how quickly
// evidence accumulates. So a marker lock taking much longer than one
// marker period means markers are NOT ARRIVING -- a different fault from a
// slow search, and one this module makes distinguishable.
module marker_detector
  import marker_pkg::*;
#(
  parameter int unsigned MARKER_PERIOD = 16384,
  // Consecutive markers at the expected spacing before lock is declared.
  // More than one, because a data block can coincidentally resemble a
  // marker; the SPACING is the strong evidence, not the pattern alone.
  parameter int unsigned LOCK_COUNT = 4,
  parameter int unsigned CNT_W = 24
) (
  input  logic clk,
  input  logic rst_n,
 
  input  logic        blk_valid,
  input  logic [65:0] blk_in,
 
  output logic             marker_seen,
  output logic [LANE_W-1:0] detected_lane_id,
  output logic             marker_locked,
 
  // Cycles since the last marker. If this exceeds the period by a margin,
  // markers have stopped -- which is a transmitter or upstream fault, not
  // a receive search problem.
  output logic [CNT_W-1:0] since_last_marker,
  output logic             markers_missing,
 
  output logic [CNT_W-1:0] c_markers_seen,
  output logic [CNT_W-1:0] c_markers_missed
);
 
  logic [CNT_W-1:0]        gap_q;
  logic [$clog2(LOCK_COUNT+1)-1:0] good_q;
  logic                    is_marker_c;
  logic                    spacing_ok_c;
 
  // Recognition: the control sync header plus the marker body pattern.
  assign is_marker_c = blk_valid
                    && (blk_in[65:64] == 2'b10)
                    && (blk_in[63:56] == 8'hA5);
 
  // The spacing check is the real evidence. A lone matching block proves
  // little; one arriving exactly a period after the last is convincing.
  assign spacing_ok_c = (gap_q >= CNT_W'(MARKER_PERIOD - 2))
                     && (gap_q <= CNT_W'(MARKER_PERIOD + 2));
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      gap_q            <= '0;
      good_q           <= '0;
      marker_seen      <= 1'b0;
      marker_locked    <= 1'b0;
      detected_lane_id <= '0;
      c_markers_seen   <= '0;
      c_markers_missed <= '0;
    end else begin
      marker_seen <= is_marker_c;
 
      if (is_marker_c) begin
        detected_lane_id <= blk_in[LANE_W-1:0];
        gap_q            <= '0;
        if (!(&c_markers_seen)) c_markers_seen <= c_markers_seen + 1'b1;
 
        if (spacing_ok_c) begin
          if (good_q < ($clog2(LOCK_COUNT+1))'(LOCK_COUNT)) good_q <= good_q + 1'b1;
          if (good_q + 1'b1 >= ($clog2(LOCK_COUNT+1))'(LOCK_COUNT)) marker_locked <= 1'b1;
        end else begin
          // Right pattern, wrong spacing: a coincidental match. Restart the
          // evidence rather than counting it.
          good_q <= '0;
        end
      end else begin
        if (blk_valid && (gap_q != '1)) gap_q <= gap_q + 1'b1;
 
        // A marker period passed with no marker. Lock is lost, and the
        // cause is upstream rather than here.
        if (gap_q > CNT_W'(MARKER_PERIOD + (MARKER_PERIOD >> 2))) begin
          marker_locked <= 1'b0;
          good_q        <= '0;
          if (!(&c_markers_missed)) c_markers_missed <= c_markers_missed + 1'b1;
        end
      end
    end
  end
 
  assign since_last_marker = gap_q;
  assign markers_missing   = (gap_q > CNT_W'(MARKER_PERIOD + (MARKER_PERIOD >> 2)));
 
endmodule

// SYNTHESIZABLE. Lane deskew with measurement.
//
// HOW SKEW IS MEASURED: the transmitter inserts the SAME marker into every
// lane at the SAME moment. Any difference in arrival time at the receiver
// is skew accumulated along the physical path -- different fibre lengths,
// different trace lengths, different retimer delays.
//
// So the measurement is: note when each lane's marker arrives, take the
// earliest as the reference, and each lane's lag is its delay.
//
// WHY MEASURING MATTERS MORE THAN ABSORBING: skew drifts with temperature.
// A design that absorbs skew silently works until the day the drift exceeds
// the buffer, and then fails with no warning. A design that REPORTS the
// margin gives months of it.
module lane_deskew
  import marker_pkg::*;
#(
  parameter int unsigned DEPTH  = 64,          // blocks of skew absorbable
  parameter int unsigned PTR_W  = $clog2(DEPTH),
  parameter int unsigned BLK_W  = 66
) (
  input  logic clk,
  input  logic rst_n,
 
  input  logic [LANES-1:0]  lane_valid,
  input  logic [BLK_W-1:0]  lane_blk    [LANES],
  input  logic [LANES-1:0]  lane_marker,     // this lane's marker arrived now
  input  logic [LANES-1:0]  lane_locked,     // this lane has marker lock
 
  output logic              aligned_valid,
  output logic [BLK_W-1:0]  aligned_blk [LANES],
 
  output logic              deskew_ok,
 
  // Measured skew per lane, in blocks, relative to the earliest lane.
  output logic [PTR_W:0]    lane_skew [LANES],
  output logic [PTR_W:0]    worst_skew,
  output logic [LANE_W-1:0] worst_lane,
 
  // How much of the buffer is unused at the current worst skew. This is the
  // number to trend: it shrinks as the system warms, and it reaches zero
  // before anything fails.
  output logic [PTR_W:0]    skew_margin,
 
  // Skew exceeded what the buffer can absorb. Distinct from "not yet
  // aligned" -- this one cannot be fixed by waiting.
  output logic              skew_overflow,
  output logic [15:0]       c_skew_overflow
);
 
  // Per-lane elastic storage. Each lane writes on arrival and all lanes are
  // read together once every lane's marker has been seen.
  logic [BLK_W-1:0] fifo [LANES][DEPTH];
  logic [PTR_W-1:0] wptr [LANES];
  logic [PTR_W-1:0] rptr;
 
  // Marker arrival capture. The first lane to present its marker sets the
  // reference; every other lane's lag is counted from there.
  logic [LANES-1:0] marker_seen_q;
  logic [PTR_W:0]   marker_at   [LANES];
  logic [PTR_W:0]   ref_time_q;
  logic             measuring_q;
  logic [PTR_W:0]   tick_q;
 
  logic all_markers_c;
  assign all_markers_c = &marker_seen_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (int unsigned l = 0; l < LANES; l++) begin
        wptr[l]       <= '0;
        marker_at[l]  <= '0;
        lane_skew[l]  <= '0;
      end
      rptr            <= '0;
      marker_seen_q   <= '0;
      measuring_q     <= 1'b0;
      tick_q          <= '0;
      ref_time_q      <= '0;
      deskew_ok       <= 1'b0;
      skew_overflow   <= 1'b0;
      c_skew_overflow <= '0;
      aligned_valid   <= 1'b0;
    end else begin
      // Write side: each lane stores independently, as it arrives.
      for (int unsigned l = 0; l < LANES; l++) begin
        if (lane_valid[l]) begin
          fifo[l][wptr[l]] <= lane_blk[l];
          wptr[l]          <= wptr[l] + 1'b1;
        end
      end
 
      // Measurement window: opens on the first marker of a round.
      if (|lane_marker && !measuring_q) begin
        measuring_q   <= 1'b1;
        tick_q        <= '0;
        ref_time_q    <= '0;
        marker_seen_q <= lane_marker;
        for (int unsigned l = 0; l < LANES; l++)
          if (lane_marker[l]) marker_at[l] <= '0;
      end else if (measuring_q) begin
        tick_q <= tick_q + 1'b1;
 
        for (int unsigned l = 0; l < LANES; l++) begin
          if (lane_marker[l] && !marker_seen_q[l]) begin
            marker_seen_q[l] <= 1'b1;
            marker_at[l]     <= tick_q;
            lane_skew[l]     <= tick_q;      // lag behind the earliest lane
          end
        end
 
        // Every lane reported: the round is complete.
        if (all_markers_c) begin
          measuring_q   <= 1'b0;
          marker_seen_q <= '0;
          deskew_ok     <= (&lane_locked) && (tick_q < (PTR_W+1)'(DEPTH));
          if (tick_q >= (PTR_W+1)'(DEPTH)) begin
            skew_overflow <= 1'b1;
            if (!(&c_skew_overflow)) c_skew_overflow <= c_skew_overflow + 1'b1;
          end else begin
            skew_overflow <= 1'b0;
          end
        end else if (tick_q >= (PTR_W+1)'(DEPTH)) begin
          // A lane's marker has not arrived within the buffer's reach. It
          // cannot be aligned no matter how long we wait.
          measuring_q   <= 1'b0;
          marker_seen_q <= '0;
          deskew_ok     <= 1'b0;
          skew_overflow <= 1'b1;
          if (!(&c_skew_overflow)) c_skew_overflow <= c_skew_overflow + 1'b1;
        end
      end
 
      // Read side: all lanes advance together once aligned.
      aligned_valid <= deskew_ok;
      if (deskew_ok) rptr <= rptr + 1'b1;
    end
  end
 
  always_comb begin
    for (int unsigned l = 0; l < LANES; l++)
      aligned_blk[l] = fifo[l][(rptr - PTR_W'(lane_skew[l]))];
  end
 
  // Worst lane and the remaining headroom.
  logic [PTR_W:0]    max_c;
  logic [LANE_W-1:0] maxl_c;
  always_comb begin
    max_c  = lane_skew[0];
    maxl_c = '0;
    for (int unsigned l = 1; l < LANES; l++) begin
      if (lane_skew[l] > max_c) begin
        max_c  = lane_skew[l];
        maxl_c = LANE_W'(l);
      end
    end
    worst_skew  = max_c;
    worst_lane  = maxl_c;
    skew_margin = (max_c < (PTR_W+1)'(DEPTH)) ? ((PTR_W+1)'(DEPTH) - max_c)
                                              : '0;
  end
 
endmodule

// SYNTHESIZABLE. Auto-negotiation as a state machine, without a page format.
//
// NO CLAUSE'S LINK CODEWORD IS ENCODED HERE. What is modelled is the shape
// common to every family that negotiates:
//
//   ADVERTISE -> ACKNOWLEDGE -> RESOLVE -> COMMIT
//
// The elegant part is RESOLVE. There is no bargaining -- both ends apply the
// SAME deterministic priority rule to the SAME capability intersection, so
// they agree by construction rather than by exchange. There is no state in
// which the two ends have committed to different answers.
module autoneg
#(
  parameter int unsigned CAP_W       = 8,     // one bit per capability
  parameter int unsigned T_ADVERTISE = 500_000,
  parameter int unsigned T_ACK       = 500_000,
  parameter int unsigned TMR_W       = 24
) (
  input  logic clk,
  input  logic rst_n,
 
  input  logic             an_enable,      // some ports are forced, not negotiated
  input  logic [CAP_W-1:0] local_caps,
 
  // From the far end. Not modelled: how these are carried on the wire.
  input  logic             remote_valid,
  input  logic [CAP_W-1:0] remote_caps,
  input  logic             remote_ack,
 
  output logic             advertising,
  output logic             local_ack,
 
  output logic             negotiated,
  output logic [CAP_W-1:0] selected_cap,   // one-hot: the agreed mode
 
  // Why negotiation did not complete. Three causes, three owners -- and the
  // second is the one that produces the hardest field failures.
  output logic             no_remote,          // far end never advertised
  output logic             no_common_cap,      // both advertised, nothing shared
  output logic             an_timeout,
 
  // Sticky: negotiation completed without the far end participating, so a
  // default was assumed. Section 4's case one, made visible -- this is the
  // duplex-mismatch signature.
  output logic             defaulted
);
 
  typedef enum logic [2:0] {
    AN_IDLE, AN_ADVERTISE, AN_ACK, AN_RESOLVE, AN_DONE, AN_FAIL
  } an_state_e;
 
  an_state_e        state_q, state_d;
  logic [TMR_W-1:0] timer_q;
  logic [CAP_W-1:0] common_c;
 
  assign common_c = local_caps & remote_caps;
 
  // The deterministic priority rule. Highest set bit wins, and BOTH ENDS
  // COMPUTE THE SAME FUNCTION -- which is what makes agreement automatic.
  // The rule itself must be identical at both ends; a design whose priority
  // differs from its peer's produces two ends committed to different modes,
  // each believing negotiation succeeded.
  function automatic logic [CAP_W-1:0] resolve(input logic [CAP_W-1:0] c);
    resolve = '0;
    for (int unsigned i = 0; i < CAP_W; i++)
      if (c[i]) resolve = (CAP_W)'(1) << i;   // highest set bit survives
  endfunction
 
  always_comb begin
    state_d = state_q;
    unique case (state_q)
      AN_IDLE:      if (an_enable) state_d = AN_ADVERTISE;
 
      AN_ADVERTISE: begin
        if      (remote_valid)                       state_d = AN_ACK;
        else if (timer_q >= TMR_W'(T_ADVERTISE))     state_d = AN_FAIL;
      end
 
      AN_ACK: begin
        if      (remote_ack)                   state_d = AN_RESOLVE;
        else if (timer_q >= TMR_W'(T_ACK))     state_d = AN_FAIL;
      end
 
      AN_RESOLVE:   state_d = (common_c != '0) ? AN_DONE : AN_FAIL;
 
      AN_DONE:      if (!an_enable || !remote_valid) state_d = AN_IDLE;
 
      AN_FAIL:      if (!an_enable)                  state_d = AN_IDLE;
 
      default:      state_d = AN_IDLE;
    endcase
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      state_q      <= AN_IDLE;
      timer_q      <= '0;
      selected_cap <= '0;
      defaulted    <= 1'b0;
    end else begin
      state_q <= state_d;
      if (state_d != state_q) timer_q <= '0;
      else if (timer_q != '1) timer_q <= timer_q + 1'b1;
 
      if (state_d == AN_DONE) selected_cap <= resolve(common_c);
 
      // Negotiation was enabled, the far end never spoke, and we proceeded
      // on a default. This is the duplex-mismatch signature, and it is
      // sticky because by the time anyone looks the link may be "up".
      if ((state_q == AN_ADVERTISE) && (state_d == AN_FAIL) && !remote_valid)
        defaulted <= 1'b1;
    end
  end
 
  assign advertising   = (state_q == AN_ADVERTISE);
  assign local_ack     = (state_q == AN_ACK) || (state_q == AN_RESOLVE);
  assign negotiated    = (state_q == AN_DONE) || !an_enable;
  assign no_remote     = (state_q == AN_FAIL) && !remote_valid;
  assign no_common_cap = (state_q == AN_FAIL) && remote_valid && (common_c == '0);
  assign an_timeout    = (state_q == AN_FAIL) && (timer_q >= TMR_W'(T_ACK));
 
endmodule

// SYNTHESIZABLE INSTRUMENTATION.
//
// Current state answers "is the link up". It cannot answer:
//
//   - which gate did it stall at?
//   - how long did each gate take?
//   - did it get further last time than this time?
//   - is bring-up getting slower over weeks?
//
// Those are the questions with owners, and all four need a TIMELINE.
module bringup_timeline
  import bringup_pkg::*;
#(
  parameter int unsigned TS_W   = 32,
  parameter int unsigned NSTAGE = 6
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic        attempt_start,     // a bring-up attempt begins
  input  link_state_e state,
  input  logic        advanced,
  input  logic        regressed,
  input  logic        stage_stalled,
 
  // Time spent in each stage during the attempt that just finished.
  output logic [TS_W-1:0] stage_duration [NSTAGE],
  output logic            timeline_valid,
 
  // The furthest state reached this attempt, and ever. "Ever" matters: a
  // link that once reached UP and now stalls at BLOCKED is a regression,
  // and one that has NEVER reached UP was never configured correctly --
  // completely different investigations.
  output link_state_e furthest_this_attempt,
  output link_state_e furthest_ever,
 
  // Where it stalled, if it did.
  output link_state_e stall_state,
  output logic        stall_valid,
 
  output logic [15:0] c_attempts,
  output logic [15:0] c_successes,
  output logic [15:0] c_regressions,
 
  // Total time of the last successful bring-up. Trend it: a bring-up that
  // took 3 ms in January and 300 ms in July is a marginal link, even though
  // both succeeded and both report UP.
  output logic [TS_W-1:0] last_bringup_time
);
 
  logic [TS_W-1:0] stage_timer_q;
  logic [TS_W-1:0] total_timer_q;
  link_state_e     prev_state_q;
  logic            in_attempt_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (int unsigned i = 0; i < NSTAGE; i++) stage_duration[i] <= '0;
      stage_timer_q         <= '0;
      total_timer_q         <= '0;
      prev_state_q          <= LS_DOWN;
      in_attempt_q          <= 1'b0;
      timeline_valid        <= 1'b0;
      furthest_this_attempt <= LS_DOWN;
      furthest_ever         <= LS_DOWN;
      stall_state           <= LS_DOWN;
      stall_valid           <= 1'b0;
      c_attempts            <= '0;
      c_successes           <= '0;
      c_regressions         <= '0;
      last_bringup_time     <= '0;
    end else begin
      if (clear) begin
        c_attempts    <= '0;
        c_successes   <= '0;
        c_regressions <= '0;
        // furthest_ever deliberately NOT cleared: it distinguishes "never
        // worked" from "worked and regressed", which no counter can.
      end
 
      if (attempt_start) begin
        for (int unsigned i = 0; i < NSTAGE; i++) stage_duration[i] <= '0;
        stage_timer_q         <= '0;
        total_timer_q         <= '0;
        in_attempt_q          <= 1'b1;
        timeline_valid        <= 1'b0;
        furthest_this_attempt <= LS_DOWN;
        stall_valid           <= 1'b0;
        if (!(&c_attempts)) c_attempts <= c_attempts + 1'b1;
      end else if (in_attempt_q) begin
        if (stage_timer_q != '1) stage_timer_q <= stage_timer_q + 1'b1;
        if (total_timer_q != '1) total_timer_q <= total_timer_q + 1'b1;
 
        // A state change closes the stage that just ended.
        if (state != prev_state_q) begin
          stage_duration[prev_state_q] <= stage_timer_q;
          stage_timer_q                <= '0;
        end
 
        if (state > furthest_this_attempt) furthest_this_attempt <= state;
        if (state > furthest_ever)         furthest_ever         <= state;
 
        if (regressed && !(&c_regressions)) c_regressions <= c_regressions + 1'b1;
 
        // Stalled: record WHERE, once, and hold it.
        if (stage_stalled && !stall_valid) begin
          stall_state <= state;
          stall_valid <= 1'b1;
        end
 
        if (state == LS_UP) begin
          in_attempt_q      <= 1'b0;
          timeline_valid    <= 1'b1;
          last_bringup_time <= total_timer_q;
          if (!(&c_successes)) c_successes <= c_successes + 1'b1;
        end
      end
 
      prev_state_q <= state;
    end
  end
 
endmodule

// SYNTHESIZABLE. Per-lane lock, combined late and preserved.
//
// The sequencer needs one bit. An engineer needs LANES bits. Both are cheap;
// only the second is ever omitted, and it is the one that answers the
// question every multi-lane investigation starts with: WHICH LANE?
//
// The asymmetry that makes this worth a module: a link is up only when
// EVERY lane is locked, so the combined bit is dominated by the WORST lane.
// One lane cycling in and out of lock makes the whole link flap, and from
// the combined bit alone that is indistinguishable from all lanes being
// marginal -- a completely different fault with a completely different fix.
module lane_lock_aggregator
  import marker_pkg::*;
#(
  parameter int unsigned CNT_W = 20
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic [LANES-1:0] lane_block_locked,
  input  logic [LANES-1:0] lane_marker_locked,
  input  logic [LANES-1:0] lane_markers_missing,
 
  // What the sequencer of Section 5 consumes.
  output logic block_locked,
  output logic markers_locked,
 
  // What an engineer consumes. Never reduced.
  output logic [LANES-1:0] block_mask,
  output logic [LANES-1:0] marker_mask,
 
  // Lock losses per lane. One lane dominating this is a physical claim
  // about one fibre or one trace; a uniform spread points at something
  // shared -- the reference clock, the supply, the far end.
  output logic [CNT_W-1:0] c_block_loss  [LANES],
  output logic [CNT_W-1:0] c_marker_loss [LANES],
 
  // The lane that has lost lock most often. The single most useful output
  // in the module, and the one an AND gate destroys.
  output logic [LANE_W-1:0] worst_lane,
  output logic              worst_lane_valid,
 
  // Which lanes were unlocked at the moment the combined bit last fell.
  // By the time anyone reads it the lane has usually recovered, so live
  // state says nothing and this is the only surviving evidence.
  output logic [LANES-1:0] down_cause_mask,
  output logic             down_cause_valid,
 
  // Sticky per lane: has this lane EVER locked? Distinguishes a lane that
  // has never worked -- miswired, wrong fibre, dead transceiver -- from one
  // that works and drops. Different faults, identical combined bit.
  output logic [LANES-1:0] ever_locked
);
 
  logic [LANES-1:0] blk_q, mrk_q;
  logic             combined_q;
 
  assign block_locked   = &lane_block_locked;
  assign markers_locked = &lane_marker_locked;
  assign block_mask     = lane_block_locked;
  assign marker_mask    = lane_marker_locked;
 
  wire combined_c = (&lane_block_locked) && (&lane_marker_locked);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (int unsigned l = 0; l < LANES; l++) begin
        c_block_loss[l]  <= '0;
        c_marker_loss[l] <= '0;
      end
      blk_q            <= '0;
      mrk_q            <= '0;
      combined_q       <= 1'b0;
      down_cause_mask  <= '0;
      down_cause_valid <= 1'b0;
      ever_locked      <= '0;
    end else begin
      if (clear) begin
        for (int unsigned l = 0; l < LANES; l++) begin
          c_block_loss[l]  <= '0;
          c_marker_loss[l] <= '0;
        end
        // ever_locked deliberately NOT cleared -- it is a property of the
        // installation, not of a window an operator happened to choose.
      end else begin
        for (int unsigned l = 0; l < LANES; l++) begin
          if (blk_q[l] && !lane_block_locked[l] && !(&c_block_loss[l]))
            c_block_loss[l] <= c_block_loss[l] + 1'b1;
          if (mrk_q[l] && !lane_marker_locked[l] && !(&c_marker_loss[l]))
            c_marker_loss[l] <= c_marker_loss[l] + 1'b1;
        end
      end
 
      blk_q      <= lane_block_locked;
      mrk_q      <= lane_marker_locked;
      combined_q <= combined_c;
 
      for (int unsigned l = 0; l < LANES; l++)
        if (lane_block_locked[l] && lane_marker_locked[l]) ever_locked[l] <= 1'b1;
 
      // Capture on the DOWN edge only. Sampling throughout the outage would
      // record recovery rather than failure.
      if (combined_q && !combined_c) begin
        down_cause_mask  <= ~(lane_block_locked & lane_marker_locked);
        down_cause_valid <= 1'b1;
      end
    end
  end
 
  // Worst lane by combined loss count.
  logic [CNT_W-1:0]  max_c;
  logic [LANE_W-1:0] maxl_c;
  logic              any_c;
 
  always_comb begin
    max_c  = c_block_loss[0] + c_marker_loss[0];
    maxl_c = '0;
    any_c  = (max_c != '0);
    for (int unsigned l = 1; l < LANES; l++) begin
      automatic logic [CNT_W-1:0] tot = c_block_loss[l] + c_marker_loss[l];
      if (tot != '0) any_c = 1'b1;
      if (tot > max_c) begin
        max_c  = tot;
        maxl_c = LANE_W'(l);
      end
    end
    worst_lane       = maxl_c;
    worst_lane_valid = any_c;
  end
 
endmodule

// ─── Ordering: the ladder cannot be skipped ────────────────────────────────
// The chapter's central claim, asserted. Catches: a sequencer that advances
// on a stale lock indication, declaring a link up on preconditions that no
// longer hold.
property p_ladder_is_monotone_upward;
  @(posedge clk) disable iff (!rst_n)
  advanced |-> (state == link_state_e'($past(state) + 1));
endproperty
 
// ─── Safety: signal loss dominates every other transition ──────────────────
// Catches a priority inversion where a stale block_locked lets the machine
// advance after the cable was unplugged. Same rule Chapter 3.1 §13 asserted
// for pair training, at link scope.
property p_signal_loss_wins;
  @(posedge clk) disable iff (!rst_n)
  (!signal_ok && (state != LS_DOWN)) |=> (state == LS_DOWN);
endproperty
 
// ─── Ordering: fallback goes exactly one rung ──────────────────────────────
// Catches a sequencer returning to LS_DOWN on any loss, which turns a
// microsecond block re-lock into a full outage every layer above absorbs.
property p_block_loss_falls_back_one;
  @(posedge clk) disable iff (!rst_n)
  ((state == LS_BLOCKED) && signal_ok && !block_locked) |=> (state == LS_CLOCKED);
endproperty
 
property p_marker_loss_falls_back_one;
  @(posedge clk) disable iff (!rst_n)
  ((state == LS_MARKED) && signal_ok && block_locked && !markers_locked)
    |=> (state == LS_BLOCKED);
endproperty
 
// ─── Causation: negotiation gates the ladder ───────────────────────────────
// Catches a ladder starting before both ends agree what to attempt, which
// fails at clock lock on a healthy channel -- Section 4's hardest case.
property p_ladder_needs_negotiation;
  @(posedge clk) disable iff (!rst_n)
  ((state == LS_DOWN) && !negotiated) |=> (state == LS_DOWN);
endproperty
 
// ─── Safety: link_up requires every gate ───────────────────────────────────
// Catches a design declaring the link usable on a subset of preconditions.
property p_up_requires_all_gates;
  @(posedge clk) disable iff (!rst_n)
  link_up |-> (signal_ok && clock_locked && block_locked
               && markers_locked && deskew_ok);
endproperty
 
// ─── MARKER PROPERTY: all lanes insert simultaneously ──────────────────────
// Section 7's skew measurement is meaningless unless this holds. Catches a
// per-lane counter that can drift, after which measured "skew" is actually
// insertion phase error and the deskew buffer absorbs a fiction.
property p_markers_inserted_together;
  @(posedge clk) disable iff (!rst_n)
  |marker_inserted_vec |-> &marker_inserted_vec;
endproperty
 
// ─── Causation: marker lock needs spacing, not just a pattern ──────────────
// Catches lock declared on a single coincidental pattern match, which locks
// onto a data block that happened to resemble a marker.
property p_marker_lock_needs_spacing;
  @(posedge clk) disable iff (!rst_n)
  $rose(marker_locked) |-> $past(spacing_ok_c);
endproperty
 
// ─── Safety: deskew requires every lane locked ─────────────────────────────
// Catches alignment declared while a lane is still searching, which reads
// that lane's buffer at an arbitrary offset and corrupts every word.
property p_deskew_needs_all_lanes;
  @(posedge clk) disable iff (!rst_n)
  deskew_ok |-> (&lane_locked);
endproperty
 
// ─── Safety: measured skew never exceeds the buffer ────────────────────────
// Catches a read pointer computed from a skew larger than DEPTH, which
// wraps and silently reads the wrong blocks -- data corruption on a link
// reporting alignment.
property p_skew_within_depth;
  @(posedge clk) disable iff (!rst_n)
  deskew_ok |-> (worst_skew < DEPTH);
endproperty
 
// ─── Mutual exclusion: overflow is not "still trying" ──────────────────────
// Catches merging the two, producing a link that appears to be progressing
// when it has actually failed and cannot recover by waiting.
property p_overflow_excludes_ok;
  @(posedge clk) disable iff (!rst_n)
  skew_overflow |-> !deskew_ok;
endproperty
 
// ─── Conservation: the timeline accounts for the whole attempt ─────────────
// Catches stage durations that drop time, making the timeline unusable for
// exactly the diagnosis it exists for.
property p_stage_durations_sum;
  @(posedge clk) disable iff (!rst_n)
  timeline_valid |-> (last_bringup_time == stage_duration_sum);
endproperty
 
// ─── Stability: furthest_ever never decreases ──────────────────────────────
// Catches furthest_ever folded into the clear branch, destroying the
// distinction between "never worked" and "worked and regressed".
property p_furthest_ever_monotone;
  @(posedge clk) disable iff (!rst_n)
  1'b1 |=> (furthest_ever >= $past(furthest_ever));
endproperty
 
// ─── Bounded response: a stalled stage is reported ─────────────────────────
// Catches a watchdog that never fires, leaving a link stuck forever with
// nothing recording where.
property p_stall_is_reported;
  @(posedge clk) disable iff (!rst_n)
  (stage_stalled && (state != LS_UP)) |-> ##[0:2] stall_valid;
endproperty
 
// ─── Conservation: the combined bit is exactly the AND of the lanes ────────
// Catches a combined signal that drifts from its inputs -- typically a
// registered copy that misses a one-cycle drop, after which the sequencer
// and the per-lane masks disagree about whether the link is locked.
property p_combined_matches_lanes;
  @(posedge clk) disable iff (!rst_n)
  (block_locked == (&lane_block_locked))
    && (markers_locked == (&lane_marker_locked));
endproperty
 
// ─── Stability: ever_locked never clears ───────────────────────────────────
// Catches ever_locked folded into the clear branch, which destroys the
// distinction between a lane that has never worked and one that drops.
property p_ever_locked_monotone;
  @(posedge clk) disable iff (!rst_n)
  1'b1 |=> (ever_locked == ($past(ever_locked) | ever_locked));
endproperty