Frame Preemption (802.1Qbu / 802.3br)

guard_band  =  L_uninterruptible / R  +  2 × sync_error

// -----------------------------------------------------------------------
// preempt_pkg -- shared types for 802.1Qbu / 802.3br frame preemption.
// -----------------------------------------------------------------------
package preempt_pkg;

  // The Start mData Delimiter replaces the last octet of the preamble,
  // where 5.2's SFD sits. Its value says what follows.
  localparam logic [7:0] SMD_E  = 8'hD5;   // express -- the ordinary SFD
  localparam logic [7:0] SMD_V  = 8'h07;   // verify
  localparam logic [7:0] SMD_R  = 8'h19;   // response

  // Four SMD-S codes and four SMD-C codes, cycled so a receiver can
  // detect a lost fragment rather than silently concatenating.
  localparam logic [7:0] SMD_S [4] = '{8'hE6, 8'h4C, 8'h7F, 8'hB3};
  localparam logic [7:0] SMD_C [4] = '{8'h61, 8'h52, 8'h9E, 8'h2A};

  localparam int MIN_FRAG_OCTETS = 64;    // 7.3's runt threshold
  localparam int MCRC_OCTETS     = 4;

  typedef enum logic [1:0] {
    MAC_EXPRESS,        // never preempted, never fragmented
    MAC_PREEMPTABLE     // may be interrupted at a legal boundary
  } mac_kind_e;

  typedef enum logic [2:0] {
    SMD_KIND_EXPRESS, SMD_KIND_START, SMD_KIND_CONT,
    SMD_KIND_VERIFY,  SMD_KIND_RESPONSE, SMD_KIND_INVALID
  } smd_kind_e;

  // 6.3's residue for a good frame, and its complement for a
  // fragment terminated by an mCRC. Section 8.
  localparam logic [31:0] FCS_RESIDUE  = 32'hC704_DD7B;
  localparam logic [31:0] MCRC_RESIDUE = 32'h38FB_2284;

endpackage

// -----------------------------------------------------------------------
// dual_mac_mux -- arbitrates one PHY interface between an express MAC
// and a preemptable one, and performs the interruption itself.
//
// The express MAC is an ordinary 7.1 transmit path. The preemptable
// one must be able to STOP mid-frame and resume later with its state
// intact -- which is the whole difference.
// -----------------------------------------------------------------------
module dual_mac_mux
  import preempt_pkg::*;
(
  input  logic       clk,
  input  logic       rst_n,

  // Express MAC -- 7.1's transmit path, unchanged.
  input  logic       exp_valid,
  input  logic [7:0] exp_octet,
  input  logic       exp_sop,
  input  logic       exp_eop,
  output logic       exp_ready,

  // Preemptable MAC.
  input  logic       pre_valid,
  input  logic [7:0] pre_octet,
  input  logic       pre_sop,
  input  logic       pre_eop,
  output logic       pre_ready,

  // From section 10: may we cut here, and should we.
  input  logic       cut_legal,
  input  logic       cut_wanted,

  input  logic       preemption_enabled,   // section 13's handshake

  output logic       tx_valid,
  output logic [7:0] tx_octet,
  output logic       tx_sop,
  output logic       tx_eop,
  output logic       emit_mcrc,            // terminate this fragment
  output logic       resuming,             // the next SMD is a CONT

  output logic [31:0] c_preemptions,
  output logic [31:0] c_express_frames,
  output logic [31:0] c_fragments,
  output logic       express_waited_ns_valid,
  output logic [31:0] express_wait_ns
);

  typedef enum logic [2:0] {
    S_IDLE, S_EXPRESS, S_PREEMPTABLE, S_CUTTING, S_HELD
  } st_e;
  st_e st;

  logic [31:0] wait_cnt;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      st <= S_IDLE; wait_cnt <= '0;
      emit_mcrc <= 1'b0; resuming <= 1'b0;
      c_preemptions <= '0; c_express_frames <= '0; c_fragments <= '0;
      express_waited_ns_valid <= 1'b0; express_wait_ns <= '0;
    end else begin
      emit_mcrc <= 1'b0;
      express_waited_ns_valid <= 1'b0;

      unique case (st)
        S_IDLE: begin
          if (exp_valid && exp_sop) begin
            st <= S_EXPRESS;
            c_express_frames <= c_express_frames + 1;
          end else if (pre_valid && pre_sop) begin
            st <= S_PREEMPTABLE;
          end
        end

        S_EXPRESS: begin
          // Express frames are NEVER preempted. An express frame
          // cannot be interrupted by another express frame either --
          // there is only one express MAC.
          if (exp_valid && exp_eop) st <= S_IDLE;
        end

        S_PREEMPTABLE: begin
          wait_cnt <= wait_cnt + 1;
          if (cut_wanted && preemption_enabled) begin
            if (cut_legal) begin
              // Terminate this fragment with an mCRC and yield.
              emit_mcrc     <= 1'b1;
              st            <= S_CUTTING;
              c_preemptions <= c_preemptions + 1;
              c_fragments   <= c_fragments + 1;
            end
            // If the cut is not legal here -- section 11's 64-octet
            // floor -- we keep transmitting and the express frame
            // waits. That wait is the residual guard band.
          end else if (pre_valid && pre_eop) begin
            st          <= S_IDLE;
            c_fragments <= c_fragments + 1;
          end
        end

        S_CUTTING: begin
          // One cycle to let the mCRC leave, then the express MAC has
          // the wire.
          st                      <= S_EXPRESS;
          express_wait_ns         <= wait_cnt;
          express_waited_ns_valid <= 1'b1;
          wait_cnt                <= '0;
          resuming                <= 1'b1;
        end

        S_HELD: begin
          if (!exp_valid) st <= S_PREEMPTABLE;
        end
      endcase

      if ((st == S_EXPRESS) && exp_valid && exp_eop && resuming) begin
        st       <= S_PREEMPTABLE;
        resuming <= 1'b0;
      end
    end
  end

  assign tx_valid  = (st == S_EXPRESS) ? exp_valid
                   : (st == S_PREEMPTABLE) ? pre_valid : 1'b0;
  assign tx_octet  = (st == S_EXPRESS) ? exp_octet : pre_octet;
  assign tx_sop    = (st == S_EXPRESS) ? exp_sop   : pre_sop;
  assign tx_eop    = (st == S_EXPRESS) ? exp_eop   : pre_eop;
  assign exp_ready = (st == S_EXPRESS) || (st == S_IDLE);
  assign pre_ready = (st == S_PREEMPTABLE);

endmodule

// -----------------------------------------------------------------------
// smd_framer -- replaces 5.2's SFD with a Start mData Delimiter that
// says what kind of thing follows, and adds a fragment counter to
// continuation fragments.
//
// The SMD occupies the SFD's octet. Nothing is added to the frame's
// length -- which is why preemption does not change 8.3's efficiency.
// -----------------------------------------------------------------------
module smd_framer
  import preempt_pkg::*;
(
  input  logic       clk,
  input  logic       rst_n,

  input  logic       start,
  input  smd_kind_e  kind,
  input  logic [1:0] seq,              // cycles 0..3 across fragments
  input  logic [7:0] frag_count,       // continuation fragments only

  output logic       tx_valid,
  output logic [7:0] tx_octet,
  output logic       tx_sop,
  output logic       preamble_done,
  output logic [31:0] c_by_kind [6]
);

  logic [3:0] idx;
  logic       busy;

  // 5.2's preamble is seven 0x55 octets then the SFD. The SMD takes
  // the SFD's place, so the preamble's length is unchanged.
  localparam logic [7:0] PREAMBLE = 8'h55;

  function automatic logic [7:0] smd_of(input smd_kind_e k, input logic [1:0] s);
    case (k)
      SMD_KIND_EXPRESS:  smd_of = SMD_E;
      SMD_KIND_START:    smd_of = SMD_S[s];
      SMD_KIND_CONT:     smd_of = SMD_C[s];
      SMD_KIND_VERIFY:   smd_of = SMD_V;
      SMD_KIND_RESPONSE: smd_of = SMD_R;
      default:           smd_of = SMD_E;
    endcase
  endfunction

  always_ff @(posedge clk or negedge rst_n) begin
    int i;
    if (!rst_n) begin
      idx <= '0; busy <= 1'b0; preamble_done <= 1'b0;
      for (i = 0; i < 6; i++) c_by_kind[i] <= '0;
    end else begin
      preamble_done <= 1'b0;

      if (start && !busy) begin
        busy <= 1'b1; idx <= '0;
        c_by_kind[kind] <= c_by_kind[kind] + 1;
      end else if (busy) begin
        // A continuation fragment carries one extra octet after the
        // SMD: the fragment count, so a receiver can detect a LOST
        // fragment rather than concatenating across a gap.
        if (idx == ((kind == SMD_KIND_CONT) ? 4'd8 : 4'd7)) begin
          busy          <= 1'b0;
          preamble_done <= 1'b1;
          idx           <= '0;
        end else begin
          idx <= idx + 1'b1;
        end
      end
    end
  end

  assign tx_valid = busy;
  assign tx_sop   = busy && (idx == 4'd0);
  assign tx_octet = (idx <  4'd7) ? PREAMBLE
                  : (idx == 4'd7) ? smd_of(kind, seq)
                  :                 frag_count;

endmodule

FCS   = CRC32(frame)
mCRC  = ~CRC32(fragment)

// -----------------------------------------------------------------------
// mcrc_generator -- produces both the per-fragment mCRC and the
// whole-frame FCS from one datapath.
//
// The two registers run over different spans:
//   frame_crc    covers every octet of the frame, across all fragments
//   fragment_crc covers only the octets of the CURRENT fragment
// The first terminates the LAST fragment; the second terminates every
// earlier one, complemented.
// -----------------------------------------------------------------------
module mcrc_generator
  import preempt_pkg::*;
(
  input  logic       clk,
  input  logic       rst_n,

  input  logic       frame_start,        // a new preemptable frame
  input  logic       fragment_start,     // a new fragment of it
  input  logic       octet_valid,
  input  logic [7:0] octet,

  input  logic       terminate_fragment, // section 10 decided to cut
  input  logic       terminate_frame,    // the frame's last octet

  output logic [31:0] mcrc_out,
  output logic [31:0] fcs_out,
  output logic        emit_valid,
  output logic        emit_is_mcrc,
  output logic [31:0] c_mcrc_emitted,
  output logic [31:0] c_fcs_emitted
);

  // 6.2's CRC-32: polynomial 0x04C11DB7, initial value all ones,
  // reflected input and output, final complement. Written here as a
  // bit-serial update for clarity; 6.4 unrolls it.
  localparam logic [31:0] POLY = 32'h04C1_1DB7;

  logic [31:0] frame_crc, frag_crc;

  function automatic logic [31:0] crc_step(input logic [31:0] c, input logic [7:0] d);
    logic [31:0] r;
    int i;
    begin
      r = c;
      for (i = 7; i >= 0; i--) begin
        if (r[31] ^ d[i]) r = {r[30:0], 1'b0} ^ POLY;
        else              r = {r[30:0], 1'b0};
      end
      crc_step = r;
    end
  endfunction

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      frame_crc <= 32'hFFFF_FFFF;
      frag_crc  <= 32'hFFFF_FFFF;
      emit_valid <= 1'b0; emit_is_mcrc <= 1'b0;
      mcrc_out <= '0; fcs_out <= '0;
      c_mcrc_emitted <= '0; c_fcs_emitted <= '0;
    end else begin
      emit_valid <= 1'b0;

      // The FRAME register is initialised once per frame and runs
      // across every fragment. The FRAGMENT register is reinitialised
      // at every fragment boundary.
      if (frame_start)    frame_crc <= 32'hFFFF_FFFF;
      if (fragment_start) frag_crc  <= 32'hFFFF_FFFF;

      if (octet_valid) begin
        frame_crc <= crc_step(frame_crc, octet);
        frag_crc  <= crc_step(frag_crc,  octet);
      end

      if (terminate_fragment) begin
        // The mCRC is the ordinary CRC of the fragment, COMPLEMENTED
        // a second time -- once by 6.2's final complement and once by
        // the mCRC rule. Section 6's two residues follow from this.
        mcrc_out       <= ~(~frag_crc);
        emit_valid     <= 1'b1;
        emit_is_mcrc   <= 1'b1;
        c_mcrc_emitted <= c_mcrc_emitted + 1;
      end else if (terminate_frame) begin
        fcs_out       <= ~frame_crc;
        emit_valid    <= 1'b1;
        emit_is_mcrc  <= 1'b0;
        c_fcs_emitted <= c_fcs_emitted + 1;
      end
    end
  end

endmodule

// -----------------------------------------------------------------------
// fragment_classifier -- decides what a received unit is.
//
// Three-way, where 6.3 had two. The SMD says what was CLAIMED and the
// residue says what was DELIVERED, and the classification is the
// conjunction -- which is what keeps a corrupt frame from being taken
// for a fragment.
// -----------------------------------------------------------------------
module fragment_classifier
  import preempt_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,

  input  logic        unit_end,
  input  logic [31:0] running_residue,    // 6.3's engine, unchanged
  input  smd_kind_e   smd_kind,
  input  logic [1:0]  smd_seq,
  input  logic [13:0] unit_octets,

  output logic        is_complete_frame,
  output logic        is_nonfinal_fragment,
  output logic        is_corrupt,
  output logic        is_runt,

  output logic [31:0] c_frames,
  output logic [31:0] c_fragments,
  output logic [31:0] c_corrupt,
  output logic [31:0] c_runts,
  output logic [31:0] c_smd_mismatch      // SMD and residue disagree
);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      is_complete_frame <= 1'b0; is_nonfinal_fragment <= 1'b0;
      is_corrupt <= 1'b0; is_runt <= 1'b0;
      c_frames <= '0; c_fragments <= '0; c_corrupt <= '0;
      c_runts <= '0; c_smd_mismatch <= '0;
    end else begin
      is_complete_frame    <= 1'b0;
      is_nonfinal_fragment <= 1'b0;
      is_corrupt           <= 1'b0;
      is_runt              <= 1'b0;

      if (unit_end) begin
        // Gate 0 -- 7.3's runt check, before anything else. A unit
        // shorter than 64 octets is not a fragment however its CRC
        // comes out, because the standard forbids emitting one.
        if (unit_octets < MIN_FRAG_OCTETS) begin
          is_runt <= 1'b1;
          c_runts <= c_runts + 1;
        end
        // A frame or a FINAL fragment: the FCS residue.
        else if (running_residue == FCS_RESIDUE) begin
          if ((smd_kind == SMD_KIND_EXPRESS) ||
              (smd_kind == SMD_KIND_START)   ||
              (smd_kind == SMD_KIND_CONT)) begin
            is_complete_frame <= 1'b1;
            c_frames          <= c_frames + 1;
          end else begin
            // A valid FCS on a VERIFY or RESPONSE unit is a protocol
            // error, not a frame.
            c_smd_mismatch <= c_smd_mismatch + 1;
          end
        end
        // A NON-FINAL fragment: the complemented residue.
        else if (running_residue == MCRC_RESIDUE) begin
          // And the SMD must agree that more is coming. A unit with
          // an mCRC residue and an EXPRESS delimiter is corrupt, not
          // a fragment -- section 9.
          if ((smd_kind == SMD_KIND_START) || (smd_kind == SMD_KIND_CONT)) begin
            is_nonfinal_fragment <= 1'b1;
            c_fragments          <= c_fragments + 1;
          end else begin
            is_corrupt     <= 1'b1;
            c_corrupt      <= c_corrupt + 1;
            c_smd_mismatch <= c_smd_mismatch + 1;
          end
        end
        else begin
          is_corrupt <= 1'b1;
          c_corrupt  <= c_corrupt + 1;
        end
      end
    end
  end

endmodule

P(corrupt frame accepted as a fragment)  ≈  (8/256) × 2⁻³²  ≈  7.3 × 10⁻¹²

// -----------------------------------------------------------------------
// preemption_decider -- decides whether the preemptable frame in
// flight may be, and should be, interrupted right now.
//
// Two independent questions with different answers:
//   LEGAL  -- section 11's 64-octet floor, on both sides of the cut
//   WANTED -- an express frame is waiting, or a gate is about to shut
// -----------------------------------------------------------------------
module preemption_decider
  import preempt_pkg::*;
#(
  parameter int LINE_RATE_MBPS = 1000
)(
  input  logic        clk,
  input  logic        rst_n,

  input  logic        pre_in_flight,
  input  logic [13:0] octets_sent,        // of this fragment
  input  logic [13:0] octets_remaining,   // of the frame

  input  logic        express_pending,
  input  logic [31:0] time_to_gate_close_ns,   // 17.2 section 7
  input  logic        preemption_enabled,

  output logic        cut_legal,
  output logic        cut_wanted,
  output logic [13:0] octets_until_legal,
  output logic [31:0] c_wanted_but_illegal,
  output logic [31:0] c_cut,
  output logic [31:0] worst_illegal_wait_ns
);

  logic [31:0] illegal_wait;

  always_comb begin
    // A cut is legal only if BOTH pieces will be at least 64 octets.
    // The fragment being closed needs 64 including its 4-octet mCRC;
    // the remainder needs 64 including its FCS. Section 11.
    cut_legal = pre_in_flight &&
                (octets_sent      >= 14'(MIN_FRAG_OCTETS)) &&
                (octets_remaining >= 14'(MIN_FRAG_OCTETS));

    octets_until_legal = (octets_sent >= 14'(MIN_FRAG_OCTETS))
                       ? 14'd0
                       : (14'(MIN_FRAG_OCTETS) - octets_sent);

    // Two reasons to want a cut, and the second is why this module
    // belongs to Module 17 rather than to Module 13.
    cut_wanted = preemption_enabled &&
                 (express_pending ||
                  (time_to_gate_close_ns <
                   ((32'(octets_remaining) * 8000) / LINE_RATE_MBPS)));
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      c_wanted_but_illegal <= '0; c_cut <= '0;
      worst_illegal_wait_ns <= '0; illegal_wait <= '0;
    end else begin
      if (cut_wanted && !cut_legal) begin
        c_wanted_but_illegal <= c_wanted_but_illegal + 1;
        illegal_wait         <= illegal_wait + 1;
        if (illegal_wait > worst_illegal_wait_ns)
          worst_illegal_wait_ns <= illegal_wait;
      end else begin
        illegal_wait <= '0;
      end

      if (cut_wanted && cut_legal) c_cut <= c_cut + 1;
    end
  end

endmodule

L_uninterruptible = max(MIN_FRAG, shortest_preemptable_frame_that_cannot_be_cut)

// -----------------------------------------------------------------------
// reassembly_fsm -- rebuilds a preempted frame from its fragments.
//
// Three failure modes, each with its own counter, and all three
// produce a discarded frame rather than a corrupt one:
//   a lost fragment       -- the SMD sequence skips
//   an interleaved frame  -- an SMD-S arrives mid-reassembly
//   an abandoned frame    -- no continuation ever arrives
// -----------------------------------------------------------------------
module reassembly_fsm
  import preempt_pkg::*;
#(
  parameter int MAX_FRAME   = 1518,
  parameter int TIMEOUT_CYC = 500_000       // 1 ms at 500 MHz
)(
  input  logic        clk,
  input  logic        rst_n,

  input  logic        unit_valid,
  input  smd_kind_e   smd_kind,
  input  logic [1:0]  smd_seq,
  input  logic [7:0]  frag_count,
  input  logic        is_nonfinal_fragment,
  input  logic        is_complete_frame,
  input  logic [13:0] unit_octets,

  output logic        frame_out_valid,
  output logic [13:0] frame_out_octets,
  output logic        reassembling,

  output logic [31:0] c_reassembled,
  output logic [31:0] c_lost_fragment,
  output logic [31:0] c_interleaved,
  output logic [31:0] c_timed_out,
  output logic [31:0] c_oversize,
  output logic [7:0]  worst_fragments_seen
);

  logic [1:0]  expect_seq;
  logic [7:0]  expect_count;
  logic [13:0] accumulated;
  logic [31:0] age;
  logic [7:0]  frags_this_frame;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      reassembling <= 1'b0; expect_seq <= '0; expect_count <= '0;
      accumulated <= '0; age <= '0; frags_this_frame <= '0;
      frame_out_valid <= 1'b0; frame_out_octets <= '0;
      c_reassembled <= '0; c_lost_fragment <= '0;
      c_interleaved <= '0; c_timed_out <= '0; c_oversize <= '0;
      worst_fragments_seen <= '0;
    end else begin
      frame_out_valid <= 1'b0;

      // A reassembly that never completes must be abandoned, or one
      // lost final fragment stalls the receiver for ever.
      if (reassembling) begin
        age <= age + 1;
        if (age == TIMEOUT_CYC) begin
          reassembling <= 1'b0;
          accumulated  <= '0;
          c_timed_out  <= c_timed_out + 1;
        end
      end

      if (unit_valid) begin
        unique case (smd_kind)
          SMD_KIND_EXPRESS: begin
            // An express frame passes through untouched and does NOT
            // disturb an in-progress reassembly -- the two MACs are
            // independent all the way to the receiver.
            if (is_complete_frame) begin
              frame_out_valid  <= 1'b1;
              frame_out_octets <= unit_octets;
            end
          end

          SMD_KIND_START: begin
            // An SMD-S while already reassembling means the previous
            // frame's continuation never arrived. Discard it.
            if (reassembling) c_interleaved <= c_interleaved + 1;

            reassembling     <= is_nonfinal_fragment;
            accumulated      <= unit_octets;
            expect_seq       <= smd_seq + 2'd1;
            expect_count     <= 8'd1;
            age              <= '0;
            frags_this_frame <= 8'd1;

            // A START that is already complete is an unpreempted
            // frame that happened to be announced as preemptable.
            if (is_complete_frame) begin
              frame_out_valid  <= 1'b1;
              frame_out_octets <= unit_octets;
              c_reassembled    <= c_reassembled + 1;
            end
          end

          SMD_KIND_CONT: begin
            if (!reassembling) begin
              // A continuation with nothing to continue: its START
              // was lost.
              c_lost_fragment <= c_lost_fragment + 1;
            end else if ((smd_seq != expect_seq) ||
                         (frag_count != expect_count)) begin
              // The sequence skipped. Four SMD-C codes give a
              // detection window of three lost fragments -- section 5.
              c_lost_fragment <= c_lost_fragment + 1;
              reassembling    <= 1'b0;
              accumulated     <= '0;
            end else if ((accumulated + unit_octets) > 14'(MAX_FRAME)) begin
              c_oversize   <= c_oversize + 1;
              reassembling <= 1'b0;
              accumulated  <= '0;
            end else begin
              accumulated      <= accumulated + unit_octets;
              expect_seq       <= smd_seq + 2'd1;
              expect_count     <= expect_count + 8'd1;
              age              <= '0;
              frags_this_frame <= frags_this_frame + 8'd1;

              if (is_complete_frame) begin
                reassembling     <= 1'b0;
                frame_out_valid  <= 1'b1;
                frame_out_octets <= accumulated + unit_octets;
                c_reassembled    <= c_reassembled + 1;
                if (frags_this_frame + 8'd1 > worst_fragments_seen)
                  worst_fragments_seen <= frags_this_frame + 8'd1;
              end
            end
          end

          default: ;
        endcase
      end
    end
  end

endmodule

// -----------------------------------------------------------------------
// verify_response_fsm -- establishes that the link partner understands
// preemption before any fragment is transmitted.
//
// The shape is 15.3's LACP in miniature: a periodic assertion, a
// timeout, and a capability that stays DISABLED until confirmed.
// -----------------------------------------------------------------------
module verify_response_fsm
  import preempt_pkg::*;
#(
  parameter int VERIFY_PERIOD_CYC = 64_000_000,   // 128 ms at 500 MHz
  parameter int VERIFY_LIMIT      = 3
)(
  input  logic       clk,
  input  logic       rst_n,

  input  logic       cfg_preemption_requested,
  input  logic       link_up,

  input  logic       rx_verify,           // an SMD-V arrived
  input  logic       rx_response,         // an SMD-R arrived

  output logic       tx_verify,
  output logic       tx_response,
  output logic       preemption_enabled,
  output logic [2:0] state_out,
  output logic [31:0] c_verify_sent,
  output logic [31:0] c_verify_failed,
  output logic [31:0] c_responses_sent
);

  typedef enum logic [2:0] {
    V_DISABLED, V_INIT, V_VERIFYING, V_SUCCEEDED, V_FAILED
  } vstate_e;
  vstate_e st;

  logic [31:0] timer;
  logic [2:0]  attempts;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      st <= V_DISABLED; timer <= '0; attempts <= '0;
      tx_verify <= 1'b0; tx_response <= 1'b0;
      preemption_enabled <= 1'b0;
      c_verify_sent <= '0; c_verify_failed <= '0; c_responses_sent <= '0;
    end else begin
      tx_verify   <= 1'b0;
      tx_response <= 1'b0;

      // Responding is UNCONDITIONAL: a device that understands
      // preemption answers a verify even if it is not requesting it
      // itself. 15.3's passive/passive deadlock is avoided this way.
      if (rx_verify) begin
        tx_response      <= 1'b1;
        c_responses_sent <= c_responses_sent + 1;
      end

      if (!link_up || !cfg_preemption_requested) begin
        st                 <= V_DISABLED;
        preemption_enabled <= 1'b0;
        attempts           <= '0;
      end else begin
        unique case (st)
          V_DISABLED: begin
            st       <= V_INIT;
            timer    <= '0;
            attempts <= '0;
          end

          V_INIT: begin
            st            <= V_VERIFYING;
            tx_verify     <= 1'b1;
            timer         <= '0;
            attempts      <= 3'd1;
            c_verify_sent <= c_verify_sent + 1;
          end

          V_VERIFYING: begin
            timer <= timer + 1;
            if (rx_response) begin
              st                 <= V_SUCCEEDED;
              preemption_enabled <= 1'b1;
            end else if (timer == VERIFY_PERIOD_CYC) begin
              timer <= '0;
              if (attempts == VERIFY_LIMIT) begin
                // The partner does not answer. Preemption stays OFF,
                // which is the safe state: whole frames always work.
                st              <= V_FAILED;
                c_verify_failed <= c_verify_failed + 1;
              end else begin
                attempts      <= attempts + 3'd1;
                tx_verify     <= 1'b1;
                c_verify_sent <= c_verify_sent + 1;
              end
            end
          end

          V_SUCCEEDED: begin
            preemption_enabled <= 1'b1;
          end

          V_FAILED: begin
            preemption_enabled <= 1'b0;
          end
        endcase
      end
    end
  end

  assign state_out = st;

endmodule

// -----------------------------------------------------------------------
// preempt_conformance_monitor -- one bit.
//
// It asserts the local invariants: fragments meet the 64-octet floor,
// express frames are never fragmented, the mCRC is emitted on every
// non-final fragment, and nothing was preempted before the handshake
// completed.
// -----------------------------------------------------------------------
module preempt_conformance_monitor
  import preempt_pkg::*;
(
  input  logic  clk,
  input  logic  rst_n,

  input  logic  fragment_below_floor,
  input  logic  remainder_below_floor,
  input  logic  express_was_fragmented,
  input  logic  mcrc_missing_on_fragment,
  input  logic  fcs_on_nonfinal_fragment,
  input  logic  preempted_before_verify,
  input  logic  smd_sequence_reused,       // same code twice running
  input  logic  cfg_all_classes_express,   // section 4's row three
  input  logic  cfg_no_class_express,      // nothing to preempt for

  output logic  conformant,
  output logic [15:0] fault_vector,
  output logic [31:0] c_violations
);

  logic v_frag, v_rem, v_exp, v_mcrc, v_fcs, v_early, v_seq;
  logic v_allexp, v_noexp;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      v_frag <= 1'b0; v_rem <= 1'b0; v_exp <= 1'b0; v_mcrc <= 1'b0;
      v_fcs <= 1'b0; v_early <= 1'b0; v_seq <= 1'b0;
      v_allexp <= 1'b0; v_noexp <= 1'b0; c_violations <= '0;
    end else begin
      // A fragment below the floor is discarded as a runt by every
      // receiver -- 7.3 -- so its frame never reassembles.
      if (fragment_below_floor)     begin v_frag  <= 1'b1; c_violations <= c_violations + 1; end
      if (remainder_below_floor)    begin v_rem   <= 1'b1; c_violations <= c_violations + 1; end
      if (express_was_fragmented)   begin v_exp   <= 1'b1; c_violations <= c_violations + 1; end
      if (mcrc_missing_on_fragment) begin v_mcrc  <= 1'b1; c_violations <= c_violations + 1; end
      if (fcs_on_nonfinal_fragment) begin v_fcs   <= 1'b1; c_violations <= c_violations + 1; end
      // Section 14: fragments to a partner that never answered.
      if (preempted_before_verify)  begin v_early <= 1'b1; c_violations <= c_violations + 1; end
      if (smd_sequence_reused)      begin v_seq   <= 1'b1; c_violations <= c_violations + 1; end

      // Standing configuration properties -- section 4's table.
      v_allexp <= cfg_all_classes_express;
      v_noexp  <= cfg_no_class_express;
    end
  end

  assign conformant = !(v_frag || v_rem || v_exp || v_mcrc || v_fcs ||
                        v_early || v_seq || v_allexp || v_noexp);
  assign fault_vector = {7'b0, v_noexp, v_allexp, v_seq, v_early,
                         v_fcs, v_mcrc, v_exp, v_rem, v_frag};

endmodule

// P1. An express frame is never fragmented. There is one express MAC
// and nothing can interrupt it.
property p_express_never_fragmented;
  @(posedge clk) disable iff (!rst_n)
  (st == S_EXPRESS) |-> !emit_mcrc;
endproperty

// P2. A preemptable frame yields only at a LEGAL cut.
property p_cut_only_when_legal;
  @(posedge clk) disable iff (!rst_n)
  emit_mcrc |-> $past(cut_legal);
endproperty

// P3. And only when preemption has been verified -- section 13.
property p_cut_only_when_enabled;
  @(posedge clk) disable iff (!rst_n)
  emit_mcrc |-> $past(preemption_enabled);
endproperty

// P4. After a cut the express MAC gets the wire.
property p_cut_yields_to_express;
  @(posedge clk) disable iff (!rst_n)
  (st == S_CUTTING) |=> (st == S_EXPRESS);
endproperty

// P5. And the preemptable frame resumes after the express one ends.
property p_preemptable_resumes;
  @(posedge clk) disable iff (!rst_n)
  (resuming && (st == S_EXPRESS) && exp_eop) |=> (st == S_PREEMPTABLE);
endproperty

// P6. The SMD occupies the SFD's octet. Nothing is added to the
// frame's length -- which is why preemption costs no bandwidth.
property p_smd_replaces_sfd;
  @(posedge clk) disable iff (!rst_n)
  (tx_valid && (idx == 4'd7)) |-> (tx_octet == smd_of(kind, seq));
endproperty

// P7. The preamble is otherwise unchanged -- seven 0x55 octets.
property p_preamble_unchanged;
  @(posedge clk) disable iff (!rst_n)
  (tx_valid && (idx < 4'd7)) |-> (tx_octet == 8'h55);
endproperty

// P8. Only continuation fragments carry a fragment count.
property p_count_only_on_cont;
  @(posedge clk) disable iff (!rst_n)
  (tx_valid && (idx == 4'd8)) |-> (kind == SMD_KIND_CONT);
endproperty

// P9. The SMD sequence advances by one across fragments, so a loss
// is detectable rather than silently concatenated.
property p_seq_advances;
  @(posedge clk) disable iff (!rst_n)
  (start && (kind == SMD_KIND_CONT)) |-> (seq == ($past(seq) + 2'd1));
endproperty

// P10. The frame CRC is initialised once per FRAME and the fragment
// CRC once per FRAGMENT. They cover different spans.
property p_two_spans;
  @(posedge clk) disable iff (!rst_n)
  fragment_start |=> (frag_crc == 32'hFFFF_FFFF);
endproperty

property p_frame_span_survives_fragments;
  @(posedge clk) disable iff (!rst_n)
  (fragment_start && !frame_start) |=> $stable(frame_crc);
endproperty

// P11. A non-final fragment is terminated by an mCRC and never by
// an FCS. The opposite delivers a truncated frame that CHECKS.
property p_nonfinal_gets_mcrc;
  @(posedge clk) disable iff (!rst_n)
  terminate_fragment |=> (emit_valid && emit_is_mcrc);
endproperty

// P12. And the final one by an FCS over the WHOLE frame.
property p_final_gets_fcs;
  @(posedge clk) disable iff (!rst_n)
  terminate_frame |=> (emit_valid && !emit_is_mcrc && (fcs_out == ~frame_crc));
endproperty

// P13. The two residues are complements -- which is why one engine
// distinguishes them. Section 6.
property p_residues_are_complements;
  @(posedge clk) disable iff (!rst_n)
  (MCRC_RESIDUE == ~FCS_RESIDUE);
endproperty

// P14. The runt check comes FIRST. A 40-octet unit is a runt whatever
// its residue -- 7.3, and section 11's floor exists so that it is.
property p_runt_check_is_first;
  @(posedge clk) disable iff (!rst_n)
  (unit_end && (unit_octets < MIN_FRAG_OCTETS))
    |=> (is_runt && !is_nonfinal_fragment && !is_complete_frame);
endproperty

// P15. A fragment requires BOTH the mCRC residue and a fragment SMD.
// Requiring both is what keeps 6.1's error budget.
property p_fragment_needs_both;
  @(posedge clk) disable iff (!rst_n)
  is_nonfinal_fragment |-> (($past(running_residue) == MCRC_RESIDUE) &&
                            (($past(smd_kind) == SMD_KIND_START) ||
                             ($past(smd_kind) == SMD_KIND_CONT)));
endproperty

// P16. A disagreement between the SMD and the residue is corruption,
// and it is counted.
property p_mismatch_is_corrupt;
  @(posedge clk) disable iff (!rst_n)
  (unit_end && (running_residue == MCRC_RESIDUE) &&
   (smd_kind == SMD_KIND_EXPRESS)) |=> (is_corrupt && $changed(c_smd_mismatch));
endproperty

// P17. Exactly one classification per unit.
property p_one_classification;
  @(posedge clk) disable iff (!rst_n)
  unit_end |=> ($countones({is_complete_frame, is_nonfinal_fragment,
                            is_corrupt, is_runt}) == 1);
endproperty

// P18. An express frame passes through without disturbing an
// in-progress reassembly. The two MACs are independent to the end.
property p_express_does_not_disturb;
  @(posedge clk) disable iff (!rst_n)
  (unit_valid && (smd_kind == SMD_KIND_EXPRESS) && reassembling)
    |=> $stable(accumulated);
endproperty

// P19. A sequence skip discards rather than concatenating.
property p_skip_discards;
  @(posedge clk) disable iff (!rst_n)
  (unit_valid && (smd_kind == SMD_KIND_CONT) && reassembling &&
   (smd_seq != expect_seq)) |=> (!reassembling && $changed(c_lost_fragment));
endproperty

// P20. A reassembly always terminates -- completed or timed out.
property p_reassembly_terminates;
  @(posedge clk) disable iff (!rst_n)
  $rose(reassembling) |-> ##[1:TIMEOUT_CYC+1] !reassembling;
endproperty

// P21. The reassembled length never exceeds the MTU.
property p_no_oversize;
  @(posedge clk) disable iff (!rst_n)
  frame_out_valid |-> (frame_out_octets <= 14'(MAX_FRAME));
endproperty

// P22. An SMD-S mid-reassembly abandons the old frame and starts a
// new one -- it never merges them.
property p_start_abandons;
  @(posedge clk) disable iff (!rst_n)
  (unit_valid && (smd_kind == SMD_KIND_START) && reassembling)
    |=> ($changed(c_interleaved) && (accumulated == $past(unit_octets)));
endproperty

// P23. Both sides of a cut meet the 64-octet floor.
property p_both_sides_meet_the_floor;
  @(posedge clk) disable iff (!rst_n)
  cut_legal |-> ((octets_sent >= 14'(MIN_FRAG_OCTETS)) &&
                 (octets_remaining >= 14'(MIN_FRAG_OCTETS)));
endproperty

// P24. A frame under 128 octets has no legal cut point.
property p_short_frames_not_preemptible;
  @(posedge clk) disable iff (!rst_n)
  ((octets_sent + octets_remaining) < 14'd128) |-> !cut_legal;
endproperty

// P25. The guard band's L_uninterruptible and the decider's floor are
// the SAME number. A design using two has a band that does not cover
// its own decider.
property p_band_matches_decider;
  @(posedge clk) disable iff (!rst_n)
  (GUARD_L_UNINTERRUPTIBLE == MIN_FRAG_OCTETS);
endproperty

// P26. Preemption stays disabled until a response arrives.
property p_disabled_until_response;
  @(posedge clk) disable iff (!rst_n)
  preemption_enabled |-> ($past(st) inside {V_SUCCEEDED, V_VERIFYING});
endproperty

// P27. A verify is answered unconditionally -- 15.3's passive/passive
// deadlock avoided by construction.
property p_verify_always_answered;
  @(posedge clk) disable iff (!rst_n)
  rx_verify |=> tx_response;
endproperty

// P28. Failure leaves preemption OFF, which is the safe direction:
// whole frames always work.
property p_fails_closed;
  @(posedge clk) disable iff (!rst_n)
  (st == V_FAILED) |-> !preemption_enabled;
endproperty

// P29. A link event re-runs the handshake -- a remembered capability
// is the optimistic enable section 14 exists to prevent.
property p_link_event_reverifies;
  @(posedge clk) disable iff (!rst_n)
  $fell(link_up) |=> !preemption_enabled;
endproperty

// P30. Standing property: at least one class is express and not all
// of them are. Both extremes disable the mechanism.
property p_sensible_class_split;
  @(posedge clk) disable iff (!rst_n)
  (!cfg_all_classes_express && !cfg_no_class_express);
endproperty

// P31. conformant is exactly the conjunction it claims.
property p_conformant_definition;
  @(posedge clk) disable iff (!rst_n)
  conformant <-> (fault_vector == 16'h0000);
endproperty