Where the MAC Ends and the PHY Begins

// SYNTHESIZABLE. The MAC's view of the boundary.
//
// EVERY SIGNAL BELOW CARRIES ITS JUSTIFICATION. That is the discipline this
// module exists to demonstrate: a boundary signal that cannot be traced to
// an owned responsibility or to a contract assumption is a leak of one
// side's internals into the other, and it will become a dependency that
// nobody intended and nobody can remove later.
//
// No xMII generation is encoded here. Chapter 4.2 owns the mechanics.
package macphy_pkg;
  // Which side owns a responsibility, by the rule of Section 3.
  typedef enum logic [1:0] {
    OWN_MAC      = 2'd0,   // failure detectable in the frame
    OWN_PHY      = 2'd1,   // failure detectable in the signal
    OWN_BOUNDARY = 2'd2    // detectable by neither alone -- needs a contract
  } owner_e;
 
  typedef enum logic [2:0] {
    XC_IDLE  = 3'd0,
    XC_START = 3'd1,
    XC_DATA  = 3'd2,
    XC_END   = 3'd3,
    XC_ERROR = 3'd4        // the MAC abandoned this frame
  } xctrl_e;
endpackage
 
module mac_phy_boundary
  import macphy_pkg::*;
#(
  parameter int unsigned W = 32
) (
  // ── Clocking ────────────────────────────────────────────────────────────
  // OWNER: PHY. The link rate is a property of the medium and the coding,
  // both of which the PHY owns. The MAC runs against what it is given --
  // which is the concrete form of the MAC's assumption 2, that the rate is
  // known and constant while the link is up.
  input  logic clk,
  input  logic rst_n,
 
  // ── Transmit: MAC to PHY ────────────────────────────────────────────────
  // OWNER: MAC. Frame construction is MAC-owned because a malformed frame
  // is detectable in the frame -- the check value fails.
  output logic [W-1:0] tx_data,
  output xctrl_e       tx_ctrl,
  output logic         tx_valid,
 
  // DISCHARGES: PHY assumption 1 -- the handshake is honoured. Data offered
  // must stay stable until tx_ready is seen. The PHY cannot verify this and
  // must simply rely on it, which is why Section 8 checks it explicitly.
  input  logic         tx_ready,
 
  // OWNER: MAC. An abandoned frame must be MARKED, not silently truncated,
  // or the far end receives a short but structurally valid frame -- which
  // fails its check value and gets attributed to the link.
  output logic         tx_error,
 
  // ── Receive: PHY to MAC ─────────────────────────────────────────────────
  // OWNER: PHY for delivery, MAC for interpretation. The PHY guarantees
  // order and reports what it could not deliver; it does not interpret.
  input  logic [W-1:0] rx_data,
  input  xctrl_e       rx_ctrl,
  input  logic         rx_valid,
 
  // OWNER: PHY. DISCHARGES: MAC assumption 3 -- failures are reported, not
  // hidden. This is the PHY saying "these octets are suspect" rather than
  // delivering plausible garbage the MAC would then trust.
  input  logic         rx_error,
 
  // ── Status: PHY to MAC ──────────────────────────────────────────────────
  // OWNER: PHY. Chapter 3.4 §13 argued this must be a VECTOR rather than a
  // bit, because the lowest deasserted element names the sublayer that owns
  // the problem. Reducing it here would discard that at the boundary --
  // after which the MAC can report only "the link is down".
  input  logic         link_up,
  input  logic [3:0]   link_status_vector,
 
  // OWNER: BOUNDARY. Neither side can detect a rate mismatch alone: the MAC
  // has no view of the signal, the PHY no view of what the MAC expects. So
  // the negotiated rate is CARRIED, not assumed -- Section 11's subject.
  input  logic [3:0]   negotiated_rate,
  input  logic         rate_valid,
 
  // ── Boundary responsibilities ───────────────────────────────────────────
  // OWNER: BOUNDARY, by Section 3's third branch. The PHY captures the
  // instant because only it is near the wire; the MAC associates it with a
  // frame because only it knows what a frame is. Neither can do both, so
  // the interface carries the association.
  input  logic         ts_capture_valid,
  input  logic [63:0]  ts_capture_value,
  output logic         ts_request,
 
  // ── What is deliberately ABSENT ─────────────────────────────────────────
  // There is no signal here for: the PHY's block lock state, its equaliser
  // taps, its FEC correction counts, its eye margin, or its lane skew.
  //
  // Every one of those is a PHY-owned failure the PHY detects itself, so
  // exposing it at this boundary would give the MAC a dependency on PHY
  // internals -- and a MAC that reads FEC counters is a MAC that cannot be
  // paired with a PHY that has no FEC.
  //
  // Those quantities belong on a MANAGEMENT interface, which is a different
  // boundary with a different contract. The distinction is the single most
  // common architectural mistake at this interface.
  output logic         mgmt_request   // the separate path, named not modelled
);
 
  // The module is a declaration. Its content is the justification above,
  // and its value is that a reviewer can check every signal against a rule.
  assign ts_request   = 1'b0;
  assign mgmt_request = 1'b0;
 
endmodule

// SYNTHESIZABLE INSTRUMENTATION. MAC side.
//
// Checks the PHY against the four things the MAC is allowed to assume
// (Section 4). None of these is checkable by the MAC's ordinary logic --
// that is precisely why they are ASSUMPTIONS -- so each needs deliberate
// instrumentation or the violation is invisible.
//
// Every finding here is one the MAC would otherwise blame on the medium.
module mac_side_conformance
  import macphy_pkg::*;
#(
  parameter int unsigned CNT_W = 20,
  // Cycles the link may report up while delivering nothing before that
  // combination is treated as a contract violation rather than idleness.
  parameter int unsigned SILENCE_LIMIT = 1_000_000
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic       link_up,
  input  logic [3:0] link_status_vector,
  input  logic       rate_valid,
  input  logic [3:0] negotiated_rate,
 
  input  logic   rx_valid,
  input  xctrl_e rx_ctrl,
  input  logic   rx_error,
 
  // ── Assumption 3: failures are reported, not hidden ─────────────────────
  // The link claims to be up while its own status vector says a sublayer is
  // unsatisfied. The PHY is contradicting itself, and the MAC would
  // otherwise trust the summary bit and deliver corrupt frames upward.
  output logic v_status_contradiction,
  output logic [CNT_W-1:0] c_status_contradiction,
 
  // The link reports up and delivers nothing at all for a long time.
  // Chapter 3.4 §9 established the PHY never goes silent -- idle is
  // transmitted. Prolonged silence with link_up asserted is a violation.
  output logic v_silent_while_up,
  output logic [CNT_W-1:0] c_silent_while_up,
 
  // ── Assumption 2: the rate is known and constant while up ───────────────
  // A rate change without the link dropping invalidates every gap and
  // sizing calculation the MAC has in flight.
  output logic v_rate_changed_while_up,
  output logic [CNT_W-1:0] c_rate_changed_while_up,
 
  // ── Frame structure: an END without a START ─────────────────────────────
  // The PHY delivering a malformed control sequence. Not a corrupted frame
  // -- a corrupted CONTRACT, and the two need different responses.
  output logic v_end_without_start,
  output logic [CNT_W-1:0] c_end_without_start,
 
  // ── Assumption 3 again, on a per-frame basis ────────────────────────────
  // rx_error asserted outside a frame is meaningless: there is nothing for
  // it to qualify, and a MAC acting on it will discard the NEXT frame.
  output logic v_error_outside_frame,
  output logic [CNT_W-1:0] c_error_outside_frame,
 
  // First violation observed, held. During an incident several will be set;
  // which came first identifies the initiating fault.
  output logic [2:0] first_violation,
  output logic       first_violation_valid
);
 
  logic       in_frame_q;
  logic [3:0] rate_q;
  logic [$clog2(SILENCE_LIMIT+1)-1:0] silence_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_comb begin
    // link_up asserted while the status vector is not fully satisfied.
    v_status_contradiction  = link_up && !(&link_status_vector);
    v_silent_while_up       = link_up
                            && (silence_q >= ($clog2(SILENCE_LIMIT+1))'(SILENCE_LIMIT));
    v_rate_changed_while_up = link_up && rate_valid && (negotiated_rate != rate_q);
    v_end_without_start     = rx_valid && (rx_ctrl == XC_END) && !in_frame_q;
    v_error_outside_frame   = rx_valid && rx_error && !in_frame_q
                            && (rx_ctrl != XC_START);
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      in_frame_q              <= 1'b0;
      rate_q                  <= '0;
      silence_q               <= '0;
      c_status_contradiction  <= '0;
      c_silent_while_up       <= '0;
      c_rate_changed_while_up <= '0;
      c_end_without_start     <= '0;
      c_error_outside_frame   <= '0;
      first_violation         <= '0;
      first_violation_valid   <= 1'b0;
    end else begin
      if (clear) begin
        c_status_contradiction  <= '0;
        c_silent_while_up       <= '0;
        c_rate_changed_while_up <= '0;
        c_end_without_start     <= '0;
        c_error_outside_frame   <= '0;
      end else begin
        c_status_contradiction  <= bump(c_status_contradiction,  v_status_contradiction);
        c_silent_while_up       <= bump(c_silent_while_up,       v_silent_while_up);
        c_rate_changed_while_up <= bump(c_rate_changed_while_up, v_rate_changed_while_up);
        c_end_without_start     <= bump(c_end_without_start,     v_end_without_start);
        c_error_outside_frame   <= bump(c_error_outside_frame,   v_error_outside_frame);
      end
 
      // Frame tracking, from the control encoding alone.
      if (rx_valid) begin
        if      (rx_ctrl == XC_START) in_frame_q <= 1'b1;
        else if (rx_ctrl == XC_END)   in_frame_q <= 1'b0;
      end
 
      if (rate_valid) rate_q <= negotiated_rate;
 
      // Silence tracking: any delivery resets it.
      if (rx_valid)        silence_q <= '0;
      else if (!(&silence_q)) silence_q <= silence_q + 1'b1;
 
      // First cause, held.
      if (!first_violation_valid) begin
        if      (v_status_contradiction)  begin first_violation <= 3'd0; first_violation_valid <= 1'b1; end
        else if (v_rate_changed_while_up) begin first_violation <= 3'd1; first_violation_valid <= 1'b1; end
        else if (v_end_without_start)     begin first_violation <= 3'd2; first_violation_valid <= 1'b1; end
        else if (v_error_outside_frame)   begin first_violation <= 3'd3; first_violation_valid <= 1'b1; end
        else if (v_silent_while_up)       begin first_violation <= 3'd4; first_violation_valid <= 1'b1; end
      end
    end
  end
 
endmodule

// SYNTHESIZABLE INSTRUMENTATION. PHY side.
//
// Checks the MAC against the four things the PHY is allowed to assume.
//
// Note the asymmetry with Section 6, because it is the point of having
// both: the MAC's violations are PROTOCOL violations -- it broke the
// handshake, mismarked a frame, closed the gap. The PHY's violations are
// HONESTY violations -- it claimed a state it was not in. Different kinds
// of assumption produce different kinds of check, and a design that
// implements one checker and calls the boundary covered has covered half.
module phy_side_conformance
  import macphy_pkg::*;
#(
  parameter int unsigned CNT_W = 20,
  parameter int unsigned W     = 32,
  // Minimum idle cycles the PHY needs between frames for rate compensation.
  parameter int unsigned MIN_GAP = 12,
  parameter int unsigned MAX_FRAME_WORDS = 380
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic         tx_valid,
  input  logic [W-1:0] tx_data,
  input  xctrl_e       tx_ctrl,
  input  logic         tx_error,
  input  logic         tx_ready,
 
  // ── Assumption 1: the handshake is honoured ─────────────────────────────
  // Data offered must stay stable until accepted. THE violation that only
  // appears under back-pressure -- which light testing never creates, so it
  // ships. Chapter 3.4 §15 named it and this is where it is caught.
  output logic v_data_changed_while_stalled,
  output logic [CNT_W-1:0] c_data_changed_while_stalled,
 
  // ── Assumption 2: frame boundaries are marked correctly ─────────────────
  output logic v_start_inside_frame,
  output logic v_data_outside_frame,
  output logic [CNT_W-1:0] c_start_inside_frame,
  output logic [CNT_W-1:0] c_data_outside_frame,
 
  // ── Assumption 3: the interframe gap is respected ───────────────────────
  // The PHY inserts and deletes idles in the gap to absorb the frequency
  // difference between two independent oscillators (Chapter 2.6). A MAC
  // that closes the gap leaves nowhere to do it, and the elastic buffer
  // eventually overruns -- an error attributed to the PHY, caused above it.
  output logic v_gap_too_short,
  output logic [CNT_W-1:0] c_gap_too_short,
 
  // ── Assumption 4: sizes are within negotiated limits ────────────────────
  // The PHY does not enforce length -- that is MAC-owned by Section 3's
  // rule. But it must NOTICE, or an oversized frame silently overruns
  // whatever the PHY sized for it.
  output logic v_frame_too_long,
  output logic [CNT_W-1:0] c_frame_too_long,
 
  output logic [2:0] first_violation,
  output logic       first_violation_valid
);
 
  logic         in_frame_q;
  logic [W-1:0] held_data_q;
  xctrl_e       held_ctrl_q;
  logic         was_stalled_q;
  logic [$clog2(MIN_GAP+2)-1:0]         gap_q;
  logic [$clog2(MAX_FRAME_WORDS+2)-1:0] len_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_comb begin
    // Offered last cycle, not accepted, and the offer has changed.
    v_data_changed_while_stalled = was_stalled_q && tx_valid
                                && ((tx_data != held_data_q) || (tx_ctrl != held_ctrl_q));
 
    v_start_inside_frame = tx_valid && tx_ready && (tx_ctrl == XC_START) && in_frame_q;
    v_data_outside_frame = tx_valid && tx_ready && (tx_ctrl == XC_DATA)  && !in_frame_q;
 
    v_gap_too_short = tx_valid && tx_ready && (tx_ctrl == XC_START)
                    && (gap_q < ($clog2(MIN_GAP+2))'(MIN_GAP));
 
    v_frame_too_long = tx_valid && tx_ready && in_frame_q
                     && (len_q >= ($clog2(MAX_FRAME_WORDS+2))'(MAX_FRAME_WORDS));
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      in_frame_q                   <= 1'b0;
      held_data_q                  <= '0;
      held_ctrl_q                  <= XC_IDLE;
      was_stalled_q                <= 1'b0;
      gap_q                        <= '1;
      len_q                        <= '0;
      c_data_changed_while_stalled <= '0;
      c_start_inside_frame         <= '0;
      c_data_outside_frame         <= '0;
      c_gap_too_short              <= '0;
      c_frame_too_long             <= '0;
      first_violation              <= '0;
      first_violation_valid        <= 1'b0;
    end else begin
      if (clear) begin
        c_data_changed_while_stalled <= '0;
        c_start_inside_frame         <= '0;
        c_data_outside_frame         <= '0;
        c_gap_too_short              <= '0;
        c_frame_too_long             <= '0;
      end else begin
        c_data_changed_while_stalled <= bump(c_data_changed_while_stalled, v_data_changed_while_stalled);
        c_start_inside_frame         <= bump(c_start_inside_frame,         v_start_inside_frame);
        c_data_outside_frame         <= bump(c_data_outside_frame,         v_data_outside_frame);
        c_gap_too_short              <= bump(c_gap_too_short,              v_gap_too_short);
        c_frame_too_long             <= bump(c_frame_too_long,             v_frame_too_long);
      end
 
      // Hold the offer so the next cycle can compare against it.
      was_stalled_q <= tx_valid && !tx_ready;
      if (tx_valid && !tx_ready) begin
        held_data_q <= tx_data;
        held_ctrl_q <= tx_ctrl;
      end
 
      if (tx_valid && tx_ready) begin
        unique case (tx_ctrl)
          XC_START: begin in_frame_q <= 1'b1; gap_q <= '0; len_q <= '0; end
          XC_END:   begin in_frame_q <= 1'b0; gap_q <= '0;              end
          XC_DATA:  if (!(&len_q)) len_q <= len_q + 1'b1;
          default:  if (!in_frame_q && !(&gap_q)) gap_q <= gap_q + 1'b1;
        endcase
      end else if (!in_frame_q && !(&gap_q)) begin
        gap_q <= gap_q + 1'b1;
      end
 
      if (!first_violation_valid) begin
        if      (v_data_changed_while_stalled) begin first_violation <= 3'd0; first_violation_valid <= 1'b1; end
        else if (v_start_inside_frame)         begin first_violation <= 3'd1; first_violation_valid <= 1'b1; end
        else if (v_data_outside_frame)         begin first_violation <= 3'd2; first_violation_valid <= 1'b1; end
        else if (v_gap_too_short)              begin first_violation <= 3'd3; first_violation_valid <= 1'b1; end
        else if (v_frame_too_long)             begin first_violation <= 3'd4; first_violation_valid <= 1'b1; end
      end
    end
  end
 
endmodule

// SYNTHESIZABLE INSTRUMENTATION.
//
// The question is always "the link is up and frames are being lost -- whose
// problem is it?" Neither side can answer it alone, by Section 4. This block
// answers it from both checkers plus the PHY's own status.
//
// The PRIORITY ORDERING is the design. It encodes which evidence is more
// conclusive, and getting it wrong sends people to the wrong team with
// apparent authority -- which is worse than sending them nowhere.
module boundary_attribution
  import macphy_pkg::*;
#(
  parameter int unsigned CNT_W = 20
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  // From Section 6 -- the PHY violated what the MAC assumed.
  input  logic mac_side_violation,
  input  logic [2:0] mac_side_first,
 
  // From Section 7 -- the MAC violated what the PHY assumed.
  input  logic phy_side_violation,
  input  logic [2:0] phy_side_first,
 
  // The PHY's own view of itself (Chapter 3.4 §13).
  input  logic       link_up,
  input  logic [3:0] link_status_vector,
 
  // Frames lost, from the MAC's own accounting.
  input  logic frame_lost,
 
  // At most one is asserted. All low means no attribution is possible,
  // which is itself a reportable state and must not be silently defaulted.
  output logic blame_phy_internal,   // the PHY says it is not working
  output logic blame_phy_contract,   // the PHY broke the contract
  output logic blame_mac_contract,   // the MAC broke the contract
  output logic blame_unattributed,   // frames lost, no evidence either way
 
  output logic [CNT_W-1:0] c_phy_internal,
  output logic [CNT_W-1:0] c_phy_contract,
  output logic [CNT_W-1:0] c_mac_contract,
  output logic [CNT_W-1:0] c_unattributed
);
 
  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
 
  // THE PRIORITY ORDERING, and the reasoning for each step.
  //
  // 1. The PHY's own status FIRST. If the PHY says a sublayer is
  //    unsatisfied, that is a self-report and it is the most conclusive
  //    evidence available -- nothing else needs explaining. Checking a
  //    contract violation before this would blame an interface for a link
  //    that is simply down.
  //
  // 2. Then contract violations, MAC-side checker before PHY-side. A PHY
  //    that contradicts its own status vector is broken in a way that makes
  //    every other observation unreliable, so it must be ruled out before
  //    the MAC is blamed for anything.
  //
  // 3. Then MAC violations.
  //
  // 4. Only then "unattributed" -- and it must be REPORTED, not defaulted
  //    to one side. A design whose fallback blames one party will blame it
  //    for every fault it cannot explain.
  always_comb begin
    blame_phy_internal = 1'b0;
    blame_phy_contract = 1'b0;
    blame_mac_contract = 1'b0;
    blame_unattributed = 1'b0;
 
    if (!link_up || !(&link_status_vector)) blame_phy_internal = 1'b1;
    else if (mac_side_violation)            blame_phy_contract = 1'b1;
    else if (phy_side_violation)            blame_mac_contract = 1'b1;
    else if (frame_lost)                    blame_unattributed = 1'b1;
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n || clear) begin
      c_phy_internal <= '0;
      c_phy_contract <= '0;
      c_mac_contract <= '0;
      c_unattributed <= '0;
    end else begin
      c_phy_internal <= bump(c_phy_internal, blame_phy_internal);
      c_phy_contract <= bump(c_phy_contract, blame_phy_contract);
      c_mac_contract <= bump(c_mac_contract, blame_mac_contract);
      c_unattributed <= bump(c_unattributed, blame_unattributed);
    end
  end
 
endmodule

// SYNTHESIZABLE. MAC/PHY capability agreement, inside one device.
//
// NOT Chapter 3.8's auto-negotiation. That is between LINK PARTNERS, across
// the wire. This is between a MAC and the PHY it is bonded to, and the
// failure it prevents is different: a MAC configured for a frame size or a
// feature its PHY does not implement, which produces frames the PHY mangles
// while both sides report healthy.
//
// The rule: a parameter both sides must agree on and NEITHER can verify
// unilaterally must be NEGOTIATED, not configured twice. Configuring twice
// is how the two ends come to disagree while each believes it is correct.
module macphy_capability
  import macphy_pkg::*;
#(
  parameter int unsigned CAP_W = 8
) (
  input  logic clk,
  input  logic rst_n,
 
  // What each side can do. From straps, fuses, firmware or discovery.
  input  logic [CAP_W-1:0] mac_caps,
  input  logic [CAP_W-1:0] phy_caps,
  input  logic             phy_caps_valid,
 
  // The agreed set, and a per-capability enable both sides use.
  output logic [CAP_W-1:0] agreed_caps,
  output logic             agreement_valid,
 
  // A capability the MAC needs and the PHY does not have. This is the fault
  // that otherwise appears as inexplicable frame corruption -- the MAC
  // emitting something structurally legal that this PHY cannot carry.
  output logic [CAP_W-1:0] mac_wants_unsupported,
  output logic             capability_shortfall,
 
  // A capability the PHY has that the MAC will not use. Not a fault, but
  // worth reporting: it usually means a configuration was not applied, and
  // a system quietly running below its hardware is a real cost.
  output logic [CAP_W-1:0] phy_offers_unused,
 
  // Sticky: the MAC operated before agreement completed. Every parameter it
  // used until then was assumed rather than agreed.
  output logic             operated_before_agreement
);
 
  logic agreed_q;
 
  always_comb begin
    agreed_caps           = mac_caps & phy_caps;
    mac_wants_unsupported = mac_caps & ~phy_caps;
    phy_offers_unused     = phy_caps & ~mac_caps;
    capability_shortfall  = phy_caps_valid && (mac_wants_unsupported != '0);
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      agreed_q                  <= 1'b0;
      agreement_valid           <= 1'b0;
      operated_before_agreement <= 1'b0;
    end else begin
      // Agreement requires the PHY to have actually reported. A design that
      // treats "no report yet" as "no capabilities" silently configures the
      // intersection with zero and disables everything.
      agreed_q        <= phy_caps_valid;
      agreement_valid <= phy_caps_valid;
 
      if (!phy_caps_valid && agreed_q) operated_before_agreement <= 1'b1;
    end
  end
 
endmodule

// SYNTHESIZABLE INSTRUMENTATION. Outside the datapath.
//
// The checkers of Sections 6 and 7 answer WHETHER and WHICH. Neither
// answers WHAT LED TO IT, and for the interaction faults of Section 13 that
// is the only useful question -- the violation is a consequence, and the
// coincidence that caused it happened several cycles earlier.
//
// A circular buffer that FREEZES on the first violation is the whole idea.
// It costs a small memory and it is the difference between "the gap check
// fired" and "the gap check fired two cycles after an abort coincided with
// an idle deletion".
module boundary_trace
  import macphy_pkg::*;
#(
  parameter int unsigned DEPTH  = 64,
  parameter int unsigned PTR_W  = $clog2(DEPTH),
  parameter int unsigned W      = 32,
  // Cycles to keep recording AFTER the trigger, so the consequence is
  // captured alongside its cause. Without this the trace stops exactly at
  // the interesting moment.
  parameter int unsigned POST_TRIGGER = 8
) (
  input  logic clk,
  input  logic rst_n,
  input  logic arm,               // begin recording; clears a previous freeze
 
  // Both directions, sampled together. Sampling only one side is what makes
  // an interaction fault unreconstructable.
  input  logic         tx_valid,
  input  logic         tx_ready,
  input  xctrl_e       tx_ctrl,
  input  logic         tx_error,
  input  logic         rx_valid,
  input  xctrl_e       rx_ctrl,
  input  logic         rx_error,
  input  logic         link_up,
  input  logic [3:0]   link_status_vector,
 
  // Any checker firing, from either side.
  input  logic         trigger,
 
  output logic         frozen,
  output logic [PTR_W-1:0] entries_valid,
  // Read port for software or a debug interface.
  input  logic [PTR_W-1:0] rd_addr,
  output logic [15:0]      rd_entry,
  // Where the trigger landed in the buffer, so software knows which entry
  // is the violation and which are its history.
  output logic [PTR_W-1:0] trigger_index,
  output logic             trigger_valid
);
 
  // A compact per-cycle record. Deliberately narrow: depth matters more
  // than width here, because an interaction fault needs history and the
  // signals that matter at this boundary are nearly all single bits.
  logic [15:0] mem [DEPTH];
  logic [PTR_W-1:0] wptr_q;
  logic [PTR_W-1:0] count_q;
  logic [$clog2(POST_TRIGGER+1)-1:0] post_q;
  logic             armed_q;
 
  wire [15:0] sample_c = {
    tx_valid, tx_ready, tx_error,
    rx_valid, rx_error,
    link_up,
    link_status_vector,          // 4 bits
    tx_ctrl[2:0], rx_ctrl[1:0]   // 5 bits
  };
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      wptr_q        <= '0;
      count_q       <= '0;
      post_q        <= '0;
      armed_q       <= 1'b0;
      frozen        <= 1'b0;
      trigger_index <= '0;
      trigger_valid <= 1'b0;
    end else if (arm) begin
      wptr_q        <= '0;
      count_q       <= '0;
      post_q        <= '0;
      armed_q       <= 1'b1;
      frozen        <= 1'b0;
      trigger_valid <= 1'b0;
    end else if (armed_q && !frozen) begin
      mem[wptr_q] <= sample_c;
      wptr_q      <= wptr_q + 1'b1;
      if (count_q != PTR_W'(DEPTH - 1)) count_q <= count_q + 1'b1;
 
      // First trigger only. A later violation is almost always a consequence
      // of the first, and overwriting would replace the cause with an effect.
      if (trigger && !trigger_valid) begin
        trigger_index <= wptr_q;
        trigger_valid <= 1'b1;
      end
 
      // Keep recording briefly past the trigger so the consequence is in
      // the same trace as its cause.
      if (trigger_valid) begin
        if (post_q == ($clog2(POST_TRIGGER+1))'(POST_TRIGGER)) frozen <= 1'b1;
        else post_q <= post_q + 1'b1;
      end
    end
  end
 
  assign entries_valid = count_q;
  assign rd_entry      = mem[rd_addr];
 
endmodule

// ─── Safety: the handshake holds data stable ───────────────────────────────
// The PHY's assumption 1, asserted at the boundary. Catches the violation
// that only appears under back-pressure and therefore ships.
property p_held_data_stable;
  @(posedge clk) disable iff (!rst_n)
  (tx_valid && !tx_ready) |=> (tx_valid && $stable(tx_data) && $stable(tx_ctrl));
endproperty
 
// ─── Ordering: frame structure is well formed ──────────────────────────────
// The PHY's assumption 2. Catches a MAC emitting a START inside a frame,
// which the PHY cannot detect through any ordinary path.
property p_no_start_inside_frame;
  @(posedge clk) disable iff (!rst_n)
  (tx_valid && tx_ready && (tx_ctrl == XC_START)) |-> !in_frame_q;
endproperty
 
property p_no_data_outside_frame;
  @(posedge clk) disable iff (!rst_n)
  (tx_valid && tx_ready && (tx_ctrl == XC_DATA)) |-> in_frame_q;
endproperty
 
// ─── Safety: an abandoned frame is marked ──────────────────────────────────
// Carried from Chapter 3.4 §15 because it is a boundary obligation. Catches
// silent truncation, which produces a short but structurally valid frame at
// the far end -- attributed to the link, caused above it.
property p_abort_is_marked;
  @(posedge clk) disable iff (!rst_n)
  (tx_valid && tx_error) |-> (tx_ctrl == XC_ERROR) || in_frame_q;
endproperty
 
// ─── Safety: the gap is respected ──────────────────────────────────────────
// The PHY's assumption 3. Catches a MAC that closes the gap, leaving the
// elastic buffer nowhere to insert or delete idles -- an overrun the PHY
// reports and the MAC caused.
property p_gap_respected;
  @(posedge clk) disable iff (!rst_n)
  (tx_valid && tx_ready && (tx_ctrl == XC_START)) |-> (gap_q >= MIN_GAP);
endproperty
 
// ─── Causation: link_up agrees with the status vector ──────────────────────
// The MAC's assumption 3. Catches a PHY whose summary bit is derived
// independently of its own status, so the two can disagree -- after which
// the MAC delivers frames from a link the PHY considers unusable.
property p_link_up_agrees_with_vector;
  @(posedge clk) disable iff (!rst_n)
  link_up |-> (&link_status_vector);
endproperty
 
// ─── Safety: the rate is stable while the link is up ───────────────────────
// The MAC's assumption 2. Catches a rate change without a link drop, which
// invalidates every gap and sizing calculation the MAC has in flight.
property p_rate_stable_while_up;
  @(posedge clk) disable iff (!rst_n)
  (link_up && rate_valid) |=> (!link_up || (negotiated_rate == $past(negotiated_rate)));
endproperty
 
// ─── Safety: receive errors qualify something ──────────────────────────────
// Catches rx_error asserted outside a frame, which is meaningless and makes
// a MAC acting on it discard the NEXT frame.
property p_rx_error_inside_frame;
  @(posedge clk) disable iff (!rst_n)
  (rx_valid && rx_error) |-> (in_frame_q || (rx_ctrl == XC_START));
endproperty
 
// ─── Mutual exclusion: at most one party is blamed ─────────────────────────
// Catches an attribution that fires two outputs, which sends two teams to
// two places for one fault.
property p_attribution_onehot;
  @(posedge clk) disable iff (!rst_n)
  $onehot0({blame_phy_internal, blame_phy_contract,
            blame_mac_contract, blame_unattributed});
endproperty
 
// ─── Causation: PHY self-report outranks contract evidence ─────────────────
// The priority ordering of Section 8, asserted. Catches an ordering that
// blames an interface for a link that is simply down.
property p_status_outranks_contract;
  @(posedge clk) disable iff (!rst_n)
  (!link_up || !(&link_status_vector)) |-> blame_phy_internal;
endproperty
 
// ─── Conservation: a lost frame is always attributed ───────────────────────
// Catches a frame loss producing no attribution at all -- which is the same
// as no instrumentation, since the question was "whose problem is it".
property p_loss_is_attributed;
  @(posedge clk) disable iff (!rst_n)
  frame_lost |-> $onehot({blame_phy_internal, blame_phy_contract,
                          blame_mac_contract, blame_unattributed});
endproperty
 
// ─── Safety: capabilities are the intersection, and only after report ──────
// Catches a design treating "no PHY report yet" as "no capabilities", which
// silently configures the intersection with zero and disables everything.
property p_agreement_needs_phy_report;
  @(posedge clk) disable iff (!rst_n)
  agreement_valid |-> $past(phy_caps_valid);
endproperty
 
// ─── Stability: first-violation records the first ──────────────────────────
// Catches a first-cause register that is overwritten, reporting the loudest
// violation rather than the initiating one.
property p_first_violation_is_stable;
  @(posedge clk) disable iff (!rst_n)
  first_violation_valid |=> $stable(first_violation);
endproperty
 
// ─── Stability: the trace freezes after the post-trigger window ────────────
// Catches a trace that keeps recording after freezing, overwriting the
// history that was the reason for capturing it.
property p_trace_freezes;
  @(posedge clk) disable iff (!rst_n)
  frozen |=> ($stable(trigger_index) && frozen);
endproperty
 
// ─── Causation: the trigger index is captured once ─────────────────────────
// Catches a trigger index overwritten by a later violation, which replaces
// the cause with one of its consequences.
property p_trigger_index_captured_once;
  @(posedge clk) disable iff (!rst_n)
  trigger_valid |=> $stable(trigger_index);
endproperty