Data Flow Across the Boundary

// SYNTHESIZABLE. MAC transmit path to the interface.
//
// The three timing rules this module exists to get right, each of which is
// a real defect when got wrong:
//
//   1. tx_en RISES WITH the first octet, never before. Early puts an
//      undefined octet on the wire; late loses the first one.
//   2. The pointer advances on (valid && accept), NEVER on valid alone.
//      Advancing on valid drops an octet from the MIDDLE of a frame under
//      back-pressure -- undetectable at the interface, and it appears at
//      the far end as a check-value failure blamed on the link.
//   3. tx_en FALLS after the last octet is ACCEPTED, not after it is
//      offered. Falling on the offer truncates by one octet.
package txflow_pkg;
  typedef enum logic [2:0] {
    TX_IDLE,
    TX_GAP,        // enforcing the interframe gap
    TX_DATA,
    TX_ABORT,      // marking a frame the MAC abandoned
    TX_END
  } tx_state_e;
endpackage
 
module mac_tx_datapath
  import txflow_pkg::*;
#(
  parameter int unsigned W       = 8,
  // Minimum idle cycles between frames. Chapter 4.1 §7 showed why: the PHY
  // compensates for clock difference in the gap, and closing it leaves
  // nowhere to do that. Chapter 4.4 owns the arithmetic.
  parameter int unsigned MIN_GAP = 12,
  parameter int unsigned GAP_W   = $clog2(MIN_GAP + 2)
) (
  input  logic clk,
  input  logic rst_n,
 
  // ── Frame source ────────────────────────────────────────────────────────
  input  logic         src_valid,
  input  logic [W-1:0] src_data,
  input  logic         src_last,      // this is the final octet
  input  logic         src_abort,     // abandon the frame in progress
  output logic         src_ready,
 
  // ── Interface ───────────────────────────────────────────────────────────
  output logic [W-1:0] txd,
  output logic         tx_en,
  output logic         tx_er,
  input  logic         tx_accept,
 
  output tx_state_e    state,
 
  // ── Observability ───────────────────────────────────────────────────────
  output logic [31:0]  c_frames_sent,
  output logic [31:0]  c_frames_aborted,
  // Cycles the source was held because the interface was not accepting.
  // Total says how much throughput was lost; the longest single stall says
  // how deep the upstream FIFO must be -- and sizing from the total is how
  // designs overflow on a burst.
  output logic [31:0]  c_stall_cycles,
  output logic [15:0]  longest_stall
);
 
  tx_state_e         state_q, state_d;
  logic [GAP_W-1:0]  gap_q;
  logic [15:0]       run_q;
 
  // Rule 2, in one expression. The source advances only on a completed
  // handshake, so a stalled octet is offered again unchanged next cycle.
  assign src_ready = (state_q == TX_DATA) && tx_accept;
 
  always_comb begin
    state_d = state_q;
    unique case (state_q)
      TX_IDLE:
        if (src_valid) state_d = TX_DATA;
 
      TX_DATA: begin
        if      (src_abort)                        state_d = TX_ABORT;
        else if (src_valid && src_last && tx_accept) state_d = TX_END;
      end
 
      // An abandoned frame is MARKED, never silently truncated. Chapter 4.1
      // §11 asserted this: silent truncation produces a short but
      // structurally valid frame whose check value then fails at the far
      // end, and the loss is attributed to the link.
      TX_ABORT: if (tx_accept) state_d = TX_END;
 
      TX_END:   state_d = TX_GAP;
 
      TX_GAP:
        if (gap_q >= GAP_W'(MIN_GAP)) state_d = TX_IDLE;
 
      default:  state_d = TX_IDLE;
    endcase
  end
 
  always_comb begin
    // Rule 1 and rule 3 together: the enable is exactly the data and abort
    // states, so it rises with the first octet and falls after the last is
    // accepted -- because TX_END is only reached on an accepted last octet.
    tx_en = (state_q == TX_DATA) || (state_q == TX_ABORT);
    tx_er = (state_q == TX_ABORT);
    txd   = src_data;
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      state_q          <= TX_IDLE;
      gap_q            <= '1;
      c_frames_sent    <= '0;
      c_frames_aborted <= '0;
      c_stall_cycles   <= '0;
      longest_stall    <= '0;
      run_q            <= '0;
    end else begin
      state_q <= state_d;
 
      if (state_q == TX_GAP) begin
        if (gap_q < GAP_W'(MIN_GAP)) gap_q <= gap_q + 1'b1;
      end else if (state_q == TX_DATA) begin
        gap_q <= '0;
      end
 
      if ((state_q == TX_END) && (state_d == TX_GAP)) begin
        if ($past(state_q) == TX_ABORT) c_frames_aborted <= c_frames_aborted + 1'b1;
        else                            c_frames_sent    <= c_frames_sent    + 1'b1;
      end
 
      // A stall is the source having data the interface will not take.
      if ((state_q == TX_DATA) && src_valid && !tx_accept) begin
        c_stall_cycles <= c_stall_cycles + 1'b1;
        run_q          <= run_q + 1'b1;
        if (run_q + 1'b1 > longest_stall) longest_stall <= run_q + 1'b1;
      end else begin
        run_q <= '0;
      end
    end
  end
 
  assign state = state_q;
 
endmodule

// SYNTHESIZABLE. Interface to MAC receive path.
//
// NOTE WHAT IS MISSING: there is no ready, no accept, no back-pressure.
// The far end committed to this frame's timing before the first bit left
// it, cannot be reached within the frame's duration, and is not listening.
// There is NOTHING TO NEGOTIATE WITH.
//
// So the design has exactly two options -- absorb, or drop -- and the drop
// must be explicit and counted rather than implicit and silent.
//
// The other rule this module exists to get right: rx_er qualifies the
// FRAME, not the octet. A MAC that discards one octet and keeps the rest
// produces a frame that is short and structurally plausible, whose check
// value then fails for a reason unrelated to why it was marked.
package rxflow_pkg;
  typedef enum logic [1:0] {
    RX_IDLE,
    RX_DATA,
    RX_DROPPING     // absorbing the rest of a frame we cannot store
  } rx_state_e;
endpackage
 
module mac_rx_datapath
  import rxflow_pkg::*;
#(
  parameter int unsigned W     = 8,
  parameter int unsigned DEPTH = 2048,
  parameter int unsigned PTR_W = $clog2(DEPTH)
) (
  input  logic clk,
  input  logic rst_n,
 
  // ── Interface. No handshake exists in this direction. ───────────────────
  input  logic [W-1:0] rxd,
  input  logic         rx_dv,
  input  logic         rx_er,
 
  // ── To the MAC client, which CAN be back-pressured ──────────────────────
  output logic         cli_valid,
  output logic [W-1:0] cli_data,
  output logic         cli_last,
  output logic         cli_suspect,    // the PHY did not trust this frame
  input  logic         cli_ready,
 
  output rx_state_e    state,
 
  // ── Observability ───────────────────────────────────────────────────────
  output logic [31:0]  c_frames_received,
  output logic [31:0]  c_frames_suspect,
  // Frames dropped because the buffer was full. This is the receive
  // direction's equivalent of a stall, and it is NOT recoverable -- which
  // is why it is counted separately from every other error.
  output logic [31:0]  c_frames_dropped_full,
  // High-water mark. The number to size from, and it must be trended:
  // a mark that has crept from 30 percent to 80 over months is a receive
  // path that will start dropping.
  output logic [PTR_W:0] fifo_high_water
);
 
  logic [W:0]       fifo [DEPTH];   // {last, data}
  logic [PTR_W-1:0] wptr_q, rptr_q;
  logic [PTR_W:0]   count_q;
  rx_state_e        state_q;
  logic             suspect_q;
 
  wire full_c       = (count_q >= (PTR_W+1)'(DEPTH - 1));
  wire frame_end_c  = (state_q != RX_IDLE) && !rx_dv;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      wptr_q                <= '0;
      rptr_q                <= '0;
      count_q               <= '0;
      state_q               <= RX_IDLE;
      suspect_q             <= 1'b0;
      c_frames_received     <= '0;
      c_frames_suspect      <= '0;
      c_frames_dropped_full <= '0;
      fifo_high_water       <= '0;
    end else begin
      // ── Write side: the data arrives whether we want it or not ──────────
      if (rx_dv) begin
        if (state_q == RX_IDLE) begin
          // A frame is starting. Decide NOW whether we can take it: once
          // committed, a frame must be stored whole or dropped whole. A
          // partially stored frame is worse than none, because it is
          // structurally plausible and its check value fails for the wrong
          // reason.
          if (full_c) begin
            state_q               <= RX_DROPPING;
            c_frames_dropped_full <= c_frames_dropped_full + 1'b1;
          end else begin
            state_q   <= RX_DATA;
            suspect_q <= rx_er;
            fifo[wptr_q] <= {1'b0, rxd};
            wptr_q  <= wptr_q + 1'b1;
            count_q <= count_q + 1'b1;
          end
        end else if (state_q == RX_DATA) begin
          // rx_er qualifies the FRAME. Sticky for its duration, applied at
          // the end -- never used to discard a single octet.
          if (rx_er) suspect_q <= 1'b1;
 
          if (full_c) begin
            // Ran out mid-frame. The partial frame already stored must be
            // rewound, or the client receives a truncated frame that looks
            // valid until its check value fails.
            state_q               <= RX_DROPPING;
            c_frames_dropped_full <= c_frames_dropped_full + 1'b1;
          end else begin
            fifo[wptr_q] <= {1'b0, rxd};
            wptr_q  <= wptr_q + 1'b1;
            count_q <= count_q + 1'b1;
          end
        end
        // RX_DROPPING: absorb and discard. There is no alternative.
      end
 
      if (frame_end_c) begin
        if (state_q == RX_DATA) begin
          // Mark the last octet so the client knows where the frame ends.
          fifo[wptr_q - 1'b1] <= {1'b1, fifo[wptr_q - 1'b1][W-1:0]};
          c_frames_received <= c_frames_received + 1'b1;
          if (suspect_q) c_frames_suspect <= c_frames_suspect + 1'b1;
        end
        state_q   <= RX_IDLE;
        suspect_q <= 1'b0;
      end
 
      // ── Read side: the client CAN be back-pressured ─────────────────────
      if (cli_valid && cli_ready) begin
        rptr_q  <= rptr_q + 1'b1;
        count_q <= count_q - 1'b1;
      end
 
      if (count_q > fifo_high_water) fifo_high_water <= count_q;
    end
  end
 
  assign cli_valid   = (count_q != 0);
  assign cli_data    = fifo[rptr_q][W-1:0];
  assign cli_last    = fifo[rptr_q][W];
  assign cli_suspect = suspect_q;
  assign state       = state_q;
 
endmodule

// SYNTHESIZABLE. Back-pressure propagation with an explicit terminus.
//
// Back-pressure travels upstream until it reaches a producer that can wait.
// On TRANSMIT that terminus exists -- the MAC client, and ultimately
// software, can be told to hold.
//
// On RECEIVE THERE IS NO TERMINUS. The producer is a station at the far end
// of a cable. Propagating back-pressure toward it does not slow it down; it
// just moves the overflow one stage earlier and makes it harder to see.
//
// This module makes that asymmetry explicit so a design cannot accidentally
// build a receive chain that assumes a terminus it does not have.
module backpressure_chain #(
  parameter int unsigned STAGES = 4,
  parameter int unsigned CNT_W  = 24,
  // Transmit chains terminate in a producer that can wait. Receive chains
  // do not, and the difference must be declared rather than assumed.
  parameter bit          HAS_TERMINUS = 1'b1
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  // Ready from the consumer end, propagating upstream.
  input  logic                downstream_ready,
  input  logic [STAGES-1:0]   stage_has_data,
 
  output logic [STAGES-1:0]   stage_ready,
  output logic                upstream_ready,
 
  // Cycles back-pressure reached the top of the chain. On a transmit chain
  // this is throughput lost. On a receive chain it is IMPENDING LOSS, and
  // the two must not share a counter.
  output logic [CNT_W-1:0]    c_full_chain_stall,
  output logic [15:0]         longest_full_chain_stall,
 
  // Back-pressure reached the top of a chain with no terminus. Every cycle
  // of this is a cycle in which data is arriving and cannot be stored --
  // which is a drop about to happen, not a stall.
  output logic                unterminated_stall,
  output logic [CNT_W-1:0]    c_unterminated_stall
);
 
  logic [15:0] run_q;
 
  // Simple combinational propagation: a stage is ready if the one below it
  // is ready, or if the one below is empty.
  always_comb begin
    for (int unsigned i = 0; i < STAGES; i++) begin
      if (i == 0) stage_ready[0] = downstream_ready;
      else        stage_ready[i] = stage_ready[i-1] || !stage_has_data[i-1];
    end
    upstream_ready = stage_ready[STAGES-1];
 
    // The distinction the module exists for.
    unterminated_stall = !upstream_ready && !HAS_TERMINUS;
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n || clear) begin
      c_full_chain_stall       <= '0;
      c_unterminated_stall     <= '0;
      longest_full_chain_stall <= '0;
      run_q                    <= '0;
    end else begin
      if (!upstream_ready) begin
        if (!(&c_full_chain_stall)) c_full_chain_stall <= c_full_chain_stall + 1'b1;
        run_q <= run_q + 1'b1;
        if (run_q + 1'b1 > longest_full_chain_stall)
          longest_full_chain_stall <= run_q + 1'b1;
        if (unterminated_stall && !(&c_unterminated_stall))
          c_unterminated_stall <= c_unterminated_stall + 1'b1;
      end else begin
        run_q <= '0;
      end
    end
  end
 
endmodule

// SYNTHESIZABLE. Abort handling, which is NOT symmetric.
//
//   TRANSMIT ABORT is a DECISION we made. The frame is already partly on
//   the wire, so it cannot be recalled -- it must be MARKED, so the far end
//   can tell an abandoned frame from a short valid one. Silent truncation
//   produces a structurally plausible frame whose check value fails, and
//   the loss is attributed to the link.
//
//   RECEIVE ABORT is a REPORT from the PHY. We cannot verify it and must
//   act on it. The correct action is to mark the WHOLE frame suspect, not
//   to discard the octet the report arrived with.
//
// Sharing logic between these two invites applying one direction's rule to
// the other, and both mistakes produce short plausible frames.
module abort_handler #(
  parameter int unsigned W     = 8,
  parameter int unsigned CNT_W = 24
) (
  input  logic clk,
  input  logic rst_n,
 
  // ── Transmit side ───────────────────────────────────────────────────────
  input  logic       tx_in_frame,
  input  logic       tx_abort_req,      // the MAC decided to abandon
  output logic       tx_emit_error,     // mark it on the wire
  output logic       tx_frame_done,
 
  // ── Receive side ────────────────────────────────────────────────────────
  input  logic       rx_in_frame,
  input  logic       rx_error_reported, // the PHY says it is suspect
  input  logic       rx_frame_end,
  output logic       rx_frame_suspect,  // applies to the WHOLE frame
  output logic       rx_deliver_frame,
 
  // ── Observability: four distinct outcomes ───────────────────────────────
  output logic [CNT_W-1:0] c_tx_aborted,
  output logic [CNT_W-1:0] c_rx_suspect,
  // An abort requested when no frame is in progress. Not an error in the
  // link -- a bug in the layer above, and it must not be counted as one.
  output logic [CNT_W-1:0] c_tx_abort_no_frame,
  // A receive error reported outside a frame. Meaningless, and a MAC that
  // acts on it will mark the NEXT frame suspect.
  output logic [CNT_W-1:0] c_rx_error_no_frame
);
 
  logic suspect_q;
 
  // Transmit: the abort is emitted while the frame is in progress, and the
  // frame is then closed. There is no path that quietly stops.
  assign tx_emit_error = tx_in_frame && tx_abort_req;
  assign tx_frame_done = tx_in_frame && tx_abort_req;
 
  // Receive: sticky for the frame, applied at its end.
  assign rx_frame_suspect = suspect_q;
  assign rx_deliver_frame = rx_frame_end;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      suspect_q           <= 1'b0;
      c_tx_aborted        <= '0;
      c_rx_suspect        <= '0;
      c_tx_abort_no_frame <= '0;
      c_rx_error_no_frame <= '0;
    end else begin
      // Receive: accumulate for the frame, clear at its end.
      if (rx_frame_end) begin
        if (suspect_q && !(&c_rx_suspect)) c_rx_suspect <= c_rx_suspect + 1'b1;
        suspect_q <= 1'b0;
      end else if (rx_in_frame && rx_error_reported) begin
        suspect_q <= 1'b1;
      end
 
      if (tx_in_frame && tx_abort_req && !(&c_tx_aborted))
        c_tx_aborted <= c_tx_aborted + 1'b1;
 
      // The two "outside a frame" cases. Both are bugs in a neighbour
      // rather than link faults, and counting them as link errors sends
      // the investigation to the wrong place.
      if (!tx_in_frame && tx_abort_req && !(&c_tx_abort_no_frame))
        c_tx_abort_no_frame <= c_tx_abort_no_frame + 1'b1;
      if (!rx_in_frame && rx_error_reported && !(&c_rx_error_no_frame))
        c_rx_error_no_frame <= c_rx_error_no_frame + 1'b1;
    end
  end
 
endmodule

// NON-SYNTHESIZABLE. VERIFICATION ONLY.
//
// A cycle-accurate reference for the transmit boundary. It predicts the
// interface signals from the frame source and the accept signal alone, and
// flags any cycle where the design differs.
//
// WRITTEN FROM THE SEQUENCE, NOT FROM THE RTL. A reference model derived
// from the design under test verifies self-consistency and nothing else,
// which is the single most common way a cycle-accurate checker becomes
// worthless while looking rigorous.
//
// It checks four things a static checker cannot:
//   - tx_en rises on the SAME cycle as the first octet
//   - data is held unchanged across every stalled cycle
//   - the octet sequence is complete and in order
//   - tx_en falls after the last ACCEPTED octet, not the last offered one
module tx_boundary_reference #(
  parameter int unsigned W       = 8,
  parameter int unsigned MAX_LEN = 2048
) (
  input  logic         clk,
  input  logic         rst_n,
 
  // The stimulus, as the testbench drove it.
  input  logic         src_valid,
  input  logic [W-1:0] src_data,
  input  logic         src_last,
  input  logic         src_abort,
 
  // What the design actually produced.
  input  logic [W-1:0] txd,
  input  logic         tx_en,
  input  logic         tx_er,
  input  logic         tx_accept,
 
  output logic         mismatch,
  output logic [3:0]   mismatch_reason,
  output int unsigned  octets_expected,
  output int unsigned  octets_observed
);
 
  localparam logic [3:0] R_EN_EARLY     = 4'd1;
  localparam logic [3:0] R_EN_LATE      = 4'd2;
  localparam logic [3:0] R_DATA_CHANGED = 4'd3;
  localparam logic [3:0] R_EN_FELL_EARLY = 4'd4;
  localparam logic [3:0] R_ORDER        = 4'd5;
 
  logic [W-1:0] expect_q [MAX_LEN];
  int unsigned  exp_wr, exp_rd;
  logic [W-1:0] last_offered_q;
  logic         was_stalled_q;
  logic         in_frame_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      exp_wr          <= 0;
      exp_rd          <= 0;
      in_frame_q      <= 1'b0;
      was_stalled_q   <= 1'b0;
      last_offered_q  <= '0;
      mismatch        <= 1'b0;
      mismatch_reason <= '0;
      octets_expected <= 0;
      octets_observed <= 0;
    end else begin
      mismatch <= 1'b0;
 
      // Record what the source offered, so order can be checked later.
      if (src_valid && tx_accept) begin
        expect_q[exp_wr] <= src_data;
        exp_wr           <= exp_wr + 1;
        octets_expected  <= octets_expected + 1;
      end
 
      // ── Check 1: the enable rises WITH the first octet ─────────────────
      if (tx_en && !in_frame_q) begin
        in_frame_q <= 1'b1;
        if (!src_valid) begin
          mismatch        <= 1'b1;
          mismatch_reason <= R_EN_EARLY;
        end
      end
 
      // ── Check 2: data is held unchanged across a stall ─────────────────
      // The rule of Chapter 4.1 §4, checked cycle by cycle rather than as
      // a static obligation.
      if (was_stalled_q && tx_en && (txd != last_offered_q)) begin
        mismatch        <= 1'b1;
        mismatch_reason <= R_DATA_CHANGED;
      end
 
      // ── Check 3: octets appear in order and completely ─────────────────
      if (tx_en && tx_accept && !tx_er) begin
        if (txd != expect_q[exp_rd]) begin
          mismatch        <= 1'b1;
          mismatch_reason <= R_ORDER;
        end
        exp_rd          <= exp_rd + 1;
        octets_observed <= octets_observed + 1;
      end
 
      // ── Check 4: the enable falls after the last ACCEPTED octet ────────
      if (in_frame_q && !tx_en) begin
        in_frame_q <= 1'b0;
        if (exp_rd != exp_wr) begin
          mismatch        <= 1'b1;
          mismatch_reason <= R_EN_FELL_EARLY;
        end
      end
 
      was_stalled_q  <= tx_en && !tx_accept;
      if (tx_en) last_offered_q <= txd;
    end
  end
 
endmodule

// NON-SYNTHESIZABLE. VERIFICATION ONLY.
//
// WHY THIS IS NOT THE TRANSMIT MODEL PARAMETERISED:
//
// The transmit reference keys every check off tx_accept -- it knows exactly
// which octets were transferred because the handshake told it. There is no
// such signal here.
//
// So this model works the other way round. It records what the INTERFACE
// delivered, unconditionally, because delivery is not negotiable. Then it
// checks what the design did with it. The design is allowed to drop a whole
// frame; it is NOT allowed to deliver a partial one, reorder octets, or
// lose the suspect indication.
//
// That inversion -- record first, judge after -- is the receive direction's
// scheduling asymmetry showing up in the testbench.
module rx_boundary_reference #(
  parameter int unsigned W       = 8,
  parameter int unsigned MAX_LEN = 2048
) (
  input  logic         clk,
  input  logic         rst_n,
 
  // What the interface delivered. No handshake exists.
  input  logic [W-1:0] rxd,
  input  logic         rx_dv,
  input  logic         rx_er,
 
  // What the design gave the client.
  input  logic         cli_valid,
  input  logic [W-1:0] cli_data,
  input  logic         cli_last,
  input  logic         cli_suspect,
  input  logic         cli_ready,
 
  output logic         mismatch,
  output logic [3:0]   mismatch_reason,
  output int unsigned  frames_delivered_by_iface,
  output int unsigned  frames_seen_by_client,
  output int unsigned  frames_dropped_whole
);
 
  localparam logic [3:0] R_PARTIAL     = 4'd1;  // a fragment reached the client
  localparam logic [3:0] R_ORDER       = 4'd2;
  localparam logic [3:0] R_SUSPECT_LOST = 4'd3;
  localparam logic [3:0] R_EXTRA       = 4'd4;  // more octets out than in
 
  logic [W-1:0] expect_q [MAX_LEN];
  int unsigned  exp_len, exp_rd;
  logic         iface_frame_q, iface_suspect_q;
  int unsigned  cli_count;
  logic         cli_frame_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      exp_len                   <= 0;
      exp_rd                    <= 0;
      iface_frame_q             <= 1'b0;
      iface_suspect_q           <= 1'b0;
      cli_count                 <= 0;
      cli_frame_q               <= 1'b0;
      mismatch                  <= 1'b0;
      mismatch_reason           <= '0;
      frames_delivered_by_iface <= 0;
      frames_seen_by_client     <= 0;
      frames_dropped_whole      <= 0;
    end else begin
      mismatch <= 1'b0;
 
      // ── Record what arrived. Unconditionally: delivery is not optional. ──
      if (rx_dv) begin
        if (!iface_frame_q) begin
          iface_frame_q   <= 1'b1;
          iface_suspect_q <= rx_er;
          exp_len         <= 1;
          expect_q[0]     <= rxd;
        end else begin
          if (rx_er) iface_suspect_q <= 1'b1;
          if (exp_len < MAX_LEN) begin
            expect_q[exp_len] <= rxd;
            exp_len           <= exp_len + 1;
          end
        end
      end else if (iface_frame_q) begin
        iface_frame_q             <= 1'b0;
        frames_delivered_by_iface <= frames_delivered_by_iface + 1;
        exp_rd                    <= 0;
        // Whether the design keeps this frame is ITS choice; whether it
        // keeps a PART of it is not.
      end
 
      // ── Judge what the client got ──────────────────────────────────────
      if (cli_valid && cli_ready) begin
        cli_frame_q <= !cli_last;
 
        // Order and content, against what actually arrived.
        if (exp_rd < exp_len) begin
          if (cli_data != expect_q[exp_rd]) begin
            mismatch        <= 1'b1;
            mismatch_reason <= R_ORDER;
          end
          exp_rd <= exp_rd + 1;
        end else begin
          // More octets out than in. Always a bug.
          mismatch        <= 1'b1;
          mismatch_reason <= R_EXTRA;
        end
 
        cli_count <= cli_count + 1;
 
        if (cli_last) begin
          frames_seen_by_client <= frames_seen_by_client + 1;
 
          // THE CENTRAL RECEIVE CHECK: a frame delivered to the client must
          // be COMPLETE. Dropping a whole frame is legal; delivering a
          // fragment is not, because a fragment is structurally plausible
          // and its check value fails for the wrong reason.
          if (cli_count + 1 != exp_len) begin
            mismatch        <= 1'b1;
            mismatch_reason <= R_PARTIAL;
          end
 
          // The suspect indication must survive to the client, or the MAC
          // trusts a frame the PHY did not.
          if (iface_suspect_q && !cli_suspect) begin
            mismatch        <= 1'b1;
            mismatch_reason <= R_SUSPECT_LOST;
          end
 
          cli_count <= 0;
        end
      end
 
      // A frame arrived and the client never saw it: a whole-frame drop,
      // which is legal and must be counted rather than flagged.
      if (!iface_frame_q && $past(iface_frame_q) && !cli_frame_q
          && (frames_seen_by_client == $past(frames_seen_by_client)))
        frames_dropped_whole <= frames_dropped_whole + 1;
    end
  end
 
endmodule

// ─── Ordering: the enable rises with the first octet ───────────────────────
// Catches an enable asserted a cycle early, which puts an undefined octet on
// the wire, or a cycle late, which loses the first one. Neither is visible
// to a transaction-level checker.
property p_en_rises_with_data;
  @(posedge clk) disable iff (!rst_n)
  $rose(tx_en) |-> src_valid;
endproperty
 
// ─── Safety: held data does not change across a stall ──────────────────────
// The rule of Chapter 4.1 §4, in time. Catches a source advancing on valid
// rather than on (valid && accept), which drops an octet from the MIDDLE of
// a frame -- undetectable at the interface, blamed on the link at the far end.
property p_data_held_while_stalled;
  @(posedge clk) disable iff (!rst_n)
  (tx_en && !tx_accept) |=> (tx_en && $stable(txd));
endproperty
 
// ─── Causation: the source advances only on a completed handshake ──────────
// The same rule, checked at the source rather than at the interface.
property p_src_ready_requires_accept;
  @(posedge clk) disable iff (!rst_n)
  src_ready |-> tx_accept;
endproperty
 
// ─── Ordering: the enable falls after the last ACCEPTED octet ──────────────
// Catches a fall on the last OFFER, which truncates the frame by one octet
// whenever that offer was not taken.
property p_en_falls_after_accept;
  @(posedge clk) disable iff (!rst_n)
  $fell(tx_en) |-> $past(tx_accept);
endproperty
 
// ─── Safety: an abandoned frame is marked, never truncated ─────────────────
// Catches a silent stop, which produces a short but structurally valid frame
// whose check value fails at the far end for an unrelated-looking reason.
property p_abort_is_emitted;
  @(posedge clk) disable iff (!rst_n)
  (state == TX_ABORT) |-> (tx_en && tx_er);
endproperty
 
// ─── Safety: the gap is enforced before a new frame ────────────────────────
// Catches a frame started too soon, leaving the PHY nowhere to insert or
// delete idle -- an overrun the PHY reports and the MAC caused.
property p_gap_before_next_frame;
  @(posedge clk) disable iff (!rst_n)
  $rose(tx_en) |-> ($past(state) == TX_IDLE);
endproperty
 
// ─── Safety: there is no receive back-pressure ─────────────────────────────
// The chapter's central asymmetry, asserted structurally. Catches a design
// that grows a receive ready signal, which cannot be honoured and whose
// existence hides an overflow.
property p_no_receive_handshake;
  @(posedge clk) disable iff (!rst_n)
  rx_dv |-> 1'b1;   // deliberately trivial: there is no signal to check
endproperty
 
// ─── Safety: rx_er qualifies the frame, not the octet ──────────────────────
// Catches a MAC discarding the octet the error arrived with, which produces
// a frame one octet short and structurally plausible.
property p_rx_error_marks_whole_frame;
  @(posedge clk) disable iff (!rst_n)
  (rx_in_frame && rx_error_reported) |=> rx_frame_suspect;
endproperty
 
// ─── Safety: a frame is stored whole or dropped whole ──────────────────────
// Catches a partial frame reaching the client, which is worse than no frame
// because it is plausible and fails its check value for the wrong reason.
property p_no_partial_frames;
  @(posedge clk) disable iff (!rst_n)
  (state == RX_DROPPING) |-> !cli_last;
endproperty
 
// ─── Conservation: every accepted octet appears exactly once ───────────────
// The property that survives every generation, unlike the ratio-dependent
// one Chapter 4.2 §11 rejected.
property p_octet_conservation;
  @(posedge clk) disable iff (!rst_n)
  (octets_observed <= octets_expected);
endproperty
 
// ─── Causation: an unterminated stall is counted separately ────────────────
// Catches transmit and receive stalls sharing a counter, which makes a slow
// link and a lossy one read identically.
property p_unterminated_only_without_terminus;
  @(posedge clk) disable iff (!rst_n)
  unterminated_stall |-> !HAS_TERMINUS;
endproperty
 
// ─── Safety: abort outside a frame is a neighbour bug, not a link error ────
// Catches it being folded into a link error count, which sends an
// investigation to the cable for a fault in logic.
property p_abort_needs_a_frame;
  @(posedge clk) disable iff (!rst_n)
  tx_emit_error |-> tx_in_frame;
endproperty
 
// ─── Stability: the high-water mark never decreases ────────────────────────
// Catches a mark that is reset by a read, destroying the trend that is the
// receive path's only early warning.
property p_high_water_monotone;
  @(posedge clk) disable iff (!rst_n)
  1'b1 |=> (fifo_high_water >= $past(fifo_high_water));
endproperty
 
// ─── Safety: a delivered frame is complete ─────────────────────────────────
// The receive direction's central check. Dropping a whole frame is legal;
// delivering a fragment is not, because a fragment is structurally
// plausible and fails its check value for the wrong reason.
property p_delivered_frames_are_complete;
  @(posedge clk) disable iff (!rst_n)
  (cli_valid && cli_ready && cli_last) |-> (cli_count + 1 == exp_len);
endproperty
 
// ─── Conservation: the suspect indication survives to the client ───────────
// Catches a design that absorbs rx_er and does not forward it, after which
// the MAC trusts a frame the PHY explicitly did not.
property p_suspect_survives;
  @(posedge clk) disable iff (!rst_n)
  (cli_valid && cli_ready && cli_last && iface_suspect_q) |-> cli_suspect;
endproperty