10 Gigabit — 64B/66B, XGMII and the End of Shared Media

// SYNTHESIZABLE.
//
// Places frames onto XGMII, which is four byte lanes wide.
//
// XGMII, by the numbers:
//   32 data bits  = 4 lanes x 8 bits, one CONTROL bit per lane
//   10 Gb/s / 32  = 312.5 MT/s
//   312.5 / 2     = 156.25 MHz DDR clock
//   (8 bits at 10 Gb/s would have needed 1.25 GHz -- which is why
//    GMII's width could not simply be carried forward.)
//
// A byte's meaning depends on its control bit:
//   ctrl = 0 -- the byte is DATA
//   ctrl = 1 -- the byte is a CONTROL character:
//        /I/ 0x07 idle      /S/ 0xFB start
//        /T/ 0xFD terminate /E/ 0xFE error
//        /Q/ 0x9C sequence  (ordered set, lane 0 only)
//
// THE PLACEMENT RULE:
//   /S/ -- lane 0 ONLY
//   /T/ -- any lane
//   /I/ -- any lane
package xgmii_pkg;
 
  localparam int unsigned LANES = 4;
 
  localparam logic [7:0] XC_IDLE      = 8'h07;
  localparam logic [7:0] XC_START     = 8'hFB;
  localparam logic [7:0] XC_TERMINATE = 8'hFD;
  localparam logic [7:0] XC_ERROR     = 8'hFE;
  localparam logic [7:0] XC_SEQUENCE  = 8'h9C;
 
  // Minimum interframe gap, in bytes (Chapter 5.9). One XGMII transfer
  // carries 4 bytes, so 12 bytes is exactly 3 columns -- but only when
  // the frame's length is a multiple of 4.
  localparam int unsigned IPG_BYTES   = 12;
  localparam int unsigned BYTES_PER_COLUMN = 4;
 
endpackage
 
module xgmii_lane_encoder
  import xgmii_pkg::*;
#(
  parameter int unsigned CNT_W = 16
) (
  input  logic clk,
  input  logic rst_n,
 
  input  logic       frame_start,      // a frame's first byte is offered
  input  logic       frame_active,
  input  logic       frame_end,
  input  logic [1:0] last_lane,        // which lane holds the last byte
  input  logic [LANES-1:0][7:0] data_in,
 
  output logic [LANES-1:0][7:0] xgmii_d,
  output logic [LANES-1:0]      xgmii_c,
 
  // The MAC offered a frame start when the encoder was not on a lane-0
  // boundary. It is deferred, never placed off lane 0 -- and the count
  // is what makes the deferral visible.
  output logic             start_deferred,
  output logic [CNT_W-1:0] c_frames,
  output logic [CNT_W-1:0] c_start_deferrals
);
 
  logic sending_q;
  integer i;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      sending_q <= 1'b0; start_deferred <= 1'b0;
      c_frames <= '0; c_start_deferrals <= '0;
      for (i = 0; i < LANES; i = i + 1) begin
        xgmii_d[i] <= XC_IDLE;
        xgmii_c[i] <= 1'b1;
      end
    end else begin
      start_deferred <= 1'b0;
 
      // Default: all four lanes idle. Everything below overwrites.
      for (i = 0; i < LANES; i = i + 1) begin
        xgmii_d[i] <= XC_IDLE;
        xgmii_c[i] <= 1'b1;
      end
 
      if (frame_start && !sending_q) begin
        // START. Lane 0 carries /S/; lanes 1..3 carry the frame's first
        // three bytes. There is no other legal arrangement -- a start
        // on lane 2 is not a late start, it is an illegal one.
        xgmii_d[0] <= XC_START;
        xgmii_c[0] <= 1'b1;
        for (i = 1; i < LANES; i = i + 1) begin
          xgmii_d[i] <= data_in[i];
          xgmii_c[i] <= 1'b0;
        end
        sending_q <= 1'b1;
        if (!(&c_frames)) c_frames <= c_frames + 1'b1;
 
      end else if (frame_end && sending_q) begin
        // TERMINATE, on any lane. Lanes before it carry the frame's
        // last bytes; lanes after it are idle.
        for (i = 0; i < LANES; i = i + 1) begin
          if (i < int'(last_lane)) begin
            xgmii_d[i] <= data_in[i];
            xgmii_c[i] <= 1'b0;
          end else if (i == int'(last_lane)) begin
            xgmii_d[i] <= XC_TERMINATE;
            xgmii_c[i] <= 1'b1;
          end
        end
        sending_q <= 1'b0;
 
      end else if (sending_q && frame_active) begin
        for (i = 0; i < LANES; i = i + 1) begin
          xgmii_d[i] <= data_in[i];
          xgmii_c[i] <= 1'b0;
        end
 
      end else if (frame_start && sending_q) begin
        // A start offered while a frame is in flight. Defer and report;
        // placing it would emit a start inside a frame.
        start_deferred <= 1'b1;
        if (!(&c_start_deferrals))
          c_start_deferrals <= c_start_deferrals + 1'b1;
      end
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// Deficit idle count: keep the AVERAGE interframe gap at the standard's
// minimum when the gap can only be adjusted four bytes at a time.
//
// THE PROBLEM (Section 5):
//   The gap must be at least 12 bytes. A frame start must be on lane 0.
//   A frame whose length is not a multiple of 4 leaves 1 to 3 lanes of
//   its final column unusable, so the realised gap is 13, 14 or 15.
//
// THE MECHANISM:
//   Allow the transmitter to DELETE up to 3 idle bytes -- taking a
//   single gap below 12 -- provided it has previously ACCUMULATED that
//   many extra idle bytes. The deficit is bounded (0..3), so no gap can
//   be short unless an earlier one was long by at least as much.
//
//   The result: every individual gap is between 9 and 15 bytes, and the
//   long-run average is 12. Which preserves what Chapter 5.9's gap is
//   FOR -- receiver recovery time, on average -- while giving back the
//   capacity the lane rule was taking.
module xgmii_deficit_idle_handler
  import xgmii_pkg::*;
#(
  parameter int unsigned CNT_W = 16
) (
  input  logic clk,
  input  logic rst_n,
 
  input  logic       frame_ended,
  input  logic [1:0] end_remainder,     // frame_length mod 4
  input  logic       next_frame_waiting,
 
  output logic [3:0] gap_bytes,         // gap to emit for this frame
  output logic [1:0] deficit,           // 0..3, the running credit
  output logic       gap_shortened,
  output logic       gap_lengthened,
 
  // The average, tracked so the mechanism can be checked rather than
  // trusted: total idle bytes emitted against frames sent.
  output logic [CNT_W+4:0] total_gap_bytes,
  output logic [CNT_W-1:0] c_gaps
);
 
  // Idle bytes forced by the lane rule, given the frame's remainder.
  wire [1:0] forced_pad = (end_remainder == 2'd0) ? 2'd0
                                                  : 2'd(4) - end_remainder;
 
  logic [1:0] deficit_q;
  assign deficit = deficit_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      deficit_q <= 2'd0; gap_bytes <= 4'd12;
      gap_shortened <= 1'b0; gap_lengthened <= 1'b0;
      total_gap_bytes <= '0; c_gaps <= '0;
    end else begin
      gap_shortened  <= 1'b0;
      gap_lengthened <= 1'b0;
 
      if (frame_ended && next_frame_waiting) begin
        if (!(&c_gaps)) c_gaps <= c_gaps + 1'b1;
 
        if (forced_pad == 2'd0) begin
          // The frame ended on a column boundary. If credit has been
          // accumulated, SPEND it now -- this is the only kind of gap
          // that can be shortened, because it is the only one whose
          // length is not already forced.
          if (deficit_q != 2'd0) begin
            gap_bytes     <= 4'(IPG_BYTES) - 4'(deficit_q);
            deficit_q     <= 2'd0;
            gap_shortened <= 1'b1;
            total_gap_bytes <= total_gap_bytes +
                               (CNT_W+5)'(IPG_BYTES - int'(deficit_q));
          end else begin
            gap_bytes <= 4'(IPG_BYTES);
            total_gap_bytes <= total_gap_bytes + (CNT_W+5)'(IPG_BYTES);
          end
        end else begin
          // The lane rule forces extra idle. ACCUMULATE the excess as
          // credit, saturating -- an unbounded deficit would let a long
          // run of awkward lengths buy an arbitrarily short gap later,
          // which is not what the averaging is for.
          gap_bytes      <= 4'(IPG_BYTES) + 4'(forced_pad);
          gap_lengthened <= 1'b1;
          deficit_q      <= (deficit_q + forced_pad > 2'd3)
                              ? 2'd3 : deficit_q + forced_pad;
          total_gap_bytes <= total_gap_bytes +
                             (CNT_W+5)'(IPG_BYTES + int'(forced_pad));
        end
      end
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// Checks the legality of the control characters on a received XGMII
// stream, and REPORTS violations rather than assuming they cannot
// happen.
//
// This is a RECEIVE-side module, and the distinction matters more here
// than anywhere else in the chapter. On the transmit side, the
// placement rules are obligations this design must meet. On the receive
// side they are claims about a PEER -- and a peer can be wrong, can be
// mid-reset, or can be a link that is bit-slipped.
//
// So every rule below is DETECTED. None is assumed.
//
//   /S/ start     -- lane 0 only, and only when no frame is open
//   /T/ terminate -- any lane, and only when a frame is open
//   /I/ idle      -- any lane, and only between frames
//   /E/ error     -- any lane, always legal, always meaningful
//   /Q/ sequence  -- lane 0 only
//   any other control code -- reserved, and receiving one is an event
module xgmii_control_validator
  import xgmii_pkg::*;
#(
  parameter int unsigned CNT_W = 16
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic [LANES-1:0][7:0] xgmii_d,
  input  logic [LANES-1:0]      xgmii_c,
  input  logic                  valid,
 
  output logic       violation,
  output logic [2:0] violation_kind,
  output logic [1:0] violation_lane,
 
  // The FIRST violation, latched and held. A stream that has gone wrong
  // produces many; only the first one has a cause.
  output logic       first_violation_valid,
  output logic [2:0] first_violation_kind,
  output logic [1:0] first_violation_lane,
 
  output logic [CNT_W-1:0] c_violations,
  output logic             frame_open
);
 
  typedef enum logic [2:0] {
    V_NONE,
    V_START_OFF_LANE0,     // /S/ somewhere other than lane 0
    V_START_INSIDE_FRAME,  // /S/ while a frame is already open
    V_TERMINATE_NO_FRAME,  // /T/ with no frame open
    V_DATA_NO_FRAME,       // a data byte outside any frame
    V_RESERVED_CODE,       // a control byte that is not a defined code
    V_SEQUENCE_OFF_LANE0   // /Q/ somewhere other than lane 0
  } viol_e;
 
  logic open_q;
  assign frame_open = open_q;
 
  logic [2:0] kind_c;
  logic [1:0] lane_c;
  logic       viol_c;
  logic       open_n;
 
  always_comb begin
    viol_c = 1'b0;
    kind_c = 3'(V_NONE);
    lane_c = 2'd0;
    open_n = open_q;
 
    if (valid) begin
      for (int l = 0; l < LANES; l = l + 1) begin
        if (xgmii_c[l]) begin
          unique case (xgmii_d[l])
            XC_START: begin
              if (l != 0) begin
                // NOT clamped, NOT ignored. The stream is telling us
                // something the standard says cannot happen, and the
                // only useful response is to name it.
                viol_c = 1'b1; kind_c = 3'(V_START_OFF_LANE0); lane_c = 2'(l);
              end else if (open_q) begin
                viol_c = 1'b1; kind_c = 3'(V_START_INSIDE_FRAME); lane_c = 2'(l);
              end else begin
                open_n = 1'b1;
              end
            end
            XC_TERMINATE: begin
              if (!open_q && !open_n) begin
                viol_c = 1'b1; kind_c = 3'(V_TERMINATE_NO_FRAME); lane_c = 2'(l);
              end else begin
                open_n = 1'b0;
              end
            end
            XC_SEQUENCE: begin
              if (l != 0) begin
                viol_c = 1'b1; kind_c = 3'(V_SEQUENCE_OFF_LANE0); lane_c = 2'(l);
              end
            end
            XC_IDLE, XC_ERROR: ;   // legal on any lane, at any time
            default: begin
              viol_c = 1'b1; kind_c = 3'(V_RESERVED_CODE); lane_c = 2'(l);
            end
          endcase
        end else if (!open_q && !open_n) begin
          // A data byte with no frame open. Usually a bit slip, and it
          // is the violation that most often precedes all the others.
          viol_c = 1'b1; kind_c = 3'(V_DATA_NO_FRAME); lane_c = 2'(l);
        end
      end
    end
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      open_q <= 1'b0; violation <= 1'b0; violation_kind <= 3'(V_NONE);
      violation_lane <= 2'd0; first_violation_valid <= 1'b0;
      first_violation_kind <= 3'(V_NONE); first_violation_lane <= 2'd0;
      c_violations <= '0;
    end else begin
      open_q         <= open_n;
      violation      <= viol_c;
      violation_kind <= kind_c;
      violation_lane <= lane_c;
 
      if (clear) begin
        c_violations          <= '0;
        first_violation_valid <= 1'b0;
      end else if (viol_c) begin
        if (!(&c_violations)) c_violations <= c_violations + 1'b1;
        // FIRST CAUSE. A bit-slipped stream produces a violation every
        // transfer; the hundredth one describes the aftermath, and only
        // the first one describes what happened.
        if (!first_violation_valid) begin
          first_violation_valid <= 1'b1;
          first_violation_kind  <= kind_c;
          first_violation_lane  <= lane_c;
        end
      end
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// Watches XGMII for the failures that come specifically from being
// PARALLEL, which a serial interface cannot have.
//
// Four byte lanes on a board are four sets of traces with four sets of
// setup and hold margins. What goes wrong is not the protocol:
//
//   A LANE STUCK      -- one lane frozen at a value while the others
//                        move. Idle is 0x07, so a stuck-at-idle lane on
//                        an idle link looks perfectly healthy and is
//                        invisible until traffic starts.
//   A LANE INVERTED / SWAPPED -- lanes crossed on the board. The
//                        control bits still line up; only the data is
//                        rearranged, so the stream stays structurally
//                        legal and every frame fails its CRC.
//   CONTROL/DATA SKEW -- the control bit arriving a transfer away from
//                        the data byte it describes.
//
// The common property: NONE of these makes the stream illegal. They
// make it wrong. So they are found by watching for activity and
// agreement, not by checking rules.
module xgmii_lane_alignment_checker
  import xgmii_pkg::*;
#(
  parameter int unsigned WINDOW_BITS = 20,
  parameter int unsigned CNT_W = 16
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic [LANES-1:0][7:0] xgmii_d,
  input  logic [LANES-1:0]      xgmii_c,
  input  logic                  valid,
  input  logic                  frame_open,
 
  output logic [LANES-1:0] lane_stuck,
  output logic [LANES-1:0] lane_never_carried_data,
  output logic             window_valid,
  // All four lanes must leave idle together at a frame's start. If some
  // do and some do not, the lanes are not aligned with each other.
  output logic             partial_column,
  output logic [CNT_W-1:0] c_partial_columns,
  output logic [LANES-1:0] ever_stuck
);
 
  logic [WINDOW_BITS-1:0]  win_q;
  logic [LANES-1:0][7:0]   prev_d;
  logic [LANES-1:0]        changed_q;
  logic [LANES-1:0]        carried_data_q;
 
  integer i;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      win_q <= '0; window_valid <= 1'b0; changed_q <= '0;
      carried_data_q <= '0; lane_stuck <= '0; ever_stuck <= '0;
      lane_never_carried_data <= '0; partial_column <= 1'b0;
      c_partial_columns <= '0;
      for (i = 0; i < LANES; i = i + 1) prev_d[i] <= 8'h00;
    end else begin
      partial_column <= 1'b0;
 
      if (clear) begin
        win_q <= '0; window_valid <= 1'b0;
        changed_q <= '0; carried_data_q <= '0;
        lane_stuck <= '0; lane_never_carried_data <= '0;
        c_partial_columns <= '0;
        // ever_stuck is NOT cleared -- a lane that has been stuck is
        // evidence about the board, and the board did not change.
      end else if (valid) begin
        win_q  <= win_q + 1'b1;
        prev_d <= xgmii_d;
 
        for (i = 0; i < LANES; i = i + 1) begin
          if (xgmii_d[i] != prev_d[i]) changed_q[i] <= 1'b1;
          if (!xgmii_c[i])             carried_data_q[i] <= 1'b1;
        end
 
        // A start column must take ALL FOUR lanes out of idle together:
        // lane 0 carries /S/ and lanes 1..3 carry data. Anything else
        // is lanes that are not moving as one.
        if (xgmii_c[0] && (xgmii_d[0] == XC_START)) begin
          if (xgmii_c[1] || xgmii_c[2] || xgmii_c[3]) begin
            partial_column <= 1'b1;
            if (!(&c_partial_columns))
              c_partial_columns <= c_partial_columns + 1'b1;
          end
        end
 
        if (&win_q) begin
          window_valid <= 1'b1;
          for (i = 0; i < LANES; i = i + 1) begin
            // Stuck: a whole window with no change at all.
            lane_stuck[i] <= !changed_q[i];
            if (!changed_q[i]) ever_stuck[i] <= 1'b1;
            // Never carried data: a lane that has only ever been
            // control. On an idle link this is normal; with frames
            // flowing it means the lane is not connected.
            lane_never_carried_data[i] <= !carried_data_q[i];
          end
          changed_q      <= '0;
          carried_data_q <= '0;
        end
      end
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// Measures the three statistical claims 10 Gigabit rests on, because a
// statistic nobody samples is an assumption.
//
//   1. RUN LENGTH -- the scrambler makes a long run improbable, not
//      impossible. The design's clock recovery is specified against a
//      run bound it was never given. So MEASURE the longest run seen.
//   2. AVERAGE GAP -- deficit idle claims the mean interframe gap is
//      the standard's minimum. So COMPUTE the mean and compare.
//   3. BLOCK LOCK -- established by eliminating wrong offsets. A link
//      that relocks repeatedly is one whose elimination is marginal.
//      So COUNT relocks, and remember that it ever happened.
module xgmii_conformance_monitor
  import xgmii_pkg::*;
#(
  parameter int unsigned RUN_W = 8,
  parameter int unsigned CNT_W = 24,
  // The run length beyond which clock recovery has no margin left.
  parameter int unsigned RUN_ALARM = 8'd64
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic serial_bit,
  input  logic serial_valid,
 
  input  logic       gap_emitted,
  input  logic [3:0] gap_bytes,
 
  input  logic block_lock,
 
  output logic [RUN_W-1:0] longest_run,
  output logic             run_alarm,
 
  output logic [CNT_W-1:0] total_gap_bytes,
  output logic [CNT_W-1:0] c_gaps,
  output logic [CNT_W-1:0] c_relocks,
  // Sticky across clear: this link has lost block lock at least once.
  output logic             ever_lost_lock,
  output logic             ever_run_alarm
);
 
  logic                 prev_bit;
  logic [RUN_W-1:0]     run_q;
  logic                 lock_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      prev_bit <= 1'b0; run_q <= '0; longest_run <= '0;
      run_alarm <= 1'b0; total_gap_bytes <= '0; c_gaps <= '0;
      c_relocks <= '0; lock_q <= 1'b0;
      ever_lost_lock <= 1'b0; ever_run_alarm <= 1'b0;
    end else begin
      run_alarm <= 1'b0;
 
      if (clear) begin
        longest_run <= '0; total_gap_bytes <= '0;
        c_gaps <= '0; c_relocks <= '0;
        // ever_lost_lock and ever_run_alarm survive. They are the two
        // facts a later reader needs and the two a clear destroys.
      end else begin
 
        // 1. RUN LENGTH, on the serial stream.
        if (serial_valid) begin
          prev_bit <= serial_bit;
          if (serial_bit == prev_bit) begin
            if (!(&run_q)) run_q <= run_q + 1'b1;
            if ((run_q + 1'b1) > longest_run) longest_run <= run_q + 1'b1;
            if ((run_q + 1'b1) == RUN_W'(RUN_ALARM)) begin
              run_alarm      <= 1'b1;
              ever_run_alarm <= 1'b1;
            end
          end else begin
            run_q <= '0;
          end
        end
 
        // 2. AVERAGE GAP. Two counters, and the division is done by
        // whoever reads them -- which keeps a divider out of a path
        // that runs at line rate.
        if (gap_emitted) begin
          total_gap_bytes <= total_gap_bytes + CNT_W'(gap_bytes);
          if (!(&c_gaps)) c_gaps <= c_gaps + 1'b1;
        end
 
        // 3. BLOCK LOCK. Count re-acquisitions, not the state.
        lock_q <= block_lock;
        if (block_lock && !lock_q) begin
          if (!(&c_relocks)) c_relocks <= c_relocks + 1'b1;
        end
        if (!block_lock && lock_q) ever_lost_lock <= 1'b1;
      end
    end
  end
 
endmodule

// P1. A start character is ONLY ever emitted on lane 0. On the TX side
// this is a design obligation, and it is unconditionally assertable.
property p_tx_start_on_lane0;
  @(posedge clk) disable iff (!rst_n)
  !((xgmii_c[1] && (xgmii_d[1] == XC_START)) ||
    (xgmii_c[2] && (xgmii_d[2] == XC_START)) ||
    (xgmii_c[3] && (xgmii_d[3] == XC_START)));
endproperty
a_tx_start_on_lane0: assert property (p_tx_start_on_lane0);
 
// P2. A start column takes all four lanes out of idle together: /S/ on
// lane 0 and DATA on lanes 1 to 3. There is no partial start.
property p_tx_start_column_complete;
  @(posedge clk) disable iff (!rst_n)
  (xgmii_c[0] && (xgmii_d[0] == XC_START))
    |-> (!xgmii_c[1] && !xgmii_c[2] && !xgmii_c[3]);
endproperty
a_tx_start_column_complete: assert property (p_tx_start_column_complete);
 
// P3. A start is never emitted inside an open frame. The encoder defers
// instead, which is what start_deferred reports.
property p_tx_no_start_inside_frame;
  @(posedge clk) disable iff (!rst_n)
  (sending_q && frame_start) |-> start_deferred;
endproperty
a_tx_no_start_inside_frame: assert property (p_tx_no_start_inside_frame);
 
// P4. Every lane after the terminate character is idle. A data byte
// after /T/ is a byte the receiver has no frame to put in. Written per
// lane, because terminate is legal on all four.
generate
  for (genvar L = 0; L < LANES-1; L++) begin : g_after_terminate
    property p_tx_idle_after_terminate;
      @(posedge clk) disable iff (!rst_n)
      (xgmii_c[L] && (xgmii_d[L] == XC_TERMINATE))
        |-> (xgmii_c[L+1] && (xgmii_d[L+1] == XC_IDLE));
    endproperty
    a_tx_idle_after_terminate: assert property (p_tx_idle_after_terminate);
  end
endgenerate
 
// P5. A frame is opened before it is closed. Terminate with no open
// frame is a transmit-path bug, not a peer's problem.
property p_tx_terminate_needs_frame;
  @(posedge clk) disable iff (!rst_n)
  frame_end |-> sending_q;
endproperty
a_tx_terminate_needs_frame: assert property (p_tx_terminate_needs_frame);

// P6. The deficit is bounded. An unbounded credit would eventually
// authorise an arbitrarily short gap.
property p_deficit_bounded;
  @(posedge clk) disable iff (!rst_n)
  deficit <= 2'd3;
endproperty
a_deficit_bounded: assert property (p_deficit_bounded);
 
// P7. Every emitted gap sits in the band the mechanism permits: never
// shorter than the minimum less the maximum credit, never longer than
// the minimum plus the maximum forced padding.
property p_gap_within_band;
  @(posedge clk) disable iff (!rst_n)
  gap_emitted |-> ((gap_bytes >= 4'(IPG_BYTES - 3)) &&
                   (gap_bytes <= 4'(IPG_BYTES + 3)));
endproperty
a_gap_within_band: assert property (p_gap_within_band);
 
// P8. THE CREDIT PROPERTY. A gap is only shortened when credit exists,
// which is what makes this an average rather than a shortcut.
property p_shorten_needs_credit;
  @(posedge clk) disable iff (!rst_n)
  gap_shortened |-> ($past(deficit) != 2'd0);
endproperty
a_shorten_needs_credit: assert property (p_shorten_needs_credit);
 
// P9. Spending the credit empties it. Credit is not reusable, which is
// the difference between averaging and drifting.
property p_credit_spent_once;
  @(posedge clk) disable iff (!rst_n)
  gap_shortened |=> (deficit == 2'd0);
endproperty
a_credit_spent_once: assert property (p_credit_spent_once);
 
// P10. Credit only ever accrues from a gap that was FORCED long. It
// cannot be created by an idle link or by a frame that fitted exactly.
property p_credit_from_forced_padding;
  @(posedge clk) disable iff (!rst_n)
  (deficit > $past(deficit)) |-> $past(gap_lengthened);
endproperty
a_credit_from_padding: assert property (p_credit_from_forced_padding);

// P11. Every violation is REPORTED with a kind. A violation flag with
// no kind is a design that noticed and cannot say what.
property p_violation_has_kind;
  @(posedge clk) disable iff (!rst_n)
  violation |-> (violation_kind != 3'(V_NONE));
endproperty
a_violation_has_kind: assert property (p_violation_has_kind);
 
// P12. FIRST CAUSE. The first violation is latched and never
// overwritten -- because the hundredth describes the aftermath.
property p_first_violation_stable;
  @(posedge clk) disable iff (!rst_n)
  (first_violation_valid && !clear)
    |=> $stable({first_violation_kind, first_violation_lane});
endproperty
a_first_violation_stable: assert property (p_first_violation_stable);
 
// P13. A start off lane 0 on the RECEIVED stream is detected -- the
// receive-side counterpart of P1, and it is a DETECTION property
// rather than an assumption about the peer.
property p_rx_detects_start_off_lane0;
  @(posedge clk) disable iff (!rst_n)
  (valid && ((xgmii_c[1] && (xgmii_d[1] == XC_START)) ||
             (xgmii_c[2] && (xgmii_d[2] == XC_START)) ||
             (xgmii_c[3] && (xgmii_d[3] == XC_START))))
    |=> (violation && (violation_kind == 3'(V_START_OFF_LANE0)));
endproperty
a_rx_detects_start_off_lane0: assert property (p_rx_detects_start_off_lane0);
 
// P14. A reserved control code is detected rather than silently
// treated as one of the defined ones.
property p_rx_detects_reserved;
  @(posedge clk) disable iff (!rst_n)
  (valid && xgmii_c[0] &&
   !(xgmii_d[0] inside {XC_IDLE, XC_START, XC_TERMINATE,
                        XC_ERROR, XC_SEQUENCE}))
    |=> (violation && (violation_kind == 3'(V_RESERVED_CODE)));
endproperty
a_rx_detects_reserved: assert property (p_rx_detects_reserved);
 
// P15. frame_open tracks start and terminate and nothing else. A frame
// that opens without a start is a state machine that drifted.
property p_frame_open_needs_start;
  @(posedge clk) disable iff (!rst_n)
  $rose(frame_open) |-> $past(valid && xgmii_c[0] &&
                              (xgmii_d[0] == XC_START));
endproperty
a_frame_open_needs_start: assert property (p_frame_open_needs_start);
 
// P16. Sticky evidence survives clear. A lane that has been stuck is a
// fact about the board, and clearing a counter does not fix a board.
property p_ever_stuck_survives;
  @(posedge clk) disable iff (!rst_n)
  (|ever_stuck) |=> (|ever_stuck);
endproperty
a_ever_stuck_survives: assert property (p_ever_stuck_survives);
 
// P17. And so does the lock history, for the same reason.
property p_lock_history_survives;
  @(posedge clk) disable iff (!rst_n)
  ever_lost_lock |=> ever_lost_lock;
endproperty
a_lock_history_survives: assert property (p_lock_history_survives);