PAUSE Frames

// -----------------------------------------------------------------------
// pause_pkg -- shared types for 802.3x flow control.
// -----------------------------------------------------------------------
package pause_pkg;

  // The reserved multicast that must never be forwarded. Chapter 12.4's
  // flooding, Chapter 12.2's learning and Chapter 12.3's gates all have
  // to exclude it explicitly -- nothing about its FORM marks it special.
  localparam logic [47:0] PAUSE_DA   = 48'h0180_C200_0001;
  localparam logic [15:0] MAC_CTRL   = 16'h8808;
  localparam logic [15:0] OP_PAUSE   = 16'h0001;

  // A quantum is 512 BIT TIMES, so its duration depends on the line rate.
  localparam int QUANTUM_BITS = 512;
  localparam int MAX_QUANTA   = 65535;

  typedef enum logic [2:0] {
    PR_OK          = 3'd0,
    PR_NOT_CONTROL = 3'd1,  // wrong EtherType
    PR_WRONG_OP    = 3'd2,  // MAC control, but not PAUSE
    PR_WRONG_DA    = 3'd3,  // a PAUSE addressed to somebody else
    PR_BAD_LEN     = 3'd4,
    PR_NOT_ENABLED = 3'd5   // this port does not honour PAUSE
  } pause_reject_e;

  // What the transmitter is doing about a pause it has been given.
  typedef enum logic [1:0] {
    TX_RUNNING   = 2'd0,
    TX_FINISHING = 2'd1,   // mid-frame -- must complete it
    TX_PAUSED    = 2'd2
  } tx_state_e;

endpackage

// -----------------------------------------------------------------------
// pause_frame_builder -- constructs a 64-octet MAC control frame.
//
// The frame is exactly the minimum length, which is not a coincidence:
// 6 + 6 + 2 + 2 + 2 = 18 octets of content, 42 of padding and 4 of FCS.
// Everything after the pause_time field is zeros that exist only to reach
// Chapter 5.6's floor.
// -----------------------------------------------------------------------
module pause_frame_builder
  import pause_pkg::*;
#(
  parameter int CNT_W = 32
)(
  input  logic             clk,
  input  logic             rst_n,

  input  logic             send_req,
  input  logic [15:0]      quanta,
  input  logic [47:0]      my_address,

  output logic             frame_valid,
  output logic [511:0]     frame_head,     // first 64 octets, MSB first
  output logic [13:0]      frame_len,
  output logic             is_release,     // quanta == 0

  output logic [CNT_W-1:0] c_pause_sent,
  output logic [CNT_W-1:0] c_release_sent,
  output logic [CNT_W-1:0] quanta_sent_total
);

  // A pause_time of ZERO is a RELEASE, not a zero-length pause. It is the
  // only way to end a pause early, and a design that treats it as "pause
  // for no time" has a mechanism that cannot be cancelled.
  assign is_release = (quanta == 16'd0);

  assign frame_len = 14'd64;

  always_comb begin
    frame_head = '0;
    frame_head[511 -: 48]  = PAUSE_DA;      // octets 0-5
    frame_head[463 -: 48]  = my_address;    // octets 6-11
    frame_head[415 -: 16]  = MAC_CTRL;      // octets 12-13
    frame_head[399 -: 16]  = OP_PAUSE;      // octets 14-15
    frame_head[383 -: 16]  = quanta;        // octets 16-17
    // octets 18-59 remain zero: Chapter 5.6's padding to the 64-octet
    // floor. Chapter 13.3 Section 12 established that padding beyond a
    // payload's declared length is invisible to the layer above, and here
    // there is no payload at all.
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      frame_valid       <= 1'b0;
      c_pause_sent      <= '0;
      c_release_sent    <= '0;
      quanta_sent_total <= '0;
    end else begin
      frame_valid <= send_req;
      if (send_req) begin
        if (is_release) begin
          if (!(&c_release_sent)) c_release_sent <= c_release_sent + 1'b1;
        end else begin
          if (!(&c_pause_sent)) c_pause_sent <= c_pause_sent + 1'b1;
          quanta_sent_total <= quanta_sent_total + CNT_W'(quanta);
        end
      end
    end
  end

endmodule

// -----------------------------------------------------------------------
// pause_frame_parser -- is this a PAUSE for us, and is it valid?
//
// The destination check is the one that gets left out, and omitting it
// means honouring a PAUSE that was addressed to a different device --
// which on a shared segment is a station stopping traffic it has no
// authority over.
// -----------------------------------------------------------------------
module pause_frame_parser
  import pause_pkg::*;
#(
  parameter int CNT_W = 32
)(
  input  logic             clk,
  input  logic             rst_n,

  input  logic             rx_valid,
  input  logic [47:0]      rx_da,
  input  logic [15:0]      rx_ethertype,
  input  logic [15:0]      rx_opcode,
  input  logic [15:0]      rx_quanta,
  input  logic [13:0]      rx_len,
  input  logic             pause_enabled,   // negotiated -- Chapter 11.2

  output logic             pause_valid,
  output logic [15:0]      quanta,
  output logic             is_release,
  output pause_reject_e    reject,

  output logic             consume,         // never forward this frame
  output logic [CNT_W-1:0] c_pause_rx,
  output logic [CNT_W-1:0] c_rejected [6],
  output logic [CNT_W-1:0] quanta_rx_total
);

  always_comb begin
    pause_valid = 1'b0;
    reject      = PR_OK;

    if (rx_valid) begin
      // THE DESTINATION CHECK. A PAUSE is link-local and addressed to the
      // reserved multicast; one addressed anywhere else is not a PAUSE
      // for this device, whatever its opcode says.
      if (rx_da != PAUSE_DA)            reject = PR_WRONG_DA;
      else if (rx_ethertype != MAC_CTRL) reject = PR_NOT_CONTROL;
      else if (rx_opcode != OP_PAUSE)    reject = PR_WRONG_OP;
      else if (rx_len != 14'd64)         reject = PR_BAD_LEN;
      else if (!pause_enabled)           reject = PR_NOT_ENABLED;
      else                               pause_valid = 1'b1;
    end
  end

  // CONSUMED, NOT FORWARDED -- and consumed even when this port does not
  // honour PAUSE. Chapter 12.4's flooding must never see this address:
  // forwarding a PAUSE means telling somebody else to stop, which is not
  // a statement the frame can make.
  assign consume    = rx_valid && (rx_da == PAUSE_DA) &&
                      (rx_ethertype == MAC_CTRL);
  assign quanta     = pause_valid ? rx_quanta : 16'd0;
  assign is_release = pause_valid && (rx_quanta == 16'd0);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      c_pause_rx <= '0;
      quanta_rx_total <= '0;
      for (int i = 0; i < 6; i++) c_rejected[i] <= '0;
    end else if (rx_valid) begin
      if (pause_valid) begin
        c_pause_rx      <= c_pause_rx + 1'b1;
        quanta_rx_total <= quanta_rx_total + CNT_W'(rx_quanta);
      end else begin
        c_rejected[reject[2:0]] <= c_rejected[reject[2:0]] + 1'b1;
      end
    end
  end

endmodule

// -----------------------------------------------------------------------
// pause_trigger -- watermark crossings to PAUSE and RELEASE decisions.
//
// The asymmetry between the thresholds is the whole design. Asserting at
// HIGH leaves Section 5's headroom for the dead time; releasing at LOW
// rather than at HIGH prevents the mechanism oscillating once per frame.
// -----------------------------------------------------------------------
module pause_trigger
  import pause_pkg::*;
#(
  parameter int HIGH_CELLS   = 3072,
  parameter int LOW_CELLS    = 1024,
  parameter int PAUSE_QUANTA = 1000,     // ~512 us at 1 Gb/s
  parameter int REISSUE_AT   = 700,      // re-issue before it expires
  parameter int CNT_W        = 32
)(
  input  logic             clk,
  input  logic             rst_n,
  input  logic             quantum_tick,      // one per 512 bit times

  input  logic [15:0]      occupancy_cells,
  input  logic             tx_ready,          // the transmitter took it

  output logic             send_pause,
  output logic [15:0]      send_quanta,
  output logic             paused_state,

  output logic [CNT_W-1:0] c_asserted,
  output logic [CNT_W-1:0] c_reissued,
  output logic [CNT_W-1:0] c_released,
  output logic [CNT_W-1:0] quanta_outstanding,
  output logic [CNT_W-1:0] c_late_reissue     // expired before re-issuing
);

  logic [15:0] remaining;

  always_comb begin
    send_pause  = 1'b0;
    send_quanta = 16'd0;

    if (!paused_state && (occupancy_cells >= 16'(HIGH_CELLS))) begin
      // ASSERT at HIGH, not at full. Section 5's headroom is the space
      // between HIGH and the queue's limit, and it must cover the dead
      // time's worth of arrivals.
      send_pause  = 1'b1;
      send_quanta = 16'(PAUSE_QUANTA);
    end else if (paused_state && (occupancy_cells <= 16'(LOW_CELLS))) begin
      // RELEASE with pause_time = 0. Section 3 established this is the
      // only way to end a pause early, and without it the link stays idle
      // for however long was asked for.
      send_pause  = 1'b1;
      send_quanta = 16'd0;
    end else if (paused_state && (remaining <= 16'(PAUSE_QUANTA - REISSUE_AT))) begin
      // RE-ISSUE BEFORE EXPIRY. A pause that lapses while the queue is
      // still above LOW lets the sender resume, and the queue -- which
      // has not drained -- overflows during the next dead time. The
      // re-issue must arrive before the current one expires.
      send_pause  = 1'b1;
      send_quanta = 16'(PAUSE_QUANTA);
    end
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      paused_state       <= 1'b0;
      remaining          <= '0;
      c_asserted         <= '0;
      c_reissued         <= '0;
      c_released         <= '0;
      quanta_outstanding <= '0;
      c_late_reissue     <= '0;
    end else begin
      if (send_pause && tx_ready) begin
        if (send_quanta == 16'd0) begin
          paused_state <= 1'b0;
          remaining    <= '0;
          if (!(&c_released)) c_released <= c_released + 1'b1;
        end else begin
          if (!paused_state) begin
            if (!(&c_asserted)) c_asserted <= c_asserted + 1'b1;
          end else begin
            if (!(&c_reissued)) c_reissued <= c_reissued + 1'b1;
          end
          paused_state       <= 1'b1;
          remaining          <= send_quanta;
          quanta_outstanding <= quanta_outstanding + CNT_W'(send_quanta);
        end
      end

      if (quantum_tick && (remaining != 16'd0)) begin
        remaining <= remaining - 16'd1;
        // The pause expired while the queue was still above LOW. The
        // sender is now free to resume into a queue that has not drained.
        if ((remaining == 16'd1) && (occupancy_cells > 16'(LOW_CELLS)))
          if (!(&c_late_reissue)) c_late_reissue <= c_late_reissue + 1'b1;
      end
    end
  end

endmodule

// -----------------------------------------------------------------------
// headroom_calculator -- where the HIGH watermark must sit.
//
// Section 5's dead time, converted into cells. A design that picks a
// watermark by intuition is picking a link length and a neighbour's frame
// size without knowing it.
// -----------------------------------------------------------------------
module headroom_calculator
  import pause_pkg::*;
#(
  parameter int LINK_MBPS   = 1000,
  parameter int CELL_OCTETS = 128,
  parameter int CABLE_M     = 100,
  parameter int NS_PER_M    = 5,        // ~5 ns/m in copper, ~5 in fibre
  parameter int MAX_FRAME   = 1518,
  parameter int QUEUE_CELLS = 4096
)(
  input  logic         clk,
  input  logic         rst_n,

  input  logic [15:0]  tx_backlog_octets,   // ahead of the PAUSE in the TX path

  output logic [19:0]  dead_time_ns,
  output logic [19:0]  headroom_octets,
  output logic [15:0]  headroom_cells,
  output logic [15:0]  high_watermark_cells,
  output logic [15:0]  prop_share_pct,
  output logic         watermark_infeasible   // headroom exceeds the queue
);

  // Three components, Section 5's table. The PAUSE frame is 84 octets on
  // the wire including Chapter 5.2's preamble and the interframe gap.
  localparam int PAUSE_TX_NS = (84 * 8 * 1000) / LINK_MBPS;
  localparam int PROP_NS     = CABLE_M * NS_PER_M;
  localparam int FINISH_NS   = (MAX_FRAME * 8 * 1000) / LINK_MBPS;

  // tx_backlog is what sits AHEAD of the PAUSE in our own transmit path.
  // Section 11: a PAUSE queued behind ordinary traffic arrives late by
  // exactly the amount that matters.
  logic [19:0] backlog_ns;
  assign backlog_ns = (20'(tx_backlog_octets) * 20'd8 * 20'd1000) / 20'(LINK_MBPS);

  assign dead_time_ns = 20'(PAUSE_TX_NS) + 20'(PROP_NS) +
                        20'(FINISH_NS) + backlog_ns;

  // Octets that arrive during the dead time, at the neighbour's line rate.
  assign headroom_octets = (dead_time_ns * 20'(LINK_MBPS)) / 20'd8000;
  assign headroom_cells  = 16'((headroom_octets + 20'(CELL_OCTETS) - 20'd1) /
                               20'(CELL_OCTETS));

  // The watermark is the queue's limit MINUS the headroom, not a fraction
  // of the queue. A design that sets it at 75% has assumed a headroom.
  assign high_watermark_cells = (16'(QUEUE_CELLS) > headroom_cells)
                              ? (16'(QUEUE_CELLS) - headroom_cells) : 16'd0;

  // Propagation's share, which is what grows with line rate -- Section 5.
  assign prop_share_pct = 16'((20'(PROP_NS) * 20'd100) / dead_time_ns);

  // A QUEUE TOO SMALL TO PAUSE FROM. If the headroom exceeds the queue,
  // there is no watermark at which a pause can be issued in time, and the
  // mechanism cannot work on this link at all.
  assign watermark_infeasible = (headroom_cells >= 16'(QUEUE_CELLS));

endmodule

// -----------------------------------------------------------------------
// pause_timer -- counts down a received pause, in quanta.
//
// A quantum is 512 bit times, so the tick generator is a divider off the
// transmit clock rather than a wall-clock timer. That is what makes the
// duration rate-relative and Section 2's ceiling rate-dependent.
// -----------------------------------------------------------------------
module pause_timer
  import pause_pkg::*;
#(
  parameter int CNT_W = 32
)(
  input  logic             clk,
  input  logic             rst_n,
  input  logic             quantum_tick,     // one per 512 bit times

  input  logic             pause_valid,
  input  logic [15:0]      quanta,

  output logic             paused,
  output logic [15:0]      remaining,
  output logic [CNT_W-1:0] c_paused_quanta,
  output logic [CNT_W-1:0] c_overwritten,    // a pause arrived while paused
  output logic [CNT_W-1:0] c_released_early,
  output logic [19:0]      longest_pause_q,
  output logic [15:0]      idle_pct_x100     // share of time paused
);

  logic [CNT_W-1:0] ticks_total, ticks_paused;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      remaining        <= '0;
      c_paused_quanta  <= '0;
      c_overwritten    <= '0;
      c_released_early <= '0;
      longest_pause_q  <= '0;
      ticks_total      <= '0;
      ticks_paused     <= '0;
      idle_pct_x100    <= '0;
    end else begin
      if (pause_valid) begin
        // A NEW PAUSE REPLACES the outstanding one -- it does not add to
        // it. A device re-issuing every 700 quanta is REFRESHING a 1000
        // quantum pause, not accumulating 1700.
        if ((remaining != 16'd0) && (quanta != 16'd0))
          if (!(&c_overwritten)) c_overwritten <= c_overwritten + 1'b1;
        if ((remaining != 16'd0) && (quanta == 16'd0))
          if (!(&c_released_early)) c_released_early <= c_released_early + 1'b1;

        remaining <= quanta;
        if (20'(quanta) > longest_pause_q) longest_pause_q <= 20'(quanta);
      end else if (quantum_tick && (remaining != 16'd0)) begin
        remaining       <= remaining - 16'd1;
        c_paused_quanta <= c_paused_quanta + 1'b1;
      end

      if (quantum_tick) begin
        ticks_total <= ticks_total + 1'b1;
        if (remaining != 16'd0) ticks_paused <= ticks_paused + 1'b1;
        if (ticks_total >= CNT_W'(100_000)) begin
          idle_pct_x100 <= 16'((ticks_paused * CNT_W'(10_000)) / ticks_total);
          ticks_total   <= '0;
          ticks_paused  <= '0;
        end
      end
    end
  end

  assign paused = (remaining != 16'd0);

endmodule

// -----------------------------------------------------------------------
// pause_transmit_gate -- what a paused transmitter actually does.
//
// Three rules that are easy to get wrong:
//   1. A frame in progress is FINISHED. Ethernet cannot abort one.
//   2. A pause does not stop MAC control frames -- otherwise a paused
//      device could never send its own PAUSE or RELEASE.
//   3. The PAUSE we send must not queue behind ordinary traffic, or
//      Section 8's dead time grows by the backlog ahead of it.
// -----------------------------------------------------------------------
module pause_transmit_gate
  import pause_pkg::*;
#(
  parameter int CNT_W = 32
)(
  input  logic             clk,
  input  logic             rst_n,

  input  logic             paused,
  input  logic             frame_pending,
  input  logic             frame_in_progress,
  input  logic             frame_is_control,   // our own PAUSE or RELEASE
  input  logic             frame_end,

  output logic             tx_permit,
  output tx_state_e        state,
  output logic             control_bypass,

  output logic [CNT_W-1:0] c_frames_after_pause,   // finished mid-frame
  output logic [CNT_W-1:0] c_control_through,
  output logic [CNT_W-1:0] c_blocked,
  output logic [15:0]      worst_finish_octets
);

  tx_state_e st_q;
  logic [15:0] finish_octets;

  always_comb begin
    tx_permit      = 1'b0;
    control_bypass = 1'b0;

    // RULE 2, first, because it is the one that makes the mechanism
    // bidirectional. A paused device must still be able to pause ITS
    // neighbour -- otherwise congestion cannot propagate upstream at all,
    // which is Chapter 14.3's subject.
    if (frame_is_control) begin
      tx_permit      = 1'b1;
      control_bypass = 1'b1;
    end else if (frame_in_progress) begin
      // RULE 1. Ethernet has no abort. Chapter 12.6 Section 8 established
      // that a truncated frame is discarded by every receiver, so
      // stopping mid-frame would destroy the frame AND waste the wire.
      tx_permit = 1'b1;
    end else if (!paused) begin
      tx_permit = frame_pending;
    end
  end

  always_comb begin
    if (!paused)                     state = TX_RUNNING;
    else if (frame_in_progress)      state = TX_FINISHING;
    else                             state = TX_PAUSED;
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      st_q                 <= TX_RUNNING;
      finish_octets        <= '0;
      c_frames_after_pause <= '0;
      c_control_through    <= '0;
      c_blocked            <= '0;
      worst_finish_octets  <= '0;
    end else begin
      st_q <= state;

      // MEASURE THE OVERRUN. How many octets did we transmit after being
      // told to stop? Section 5 predicts up to a maximum frame, and a
      // measurement far from that means the neighbour's assumption about
      // our frame size is wrong.
      if (paused && frame_in_progress) begin
        finish_octets <= finish_octets + 16'd1;
      end else if (frame_end) begin
        if (paused && (finish_octets > worst_finish_octets))
          worst_finish_octets <= finish_octets;
        if (paused)
          if (!(&c_frames_after_pause))
            c_frames_after_pause <= c_frames_after_pause + 1'b1;
        finish_octets <= '0;
      end

      if (control_bypass)
        if (!(&c_control_through)) c_control_through <= c_control_through + 1'b1;
      if (paused && frame_pending && !tx_permit)
        if (!(&c_blocked)) c_blocked <= c_blocked + 1'b1;
    end
  end

endmodule

// -----------------------------------------------------------------------
// pause_telemetry -- is flow control helping, and at what cost?
//
// The two conditions that matter both look like success from a drop
// counter: a link paused so often it is running at a fraction of its
// rate, and a pause issued too late to prevent the drop it was for.
// -----------------------------------------------------------------------
module pause_telemetry
  import pause_pkg::*;
#(
  parameter int CNT_W = 32,
  parameter int WIN   = 1_000_000
)(
  input  logic             clk,
  input  logic             rst_n,
  input  logic             quantum_tick,

  input  logic             pause_sent,
  input  logic             pause_rx,
  input  logic             paused_now,
  input  logic             drop_while_paused,
  input  logic             drop_any,
  input  logic [15:0]      occupancy_cells,
  input  logic [15:0]      high_watermark,
  input  logic [CNT_W-1:0] c_late_reissue,

  output logic             window_valid,
  output logic [15:0]      paused_pct_x100,
  output logic [15:0]      effective_rate_pct,
  output logic [15:0]      pause_overhead_ppm,
  output logic             pause_ineffective,   // paused AND still dropping
  output logic             pause_excessive,     // link idle a large fraction
  output logic             pause_too_late,      // Section 7's failure
  output logic [CNT_W-1:0] c_sent,
  output logic [CNT_W-1:0] c_rx
);

  logic [CNT_W-1:0] win_ticks, win_paused, win_sent, win_drop_paused, win_drop;
  logic [CNT_W-1:0] prev_late;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      win_ticks <= '0; win_paused <= '0; win_sent <= '0;
      win_drop_paused <= '0; win_drop <= '0; prev_late <= '0;
      c_sent <= '0; c_rx <= '0;
      window_valid       <= 1'b0;
      paused_pct_x100    <= '0;
      effective_rate_pct <= 16'd100;
      pause_overhead_ppm <= '0;
      pause_ineffective  <= 1'b0;
      pause_excessive    <= 1'b0;
      pause_too_late     <= 1'b0;
    end else begin
      window_valid <= 1'b0;

      if (pause_sent) begin win_sent <= win_sent + 1'b1; c_sent <= c_sent + 1'b1; end
      if (pause_rx)   c_rx <= c_rx + 1'b1;
      if (drop_while_paused) win_drop_paused <= win_drop_paused + 1'b1;
      if (drop_any) win_drop <= win_drop + 1'b1;

      if (quantum_tick) begin
        win_ticks <= win_ticks + 1'b1;
        if (paused_now) win_paused <= win_paused + 1'b1;

        if (win_ticks >= CNT_W'(WIN)) begin
          paused_pct_x100 <= 16'((win_paused * CNT_W'(10_000)) / win_ticks);
          // THE NUMBER NOBODY COMPUTES. A link paused 30% of the time is
          // a 70% link, and no rate counter says so.
          effective_rate_pct <= 16'(100 - ((win_paused * CNT_W'(100)) / win_ticks));
          // The PAUSE frames' own bandwidth: 672 bits each, against
          // 512 bits per quantum of link time.
          pause_overhead_ppm <= 16'((win_sent * CNT_W'(672) * CNT_W'(1_000_000)) /
                                    (win_ticks * CNT_W'(512)));

          // PAUSED AND STILL DROPPING. Either the headroom is wrong --
          // Section 8 -- or the congestion exceeds what pausing one
          // neighbour can fix.
          pause_ineffective <= (win_drop_paused > (win_drop >> 1)) &&
                               (win_drop != '0);
          // The link is idle a large fraction of the time by request.
          pause_excessive   <= (win_paused > (win_ticks >> 2));
          // Section 7's lapsed pause.
          pause_too_late    <= (c_late_reissue != prev_late);

          prev_late <= c_late_reissue;
          win_ticks <= '0; win_paused <= '0; win_sent <= '0;
          win_drop_paused <= '0; win_drop <= '0;
          window_valid <= 1'b1;
        end
      end
    end
  end

  wire _unused = |occupancy_cells | |high_watermark;

endmodule

// -----------------------------------------------------------------------
// pause_conformance_monitor -- checks a control loop whose response is
// late by construction.
//
// The invariant is NOT that no frames arrive after a PAUSE. It is that
// none arrive after the DEAD TIME has elapsed, that the headroom covers
// the dead time, and that the frame itself was well formed and consumed.
// Section 17 is about the difference.
// -----------------------------------------------------------------------
module pause_conformance_monitor
  import pause_pkg::*;
#(
  parameter int CNT_W = 32
)(
  input  logic             clk,
  input  logic             rst_n,
  input  logic             quantum_tick,

  input  logic             pause_tx,           // we transmitted one
  input  logic [15:0]      tx_quanta,
  input  logic [19:0]      dead_time_ns,
  input  logic [19:0]      ns_since_pause,
  input  logic             rx_frame,           // a frame arrived from them
  input  logic             rx_is_control,

  input  logic             pause_rx,           // we received one
  input  logic             we_transmitted,
  input  logic             we_were_paused,
  input  logic             tx_was_control,
  input  logic             tx_in_progress,

  input  logic [15:0]      headroom_cells,
  input  logic [15:0]      queue_cells,
  input  logic [47:0]      rx_pause_da,
  input  logic             pause_forwarded,

  output logic [CNT_W-1:0] v_late_arrival,     // after the dead time
  output logic [CNT_W-1:0] v_transmitted_paused,
  output logic [CNT_W-1:0] v_pause_forwarded,  // must never happen
  output logic [CNT_W-1:0] v_headroom_short,
  output logic [CNT_W-1:0] v_control_blocked,
  output logic             headroom_feasible,
  output logic             conformant
);

  // A STANDING PROPERTY. If the dead time's arrivals exceed the queue,
  // no watermark works and the mechanism cannot function on this link.
  assign headroom_feasible = (headroom_cells < queue_cells);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      v_late_arrival       <= '0;
      v_transmitted_paused <= '0;
      v_pause_forwarded    <= '0;
      v_headroom_short     <= '0;
      v_control_blocked    <= '0;
    end else begin
      // THE REAL CHECK. Frames arriving DURING the dead time are
      // expected; frames arriving AFTER it are the neighbour ignoring us.
      if (rx_frame && !rx_is_control &&
          (ns_since_pause > dead_time_ns) && (tx_quanta != 16'd0))
        if (!(&v_late_arrival)) v_late_arrival <= v_late_arrival + 1'b1;

      // We transmitted ordinary traffic while paused, and not because we
      // were finishing a frame.
      if (we_transmitted && we_were_paused && !tx_was_control && !tx_in_progress)
        if (!(&v_transmitted_paused))
          v_transmitted_paused <= v_transmitted_paused + 1'b1;

      // A PAUSE THAT LEFT THIS DEVICE. Chapter 12.4's flooding must never
      // touch the reserved address -- forwarding one tells a third party
      // to stop sending to somebody it was not sending to.
      if (pause_forwarded && (rx_pause_da == PAUSE_DA))
        if (!(&v_pause_forwarded))
          v_pause_forwarded <= v_pause_forwarded + 1'b1;

      // The watermark was set without enough room for the dead time.
      if (pause_tx && !headroom_feasible)
        if (!(&v_headroom_short)) v_headroom_short <= v_headroom_short + 1'b1;

      // Our own control frames were blocked by a pause. Section 11's
      // rule 2 -- without it, congestion cannot propagate at all.
      if (we_were_paused && tx_was_control && !we_transmitted)
        if (!(&v_control_blocked))
          v_control_blocked <= v_control_blocked + 1'b1;
    end
  end

  assign conformant = (v_late_arrival       == '0) &&
                      (v_transmitted_paused == '0) &&
                      (v_pause_forwarded    == '0) &&
                      (v_headroom_short     == '0) &&
                      (v_control_blocked    == '0) &&
                      headroom_feasible;

endmodule

// P1. A PAUSE is addressed to the reserved multicast, always.
property p_pause_da_is_reserved;
  @(posedge clk) disable iff (!rst_n)
  frame_valid |-> (frame_head[511 -: 48] == PAUSE_DA);
endproperty
a_pause_da: assert property (p_pause_da_is_reserved);

// P2. It carries the MAC Control EtherType and the PAUSE opcode.
property p_pause_type_and_opcode;
  @(posedge clk) disable iff (!rst_n)
  frame_valid |-> ((frame_head[415 -: 16] == MAC_CTRL) &&
                   (frame_head[399 -: 16] == OP_PAUSE));
endproperty
a_pause_fields: assert property (p_pause_type_and_opcode);

// P3. It is exactly 64 octets -- Chapter 5.6's minimum, reached with 42
// octets of padding around an 18-octet payload.
property p_pause_is_minimum_length;
  @(posedge clk) disable iff (!rst_n)
  frame_valid |-> (frame_len == 14'd64);
endproperty
a_pause_length: assert property (p_pause_is_minimum_length);

// P4. pause_time = 0 is a RELEASE, not a zero-length pause. Without this
// a pause cannot be cancelled.
property p_zero_is_release;
  @(posedge clk) disable iff (!rst_n)
  (frame_valid && (frame_head[383 -: 16] == 16'd0)) |-> is_release;
endproperty
a_zero_releases: assert property (p_zero_is_release);

// P5. A PAUSE is CONSUMED, never forwarded -- even by a port that does
// not honour it. Chapter 12.4's flooding must not touch this address.
property p_pause_never_forwarded;
  @(posedge clk) disable iff (!rst_n)
  (rx_valid && (rx_da == PAUSE_DA)) |-> consume;
endproperty
a_never_forwarded: assert property (p_pause_never_forwarded);

// P6. The DESTINATION is checked, not only the EtherType and opcode. A
// PAUSE addressed elsewhere is not a PAUSE for this device.
property p_destination_checked;
  @(posedge clk) disable iff (!rst_n)
  (rx_valid && (rx_da != PAUSE_DA)) |-> !pause_valid;
endproperty
a_da_checked: assert property (p_destination_checked);

// P7. Assert at HIGH, not at full. The space above HIGH is Section 5's
// headroom and it must cover the dead time.
property p_assert_at_high;
  @(posedge clk) disable iff (!rst_n)
  (send_pause && (send_quanta != 16'd0) && !paused_state)
    |-> (occupancy_cells >= 16'(HIGH_CELLS));
endproperty
a_assert_high: assert property (p_assert_at_high);

// P8. Release at LOW, not at HIGH. Without hysteresis the trigger
// oscillates once per frame.
property p_release_at_low;
  @(posedge clk) disable iff (!rst_n)
  (send_pause && (send_quanta == 16'd0))
    |-> (occupancy_cells <= 16'(LOW_CELLS));
endproperty
a_release_low: assert property (p_release_at_low);

// P9. HIGH is above LOW. The hysteresis exists.
property p_hysteresis_exists;
  @(posedge clk) disable iff (!rst_n)
  (HIGH_CELLS > LOW_CELLS);
endproperty
a_hysteresis: assert property (p_hysteresis_exists);

// P10. A pause is RE-ISSUED before it expires while the queue is still
// above LOW -- Section 2's ceiling means a pause is finite and a
// congestion event may not be.
property p_reissue_before_expiry;
  @(posedge clk) disable iff (!rst_n)
  (paused_state && (remaining <= 16'(PAUSE_QUANTA - REISSUE_AT)) &&
   (occupancy_cells > 16'(LOW_CELLS)))
    |-> send_pause;
endproperty
a_reissue: assert property (p_reissue_before_expiry);

// P11. A lapsed pause with the queue still above LOW is COUNTED -- it is
// the failure the re-issue exists to prevent.
property p_lapse_counted;
  @(posedge clk) disable iff (!rst_n)
  (quantum_tick && (remaining == 16'd1) && (occupancy_cells > 16'(LOW_CELLS)))
    |=> (c_late_reissue > $past(c_late_reissue));
endproperty
a_lapse_counted: assert property (p_lapse_counted);

// P12. THE DEAD TIME is the sum of its three parts plus our own transmit
// backlog -- and a design that omits the backlog under-reserves by
// exactly the amount its own transmitter is busy.
property p_dead_time_complete;
  @(posedge clk) disable iff (!rst_n)
  (dead_time_ns == (20'(PAUSE_TX_NS) + 20'(PROP_NS) + 20'(FINISH_NS) +
                    backlog_ns));
endproperty
a_dead_time: assert property (p_dead_time_complete);

// P13. The headroom is the dead time's arrivals at line rate.
property p_headroom_from_dead_time;
  @(posedge clk) disable iff (!rst_n)
  (headroom_octets == ((dead_time_ns * 20'(LINK_MBPS)) / 20'd8000));
endproperty
a_headroom: assert property (p_headroom_from_dead_time);

// P14. The watermark is queue MINUS headroom, not a fraction of the
// queue. A fraction is a guess about a duration.
property p_watermark_is_derived;
  @(posedge clk) disable iff (!rst_n)
  (high_watermark_cells == (16'(QUEUE_CELLS) - headroom_cells));
endproperty
a_watermark_derived: assert property (p_watermark_is_derived);

// P15. A link whose headroom exceeds its queue is flagged INFEASIBLE --
// there is no watermark at which a pause arrives in time.
property p_infeasible_flagged;
  @(posedge clk) disable iff (!rst_n)
  (headroom_cells >= 16'(QUEUE_CELLS)) |-> watermark_infeasible;
endproperty
a_infeasible: assert property (p_infeasible_flagged);

// P16. Propagation's share of the dead time is reported, because it is
// the component that grows with line rate and cannot be reduced.
property p_prop_share_computed;
  @(posedge clk) disable iff (!rst_n)
  (prop_share_pct <= 16'd100);
endproperty
a_prop_share: assert property (p_prop_share_computed);

// P17. A new pause REPLACES the outstanding one; it does not accumulate.
// Otherwise a bounded stream of requests builds an unbounded pause.
property p_pause_replaces_not_adds;
  @(posedge clk) disable iff (!rst_n)
  (pause_valid && (quanta != 16'd0)) |=> (remaining == $past(quanta));
endproperty
a_replaces: assert property (p_pause_replaces_not_adds);

// P18. A release ends the pause immediately.
property p_release_ends_pause;
  @(posedge clk) disable iff (!rst_n)
  (pause_valid && (quanta == 16'd0)) |=> (remaining == 16'd0);
endproperty
a_release_now: assert property (p_release_ends_pause);

// P19. The counter decrements once per quantum and never below zero.
property p_timer_decrements;
  @(posedge clk) disable iff (!rst_n)
  (quantum_tick && (remaining != 16'd0) && !pause_valid)
    |=> (remaining == $past(remaining) - 16'd1);
endproperty
a_timer: assert property (p_timer_decrements);

// P20. A frame in progress is FINISHED. Ethernet has no abort, and
// Chapter 12.6 Section 8 established a truncated frame is discarded.
property p_frame_in_progress_completes;
  @(posedge clk) disable iff (!rst_n)
  (paused && frame_in_progress) |-> tx_permit;
endproperty
a_finish_frame: assert property (p_frame_in_progress_completes);

// P21. CONTROL FRAMES BYPASS THE PAUSE. Without this a paused switch
// cannot pause ITS neighbour and congestion cannot propagate at all.
property p_control_bypasses;
  @(posedge clk) disable iff (!rst_n)
  (paused && frame_is_control) |-> (tx_permit && control_bypass);
endproperty
a_control_bypass: assert property (p_control_bypasses);

// P22. Ordinary traffic does NOT bypass.
property p_ordinary_blocked;
  @(posedge clk) disable iff (!rst_n)
  (paused && frame_pending && !frame_is_control && !frame_in_progress)
    |-> !tx_permit;
endproperty
a_ordinary_stops: assert property (p_ordinary_blocked);

// P23. THE NUMBER NOBODY COMPUTES. A link paused a fraction of the time
// is delivering that much less than its rate.
property p_effective_rate_reported;
  @(posedge clk) disable iff (!rst_n)
  window_valid |-> (effective_rate_pct ==
                    16'(100 - (paused_pct_x100 / 16'd100)));
endproperty
a_effective_rate: assert property (p_effective_rate_reported);

// P24. Paused and still dropping is reported -- either the headroom is
// wrong or the congestion exceeds what pausing one neighbour can fix.
property p_ineffective_reported;
  @(posedge clk) disable iff (!rst_n)
  (window_valid && pause_ineffective) |-> (c_sent != '0);
endproperty
a_ineffective: assert property (p_ineffective_reported);

// P25. The PAUSE frames' own bandwidth is accounted -- 672 bits each,
// on the link they are relieving.
property p_overhead_accounted;
  @(posedge clk) disable iff (!rst_n)
  (window_valid && (c_sent != '0)) |-> (pause_overhead_ppm != 16'd0);
endproperty
a_overhead: assert property (p_overhead_accounted);

// P26. THE CORRECT ARRIVAL CHECK. Frames after the DEAD TIME are the
// neighbour ignoring us; frames during it are physics.
property p_no_arrivals_after_dead_time;
  @(posedge clk) disable iff (!rst_n)
  (rx_frame && !rx_is_control && (tx_quanta != 16'd0) &&
   (ns_since_pause > dead_time_ns))
    |-> v_late_arrival_will_increment;
endproperty
a_late_arrival: assert property (p_no_arrivals_after_dead_time);

// P27. A PAUSE never leaves this device.
property p_pause_not_relayed;
  @(posedge clk) disable iff (!rst_n)
  (rx_pause_da == PAUSE_DA) |-> !pause_forwarded;
endproperty
a_not_relayed: assert property (p_pause_not_relayed);

// P28. Conformance INCLUDES headroom_feasible -- a standing property of
// the link, not a history of events.
property p_conformant_includes_feasible;
  @(posedge clk) disable iff (!rst_n)
  conformant |-> headroom_feasible;
endproperty
a_conformant_feasible: assert property (p_conformant_includes_feasible);

// P29. Conformance means the mechanism behaved as specified -- never
// that no frame was lost.
property p_conformant_definition;
  @(posedge clk) disable iff (!rst_n)
  conformant |-> ((v_late_arrival == '0) && (v_transmitted_paused == '0) &&
                  (v_pause_forwarded == '0) && (v_headroom_short == '0) &&
                  (v_control_blocked == '0));
endproperty
a_conformant_def: assert property (p_conformant_definition);

// P30. PAUSE capability is per DIRECTION. A device may pause and not be
// pausable, or the reverse, and the two are negotiated independently.
property p_direction_independent;
  @(posedge clk) disable iff (!rst_n)
  (pause_tx_enabled != pause_rx_enabled) |-> asymmetric_pause_configured;
endproperty
a_per_direction: assert property (p_direction_independent);