The PHY Layer

// SYNTHESIZABLE. A small block coder illustrating the two things every line
// code does: guarantee transitions, and control running disparity.
//
// NOT 4B/5B, 8B/10B or 64B/66B — the table is illustrative. Chapter 3.5
// owns the real codes and their normative mappings.
module block_coder #(
  parameter int unsigned IN_W  = 4,
  parameter int unsigned OUT_W = 5
) (
  input  logic clk,
  input  logic rst_n,
 
  input  logic             in_valid,
  input  logic [IN_W-1:0]  in_data,
  input  logic             in_control,   // a control code, not data
  output logic             in_ready,
 
  output logic             out_valid,
  output logic [OUT_W-1:0] out_code,
  input  logic             out_ready,
 
  // Running disparity: the cumulative excess of ones over zeros. The
  // channel cannot pass a sustained offset, so this must stay bounded.
  output logic signed [5:0] disparity,
  output logic              disparity_alarm
);
 
  // ILLUSTRATIVE table. Every entry has at least two transitions, which is
  // the transition-density guarantee — a receiver's timing recovery has
  // something to lock onto no matter what the data is.
  function automatic logic [OUT_W-1:0] encode(input logic [IN_W-1:0] d);
    case (d)
      4'h0: encode = 5'b11110; 4'h1: encode = 5'b01001;
      4'h2: encode = 5'b10100; 4'h3: encode = 5'b10101;
      4'h4: encode = 5'b01010; 4'h5: encode = 5'b01011;
      4'h6: encode = 5'b01110; 4'h7: encode = 5'b01111;
      4'h8: encode = 5'b10010; 4'h9: encode = 5'b10011;
      4'hA: encode = 5'b10110; 4'hB: encode = 5'b10111;
      4'hC: encode = 5'b11010; 4'hD: encode = 5'b11011;
      4'hE: encode = 5'b11100; default: encode = 5'b11101;
    endcase
  endfunction
 
  // A control code is a symbol that CANNOT appear in the data mapping. That
  // is how a receiver distinguishes "this is an idle marker" from "this is
  // the data value that happens to look like one" — and it is why a code
  // must have spare symbols. A code with no spare capacity cannot signal
  // anything out of band.
  localparam logic [OUT_W-1:0] CTRL_IDLE = 5'b00111;
 
  logic signed [5:0] disp_q;
  logic [OUT_W-1:0]  code_q;
  logic              v_q;
 
  assign in_ready  = !v_q || out_ready;
  assign out_valid = v_q;
  assign out_code  = code_q;
 
  wire [OUT_W-1:0] chosen = in_control ? CTRL_IDLE : encode(in_data);
  // Ones minus zeros for this symbol. Summed over time this is the DC
  // content the channel sees.
  wire signed [5:0] delta = 6'sd0 + 6'($countones(chosen)) - 6'(OUT_W - $countones(chosen));
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      v_q <= 1'b0; code_q <= '0; disp_q <= '0;
    end else begin
      if (v_q && out_ready) v_q <= 1'b0;
      if (in_valid && in_ready) begin
        code_q <= chosen;
        v_q    <= 1'b1;
        disp_q <= disp_q + delta;
      end
    end
  end
 
  assign disparity = disp_q;
  // A real code SELECTS between two representations of each value to hold
  // disparity bounded. This model only MEASURES it, and alarms when the
  // bound is exceeded — which makes the mechanism's absence visible rather
  // than pretending the simplification does not matter.
  assign disparity_alarm = (disp_q > 6'sd6) || (disp_q < -6'sd6);
 
endmodule

// SYNTHESIZABLE. Parallel to serial and back, in one clock domain.
//
// NOT a real PMA: a real serial side runs at WIDTH times the parallel rate
// and uses circuit techniques outside RTL. This is the digital shape.
module pma_serdes #(
  parameter int unsigned WIDTH = 10,
  // Which end goes first. A SPECIFICATION decision that both ends must
  // share — and the classic bring-up failure when they do not, because the
  // link comes up and every frame is garbled.
  parameter bit MSB_FIRST = 1'b1
) (
  input  logic clk,
  input  logic rst_n,
 
  // Transmit: parallel in, serial out.
  input  logic             tx_valid,
  input  logic [WIDTH-1:0] tx_word,
  output logic             tx_ready,
  output logic             serial_out,
  output logic             serial_active,
 
  // Receive: serial in, parallel out. Alignment is NOT solved here — this
  // block emits a word every WIDTH bits from wherever it started counting,
  // which is almost certainly the wrong boundary. Section 8 fixes that.
  input  logic             serial_in,
  input  logic             serial_valid,
  output logic             rx_valid,
  output logic [WIDTH-1:0] rx_word
);
 
  localparam int unsigned CNT_W = $clog2(WIDTH);
 
  // ── Transmit ───────────────────────────────────────────────────────────
  logic [WIDTH-1:0] tx_sr_q;
  logic [CNT_W-1:0] tx_cnt_q;
  logic             tx_busy_q;
 
  assign tx_ready = !tx_busy_q || (tx_cnt_q == CNT_W'(WIDTH - 1));
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      tx_sr_q <= '0; tx_cnt_q <= '0; tx_busy_q <= 1'b0;
    end else if (tx_valid && tx_ready) begin
      tx_sr_q  <= tx_word;
      tx_cnt_q <= '0;
      tx_busy_q <= 1'b1;
    end else if (tx_busy_q) begin
      // Shift toward whichever end goes first. The two cases are mirror
      // images and choosing wrongly is undetectable locally — both ends
      // must agree, and neither can tell alone.
      tx_sr_q  <= MSB_FIRST ? {tx_sr_q[WIDTH-2:0], 1'b0}
                            : {1'b0, tx_sr_q[WIDTH-1:1]};
      if (tx_cnt_q == CNT_W'(WIDTH - 1)) tx_busy_q <= 1'b0;
      else                               tx_cnt_q  <= tx_cnt_q + 1'b1;
    end
  end
 
  assign serial_out    = MSB_FIRST ? tx_sr_q[WIDTH-1] : tx_sr_q[0];
  assign serial_active = tx_busy_q;
 
  // ── Receive ────────────────────────────────────────────────────────────
  logic [WIDTH-1:0] rx_sr_q;
  logic [CNT_W-1:0] rx_cnt_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      rx_sr_q <= '0; rx_cnt_q <= '0;
    end else if (serial_valid) begin
      rx_sr_q  <= MSB_FIRST ? {rx_sr_q[WIDTH-2:0], serial_in}
                            : {serial_in, rx_sr_q[WIDTH-1:1]};
      rx_cnt_q <= (rx_cnt_q == CNT_W'(WIDTH - 1)) ? '0 : rx_cnt_q + 1'b1;
    end
  end
 
  // THE HONEST LIMITATION. A word is emitted every WIDTH bits from an
  // arbitrary starting point. Nothing here knows where a code group
  // actually begins — that is block synchronisation, and it is a SEARCH
  // (Chapter 2.2's discovery problem) rather than a conversion.
  assign rx_valid = serial_valid && (rx_cnt_q == CNT_W'(WIDTH - 1));
  assign rx_word  = rx_sr_q;
 
endmodule

// BEHAVIOURAL MODEL — not synthesisable as a real recovery loop.
//
// ABSTRACTION BOUNDARY, stated: a real CDR is a phase detector, a loop
// filter and a controlled oscillator, operating in continuous time. This
// model captures only the digital consequences a MAC-side designer must
// account for: acquisition takes time, lock is lost when transitions stop,
// and re-acquisition takes time again.
module cdr_behavioural #(
  // ILLUSTRATIVE. Real acquisition time depends on loop bandwidth and the
  // incoming signal, and is specified in the PHY's datasheet.
  parameter int unsigned LOCK_SYMBOLS   = 64,
  // The bounded run length a code guarantees. Exceeding it starves the
  // recovery loop — which is WHY line codes guarantee transition density.
  parameter int unsigned MAX_RUN_LENGTH = 5
) (
  input  logic clk,
  input  logic rst_n,
 
  input  logic signal_present,   // from the PMD: something is arriving
  input  logic rx_bit,
  input  logic rx_bit_valid,
 
  output logic clk_locked,
  output logic [7:0] lock_acquisitions,
  output logic [7:0] lock_losses,
  output logic [3:0] longest_run
);
 
  logic [7:0] lock_cnt_q;
  logic [3:0] run_q, longest_q;
  logic       last_bit_q, locked_q;
  logic [7:0] acq_q, loss_q;
 
  // Run length: consecutive identical bits. This is the quantity a line
  // code exists to bound, and tracking it here is what connects Section 3's
  // coding argument to a measurable consequence.
  wire same_as_last = (rx_bit == last_bit_q);
  wire run_too_long = (run_q >= 4'(MAX_RUN_LENGTH));
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      lock_cnt_q <= '0; run_q <= '0; longest_q <= '0;
      last_bit_q <= 1'b0; locked_q <= 1'b0; acq_q <= '0; loss_q <= '0;
    end else begin
      if (rx_bit_valid) begin
        last_bit_q <= rx_bit;
        run_q      <= same_as_last ? run_q + 1'b1 : '0;
        if (run_q > longest_q) longest_q <= run_q;
      end
 
      if (!signal_present) begin
        // No signal, no lock. Immediate, because there is nothing to track.
        if (locked_q && loss_q != 8'hFF) loss_q <= loss_q + 1'b1;
        locked_q   <= 1'b0;
        lock_cnt_q <= '0;
      end else if (run_too_long && locked_q) begin
        // Transitions stopped for longer than the code should ever allow.
        // A real loop drifts and eventually samples wrongly; this model
        // declares the loss, which is the digital consequence.
        if (loss_q != 8'hFF) loss_q <= loss_q + 1'b1;
        locked_q   <= 1'b0;
        lock_cnt_q <= '0;
      end else if (!locked_q && rx_bit_valid) begin
        // Acquisition takes time. That delay is why a link does not come up
        // instantly and why Chapter 2.1's link_up has a term for it.
        if (lock_cnt_q == 8'(LOCK_SYMBOLS - 1)) begin
          locked_q <= 1'b1;
          if (acq_q != 8'hFF) acq_q <= acq_q + 1'b1;
        end else lock_cnt_q <= lock_cnt_q + 1'b1;
      end
    end
  end
 
  assign clk_locked        = locked_q;
  assign lock_acquisitions = acq_q;
  assign lock_losses       = loss_q;
  assign longest_run       = longest_q;
 
endmodule

// SYNTHESIZABLE. Finds the code-group boundary by trying an offset,
// measuring how often it yields valid symbols, and shifting when it does
// not.
//
// NOT a standard's mechanism — Chapter 3.5 owns those. The structure is the
// content: hypothesis, evidence, commit, and re-verify.
module block_sync #(
  parameter int unsigned WIDTH      = 10,
  // How many consecutive valid symbols before declaring lock. Larger is
  // slower to lock and less likely to lock falsely.
  parameter int unsigned GOOD_LIMIT = 16,
  // How many invalid symbols before giving up the hypothesis.
  parameter int unsigned BAD_LIMIT  = 4
) (
  input  logic clk,
  input  logic rst_n,
 
  input  logic             sym_valid,
  input  logic [WIDTH-1:0] sym_data,
  input  logic             sym_legal,     // from the decoder: is this a
                                          // symbol the code can produce?
  output logic             shift_request, // try the next offset
  output logic             block_lock,
  output logic [$clog2(WIDTH)-1:0] offset,
  output logic [7:0]       lock_losses
);
 
  typedef enum logic [1:0] { S_HUNT, S_TEST, S_LOCKED } s_state_e;
  s_state_e state_q, state_d;
 
  logic [$clog2(GOOD_LIMIT+1)-1:0] good_q;
  logic [$clog2(BAD_LIMIT+1)-1:0]  bad_q;
  logic [$clog2(WIDTH)-1:0]        off_q;
  logic [7:0]                      loss_q;
 
  // THE EVIDENCE. A wrong offset slices code groups across their
  // boundaries, producing bit patterns the code cannot generate. Illegal
  // symbols are therefore the signal that the hypothesis is wrong — and
  // this is why a code needs INVALID symbols as well as spare valid ones.
  // A code in which every bit pattern were legal could not be synchronised
  // this way at all.
  always_comb begin
    state_d = state_q;
    case (state_q)
      S_HUNT: if (sym_valid) state_d = S_TEST;
      S_TEST: if (sym_valid && !sym_legal)      state_d = S_HUNT;
              else if (good_q == GOOD_LIMIT-1)  state_d = S_LOCKED;
      // Lock is not permanent. A locked receiver keeps checking, because a
      // channel that degrades will start producing illegal symbols and the
      // offset may need re-establishing.
      S_LOCKED: if (bad_q == BAD_LIMIT-1) state_d = S_HUNT;
      default: state_d = S_HUNT;
    endcase
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      state_q <= S_HUNT; good_q <= '0; bad_q <= '0; off_q <= '0; loss_q <= '0;
    end else begin
      state_q <= state_d;
 
      if (state_q == S_HUNT && state_d == S_TEST) good_q <= '0;
      else if (state_q == S_TEST && sym_valid)
        good_q <= sym_legal ? good_q + 1'b1 : '0;
 
      if (state_q != S_LOCKED)                    bad_q <= '0;
      else if (sym_valid)                         bad_q <= sym_legal ? '0 : bad_q + 1'b1;
 
      // Each failed hypothesis advances to the next offset. WIDTH offsets
      // exist and exactly one is right, so this terminates — a search that
      // could not exhaust its space would be a receiver that hangs.
      if (state_q == S_TEST && state_d == S_HUNT)
        off_q <= (off_q == $clog2(WIDTH)'(WIDTH-1)) ? '0 : off_q + 1'b1;
 
      if (state_q == S_LOCKED && state_d == S_HUNT && loss_q != 8'hFF)
        loss_q <= loss_q + 1'b1;
    end
  end
 
  assign shift_request = (state_q == S_TEST) && (state_d == S_HUNT);
  assign block_lock    = (state_q == S_LOCKED);
  assign offset        = off_q;
  assign lock_losses   = loss_q;
 
endmodule

// SYNTHESIZABLE. Absorbs a bounded frequency difference between the
// recovered receive clock and the local clock by deleting idle when the
// buffer fills and inserting it when the buffer empties.
//
// Chapter 4.4 owns this mechanism in depth; this shows its place in the PHY.
module elastic_buffer #(
  parameter int unsigned WIDTH = 10,
  parameter int unsigned DEPTH = 16,
  localparam int unsigned PTR_W = $clog2(DEPTH),
  localparam int unsigned CNT_W = $clog2(DEPTH + 1)
) (
  input  logic clk,
  input  logic rst_n,
 
  input  logic             wr_valid,
  input  logic [WIDTH-1:0] wr_data,
  input  logic             wr_is_idle,   // this symbol is deletable
 
  input  logic             rd_ready,
  output logic             rd_valid,
  output logic [WIDTH-1:0] rd_data,
 
  output logic [CNT_W-1:0] occupancy,
  output logic [15:0]      idles_deleted,
  output logic [15:0]      idles_inserted,
  output logic             overflow,
  output logic             underflow
);
 
  localparam logic [CNT_W-1:0] HIGH_MARK = CNT_W'((DEPTH * 3) / 4);
  localparam logic [CNT_W-1:0] LOW_MARK  = CNT_W'(DEPTH / 4);
  localparam logic [WIDTH-1:0] IDLE_SYM  = {WIDTH{1'b0}};  // ILLUSTRATIVE
 
  logic [WIDTH-1:0] mem_q [DEPTH];
  logic [PTR_W-1:0] wr_q, rd_q;
  logic [CNT_W-1:0] cnt_q;
  logic [15:0]      del_q, ins_q;
 
  wire full  = (cnt_q == CNT_W'(DEPTH));
  wire empty = (cnt_q == '0);
 
  // THE ADJUSTMENT, and both directions are needed because the offset can
  // have either sign. Idle is the ONLY symbol that may be added or removed,
  // because it carries no information — which is why the interframe gap is
  // a MINIMUM rather than a fixed value (Chapter 2.5 section 8).
  wire delete_now = wr_valid && wr_is_idle && (cnt_q >= HIGH_MARK);
  wire insert_now = rd_ready && empty;
 
  wire do_wr = wr_valid && !full && !delete_now;
  wire do_rd = rd_ready && !empty;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      wr_q <= '0; rd_q <= '0; cnt_q <= '0; del_q <= '0; ins_q <= '0;
    end else begin
      if (do_wr) begin
        mem_q[wr_q] <= wr_data;
        wr_q <= (wr_q == PTR_W'(DEPTH-1)) ? '0 : wr_q + 1'b1;
      end
      if (do_rd) rd_q <= (rd_q == PTR_W'(DEPTH-1)) ? '0 : rd_q + 1'b1;
 
      case ({do_wr, do_rd})
        2'b10:   cnt_q <= cnt_q + 1'b1;
        2'b01:   cnt_q <= cnt_q - 1'b1;
        default: cnt_q <= cnt_q;
      endcase
 
      if (delete_now && del_q != 16'hFFFF) del_q <= del_q + 1'b1;
      if (insert_now && ins_q != 16'hFFFF) ins_q <= ins_q + 1'b1;
    end
  end
 
  assign rd_valid  = !empty || insert_now;
  assign rd_data   = empty ? IDLE_SYM : mem_q[rd_q];
  assign occupancy = cnt_q;
 
  // These two must NEVER assert. If they do, the frequency offset exceeded
  // what the buffer can absorb, or the idle supply was insufficient — and
  // the consequence is corrupted data rather than merely degraded timing.
  assign overflow      = wr_valid && full && !wr_is_idle;
  assign underflow     = rd_ready && empty && !insert_now;
  assign idles_deleted = del_q;
  assign idles_inserted = ins_q;
 
endmodule

// SYNTHESIZABLE. Aggregates the PHY's own conditions into the terms
// Chapter 2.1's link_up consumes, and qualifies them so a MARGINAL link is
// distinguishable from a healthy one.
module phy_status #(
  // How long every condition must hold before the link is declared up.
  // Prevents a link that is oscillating from appearing usable.
  parameter int unsigned STABLE_SYMBOLS = 256,
  // Lock losses within the observation window that make a link marginal
  // even though it is currently up.
  parameter int unsigned MARGINAL_LOSSES = 4
) (
  input  logic clk,
  input  logic rst_n,
 
  input  logic signal_detect,   // PMD
  input  logic clk_locked,      // PMA
  input  logic block_lock,      // PCS
  input  logic lane_aligned,    // PCS
 
  input  logic [7:0] cdr_losses,
  input  logic [7:0] block_losses,
 
  output logic phy_ready,
  output logic phy_marginal,    // up, and should not be trusted
  output logic [1:0] lowest_failing   // which term fails first
);
 
  logic [$clog2(STABLE_SYMBOLS+1)-1:0] stable_q;
  logic ready_q;
 
  // ALL FOUR, and the order matters for diagnosis rather than for logic:
  // each depends on the ones below it, so the LOWEST failing term is the
  // cause and everything above it is a consequence. Chapter 2.1 section 15
  // builds the descent method on exactly this.
  wire all_ok = signal_detect && clk_locked && block_lock && lane_aligned;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      stable_q <= '0; ready_q <= 1'b0;
    end else if (!all_ok) begin
      // Any term dropping clears the timer immediately. A link that
      // oscillates never accumulates enough stability to be declared up,
      // which is the intended behaviour — an intermittent link is worse
      // than a down one, because software will try to use it.
      stable_q <= '0;
      ready_q  <= 1'b0;
    end else if (stable_q != $clog2(STABLE_SYMBOLS+1)'(STABLE_SYMBOLS)) begin
      stable_q <= stable_q + 1'b1;
    end else begin
      ready_q <= 1'b1;
    end
  end
 
  assign phy_ready = ready_q;
 
  // MARGINAL is the output that earns its area. A link can satisfy every
  // term right now and have lost lock repeatedly, which predicts failure
  // under load. Without this, "up" and "reliably up" are the same reading.
  assign phy_marginal = ready_q
                        && ((cdr_losses   >= 8'(MARGINAL_LOSSES))
                         || (block_losses >= 8'(MARGINAL_LOSSES)));
 
  // The lowest failing term, for the descent in Chapter 2.1 section 15.
  always_comb begin
    if      (!signal_detect) lowest_failing = 2'd0;   // PMD
    else if (!clk_locked)    lowest_failing = 2'd1;   // PMA
    else if (!block_lock)    lowest_failing = 2'd2;   // PCS
    else if (!lane_aligned)  lowest_failing = 2'd3;   // PCS
    else                     lowest_failing = 2'd3;
  end
 
endmodule

// SVA over the modules in this chapter.
 
// SAFETY — P1: running disparity stays bounded. The DC-balance guarantee;
// exceeding it means an AC-coupled channel accumulates an offset and the
// receiver's threshold shifts.
property p_disparity_bounded;
  @(posedge clk) disable iff (!rst_n)
  !disparity_alarm;
endproperty
a_disparity_bounded : assert property (p_disparity_bounded);
 
// SAFETY — P2: a control code is never a data code. If they overlapped, a
// receiver could not distinguish an idle marker from a data value, and the
// out-of-band alphabet would not exist.
property p_control_distinct;
  @(posedge clk) disable iff (!rst_n)
  (out_valid && in_control) |-> (out_code == CTRL_IDLE);
endproperty
a_control_distinct : assert property (p_control_distinct);
 
// CONSERVATION — P3: every parallel word produces exactly WIDTH serial
// bits. Catches a shift counter that skips or repeats, which shifts every
// subsequent word and garbles the link from that point on.
property p_serialiser_conserves;
  @(posedge clk) disable iff (!rst_n)
  (tx_valid && tx_ready) |=> (serial_active [*WIDTH]);
endproperty
a_serialiser_conserves : assert property (p_serialiser_conserves);
 
// SAFETY — P4: status terms assert bottom-up. Block lock without clock lock
// is impossible physically, so asserting it catches a status path that
// latches or a term computed from the wrong source.
property p_status_ordered;
  @(posedge clk) disable iff (!rst_n)
  block_lock |-> (clk_locked && signal_detect);
endproperty
a_status_ordered : assert property (p_status_ordered);
 
// SAFETY — P5: the block synchroniser's search terminates. WIDTH offsets
// exist and exactly one is correct; a search that could not exhaust its
// space is a receiver that hangs with no error.
property p_search_terminates;
  @(posedge clk) disable iff (!rst_n)
  (state_q == S_HUNT) |-> s_eventually (offset != $past(offset) || block_lock);
endproperty
a_search_terminates : assert property (p_search_terminates);
 
// SAFETY — P6: lock is re-verified while held. A locked receiver that
// stopped checking would hold a stale lock through a channel degradation
// and deliver garbage with every status bit green.
property p_lock_reverified;
  @(posedge clk) disable iff (!rst_n)
  (block_lock && sym_valid && !sym_legal) |=> (bad_q > 0 || !block_lock);
endproperty
a_lock_reverified : assert property (p_lock_reverified);
 
// SAFETY — P7: the elastic buffer never overflows or underflows. Both mean
// the frequency offset exceeded what the buffer absorbs, and the result is
// corrupted data rather than degraded timing.
property p_elastic_never_spills;
  @(posedge clk) disable iff (!rst_n)
  !overflow && !underflow;
endproperty
a_elastic_safe : assert property (p_elastic_never_spills);
 
// SAFETY — P8: only idle symbols are deleted. Deleting a data symbol
// silently corrupts a frame, and the check value two layers up is the only
// thing that would ever notice.
property p_only_idle_deleted;
  @(posedge clk) disable iff (!rst_n)
  delete_now |-> wr_is_idle;
endproperty
a_only_idle_deleted : assert property (p_only_idle_deleted);
 
// SAFETY — P9: the link is not declared ready until every term has been
// stable for the declared interval. Catches a design that reports up on the
// instant all four are true, which makes an oscillating link look usable.
property p_ready_needs_stability;
  @(posedge clk) disable iff (!rst_n)
  $rose(phy_ready) |-> (stable_q == STABLE_SYMBOLS);
endproperty
a_ready_stable : assert property (p_ready_needs_stability);
 
// LIVENESS — P10: a link with a good signal eventually becomes ready.
// ASSUMPTIONS, stated: the signal persists, and the symbols are legal at
// some offset. Without both this is false for a correct design — which is
// the whole point of a receiver that can fail to lock.
assume property (@(posedge clk) s_eventually (signal_detect));
assume property (@(posedge clk) s_eventually (sym_valid && sym_legal));
property p_link_eventually_ready;
  @(posedge clk) disable iff (!rst_n)
  signal_detect |-> s_eventually (phy_ready);
endproperty
a_link_ready : assert property (p_link_eventually_ready);

// FALSE for a correct design. Included as a warning, not as a check.
// property p_lock_once_acquired_is_held;
//   @(posedge clk) disable iff (!rst_n)
//   block_lock |=> block_lock;
// endproperty

// NON-SYNTHESIZABLE — directed stimulus. Instantiates a serialiser and a
// deserialiser with OPPOSITE bit orders and shows that every status bit
// reports healthy while every word is wrong.
task automatic bit_order_mismatch_reports_healthy();
  logic [WIDTH-1:0] sent, got;
 
  sent = 10'b1100100011;
  send_word(sent);
  wait (rx_valid);
  got = rx_word;
 
  // Everything that could report a problem does not.
  assert (dut_phy.phy_ready)
    else $error("precondition: the link should report ready");
  assert (dut_sync.block_lock)
    else $error("precondition: block lock should hold");
  assert (dut_eb.overflow == 1'b0 && dut_eb.underflow == 1'b0)
    else $error("precondition: the elastic buffer should be quiet");
 
  // AND THE DATA IS REVERSED. This is the only evidence, and it requires
  // comparing across the boundary — no single block can detect it.
  assert (got == {<<{sent}})
    else $error("expected a bit-reversed word; the mismatch model is wrong");
  assert (got != sent)
    else $error("bit orders did not actually differ — the test proves nothing");
 
  $display("bit-order mismatch: sent %b, received %b, every status term healthy",
           sent, got);
endtask