Where Frames Are Lost

// -----------------------------------------------------------------------
// congest_pkg -- shared types for congestion and flow control.
// -----------------------------------------------------------------------
package congest_pkg;

  // Why an enqueue failed. The distinction between the first two is this
  // chapter's subject: one is this port's problem and one is somebody
  // else's, and a single "drop" counter merges them.
  typedef enum logic [2:0] {
    EF_OK          = 3'd0,
    EF_QUEUE_LIMIT = 3'd1,  // this port has reached its own limit
    EF_POOL_EMPTY  = 3'd2,  // the SHARED pool is exhausted -- Section 8
    EF_NO_RESERVE  = 3'd3,  // below reserve and the reserve is spent
    EF_PORT_DOWN   = 3'd4
  } enq_fail_e;

  // Where a buffer's occupancy sits relative to its thresholds. Chapter
  // 14.2's PAUSE and Chapter 14.4's per-priority pause both trigger on
  // these rather than on "full".
  typedef enum logic [1:0] {
    WM_EMPTY = 2'd0,
    WM_LOW   = 2'd1,   // below the resume threshold
    WM_HIGH  = 2'd2,   // above the assert threshold
    WM_FULL  = 2'd3
  } watermark_e;

  localparam int CELL_OCTETS = 128;   // allocation granularity

endpackage

// -----------------------------------------------------------------------
// egress_queue_model -- one port's queue, its watermarks, and the rate at
// which it fills.
//
// Chapter 12.1 Section 9 built the tail-drop policy on this queue. What
// that chapter treated as a fixed depth is, on a shared-buffer switch, a
// claim against a pool -- which is Section 5's subject and the reason
// this module reports its occupancy in CELLS rather than octets.
// -----------------------------------------------------------------------
module egress_queue_model
  import congest_pkg::*;
#(
  parameter int MAX_CELLS  = 4096,      // this port's limit, not its memory
  parameter int HIGH_CELLS = 3072,
  parameter int LOW_CELLS  = 1024,
  parameter int CNT_W      = 32
)(
  input  logic                 clk,
  input  logic                 rst_n,

  input  logic                 enq_valid,
  input  logic [7:0]           enq_cells,       // frame size in cells
  input  logic                 pool_granted,    // Section 5 said yes
  input  logic                 deq_valid,
  input  logic [7:0]           deq_cells,

  output logic                 enq_accept,
  output enq_fail_e            enq_fail,

  output logic [15:0]          occupancy_cells,
  output logic [15:0]          peak_cells,
  output watermark_e           watermark,
  output logic                 above_high,
  output logic                 below_low,

  output logic [CNT_W-1:0]     c_enq,
  output logic [CNT_W-1:0]     c_drop_limit,
  output logic [CNT_W-1:0]     c_drop_pool,
  output logic [CNT_W-1:0]     c_cells_dropped
);

  always_comb begin
    enq_accept = 1'b0;
    enq_fail   = EF_OK;

    if (enq_valid) begin
      // THE TWO REFUSALS, KEPT APART. Reaching this port's own limit is
      // this port's congestion. Failing to get a cell from the pool is
      // somebody else's congestion arriving here -- Section 10.
      if ((occupancy_cells + 16'(enq_cells)) > 16'(MAX_CELLS))
        enq_fail = EF_QUEUE_LIMIT;
      else if (!pool_granted)
        enq_fail = EF_POOL_EMPTY;
      else
        enq_accept = 1'b1;
    end
  end

  always_comb begin
    if      (occupancy_cells == 16'd0)             watermark = WM_EMPTY;
    else if (occupancy_cells >= 16'(MAX_CELLS))    watermark = WM_FULL;
    else if (occupancy_cells >= 16'(HIGH_CELLS))   watermark = WM_HIGH;
    else if (occupancy_cells <= 16'(LOW_CELLS))    watermark = WM_LOW;
    else                                            watermark = WM_LOW;
  end

  // Chapter 14.2's PAUSE and Chapter 14.4's per-priority pause both
  // trigger on the HIGH watermark and release on the LOW one, never on
  // "full" -- by the time a queue is full the frames that would have
  // been paused have already arrived.
  assign above_high = (occupancy_cells >= 16'(HIGH_CELLS));
  assign below_low  = (occupancy_cells <= 16'(LOW_CELLS));

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      occupancy_cells <= '0;
      peak_cells      <= '0;
      c_enq           <= '0;
      c_drop_limit    <= '0;
      c_drop_pool     <= '0;
      c_cells_dropped <= '0;
    end else begin
      if (enq_valid && enq_accept) begin
        occupancy_cells <= occupancy_cells + 16'(enq_cells);
        c_enq           <= c_enq + 1'b1;
        if ((occupancy_cells + 16'(enq_cells)) > peak_cells)
          peak_cells <= occupancy_cells + 16'(enq_cells);
      end else if (enq_valid) begin
        c_cells_dropped <= c_cells_dropped + CNT_W'(enq_cells);
        if (enq_fail == EF_QUEUE_LIMIT) begin
          if (!(&c_drop_limit)) c_drop_limit <= c_drop_limit + 1'b1;
        end else if (enq_fail == EF_POOL_EMPTY) begin
          if (!(&c_drop_pool)) c_drop_pool <= c_drop_pool + 1'b1;
        end
      end

      if (deq_valid) occupancy_cells <= occupancy_cells - 16'(deq_cells);
    end
  end

endmodule

// -----------------------------------------------------------------------
// buffer_pool_manager -- one memory, many ports, three regions.
//
// The three regions are the whole design. A per-port RESERVE that only
// that port may use; a SHARED region any port may draw from; and a
// per-port LIMIT on how much of the shared region one port may hold. The
// sum of the reserves plus the shared region is the pool; the sum of the
// LIMITS deliberately exceeds it -- Section 18's rejected property.
// -----------------------------------------------------------------------
module buffer_pool_manager
  import congest_pkg::*;
#(
  parameter int N_PORTS      = 24,
  parameter int POOL_CELLS   = 98304,   // 12 MiB at 128 octets per cell
  parameter int RESERVE_CELLS = 512,    // per port, guaranteed
  parameter int LIMIT_CELLS  = 24576,   // per port, of the SHARED region
  parameter int CNT_W        = 32
)(
  input  logic                 clk,
  input  logic                 rst_n,

  input  logic                 req_valid,
  input  logic [4:0]           req_port,
  input  logic [7:0]           req_cells,

  input  logic                 rel_valid,
  input  logic [4:0]           rel_port,
  input  logic [7:0]           rel_cells,

  output logic                 grant,
  output enq_fail_e            fail,

  output logic [17:0]          pool_free,
  output logic [17:0]          shared_free,
  output logic [17:0]          held [N_PORTS],
  output logic [4:0]           largest_holder,
  output logic [15:0]          largest_share_pct,
  output logic                 pool_exhausted,

  output logic [CNT_W-1:0]     c_grant,
  output logic [CNT_W-1:0]     c_refuse_limit,
  output logic [CNT_W-1:0]     c_refuse_pool,
  output logic [CNT_W-1:0]     overcommit_ratio_x100
);

  localparam int RESERVED_TOTAL = N_PORTS * RESERVE_CELLS;
  localparam int SHARED_TOTAL   = POOL_CELLS - RESERVED_TOTAL;

  logic [17:0] shared_used;

  // A port's reserve is spent first and belongs to nobody else. Only what
  // it holds ABOVE the reserve comes from the shared region.
  function automatic logic [17:0] shared_held(input logic [17:0] h);
    shared_held = (h > 18'(RESERVE_CELLS)) ? (h - 18'(RESERVE_CELLS)) : 18'd0;
  endfunction

  always_comb begin
    automatic logic [17:0] h  = held[req_port];
    automatic logic [17:0] sh = shared_held(h);
    grant = 1'b0;
    fail  = EF_OK;

    if (req_valid) begin
      if ((h + 18'(req_cells)) <= 18'(RESERVE_CELLS)) begin
        // WITHIN THE RESERVE. Always granted -- this is the guarantee
        // that makes the shared region safe to over-commit.
        grant = 1'b1;
      end else if ((sh + 18'(req_cells)) > 18'(LIMIT_CELLS)) begin
        // This port has taken as much of the shared region as it is
        // allowed. Its congestion is now its own problem, which is the
        // entire purpose of the limit.
        fail = EF_QUEUE_LIMIT;
      end else if ((shared_used + 18'(req_cells)) > 18'(SHARED_TOTAL)) begin
        // THE SHARED REGION IS GONE. Somebody else took it -- Section 8.
        fail = EF_POOL_EMPTY;
      end else begin
        grant = 1'b1;
      end
    end
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (int p = 0; p < N_PORTS; p++) held[p] <= '0;
      shared_used           <= '0;
      c_grant               <= '0;
      c_refuse_limit        <= '0;
      c_refuse_pool         <= '0;
      largest_holder        <= '0;
      largest_share_pct     <= '0;
      pool_exhausted        <= 1'b0;
    end else begin
      if (req_valid && grant) begin
        held[req_port] <= held[req_port] + 18'(req_cells);
        if (held[req_port] >= 18'(RESERVE_CELLS))
          shared_used <= shared_used + 18'(req_cells);
        c_grant <= c_grant + 1'b1;
      end else if (req_valid) begin
        if (fail == EF_QUEUE_LIMIT) begin
          if (!(&c_refuse_limit)) c_refuse_limit <= c_refuse_limit + 1'b1;
        end else begin
          if (!(&c_refuse_pool)) c_refuse_pool <= c_refuse_pool + 1'b1;
        end
      end

      if (rel_valid) begin
        held[rel_port] <= held[rel_port] - 18'(rel_cells);
        if (held[rel_port] > 18'(RESERVE_CELLS))
          shared_used <= shared_used - 18'(rel_cells);
      end

      // WHO IS HOLDING THE POOL. This is the number that turns a drop on
      // port 3 into a finding about port 7 -- Section 10.
      begin
        automatic logic [17:0] hi = '0;
        automatic logic [4:0]  hp = '0;
        for (int p = 0; p < N_PORTS; p++)
          if (held[p] > hi) begin hi = held[p]; hp = 5'(p); end
        largest_holder    <= hp;
        largest_share_pct <= 16'((hi * 18'd100) / 18'(POOL_CELLS));
      end

      pool_exhausted <= (shared_used >= 18'(SHARED_TOTAL));
    end
  end

  assign shared_free = 18'(SHARED_TOTAL) - shared_used;
  assign pool_free   = shared_free;

  // THE OVER-COMMITMENT, COMPUTED. The sum of what every port is allowed
  // to take, against what exists. A value above 100 is the design working
  // as intended -- Section 18.
  assign overcommit_ratio_x100 =
    CNT_W'((((N_PORTS * (RESERVE_CELLS + LIMIT_CELLS)) * 100) / POOL_CELLS));

endmodule

// -----------------------------------------------------------------------
// shared_pool_accountant -- attributes pool exhaustion to the port that
// caused it, which is not the port that suffered it.
//
// Chapter 12.1 Section 11 made the same argument one level down: c_drops
// says an egress port is oversubscribed, and drops_by_ingress says which
// conversation is doing it. This is that argument applied to the pool.
// -----------------------------------------------------------------------
module shared_pool_accountant
  import congest_pkg::*;
#(
  parameter int N_PORTS = 24,
  parameter int CNT_W   = 32,
  parameter int WIN     = 1_000_000
)(
  input  logic             clk,
  input  logic             rst_n,

  input  logic [17:0]      held [N_PORTS],
  input  logic [17:0]      shared_total,
  input  logic             pool_exhausted,

  input  logic             drop_valid,
  input  logic [4:0]       drop_port,
  input  enq_fail_e        drop_reason,

  output logic [CNT_W-1:0] drops_suffered [N_PORTS],
  output logic [CNT_W-1:0] pool_drops_caused [N_PORTS],
  output logic [4:0]       victim_port,
  output logic [4:0]       culprit_port,
  output logic             victim_is_not_culprit,
  output logic [15:0]      culprit_share_pct,
  output logic             window_valid
);

  logic [CNT_W-1:0] win;

  // WHO HELD THE POOL AT THE MOMENT OF THE DROP. Sampling this at the
  // drop rather than periodically is what makes the attribution sound --
  // a periodic sample tells you who is usually busy, not who was holding
  // the memory the instant a frame was refused.
  logic [4:0]  hi_port;
  logic [17:0] hi_held;

  always_comb begin
    hi_port = 5'd0;
    hi_held = 18'd0;
    for (int p = 0; p < N_PORTS; p++)
      if (held[p] > hi_held) begin hi_held = held[p]; hi_port = 5'(p); end
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (int p = 0; p < N_PORTS; p++) begin
        drops_suffered[p]    <= '0;
        pool_drops_caused[p] <= '0;
      end
      win                   <= '0;
      victim_port           <= '0;
      culprit_port          <= '0;
      victim_is_not_culprit <= 1'b0;
      culprit_share_pct     <= '0;
      window_valid          <= 1'b0;
    end else begin
      window_valid <= 1'b0;

      if (drop_valid) begin
        drops_suffered[drop_port] <= drops_suffered[drop_port] + 1'b1;
        win <= win + 1'b1;

        // THE ATTRIBUTION. A drop caused by an exhausted POOL is charged
        // to whoever is holding it, not to the port that could not
        // allocate. A drop caused by this port's own LIMIT is charged
        // here, because that is this port's congestion.
        if (drop_reason == EF_POOL_EMPTY) begin
          pool_drops_caused[hi_port] <= pool_drops_caused[hi_port] + 1'b1;
          victim_port                <= drop_port;
          culprit_port               <= hi_port;
          victim_is_not_culprit      <= (drop_port != hi_port);
          culprit_share_pct          <= 16'((hi_held * 18'd100) / shared_total);
        end
      end

      if (win >= CNT_W'(WIN)) begin
        win          <= '0;
        window_valid <= 1'b1;
      end
    end
  end

endmodule

// -----------------------------------------------------------------------
// drop_attribution -- every discard, classified and attributed.
//
// Chapter 12.3 Section 10's deciding_gate did this for the forwarding
// decision. This does it for the buffer, and the reasons are unrelated
// to each other in exactly the same way.
// -----------------------------------------------------------------------
module drop_attribution
  import congest_pkg::*;
#(
  parameter int N_PORTS = 24,
  parameter int CNT_W   = 32,
  parameter int WIN     = 1_000_000
)(
  input  logic             clk,
  input  logic             rst_n,

  input  logic             drop_valid,
  input  enq_fail_e        reason,
  input  logic [4:0]       egress_port,
  input  logic [4:0]       ingress_port,
  input  logic [4:0]       pool_holder,

  output logic [CNT_W-1:0] c_by_reason [5],
  output logic [CNT_W-1:0] c_by_egress [N_PORTS],
  output logic [CNT_W-1:0] c_by_ingress [N_PORTS],

  output logic             window_valid,
  output logic [15:0]      pool_drop_share_pct,
  output logic             mostly_somebody_else,
  output logic [4:0]       dominant_ingress,
  output logic [4:0]       dominant_holder
);

  logic [CNT_W-1:0] win, win_pool;
  logic [CNT_W-1:0] holder_hits [N_PORTS];

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (int i = 0; i < 5; i++) c_by_reason[i] <= '0;
      for (int p = 0; p < N_PORTS; p++) begin
        c_by_egress[p] <= '0; c_by_ingress[p] <= '0; holder_hits[p] <= '0;
      end
      win <= '0; win_pool <= '0;
      window_valid        <= 1'b0;
      pool_drop_share_pct <= '0;
      mostly_somebody_else<= 1'b0;
      dominant_ingress    <= '0;
      dominant_holder     <= '0;
    end else begin
      window_valid <= 1'b0;

      if (drop_valid) begin
        c_by_reason[reason[2:0]] <= c_by_reason[reason[2:0]] + 1'b1;
        // THREE ATTRIBUTIONS PER DROP, and they answer three questions.
        // Egress: where did it fail. Ingress: whose traffic was it.
        // Holder: whose memory was it waiting for.
        c_by_egress[egress_port]   <= c_by_egress[egress_port] + 1'b1;
        c_by_ingress[ingress_port] <= c_by_ingress[ingress_port] + 1'b1;
        win <= win + 1'b1;

        if (reason == EF_POOL_EMPTY) begin
          win_pool               <= win_pool + 1'b1;
          holder_hits[pool_holder] <= holder_hits[pool_holder] + 1'b1;
        end
      end

      if (win >= CNT_W'(WIN)) begin
        automatic logic [CNT_W-1:0] hi = '0;
        automatic logic [4:0] hp = '0;
        automatic logic [CNT_W-1:0] hi2 = '0;
        automatic logic [4:0] hp2 = '0;
        for (int p = 0; p < N_PORTS; p++) begin
          if (holder_hits[p] > hi)      begin hi = holder_hits[p];  hp = 5'(p); end
          if (c_by_ingress[p] > hi2)    begin hi2 = c_by_ingress[p]; hp2 = 5'(p); end
        end
        pool_drop_share_pct <= 16'((win_pool * CNT_W'(100)) / win);
        // MORE THAN HALF OF THIS PORT'S DROPS WERE SOMEBODY ELSE'S FAULT.
        // The single most useful bit in the module.
        mostly_somebody_else <= (win_pool > (win >> 1));
        dominant_holder      <= hp;
        dominant_ingress     <= hp2;
        win <= '0; win_pool <= '0;
        for (int p = 0; p < N_PORTS; p++) holder_hits[p] <= '0;
        window_valid <= 1'b1;
      end
    end
  end

endmodule

// -----------------------------------------------------------------------
// queue_delay_estimator -- occupancy to latency, in hardware.
//
// L = lambda * W, so W = L / lambda: the wait a frame joining the queue
// now will experience is the current occupancy divided by the drain rate.
// It is exact for a work-conserving server and it is the number an
// application cares about, which occupancy is not.
// -----------------------------------------------------------------------
module queue_delay_estimator
  import congest_pkg::*;
#(
  parameter int LINK_MBPS = 1000,
  parameter int CNT_W     = 32
)(
  input  logic             clk,
  input  logic             rst_n,

  input  logic [15:0]      occupancy_cells,
  input  logic             sample,

  output logic [19:0]      delay_ns,
  output logic [19:0]      peak_delay_ns,
  output logic [19:0]      p99_delay_ns,       // coarse, from a histogram
  output logic             delay_over_1ms,
  output logic [CNT_W-1:0] hist [8]            // log2 buckets of delay
);

  // Cells to bits, bits to nanoseconds. At 128 octets per cell and
  // 1000 Mb/s: one cell is 1024 bits and drains in 1024 ns.
  localparam int NS_PER_CELL = (CELL_OCTETS * 8 * 1000) / LINK_MBPS;

  assign delay_ns = 20'(occupancy_cells) * 20'(NS_PER_CELL);

  // A log2 histogram rather than a mean. Chapter 12.6 Section 6
  // established that jitter is what real-time traffic is engineered
  // against, and a mean delay hides the tail entirely.
  function automatic logic [2:0] bucket(input logic [19:0] d);
    if      (d < 20'd1000)    bucket = 3'd0;   // < 1 us
    else if (d < 20'd4000)    bucket = 3'd1;
    else if (d < 20'd16000)   bucket = 3'd2;
    else if (d < 20'd64000)   bucket = 3'd3;
    else if (d < 20'd256000)  bucket = 3'd4;   // < 256 us
    else if (d < 20'd512000)  bucket = 3'd5;
    else if (d < 20'd1000000) bucket = 3'd6;   // < 1 ms
    else                      bucket = 3'd7;   // >= 1 ms
  endfunction

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (int i = 0; i < 8; i++) hist[i] <= '0;
      peak_delay_ns  <= '0;
      p99_delay_ns   <= '0;
      delay_over_1ms <= 1'b0;
    end else if (sample) begin
      hist[bucket(delay_ns)] <= hist[bucket(delay_ns)] + 1'b1;
      if (delay_ns > peak_delay_ns) peak_delay_ns <= delay_ns;
      delay_over_1ms <= (delay_ns >= 20'd1000000);

      // A coarse 99th percentile: the lowest bucket boundary above which
      // fewer than one percent of samples fall. Computed by walking the
      // histogram from the top, which is a handful of comparisons.
      begin
        automatic logic [CNT_W-1:0] tot = '0;
        automatic logic [CNT_W-1:0] acc = '0;
        for (int i = 0; i < 8; i++) tot = tot + hist[i];
        for (int i = 7; i >= 0; i--) begin
          acc = acc + hist[i];
          if (acc > (tot / 100)) begin
            p99_delay_ns <= 20'd1000 << (3 * i);
            break;
          end
        end
      end
    end
  end

endmodule

// -----------------------------------------------------------------------
// burst_absorption_model -- how long this buffer holds out.
//
// A buffer absorbs a RATE MISMATCH for a DURATION. Quoting its size in
// bytes hides both variables; quoting the duration it buys at a stated
// oversubscription ratio states them.
// -----------------------------------------------------------------------
module burst_absorption_model
  import congest_pkg::*;
#(
  parameter int LINK_MBPS = 1000,
  parameter int CNT_W     = 32
)(
  input  logic             clk,
  input  logic             rst_n,

  input  logic [15:0]      free_cells,
  input  logic [5:0]       oversub_ratio,   // N:1, so excess = (N-1) x link
  input  logic             sample,

  output logic [19:0]      absorb_us,
  output logic [19:0]      worst_absorb_us,
  output logic             under_100us,
  output logic             under_10us,

  input  logic             fill_started,
  input  logic             fill_ended,
  output logic [19:0]      last_burst_us,
  output logic [19:0]      longest_burst_us,
  output logic [CNT_W-1:0] c_bursts,
  output logic             buffer_was_adequate
);

  // Excess rate = (ratio - 1) x link. Time = bits / excess.
  // At 128 octets per cell and 1000 Mb/s, one cell is 1024 bits and
  // drains in 1.024 us at the link rate.
  localparam int NS_PER_CELL = (CELL_OCTETS * 8 * 1000) / LINK_MBPS;

  always_comb begin
    if (oversub_ratio <= 6'd1) absorb_us = 20'hFFFFF;   // no excess
    else absorb_us = (20'(free_cells) * 20'(NS_PER_CELL)) /
                     (20'(oversub_ratio) - 20'd1) / 20'd1000;
  end

  assign under_100us = (absorb_us < 20'd100);
  assign under_10us  = (absorb_us < 20'd10);

  logic [19:0] burst_ns;
  logic        in_burst;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      worst_absorb_us     <= 20'hFFFFF;
      burst_ns            <= '0;
      in_burst            <= 1'b0;
      last_burst_us       <= '0;
      longest_burst_us    <= '0;
      c_bursts            <= '0;
      buffer_was_adequate <= 1'b1;
    end else begin
      if (sample && (absorb_us < worst_absorb_us))
        worst_absorb_us <= absorb_us;

      // MEASURE THE BURSTS THAT ACTUALLY ARRIVE, not the ones the buffer
      // was sized for. A buffer sized for 1 ms on a network whose bursts
      // are 20 us is oversized by 50x, and nothing else says so.
      if (fill_started && !in_burst) begin
        in_burst <= 1'b1;
        burst_ns <= '0;
      end else if (in_burst) begin
        burst_ns <= burst_ns + 20'd8;      // 8 ns per cycle at 125 MHz
        if (fill_ended) begin
          in_burst      <= 1'b0;
          last_burst_us <= burst_ns / 20'd1000;
          if ((burst_ns / 20'd1000) > longest_burst_us)
            longest_burst_us <= burst_ns / 20'd1000;
          if (!(&c_bursts)) c_bursts <= c_bursts + 1'b1;
        end
      end

      // The buffer was adequate if it absorbed every burst that arrived.
      buffer_was_adequate <= (longest_burst_us < worst_absorb_us);
    end
  end

endmodule

// -----------------------------------------------------------------------
// congestion_telemetry -- the per-window state of the buffer subsystem.
//
// Every quantity is derived from signals the datapath already has. The
// value is that a single "discards" figure conflates six unrelated
// conditions, and each of the six has a different remedy.
// -----------------------------------------------------------------------
module congestion_telemetry
  import congest_pkg::*;
#(
  parameter int N_PORTS = 24,
  parameter int CNT_W   = 32,
  parameter int WIN     = 1_000_000
)(
  input  logic             clk,
  input  logic             rst_n,

  input  logic             frame_valid,
  input  logic             drop_valid,
  input  enq_fail_e        drop_reason,
  input  logic [17:0]      shared_free,
  input  logic [17:0]      shared_total,
  input  logic [15:0]      largest_share_pct,
  input  logic [19:0]      p99_delay_ns,
  input  logic [19:0]      worst_absorb_us,
  input  logic             pool_exhausted,

  output logic             window_valid,
  output logic [15:0]      drop_rate_ppm,
  output logic [15:0]      pool_free_pct,
  output logic [15:0]      pool_exhausted_ppm,
  output logic             congested,
  output logic             one_port_dominant,
  output logic             delay_bound_exceeded,
  output logic             headroom_critical,
  output logic [CNT_W-1:0] c_frames,
  output logic [CNT_W-1:0] c_drops
);

  logic [CNT_W-1:0] win, win_drop, win_exh;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      win <= '0; win_drop <= '0; win_exh <= '0;
      c_frames <= '0; c_drops <= '0;
      window_valid         <= 1'b0;
      drop_rate_ppm        <= '0;
      pool_free_pct        <= 16'd100;
      pool_exhausted_ppm   <= '0;
      congested            <= 1'b0;
      one_port_dominant    <= 1'b0;
      delay_bound_exceeded <= 1'b0;
      headroom_critical    <= 1'b0;
    end else begin
      window_valid <= 1'b0;

      if (frame_valid) begin win <= win + 1'b1; c_frames <= c_frames + 1'b1; end
      if (drop_valid)  begin win_drop <= win_drop + 1'b1; c_drops <= c_drops + 1'b1; end
      if (pool_exhausted) win_exh <= win_exh + 1'b1;

      if (win >= CNT_W'(WIN)) begin
        // PARTS PER MILLION, not percent. A drop rate of 0.05% is 500 ppm
        // and matters; as an integer percentage it is zero.
        drop_rate_ppm      <= 16'((win_drop * CNT_W'(1_000_000)) / win);
        pool_exhausted_ppm <= 16'((win_exh  * CNT_W'(1_000_000)) / win);
        pool_free_pct      <= 16'((18'(shared_free) * 18'd100) / shared_total);

        congested            <= (win_drop != '0) || (win_exh != '0);
        // ONE PORT HOLDING MORE THAN HALF THE POOL. Section 8's condition,
        // as a bit.
        one_port_dominant    <= (largest_share_pct > 16'd50);
        // A millisecond of queueing -- Section 12 puts this at about 99%
        // utilisation, which a five-minute average reports as 70%.
        delay_bound_exceeded <= (p99_delay_ns >= 20'd1000000);
        // Less than ten microseconds of absorption left: roughly one
        // maximum-length frame at 1 Gb/s.
        headroom_critical    <= (worst_absorb_us < 20'd10);

        win <= '0; win_drop <= '0; win_exh <= '0;
        window_valid <= 1'b1;
      end
    end
  end

endmodule

// -----------------------------------------------------------------------
// congestion_conformance_monitor -- checks a buffer subsystem whose
// design premise is that it promises more than it has.
//
// The invariant is NOT that allocations sum to the pool. It is that the
// RESERVES do, that no port exceeds its limit, that accounting balances,
// and that every drop is attributed. Section 18 is about the difference.
// -----------------------------------------------------------------------
module congestion_conformance_monitor
  import congest_pkg::*;
#(
  parameter int N_PORTS       = 24,
  parameter int POOL_CELLS    = 98304,
  parameter int RESERVE_CELLS = 512,
  parameter int LIMIT_CELLS   = 24576,
  parameter int CNT_W         = 32
)(
  input  logic             clk,
  input  logic             rst_n,

  input  logic [17:0]      held [N_PORTS],
  input  logic [17:0]      shared_used,
  input  logic             grant,
  input  logic [4:0]       req_port,
  input  logic             drop_valid,
  input  enq_fail_e        drop_reason,
  input  logic             drop_attributed,

  output logic [CNT_W-1:0] v_over_limit,        // a port exceeded its limit
  output logic [CNT_W-1:0] v_over_pool,         // held exceeds what exists
  output logic [CNT_W-1:0] v_reserve_denied,    // refused within the reserve
  output logic [CNT_W-1:0] v_accounting_drift,
  output logic [CNT_W-1:0] v_drop_unattributed,
  output logic             reserves_fit,        // a STANDING property
  output logic             conformant
);

  logic [17:0] total_held;

  always_comb begin
    total_held = 18'd0;
    for (int p = 0; p < N_PORTS; p++) total_held = total_held + held[p];
  end

  // THE STANDING PROPERTY THAT IS TRUE. The reserves must fit; the
  // LIMITS deliberately do not -- Section 18.
  assign reserves_fit = ((N_PORTS * RESERVE_CELLS) <= POOL_CELLS);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      v_over_limit        <= '0;
      v_over_pool         <= '0;
      v_reserve_denied    <= '0;
      v_accounting_drift  <= '0;
      v_drop_unattributed <= '0;
    end else begin
      // No port holds more than its reserve plus its limit.
      for (int p = 0; p < N_PORTS; p++)
        if (held[p] > 18'(RESERVE_CELLS + LIMIT_CELLS))
          if (!(&v_over_limit)) v_over_limit <= v_over_limit + 1'b1;

      // THE REAL CONSERVATION LAW. What is held cannot exceed what
      // exists -- unlike the sum of ALLOWANCES, which is 612% of it.
      if (total_held > 18'(POOL_CELLS))
        if (!(&v_over_pool)) v_over_pool <= v_over_pool + 1'b1;

      // THE GUARANTEE. A request within a port's reserve is never
      // refused, whatever the pool's state. This is what makes the
      // over-commitment safe.
      if (drop_valid && (held[req_port] < 18'(RESERVE_CELLS)))
        if (!(&v_reserve_denied)) v_reserve_denied <= v_reserve_denied + 1'b1;

      // Shared accounting must match the sum of holdings above reserve.
      begin
        automatic logic [17:0] sh = 18'd0;
        for (int p = 0; p < N_PORTS; p++)
          if (held[p] > 18'(RESERVE_CELLS))
            sh = sh + (held[p] - 18'(RESERVE_CELLS));
        if (sh != shared_used)
          if (!(&v_accounting_drift))
            v_accounting_drift <= v_accounting_drift + 1'b1;
      end

      // Every drop is attributed -- Section 9. An unattributed drop is a
      // number with no finding attached to it.
      if (drop_valid && !drop_attributed)
        if (!(&v_drop_unattributed))
          v_drop_unattributed <= v_drop_unattributed + 1'b1;
    end
  end

  assign conformant = (v_over_limit       == '0) && (v_over_pool        == '0) &&
                      (v_reserve_denied   == '0) && (v_accounting_drift == '0) &&
                      (v_drop_unattributed == '0) && reserves_fit;

endmodule

// P1. A frame is enqueued only when both the port's limit and the pool
// permit it. Two independent conditions, two distinct refusals.
property p_enqueue_needs_both;
  @(posedge clk) disable iff (!rst_n)
  (enq_valid && enq_accept) |-> (pool_granted &&
    ((occupancy_cells + 16'(enq_cells)) <= 16'(MAX_CELLS)));
endproperty
a_enqueue_conditions: assert property (p_enqueue_needs_both);

// P2. THE TWO REFUSALS ARE KEPT APART. This port's own limit is this
// port's congestion; an exhausted pool is somebody else's.
property p_refusals_distinguished;
  @(posedge clk) disable iff (!rst_n)
  (enq_valid && !enq_accept)
    |-> (enq_fail inside {EF_QUEUE_LIMIT, EF_POOL_EMPTY, EF_NO_RESERVE});
endproperty
a_refusal_classified: assert property (p_refusals_distinguished);

// P3. Occupancy never exceeds the port's limit.
property p_occupancy_bounded;
  @(posedge clk) disable iff (!rst_n)
  (occupancy_cells <= 16'(MAX_CELLS));
endproperty
a_occupancy_bounded: assert property (p_occupancy_bounded);

// P4. Watermarks trigger at the HIGH threshold, never at full. A
// mechanism that waits for full has already lost the frames in flight
// during its signal's propagation -- Chapter 14.2 quantifies them.
property p_high_watermark_before_full;
  @(posedge clk) disable iff (!rst_n)
  above_high |-> (occupancy_cells < 16'(MAX_CELLS)) or (watermark == WM_FULL);
endproperty
a_watermark_early: assert property (p_high_watermark_before_full);

// P5. Peak occupancy is retained, not averaged away.
property p_peak_monotonic;
  @(posedge clk) disable iff (!rst_n)
  $stable(rst_n) |-> (peak_cells >= $past(peak_cells));
endproperty
a_peak_retained: assert property (p_peak_monotonic);

// P6. THE CONSERVATION LAW. What is held cannot exceed what exists.
// This is the invariant that IS true -- contrast the budget property in
// the rejected callout.
property p_held_within_pool;
  @(posedge clk) disable iff (!rst_n)
  (total_held <= 18'(POOL_CELLS));
endproperty
a_conservation: assert property (p_held_within_pool);

// P7. THE GUARANTEE. A request within a port's own reserve is NEVER
// refused, whatever the pool's state. This is what makes the
// over-commitment safe.
property p_reserve_always_granted;
  @(posedge clk) disable iff (!rst_n)
  (req_valid && ((held[req_port] + 18'(req_cells)) <= 18'(RESERVE_CELLS)))
    |-> grant;
endproperty
a_reserve_honoured: assert property (p_reserve_always_granted);

// P8. No port exceeds its reserve plus its share limit.
property p_limit_enforced;
  @(posedge clk) disable iff (!rst_n)
  (held[req_port] <= 18'(RESERVE_CELLS + LIMIT_CELLS));
endproperty
a_limit_enforced: assert property (p_limit_enforced);

// P9. The reserves fit the pool. THIS budget property is true and must
// be -- a design whose reserves alone exceed the pool cannot honour P7.
property p_reserves_fit;
  @(posedge clk) disable iff (!rst_n)
  reserves_fit;
endproperty
a_reserves_fit: assert property (p_reserves_fit);

// P10. Shared accounting matches the sum of holdings above reserve.
property p_shared_accounting_balances;
  @(posedge clk) disable iff (!rst_n)
  (v_accounting_drift == $past(v_accounting_drift));
endproperty
a_accounting_balances: assert property (p_shared_accounting_balances);

// P11. A release returns exactly what was taken.
property p_release_matches_grant;
  @(posedge clk) disable iff (!rst_n)
  (rel_valid && (rel_cells != 8'd0)) |-> (held[rel_port] >= 18'(rel_cells));
endproperty
a_release_sane: assert property (p_release_matches_grant);

// P12. Every drop is attributed to an egress port, an ingress port and,
// when the pool was the cause, a holder.
property p_every_drop_attributed;
  @(posedge clk) disable iff (!rst_n)
  drop_valid |-> drop_attributed;
endproperty
a_drop_attributed: assert property (p_every_drop_attributed);

// P13. A pool-exhaustion drop is charged to the HOLDER, not to the port
// that could not allocate -- Section 10's whole point.
property p_pool_drop_charged_to_holder;
  @(posedge clk) disable iff (!rst_n)
  (drop_valid && (drop_reason == EF_POOL_EMPTY))
    |=> (pool_drops_caused[$past(pool_holder)] >
         $past(pool_drops_caused[$past(pool_holder)]));
endproperty
a_charged_to_holder: assert property (p_pool_drop_charged_to_holder);

// P14. The holder is sampled AT THE DROP. A periodic sample says who is
// usually busy, not who held the memory this frame needed.
property p_holder_sampled_at_drop;
  @(posedge clk) disable iff (!rst_n)
  (drop_valid && (drop_reason == EF_POOL_EMPTY))
    |-> (pool_holder == largest_holder);
endproperty
a_sampled_at_drop: assert property (p_holder_sampled_at_drop);

// P15. victim_is_not_culprit is high exactly when the port that dropped
// is not the port holding the pool.
property p_victim_culprit_distinguished;
  @(posedge clk) disable iff (!rst_n)
  (drop_valid && (drop_reason == EF_POOL_EMPTY))
    |=> (victim_is_not_culprit == ($past(drop_port) != $past(pool_holder)));
endproperty
a_victim_culprit: assert property (p_victim_culprit_distinguished);

// P16. Exactly one reason counter moves per drop.
property p_one_reason_per_drop;
  @(posedge clk) disable iff (!rst_n)
  drop_valid |=> ($countones({$changed(c_by_reason[1]), $changed(c_by_reason[2]),
                              $changed(c_by_reason[3]), $changed(c_by_reason[4])}) == 1);
endproperty
a_one_reason: assert property (p_one_reason_per_drop);

// P17. LITTLE'S LAW, as an identity. Delay is occupancy divided by the
// drain rate, exactly, for a work-conserving server.
property p_delay_is_occupancy_over_rate;
  @(posedge clk) disable iff (!rst_n)
  sample |-> (delay_ns == (20'(occupancy_cells) * 20'(NS_PER_CELL)));
endproperty
a_littles_law: assert property (p_delay_is_occupancy_over_rate);

// P18. Delay is reported as a HISTOGRAM, not a mean. Chapter 12.6
// Section 6: jitter is what real-time traffic is engineered against, and
// a mean hides the tail.
property p_histogram_maintained;
  @(posedge clk) disable iff (!rst_n)
  sample |=> ($changed(hist[0]) || $changed(hist[1]) || $changed(hist[2]) ||
              $changed(hist[3]) || $changed(hist[4]) || $changed(hist[5]) ||
              $changed(hist[6]) || $changed(hist[7]));
endproperty
a_histogram: assert property (p_histogram_maintained);

// P19. A deeper buffer means a longer wait at full occupancy. The two
// are the same number, which is why "add buffer" is a latency decision.
property p_deeper_buffer_is_longer_wait;
  @(posedge clk) disable iff (!rst_n)
  (sample && (occupancy_cells > $past(occupancy_cells)))
    |-> (delay_ns > $past(delay_ns));
endproperty
a_buffer_is_delay: assert property (p_deeper_buffer_is_longer_wait);

// P20. Absorption time is free cells divided by the excess rate -- a
// buffer's worth is a DURATION, not a size.
property p_absorption_is_a_duration;
  @(posedge clk) disable iff (!rst_n)
  (sample && (oversub_ratio > 6'd1))
    |-> (absorb_us == ((20'(free_cells) * 20'(NS_PER_CELL)) /
                       (20'(oversub_ratio) - 20'd1) / 20'd1000));
endproperty
a_absorption: assert property (p_absorption_is_a_duration);

// P21. The bursts that ACTUALLY arrive are measured, not the ones the
// buffer was sized for.
property p_real_bursts_measured;
  @(posedge clk) disable iff (!rst_n)
  fill_ended |=> (c_bursts > $past(c_bursts));
endproperty
a_bursts_measured: assert property (p_real_bursts_measured);

// P22. The drop rate is in parts per million. 0.05% is 500 ppm and
// matters; as an integer percentage it is zero.
property p_drop_rate_has_resolution;
  @(posedge clk) disable iff (!rst_n)
  (window_valid && (c_drops != '0)) |-> (drop_rate_ppm != 16'd0);
endproperty
a_ppm_resolution: assert property (p_drop_rate_has_resolution);

// P23. A latency violation is reported even when nothing is dropping --
// the one condition a loss-oriented investigation never finds.
property p_delay_reported_without_loss;
  @(posedge clk) disable iff (!rst_n)
  (window_valid && (p99_delay_ns >= 20'd1000000)) |-> delay_bound_exceeded;
endproperty
a_latency_visible: assert property (p_delay_reported_without_loss);

// P24. headroom_critical fires while the port is still clean, which is
// the only useful time.
property p_headroom_warns_early;
  @(posedge clk) disable iff (!rst_n)
  (window_valid && (worst_absorb_us < 20'd10)) |-> headroom_critical;
endproperty
a_headroom_early: assert property (p_headroom_warns_early);

// P25. One port holding more than half the pool is reported as such.
property p_dominance_reported;
  @(posedge clk) disable iff (!rst_n)
  (window_valid && (largest_share_pct > 16'd50)) |-> one_port_dominant;
endproperty
a_dominance: assert property (p_dominance_reported);

// P26. Conformance INCLUDES reserves_fit -- a standing property of the
// configuration, not a history of events.
property p_conformant_includes_reserves;
  @(posedge clk) disable iff (!rst_n)
  conformant |-> reserves_fit;
endproperty
a_conformant_reserves: assert property (p_conformant_includes_reserves);

// P27. Conformance means the accounting is sound and every drop is
// attributed -- never that no frame was lost.
property p_conformant_definition;
  @(posedge clk) disable iff (!rst_n)
  conformant |-> ((v_over_limit == '0) && (v_over_pool == '0) &&
                  (v_reserve_denied == '0) && (v_accounting_drift == '0) &&
                  (v_drop_unattributed == '0));
endproperty
a_conformant_def: assert property (p_conformant_definition);

// P28. Chapter 12.1's discard policy survives: a drop happens only when
// there is genuinely nowhere to put the frame.
property p_drop_only_when_no_room;
  @(posedge clk) disable iff (!rst_n)
  drop_valid |-> ((occupancy_cells + 16'(enq_cells) > 16'(MAX_CELLS)) ||
                  (shared_free < 18'(enq_cells)));
endproperty
a_drop_justified: assert property (p_drop_only_when_no_room);

// P29. An exhausted pool degrades every port and disconnects none --
// P7's guarantee, stated as an outcome.
property p_exhaustion_degrades_not_disconnects;
  @(posedge clk) disable iff (!rst_n)
  pool_exhausted |-> (held[req_port] >= 18'd1 || grant);
endproperty
a_degrade_not_cut: assert property (p_exhaustion_degrades_not_disconnects);

// P30. A port's own limit refusal is counted separately from a pool
// refusal, because the remedies are in different places.
property p_limit_and_pool_counted_apart;
  @(posedge clk) disable iff (!rst_n)
  (drop_valid && (drop_reason == EF_QUEUE_LIMIT)) |-> $stable(c_refuse_pool);
endproperty
a_counted_apart: assert property (p_limit_and_pool_counted_apart);