Link Discovery — FLP Bursts and Parallel Detection

// SYNTHESIZABLE.
//
// Transmits a fast link pulse burst.
//
// THE STRUCTURE:
//   33 positions = 17 clock + 16 data
//   clock-to-clock : 125 us (+/- 14 us tolerated by the receiver)
//   clock-to-data  : 62.5 us (+/- 7 us)
//   burst duration : 16 x 125 us = 2 ms
//   burst-to-burst : 8 to 16 ms, inside 10BASE-T's 16 +/- 8 ms window
//   pulse width    : ~100 ns
//
// A ONE IS A PULSE AND A ZERO IS NOTHING. So this module emits between
// 17 and 33 pulses depending on the link code word, and a word of all
// zeros produces a burst that is indistinguishable, position by
// position, from 17 clock pulses -- which is exactly what it is.
package discovery_pkg;
 
  localparam int unsigned FLP_POSITIONS   = 33;
  localparam int unsigned FLP_CLOCK_PULSES = 17;
  localparam int unsigned FLP_DATA_BITS   = 16;
 
  // Timing, in microseconds. A receiver's windows are wider than a
  // transmitter's nominal values, which is the usual asymmetry: send
  // precisely, accept generously.
  localparam int unsigned CLK_SPACING_US   = 125;
  localparam int unsigned CLK_TOL_US       = 14;
  localparam int unsigned DATA_OFFSET_US   = 62;    // 62.5, truncated
  localparam int unsigned DATA_TOL_US      = 7;
  // A pulse later than this after a clock pulse is not a data pulse.
  localparam int unsigned DATA_DETECT_MAX_US = 100;
 
  localparam int unsigned BURST_MIN_MS = 8;
  localparam int unsigned BURST_MAX_MS = 16;
 
  // 10BASE-T link integrity: lc_max, the number of consecutive link
  // pulses required to declare the link up, is between 2 and 10.
  localparam int unsigned LC_MIN = 2;
  localparam int unsigned LC_MAX = 10;
 
  typedef enum logic [2:0] {
    SIG_NONE,          // nothing on the wire
    SIG_LINK_PULSE,    // single pulses at ~16 ms: 10BASE-T
    SIG_FLP_BURST,     // 33-position bursts: autonegotiation
    SIG_IDLE_SYMBOLS,  // continuous: 100BASE-TX, no negotiation
    SIG_AMBIGUOUS      // activity that fits none of the above
  } signalling_e;
 
endpackage
 
module flp_burst_transmitter
  import discovery_pkg::*;
#(
  parameter int unsigned CLK_MHZ = 25,
  parameter int unsigned CNT_W   = 20
) (
  input  logic clk,
  input  logic rst_n,
 
  input  logic        enable,
  input  logic [15:0] link_code_word,
  // Randomised burst spacing within the legal window, so two devices
  // powering up together do not lock into a repeating phase relation.
  input  logic [2:0]  spacing_jitter_ms,
 
  output logic        pulse,
  output logic        burst_active,
  output logic [5:0]  position,        // 0..32
  output logic        burst_complete,
 
  output logic [CNT_W-1:0] c_bursts,
  output logic [CNT_W-1:0] c_pulses,
  // Pulses emitted in the last burst. Between 17 (all-zero word) and
  // 33 (all-ones), and exported because it is a free check that the
  // word being advertised is the word intended.
  output logic [5:0]       pulses_last_burst
);
 
  localparam int unsigned TICKS_PER_US = CLK_MHZ;
  // Half a clock-to-clock interval: the data position sits here.
  localparam int unsigned HALF_TICKS  = (CLK_SPACING_US * CLK_MHZ) / 2;
  localparam int unsigned FULL_TICKS  = CLK_SPACING_US * CLK_MHZ;
  localparam int unsigned PULSE_TICKS = (100 * CLK_MHZ) / 1000;   // ~100 ns
 
  logic [15:0] tick_q;
  logic [5:0]  pos_q;
  logic [5:0]  pulses_q;
  logic [31:0] gap_q;
  logic        in_burst_q;
 
  assign position     = pos_q;
  assign burst_active = in_burst_q;
 
  // A position is a CLOCK position when even, a DATA position when odd:
  //   0 clk, 1 data, 2 clk, 3 data, ... 32 clk
  // which gives 17 clock and 16 data, and brackets every data bit.
  wire is_clock_position = !pos_q[0];
  wire [3:0] data_index  = pos_q[4:1];
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      tick_q <= '0; pos_q <= 6'd0; pulses_q <= 6'd0; gap_q <= '0;
      in_burst_q <= 1'b0; pulse <= 1'b0; burst_complete <= 1'b0;
      c_bursts <= '0; c_pulses <= '0; pulses_last_burst <= 6'd0;
    end else begin
      pulse          <= 1'b0;
      burst_complete <= 1'b0;
 
      if (!enable) begin
        in_burst_q <= 1'b0;
        gap_q      <= '0;
 
      end else if (in_burst_q) begin
        if (tick_q < 16'(PULSE_TICKS)) begin
          // THE PULSE. A clock position always pulses; a data position
          // pulses only for a one -- and emits NOTHING for a zero,
          // which is the encoding this whole chapter is about.
          if (is_clock_position || link_code_word[data_index]) begin
            pulse <= 1'b1;
            if (tick_q == 16'd0) begin
              pulses_q <= pulses_q + 6'd1;
              if (!(&c_pulses)) c_pulses <= c_pulses + 1'b1;
            end
          end
        end
 
        // Clock positions are a full interval apart; the data position
        // between them sits at half.
        if (tick_q == 16'(HALF_TICKS - 1)) begin
          tick_q <= '0;
          if (pos_q == 6'(FLP_POSITIONS - 1)) begin
            in_burst_q        <= 1'b0;
            burst_complete    <= 1'b1;
            pulses_last_burst <= pulses_q;
            pos_q             <= 6'd0;
            gap_q             <= '0;
            if (!(&c_bursts)) c_bursts <= c_bursts + 1'b1;
          end else begin
            pos_q <= pos_q + 6'd1;
          end
        end else begin
          tick_q <= tick_q + 16'd1;
        end
 
      end else begin
        // BETWEEN BURSTS. The spacing is randomised inside the legal
        // window so that two devices powering up together do not settle
        // into a repeating phase relationship in which one always
        // transmits while the other is blind.
        if (gap_q == 32'((BURST_MIN_MS + 0) * 1000 * CLK_MHZ) +
                     32'(spacing_jitter_ms) * 32'(1000 * CLK_MHZ)) begin
          in_burst_q <= 1'b1;
          pos_q      <= 6'd0;
          tick_q     <= '0;
          pulses_q   <= 6'd0;
        end else begin
          gap_q <= gap_q + 1'b1;
        end
      end
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// Receives an FLP burst and reports, per position, both the decoded bit
// AND the evidence behind it.
//
// THE ASYMMETRY THIS MODULE EXISTS FOR:
//   a ONE  is a pulse that ARRIVED -- positive evidence
//   a ZERO is a pulse that DID NOT -- and an absence has three causes:
//        the partner sent a zero,
//        the partner sent a one and it was lost,
//        the partner stopped transmitting.
//   All three decode identically.
//
// WHAT DISAMBIGUATES THEM is the CLOCK pulses. Sixteen data bits sit
// between SEVENTEEN clock pulses, so every data position is bracketed.
// If both bracketing clock pulses arrived, the medium was carrying
// pulses and this receiver was detecting them during the interval --
// so a missing data pulse was NOT SENT rather than lost.
//
// Which is why this module exports a per-bit CONFIDENCE alongside the
// decoded word, and why Section 15's rejected property is what happens
// when a design exports only the word.
module flp_burst_receiver
  import discovery_pkg::*;
#(
  parameter int unsigned CLK_MHZ = 25,
  parameter int unsigned CNT_W   = 20
) (
  input  logic clk,
  input  logic rst_n,
 
  input  logic pulse_in,          // a detected pulse, one cycle wide
 
  output logic [15:0] link_code_word,
  // Bit n set = the bit at position n was bracketed by two clock pulses
  // that both arrived within tolerance. Only those bits are believable.
  output logic [15:0] bit_confidence,
  output logic        word_valid,
  // TRUE only when EVERY bit was bracketed. A word with any low
  // confidence bit is not a word; it is a guess with a shape.
  output logic        word_fully_bracketed,
 
  output logic [5:0]  clock_pulses_seen,
  output logic [5:0]  data_pulses_seen,
  output logic [15:0] worst_clock_interval_us,
 
  // A clock pulse outside the 111..139 us window. The burst's timing
  // reference is broken from here on, because every later position is
  // measured from it.
  output logic        clock_interval_violation,
  // A pulse later than data_detect_max after its clock pulse. Not a
  // data pulse -- it is the next clock pulse arriving early, and
  // treating it as data shifts every subsequent bit.
  output logic        late_pulse_seen,
 
  output logic [CNT_W-1:0] c_bursts_decoded,
  output logic [CNT_W-1:0] c_bursts_discarded,
  output logic             ever_partial_burst
);
 
  localparam int unsigned TICKS_PER_US = CLK_MHZ;
  localparam int unsigned CLK_MIN_T = (CLK_SPACING_US - CLK_TOL_US) * CLK_MHZ;
  localparam int unsigned CLK_MAX_T = (CLK_SPACING_US + CLK_TOL_US) * CLK_MHZ;
  localparam int unsigned DAT_MIN_T = (DATA_OFFSET_US - DATA_TOL_US) * CLK_MHZ;
  localparam int unsigned DAT_MAX_T = (DATA_OFFSET_US + DATA_TOL_US) * CLK_MHZ;
  localparam int unsigned DET_MAX_T = DATA_DETECT_MAX_US * CLK_MHZ;
  // No pulse for this long ends the burst.
  localparam int unsigned BURST_END_T = 300 * CLK_MHZ;
 
  logic [15:0] since_pulse_q;
  logic [3:0]  bit_index_q;
  logic        in_burst_q;
  logic        saw_data_q;       // a data pulse since the last clock
  logic        prev_clock_ok_q;  // the clock pulse before this bit was good
  logic [15:0] word_q;
  logic [15:0] conf_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      since_pulse_q <= '0; bit_index_q <= 4'd0; in_burst_q <= 1'b0;
      saw_data_q <= 1'b0; prev_clock_ok_q <= 1'b0;
      word_q <= 16'd0; conf_q <= 16'd0;
      link_code_word <= 16'd0; bit_confidence <= 16'd0;
      word_valid <= 1'b0; word_fully_bracketed <= 1'b0;
      clock_pulses_seen <= 6'd0; data_pulses_seen <= 6'd0;
      worst_clock_interval_us <= 16'd0;
      clock_interval_violation <= 1'b0; late_pulse_seen <= 1'b0;
      c_bursts_decoded <= '0; c_bursts_discarded <= '0;
      ever_partial_burst <= 1'b0;
    end else begin
      word_valid               <= 1'b0;
      clock_interval_violation <= 1'b0;
      late_pulse_seen          <= 1'b0;
 
      if (pulse_in) begin
        if (!in_burst_q) begin
          // FIRST PULSE of a burst. It is a clock pulse by definition,
          // and it is the reference everything after is measured from.
          in_burst_q        <= 1'b1;
          bit_index_q       <= 4'd0;
          word_q            <= 16'd0;
          conf_q            <= 16'd0;
          saw_data_q        <= 1'b0;
          prev_clock_ok_q   <= 1'b1;
          clock_pulses_seen <= 6'd1;
          data_pulses_seen  <= 6'd0;
 
        end else if ((since_pulse_q >= 16'(DAT_MIN_T)) &&
                     (since_pulse_q <= 16'(DAT_MAX_T))) begin
          // A DATA PULSE: inside the 55.5..69.5 us window.
          saw_data_q       <= 1'b1;
          data_pulses_seen <= data_pulses_seen + 6'd1;
 
        end else if ((since_pulse_q >= 16'(CLK_MIN_T)) &&
                     (since_pulse_q <= 16'(CLK_MAX_T))) begin
          // A CLOCK PULSE. It closes the data position that preceded
          // it, and its arrival is HALF the evidence for that bit.
          clock_pulses_seen <= clock_pulses_seen + 6'd1;
 
          word_q[bit_index_q] <= saw_data_q;
          // CONFIDENCE. The bit is believable only if the clock pulse
          // BEFORE it was good AND this one is -- which is exactly the
          // bracketing the 17-for-16 ratio provides.
          conf_q[bit_index_q] <= prev_clock_ok_q;
 
          if (since_pulse_q[15:0] > worst_clock_interval_us)
            worst_clock_interval_us <= since_pulse_q;
 
          prev_clock_ok_q <= 1'b1;
          saw_data_q      <= 1'b0;
          bit_index_q     <= bit_index_q + 4'd1;
 
        end else if (since_pulse_q > 16'(DET_MAX_T)) begin
          // A pulse beyond data_detect_max but outside the clock
          // window. The timing reference is broken; every bit after
          // this one is measured from a position that is not where the
          // transmitter put it.
          late_pulse_seen          <= 1'b1;
          clock_interval_violation <= 1'b1;
          prev_clock_ok_q          <= 1'b0;
          saw_data_q               <= 1'b0;
          bit_index_q              <= bit_index_q + 4'd1;
 
        end else begin
          // Too early to be anything legal.
          clock_interval_violation <= 1'b1;
          prev_clock_ok_q          <= 1'b0;
        end
 
        since_pulse_q <= '0;
 
      end else if (in_burst_q) begin
        if (since_pulse_q == 16'(BURST_END_T)) begin
          // THE BURST ENDED. A full burst has 17 clock pulses; anything
          // fewer means positions were lost, and the word is published
          // WITH its confidence rather than withheld -- because a
          // partially-bracketed word is still evidence, and Section 9's
          // classifier needs it.
          in_burst_q     <= 1'b0;
          link_code_word <= word_q;
          bit_confidence <= conf_q;
          word_valid     <= 1'b1;
          word_fully_bracketed <= (conf_q == 16'hFFFF) &&
                                  (clock_pulses_seen == 6'(FLP_CLOCK_PULSES));
 
          if ((conf_q == 16'hFFFF) &&
              (clock_pulses_seen == 6'(FLP_CLOCK_PULSES))) begin
            if (!(&c_bursts_decoded)) c_bursts_decoded <= c_bursts_decoded + 1'b1;
          end else begin
            ever_partial_burst <= 1'b1;
            if (!(&c_bursts_discarded))
              c_bursts_discarded <= c_bursts_discarded + 1'b1;
          end
        end else begin
          since_pulse_q <= since_pulse_q + 16'd1;
        end
 
      end else begin
        if (since_pulse_q != 16'hFFFF) since_pulse_q <= since_pulse_q + 16'd1;
      end
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// Classifies the signalling on the wire into one of four cases, which
// is the first decision in the entire link bring-up and the one every
// later step depends on.
//
// THE FOUR CASES AND THEIR SIGNATURES:
//   SIG_FLP_BURST    -- groups of pulses 125 us apart, groups repeating
//                       every 8..16 ms. The fine structure is what
//                       distinguishes it from the next case.
//   SIG_LINK_PULSE   -- SINGLE pulses roughly every 16 ms, with no
//                       125 us structure inside. A 10BASE-T partner.
//   SIG_IDLE_SYMBOLS -- continuous activity with no pulse structure at
//                       all. A 100BASE-TX partner with negotiation off.
//   SIG_NONE         -- nothing.
//
// THE HAZARD: the first two repeat at overlapping rates, deliberately,
// because that is what makes FLP backward compatible. So they can ONLY
// be told apart by the MICROSECOND structure inside a burst, and a
// classifier that measures only the millisecond rate cannot separate
// them at all.
module signalling_classifier
  import discovery_pkg::*;
#(
  parameter int unsigned CLK_MHZ = 25,
  parameter int unsigned CNT_W   = 20,
  // Bursts or pulses observed before the classification is believed.
  parameter int unsigned CONFIRM = 3
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic pulse_in,
  input  logic activity_in,        // continuous energy, not pulses
 
  output signalling_e  classification,
  output logic         classification_valid,
  output logic         classification_changed,
 
  // The measurements the classification rests on, exported so a human
  // can see WHY the design decided what it decided.
  output logic [15:0]  last_intra_group_us,
  output logic [15:0]  last_inter_group_ms,
  output logic [5:0]   last_group_size,
 
  output logic [CNT_W-1:0] c_groups,
  output logic [CNT_W-1:0] c_classifications,
  // Activity that fits none of the four signatures. Reported rather
  // than forced into the nearest one -- a partner doing something
  // undefined is information, and rounding it away loses it.
  output logic             ambiguous_signalling,
  output logic [CNT_W-1:0] c_ambiguous
);
 
  localparam int unsigned INTRA_MIN_T = (CLK_SPACING_US - CLK_TOL_US) * CLK_MHZ;
  localparam int unsigned INTRA_MAX_T = (CLK_SPACING_US + CLK_TOL_US) * CLK_MHZ;
  localparam int unsigned GROUP_END_T = 300 * CLK_MHZ;
  localparam int unsigned MS_TICKS    = 1000 * CLK_MHZ;
 
  logic [31:0]  since_pulse_q;
  logic [31:0]  since_group_q;
  logic [5:0]   group_size_q;
  logic         in_group_q;
  logic [3:0]   confirm_q;
  signalling_e  candidate_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      since_pulse_q <= '0; since_group_q <= '0; group_size_q <= 6'd0;
      in_group_q <= 1'b0; confirm_q <= 4'd0; candidate_q <= SIG_NONE;
      classification <= SIG_NONE; classification_valid <= 1'b0;
      classification_changed <= 1'b0;
      last_intra_group_us <= 16'd0; last_inter_group_ms <= 16'd0;
      last_group_size <= 6'd0;
      c_groups <= '0; c_classifications <= '0;
      ambiguous_signalling <= 1'b0; c_ambiguous <= '0;
    end else if (clear) begin
      c_groups <= '0; c_classifications <= '0; c_ambiguous <= '0;
      classification_changed <= 1'b0;
    end else begin
      classification_changed <= 1'b0;
      ambiguous_signalling   <= 1'b0;
 
      if (pulse_in) begin
        if (!in_group_q) begin
          in_group_q          <= 1'b1;
          group_size_q        <= 6'd1;
          last_inter_group_ms <= 16'(since_group_q / 32'(MS_TICKS));
          since_group_q       <= '0;
        end else begin
          group_size_q <= group_size_q + 6'd1;
          // THE INTRA-GROUP MEASUREMENT. This is what separates a burst
          // from a link pulse, and a classifier that omits it cannot.
          last_intra_group_us <= 16'(since_pulse_q / 32'(CLK_MHZ));
        end
        since_pulse_q <= '0;
 
      end else begin
        if (since_pulse_q != 32'hFFFF_FFFF) since_pulse_q <= since_pulse_q + 1'b1;
        if (since_group_q != 32'hFFFF_FFFF) since_group_q <= since_group_q + 1'b1;
 
        if (in_group_q && (since_pulse_q == 32'(GROUP_END_T))) begin
          // A GROUP ENDED. Classify it from its SIZE and its internal
          // spacing, not from its repetition rate -- the repetition
          // rates of the two cases deliberately overlap.
          in_group_q      <= 1'b0;
          last_group_size <= group_size_q;
          if (!(&c_groups)) c_groups <= c_groups + 1'b1;
 
          if ((group_size_q >= 6'd17) &&
              (last_intra_group_us >= 16'(CLK_SPACING_US - CLK_TOL_US)) &&
              (last_intra_group_us <= 16'(CLK_SPACING_US + CLK_TOL_US))) begin
            // 17 or more pulses at 125 us spacing: an FLP burst.
            if (candidate_q == SIG_FLP_BURST) begin
              if (confirm_q != 4'(CONFIRM)) confirm_q <= confirm_q + 4'd1;
            end else begin
              candidate_q <= SIG_FLP_BURST;
              confirm_q   <= 4'd1;
            end
 
          end else if (group_size_q == 6'd1) begin
            // A SINGLE pulse: 10BASE-T link integrity.
            if (candidate_q == SIG_LINK_PULSE) begin
              if (confirm_q != 4'(CONFIRM)) confirm_q <= confirm_q + 4'd1;
            end else begin
              candidate_q <= SIG_LINK_PULSE;
              confirm_q   <= 4'd1;
            end
 
          end else begin
            // Pulses, but neither one nor a well-formed burst. NOT
            // rounded to the nearest case -- a partner doing something
            // undefined is information.
            ambiguous_signalling <= 1'b1;
            candidate_q          <= SIG_AMBIGUOUS;
            confirm_q            <= 4'd0;
            if (!(&c_ambiguous)) c_ambiguous <= c_ambiguous + 1'b1;
          end
        end
 
        // Continuous activity with no pulse structure at all.
        if (activity_in && !in_group_q && (since_pulse_q > 32'(GROUP_END_T))) begin
          if (candidate_q == SIG_IDLE_SYMBOLS) begin
            if (confirm_q != 4'(CONFIRM)) confirm_q <= confirm_q + 4'd1;
          end else begin
            candidate_q <= SIG_IDLE_SYMBOLS;
            confirm_q   <= 4'd1;
          end
        end
      end
 
      if ((confirm_q == 4'(CONFIRM)) && (classification != candidate_q)) begin
        classification         <= candidate_q;
        classification_valid   <= 1'b1;
        classification_changed <= 1'b1;
        if (!(&c_classifications)) c_classifications <= c_classifications + 1'b1;
      end
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// Parallel detection: determine what a NON-NEGOTIATING partner is, from
// its signalling alone -- and keep what was MEASURED strictly separate
// from what was ASSUMED.
//
// Chapter 9.2 §9 introduced this module's ancestor. What that chapter
// established, and this one implements more carefully, is that the two
// outputs have completely different epistemic status:
//
//   SPEED  is MEASURED. Link pulses and idle symbols are entirely
//        different signals and distinguishing them takes no protocol.
//   DUPLEX is ASSUMED. Nothing in either signalling says how a partner
//        intends to behave WHEN IT TRANSMITS, and an idle link exhibits
//        none of that behaviour.
//
// So this module carries a per-field provenance, not a single validity
// bit -- because a design that reports one result cannot distinguish a
// measurement from a default, and Chapter 9.2's duplex mismatch is
// exactly what that costs.
module parallel_detection_fsm
  import discovery_pkg::*;
#(
  parameter int unsigned CLK_MHZ = 25,
  // How long a non-negotiating signalling must persist before parallel
  // detection is used. Long enough that a slow negotiator is not
  // misjudged as a device that cannot negotiate.
  parameter int unsigned DETECT_MS = 500,
  parameter int unsigned CNT_W = 20
) (
  input  logic clk,
  input  logic rst_n,
 
  input  signalling_e classification,
  input  logic        classification_valid,
 
  output logic       detection_valid,
  output logic [1:0] detected_speed,       // 0 = 10, 1 = 100
  output logic       detected_duplex,      // always half
 
  // THE PROVENANCE. Two bits, one per field, and they are never equal
  // on a parallel-detected link.
  output logic       speed_is_measured,
  output logic       duplex_is_assumed,
 
  output logic       partner_negotiates,
  output logic [15:0] detect_elapsed_ms,
 
  output logic [CNT_W-1:0] c_detections,
  // Sticky. A port that has EVER parallel detected is a port whose
  // duplex was never agreed, and that stays true after the link
  // bounces and comes back looking new.
  output logic             ever_parallel_detected,
  // The classification changed while the detection timer was running.
  // Reported, because it usually means the partner was mid-reset and
  // the detection would have been made about a transient.
  output logic             detection_aborted,
  output logic [CNT_W-1:0] c_aborts
);
 
  localparam int unsigned MS_TICKS = 1000 * CLK_MHZ;
 
  logic [31:0]  tick_q;
  logic [15:0]  ms_q;
  logic         timing_q;
  signalling_e  timing_class_q;
 
  assign detect_elapsed_ms = ms_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      tick_q <= '0; ms_q <= 16'd0; timing_q <= 1'b0;
      timing_class_q <= SIG_NONE;
      detection_valid <= 1'b0; detected_speed <= 2'd0;
      detected_duplex <= 1'b0;
      speed_is_measured <= 1'b0; duplex_is_assumed <= 1'b0;
      partner_negotiates <= 1'b0;
      c_detections <= '0; ever_parallel_detected <= 1'b0;
      detection_aborted <= 1'b0; c_aborts <= '0;
    end else begin
      detection_valid   <= 1'b0;
      detection_aborted <= 1'b0;
 
      if (classification_valid && (classification == SIG_FLP_BURST)) begin
        // The partner negotiates. Parallel detection is not used, and
        // duplex will be AGREED rather than assumed.
        partner_negotiates <= 1'b1;
        duplex_is_assumed  <= 1'b0;
        speed_is_measured  <= 1'b0;
        timing_q           <= 1'b0;
        ms_q               <= 16'd0;
 
      end else if ((classification == SIG_LINK_PULSE) ||
                   (classification == SIG_IDLE_SYMBOLS)) begin
        partner_negotiates <= 1'b0;
 
        if (!timing_q) begin
          timing_q       <= 1'b1;
          timing_class_q <= classification;
          ms_q           <= 16'd0;
          tick_q         <= '0;
 
        end else if (classification != timing_class_q) begin
          // THE CLASSIFICATION CHANGED mid-timer. Usually a partner
          // that was mid-reset; making a detection about a transient
          // is how a working device gets classified as a legacy one.
          detection_aborted <= 1'b1;
          timing_q          <= 1'b0;
          ms_q              <= 16'd0;
          if (!(&c_aborts)) c_aborts <= c_aborts + 1'b1;
 
        end else if (ms_q == 16'(DETECT_MS)) begin
          detection_valid <= 1'b1;
          // SPEED: measured. The two signallings are entirely different
          // and telling them apart requires no protocol at all.
          detected_speed    <= (classification == SIG_IDLE_SYMBOLS) ? 2'd1 : 2'd0;
          speed_is_measured <= 1'b1;
          // DUPLEX: assumed, and HALF, because duplex is unobservable
          // and half is the choice that is safe against a partner that
          // might collide.
          detected_duplex   <= 1'b0;
          duplex_is_assumed <= 1'b1;
 
          ever_parallel_detected <= 1'b1;
          timing_q               <= 1'b0;
          ms_q                   <= 16'd0;
          if (!(&c_detections)) c_detections <= c_detections + 1'b1;
 
        end else begin
          if (tick_q == 32'(MS_TICKS - 1)) begin
            tick_q <= '0;
            ms_q   <= ms_q + 16'd1;
          end else begin
            tick_q <= tick_q + 1'b1;
          end
        end
 
      end else begin
        // Nothing, or ambiguous. Stop timing; do not detect about it.
        if (timing_q) begin
          detection_aborted <= 1'b1;
          if (!(&c_aborts)) c_aborts <= c_aborts + 1'b1;
        end
        timing_q <= 1'b0;
        ms_q     <= 16'd0;
      end
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// Sequences and bounds link discovery, so that every path through it
// terminates in a named outcome rather than in waiting.
//
// THE ORDERING, which cannot be rearranged:
//   1. observe        -- is there anything on the wire at all?
//   2. classify       -- which of the four signallings is it?
//   3a. if FLP        -- decode bursts, hand the word to Chapter 11.2
//   3b. if not FLP    -- run the parallel-detection timer
//   4. bounded failure -- if none of the above resolves, restart
//
// AND EVERY STEP HAS A TIMER, because every step can hang. Clause 28
// names several -- break_link_timer, link_fail_inhibit_timer,
// autoneg_wait_timer -- and their common purpose is that no state is
// entered which the design cannot leave.
module discovery_retry_sequencer
  import discovery_pkg::*;
#(
  parameter int unsigned CLK_MHZ         = 25,
  parameter int unsigned OBSERVE_MS      = 100,
  parameter int unsigned CLASSIFY_MS     = 200,
  parameter int unsigned DECODE_MS       = 300,
  parameter int unsigned BREAK_LINK_MS   = 1500,
  parameter int unsigned MAX_ATTEMPTS    = 8,
  parameter int unsigned CNT_W = 20
) (
  input  logic clk,
  input  logic rst_n,
 
  input  logic        restart,
  input  logic        activity_seen,
  input  signalling_e classification,
  input  logic        classification_valid,
  input  logic        word_valid,
  input  logic        word_fully_bracketed,
  input  logic        detection_valid,
 
  output logic [2:0]  stage,
  output logic        abilities_available,
  output logic        detection_used,
  output logic        discovery_failed,
  output logic [2:0]  failed_stage,
 
  // Time from the first activity to a usable result. A margin
  // measurement: a link that consistently takes most of its budget is
  // a link one disturbance from failing.
  output logic [15:0]      last_discovery_ms,
  output logic [15:0]      worst_discovery_ms,
 
  output logic [CNT_W-1:0] c_attempts,
  output logic [CNT_W-1:0] c_successes,
  output logic [CNT_W-1:0] c_failures,
  output logic [3:0]       attempts_this_link,
  output logic             ever_failed
);
 
  typedef enum logic [2:0] {
    D_IDLE, D_OBSERVE, D_CLASSIFY, D_DECODE, D_DETECT, D_DONE, D_FAILED
  } dstage_e;
 
  localparam int unsigned MS_TICKS = 1000 * CLK_MHZ;
 
  dstage_e     st_q;
  logic [31:0] tick_q;
  logic [15:0] ms_q;
  logic [15:0] total_ms_q;
 
  assign stage = st_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      st_q <= D_IDLE; tick_q <= '0; ms_q <= 16'd0; total_ms_q <= 16'd0;
      abilities_available <= 1'b0; detection_used <= 1'b0;
      discovery_failed <= 1'b0; failed_stage <= 3'(D_IDLE);
      last_discovery_ms <= 16'd0; worst_discovery_ms <= 16'd0;
      c_attempts <= '0; c_successes <= '0; c_failures <= '0;
      attempts_this_link <= 4'd0; ever_failed <= 1'b0;
    end else begin
      discovery_failed <= 1'b0;
 
      // A free-running millisecond tick shared by every stage timer.
      if (tick_q == 32'(MS_TICKS - 1)) begin
        tick_q <= '0;
        if (ms_q != 16'hFFFF)       ms_q       <= ms_q + 16'd1;
        if (total_ms_q != 16'hFFFF) total_ms_q <= total_ms_q + 16'd1;
      end else begin
        tick_q <= tick_q + 1'b1;
      end
 
      if (restart) begin
        st_q <= D_OBSERVE; ms_q <= 16'd0; total_ms_q <= 16'd0;
        abilities_available <= 1'b0; detection_used <= 1'b0;
        attempts_this_link  <= 4'd0;
        if (!(&c_attempts)) c_attempts <= c_attempts + 1'b1;
      end else begin
        unique case (st_q)
          D_IDLE: if (activity_seen) begin
            st_q <= D_OBSERVE; ms_q <= 16'd0; total_ms_q <= 16'd0;
            if (!(&c_attempts)) c_attempts <= c_attempts + 1'b1;
          end
 
          D_OBSERVE: if (!activity_seen && (ms_q == 16'(OBSERVE_MS))) begin
            // Activity stopped before anything could be classified.
            // Back to idle rather than onward -- there is nothing to
            // classify and waiting longer changes nothing.
            st_q <= D_IDLE;
          end else if (classification_valid) begin
            st_q <= D_CLASSIFY; ms_q <= 16'd0;
          end else if (ms_q == 16'(OBSERVE_MS)) begin
            st_q <= D_CLASSIFY; ms_q <= 16'd0;
          end
 
          D_CLASSIFY: begin
            if (classification == SIG_FLP_BURST) begin
              st_q <= D_DECODE; ms_q <= 16'd0;
            end else if ((classification == SIG_LINK_PULSE) ||
                         (classification == SIG_IDLE_SYMBOLS)) begin
              st_q <= D_DETECT; ms_q <= 16'd0;
            end else if (ms_q == 16'(CLASSIFY_MS)) begin
              st_q         <= D_FAILED;
              failed_stage <= 3'(D_CLASSIFY);
            end
          end
 
          D_DECODE: begin
            // A word is only useful if every bit was bracketed. A
            // partially-bracketed word is a guess with a shape, and
            // acting on it advertises abilities the partner may not
            // have claimed.
            if (word_valid && word_fully_bracketed) begin
              st_q                <= D_DONE;
              abilities_available <= 1'b1;
            end else if (classification != SIG_FLP_BURST) begin
              // The partner stopped bursting. Re-classify rather than
              // keep decoding something that is no longer there.
              st_q <= D_CLASSIFY; ms_q <= 16'd0;
            end else if (ms_q == 16'(DECODE_MS)) begin
              st_q         <= D_FAILED;
              failed_stage <= 3'(D_DECODE);
            end
          end
 
          D_DETECT: begin
            if (detection_valid) begin
              st_q           <= D_DONE;
              detection_used <= 1'b1;
            end else if (classification == SIG_FLP_BURST) begin
              // The partner started negotiating after all. Abandon the
              // detection -- a negotiated result always beats a
              // detected one, because it includes duplex.
              st_q <= D_DECODE; ms_q <= 16'd0;
            end else if (ms_q == 16'(BREAK_LINK_MS)) begin
              st_q         <= D_FAILED;
              failed_stage <= 3'(D_DETECT);
            end
          end
 
          D_DONE: begin
            last_discovery_ms <= total_ms_q;
            if (total_ms_q > worst_discovery_ms)
              worst_discovery_ms <= total_ms_q;
            if (!(&c_successes)) c_successes <= c_successes + 1'b1;
            if (!activity_seen) st_q <= D_IDLE;
          end
 
          D_FAILED: begin
            discovery_failed <= 1'b1;
            ever_failed      <= 1'b1;
            if (!(&c_failures)) c_failures <= c_failures + 1'b1;
            if (attempts_this_link != 4'(MAX_ATTEMPTS))
              attempts_this_link <= attempts_this_link + 4'd1;
            st_q <= D_IDLE;
            ms_q <= 16'd0;
          end
 
          default: st_q <= D_IDLE;
        endcase
      end
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// The 10BASE-T link integrity test: declare a link up after a run of
// consecutive link pulses, and drop it after a period of silence.
//
// WHY IT IS STILL HERE. Chapter 9.1 §9 built it, and it never went
// away -- because the FLP burst was deliberately designed to satisfy
// it. A negotiating partner's bursts arrive inside the same 16 +/- 8 ms
// window as link pulses, so this mechanism brings a link up against a
// partner speaking a protocol it has never heard of.
//
// THE CONSTANT WORTH KNOWING: lc_max, the number of consecutive pulses
// required, is between 2 and 10. At the 16 +/- 8 ms pulse period that
// is between:
//   2 pulses  ->  32 ms nominal,  48 ms worst case
//   10 pulses -> 160 ms nominal, 240 ms worst case
// A design at the low end comes up fast and is more easily fooled by
// noise; one at the high end is robust and slow. Neither is wrong, and
// exporting which was chosen is what lets two devices' behaviour be
// compared.
module link_integrity_monitor
  import discovery_pkg::*;
#(
  parameter int unsigned CLK_MHZ  = 25,
  parameter int unsigned LC_COUNT = 4,     // between LC_MIN and LC_MAX
  parameter int unsigned LINK_LOSS_MS = 150,
  parameter int unsigned CNT_W = 20
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic pulse_in,
  input  logic frame_activity,      // a received frame also proves life
 
  output logic       link_up,
  output logic       link_came_up,
  output logic       link_went_down,
 
  // The consecutive-pulse run currently held, and the worst gap ever
  // observed while up. The second is the margin: a link whose worst
  // silence approaches the loss timer will drop on the next
  // disturbance, and nothing else says so.
  output logic [3:0]  pulse_run,
  output logic [15:0] worst_silence_ms,
  output logic [15:0] loss_threshold_ms,
  // The configured lc_max, exported so two devices can be compared.
  output logic [3:0]  lc_configured,
 
  output logic [CNT_W-1:0] c_link_ups,
  output logic [CNT_W-1:0] c_link_downs,
  output logic             ever_link_down,
  // A pulse arriving sooner than the minimum period. Not a link pulse
  // -- it is noise, or a burst this monitor is not structured to see.
  output logic             early_pulse
);
 
  localparam int unsigned MS_TICKS  = 1000 * CLK_MHZ;
  // A link pulse cannot arrive sooner than this after the previous one.
  localparam int unsigned MIN_GAP_MS = 5;
 
  logic [31:0] tick_q;
  logic [15:0] ms_q;
  logic [3:0]  run_q;
 
  assign pulse_run         = run_q;
  assign loss_threshold_ms = 16'(LINK_LOSS_MS);
  assign lc_configured     = 4'(LC_COUNT);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      tick_q <= '0; ms_q <= 16'd0; run_q <= 4'd0;
      link_up <= 1'b0; link_came_up <= 1'b0; link_went_down <= 1'b0;
      worst_silence_ms <= 16'd0;
      c_link_ups <= '0; c_link_downs <= '0; ever_link_down <= 1'b0;
      early_pulse <= 1'b0;
    end else begin
      link_came_up   <= 1'b0;
      link_went_down <= 1'b0;
      early_pulse    <= 1'b0;
 
      if (clear) begin
        c_link_ups <= '0; c_link_downs <= '0; worst_silence_ms <= 16'd0;
        // ever_link_down survives: a link that has bounced has bounced.
      end
 
      if (tick_q == 32'(MS_TICKS - 1)) begin
        tick_q <= '0;
        if (ms_q != 16'hFFFF) ms_q <= ms_q + 16'd1;
      end else begin
        tick_q <= tick_q + 1'b1;
      end
 
      if (pulse_in || frame_activity) begin
        // The worst silence is recorded BEFORE the counter resets --
        // it is the margin against the loss timer, and it is the only
        // forward-looking number this module produces.
        if (link_up && (ms_q > worst_silence_ms)) worst_silence_ms <= ms_q;
 
        if (pulse_in && (ms_q < 16'(MIN_GAP_MS)) && (run_q != 4'd0)) begin
          // Too soon to be a link pulse. This is either noise or a
          // pulse from inside a burst -- and a link-integrity monitor
          // watching an FLP stream sees exactly that.
          early_pulse <= 1'b1;
        end else begin
          if (run_q != 4'(LC_COUNT)) begin
            run_q <= run_q + 4'd1;
          end else if (!link_up) begin
            link_up      <= 1'b1;
            link_came_up <= 1'b1;
            if (!(&c_link_ups)) c_link_ups <= c_link_ups + 1'b1;
          end
        end
 
        ms_q <= 16'd0;
 
      end else if (ms_q == 16'(LINK_LOSS_MS)) begin
        run_q <= 4'd0;
        if (link_up) begin
          link_up        <= 1'b0;
          link_went_down <= 1'b1;
          ever_link_down <= 1'b1;
          if (!(&c_link_downs)) c_link_downs <= c_link_downs + 1'b1;
        end
      end
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// Aggregates everything discovery learned into a record a later reader
// can act on -- including the things that are not errors.
//
// THE PRINCIPLE THIS MODULE IMPLEMENTS: discovery's most valuable
// outputs are not failures. They are PROVENANCE and MARGIN.
//
//   provenance -- was this measured, assumed, or inherited from a
//        detection? Chapter 9.2's duplex mismatch is entirely a
//        provenance problem.
//   margin     -- how close was the process to not working? Worst
//        discovery time, worst burst quality, worst silence.
//
// Neither is an error. Both are invisible unless something collects
// them, and both are what turn a link that works into a link that is
// known to keep working.
module discovery_telemetry
  import discovery_pkg::*;
#(
  parameter int unsigned CNT_W = 20
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  signalling_e classification,
  input  logic        classification_valid,
  input  logic        word_valid,
  input  logic [15:0] bit_confidence,
  input  logic        word_fully_bracketed,
  input  logic        detection_valid,
  input  logic        speed_is_measured,
  input  logic        duplex_is_assumed,
  input  logic        discovery_failed,
  input  logic [2:0]  failed_stage,
  input  logic [15:0] discovery_ms,
  input  logic [15:0] worst_silence_ms,
  input  logic [15:0] loss_threshold_ms,
 
  // Provenance.
  output logic        speed_was_measured,
  output logic        duplex_was_assumed,
  output logic        abilities_were_negotiated,
  output signalling_e partner_kind,
 
  // Margin.
  output logic [4:0]  worst_low_confidence_bits,
  output logic [15:0] worst_discovery_ms,
  output logic [7:0]  silence_margin_percent,
 
  // Counts.
  output logic [CNT_W-1:0] c_words,
  output logic [CNT_W-1:0] c_words_fully_bracketed,
  output logic [CNT_W-1:0] c_detections,
  output logic [CNT_W-1:0] c_failures,
  output logic [2:0]       first_failed_stage,
  output logic             first_failure_valid,
 
  // Sticky facts a later reader needs and a counter clear destroys.
  output logic ever_assumed_duplex,
  output logic ever_low_confidence,
  output logic ever_failed
);
 
  function automatic logic [4:0] count_zeros (input logic [15:0] v);
    count_zeros = 5'd0;
    for (int i = 0; i < 16; i = i + 1)
      if (!v[i]) count_zeros = count_zeros + 5'd1;
  endfunction
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      speed_was_measured <= 1'b0; duplex_was_assumed <= 1'b0;
      abilities_were_negotiated <= 1'b0; partner_kind <= SIG_NONE;
      worst_low_confidence_bits <= 5'd0; worst_discovery_ms <= 16'd0;
      silence_margin_percent <= 8'd100;
      c_words <= '0; c_words_fully_bracketed <= '0;
      c_detections <= '0; c_failures <= '0;
      first_failed_stage <= 3'd0; first_failure_valid <= 1'b0;
      ever_assumed_duplex <= 1'b0; ever_low_confidence <= 1'b0;
      ever_failed <= 1'b0;
    end else begin
      if (clear) begin
        c_words <= '0; c_words_fully_bracketed <= '0;
        c_detections <= '0; c_failures <= '0;
        first_failure_valid <= 1'b0;
        worst_low_confidence_bits <= 5'd0; worst_discovery_ms <= 16'd0;
        // The three ever_* flags survive. They are the facts a later
        // reader needs and the ones a counter clear would destroy.
      end
 
      if (classification_valid) partner_kind <= classification;
 
      if (word_valid) begin
        if (!(&c_words)) c_words <= c_words + 1'b1;
        abilities_were_negotiated <= 1'b1;
 
        if (word_fully_bracketed) begin
          if (!(&c_words_fully_bracketed))
            c_words_fully_bracketed <= c_words_fully_bracketed + 1'b1;
        end else begin
          ever_low_confidence <= 1'b1;
          if (count_zeros(bit_confidence) > worst_low_confidence_bits)
            worst_low_confidence_bits <= count_zeros(bit_confidence);
        end
      end
 
      if (detection_valid) begin
        if (!(&c_detections)) c_detections <= c_detections + 1'b1;
        speed_was_measured <= speed_is_measured;
        duplex_was_assumed <= duplex_is_assumed;
        if (duplex_is_assumed) ever_assumed_duplex <= 1'b1;
      end
 
      if (discovery_ms > worst_discovery_ms) worst_discovery_ms <= discovery_ms;
 
      // The silence margin as a percentage of the loss threshold. A
      // link at 90% is up, healthy, and will drop on the next
      // disturbance -- and no other signal in the design says so.
      if (loss_threshold_ms != 16'd0)
        silence_margin_percent <= 8'((worst_silence_ms * 100) / loss_threshold_ms);
 
      if (discovery_failed) begin
        ever_failed <= 1'b1;
        if (!(&c_failures)) c_failures <= c_failures + 1'b1;
        if (!first_failure_valid) begin
          first_failure_valid <= 1'b1;
          first_failed_stage  <= failed_stage;
        end
      end
    end
  end
 
endmodule

// P1. A burst has exactly 33 positions.
property p_burst_has_33_positions;
  @(posedge clk) disable iff (!rst_n)
  burst_complete |-> ($past(position) == 6'(FLP_POSITIONS - 1));
endproperty
a_burst_33_positions: assert property (p_burst_has_33_positions);
 
// P2. Even positions are clock positions and always pulse; odd
// positions are data and pulse only for a one.
property p_clock_positions_always_pulse;
  @(posedge clk) disable iff (!rst_n)
  (burst_active && !position[0] && (tick_q == 16'd0)) |-> pulse;
endproperty
a_clock_always_pulses: assert property (p_clock_positions_always_pulse);
 
// P3. THE ENCODING. A data position pulses if and only if its bit is
// a one -- so a zero emits nothing at all.
property p_data_pulse_iff_one;
  @(posedge clk) disable iff (!rst_n)
  (burst_active && position[0] && (tick_q == 16'd0))
    |-> (pulse == link_code_word[position[4:1]]);
endproperty
a_data_pulse_iff_one: assert property (p_data_pulse_iff_one);
 
// P4. The pulse count equals 17 plus the number of ones. A free
// consistency check on the word actually being advertised.
property p_pulse_count_matches_word;
  @(posedge clk) disable iff (!rst_n)
  burst_complete |-> (pulses_last_burst ==
                      6'(FLP_CLOCK_PULSES) + 6'($countones(link_code_word)));
endproperty
a_pulse_count_matches: assert property (p_pulse_count_matches_word);
 
// P5. Bursts repeat inside the legal window, which is what keeps a
// 10BASE-T partner's link up.
property p_burst_spacing_in_window;
  @(posedge clk) disable iff (!rst_n)
  $rose(burst_active) |-> ($past(gap_q) >= 32'(BURST_MIN_MS * 1000 * CLK_MHZ));
endproperty
a_burst_spacing: assert property (p_burst_spacing_in_window);

// P6. THE PROPERTY THIS CHAPTER IS ABOUT. A bit is marked confident
// only when BOTH bracketing clock pulses arrived. This is what makes
// an absence interpretable.
property p_confidence_requires_bracketing;
  @(posedge clk) disable iff (!rst_n)
  (word_valid && bit_confidence[0]) |-> $past(prev_clock_ok_q, 1);
endproperty
a_confidence_requires_bracketing: assert property (p_confidence_requires_bracketing);
 
// P7. A fully bracketed word requires all 17 clock pulses. Sixteen
// gaps need seventeen boundaries, and a missing one leaves a bit
// unlicensed.
property p_full_bracket_needs_17_clocks;
  @(posedge clk) disable iff (!rst_n)
  word_fully_bracketed |-> (clock_pulses_seen == 6'(FLP_CLOCK_PULSES));
endproperty
a_full_bracket_needs_17: assert property (p_full_bracket_needs_17_clocks);
 
// P8. And it requires every confidence bit set.
property p_full_bracket_needs_all_confidence;
  @(posedge clk) disable iff (!rst_n)
  word_fully_bracketed |-> (bit_confidence == 16'hFFFF);
endproperty
a_full_bracket_all_conf: assert property (p_full_bracket_needs_all_confidence);
 
// P9. A clock interval outside 111..139 us is REPORTED, and it
// invalidates the bits that depend on it rather than being absorbed.
property p_clock_interval_violation_reported;
  @(posedge clk) disable iff (!rst_n)
  clock_interval_violation |=> !prev_clock_ok_q;
endproperty
a_clock_violation_reported: assert property (p_clock_interval_violation_reported);
 
// P10. A pulse beyond data_detect_max is NOT accepted as data. It is
// the next clock pulse arriving early, and accepting it shifts every
// subsequent bit.
property p_late_pulse_not_data;
  @(posedge clk) disable iff (!rst_n)
  late_pulse_seen |-> !$past(saw_data_q);
endproperty
a_late_pulse_not_data: assert property (p_late_pulse_not_data);
 
// P11. Every burst produces a word, valid or not -- the word is
// published WITH its confidence rather than withheld, because a
// partially bracketed word is still evidence.
property p_every_burst_produces_a_word;
  @(posedge clk) disable iff (!rst_n)
  ($fell(in_burst_q) && $past(in_burst_q)) |-> word_valid;
endproperty
a_every_burst_a_word: assert property (p_every_burst_produces_a_word);

// P12. A classification requires CONFIRM consistent observations.
// One burst is not a partner type.
property p_classification_needs_confirmation;
  @(posedge clk) disable iff (!rst_n)
  classification_changed |-> ($past(confirm_q) == 4'(CONFIRM));
endproperty
a_classification_confirmed: assert property (p_classification_needs_confirmation);
 
// P13. THE INTRA-GROUP PROPERTY. An FLP classification requires 17 or
// more pulses at 125 us spacing -- the repetition RATE cannot
// distinguish a burst from a link pulse, because they deliberately
// overlap.
property p_flp_needs_intra_group_structure;
  @(posedge clk) disable iff (!rst_n)
  (classification_changed && (classification == SIG_FLP_BURST))
    |-> ((last_group_size >= 6'd17) &&
         (last_intra_group_us >= 16'(CLK_SPACING_US - CLK_TOL_US)) &&
         (last_intra_group_us <= 16'(CLK_SPACING_US + CLK_TOL_US)));
endproperty
a_flp_needs_structure: assert property (p_flp_needs_intra_group_structure);
 
// P14. Activity fitting no signature is REPORTED, never rounded to the
// nearest legal case.
property p_ambiguous_not_rounded;
  @(posedge clk) disable iff (!rst_n)
  ambiguous_signalling |-> (classification != SIG_FLP_BURST);
endproperty
a_ambiguous_not_rounded: assert property (p_ambiguous_not_rounded);

// P15. Parallel detection NEVER yields full duplex. Duplex is not
// observable on an idle link, so a detected full-duplex result has
// inferred something from nothing.
property p_detection_never_full_duplex;
  @(posedge clk) disable iff (!rst_n)
  detection_valid |-> !detected_duplex;
endproperty
a_detection_never_full: assert property (p_detection_never_full_duplex);
 
// P16. And it ALWAYS marks duplex as assumed. The provenance bit is
// not optional.
property p_detection_marks_assumption;
  @(posedge clk) disable iff (!rst_n)
  detection_valid |-> duplex_is_assumed;
endproperty
a_detection_marks_assumption: assert property (p_detection_marks_assumption);
 
// P17. While speed is marked measured -- two provenance bits, never
// one validity bit.
property p_speed_marked_measured;
  @(posedge clk) disable iff (!rst_n)
  detection_valid |-> speed_is_measured;
endproperty
a_speed_marked_measured: assert property (p_speed_marked_measured);
 
// P18. An FLP burst suppresses detection entirely. A partner that
// negotiates is never guessed about.
property p_flp_suppresses_detection;
  @(posedge clk) disable iff (!rst_n)
  (classification == SIG_FLP_BURST) |=> !detection_valid;
endproperty
a_flp_suppresses: assert property (p_flp_suppresses_detection);
 
// P19. The sticky flag survives -- a port whose duplex was never
// agreed stays flagged across link bounces.
property p_ever_detected_sticky;
  @(posedge clk) disable iff (!rst_n)
  ever_parallel_detected |=> ever_parallel_detected;
endproperty
a_ever_detected_sticky: assert property (p_ever_detected_sticky);

// P20. Abilities are declared available only from a FULLY BRACKETED
// word. A partial word is a guess with a shape.
property p_abilities_need_full_bracket;
  @(posedge clk) disable iff (!rst_n)
  $rose(abilities_available) |-> $past(word_fully_bracketed);
endproperty
a_abilities_need_bracket: assert property (p_abilities_need_full_bracket);
 
// P21. A negotiated result supersedes a detection in progress.
property p_negotiation_supersedes_detection;
  @(posedge clk) disable iff (!rst_n)
  ((stage == 3'(D_DETECT)) && (classification == SIG_FLP_BURST))
    |=> (stage == 3'(D_DECODE));
endproperty
a_negotiation_supersedes: assert property (p_negotiation_supersedes_detection);
 
// P22. Every attempt terminates: done or failed, never neither.
property p_discovery_terminates;
  @(posedge clk) disable iff (!rst_n)
  (stage == 3'(D_OBSERVE)) |-> ##[1:$] ((stage == 3'(D_DONE)) ||
                                        (stage == 3'(D_FAILED)) ||
                                        (stage == 3'(D_IDLE)));
endproperty
a_discovery_terminates: assert property (p_discovery_terminates);
 
// P23. A failure names its stage, latched at the first one.
property p_failure_names_stage;
  @(posedge clk) disable iff (!rst_n)
  discovery_failed |-> (failed_stage inside {3'(D_CLASSIFY), 3'(D_DECODE),
                                             3'(D_DETECT)});
endproperty
a_failure_names_stage: assert property (p_failure_names_stage);