1 Gigabit — Four Pairs, Echo Cancellation and GMII

// SYNTHESIZABLE.
//
// Master/slave resolution for 1000BASE-T.
//
// WHY A LINK NEEDS ONE CLOCK:
//   Both ends transmit on all four pairs at once. Each receiver
//   subtracts a replica of its own transmission from what it hears. The
//   replica is aligned to the LOCAL transmit clock; the samples are
//   taken on the RECEIVE clock. If those two clocks differ, the
//   alignment walks and the replica stops cancelling.
//
//   The standard removes the possibility rather than tracking it:
//     MASTER -- transmits on its own reference clock,
//               125.00 MHz +/- 0.01%
//     SLAVE  -- recovers the clock from the master's signal and
//               transmits on the RECOVERED clock (loop timing)
//   One clock exists on the link. There is nothing to drift against.
//
// The preference is exchanged in autonegotiation's NEXT PAGES
// (Chapter 9.2), and it must resolve to exactly one master.
package gig_pkg;
 
  localparam int unsigned SYMBOL_RATE_MBAUD = 125;
  localparam int unsigned SYMBOL_PERIOD_NS  = 8;
  localparam int unsigned PAIRS             = 4;
  localparam int unsigned SKEW_LIMIT_NS     = 50;   // clause 40
  // 50 ns / 8 ns -> 6.25, so 7 symbol periods of range is the minimum
  // that covers the standard's worst case.
  localparam int unsigned SKEW_LIMIT_SYMS   = 7;
 
  typedef enum logic [1:0] {
    ROLE_UNRESOLVED,
    ROLE_MASTER,
    ROLE_SLAVE,
    ROLE_CONFLICT
  } role_e;
 
endpackage
 
module master_slave_timing_arbiter
  import gig_pkg::*;
#(
  parameter int unsigned CNT_W = 16
) (
  input  logic clk,
  input  logic rst_n,
 
  input  logic       page_valid,          // a next page arrived
  // This end's advertised preference.
  input  logic       local_prefers_master,
  input  logic       local_is_multiport,  // a switch: prefers master
  input  logic       local_manual_force,
 
  // The partner's, from the received next page.
  input  logic       partner_prefers_master,
  input  logic       partner_is_multiport,
  input  logic       partner_manual_force,
 
  // The tie break of last resort: a random seed each end generates.
  // Advertised, compared, higher wins.
  input  logic [10:0] local_seed,
  input  logic [10:0] partner_seed,
 
  output role_e      role,
  output logic       role_valid,
  // BOTH ends forced the same way. Not resolvable, and the link must
  // not come up -- a link with two masters has two clocks.
  output logic       conflict,
  // The resolution came from the seed, which means it is not stable
  // across restarts. Reported because a link that changes role on every
  // retrain is a link whose seeds collide.
  output logic       resolved_by_seed,
 
  output logic [CNT_W-1:0] c_resolutions,
  output logic [CNT_W-1:0] c_seed_ties
);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      role <= ROLE_UNRESOLVED; role_valid <= 1'b0; conflict <= 1'b0;
      resolved_by_seed <= 1'b0; c_resolutions <= '0; c_seed_ties <= '0;
    end else begin
      role_valid <= 1'b0;
 
      if (page_valid) begin
        role_valid       <= 1'b1;
        resolved_by_seed <= 1'b0;
        conflict         <= 1'b0;
        if (!(&c_resolutions)) c_resolutions <= c_resolutions + 1'b1;
 
        // PRIORITY ORDER. Each rung is checked only when the one above
        // it does not separate the two ends.
        if (local_manual_force && partner_manual_force &&
            (local_prefers_master == partner_prefers_master)) begin
          // Both administratively forced the same way. There is no
          // resolution, and coming up anyway would put two clocks --
          // or none -- on a link that permits one.
          role     <= ROLE_CONFLICT;
          conflict <= 1'b1;
        end else if (local_manual_force != partner_manual_force) begin
          // A forced end wins over an unforced one.
          role <= local_manual_force
                    ? (local_prefers_master ? ROLE_MASTER : ROLE_SLAVE)
                    : (partner_prefers_master ? ROLE_SLAVE : ROLE_MASTER);
        end else if (local_is_multiport != partner_is_multiport) begin
          // A multiport device (a switch) is master over a single-port
          // one, because its clock is the one many links already share.
          role <= local_is_multiport ? ROLE_MASTER : ROLE_SLAVE;
        end else if (local_seed != partner_seed) begin
          // THE TIE BREAK. Both ends generate a seed, advertise it, and
          // the higher one takes master.
          role             <= (local_seed > partner_seed) ? ROLE_MASTER
                                                          : ROLE_SLAVE;
          resolved_by_seed <= 1'b1;
        end else begin
          // Equal seeds: no resolution this attempt. Retry with a new
          // seed rather than pick, because picking without a rule means
          // both ends pick the same.
          role <= ROLE_UNRESOLVED;
          if (!(&c_seed_ties)) c_seed_ties <= c_seed_ties + 1'b1;
        end
      end
    end
  end
 
endmodule

// BEHAVIOURAL MODEL of the control layer around an adaptive canceller.
// The datapath is abstracted; the CONTROL is the subject.
//
// The loop's job: build a replica of the locally-known interference
// (echo from this pair's own transmitter, NEXT from the three others)
// and subtract it. It cannot be designed from a datasheet, because the
// coupling depends on THIS cable, THIS connector and THIS temperature.
// So it is MEASURED, by adapting until the residual stops falling.
//
// THREE STATES THE DESIGN MUST DISTINGUISH, and most designs carry two:
//   ADAPTING      -- residual still falling; not yet usable
//   CONVERGED     -- residual below threshold and STABLE for a dwell
//   DIVERGED      -- residual rising; the loop is making it worse
//
// The third is the one that is omitted, and its absence is why a
// mis-adapting link presents as a cable fault.
module echo_canceller_control
  import gig_pkg::*;
#(
  parameter int unsigned RESIDUAL_W    = 16,
  // Below this, the residual is small enough to decode through.
  parameter int unsigned CONV_THRESHOLD = 16'd400,
  // It must STAY there this long. A residual that dips below threshold
  // for one sample has not converged, it has been lucky.
  parameter int unsigned DWELL_CYCLES  = 16'd2048,
  // Total budget. Past this, the loop is declared failed rather than
  // left adapting forever.
  parameter int unsigned ADAPT_BUDGET  = 32'd2_000_000,
  parameter int unsigned CNT_W = 16
) (
  input  logic clk,
  input  logic rst_n,
  input  logic start,                 // begin adaptation
  input  logic freeze,                // hold coefficients
 
  // Residual error magnitude after subtraction, from the datapath.
  input  logic [RESIDUAL_W-1:0] residual,
  input  logic                  residual_valid,
 
  output logic adapting,
  output logic converged,
  // The residual is RISING. A loop that is diverging is actively making
  // the signal worse than not cancelling at all.
  output logic diverged,
  // The budget expired without convergence. Distinct from diverged:
  // this one never got worse, it just never got good enough.
  output logic budget_expired,
 
  // Sticky, surviving a retrain: this loop has failed before.
  output logic ever_failed,
 
  output logic [RESIDUAL_W-1:0] best_residual,
  output logic [CNT_W-1:0]      c_convergences,
  output logic [CNT_W-1:0]      c_failures
);
 
  logic [15:0] dwell_q;
  logic [31:0] budget_q;
  logic [RESIDUAL_W-1:0] prev_q;
  logic [3:0]  rising_q;      // consecutive rises
 
  // Four consecutive rises is a trend; one is noise. The distinction is
  // the difference between a divergence report and a false alarm on a
  // loop that is converging normally.
  localparam int unsigned RISE_TREND = 4;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      adapting <= 1'b0; converged <= 1'b0; diverged <= 1'b0;
      budget_expired <= 1'b0; ever_failed <= 1'b0;
      best_residual <= '1; dwell_q <= '0; budget_q <= '0;
      prev_q <= '1; rising_q <= '0;
      c_convergences <= '0; c_failures <= '0;
    end else if (start) begin
      adapting <= 1'b1; converged <= 1'b0; diverged <= 1'b0;
      budget_expired <= 1'b0;
      dwell_q <= '0; budget_q <= '0; best_residual <= '1;
      prev_q <= '1; rising_q <= '0;
    end else if (adapting && !freeze && residual_valid) begin
 
      budget_q <= budget_q + 1'b1;
      prev_q   <= residual;
 
      if (residual < best_residual) best_residual <= residual;
 
      // DIVERGENCE. Track a run of rises rather than a single one --
      // an adapting loop's residual is noisy and will rise sometimes.
      if (residual > prev_q) begin
        if (rising_q != RISE_TREND) rising_q <= rising_q + 1'b1;
      end else begin
        rising_q <= '0;
      end
 
      if (rising_q == RISE_TREND) begin
        adapting    <= 1'b0;
        diverged    <= 1'b1;
        ever_failed <= 1'b1;
        if (!(&c_failures)) c_failures <= c_failures + 1'b1;
 
      // CONVERGENCE requires the residual to be low AND to STAY low.
      end else if (residual <= CONV_THRESHOLD) begin
        if (dwell_q == DWELL_CYCLES) begin
          adapting  <= 1'b0;
          converged <= 1'b1;
          if (!(&c_convergences)) c_convergences <= c_convergences + 1'b1;
        end else begin
          dwell_q <= dwell_q + 1'b1;
        end
      end else begin
        // Above threshold: the dwell restarts from zero, not from where
        // it was. Partial dwell does not accumulate across excursions.
        dwell_q <= '0;
 
        if (budget_q == ADAPT_BUDGET) begin
          adapting       <= 1'b0;
          budget_expired <= 1'b1;
          ever_failed    <= 1'b1;
          if (!(&c_failures)) c_failures <= c_failures + 1'b1;
        end
      end
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// Realigns the four pairs, which do not arrive at the same time.
//
// WHY THEY DIFFER: the four pairs in a Category 5 cable have different
// twist rates -- deliberately, because differing twists is what keeps
// them from coupling into each other. Different twist rate means
// different physical length inside the same jacket, which means
// different propagation delay.
//
// THE NUMBERS (clause 40):
//   inter-pair delay skew tolerated : 50 ns
//   symbol period at 125 Mbaud      :  8 ns
//   50 / 8                          : 6.25 symbol periods
//   so the realigner needs 7 symbols of range to cover the worst case
//
// And the skew is a property of the CABLE, so it is constant while the
// link is up. It is measured once at training and then held -- which is
// why re-measuring it during data is a bug rather than robustness.
module pair_skew_compensator
  import gig_pkg::*;
#(
  parameter int unsigned SYM_W = 3,          // one PAM-5 symbol
  parameter int unsigned DEPTH = SKEW_LIMIT_SYMS + 1,
  parameter int unsigned CNT_W = 16
) (
  input  logic clk,
  input  logic rst_n,
 
  input  logic                   train_mode,
  // Per-pair arrival of the training marker, used to measure skew.
  input  logic [PAIRS-1:0]       marker_seen,
  input  logic [PAIRS-1:0][SYM_W-1:0] sym_in,
  input  logic                   sym_valid,
 
  output logic [PAIRS-1:0][SYM_W-1:0] sym_out,
  output logic                   sym_out_valid,
 
  output logic                   skew_measured,
  output logic [PAIRS-1:0][3:0]  pair_delay_syms,
  output logic [3:0]             worst_skew_syms,
  // The measured skew needs more range than the compensator has. The
  // cable is out of specification, and the correct response is to say
  // so rather than to align three pairs and mis-align the fourth.
  output logic                   skew_out_of_range,
  output logic [CNT_W-1:0]       c_measurements
);
 
  logic [PAIRS-1:0][SYM_W-1:0] pipe_q [DEPTH];
  logic [3:0]  arrive_q [PAIRS];
  logic [3:0]  tick_q;
  logic [PAIRS-1:0] arrived_q;
  logic        measuring_q;
 
  integer i, j;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      skew_measured <= 1'b0; skew_out_of_range <= 1'b0;
      worst_skew_syms <= '0; tick_q <= '0; arrived_q <= '0;
      measuring_q <= 1'b0; c_measurements <= '0;
      for (i = 0; i < PAIRS; i = i + 1) begin
        arrive_q[i]        <= '0;
        pair_delay_syms[i] <= '0;
      end
    end else begin
 
      // MEASURE, in training only. The first pair to show its marker is
      // the reference; every other pair's delay is how many symbol
      // periods later its marker arrived.
      if (train_mode) begin
        if (!measuring_q && (|marker_seen)) begin
          measuring_q <= 1'b1;
          tick_q      <= '0;
          arrived_q   <= marker_seen;
          for (i = 0; i < PAIRS; i = i + 1)
            if (marker_seen[i]) arrive_q[i] <= '0;
        end else if (measuring_q) begin
          tick_q <= tick_q + 1'b1;
          for (i = 0; i < PAIRS; i = i + 1) begin
            if (marker_seen[i] && !arrived_q[i]) begin
              arrive_q[i]  <= tick_q + 1'b1;
              arrived_q[i] <= 1'b1;
            end
          end
 
          if (&arrived_q) begin
            measuring_q   <= 1'b0;
            skew_measured <= 1'b1;
            if (!(&c_measurements)) c_measurements <= c_measurements + 1'b1;
 
            // The pair that arrived LAST needs no delay; every earlier
            // pair is held back until it agrees.
            for (i = 0; i < PAIRS; i = i + 1)
              pair_delay_syms[i] <= tick_q - arrive_q[i];
 
            worst_skew_syms <= tick_q;
            // OUT OF RANGE. Report; do not clamp. A clamped delay
            // aligns three pairs and leaves the fourth misaligned by a
            // symbol, which decodes as a burst of errors on one pair.
            skew_out_of_range <= (tick_q > 4'(SKEW_LIMIT_SYMS));
          end
        end
      end
 
      // APPLY, in data mode. A shift pipeline per pair, tapped at the
      // measured depth. The measurement is NOT repeated here: the skew
      // is a property of the cable and does not change while the link
      // is up, so a re-measurement can only be responding to noise.
      if (sym_valid) begin
        for (j = DEPTH-1; j > 0; j = j - 1) pipe_q[j] <= pipe_q[j-1];
        pipe_q[0] <= sym_in;
      end
      sym_out_valid <= sym_valid;
    end
  end
 
  always_comb begin
    for (int p = 0; p < PAIRS; p = p + 1)
      sym_out[p] = pipe_q[pair_delay_syms[p]][p];
  end
 
endmodule

// SYNTHESIZABLE.
//
// Sequences link startup, and its whole purpose is ORDERING.
//
// Gigabit bring-up has dependencies that cannot be reordered:
//
//   1. ROLE      -- master/slave must resolve first, because the slave
//                   cannot recover a clock until it knows to.
//   2. TIMING    -- the slave locks to the master's clock. Every later
//                   step assumes one time base.
//   3. SKEW      -- measured once the pairs are carrying markers.
//   4. CANCELLERS-- adapt, on all four pairs, and each must converge.
//   5. DATA      -- and only now.
//
// The sequencer's contract is that step N never begins until step N-1
// has DECLARED success, and that the whole thing is bounded.
module startup_training_sequencer
  import gig_pkg::*;
#(
  parameter int unsigned STEP_TIMEOUT = 32'd4_000_000,
  parameter int unsigned CNT_W = 16
) (
  input  logic clk,
  input  logic rst_n,
  input  logic link_signal_present,
 
  input  logic role_valid,
  input  logic role_conflict,
  input  logic timing_locked,
  input  logic skew_measured,
  input  logic skew_out_of_range,
  input  logic [PAIRS-1:0] canceller_converged,
  input  logic [PAIRS-1:0] canceller_failed,
 
  output logic       start_cancellers,
  output logic       train_mode,
  output logic       data_mode,
  output logic [2:0] stage,
  // Which stage failed, latched at the moment of failure. Held until
  // the next attempt starts, because by the time anyone reads it the
  // state machine is back at idle.
  output logic [2:0] failed_stage,
  output logic       training_failed,
  output logic [CNT_W-1:0] c_attempts,
  output logic [CNT_W-1:0] c_failures
);
 
  typedef enum logic [2:0] {
    S_IDLE, S_ROLE, S_TIMING, S_SKEW, S_CANCEL, S_DATA, S_FAILED
  } stage_e;
 
  stage_e      stage_q;
  logic [31:0] timer_q;
 
  assign stage      = stage_q;
  assign train_mode = (stage_q == S_SKEW) || (stage_q == S_CANCEL);
  assign data_mode  = (stage_q == S_DATA);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      stage_q <= S_IDLE; timer_q <= '0; start_cancellers <= 1'b0;
      failed_stage <= 3'(S_IDLE); training_failed <= 1'b0;
      c_attempts <= '0; c_failures <= '0;
    end else begin
      start_cancellers <= 1'b0;
      training_failed  <= 1'b0;
      timer_q          <= timer_q + 1'b1;
 
      // A link that drops restarts from the beginning, always. There is
      // no partial resume: every measurement below depends on a clock
      // that is no longer known to be there.
      if (!link_signal_present && (stage_q != S_IDLE)) begin
        stage_q <= S_IDLE;
        timer_q <= '0;
      end else begin
        unique case (stage_q)
          S_IDLE: if (link_signal_present) begin
            stage_q <= S_ROLE;
            timer_q <= '0;
            if (!(&c_attempts)) c_attempts <= c_attempts + 1'b1;
          end
 
          S_ROLE: if (role_conflict) begin
            // Unresolvable. Fail immediately rather than time out --
            // waiting adds latency and cannot change the answer.
            stage_q <= S_FAILED; failed_stage <= 3'(S_ROLE);
          end else if (role_valid) begin
            stage_q <= S_TIMING; timer_q <= '0;
          end else if (timer_q == STEP_TIMEOUT) begin
            stage_q <= S_FAILED; failed_stage <= 3'(S_ROLE);
          end
 
          S_TIMING: if (timing_locked) begin
            stage_q <= S_SKEW; timer_q <= '0;
          end else if (timer_q == STEP_TIMEOUT) begin
            stage_q <= S_FAILED; failed_stage <= 3'(S_TIMING);
          end
 
          S_SKEW: if (skew_measured && skew_out_of_range) begin
            stage_q <= S_FAILED; failed_stage <= 3'(S_SKEW);
          end else if (skew_measured) begin
            stage_q          <= S_CANCEL;
            timer_q          <= '0;
            start_cancellers <= 1'b1;
          end else if (timer_q == STEP_TIMEOUT) begin
            stage_q <= S_FAILED; failed_stage <= 3'(S_SKEW);
          end
 
          S_CANCEL: if (|canceller_failed) begin
            stage_q <= S_FAILED; failed_stage <= 3'(S_CANCEL);
          end else if (&canceller_converged) begin
            // ALL FOUR. Three converged pairs and one adapting is not a
            // usable link, and admitting data now puts errors on one
            // pair that look like a cable fault on all of them.
            stage_q <= S_DATA; timer_q <= '0;
          end else if (timer_q == STEP_TIMEOUT) begin
            stage_q <= S_FAILED; failed_stage <= 3'(S_CANCEL);
          end
 
          S_DATA: ;   // steady state
 
          S_FAILED: begin
            training_failed <= 1'b1;
            if (!(&c_failures)) c_failures <= c_failures + 1'b1;
            stage_q <= S_IDLE;
            timer_q <= '0;
          end
 
          default: stage_q <= S_IDLE;
        endcase
      end
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// Per-pair health, kept because the FRAME layer's symptom cannot
// attribute a fault to a pair.
//
// 8B1Q4 places one symbol of every octet on each of the four pairs, so
// ALL FOUR are required to recover ANY octet. One degraded pair
// therefore corrupts every octet, and the frame layer sees uniform,
// total failure -- the same picture a completely dead link gives.
//
// The pair identity exists only BELOW the decoder, in the per-pair
// residual and slicer margin. If it is not captured there, it does not
// exist anywhere.
module pair_health_telemetry
  import gig_pkg::*;
#(
  parameter int unsigned MARGIN_W = 12,
  parameter int unsigned WINDOW_BITS = 20,
  parameter int unsigned CNT_W = 16,
  // A pair whose margin sits below this is degraded but decoding.
  parameter int unsigned MARGIN_FLOOR = 12'd300
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic [PAIRS-1:0]               sample_valid,
  input  logic [PAIRS-1:0][MARGIN_W-1:0] slicer_margin,
  input  logic [PAIRS-1:0]               symbol_error,
 
  output logic [PAIRS-1:0][MARGIN_W-1:0] worst_margin,
  output logic [PAIRS-1:0][CNT_W-1:0]    c_pair_errors,
  output logic [PAIRS-1:0]               pair_degraded,
 
  // The single worst pair, and whether it stands out. A link where one
  // pair is far worse than the others is a connector or a pair fault; a
  // link where all four are equally poor is the cable or the length.
  output logic [1:0] worst_pair,
  output logic       single_pair_outlier,
  output logic       window_valid,
  // Sticky, surviving clear: this pair has been degraded before.
  output logic [PAIRS-1:0] ever_degraded
);
 
  logic [WINDOW_BITS-1:0] win_q;
  integer i;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      win_q <= '0; window_valid <= 1'b0; worst_pair <= 2'd0;
      single_pair_outlier <= 1'b0; ever_degraded <= '0;
      for (i = 0; i < PAIRS; i = i + 1) begin
        worst_margin[i]  <= '1;
        c_pair_errors[i] <= '0;
        pair_degraded[i] <= 1'b0;
      end
    end else begin
      if (clear) begin
        win_q <= '0; window_valid <= 1'b0;
        for (i = 0; i < PAIRS; i = i + 1) begin
          worst_margin[i]  <= '1;
          c_pair_errors[i] <= '0;
          pair_degraded[i] <= 1'b0;
        end
        // ever_degraded is NOT cleared. A pair that has been degraded
        // stays flagged, because the next reader is investigating an
        // intermittent fault and the history is the evidence.
      end else begin
        win_q <= win_q + 1'b1;
        if (&win_q) window_valid <= 1'b1;
 
        for (i = 0; i < PAIRS; i = i + 1) begin
          if (sample_valid[i]) begin
            if (slicer_margin[i] < worst_margin[i])
              worst_margin[i] <= slicer_margin[i];
 
            if (slicer_margin[i] < MARGIN_W'(MARGIN_FLOOR)) begin
              pair_degraded[i] <= 1'b1;
              ever_degraded[i] <= 1'b1;
            end
 
            if (symbol_error[i] && !(&c_pair_errors[i]))
              c_pair_errors[i] <= c_pair_errors[i] + 1'b1;
          end
        end
      end
    end
  end
 
  // Which pair is worst, and whether it is an OUTLIER. One pair far
  // worse than the rest is a pair or connector fault; four equally poor
  // pairs is the cable, the length, or the environment.
  always_comb begin
    logic [MARGIN_W-1:0] lo, hi;
    logic [1:0] lo_idx;
    lo = '1; hi = '0; lo_idx = 2'd0;
    for (int p = 0; p < PAIRS; p = p + 1) begin
      if (worst_margin[p] < lo) begin lo = worst_margin[p]; lo_idx = 2'(p); end
      if (worst_margin[p] > hi) hi = worst_margin[p];
    end
    worst_pair          = lo_idx;
    // A factor of two between best and worst is a difference the cable
    // alone does not produce.
    single_pair_outlier = window_valid && (hi > (lo << 1));
  end
 
endmodule

// P1. Exactly one role, or an explicit conflict. There is no state in
// which the arbiter has resolved and the role is meaningless.
property p_role_is_definite;
  @(posedge clk) disable iff (!rst_n)
  role_valid |-> (role inside {ROLE_MASTER, ROLE_SLAVE,
                               ROLE_CONFLICT, ROLE_UNRESOLVED});
endproperty
a_role_is_definite: assert property (p_role_is_definite);
 
// P2. Conflict is reported exactly when it is the outcome -- so a
// supervisor can act on the flag alone.
property p_conflict_matches_role;
  @(posedge clk) disable iff (!rst_n)
  role_valid |-> (conflict == (role == ROLE_CONFLICT));
endproperty
a_conflict_matches_role: assert property (p_conflict_matches_role);
 
// P3. Both ends forced the same way NEVER produces a usable role.
// The property that keeps a two-master link from coming up.
property p_double_force_conflicts;
  @(posedge clk) disable iff (!rst_n)
  (page_valid && local_manual_force && partner_manual_force &&
   (local_prefers_master == partner_prefers_master))
    |=> (role == ROLE_CONFLICT);
endproperty
a_double_force_conflicts: assert property (p_double_force_conflicts);
 
// P4. THE HONESTY PROPERTY for this module: a seed-resolved role is
// declared as such, because it is the one that will not repeat.
property p_seed_resolution_declared;
  @(posedge clk) disable iff (!rst_n)
  (role_valid && $past(page_valid) &&
   ($past(local_manual_force) == $past(partner_manual_force)) &&
   ($past(local_is_multiport) == $past(partner_is_multiport)) &&
   ($past(local_seed) != $past(partner_seed)))
    |-> resolved_by_seed;
endproperty
a_seed_resolution_declared: assert property (p_seed_resolution_declared);

// P5. The three outcomes are mutually exclusive. A loop that is both
// converged and diverged has a control bug, not a channel problem.
property p_outcomes_exclusive;
  @(posedge clk) disable iff (!rst_n)
  $onehot0({converged, diverged, budget_expired});
endproperty
a_outcomes_exclusive: assert property (p_outcomes_exclusive);
 
// P6. Adapting and any terminal outcome are exclusive too.
property p_not_adapting_when_done;
  @(posedge clk) disable iff (!rst_n)
  (converged || diverged || budget_expired) |-> !adapting;
endproperty
a_not_adapting_when_done: assert property (p_not_adapting_when_done);
 
// P7. THE DWELL. Convergence is never declared without the residual
// having been below threshold for the full dwell -- which is what stops
// a lucky sample from being called a converged loop. A white-box
// property: dwell_q is internal, reached by bind.
property p_convergence_requires_dwell;
  @(posedge clk) disable iff (!rst_n)
  $rose(converged) |-> ($past(dwell_q) == DWELL_CYCLES) &&
                       ($past(residual) <= CONV_THRESHOLD);
endproperty
a_convergence_requires_dwell: assert property (p_convergence_requires_dwell);
 
// P8. Freeze means frozen. No outcome may change while the loop is
// held, because a frozen loop is not observing anything.
property p_freeze_holds;
  @(posedge clk) disable iff (!rst_n)
  freeze |=> $stable({converged, diverged, budget_expired});
endproperty
a_freeze_holds: assert property (p_freeze_holds);
 
// P9. Adaptation terminates. This is the property that makes "adapting"
// a bounded state rather than a place a link can disappear into.
property p_adaptation_terminates;
  @(posedge clk) disable iff (!rst_n)
  $rose(adapting) |-> ##[1:$] (converged || diverged || budget_expired);
endproperty
a_adaptation_terminates: assert property (p_adaptation_terminates);
 
// P10. Any failure is remembered. Sticky across retrains, because the
// reader of this bit is investigating something intermittent.
property p_failure_is_sticky;
  @(posedge clk) disable iff (!rst_n)
  (diverged || budget_expired) |=> ever_failed;
endproperty
a_failure_is_sticky: assert property (p_failure_is_sticky);

// P11. Skew is measured in training only. A measurement during data is
// a control loop responding to noise.
property p_skew_measured_in_training;
  @(posedge clk) disable iff (!rst_n)
  $rose(skew_measured) |-> $past(train_mode);
endproperty
a_skew_in_training: assert property (p_skew_measured_in_training);
 
// P12. Out of range is REPORTED, never clamped away. A delay request
// beyond the compensator's depth must raise the flag.
property p_skew_range_reported;
  @(posedge clk) disable iff (!rst_n)
  (skew_measured && (worst_skew_syms > SKEW_LIMIT_SYMS))
    |-> skew_out_of_range;
endproperty
a_skew_range_reported: assert property (p_skew_range_reported);
 
// P13. Delay is stable during data. The cable does not change while the
// link is up, so neither may the compensation.
property p_delays_stable_in_data;
  @(posedge clk) disable iff (!rst_n)
  data_mode |=> $stable(pair_delay_syms);
endproperty
a_delays_stable: assert property (p_delays_stable_in_data);
 
// P14. THE ORDERING PROPERTY. Data mode requires ALL FOUR cancellers
// converged -- not three, not a majority. 8B1Q4 needs every pair.
property p_data_needs_all_pairs;
  @(posedge clk) disable iff (!rst_n)
  data_mode |-> (&canceller_converged);
endproperty
a_data_needs_all_pairs: assert property (p_data_needs_all_pairs);
 
// P15. And it requires the timing lock and the skew measurement that
// every canceller's convergence was conditioned on.
property p_data_needs_prerequisites;
  @(posedge clk) disable iff (!rst_n)
  data_mode |-> (timing_locked && skew_measured && !skew_out_of_range);
endproperty
a_data_needs_prereqs: assert property (p_data_needs_prerequisites);
 
// P16. A link drop returns to idle from ANY stage. There is no partial
// resume: every measurement depended on a clock that has gone.
property p_drop_restarts;
  @(posedge clk) disable iff (!rst_n)
  (!link_signal_present && (stage != S_IDLE)) |=> (stage == S_IDLE);
endproperty
a_drop_restarts: assert property (p_drop_restarts);
 
// P17. Failure names its stage. training_failed with a stale
// failed_stage sends an engineer to the wrong subsystem.
property p_failure_names_stage;
  @(posedge clk) disable iff (!rst_n)
  training_failed |-> (failed_stage inside {3'(S_ROLE), 3'(S_TIMING),
                                            3'(S_SKEW), 3'(S_CANCEL)});
endproperty
a_failure_names_stage: assert property (p_failure_names_stage);