Elastic Buffering and Clock Compensation

worst-case relative difference = 100 ppm + 100 ppm = 200 ppm = 2e-4
 
slip over one frame = frame_octets × 2e-4

minimum frame,   64 octets:   64 × 2e-4 = 0.013 octets
maximum basic, 1518 octets: 1518 × 2e-4 = 0.30  octets
jumbo,         9000 octets: 9000 × 2e-4 = 1.80  octets

depth_clock ≥ ceil(max_frame_octets × 2e-4) + margin
            = ceil(1.80) + margin  for jumbo
            = 2 + margin octets

minimum interframe gap = 12 octets
octets that may be removed while keeping the gap usable ≈ a few

// SYNTHESIZABLE. Depth derived, not asserted.
//
// The arithmetic of Sections 3 and 4, as elaboration-time constants. A
// hand-computed depth is correct exactly once -- until someone enables
// jumbo frames, or specifies a cheaper oscillator, or raises the rate.
// Deriving it means those changes update it.
//
// TWO INDEPENDENT REQUIREMENTS ARE COMPUTED SEPARATELY AND ADDED. They have
// different causes and different failure modes, and a design that computes
// one total loses the ability to say which one it ran out of.
package elastic_pkg;
 
  // ── Inputs to the derivation. All illustrative defaults; a real design
  // takes them from its own oscillator specification and configuration. ────
  parameter int unsigned PPM_LOCAL   = 100;   // IEEE 802.3 specifies +/-100
  parameter int unsigned PPM_REMOTE  = 100;
  parameter int unsigned MAX_FRAME   = 1518;  // octets; 9000 for jumbo
  parameter int unsigned MIN_GAP     = 12;    // octets
  // Octets that must remain in the gap for frame delineation. Published
  // guidance for one gigabit family is not fewer than 8 including the
  // end and start markers.
  parameter int unsigned GAP_RESERVE = 8;
 
  // ── Derived: the clock-difference requirement ──────────────────────────
  // Worst case is both ends at opposite tolerance extremes.
  parameter int unsigned PPM_TOTAL = PPM_LOCAL + PPM_REMOTE;   // 200
 
  // Slip in octets over one maximum frame, scaled by 1e6 to stay integral,
  // then rounded up. For 1518 octets at 200 ppm this is 0.3036 -> 1.
  parameter int unsigned SLIP_SCALED   = (MAX_FRAME * PPM_TOTAL);       // 303600
  parameter int unsigned SLIP_OCTETS   = (SLIP_SCALED + 999_999) / 1_000_000;
 
  // Both directions plus margin: the buffer must absorb slip in EITHER
  // direction from its centre, so the usable depth is twice the one-way
  // slip, and the centre itself must exist.
  parameter int unsigned CLOCK_MARGIN  = 2;
  parameter int unsigned DEPTH_CLOCK   = (2 * SLIP_OCTETS) + CLOCK_MARGIN;
 
  // ── Derived: discharge capacity per gap ────────────────────────────────
  parameter int unsigned DISCHARGE_PER_GAP = (MIN_GAP > GAP_RESERVE)
                                           ? (MIN_GAP - GAP_RESERVE) : 0;
 
  // Frames that may pass between discharges before the slip exceeds what
  // one gap can repay. Large is good: it means the mechanism has headroom.
  parameter int unsigned FRAMES_PER_DISCHARGE =
      (SLIP_OCTETS == 0) ? 1_000_000 : (DISCHARGE_PER_GAP * 1_000_000)
                                      / (SLIP_SCALED / MAX_FRAME == 0 ? 1
                                         : (SLIP_SCALED / MAX_FRAME));
 
endpackage
 
module elastic_depth_calc
  import elastic_pkg::*;
#(
  // The burst requirement comes from Chapter 4.3 §10 and is a completely
  // separate calculation with a different cause. It is an INPUT here so the
  // two are visibly added rather than silently merged.
  parameter int unsigned DEPTH_BURST = 2048
) (
  output int unsigned depth_clock,
  output int unsigned depth_burst,
  output int unsigned depth_total,
  output int unsigned discharge_per_gap,
  output int unsigned frames_per_discharge,
 
  // Asserted at elaboration if the discharge capacity cannot keep up with
  // the slip. On any standard configuration this is comfortably false --
  // and a configuration where it is true is one where the gap has been
  // shortened or the tolerance loosened beyond what the mechanism supports.
  output logic        discharge_insufficient
);
 
  assign depth_clock          = DEPTH_CLOCK;
  assign depth_burst          = DEPTH_BURST;
  // ADDED, not maxed. The two accumulations are independent and can be
  // adverse simultaneously: a burst can arrive while the buffer is already
  // displaced from centre by clock slip.
  assign depth_total          = DEPTH_CLOCK + DEPTH_BURST;
  assign discharge_per_gap    = DISCHARGE_PER_GAP;
  assign frames_per_discharge = FRAMES_PER_DISCHARGE;
  assign discharge_insufficient = (DISCHARGE_PER_GAP == 0);
 
endmodule

// SYNTHESIZABLE. The elastic buffer.
//
// THE DIFFERENCE FROM AN ORDINARY FIFO, and it is the whole design:
//
//   An ordinary FIFO starts EMPTY. Empty is its correct idle state, and it
//   fills when the producer is ahead.
//
//   An elastic FIFO starts HALF FULL, and half full is its correct idle
//   state. It must absorb drift in EITHER direction -- the local clock may
//   be faster or slower and which is not known at design time -- so it
//   needs room to both grow and shrink from wherever it sits.
//
// Every decision here is made against DISTANCE FROM CENTRE, never against
// fullness. A design that thinks in terms of "how full" will insert when it
// should delete on half the links it is deployed on.
module elastic_fifo
  import elastic_pkg::*;
#(
  parameter int unsigned W     = 8,
  parameter int unsigned DEPTH = 16,
  parameter int unsigned PTR_W = $clog2(DEPTH),
  // Distance from centre at which compensation is requested. Small enough
  // that a gap arrives before the buffer is in trouble; large enough that
  // it does not compensate on every gap for no reason.
  parameter int unsigned TRIGGER = 2
) (
  input  logic clk_wr,
  input  logic clk_rd,
  input  logic rst_n,
 
  // Write side, in the recovered clock domain.
  input  logic         wr_en,
  input  logic [W-1:0] wr_data,
 
  // Read side, in the local clock domain.
  input  logic         rd_en,
  output logic [W-1:0] rd_data,
 
  // Compensation requests, evaluated in the READ domain because that is
  // where the local clock lives and where the discharge is applied.
  output logic         request_delete,   // buffer above centre: drop an idle
  output logic         request_insert,   // buffer below centre: add an idle
  input  logic         in_gap,           // a gap is available now
 
  // Distance from centre, signed. THIS is the health metric, not fill --
  // Section 9 explains why the trend of this number is what matters.
  output logic signed [PTR_W:0] offset_from_centre,
 
  output logic         overrun,
  output logic         underrun
);
 
  localparam int unsigned CENTRE = DEPTH / 2;
 
  logic [W-1:0]     mem [DEPTH];
  logic [PTR_W-1:0] wptr_q, rptr_q;
  logic [PTR_W:0]   count_q;
 
  // The count is maintained in the read domain here for readability. A real
  // design must carry the pointers across the domain boundary with proper
  // synchronisation -- Chapter 4.6 owns that, and Section 13's rejected
  // property is about exactly why this simplification is dangerous to
  // reason from.
  always_ff @(posedge clk_wr or negedge rst_n) begin
    if (!rst_n) wptr_q <= '0;
    else if (wr_en) begin
      mem[wptr_q] <= wr_data;
      wptr_q      <= wptr_q + 1'b1;
    end
  end
 
  always_ff @(posedge clk_rd or negedge rst_n) begin
    if (!rst_n) begin
      rptr_q   <= '0;
      // START AT CENTRE. An elastic buffer that starts empty underruns on
      // its first read if the local clock is the faster one.
      count_q  <= (PTR_W+1)'(CENTRE);
      overrun  <= 1'b0;
      underrun <= 1'b0;
    end else begin
      if (rd_en) rptr_q <= rptr_q + 1'b1;
 
      // Fill tracking, simplified as noted above.
      case ({wr_en, rd_en})
        2'b10: count_q <= count_q + 1'b1;
        2'b01: count_q <= count_q - 1'b1;
        default: ;   // both or neither: no net change
      endcase
 
      overrun  <= (count_q >= (PTR_W+1)'(DEPTH - 1)) && wr_en && !rd_en;
      underrun <= (count_q == '0) && rd_en && !wr_en;
    end
  end
 
  assign rd_data            = mem[rptr_q];
  assign offset_from_centre = (PTR_W+1)'(count_q) - (PTR_W+1)'(CENTRE);
 
  // Compensation is requested on DISTANCE FROM CENTRE and applied only when
  // a gap is available. Requesting mid-frame would mean deleting a data
  // octet, which is not compensation -- it is corruption.
  assign request_delete = in_gap && (offset_from_centre >  (PTR_W+1)'(TRIGGER));
  assign request_insert = in_gap && (offset_from_centre < -(PTR_W+1)'(TRIGGER));
 
endmodule

// SYNTHESIZABLE. Idle insertion and deletion within a gap.
//
// Two constraints the controller must respect, and the second is the one
// designs get wrong:
//
//   1. Only in a gap. Deleting an octet mid-frame is corruption.
//   2. The gap has a RESERVE that must survive. Published guidance for one
//      gigabit family is that removal must not leave fewer than 8 octets
//      including the end and start markers -- so deletion capacity per gap
//      is finite, and a controller that deletes greedily will shorten a gap
//      below what the far end needs to delineate frames.
//
// Constraint 2 is why compensation is spread across gaps rather than done
// all at once, and why Section 5's frames_per_discharge headroom matters.
module idle_compensator
  import elastic_pkg::*;
#(
  parameter int unsigned CNT_W       = 24,
  parameter int unsigned GAP_MIN     = 12,
  parameter int unsigned GAP_RESERVE_LOCAL = 8,
  parameter int unsigned GAP_W       = $clog2(GAP_MIN + 34)
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic in_frame,
  input  logic request_delete,
  input  logic request_insert,
 
  // Idle octets seen so far in the current gap.
  input  logic idle_octet,
 
  output logic do_delete,
  output logic do_insert,
 
  // ── Observability ───────────────────────────────────────────────────────
  output logic [CNT_W-1:0] c_deleted,
  output logic [CNT_W-1:0] c_inserted,
 
  // A compensation was needed and no gap was available to do it in. This is
  // the early warning that the discharge opportunity is disappearing, and
  // it fires LONG BEFORE the buffer overruns -- which is the difference
  // between a diagnosable fault and a mysterious one.
  output logic             deferred,
  output logic [CNT_W-1:0] c_deferred,
  output logic [15:0]      longest_deferral,
 
  // A gap arrived that was already at or below the reserve, so nothing
  // could be removed from it even though removal was wanted. Distinct from
  // `deferred` -- this one names the MAC as the cause.
  output logic [CNT_W-1:0] c_gap_below_reserve
);
 
  logic [GAP_W-1:0] gap_len_q;
  logic [15:0]      defer_run_q;
  logic             in_gap_c;
 
  assign in_gap_c = !in_frame;
 
  // Deletion is permitted only while the gap still exceeds its reserve.
  wire can_delete_c = in_gap_c && (gap_len_q > GAP_W'(GAP_RESERVE_LOCAL));
  // Insertion always has room -- lengthening a gap is harmless.
  wire can_insert_c = in_gap_c;
 
  assign do_delete = request_delete && can_delete_c;
  assign do_insert = request_insert && can_insert_c;
  assign deferred  = (request_delete && !can_delete_c)
                  || (request_insert && !can_insert_c);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      gap_len_q           <= '0;
      c_deleted           <= '0;
      c_inserted          <= '0;
      c_deferred          <= '0;
      defer_run_q         <= '0;
      longest_deferral    <= '0;
      c_gap_below_reserve <= '0;
    end else begin
      if (clear) begin
        c_deleted           <= '0;
        c_inserted          <= '0;
        c_deferred          <= '0;
        longest_deferral    <= '0;
        c_gap_below_reserve <= '0;
      end
 
      // Gap length accounting.
      if (in_frame) begin
        // A gap just ended. If it was below the reserve and we wanted to
        // delete, the MAC gave us nowhere to work.
        if (gap_len_q != '0) begin
          if ((gap_len_q <= GAP_W'(GAP_RESERVE_LOCAL)) && !(&c_gap_below_reserve))
            c_gap_below_reserve <= c_gap_below_reserve + 1'b1;
        end
        gap_len_q <= '0;
      end else if (idle_octet && !(&gap_len_q)) begin
        gap_len_q <= gap_len_q + 1'b1;
      end
 
      if (do_delete) begin
        if (!(&c_deleted)) c_deleted <= c_deleted + 1'b1;
        // A deletion consumes one octet of the gap.
        if (gap_len_q != '0) gap_len_q <= gap_len_q - 1'b1;
      end
      if (do_insert && !(&c_inserted)) c_inserted <= c_inserted + 1'b1;
 
      if (deferred) begin
        if (!(&c_deferred)) c_deferred <= c_deferred + 1'b1;
        defer_run_q <= defer_run_q + 1'b1;
        if (defer_run_q + 1'b1 > longest_deferral)
          longest_deferral <= defer_run_q + 1'b1;
      end else begin
        defer_run_q <= '0;
      end
    end
  end
 
endmodule

// SYNTHESIZABLE INSTRUMENTATION.
//
// FILL IS A READING. DRIFT IS THE HEALTH METRIC.
//
// A buffer sitting at 60 percent tells you nothing -- it may have sat there
// for a year. A buffer whose offset from centre has been growing by one
// octet per second for an hour is a link that will fail, and it is still
// reporting healthy on every instantaneous check.
//
// This is the same argument Chapter 3.3 made for margin, Chapter 3.7 for
// the pre-correction error rate, and Chapter 3.8 for skew margin. At every
// layer: measure what degrades continuously, and treat what degrades
// discontinuously as an alarm of last resort.
module drift_monitor #(
  parameter int unsigned PTR_W  = 5,
  parameter int unsigned WINDOW = 1_000_000,
  parameter int unsigned WIN_W  = $clog2(WINDOW + 1),
  parameter int unsigned CNT_W  = 24
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic signed [PTR_W:0] offset_from_centre,
  input  logic                  do_delete,
  input  logic                  do_insert,
 
  // Offset at the start and end of the window that just closed. Their
  // difference is the NET drift the compensation failed to remove -- which
  // should be near zero on a healthy link.
  output logic signed [PTR_W:0] window_start_offset,
  output logic signed [PTR_W:0] window_end_offset,
  output logic signed [PTR_W+1:0] window_net_drift,
  output logic                  window_valid,
 
  // Compensation applied during the window. The ratio of deletions to
  // insertions says WHICH clock is faster, which is a fact about the
  // installation and worth knowing.
  output logic [CNT_W-1:0] window_deletes,
  output logic [CNT_W-1:0] window_inserts,
 
  // Extremes since reset. Survive `clear`: they are properties of the
  // installed link, not of a window an operator happened to choose.
  output logic signed [PTR_W:0] worst_high,
  output logic signed [PTR_W:0] worst_low,
 
  // Net drift did not return to near zero across the window, meaning
  // compensation is not keeping up. This is the finding, and it precedes
  // any overrun by a wide margin.
  output logic                  drift_uncompensated
);
 
  logic [WIN_W-1:0] win_q;
  logic [CNT_W-1:0] del_q, ins_q;
  logic signed [PTR_W:0] start_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      win_q               <= '0;
      del_q               <= '0;
      ins_q               <= '0;
      start_q             <= '0;
      window_start_offset <= '0;
      window_end_offset   <= '0;
      window_deletes      <= '0;
      window_inserts      <= '0;
      window_valid        <= 1'b0;
      worst_high          <= '0;
      worst_low           <= '0;
    end else begin
      if (clear) begin
        win_q        <= '0;
        del_q        <= '0;
        ins_q        <= '0;
        window_valid <= 1'b0;
        // worst_high and worst_low deliberately survive.
      end else begin
        if (do_delete && !(&del_q)) del_q <= del_q + 1'b1;
        if (do_insert && !(&ins_q)) ins_q <= ins_q + 1'b1;
 
        if (offset_from_centre > worst_high) worst_high <= offset_from_centre;
        if (offset_from_centre < worst_low)  worst_low  <= offset_from_centre;
 
        if (win_q == WIN_W'(WINDOW - 1)) begin
          window_start_offset <= start_q;
          window_end_offset   <= offset_from_centre;
          window_deletes      <= del_q;
          window_inserts      <= ins_q;
          window_valid        <= 1'b1;
          start_q             <= offset_from_centre;
          del_q               <= '0;
          ins_q               <= '0;
          win_q               <= '0;
        end else begin
          win_q <= win_q + 1'b1;
        end
      end
    end
  end
 
  assign window_net_drift = (PTR_W+2)'(window_end_offset) - (PTR_W+2)'(window_start_offset);
  // On a healthy link compensation returns the offset to near where it
  // started. A persistent net drift means it is not keeping up.
  assign drift_uncompensated = window_valid
                            && ((window_net_drift > 2) || (window_net_drift < -2));
 
endmodule

// SYNTHESIZABLE INSTRUMENTATION.
//
// OVERRUN and UNDERRUN are not two sides of one fault:
//
//   OVERRUN  -- the incoming rate exceeded the local one and the buffer
//               filled. DATA IS LOST. The local clock is slower, or
//               deletions were deferred.
//
//   UNDERRUN -- the local rate exceeded the incoming one and the buffer
//               emptied. NO DATA IS LOST -- the read side must emit
//               something, and what it emits is idle. The local clock is
//               faster, or insertions were deferred.
//
// One destroys data and the other does not. A shared counter makes a lossy
// link and a merely mistimed one read identically.
module buffer_fault_classifier #(
  parameter int unsigned PTR_W = 5,
  parameter int unsigned CNT_W = 24
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic overrun,
  input  logic underrun,
  input  logic in_frame,
  input  logic deferred_delete,
  input  logic deferred_insert,
 
  output logic [CNT_W-1:0] c_overrun,
  output logic [CNT_W-1:0] c_underrun,
 
  // An overrun that happened INSIDE a frame destroys that frame. One in a
  // gap costs nothing. Same event, completely different consequence.
  output logic [CNT_W-1:0] c_overrun_in_frame,
  output logic [CNT_W-1:0] c_overrun_in_gap,
 
  // Was a compensation deferred before the fault? If so, the cause is
  // upstream -- a gap too short -- rather than the buffer being too small.
  // This is the attribution that decides which team owns the problem.
  output logic             preceded_by_deferral,
  output logic [CNT_W-1:0] c_fault_after_deferral,
 
  // First fault kind since reset, held. During an incident both will be
  // set; which came first says which clock is the faster one.
  output logic             first_was_overrun,
  output logic             first_fault_valid
);
 
  logic deferral_recent_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
      c_overrun              <= '0;
      c_underrun             <= '0;
      c_overrun_in_frame     <= '0;
      c_overrun_in_gap       <= '0;
      c_fault_after_deferral <= '0;
      deferral_recent_q      <= 1'b0;
      first_was_overrun      <= 1'b0;
      first_fault_valid      <= 1'b0;
    end else begin
      if (clear) begin
        c_overrun              <= '0;
        c_underrun             <= '0;
        c_overrun_in_frame     <= '0;
        c_overrun_in_gap       <= '0;
        c_fault_after_deferral <= '0;
      end else begin
        c_overrun  <= bump(c_overrun,  overrun);
        c_underrun <= bump(c_underrun, underrun);
        c_overrun_in_frame <= bump(c_overrun_in_frame, overrun &&  in_frame);
        c_overrun_in_gap   <= bump(c_overrun_in_gap,   overrun && !in_frame);
        c_fault_after_deferral <= bump(c_fault_after_deferral,
                                       (overrun || underrun) && deferral_recent_q);
      end
 
      // A recent deferral makes the fault upstream's, not the buffer's.
      if (deferred_delete || deferred_insert) deferral_recent_q <= 1'b1;
      else if (overrun || underrun)           deferral_recent_q <= 1'b0;
 
      if (!first_fault_valid && (overrun || underrun)) begin
        first_fault_valid <= 1'b1;
        first_was_overrun <= overrun;
      end
    end
  end
 
  assign preceded_by_deferral = deferral_recent_q;
 
endmodule

// ─── Safety: compensation happens only in a gap ────────────────────────────
// The single most important property here. Deleting an octet mid-frame is
// not compensation -- it is corruption, and the frame's check value then
// fails for a reason unrelated to anything the link did.
property p_compensate_only_in_gap;
  @(posedge clk) disable iff (!rst_n)
  (do_delete || do_insert) |-> !in_frame;
endproperty
 
// ─── Safety: the gap reserve survives ──────────────────────────────────────
// Rests on the published requirement that removal must leave enough for
// frame delineation. Catches a greedy controller that shortens a gap below
// what the far end needs.
property p_reserve_survives_deletion;
  @(posedge clk) disable iff (!rst_n)
  do_delete |-> (gap_len_q > GAP_RESERVE_LOCAL);
endproperty
 
// ─── Causation: compensation direction follows the offset ──────────────────
// Catches the classic inversion -- deleting when the buffer is below centre
// -- which is correct-looking logic that accelerates the drift it is
// supposed to remove.
property p_delete_only_when_above_centre;
  @(posedge clk) disable iff (!rst_n)
  request_delete |-> (offset_from_centre > 0);
endproperty
 
property p_insert_only_when_below_centre;
  @(posedge clk) disable iff (!rst_n)
  request_insert |-> (offset_from_centre < 0);
endproperty
 
// ─── Safety: the buffer starts at centre, not empty ────────────────────────
// Catches an elastic buffer initialised like an ordinary FIFO, which
// underruns on its first read whenever the local clock is the faster one --
// so it works on half the links it is deployed on.
property p_starts_at_centre;
  @(posedge clk) disable iff (!rst_n)
  $rose(rst_n) |-> (offset_from_centre == 0);
endproperty
 
// ─── Conservation: depth is the sum, not the maximum ───────────────────────
// An elaboration-time check. Catches a design that takes the larger of the
// two requirements, leaving no room for the other when both are adverse.
property p_depth_is_sum;
  @(posedge clk) disable iff (!rst_n)
  (depth_total == depth_clock + depth_burst);
endproperty
 
// ─── Safety: a deferral is recorded, never dropped ─────────────────────────
// The early warning. Catches a controller that silently gives up on a
// compensation it could not perform, removing the only signal that precedes
// an overrun by a useful margin.
property p_deferral_is_counted;
  @(posedge clk) disable iff (!rst_n)
  deferred |=> (c_deferred == $past(c_deferred) + 1);
endproperty
 
// ─── Mutual exclusion: overrun and underrun cannot coincide ────────────────
// Catches a fill calculation that can report both, which means the count is
// wrong rather than that the buffer is in trouble.
property p_not_both_faults;
  @(posedge clk) disable iff (!rst_n)
  !(overrun && underrun);
endproperty
 
// ─── Causation: an in-frame overrun is classified as such ──────────────────
// Catches a total-only overrun counter, which alarms on harmless gap
// overruns and hides frame-destroying ones behind the same number.
property p_overrun_classified;
  @(posedge clk) disable iff (!rst_n)
  overrun |-> (c_overrun_in_frame != $past(c_overrun_in_frame))
           || (c_overrun_in_gap   != $past(c_overrun_in_gap));
endproperty
 
// ─── Stability: the historical extremes survive a clear ────────────────────
// Catches worst_high and worst_low folded into the clear branch, destroying
// the record of how far this link has ever drifted.
property p_extremes_survive_clear;
  @(posedge clk) disable iff (!rst_n)
  clear |=> ((worst_high >= $past(worst_high)) && (worst_low <= $past(worst_low)));
endproperty
 
// ─── Bounded response: a window always closes ──────────────────────────────
// Catches a window counter that can be starved, so the drift trend never
// produces a data point and the early warning never arrives.
property p_drift_window_closes;
  @(posedge clk) disable iff (!rst_n)
  $rose(rst_n) |-> ##[1:WINDOW+1] window_valid;
endproperty
 
// ─── Causation: a fault after a deferral is attributed upstream ────────────
// Catches the attribution being lost, after which every buffer fault looks
// like a sizing problem and the investigation never reaches the gap.
property p_deferral_attribution_held;
  @(posedge clk) disable iff (!rst_n)
  (deferred_delete || deferred_insert) |=> preceded_by_deferral;
endproperty