SGMII — Four Wires, and the Same Four at Every Speed

// SYNTHESIZABLE (with an 8B/10B encoder instantiated below).
//
// Builds the SGMII transmit stream: frame data, idle, and the
// configuration ordered sets that replace autonegotiation's link code
// word.
//
// THE NUMBERS:
//   1000 Mb/s x 10/8      = 1250 Mbaud
//   1250 / 10             =  125 M code groups/s
//   125 M x 8             = 1000 Mb/s      <- closes
//   1 UI                  =  800 ps
//   AND THE RATE NEVER CHANGES. 100 Mb/s repeats each code group 10x;
//   10 Mb/s repeats it 100x. Section 8 does the repeating; this module
//   does not know the link speed exists.
//
// THE ORDERED SETS. SGMII has no control pins, so every control event
// is a code group:
//   /I/  idle          -- fills the stream between frames
//   /C/  configuration -- carries the 16-bit config word, two at a time
//   /S/  start         -- replaces GMII's TX_EN rising
//   /T/  terminate     -- replaces TX_EN falling
//   /V/  error         -- replaces TX_ER
// Everything Module 10 spent pins on is a value in this stream.
package sgmii_pkg;
 
  localparam int unsigned CODE_BITS   = 10;
  localparam int unsigned OCTET_BITS  = 8;
  localparam int unsigned BAUD_MBAUD  = 1250;
  localparam int unsigned CODE_GROUPS_PER_S_M = 125;
 
  // Replication factors. 1000/100 = 10 and 1000/10 = 100.
  localparam int unsigned REP_1000 = 1;
  localparam int unsigned REP_100  = 10;
  localparam int unsigned REP_10   = 100;
 
  // The 802.3z link timer is 10 ms; SGMII shortens it to 1.6 ms so a
  // speed or link change reaches the MAC promptly.
  localparam int unsigned LINK_TIMER_US = 1600;
 
  // Special code groups, named rather than valued -- the 8B/10B
  // mapping is Chapter 3.5's subject.
  typedef enum logic [3:0] {
    K_IDLE1,      // /I1/
    K_IDLE2,      // /I2/
    K_CONFIG1,    // /C1/
    K_CONFIG2,    // /C2/
    K_START,      // /S/
    K_TERMINATE,  // /T/
    K_ERROR,      // /V/
    K_NONE
  } ordered_set_e;
 
  typedef enum logic [1:0] {
    SPD_10, SPD_100, SPD_1000, SPD_RESERVED
  } sgmii_speed_e;
 
  // The SGMII configuration word, PHY -> MAC:
  //   bit 15    link      1 = up
  //   bit 14    ACK       auto-negotiation acknowledge
  //   bit 12    duplex    1 = full
  //   bits 11:10 speed    00 = 10, 01 = 100, 10 = 1000, 11 reserved
  //   bit 0     always 1
  // MAC -> PHY sends 0x0001 -- bit 0 set, everything else zero,
  // because the MAC has nothing to advertise. The asymmetry is
  // deliberate: SGMII is not a negotiation, it is a REPORT.
  localparam int unsigned CFG_LINK_BIT   = 15;
  localparam int unsigned CFG_ACK_BIT    = 14;
  localparam int unsigned CFG_DUPLEX_BIT = 12;
  localparam logic [15:0] CFG_FROM_MAC   = 16'h0001;
 
endpackage
 
module sgmii_ordered_set_encoder
  import sgmii_pkg::*;
#(
  parameter int unsigned CNT_W = 24
) (
  input  logic clk,                  // 125 MHz code-group clock
  input  logic rst_n,
 
  // Frame interface, identical in shape to GMII's.
  input  logic [7:0] octet,
  input  logic       octet_valid,
  input  logic       frame_start,
  input  logic       frame_end,
  input  logic       tx_error,
 
  // Configuration to advertise. On a MAC this is CFG_FROM_MAC; on a
  // PHY it carries link, speed and duplex.
  input  logic        send_config,
  input  logic [15:0] config_word,
 
  // To the 8B/10B encoder.
  output logic [7:0]  code_octet,
  output logic        code_is_k,     // control code group
  output ordered_set_e code_kind,
  output logic        code_valid,
 
  output logic [CNT_W-1:0] c_frames,
  output logic [CNT_W-1:0] c_config_sets,
  output logic [CNT_W-1:0] c_idle_sets,
  // A frame octet arrived while a two-code-group ordered set was still
  // being emitted. Ordered sets are ATOMIC -- splitting one produces a
  // stream the far end cannot parse.
  output logic             ordered_set_collision
);
 
  // /C/ and /I/ are TWO code groups each: a K character followed by a
  // data character. The pair is atomic.
  logic       in_pair_q;
  logic [7:0] second_q;
  logic       second_is_k_q;
  ordered_set_e pair_kind_q;
  logic       config_phase_q;    // /C1/ then /C2/, alternating
  logic       idle_phase_q;      // /I1/ then /I2/, alternating
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      in_pair_q <= 1'b0; second_q <= 8'd0; second_is_k_q <= 1'b0;
      pair_kind_q <= K_NONE; config_phase_q <= 1'b0; idle_phase_q <= 1'b0;
      code_octet <= 8'd0; code_is_k <= 1'b0; code_kind <= K_NONE;
      code_valid <= 1'b0;
      c_frames <= '0; c_config_sets <= '0; c_idle_sets <= '0;
      ordered_set_collision <= 1'b0;
    end else begin
      code_valid            <= 1'b1;
      ordered_set_collision <= 1'b0;
 
      if (in_pair_q) begin
        // SECOND HALF of an ordered set. Unconditional -- once the K
        // character is on the wire the pair is committed, and a frame
        // octet offered here must wait.
        code_octet <= second_q;
        code_is_k  <= second_is_k_q;
        code_kind  <= pair_kind_q;
        in_pair_q  <= 1'b0;
        if (octet_valid) ordered_set_collision <= 1'b1;
 
      end else if (frame_start) begin
        // /S/ -- one code group, no pair.
        code_octet <= 8'd0;
        code_is_k  <= 1'b1;
        code_kind  <= K_START;
        if (!(&c_frames)) c_frames <= c_frames + 1'b1;
 
      end else if (frame_end) begin
        code_octet <= 8'd0;
        code_is_k  <= 1'b1;
        code_kind  <= K_TERMINATE;
 
      end else if (tx_error) begin
        // /V/ replaces GMII's TX_ER pin. A control event with no wire.
        code_octet <= 8'd0;
        code_is_k  <= 1'b1;
        code_kind  <= K_ERROR;
 
      end else if (octet_valid) begin
        code_octet <= octet;
        code_is_k  <= 1'b0;
        code_kind  <= K_NONE;
 
      end else if (send_config) begin
        // /C/ ordered set: K character, then a config byte. Two sets
        // carry the 16-bit word, low byte then high.
        code_octet    <= 8'd0;
        code_is_k     <= 1'b1;
        code_kind     <= config_phase_q ? K_CONFIG2 : K_CONFIG1;
        second_q      <= config_phase_q ? config_word[15:8]
                                        : config_word[7:0];
        second_is_k_q <= 1'b0;
        pair_kind_q   <= config_phase_q ? K_CONFIG2 : K_CONFIG1;
        in_pair_q     <= 1'b1;
        config_phase_q <= ~config_phase_q;
        if (!(&c_config_sets)) c_config_sets <= c_config_sets + 1'b1;
 
      end else begin
        // /I/ idle, alternating I1 and I2 so the running disparity is
        // driven back toward neutral rather than allowed to walk.
        code_octet    <= 8'd0;
        code_is_k     <= 1'b1;
        code_kind     <= idle_phase_q ? K_IDLE2 : K_IDLE1;
        second_q      <= 8'd0;
        second_is_k_q <= 1'b0;
        pair_kind_q   <= idle_phase_q ? K_IDLE2 : K_IDLE1;
        in_pair_q     <= 1'b1;
        idle_phase_q  <= ~idle_phase_q;
        if (!(&c_idle_sets)) c_idle_sets <= c_idle_sets + 1'b1;
      end
    end
  end
 
endmodule

// SYNTHESIZABLE (with an 8B/10B decoder ahead of it).
//
// Classifies the received stream and extracts the configuration word.
//
// THE ORDERING THAT CANNOT BE REARRANGED:
//   1. comma alignment -- find where code groups begin
//   2. 8B/10B decode   -- ten bits back to eight, plus K/data
//   3. CLASSIFY        -- this module
//   4. act
// Nothing above step 3 can consume anything, because in a serial stream
// a frame octet and a config byte are the same eight bits and differ
// only in what preceded them.
module sgmii_ordered_set_decoder
  import sgmii_pkg::*;
#(
  parameter int unsigned CNT_W = 24
) (
  input  logic clk,
  input  logic rst_n,
 
  input  logic       aligned,        // comma alignment acquired
  input  logic [7:0] code_octet,
  input  logic       code_is_k,
  input  ordered_set_e code_kind,
  input  logic       code_valid,
  input  logic       code_invalid,   // 8B/10B said this is not a code
 
  // Frame output.
  output logic [7:0] octet,
  output logic       octet_valid,
  output logic       frame_start,
  output logic       frame_end,
  output logic       frame_had_error,
 
  // Configuration output.
  output logic [15:0] config_word,
  output logic        config_valid,
  output logic        link_up,
  output sgmii_speed_e speed,
  output logic        full_duplex,
  output logic        config_ack,
 
  output logic [CNT_W-1:0] c_frames,
  output logic [CNT_W-1:0] c_config_words,
  output logic [CNT_W-1:0] c_invalid_codes,
  // A data code group with no frame open and no ordered set expecting
  // it. In a serial stream this is what a lost alignment looks like.
  output logic             orphan_data,
  output logic [CNT_W-1:0] c_orphan_data
);
 
  logic in_frame_q;
  logic expect_cfg_lo_q;
  logic expect_cfg_hi_q;
  logic [7:0] cfg_lo_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      in_frame_q <= 1'b0; expect_cfg_lo_q <= 1'b0; expect_cfg_hi_q <= 1'b0;
      cfg_lo_q <= 8'd0;
      octet <= 8'd0; octet_valid <= 1'b0; frame_start <= 1'b0;
      frame_end <= 1'b0; frame_had_error <= 1'b0;
      config_word <= 16'd0; config_valid <= 1'b0;
      link_up <= 1'b0; speed <= SPD_RESERVED; full_duplex <= 1'b0;
      config_ack <= 1'b0;
      c_frames <= '0; c_config_words <= '0; c_invalid_codes <= '0;
      orphan_data <= 1'b0; c_orphan_data <= '0;
    end else begin
      octet_valid  <= 1'b0;
      frame_start  <= 1'b0;
      frame_end    <= 1'b0;
      config_valid <= 1'b0;
      orphan_data  <= 1'b0;
 
      if (!aligned) begin
        // Nothing can be believed before alignment. Not "assume idle" --
        // NOTHING, because an unaligned stream decodes to plausible
        // code groups that mean something else entirely.
        in_frame_q      <= 1'b0;
        expect_cfg_lo_q <= 1'b0;
        expect_cfg_hi_q <= 1'b0;
 
      end else if (code_valid) begin
        if (code_invalid) begin
          // An 8B/10B code group that is not in the table. Counted, and
          // it condemns any open frame -- but note that it CANNOT catch
          // a single-bit error that turned one valid code into another.
          if (!(&c_invalid_codes)) c_invalid_codes <= c_invalid_codes + 1'b1;
          if (in_frame_q) frame_had_error <= 1'b1;
 
        end else if (code_is_k) begin
          // A control code group ends any pending ordered set, which is
          // how a truncated /C/ pair fails safely rather than merging
          // its first half with the next set's second.
          expect_cfg_lo_q <= 1'b0;
          expect_cfg_hi_q <= 1'b0;
 
          unique case (code_kind)
            K_START: begin
              in_frame_q      <= 1'b1;
              frame_start     <= 1'b1;
              frame_had_error <= 1'b0;
              if (!(&c_frames)) c_frames <= c_frames + 1'b1;
            end
            K_TERMINATE: begin
              in_frame_q <= 1'b0;
              frame_end  <= 1'b1;
            end
            K_ERROR: begin
              frame_had_error <= 1'b1;
            end
            K_CONFIG1: expect_cfg_lo_q <= 1'b1;
            K_CONFIG2: expect_cfg_hi_q <= 1'b1;
            default: ;                       // idle
          endcase
 
        end else begin
          // A DATA code group. What it means depends entirely on what
          // preceded it -- which is the structural difference between a
          // serial interface and a parallel one.
          if (in_frame_q) begin
            octet       <= code_octet;
            octet_valid <= 1'b1;
 
          end else if (expect_cfg_lo_q) begin
            cfg_lo_q        <= code_octet;
            expect_cfg_lo_q <= 1'b0;
 
          end else if (expect_cfg_hi_q) begin
            expect_cfg_hi_q <= 1'b0;
            config_word     <= {code_octet, cfg_lo_q};
            config_valid    <= 1'b1;
            if (!(&c_config_words)) c_config_words <= c_config_words + 1'b1;
 
            // Extract the fields. The PHY's report, not a negotiation.
            link_up     <= code_octet[CFG_LINK_BIT - 8];
            config_ack  <= code_octet[CFG_ACK_BIT - 8];
            full_duplex <= code_octet[CFG_DUPLEX_BIT - 8];
            speed       <= sgmii_speed_e'(code_octet[3:2]);
 
          end else begin
            // ORPHAN DATA. No frame, no ordered set expecting it. In a
            // serial stream this is the signature of alignment that was
            // lost and re-acquired at the wrong boundary -- every code
            // group decodes to something, and none of it is right.
            orphan_data <= 1'b1;
            if (!(&c_orphan_data)) c_orphan_data <= c_orphan_data + 1'b1;
          end
        end
      end
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// Serves 10 and 100 Mb/s by REPEATING each code group on transmit and
// picking one of each run on receive.
//
// THE ARITHMETIC:
//   1000 Mb/s -> 1x   (125 M code groups/s, all of them distinct)
//    100 Mb/s -> 10x  (125 M / 10 = 12.5 M distinct)
//     10 Mb/s -> 100x (125 M / 100 = 1.25 M distinct)
//
// AND THE CLOCK NEVER CHANGES. This is the module that makes SGMII's
// central claim true: the serialiser, the CDR, the encoder and the
// differential pair see exactly the same 1.25 Gbaud stream at every
// speed, and the only thing that varies is a counter.
//
// THE RECEIVE SIDE IS THE HARD HALF, and the reason is clock tolerance.
// The two ends' 125 MHz references are independent and each is within
// its own tolerance -- so over a long stream the receiver does NOT see
// runs of exactly 10. It sees mostly 10, occasionally 9 or 11, and the
// boundaries drift. A decimator that counts to exactly 10 and resets
// will slip; one that RE-SYNCHRONISES on every code-group CHANGE will
// not.
module sgmii_rate_replicator
  import sgmii_pkg::*;
#(
  parameter int unsigned CNT_W = 24
) (
  input  logic clk,
  input  logic rst_n,
 
  input  sgmii_speed_e speed,
 
  // Transmit: one code group in per REP periods out.
  input  logic [7:0]   tx_code_octet,
  input  logic         tx_code_is_k,
  input  logic         tx_code_valid,
  output logic         tx_code_ready,
  output logic [7:0]   rep_code_octet,
  output logic         rep_code_is_k,
  output logic         rep_code_valid,
 
  // Receive: REP identical code groups in, one out.
  input  logic [7:0]   rx_code_octet,
  input  logic         rx_code_is_k,
  input  logic         rx_code_valid,
  output logic [7:0]   dec_code_octet,
  output logic         dec_code_is_k,
  output logic         dec_code_valid,
 
  // The observed run length, exported. It is nominally REP and will
  // legitimately vary by one because the two ends' clocks are
  // independent -- so this is a distribution, not a constant.
  output logic [6:0]       last_run_length,
  output logic [6:0]       shortest_run,
  output logic [6:0]       longest_run,
  // A run so far from nominal that it is not clock tolerance. Reported
  // rather than absorbed, because it is the signature of the two ends
  // disagreeing about the SPEED rather than about the clock.
  output logic             run_length_anomaly,
  output logic [CNT_W-1:0] c_anomalies
);
 
  function automatic logic [6:0] rep_for (input sgmii_speed_e s);
    unique case (s)
      SPD_1000: rep_for = 7'(REP_1000);
      SPD_100:  rep_for = 7'(REP_100);
      SPD_10:   rep_for = 7'd100;          // REP_10, clipped to 7 bits
      default:  rep_for = 7'(REP_1000);
    endcase
  endfunction
 
  logic [6:0] rep_c;
  assign rep_c = rep_for(speed);
 
  // ---- transmit: hold each code group for rep_c periods ----
  logic [6:0] tx_hold_q;
  logic [7:0] tx_held_octet_q;
  logic       tx_held_k_q;
 
  assign tx_code_ready = (tx_hold_q == 7'd0);
 
  // ---- receive: pick one of each run ----
  logic [7:0] rx_prev_octet_q;
  logic       rx_prev_k_q;
  logic       rx_have_prev_q;
  logic [6:0] rx_run_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      tx_hold_q <= 7'd0; tx_held_octet_q <= 8'd0; tx_held_k_q <= 1'b0;
      rep_code_octet <= 8'd0; rep_code_is_k <= 1'b0; rep_code_valid <= 1'b0;
      rx_prev_octet_q <= 8'd0; rx_prev_k_q <= 1'b0; rx_have_prev_q <= 1'b0;
      rx_run_q <= 7'd0;
      dec_code_octet <= 8'd0; dec_code_is_k <= 1'b0; dec_code_valid <= 1'b0;
      last_run_length <= 7'd0; shortest_run <= 7'd127; longest_run <= 7'd0;
      run_length_anomaly <= 1'b0; c_anomalies <= '0;
    end else begin
      rep_code_valid     <= 1'b0;
      dec_code_valid     <= 1'b0;
      run_length_anomaly <= 1'b0;
 
      // ---------------- TRANSMIT ----------------
      if (tx_hold_q != 7'd0) begin
        rep_code_octet <= tx_held_octet_q;
        rep_code_is_k  <= tx_held_k_q;
        rep_code_valid <= 1'b1;
        tx_hold_q      <= tx_hold_q - 7'd1;
      end else if (tx_code_valid) begin
        tx_held_octet_q <= tx_code_octet;
        tx_held_k_q     <= tx_code_is_k;
        rep_code_octet  <= tx_code_octet;
        rep_code_is_k   <= tx_code_is_k;
        rep_code_valid  <= 1'b1;
        tx_hold_q       <= rep_c - 7'd1;
      end
 
      // ---------------- RECEIVE ----------------
      if (rx_code_valid) begin
        if (rx_have_prev_q &&
            (rx_code_octet == rx_prev_octet_q) &&
            (rx_code_is_k == rx_prev_k_q)) begin
          // Same code group again: still inside the run.
          if (rx_run_q != 7'd127) rx_run_q <= rx_run_q + 7'd1;
 
        end else begin
          // A DIFFERENT code group. The run ended here -- and this is
          // the resynchronisation point. Nothing counts to a fixed
          // number, so a run of 9 or 11 caused by ordinary clock
          // tolerance costs nothing at all.
          if (rx_have_prev_q) begin
            last_run_length <= rx_run_q;
            if (rx_run_q < shortest_run) shortest_run <= rx_run_q;
            if (rx_run_q > longest_run)  longest_run  <= rx_run_q;
 
            // ANOMALY: not a clock-tolerance excursion of one, but a
            // run that is wrong by a factor. That is the two ends
            // disagreeing about the speed, and it must not be absorbed.
            if ((rx_run_q > (rep_c + (rep_c >> 1))) ||
                ((rep_c > 7'd2) && (rx_run_q < (rep_c - (rep_c >> 1))))) begin
              run_length_anomaly <= 1'b1;
              if (!(&c_anomalies)) c_anomalies <= c_anomalies + 1'b1;
            end
          end
 
          // Emit exactly one code group per run, at its boundary.
          dec_code_octet <= rx_code_octet;
          dec_code_is_k  <= rx_code_is_k;
          dec_code_valid <= 1'b1;
 
          rx_prev_octet_q <= rx_code_octet;
          rx_prev_k_q     <= rx_code_is_k;
          rx_have_prev_q  <= 1'b1;
          rx_run_q        <= 7'd1;
        end
      end
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// Tracks the two pieces of 8B/10B state a receiver must hold, and --
// crucially -- distinguishes their TRANSIENTS from their failures.
//
// COMMA ALIGNMENT. A serial stream arrives as bits; code-group
// boundaries are found by searching for the comma pattern, which is
// constructed so it cannot appear across a boundary of any legal code
// group sequence. Before alignment, NOTHING can be believed -- and the
// dangerous part is that an unaligned stream still decodes to plausible
// code groups most of the time.
//
// RUNNING DISPARITY. 8B/10B keeps the count of ones and zeros bounded
// by choosing, for each octet, whichever of two code groups moves the
// running total back toward neutral. The receiver tracks the same
// state, and if its state diverges from the transmitter's, decoded
// values are wrong.
//
// AND HERE IS THE PART SECTION 16 IS ABOUT: running disparity is
// SELF-HEALING. After alignment is regained, the receiver's disparity
// state re-converges with the transmitter's within a bounded number of
// code groups, because the encoding drives it there. So there is a
// legal, expected, REQUIRED window during which disparity is wrong --
// and asserting that disparity is always correct fires during exactly
// the recovery the mechanism was designed to perform.
module sgmii_comma_disparity_monitor
  import sgmii_pkg::*;
#(
  // Code groups after alignment within which disparity must re-converge.
  parameter int unsigned CONVERGE_CODES = 16'd64,
  // Consecutive good code groups required to declare alignment.
  parameter int unsigned ALIGN_CONFIRM  = 16'd4,
  parameter int unsigned CNT_W = 24
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic comma_seen,
  input  logic code_valid,
  input  logic code_invalid,
  input  logic disparity_error,
 
  output logic aligned,
  output logic align_lost,
  // TRUE while the design is inside its legal re-convergence window.
  // Every disparity check must be qualified by this, and Section 16's
  // rejected property is what happens when it is not.
  output logic converging,
  output logic converged,
  // The window expired with disparity still wrong. THIS is a fault --
  // as distinct from disparity being wrong during the window, which is
  // the mechanism working.
  output logic convergence_failed,
 
  output logic [15:0]      codes_to_converge,
  output logic [15:0]      worst_convergence,
  output logic [CNT_W-1:0] c_aligns,
  output logic [CNT_W-1:0] c_align_losses,
  output logic [CNT_W-1:0] c_disparity_errors_in_window,
  output logic [CNT_W-1:0] c_disparity_errors_steady,
  output logic             ever_convergence_failed
);
 
  logic [15:0] good_run_q;
  logic [15:0] converge_q;
  logic        aligned_q;
 
  assign aligned = aligned_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      good_run_q <= '0; converge_q <= '0; aligned_q <= 1'b0;
      align_lost <= 1'b0; converging <= 1'b0; converged <= 1'b0;
      convergence_failed <= 1'b0;
      codes_to_converge <= '0; worst_convergence <= '0;
      c_aligns <= '0; c_align_losses <= '0;
      c_disparity_errors_in_window <= '0;
      c_disparity_errors_steady <= '0;
      ever_convergence_failed <= 1'b0;
    end else if (clear) begin
      c_aligns <= '0; c_align_losses <= '0;
      c_disparity_errors_in_window <= '0;
      c_disparity_errors_steady <= '0;
      worst_convergence <= '0;
      // ever_convergence_failed survives.
    end else begin
      align_lost         <= 1'b0;
      convergence_failed <= 1'b0;
 
      if (code_valid) begin
        if (!aligned_q) begin
          // HUNTING. A comma plus a run of decodable code groups is
          // alignment; a comma alone is not, because an unaligned
          // stream produces comma-like patterns by chance.
          if (comma_seen && !code_invalid) begin
            if (good_run_q == ALIGN_CONFIRM - 16'd1) begin
              aligned_q  <= 1'b1;
              converging <= 1'b1;      // the window OPENS here
              converged  <= 1'b0;
              converge_q <= '0;
              good_run_q <= '0;
              if (!(&c_aligns)) c_aligns <= c_aligns + 1'b1;
            end else begin
              good_run_q <= good_run_q + 16'd1;
            end
          end else if (code_invalid) begin
            good_run_q <= '0;
          end
 
        end else begin
          // ALIGNED. Two invalid code groups in a row is a lost
          // alignment; one is a bit error the frame layer will catch.
          if (code_invalid) begin
            if (good_run_q == 16'd1) begin
              aligned_q  <= 1'b0;
              align_lost <= 1'b1;
              converging <= 1'b0;
              converged  <= 1'b0;
              good_run_q <= '0;
              if (!(&c_align_losses)) c_align_losses <= c_align_losses + 1'b1;
            end else begin
              good_run_q <= good_run_q + 16'd1;
            end
          end else begin
            good_run_q <= '0;
          end
 
          // THE CONVERGENCE WINDOW. Disparity errors inside it are
          // EXPECTED -- the receiver's state is catching up with the
          // transmitter's, and the encoding drives it there. They are
          // counted separately and they are not faults.
          if (converging) begin
            converge_q <= converge_q + 16'd1;
 
            if (disparity_error) begin
              if (!(&c_disparity_errors_in_window))
                c_disparity_errors_in_window <= c_disparity_errors_in_window + 1'b1;
 
            end else if (converge_q > 16'd8) begin
              // Eight clean code groups: the states agree.
              converging        <= 1'b0;
              converged         <= 1'b1;
              codes_to_converge <= converge_q;
              if (converge_q > worst_convergence)
                worst_convergence <= converge_q;
            end
 
            if (converge_q == CONVERGE_CODES) begin
              // The window expired and disparity is STILL wrong. Now it
              // is a fault, and it is a different fault from every
              // disparity error inside the window.
              converging              <= 1'b0;
              convergence_failed      <= 1'b1;
              ever_convergence_failed <= 1'b1;
            end
 
          end else if (converged && disparity_error) begin
            // STEADY-STATE disparity error. A genuine fault: the two
            // states had agreed and no longer do.
            if (!(&c_disparity_errors_steady))
              c_disparity_errors_steady <= c_disparity_errors_steady + 1'b1;
          end
        end
      end
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// Compares the PHY's continuous report against the MAC's actual
// configuration, and reports disagreement.
//
// WHY THIS EXISTS. Section 7 established that a link with an SGMII
// interface has TWO configuration events:
//   1. the cable-side negotiation between two PHYs, which is a real
//      negotiation with Chapter 9.2's failure modes;
//   2. the near PHY REPORTING the outcome to its MAC.
//
// And a MAC can be forced -- configured by software to a fixed speed
// and duplex, decoding the /C/ ordered sets and discarding them. So a
// third disagreement becomes possible, distinct from anything in
// Chapter 9.2: the cable is at 100 half, the PHY says so in every /C/
// set, and the MAC is forced to 1000 full and does not care.
//
// NOTHING ELSE IN THE SYSTEM COMPARES THE TWO. The PHY is right, the
// MAC is doing what it was told, and no counter anywhere is wrong.
module sgmii_status_reconciler
  import sgmii_pkg::*;
#(
  // Consecutive identical config words before the report is believed.
  // 802.3z's rule is three, and it is not defensive -- it is what
  // separates a report from a transient during the far end's own
  // negotiation.
  parameter int unsigned CONFIRM_COUNT = 3,
  parameter int unsigned CNT_W = 20
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  // The PHY's report, from Section 6.
  input  logic         config_valid,
  input  logic [15:0]  config_word,
  input  logic         reported_link,
  input  sgmii_speed_e reported_speed,
  input  logic         reported_duplex,
 
  // The MAC's actual configuration.
  input  logic         mac_forced,
  input  sgmii_speed_e mac_speed,
  input  logic         mac_duplex,
 
  output logic         report_confirmed,
  output sgmii_speed_e confirmed_speed,
  output logic         confirmed_duplex,
  output logic         confirmed_link,
 
  // The disagreements, each named separately because each is a
  // different work order.
  output logic speed_disagreement,
  output logic duplex_disagreement,
  // The MAC is transmitting on a link the PHY says is DOWN. Legal in
  // forced mode, always wrong in practice, and invisible everywhere else.
  output logic tx_on_reported_down_link,
 
  output logic [CNT_W-1:0] c_reports,
  output logic [CNT_W-1:0] c_speed_disagreements,
  output logic [CNT_W-1:0] c_duplex_disagreements,
  output logic             ever_disagreed,
  // The single most useful output: this MAC is ignoring its PHY.
  output logic             operating_on_forced_config
);
 
  logic [15:0] last_word_q;
  logic [3:0]  match_q;
 
  assign operating_on_forced_config = mac_forced && report_confirmed;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      last_word_q <= 16'd0; match_q <= 4'd0;
      report_confirmed <= 1'b0; confirmed_speed <= SPD_RESERVED;
      confirmed_duplex <= 1'b0; confirmed_link <= 1'b0;
      speed_disagreement <= 1'b0; duplex_disagreement <= 1'b0;
      tx_on_reported_down_link <= 1'b0;
      c_reports <= '0; c_speed_disagreements <= '0;
      c_duplex_disagreements <= '0; ever_disagreed <= 1'b0;
    end else if (clear) begin
      c_reports <= '0; c_speed_disagreements <= '0;
      c_duplex_disagreements <= '0;
      speed_disagreement <= 1'b0; duplex_disagreement <= 1'b0;
      // ever_disagreed survives -- a MAC that has ever ignored its PHY
      // is a configuration worth remembering.
    end else begin
      if (config_valid) begin
        if (config_word == last_word_q) begin
          if (match_q != 4'(CONFIRM_COUNT)) begin
            match_q <= match_q + 4'd1;
          end else if (!report_confirmed ||
                       (confirmed_speed  != reported_speed) ||
                       (confirmed_duplex != reported_duplex) ||
                       (confirmed_link   != reported_link)) begin
            // THREE IDENTICAL WORDS. Now the report is believed -- and
            // the rule matters because the far end's own negotiation
            // produces transient config words while it converges.
            report_confirmed <= 1'b1;
            confirmed_speed  <= reported_speed;
            confirmed_duplex <= reported_duplex;
            confirmed_link   <= reported_link;
            if (!(&c_reports)) c_reports <= c_reports + 1'b1;
          end
        end else begin
          match_q     <= 4'd0;
          last_word_q <= config_word;
        end
      end
 
      // THE COMPARISON. Both sides are internally correct; only the
      // pair is wrong, which is why nothing else can see it.
      if (report_confirmed) begin
        speed_disagreement  <= mac_forced && (mac_speed  != confirmed_speed);
        duplex_disagreement <= mac_forced && (mac_duplex != confirmed_duplex);
        tx_on_reported_down_link <= mac_forced && !confirmed_link;
 
        if (mac_forced && (mac_speed != confirmed_speed)) begin
          ever_disagreed <= 1'b1;
          if (!(&c_speed_disagreements))
            c_speed_disagreements <= c_speed_disagreements + 1'b1;
        end
        if (mac_forced && (mac_duplex != confirmed_duplex)) begin
          ever_disagreed <= 1'b1;
          if (!(&c_duplex_disagreements))
            c_duplex_disagreements <= c_duplex_disagreements + 1'b1;
        end
      end
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// Runs the SGMII configuration exchange to completion or to a bounded
// failure, using 802.3z's state machine with SGMII's timing.
//
// THE TIMER THAT CHANGED. 802.3z's link_timer is 10 ms, sized for a
// fibre link establishing itself. SGMII shortens it to 1.6 ms, because
// the event being reported -- a cable-side change the PHY has ALREADY
// completed -- should reach the MAC promptly.
//
//   10 ms  -> up to 10 ms of stale MAC configuration after a change
//   1.6 ms -> up to 1.6 ms
//
// THE ACKNOWLEDGE MECHANISM, and what it does NOT establish:
//   ACK means "I received your configuration word". It does not mean
//   "I agree", "I have applied it", or "we are both configured the
//   same". Section 12's reconciler exists because ACK establishes
//   receipt and nothing more.
module sgmii_link_timer
  import sgmii_pkg::*;
#(
  parameter int unsigned CLK_MHZ = 125,
  parameter int unsigned CNT_W   = 16
) (
  input  logic clk,
  input  logic rst_n,
 
  input  logic restart,
  input  logic aligned,
  input  logic config_valid,
  input  logic partner_ack,        // the far side's ACK bit
 
  output logic        send_config,
  output logic        send_ack,
  output logic        exchange_complete,
  output logic        exchange_timed_out,
  output logic [2:0]  exchange_state,
 
  output logic [CNT_W-1:0] c_exchanges,
  output logic [CNT_W-1:0] c_timeouts,
  output logic [CNT_W-1:0] c_restarts,
  // How long the last successful exchange took, in microseconds. A
  // link that consistently completes near the timer is a link one
  // disturbance away from not completing.
  output logic [CNT_W-1:0] last_exchange_us,
  output logic [CNT_W-1:0] worst_exchange_us,
  output logic             ever_timed_out
);
 
  localparam int unsigned TICKS_PER_US = CLK_MHZ;
  localparam int unsigned LINK_TICKS   = LINK_TIMER_US * CLK_MHZ;
 
  typedef enum logic [2:0] {
    X_IDLE, X_WAIT_ALIGN, X_EXCHANGE, X_ACK_WAIT, X_DONE, X_FAILED
  } xstate_e;
 
  xstate_e     st_q;
  logic [31:0] timer_q;
  logic [31:0] us_q;
  logic [15:0] us_count_q;
 
  assign exchange_state = st_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      st_q <= X_IDLE; timer_q <= '0; us_q <= '0; us_count_q <= '0;
      send_config <= 1'b0; send_ack <= 1'b0;
      exchange_complete <= 1'b0; exchange_timed_out <= 1'b0;
      c_exchanges <= '0; c_timeouts <= '0; c_restarts <= '0;
      last_exchange_us <= '0; worst_exchange_us <= '0;
      ever_timed_out <= 1'b0;
    end else begin
      exchange_complete  <= 1'b0;
      exchange_timed_out <= 1'b0;
 
      // A free-running microsecond counter, so the exchange duration is
      // reported in a unit a human can compare against 1600.
      if (us_q == 32'(TICKS_PER_US - 1)) begin
        us_q       <= '0;
        us_count_q <= us_count_q + 16'd1;
      end else begin
        us_q <= us_q + 1'b1;
      end
 
      if (restart) begin
        st_q        <= X_WAIT_ALIGN;
        timer_q     <= '0;
        us_count_q  <= '0;
        send_config <= 1'b0;
        send_ack    <= 1'b0;
        if (!(&c_restarts)) c_restarts <= c_restarts + 1'b1;
      end else begin
        unique case (st_q)
          X_IDLE: if (aligned) st_q <= X_WAIT_ALIGN;
 
          X_WAIT_ALIGN: begin
            // Nothing can be exchanged before alignment, because the
            // ordered sets that carry it are not decodable yet.
            if (aligned) begin
              st_q        <= X_EXCHANGE;
              send_config <= 1'b1;
              timer_q     <= '0;
              if (!(&c_exchanges)) c_exchanges <= c_exchanges + 1'b1;
            end
          end
 
          X_EXCHANGE: begin
            if (!aligned) begin
              st_q        <= X_WAIT_ALIGN;
              send_config <= 1'b0;
            end else if (config_valid) begin
              // A config word arrived: acknowledge it. ACK is RECEIPT,
              // not agreement -- and the distinction is the whole of
              // Section 12.
              send_ack <= 1'b1;
              st_q     <= X_ACK_WAIT;
              timer_q  <= '0;
            end else if (timer_q == 32'(LINK_TICKS)) begin
              st_q               <= X_FAILED;
              exchange_timed_out <= 1'b1;
              ever_timed_out     <= 1'b1;
              if (!(&c_timeouts)) c_timeouts <= c_timeouts + 1'b1;
            end else begin
              timer_q <= timer_q + 1'b1;
            end
          end
 
          X_ACK_WAIT: begin
            if (!aligned) begin
              st_q        <= X_WAIT_ALIGN;
              send_config <= 1'b0;
              send_ack    <= 1'b0;
            end else if (partner_ack) begin
              st_q              <= X_DONE;
              exchange_complete <= 1'b1;
              last_exchange_us  <= us_count_q;
              if (us_count_q > worst_exchange_us)
                worst_exchange_us <= us_count_q;
            end else if (timer_q == 32'(LINK_TICKS)) begin
              st_q               <= X_FAILED;
              exchange_timed_out <= 1'b1;
              ever_timed_out     <= 1'b1;
              if (!(&c_timeouts)) c_timeouts <= c_timeouts + 1'b1;
            end else begin
              timer_q <= timer_q + 1'b1;
            end
          end
 
          X_DONE: begin
            // Keep sending idle; a new config word restarts the
            // exchange, which is how a speed change propagates.
            send_config <= 1'b0;
            send_ack    <= 1'b0;
            if (config_valid) st_q <= X_EXCHANGE;
          end
 
          X_FAILED: begin
            send_config <= 1'b0;
            send_ack    <= 1'b0;
            st_q        <= X_WAIT_ALIGN;
          end
 
          default: st_q <= X_IDLE;
        endcase
      end
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// Checks the partner's conformance to the rules a serial stream cannot
// enforce structurally.
//
// A PARALLEL interface has rules about which pin may assert when, and
// most violations are electrically visible. A SERIAL stream has rules
// about which code group may FOLLOW which, and every violation is a
// perfectly valid code group in the wrong place.
//
// THE FIVE ORDERING RULES:
//   1. /S/ opens a frame; a second /S/ before /T/ is illegal.
//   2. /T/ closes one; a /T/ with no frame open is illegal.
//   3. /C/ ordered sets are ATOMIC pairs -- a K character followed by
//      its data byte, with nothing between.
//   4. Data code groups appear only inside a frame or as the second
//      half of a /C/ pair. Anywhere else they are orphans.
//   5. Idle must appear between frames. A stream with no idle at all
//      leaves the far end no room for clock compensation.
module sgmii_conformance_monitor
  import sgmii_pkg::*;
#(
  parameter int unsigned CNT_W = 20,
  // Minimum idle code groups required between frames.
  parameter int unsigned MIN_IDLE = 4
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic         aligned,
  input  logic         code_valid,
  input  logic         code_is_k,
  input  ordered_set_e code_kind,
  input  logic         code_invalid,
 
  output logic start_inside_frame,
  output logic terminate_no_frame,
  output logic split_ordered_set,
  output logic orphan_data_code,
  output logic insufficient_idle,
 
  output logic [CNT_W-1:0] c_start_inside_frame,
  output logic [CNT_W-1:0] c_terminate_no_frame,
  output logic [CNT_W-1:0] c_split_ordered_sets,
  output logic [CNT_W-1:0] c_orphan_data,
  output logic [CNT_W-1:0] c_insufficient_idle,
 
  // First cause, latched. A stream that has lost alignment produces a
  // violation on nearly every code group, and only the first one names
  // what happened.
  output logic       first_violation_valid,
  output logic [2:0] first_violation_kind,
  output logic       ever_violated
);
 
  logic       in_frame_q;
  logic       in_pair_q;
  logic [7:0] idle_run_q;
  logic       any_c;
  logic [2:0] kind_c;
 
  always_comb begin
    any_c  = 1'b0;
    kind_c = 3'd0;
    if      (start_inside_frame) begin any_c = 1'b1; kind_c = 3'd0; end
    else if (terminate_no_frame) begin any_c = 1'b1; kind_c = 3'd1; end
    else if (split_ordered_set)  begin any_c = 1'b1; kind_c = 3'd2; end
    else if (orphan_data_code)   begin any_c = 1'b1; kind_c = 3'd3; end
    else if (insufficient_idle)  begin any_c = 1'b1; kind_c = 3'd4; end
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      in_frame_q <= 1'b0; in_pair_q <= 1'b0; idle_run_q <= 8'd0;
      start_inside_frame <= 1'b0; terminate_no_frame <= 1'b0;
      split_ordered_set <= 1'b0; orphan_data_code <= 1'b0;
      insufficient_idle <= 1'b0;
      c_start_inside_frame <= '0; c_terminate_no_frame <= '0;
      c_split_ordered_sets <= '0; c_orphan_data <= '0;
      c_insufficient_idle <= '0;
      first_violation_valid <= 1'b0; first_violation_kind <= 3'd0;
      ever_violated <= 1'b0;
    end else if (clear) begin
      c_start_inside_frame <= '0; c_terminate_no_frame <= '0;
      c_split_ordered_sets <= '0; c_orphan_data <= '0;
      c_insufficient_idle <= '0; first_violation_valid <= 1'b0;
      // ever_violated survives.
    end else begin
      start_inside_frame <= 1'b0;
      terminate_no_frame <= 1'b0;
      split_ordered_set  <= 1'b0;
      orphan_data_code   <= 1'b0;
      insufficient_idle  <= 1'b0;
 
      // Nothing is checked before alignment. An unaligned stream
      // violates every rule simultaneously, and reporting that is
      // noise rather than information.
      if (aligned && code_valid && !code_invalid) begin
        if (code_is_k) begin
          if (in_pair_q) begin
            // A K character where the second half of a /C/ or /I/ pair
            // was owed. The pair was SPLIT, which a parallel interface
            // has no equivalent of.
            split_ordered_set <= 1'b1;
            if (!(&c_split_ordered_sets))
              c_split_ordered_sets <= c_split_ordered_sets + 1'b1;
          end
          in_pair_q <= 1'b0;
 
          unique case (code_kind)
            K_START: begin
              if (in_frame_q) begin
                start_inside_frame <= 1'b1;
                if (!(&c_start_inside_frame))
                  c_start_inside_frame <= c_start_inside_frame + 1'b1;
              end else if (idle_run_q < 8'(MIN_IDLE)) begin
                // A frame beginning with too little idle behind it
                // leaves the far end no room for clock compensation.
                insufficient_idle <= 1'b1;
                if (!(&c_insufficient_idle))
                  c_insufficient_idle <= c_insufficient_idle + 1'b1;
              end
              in_frame_q <= 1'b1;
              idle_run_q <= 8'd0;
            end
 
            K_TERMINATE: begin
              if (!in_frame_q) begin
                terminate_no_frame <= 1'b1;
                if (!(&c_terminate_no_frame))
                  c_terminate_no_frame <= c_terminate_no_frame + 1'b1;
              end
              in_frame_q <= 1'b0;
              idle_run_q <= 8'd0;
            end
 
            K_IDLE1, K_IDLE2: begin
              in_pair_q <= 1'b1;
              if (idle_run_q != 8'hFF) idle_run_q <= idle_run_q + 8'd1;
            end
 
            K_CONFIG1, K_CONFIG2: begin
              in_pair_q  <= 1'b1;
              idle_run_q <= 8'd0;
            end
 
            default: ;
          endcase
 
        end else begin
          // A DATA code group. Legal inside a frame, or as the second
          // half of an ordered set. Nowhere else.
          if (in_pair_q) begin
            in_pair_q <= 1'b0;
          end else if (!in_frame_q) begin
            orphan_data_code <= 1'b1;
            if (!(&c_orphan_data)) c_orphan_data <= c_orphan_data + 1'b1;
          end
        end
      end
 
      if (any_c) begin
        ever_violated <= 1'b1;
        if (!first_violation_valid) begin
          first_violation_valid <= 1'b1;
          first_violation_kind  <= kind_c;
        end
      end
    end
  end
 
endmodule

// P1. Ordered sets are ATOMIC. Once a K character of a pair is on the
// wire, its data byte follows immediately.
property p_ordered_set_atomic;
  @(posedge clk) disable iff (!rst_n)
  in_pair_q |=> !in_pair_q;
endproperty
a_ordered_set_atomic: assert property (p_ordered_set_atomic);
 
// P2. A frame octet offered during a pair is REPORTED, never inserted.
// A serial stream cannot interleave, so the collision must surface.
property p_pair_collision_reported;
  @(posedge clk) disable iff (!rst_n)
  (in_pair_q && octet_valid) |=> ordered_set_collision;
endproperty
a_pair_collision_reported: assert property (p_pair_collision_reported);
 
// P3. /S/ is emitted exactly once per frame_start.
property p_start_once_per_frame;
  @(posedge clk) disable iff (!rst_n)
  frame_start |=> (code_is_k && (code_kind == K_START));
endproperty
a_start_once_per_frame: assert property (p_start_once_per_frame);
 
// P4. Idle alternates I1/I2, so running disparity is driven toward
// neutral rather than allowed to walk.
property p_idle_alternates;
  @(posedge clk) disable iff (!rst_n)
  (code_is_k && (code_kind == K_IDLE1)) |-> ##[1:4]
    (code_is_k && (code_kind == K_IDLE2));
endproperty
a_idle_alternates: assert property (p_idle_alternates);
 
// P5. Config sets alternate C1/C2, which is what carries a 16-bit word
// through an 8-bit channel.
property p_config_alternates;
  @(posedge clk) disable iff (!rst_n)
  (code_is_k && (code_kind == K_CONFIG1)) |-> ##[1:4]
    (code_is_k && (code_kind == K_CONFIG2));
endproperty
a_config_alternates: assert property (p_config_alternates);
 
// P6. The stream is never empty. A serial link must send something
// every 800 ps; there is no idle differential pair that is still up.
property p_stream_never_empty;
  @(posedge clk) disable iff (!rst_n)
  code_valid;
endproperty
a_stream_never_empty: assert property (p_stream_never_empty);

// P7. Nothing is classified before alignment. An unaligned 8B/10B
// stream decodes to plausible code groups meaning something else.
property p_nothing_before_alignment;
  @(posedge clk) disable iff (!rst_n)
  !aligned |-> (!octet_valid && !config_valid && !frame_start);
endproperty
a_nothing_before_alignment: assert property (p_nothing_before_alignment);
 
// P8. Alignment requires a comma AND a run of decodable code groups.
// A comma alone is not alignment, because misaligned streams produce
// comma-like patterns by chance.
property p_alignment_needs_confirmation;
  @(posedge clk) disable iff (!rst_n)
  $rose(aligned_q) |-> ($past(good_run_q) == ALIGN_CONFIRM - 16'd1);
endproperty
a_alignment_needs_confirmation: assert property (p_alignment_needs_confirmation);
 
// P9. A data code group outside a frame and outside an ordered set is
// REPORTED. The signature of alignment acquired at the wrong boundary.
property p_orphan_data_reported;
  @(posedge clk) disable iff (!rst_n)
  (aligned && code_valid && !code_is_k && !in_frame_q &&
   !expect_cfg_lo_q && !expect_cfg_hi_q) |=> orphan_data;
endproperty
a_orphan_data_reported: assert property (p_orphan_data_reported);
 
// P10. An invalid code group never yields an octet.
property p_invalid_code_yields_nothing;
  @(posedge clk) disable iff (!rst_n)
  code_invalid |=> !octet_valid;
endproperty
a_invalid_yields_nothing: assert property (p_invalid_code_yields_nothing);

// P11. Transmit holds each code group for exactly the replication
// factor. The only thing that varies with link speed.
property p_replication_factor_held;
  @(posedge clk) disable iff (!rst_n)
  (tx_code_valid && tx_code_ready) |=> (tx_hold_q == rep_c - 7'd1);
endproperty
a_replication_held: assert property (p_replication_factor_held);
 
// P12. THE RESYNCHRONISATION PROPERTY. The receive decimator emits on
// a code-group CHANGE, never on a count -- so a run of 9 or 11 caused
// by ordinary clock tolerance costs nothing.
property p_decimate_on_change;
  @(posedge clk) disable iff (!rst_n)
  dec_code_valid |-> ((rx_code_octet != rx_prev_octet_q) ||
                      (rx_code_is_k != rx_prev_k_q) || !rx_have_prev_q);
endproperty
a_decimate_on_change: assert property (p_decimate_on_change);
 
// P13. Exactly one code group is emitted per run.
property p_one_per_run;
  @(posedge clk) disable iff (!rst_n)
  dec_code_valid |=> !dec_code_valid;
endproperty
a_one_per_run: assert property (p_one_per_run);
 
// P14. A run wrong by a FACTOR is reported. Clock tolerance moves a run
// by one; a speed disagreement moves it by ten.
property p_run_anomaly_reported;
  @(posedge clk) disable iff (!rst_n)
  (dec_code_valid && rx_have_prev_q &&
   (rx_run_q > (rep_c + (rep_c >> 1)))) |-> run_length_anomaly;
endproperty
a_run_anomaly_reported: assert property (p_run_anomaly_reported);

// P15. THE PROPERTY THIS CHAPTER IS ABOUT. Disparity converges within
// the window -- not "is always correct", but "reaches correctness
// within a bound after alignment".
property p_disparity_converges;
  @(posedge clk) disable iff (!rst_n)
  $rose(converging) |-> ##[1:CONVERGE_CODES] (converged || convergence_failed);
endproperty
a_disparity_converges: assert property (p_disparity_converges);
 
// P16. Disparity errors are counted in the RIGHT bucket. Inside the
// window they are the mechanism working; outside it they are a fault.
property p_window_errors_bucketed;
  @(posedge clk) disable iff (!rst_n)
  (converging && disparity_error)
    |=> (c_disparity_errors_in_window > $past(c_disparity_errors_in_window));
endproperty
a_window_errors_bucketed: assert property (p_window_errors_bucketed);
 
// P17. And steady-state errors in the other bucket.
property p_steady_errors_bucketed;
  @(posedge clk) disable iff (!rst_n)
  (converged && !converging && disparity_error)
    |=> (c_disparity_errors_steady > $past(c_disparity_errors_steady));
endproperty
a_steady_errors_bucketed: assert property (p_steady_errors_bucketed);
 
// P18. Converging and converged are mutually exclusive states.
property p_convergence_states_exclusive;
  @(posedge clk) disable iff (!rst_n)
  !(converging && converged);
endproperty
a_convergence_states_exclusive: assert property (p_convergence_states_exclusive);
 
// P19. A failed convergence is DISTINCT from an error inside the
// window -- three outcomes, not two.
property p_convergence_failure_distinct;
  @(posedge clk) disable iff (!rst_n)
  convergence_failed |-> !converged;
endproperty
a_convergence_failure_distinct: assert property (p_convergence_failure_distinct);

// P20. A report is believed only after three identical config words.
// Not debouncing -- this is what separates a report from the far end's
// negotiation transient.
property p_report_needs_three;
  @(posedge clk) disable iff (!rst_n)
  $rose(report_confirmed) |-> ($past(match_q) == 4'(CONFIRM_COUNT));
endproperty
a_report_needs_three: assert property (p_report_needs_three);
 
// P21. A forced MAC disagreeing with a confirmed report is REPORTED.
// Both sides are internally correct; only the pair is wrong.
property p_disagreement_reported;
  @(posedge clk) disable iff (!rst_n)
  (report_confirmed && mac_forced && (mac_speed != confirmed_speed))
    |-> speed_disagreement;
endproperty
a_disagreement_reported: assert property (p_disagreement_reported);
 
// P22. The exchange terminates: complete or timed out, never neither.
property p_exchange_terminates;
  @(posedge clk) disable iff (!rst_n)
  $rose(send_config) |-> ##[1:$] (exchange_complete || exchange_timed_out ||
                                  !aligned);
endproperty
a_exchange_terminates: assert property (p_exchange_terminates);
 
// P23. Nothing is exchanged before alignment, because the ordered sets
// that carry it are not decodable yet.
property p_exchange_needs_alignment;
  @(posedge clk) disable iff (!rst_n)
  send_config |-> aligned;
endproperty
a_exchange_needs_alignment: assert property (p_exchange_needs_alignment);