Preamble and Start Frame Delimiter

preamble on the wire:  1010 1010  1010 1010  ...  (7 octets, 56 bits)
transitions:           every single bit period

// SYNTHESIZABLE. Transition-density measurement over the acquisition window.
//
// THIS DOES NOT MODEL CLOCK RECOVERY. Chapter 2.6 owns the loop and Chapter
// 3.3 §15 established why RTL cannot represent one: it is an analog control
// system, not logic.
//
// What RTL CAN measure is the EVIDENCE the loop was given. A preamble is
// supposed to present a transition every bit period; if it does not, the
// loop had less to work with than the design assumed, and that is a
// measurable, actionable fact about the transmitter or the path.
module preamble_transition_monitor #(
  // Bit periods over which density is measured -- the preamble's own length.
  parameter int unsigned WINDOW = 56,
  parameter int unsigned WIN_W  = $clog2(WINDOW + 1),
  parameter int unsigned CNT_W  = 20
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic bit_valid,
  input  logic bit_in,
  input  logic window_active,      // asserted while a preamble is expected
 
  // Transitions observed in the window that just closed. A healthy preamble
  // gives WINDOW-1 of them -- one fewer than the bit count, because the
  // first bit has no predecessor.
  output logic [WIN_W-1:0] window_transitions,
  output logic             window_valid,
 
  // Bits seen with no transition. On strict alternation this is zero, so
  // ANY non-zero value means the pattern was not what it should be.
  output logic [WIN_W-1:0] window_static_bits,
 
  // The worst window since reset, held. Survives `clear`: it is a property
  // of the installation, not of a measurement interval someone chose.
  output logic [WIN_W-1:0] worst_transition_count,
 
  output logic [CNT_W-1:0] c_windows,
  output logic [CNT_W-1:0] c_degraded_windows
);
 
  logic             prev_bit_q;
  logic             have_prev_q;
  logic [WIN_W-1:0] trans_q, static_q, count_q;
 
  function automatic logic [CNT_W-1:0] bump(input logic [CNT_W-1:0] v,
                                            input logic             en);
    bump = (en && !(&v)) ? (v + 1'b1) : v;   // saturating
  endfunction
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      prev_bit_q             <= 1'b0;
      have_prev_q            <= 1'b0;
      trans_q                <= '0;
      static_q               <= '0;
      count_q                <= '0;
      window_transitions     <= '0;
      window_static_bits     <= '0;
      window_valid           <= 1'b0;
      worst_transition_count <= '1;
      c_windows              <= '0;
      c_degraded_windows     <= '0;
    end else begin
      window_valid <= 1'b0;
 
      if (clear) begin
        c_windows          <= '0;
        c_degraded_windows <= '0;
        // worst_transition_count deliberately survives.
      end
 
      if (!window_active) begin
        trans_q     <= '0;
        static_q    <= '0;
        count_q     <= '0;
        have_prev_q <= 1'b0;
      end else if (bit_valid) begin
        if (have_prev_q) begin
          if (bit_in != prev_bit_q) trans_q  <= trans_q  + 1'b1;
          else                      static_q <= static_q + 1'b1;
        end
        prev_bit_q  <= bit_in;
        have_prev_q <= 1'b1;
 
        if (count_q == WIN_W'(WINDOW - 1)) begin
          window_transitions <= trans_q;
          window_static_bits <= static_q;
          window_valid       <= 1'b1;
          count_q            <= '0;
          trans_q            <= '0;
          static_q           <= '0;
 
          c_windows <= bump(c_windows, 1'b1);
          // A healthy preamble has exactly one static bit -- the delimiter's
          // break. More than that means the alternation itself was damaged.
          if (static_q > WIN_W'(1)) c_degraded_windows <= bump(c_degraded_windows, 1'b1);
          if (trans_q < worst_transition_count) worst_transition_count <= trans_q;
        end else begin
          count_q <= count_q + 1'b1;
        end
      end
    end
  end
 
endmodule

// SYNTHESIZABLE. Octet alignment from the delimiter, with evidence.
//
// The naive detector is one comparison: two consecutive identical bits means
// the delimiter. IT IS WRONG, because two identical bits occur in noise, in
// idle patterns, and in the tail of another station's activity.
//
// The EVIDENCE is the context, not the marker: a break at the end of a
// SUFFICIENT RUN of alternation. MIN_RUN is the whole trade --
//
//   larger  -> fewer false detections, but a shortened preamble is rejected
//   smaller -> tolerates a short preamble, but aligns on noise more often
//
// Section 12 shows why "shortened preamble" is the common case rather than
// the exceptional one, which is what makes this trade real.
package sfd_pkg;
  typedef enum logic [1:0] {
    A_IDLE,       // no run in progress
    A_RUNNING,    // accumulating alternation
    A_ALIGNED     // the break was seen with sufficient evidence
  } align_state_e;
endpackage
 
module octet_aligner
  import sfd_pkg::*;
#(
  // Bits of alternation required before a break is believed. The standard
  // preamble offers 55; a shortened one offers fewer, and Section 12
  // explains why that is normal rather than a fault.
  parameter int unsigned MIN_RUN = 16,
  parameter int unsigned RUN_W   = $clog2(MIN_RUN + 2),
  parameter int unsigned CNT_W   = 20
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic bit_valid,
  input  logic bit_in,
  input  logic carrier,           // the PHY reports signal present
 
  output align_state_e state,
  output logic         aligned,          // pulses on the octet boundary
  output logic [RUN_W-1:0] run_at_align,  // evidence behind this alignment
 
  // A break seen with INSUFFICIENT evidence. Not an error -- it is the
  // detector correctly declining -- but a rising count means the preamble
  // is arriving shorter than MIN_RUN, which Section 12 shows is a path
  // measurement rather than a fault.
  output logic             break_rejected,
  output logic [CNT_W-1:0] c_break_rejected,
 
  output logic [CNT_W-1:0] c_aligned,
  // The shortest run that was ever ACCEPTED. Trend it: a run that has
  // fallen from 55 to just above MIN_RUN means the path has gained
  // regenerations, and the next one will start rejecting frames.
  output logic [RUN_W-1:0] shortest_accepted_run
);
 
  align_state_e     state_q;
  logic             prev_q;
  logic             have_prev_q;
  logic [RUN_W-1:0] run_q;
 
  wire same_c = have_prev_q && (bit_in == prev_q);
 
  function automatic logic [CNT_W-1:0] bump(input logic [CNT_W-1:0] v,
                                            input logic             en);
    bump = (en && !(&v)) ? (v + 1'b1) : v;
  endfunction
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      state_q               <= A_IDLE;
      prev_q                <= 1'b0;
      have_prev_q           <= 1'b0;
      run_q                 <= '0;
      aligned               <= 1'b0;
      break_rejected        <= 1'b0;
      run_at_align          <= '0;
      c_aligned             <= '0;
      c_break_rejected      <= '0;
      shortest_accepted_run <= '1;
    end else begin
      aligned        <= 1'b0;
      break_rejected <= 1'b0;
 
      if (clear) begin
        c_aligned        <= '0;
        c_break_rejected <= '0;
        // shortest_accepted_run deliberately survives.
      end
 
      // Carrier loss resets everything. Alignment is per-frame and nothing
      // carries over -- which is the difference from Chapter 3.5's block
      // lock, acquired once per link and then maintained.
      if (!carrier) begin
        state_q     <= A_IDLE;
        run_q       <= '0;
        have_prev_q <= 1'b0;
      end else if (bit_valid) begin
        prev_q      <= bit_in;
        have_prev_q <= 1'b1;
 
        unique case (state_q)
          A_IDLE, A_RUNNING: begin
            if (!have_prev_q) begin
              run_q   <= '0;
              state_q <= A_RUNNING;
            end else if (!same_c) begin
              // Alternation continues: evidence accumulates.
              if (run_q != '1) run_q <= run_q + 1'b1;
              state_q <= A_RUNNING;
            end else begin
              // A break. Believe it only with enough evidence behind it.
              if (run_q >= RUN_W'(MIN_RUN)) begin
                state_q      <= A_ALIGNED;
                aligned      <= 1'b1;
                run_at_align <= run_q;
                c_aligned    <= bump(c_aligned, 1'b1);
                if (run_q < shortest_accepted_run) shortest_accepted_run <= run_q;
              end else begin
                // Correctly declining. The run restarts from here.
                break_rejected   <= 1'b1;
                c_break_rejected <= bump(c_break_rejected, 1'b1);
                run_q            <= '0;
                state_q          <= A_RUNNING;
              end
            end
          end
 
          A_ALIGNED: begin
            // Aligned for this frame. Stay until carrier drops.
          end
 
          default: state_q <= A_IDLE;
        endcase
      end
    end
  end
 
  assign state = state_q;
 
endmodule

P(false alignment at a given bit) = (1/2)^MIN_RUN × (1/2)
                                  = (1/2)^(MIN_RUN + 1)

MIN_RUN =  4  ->  (1/2)^5   = 1 in 32
MIN_RUN = 16  ->  (1/2)^17  = 1 in 131,072
MIN_RUN = 32  ->  (1/2)^33  = 1 in about 8.6 billion

// SYNTHESIZABLE INSTRUMENTATION.
//
// The preamble's length is a PATH MEASUREMENT, not a frame property. So
// this records a distribution rather than checking against a constant.
//
// What the distribution says:
//   tight at full length      -> a direct link, or store-and-forward hops
//   tight at a shorter value  -> a stable path with a known regeneration count
//   BROADENING over time      -> the path has changed, or a device is
//                                acquiring more slowly than it used to
//   creeping toward MIN_RUN   -> alignment will begin failing
//
// The last is the actionable one and it precedes any failure by months.
module preamble_length_histogram #(
  parameter int unsigned MAX_BITS = 64,
  parameter int unsigned BINS     = 8,          // 8 bits per bin
  parameter int unsigned BIN_W    = $clog2(BINS),
  parameter int unsigned CNT_W    = 20,
  parameter int unsigned MIN_RUN  = 16
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic                      align_event,
  input  logic [$clog2(MAX_BITS+1)-1:0] run_length,
 
  output logic [CNT_W-1:0] bin_count [BINS],
 
  // Shortest and longest ever accepted. Both survive `clear`: they describe
  // the installed path, not a measurement window.
  output logic [$clog2(MAX_BITS+1)-1:0] shortest_ever,
  output logic [$clog2(MAX_BITS+1)-1:0] longest_ever,
 
  // Margin between the shortest run seen and the requirement. THIS is the
  // number to alarm on -- it shrinks as the path gains regenerations, and it
  // reaches zero before any frame is rejected.
  output logic [$clog2(MAX_BITS+1)-1:0] run_margin,
  output logic                          margin_low
);
 
  function automatic logic [CNT_W-1:0] bump(input logic [CNT_W-1:0] v,
                                            input logic             en);
    bump = (en && !(&v)) ? (v + 1'b1) : v;
  endfunction
 
  wire [BIN_W-1:0] bin_c = BIN_W'(run_length >> 3);   // 8 bits per bin
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (int unsigned b = 0; b < BINS; b++) bin_count[b] <= '0;
      shortest_ever <= '1;
      longest_ever  <= '0;
    end else begin
      if (clear) begin
        for (int unsigned b = 0; b < BINS; b++) bin_count[b] <= '0;
        // shortest_ever and longest_ever deliberately survive.
      end else if (align_event) begin
        bin_count[bin_c] <= bump(bin_count[bin_c], 1'b1);
      end
 
      if (align_event) begin
        if (run_length < shortest_ever) shortest_ever <= run_length;
        if (run_length > longest_ever)  longest_ever  <= run_length;
      end
    end
  end
 
  always_comb begin
    run_margin = (shortest_ever > ($clog2(MAX_BITS+1))'(MIN_RUN))
               ? (shortest_ever - ($clog2(MAX_BITS+1))'(MIN_RUN))
               : '0;
    // Alarm well before zero. By the time margin reaches zero, frames are
    // already being rejected.
    margin_low = (run_margin < ($clog2(MAX_BITS+1))'(8));
  end
 
endmodule

// SYNTHESIZABLE INSTRUMENTATION.
//
// Three failures, one symptom ("no frames"), three different owners:
//
//   NO CARRIER          -> nothing is arriving. The PHY, the link, the far
//                          end. Chapter 3.8's ladder, below this layer.
//   CARRIER, NO ALIGN   -> a signal is present and no delimiter is found.
//                          A shortened preamble, a bit-order mismatch, or
//                          a MIN_RUN set too high for this path.
//   ALIGNED, NO FRAME   -> alignment succeeded and what followed was not a
//                          frame. Very often a FALSE alignment on noise.
//
// A single "no frames received" counter names none of them.
module preamble_telemetry #(
  parameter int unsigned CNT_W = 24,
  // Bit times of carrier without an alignment before it is called a stall.
  parameter int unsigned STALL_BITS = 4096,
  parameter int unsigned ST_W = $clog2(STALL_BITS + 1)
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic bit_valid,
  input  logic carrier,
  input  logic aligned,
  input  logic frame_parsed_ok,     // from Chapter 5.1's parser
  input  logic break_rejected,
 
  output logic [CNT_W-1:0] c_carrier_events,
  output logic [CNT_W-1:0] c_alignments,
  output logic [CNT_W-1:0] c_frames_ok,
  output logic [CNT_W-1:0] c_break_rejected,
 
  // Carrier present for a long time with no alignment. Points at the
  // preamble or the detector, not at the link.
  output logic             align_stall,
  output logic [CNT_W-1:0] c_align_stall,
 
  // Aligned, then the parser found no valid frame. The signature of a FALSE
  // alignment, and Section 7 explains why it happens.
  output logic             suspected_false_align,
  output logic [CNT_W-1:0] c_suspected_false_align,
 
  // First failure kind since reset, held. During an incident all three will
  // have counts and only ordering says which came first.
  output logic [1:0]       first_failure,
  output logic             first_failure_valid
);
 
  logic [ST_W-1:0] since_align_q;
  logic            carrier_q, aligned_q;
 
  function automatic logic [CNT_W-1:0] bump(input logic [CNT_W-1:0] v,
                                            input logic             en);
    bump = (en && !(&v)) ? (v + 1'b1) : v;
  endfunction
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      since_align_q           <= '0;
      carrier_q               <= 1'b0;
      aligned_q               <= 1'b0;
      c_carrier_events        <= '0;
      c_alignments            <= '0;
      c_frames_ok             <= '0;
      c_break_rejected        <= '0;
      c_align_stall           <= '0;
      c_suspected_false_align <= '0;
      align_stall             <= 1'b0;
      suspected_false_align   <= 1'b0;
      first_failure           <= '0;
      first_failure_valid     <= 1'b0;
    end else begin
      align_stall           <= 1'b0;
      suspected_false_align <= 1'b0;
 
      if (clear) begin
        c_carrier_events        <= '0;
        c_alignments            <= '0;
        c_frames_ok             <= '0;
        c_break_rejected        <= '0;
        c_align_stall           <= '0;
        c_suspected_false_align <= '0;
      end else begin
        c_carrier_events <= bump(c_carrier_events, carrier && !carrier_q);
        c_alignments     <= bump(c_alignments,     aligned);
        c_frames_ok      <= bump(c_frames_ok,      frame_parsed_ok);
        c_break_rejected <= bump(c_break_rejected, break_rejected);
      end
 
      carrier_q <= carrier;
      aligned_q <= aligned;
 
      // Carrier with no alignment for a long time.
      if (!carrier || aligned) begin
        since_align_q <= '0;
      end else if (bit_valid && (since_align_q != '1)) begin
        since_align_q <= since_align_q + 1'b1;
        if (since_align_q == ST_W'(STALL_BITS - 1)) begin
          align_stall   <= 1'b1;
          c_align_stall <= bump(c_align_stall, 1'b1);
          if (!first_failure_valid) begin
            first_failure       <= 2'd1;
            first_failure_valid <= 1'b1;
          end
        end
      end
 
      // Aligned and the parser then found nothing valid.
      if (aligned_q && !carrier && !frame_parsed_ok) begin
        suspected_false_align   <= 1'b1;
        c_suspected_false_align <= bump(c_suspected_false_align, 1'b1);
        if (!first_failure_valid) begin
          first_failure       <= 2'd2;
          first_failure_valid <= 1'b1;
        end
      end
    end
  end
 
endmodule

// SYNTHESIZABLE. Preamble generation, and the decision that shortens it.
//
// Emitting the pattern is trivial. The DECISION is not, and it is the
// origin of Section 8's mechanism:
//
//   REGENERATE -- emit a full-length preamble of our own. Downstream sees
//                 the full budget. Requires holding the frame until we are
//                 ready to transmit it, which is store-and-forward latency.
//
//   FORWARD    -- pass on what remains of the incoming preamble after we
//                 have taken what we needed for our own timing. Lower
//                 latency, and EVERY DOWNSTREAM DEVICE gets less budget.
//
// A cut-through device forwards, because it starts transmitting before the
// frame has finished arriving and therefore cannot have generated anything.
// That is Chapter 2.7 §5's latency-against-containment trade appearing again
// in a place it is rarely noticed -- it also trades away preamble budget.
module preamble_generator #(
  parameter int unsigned PREAMBLE_OCTETS = 7,
  parameter logic [7:0]  PREAMBLE_OCTET  = 8'h55,
  parameter logic [7:0]  SFD_OCTET       = 8'hD5,
  parameter int unsigned CNT_W           = 20,
  parameter int unsigned OCT_W           = $clog2(PREAMBLE_OCTETS + 2)
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic       frame_request,      // a frame is ready to send
  input  logic       cut_through,        // forwarding, not regenerating
  input  logic [OCT_W-1:0] inherited_octets,  // preamble left from ingress
  input  logic       out_ready,
 
  output logic       out_valid,
  output logic [7:0] out_octet,
  output logic       out_is_sfd,
  output logic       preamble_done,      // the delimiter has been sent
 
  // How many octets this transmission actually emitted. On a regenerating
  // path this is PREAMBLE_OCTETS; on a forwarding one it is whatever
  // survived, and that is what the next device downstream will measure.
  output logic [OCT_W-1:0] emitted_octets,
 
  // Frames forwarded with a preamble shorter than full length. THIS DEVICE
  // is the one shortening it, and this counter is the only place that fact
  // is visible -- the receiver downstream sees the effect and cannot see
  // the cause.
  output logic [CNT_W-1:0] c_forwarded_short,
  output logic [CNT_W-1:0] c_regenerated_full,
  // The shortest preamble this device has ever passed on. If a downstream
  // link is failing to align, this is the number that says whether this
  // device is responsible.
  output logic [OCT_W-1:0] shortest_emitted
);
 
  typedef enum logic [1:0] { G_IDLE, G_PREAMBLE, G_SFD, G_DONE } gen_state_e;
 
  gen_state_e      state_q;
  logic [OCT_W-1:0] count_q, target_q;
 
  function automatic logic [CNT_W-1:0] bump(input logic [CNT_W-1:0] v,
                                            input logic             en);
    bump = (en && !(&v)) ? (v + 1'b1) : v;   // saturating
  endfunction
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      state_q            <= G_IDLE;
      count_q            <= '0;
      target_q           <= '0;
      out_valid          <= 1'b0;
      out_octet          <= '0;
      out_is_sfd         <= 1'b0;
      preamble_done      <= 1'b0;
      emitted_octets     <= '0;
      c_forwarded_short  <= '0;
      c_regenerated_full <= '0;
      shortest_emitted   <= '1;
    end else begin
      preamble_done <= 1'b0;
 
      if (clear) begin
        c_forwarded_short  <= '0;
        c_regenerated_full <= '0;
        // shortest_emitted deliberately survives: it is a property of what
        // this device does, not of a measurement window.
      end
 
      unique case (state_q)
        G_IDLE: begin
          out_valid <= 1'b0;
          if (frame_request) begin
            // THE DECISION. Regenerating gives downstream the full budget
            // and costs the latency of holding the frame. Forwarding is
            // cheaper and spends someone else's margin.
            target_q  <= cut_through ? inherited_octets
                                     : OCT_W'(PREAMBLE_OCTETS);
            count_q   <= '0;
            state_q   <= G_PREAMBLE;
          end
        end
 
        G_PREAMBLE: if (out_ready) begin
          if (count_q >= target_q) begin
            state_q    <= G_SFD;
            out_valid  <= 1'b1;
            out_octet  <= SFD_OCTET;
            out_is_sfd <= 1'b1;
          end else begin
            out_valid  <= 1'b1;
            out_octet  <= PREAMBLE_OCTET;
            out_is_sfd <= 1'b0;
            count_q    <= count_q + 1'b1;
          end
        end
 
        G_SFD: if (out_ready) begin
          out_valid      <= 1'b0;
          out_is_sfd     <= 1'b0;
          preamble_done  <= 1'b1;
          emitted_octets <= count_q;
          state_q        <= G_DONE;
 
          c_forwarded_short  <= bump(c_forwarded_short,
                                     count_q < OCT_W'(PREAMBLE_OCTETS));
          c_regenerated_full <= bump(c_regenerated_full,
                                     count_q >= OCT_W'(PREAMBLE_OCTETS));
          if (count_q < shortest_emitted) shortest_emitted <= count_q;
        end
 
        G_DONE: state_q <= G_IDLE;
 
        default: state_q <= G_IDLE;
      endcase
    end
  end
 
endmodule

// ─── FRAME PROPERTY: the delimiter differs from the preamble in one bit ────
// The wire patterns are 10101010 and 10101011. Catches a delimiter constant
// transcribed without the bit-order conversion, which emits a pattern no
// conformant receiver recognises -- the link appears dead with a healthy
// signal.
property p_delimiter_is_one_bit_from_preamble;
  @(posedge clk) disable iff (!rst_n)
  1'b1 |-> ($countones(8'h55 ^ 8'hD5) == 1);
endproperty
 
// ─── Causation: alignment requires sufficient evidence ─────────────────────
// THE property of this chapter. Catches a detector that fires on the break
// alone, which aligns on noise, on idle, and on another station's tail --
// and then reads whatever follows as a destination address.
property p_align_requires_run;
  @(posedge clk) disable iff (!rst_n)
  aligned |-> (run_at_align >= MIN_RUN);
endproperty
 
// ─── Safety: an insufficient break is rejected, not accepted late ──────────
// Catches a detector that remembers a rejected break and accepts it once
// more evidence arrives -- which aligns on the wrong bit.
property p_rejected_break_restarts_run;
  @(posedge clk) disable iff (!rst_n)
  break_rejected |=> (run_q == 0);
endproperty
 
// ─── Safety: alignment does not survive carrier loss ───────────────────────
// Alignment is PER FRAME. Catches a design that carries it over, which is
// the difference from Chapter 3.5's block lock and produces a receiver that
// mis-aligns the first frame after an idle period.
property p_align_clears_on_carrier_loss;
  @(posedge clk) disable iff (!rst_n)
  !carrier |=> (state == A_IDLE);
endproperty
 
// ─── Conservation: a healthy preamble has exactly one static bit ───────────
// Strict alternation plus the delimiter's single break. Catches a damaged
// pattern, which is a TRANSMITTER or PATH fault observed at the receiver.
property p_one_static_bit_per_preamble;
  @(posedge clk) disable iff (!rst_n)
  window_valid |-> (window_static_bits <= 1);
endproperty
 
// ─── Conservation: transitions and static bits account for the window ──────
// Catches a bit counted as neither, which biases the density measurement in
// a way no downstream analysis can detect.
property p_window_accounting_closes;
  @(posedge clk) disable iff (!rst_n)
  window_valid |-> ((window_transitions + window_static_bits) == WINDOW - 1);
endproperty
 
// ─── Stability: the shortest accepted run never increases ──────────────────
// It is a historical minimum. Catches it being recomputed per window, which
// destroys the trend that is this chapter's early warning.
property p_shortest_run_monotone;
  @(posedge clk) disable iff (!rst_n)
  1'b1 |=> (shortest_accepted_run <= $past(shortest_accepted_run));
endproperty
 
// ─── Stability: historical extremes survive a clear ────────────────────────
// Catches them folded into the clear branch, destroying the record of what
// this path has ever delivered.
property p_extremes_survive_clear;
  @(posedge clk) disable iff (!rst_n)
  clear |=> ((shortest_ever <= $past(shortest_ever))
          && (longest_ever  >= $past(longest_ever)));
endproperty
 
// ─── Causation: the margin alarm precedes rejection ────────────────────────
// Catches an alarm set at zero margin, which fires only once frames are
// already being rejected -- an obituary rather than a warning.
property p_margin_alarm_has_headroom;
  @(posedge clk) disable iff (!rst_n)
  (run_margin == 0) |-> margin_low;
endproperty
 
// ─── Conservation: every alignment lands in exactly one histogram bin ──────
// Catches a binning path that drops entries, biasing the distribution that
// the trend depends on.
property p_alignment_binned_once;
  @(posedge clk) disable iff (!rst_n)
  align_event |=> (bin_count[$past(bin_c)] == $past(bin_count[$past(bin_c)]) + 1);
endproperty
 
// ─── Mutual exclusion: the three failure kinds are distinguished ───────────
// Catches a stall and a false alignment being counted together, which
// conflates two failures with different owners.
property p_failures_distinguished;
  @(posedge clk) disable iff (!rst_n)
  !(align_stall && suspected_false_align);
endproperty
 
// ─── Stability: the first failure kind is held ─────────────────────────────
// Catches it being overwritten by consequences of the first failure, which
// names an effect as the cause.
property p_first_failure_stable;
  @(posedge clk) disable iff (!rst_n)
  first_failure_valid |=> $stable(first_failure);
endproperty
 
// ─── Bounded response: a stall is eventually reported ──────────────────────
// Catches a stall detector that can be starved, leaving carrier present and
// no alignment with nothing recording it.
property p_stall_is_reported;
  @(posedge clk) disable iff (!rst_n)
  (carrier && !aligned && bit_valid) |-> ##[1:STALL_BITS+1] (align_stall || aligned || !carrier);
endproperty
 
// ─── Safety: the delimiter always follows the preamble ─────────────────────
// Catches a generator that can emit the delimiter early or omit it, either
// of which produces a stream no receiver aligns to.
property p_sfd_follows_preamble;
  @(posedge clk) disable iff (!rst_n)
  out_is_sfd |-> ($past(state_q) == G_PREAMBLE);
endproperty
 
// ─── Causation: forwarding mode inherits, regenerating mode does not ───────
// Catches a device configured to regenerate that forwards anyway, which
// spends downstream preamble budget while its configuration says otherwise.
property p_regenerate_emits_full;
  @(posedge clk) disable iff (!rst_n)
  (preamble_done && !$past(cut_through)) |-> (emitted_octets >= PREAMBLE_OCTETS);
endproperty