Backpressure and Head-of-Line Blocking

// -----------------------------------------------------------------------
// hol_pkg -- shared types for head-of-line blocking and backpressure.
// -----------------------------------------------------------------------
package hol_pkg;

  localparam int N_PORTS = 24;
  localparam int PORT_W  = 5;

  // Why a frame at the head could not be forwarded. The distinction
  // matters because only the first is congestion; the others are the
  // composition failing.
  typedef enum logic [2:0] {
    HB_NONE        = 3'd0,
    HB_EGRESS_BUSY = 3'd1,   // the destination is genuinely congested
    HB_EGRESS_XOFF = 3'd2,   // the destination is PAUSED by ITS neighbour
    HB_NO_BUFFER   = 3'd3,   // Chapter 14.1's pool
    HB_BLOCKED     = 3'd4    // this frame is behind one of the above
  } hol_reason_e;

  typedef enum logic [1:0] {
    QD_FIFO = 2'd0,   // one queue, head blocks -- 58.6%
    QD_VOQ  = 2'd1    // one queue per destination -- Section 11
  } queue_discipline_e;

endpackage

// -----------------------------------------------------------------------
// input_queue_fifo -- a single ingress queue, and the measurement that
// makes its blocking visible.
//
// The queue is work-conserving and correct. What it cannot do is offer
// the frame at position two to a server that is free, and that inability
// is the whole of head-of-line blocking.
// -----------------------------------------------------------------------
module input_queue_fifo
  import hol_pkg::*;
#(
  parameter int DEPTH = 64,
  parameter int CNT_W = 32
)(
  input  logic                 clk,
  input  logic                 rst_n,

  input  logic                 enq_valid,
  input  logic [PORT_W-1:0]    enq_dest,
  output logic                 enq_ready,

  input  logic [N_PORTS-1:0]   egress_available,   // which servers are free

  output logic                 head_valid,
  output logic [PORT_W-1:0]    head_dest,
  output logic                 head_can_go,
  input  logic                 head_taken,

  output logic [7:0]           occupancy,
  output logic [7:0]           runnable_behind_head,  // THE MEASUREMENT
  output hol_reason_e          reason,
  output logic [CNT_W-1:0]     c_blocked_cycles,
  output logic [CNT_W-1:0]     c_runnable_blocked,
  output logic [15:0]          hol_loss_pct
);

  logic [PORT_W-1:0] q_dest [DEPTH];
  logic [7:0]        head_ptr, tail_ptr, count;

  assign enq_ready  = (count < 8'(DEPTH));
  assign head_valid = (count != 8'd0);
  assign head_dest  = q_dest[head_ptr];

  // The head can be served if its destination is free. Nothing else in
  // the queue is consulted, which is the definition of a FIFO.
  assign head_can_go = head_valid && egress_available[head_dest];

  // THE MEASUREMENT THIS MODULE EXISTS FOR. How many frames BEHIND the
  // head have destinations that are free right now? Each one is work the
  // switch is holding while a server sits idle -- and no other signal in
  // a FIFO design reports it.
  always_comb begin
    runnable_behind_head = 8'd0;
    if (head_valid && !head_can_go) begin
      for (int i = 1; i < DEPTH; i++)
        if ((8'(i) < count) &&
            egress_available[q_dest[(head_ptr + 8'(i)) % 8'(DEPTH)]])
          runnable_behind_head = runnable_behind_head + 8'd1;
    end
  end

  always_comb begin
    reason = HB_NONE;
    if (head_valid && !head_can_go) reason = HB_EGRESS_BUSY;
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      head_ptr <= '0; tail_ptr <= '0; count <= '0;
      for (int i = 0; i < DEPTH; i++) q_dest[i] <= '0;
      c_blocked_cycles   <= '0;
      c_runnable_blocked <= '0;
      hol_loss_pct       <= '0;
    end else begin
      if (enq_valid && enq_ready) begin
        q_dest[tail_ptr] <= enq_dest;
        tail_ptr <= (tail_ptr + 8'd1) % 8'(DEPTH);
        count    <= count + 8'd1;
      end
      if (head_taken && head_valid) begin
        head_ptr <= (head_ptr + 8'd1) % 8'(DEPTH);
        count    <= count - 8'd1;
      end

      if (head_valid && !head_can_go) begin
        c_blocked_cycles <= c_blocked_cycles + 1'b1;
        // Cycles in which the switch had runnable work and could not
        // reach it. This is the capacity Section 4's bound describes.
        if (runnable_behind_head != 8'd0)
          c_runnable_blocked <= c_runnable_blocked + CNT_W'(runnable_behind_head);
      end

      if (c_blocked_cycles[15:0] == 16'hFFFF)
        hol_loss_pct <= 16'((c_runnable_blocked * CNT_W'(100)) /
                            (c_blocked_cycles + CNT_W'(1)));
    end
  end

endmodule

// -----------------------------------------------------------------------
// hol_detector -- how much throughput is this FIFO discipline costing?
//
// Section 4's bound says 41.4% under uniform traffic. This module reports
// what THIS switch is actually losing, which under non-uniform traffic is
// worse and under a single hot destination is much worse.
// -----------------------------------------------------------------------
module hol_detector
  import hol_pkg::*;
#(
  parameter int CNT_W = 32,
  parameter int WIN   = 1_000_000
)(
  input  logic                 clk,
  input  logic                 rst_n,

  input  logic [N_PORTS-1:0]   head_valid,
  input  logic [N_PORTS-1:0]   head_blocked,
  input  logic [N_PORTS-1:0]   egress_idle,
  input  logic [7:0]           runnable_behind [N_PORTS],
  input  logic [N_PORTS-1:0]   grant,

  output logic                 window_valid,
  output logic [15:0]          throughput_pct,
  output logic [15:0]          hol_loss_pct,
  output logic [15:0]          idle_with_work_pct,
  output logic                 at_the_bound,        // near 58.6%
  output logic                 below_the_bound,     // non-uniform traffic
  output logic [PORT_W-1:0]    hottest_dest,
  output logic [CNT_W-1:0]     c_slots,
  output logic [CNT_W-1:0]     c_grants
);

  logic [CNT_W-1:0] win_slots, win_grants, win_idle_work, win_runnable;
  logic [CNT_W-1:0] dest_hits [N_PORTS];

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      win_slots <= '0; win_grants <= '0; win_idle_work <= '0; win_runnable <= '0;
      for (int p = 0; p < N_PORTS; p++) dest_hits[p] <= '0;
      c_slots <= '0; c_grants <= '0;
      window_valid       <= 1'b0;
      throughput_pct     <= 16'd100;
      hol_loss_pct       <= '0;
      idle_with_work_pct <= '0;
      at_the_bound       <= 1'b0;
      below_the_bound    <= 1'b0;
      hottest_dest       <= '0;
    end else begin
      window_valid <= 1'b0;
      win_slots    <= win_slots + 1'b1;
      c_slots      <= c_slots + 1'b1;
      win_grants   <= win_grants + CNT_W'($countones(grant));
      c_grants     <= c_grants + CNT_W'($countones(grant));

      // THE CONDITION THE BOUND IS ABOUT. An egress port idle while some
      // ingress queue holds a frame for it -- behind a head it cannot
      // pass. Every one of these is capacity that exists and cannot be
      // reached.
      for (int p = 0; p < N_PORTS; p++) begin
        if (head_valid[p] && head_blocked[p] && (runnable_behind[p] != 8'd0)) begin
          win_idle_work <= win_idle_work + 1'b1;
          win_runnable  <= win_runnable + CNT_W'(runnable_behind[p]);
        end
      end

      if (win_slots >= CNT_W'(WIN)) begin
        // Throughput as a share of the N_PORTS grants per slot that a
        // fully utilised switch would issue.
        throughput_pct <= 16'((win_grants * CNT_W'(100)) /
                              (win_slots * CNT_W'(N_PORTS)));
        hol_loss_pct   <= 16'((win_runnable * CNT_W'(100)) /
                              (win_slots * CNT_W'(N_PORTS)));
        idle_with_work_pct <= 16'((win_idle_work * CNT_W'(100)) / win_slots);

        // Section 4's bound, as two bits. AT the bound means the traffic
        // is roughly uniform and the discipline is the limit. BELOW it
        // means the traffic is non-uniform, which is worse and is what
        // real traffic does.
        at_the_bound    <= (throughput_pct >= 16'd55) &&
                           (throughput_pct <= 16'd62);
        below_the_bound <= (throughput_pct < 16'd55);

        begin
          automatic logic [CNT_W-1:0] hi = '0;
          automatic logic [PORT_W-1:0] hp = '0;
          for (int p = 0; p < N_PORTS; p++)
            if (dest_hits[p] > hi) begin hi = dest_hits[p]; hp = PORT_W'(p); end
          hottest_dest <= hp;
          for (int p = 0; p < N_PORTS; p++) dest_hits[p] <= '0;
        end

        win_slots <= '0; win_grants <= '0;
        win_idle_work <= '0; win_runnable <= '0;
        window_valid <= 1'b1;
      end
    end
  end

  wire _unused = |egress_idle;

endmodule

// -----------------------------------------------------------------------
// backpressure_propagator -- how a pause at one egress becomes a pause on
// an upstream link.
//
// Nothing here is a policy decision. Each step follows from the previous
// one, and the module exists to make the chain visible rather than to
// choose anything.
// -----------------------------------------------------------------------
module backpressure_propagator
  import hol_pkg::*;
#(
  parameter int HIGH_CELLS = 3072,
  parameter int CNT_W      = 32
)(
  input  logic                 clk,
  input  logic                 rst_n,

  input  logic [N_PORTS-1:0]   egress_paused,      // by OUR neighbours
  input  logic [N_PORTS-1:0]   egress_congested,   // genuinely oversubscribed
  input  logic [PORT_W-1:0]    head_dest [N_PORTS],
  input  logic [N_PORTS-1:0]   head_valid,
  input  logic [15:0]          ingress_occupancy [N_PORTS],

  output logic [N_PORTS-1:0]   head_blocked,
  output hol_reason_e          block_reason [N_PORTS],
  output logic [N_PORTS-1:0]   send_pause_upstream,

  output logic [CNT_W-1:0]     c_blocked_by_congestion,
  output logic [CNT_W-1:0]     c_blocked_by_pause,     // second-order
  output logic [CNT_W-1:0]     c_pauses_generated,
  output logic [15:0]          second_order_pct,
  output logic                 propagating
);

  always_comb begin
    for (int p = 0; p < N_PORTS; p++) begin
      head_blocked[p]  = 1'b0;
      block_reason[p]  = HB_NONE;

      if (head_valid[p]) begin
        if (egress_congested[head_dest[p]]) begin
          // FIRST ORDER. This is real congestion at the destination.
          head_blocked[p] = 1'b1;
          block_reason[p] = HB_EGRESS_BUSY;
        end else if (egress_paused[head_dest[p]]) begin
          // SECOND ORDER. The destination is not congested -- it has
          // been PAUSED by its own neighbour. The congestion this queue
          // is suffering belongs to a switch it may never send to.
          head_blocked[p] = 1'b1;
          block_reason[p] = HB_EGRESS_XOFF;
        end
      end

      // And the consequence: a blocked head fills this ingress queue,
      // which pauses the link that feeds it -- one more hop.
      send_pause_upstream[p] = (ingress_occupancy[p] >= 16'(HIGH_CELLS));
    end
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      c_blocked_by_congestion <= '0;
      c_blocked_by_pause      <= '0;
      c_pauses_generated      <= '0;
      second_order_pct        <= '0;
      propagating             <= 1'b0;
    end else begin
      for (int p = 0; p < N_PORTS; p++) begin
        if (block_reason[p] == HB_EGRESS_BUSY)
          c_blocked_by_congestion <= c_blocked_by_congestion + 1'b1;
        if (block_reason[p] == HB_EGRESS_XOFF)
          c_blocked_by_pause <= c_blocked_by_pause + 1'b1;
        if (send_pause_upstream[p])
          c_pauses_generated <= c_pauses_generated + 1'b1;
      end

      // THE NUMBER THAT SAYS WHOSE PROBLEM THIS IS. Blocking caused by
      // a PAUSE rather than by congestion is congestion that arrived
      // from somewhere else, and this switch is a conduit rather than a
      // cause.
      if (c_blocked_by_congestion + c_blocked_by_pause != '0)
        second_order_pct <= 16'((c_blocked_by_pause * CNT_W'(100)) /
                                (c_blocked_by_congestion + c_blocked_by_pause));

      propagating <= (|send_pause_upstream) && (|egress_paused);
    end
  end

endmodule

// -----------------------------------------------------------------------
// blast_radius_tracker -- how many distinct conversations did this
// congestion event affect?
//
// The frame count says how much was lost. This says how much was
// TOUCHED, and Section 8 shows the two move in opposite directions when
// backpressure is enabled.
// -----------------------------------------------------------------------
module blast_radius_tracker
  import hol_pkg::*;
#(
  parameter int CNT_W = 32
)(
  input  logic                 clk,
  input  logic                 rst_n,

  input  logic                 event_active,      // any head blocked anywhere
  input  logic [N_PORTS-1:0]   head_blocked,
  input  logic [PORT_W-1:0]    head_dest [N_PORTS],
  input  hol_reason_e          block_reason [N_PORTS],

  output logic [15:0]          pairs_affected,
  output logic [15:0]          worst_pairs_affected,
  output logic [15:0]          ingress_ports_affected,
  output logic [15:0]          egress_ports_affected,
  output logic [15:0]          second_order_pairs,
  output logic [CNT_W-1:0]     c_events,
  output logic [CNT_W-1:0]     c_pair_seconds,
  output logic                 wide_event          // beyond one switch's worth
);

  logic [N_PORTS-1:0] pair_seen [N_PORTS];   // [ingress][egress]
  logic [N_PORTS-1:0] pair_2nd  [N_PORTS];
  logic               active_q;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (int i = 0; i < N_PORTS; i++) begin
        pair_seen[i] <= '0; pair_2nd[i] <= '0;
      end
      active_q               <= 1'b0;
      pairs_affected         <= '0;
      worst_pairs_affected   <= '0;
      ingress_ports_affected <= '0;
      egress_ports_affected  <= '0;
      second_order_pairs     <= '0;
      c_events               <= '0;
      c_pair_seconds         <= '0;
      wide_event             <= 1'b0;
    end else begin
      active_q <= event_active;

      if (event_active) begin
        for (int i = 0; i < N_PORTS; i++)
          if (head_blocked[i]) begin
            pair_seen[i][head_dest[i]] <= 1'b1;
            // A pair blocked by a PAUSE rather than by congestion is a
            // conversation affected by somebody else's problem entirely.
            if (block_reason[i] == HB_EGRESS_XOFF)
              pair_2nd[i][head_dest[i]] <= 1'b1;
            // Pair-seconds: the integral of affected conversations over
            // time, which is the closest single number to "how bad was
            // it" that a switch can compute.
            c_pair_seconds <= c_pair_seconds + 1'b1;
          end
      end

      // At the end of an event, report and reset.
      if (active_q && !event_active) begin
        automatic logic [15:0] pairs = 16'd0;
        automatic logic [15:0] snd   = 16'd0;
        automatic logic [15:0] ing   = 16'd0;
        automatic logic [N_PORTS-1:0] egr = '0;
        for (int i = 0; i < N_PORTS; i++) begin
          if (pair_seen[i] != '0) ing = ing + 16'd1;
          egr   = egr | pair_seen[i];
          pairs = pairs + 16'($countones(pair_seen[i]));
          snd   = snd   + 16'($countones(pair_2nd[i]));
        end
        pairs_affected         <= pairs;
        second_order_pairs     <= snd;
        ingress_ports_affected <= ing;
        egress_ports_affected  <= 16'($countones(egr));
        if (pairs > worst_pairs_affected) worst_pairs_affected <= pairs;
        // MORE PAIRS THAN THIS SWITCH HAS INGRESS PORTS means the event
        // touched more conversations than a single congested egress
        // could -- Section 8's compounding, observed.
        wide_event <= (pairs > 16'(N_PORTS));
        if (!(&c_events)) c_events <= c_events + 1'b1;

        for (int i = 0; i < N_PORTS; i++) begin
          pair_seen[i] <= '0; pair_2nd[i] <= '0;
        end
      end
    end
  end

endmodule

// -----------------------------------------------------------------------
// voq_bank -- N queues at one ingress port, one per egress destination.
//
// The queues are POINTER LISTS into Chapter 14.1 Section 5's shared pool,
// not separate memories. What costs is not the storage -- 32 bits of
// state per queue -- but Section 13's scheduler, which must now choose
// among N candidates per ingress instead of accepting the one it had.
// -----------------------------------------------------------------------
module voq_bank
  import hol_pkg::*;
#(
  parameter int CNT_W = 32
)(
  input  logic                 clk,
  input  logic                 rst_n,

  input  logic                 enq_valid,
  input  logic [PORT_W-1:0]    enq_dest,
  input  logic [11:0]          enq_handle,       // Chapter 14.1's pool handle

  input  logic [N_PORTS-1:0]   serve,            // scheduler's selection
  output logic [11:0]          serve_handle,

  output logic [N_PORTS-1:0]   nonempty,         // THE N CANDIDATES
  output logic [7:0]           depth [N_PORTS],
  output logic [7:0]           total_depth,
  output logic [PORT_W-1:0]    deepest_voq,

  output logic [CNT_W-1:0]     c_enq,
  output logic [CNT_W-1:0]     c_served,
  output logic [CNT_W-1:0]     bits_of_state,
  output logic                 head_of_line_possible   // permanently 0
);

  logic [11:0] head [N_PORTS];
  logic [11:0] tail [N_PORTS];
  logic [7:0]  cnt  [N_PORTS];

  always_comb begin
    for (int d = 0; d < N_PORTS; d++) nonempty[d] = (cnt[d] != 8'd0);
  end

  // THE PROPERTY THIS STRUCTURE EXISTS FOR, as a wire. With one queue per
  // destination, a blocked destination blocks only its own queue -- there
  // is no position in which a frame can be held behind a frame for a
  // different destination.
  assign head_of_line_possible = 1'b0;

  always_comb begin
    serve_handle = 12'd0;
    for (int d = 0; d < N_PORTS; d++)
      if (serve[d]) serve_handle = head[d];
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (int d = 0; d < N_PORTS; d++) begin
        head[d] <= '0; tail[d] <= '0; cnt[d] <= '0;
      end
      c_enq <= '0; c_served <= '0;
      deepest_voq <= '0;
    end else begin
      if (enq_valid) begin
        // The frame joins the queue for ITS destination. Nothing else in
        // the bank is affected, which is the whole difference.
        tail[enq_dest] <= enq_handle;
        cnt[enq_dest]  <= cnt[enq_dest] + 8'd1;
        if (cnt[enq_dest] == 8'd0) head[enq_dest] <= enq_handle;
        c_enq <= c_enq + 1'b1;
      end

      for (int d = 0; d < N_PORTS; d++)
        if (serve[d] && (cnt[d] != 8'd0)) begin
          cnt[d]   <= cnt[d] - 8'd1;
          c_served <= c_served + 1'b1;
        end

      begin
        automatic logic [7:0] hi = 8'd0;
        automatic logic [PORT_W-1:0] hp = '0;
        for (int d = 0; d < N_PORTS; d++)
          if (cnt[d] > hi) begin hi = cnt[d]; hp = PORT_W'(d); end
        deepest_voq <= hp;
      end
    end
  end

  always_comb begin
    total_depth = 8'd0;
    for (int d = 0; d < N_PORTS; d++) begin
      depth[d] = cnt[d];
      total_depth = total_depth + cnt[d];
    end
  end

  // Head, tail and count per queue. 576 queues at 32 bits is 2.3 KiB
  // against Chapter 14.1's 12 MiB pool -- the storage is not the cost.
  assign bits_of_state = CNT_W'(N_PORTS) * CNT_W'(N_PORTS) * CNT_W'(32);

endmodule

// -----------------------------------------------------------------------
// voq_scheduler -- iterative request-grant-accept matching.
//
// One round produces a MAXIMAL matching, worth about 63%. Log N rounds
// produce something close to MAXIMUM, worth about 99%. The difference is
// 36 percentage points and five cycles.
// -----------------------------------------------------------------------
module voq_scheduler
  import hol_pkg::*;
#(
  parameter int ROUNDS = 5,          // ~log2(24)
  parameter int CNT_W  = 32
)(
  input  logic                 clk,
  input  logic                 rst_n,

  input  logic                 start,
  input  logic [N_PORTS-1:0]   voq_nonempty [N_PORTS],   // [ingress][egress]

  output logic                 done,
  output logic [N_PORTS-1:0]   grant_egress [N_PORTS],   // the matching
  output logic [7:0]           match_size,
  output logic [7:0]           max_possible,

  output logic [CNT_W-1:0]     c_rounds_used,
  output logic [15:0]          match_efficiency_pct,
  output logic [7:0]           rounds_configured
);

  logic [N_PORTS-1:0] ing_matched, egr_matched;
  logic [N_PORTS-1:0] request [N_PORTS];
  logic [N_PORTS-1:0] grant   [N_PORTS];
  logic [2:0]         round_q;
  logic               busy_q;

  // Round-robin pointers, so that repeated slots do not always favour the
  // same pair. Without them the matching is stable and starves whoever
  // loses the first tie.
  logic [PORT_W-1:0] ing_ptr [N_PORTS];
  logic [PORT_W-1:0] egr_ptr [N_PORTS];

  always_comb begin
    // REQUEST. Every unmatched ingress asks every destination it has a
    // frame for. This is the step a FIFO cannot perform -- it has one
    // candidate and therefore one request.
    for (int i = 0; i < N_PORTS; i++)
      request[i] = ing_matched[i] ? '0 : (voq_nonempty[i] & ~egr_matched);

    // GRANT. Each unmatched egress picks one requester, starting from
    // its round-robin pointer.
    for (int e = 0; e < N_PORTS; e++) begin
      grant[e] = '0;
      if (!egr_matched[e]) begin
        for (int k = N_PORTS-1; k >= 0; k--) begin
          automatic int i = (int'(egr_ptr[e]) + k) % N_PORTS;
          if (request[i][e]) grant[e] = (N_PORTS'(1) << i);
        end
      end
    end
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      ing_matched <= '0; egr_matched <= '0;
      for (int i = 0; i < N_PORTS; i++) begin
        grant_egress[i] <= '0; ing_ptr[i] <= '0; egr_ptr[i] <= '0;
      end
      round_q <= '0; busy_q <= 1'b0; done <= 1'b0;
      match_size <= '0; c_rounds_used <= '0;
      match_efficiency_pct <= 16'd100;
    end else begin
      done <= 1'b0;

      if (start) begin
        ing_matched <= '0; egr_matched <= '0;
        for (int i = 0; i < N_PORTS; i++) grant_egress[i] <= '0;
        round_q <= '0; busy_q <= 1'b1;
      end else if (busy_q) begin
        // ACCEPT. Each ingress with grants takes one, and the pair is
        // removed from both sides for the remaining rounds.
        for (int i = 0; i < N_PORTS; i++) begin
          for (int e = N_PORTS-1; e >= 0; e--)
            if (grant[e][i] && !ing_matched[i]) begin
              ing_matched[i]     <= 1'b1;
              egr_matched[e]     <= 1'b1;
              grant_egress[i][e] <= 1'b1;
              ing_ptr[i]         <= PORT_W'(e) + PORT_W'(1);
              egr_ptr[e]         <= PORT_W'(i) + PORT_W'(1);
            end
        end

        round_q       <= round_q + 3'd1;
        c_rounds_used <= c_rounds_used + 1'b1;

        if (round_q == 3'(ROUNDS - 1)) begin
          busy_q     <= 1'b0;
          done       <= 1'b1;
          match_size <= 8'($countones(ing_matched));
        end
      end
    end
  end

  // The size of the matching a perfect scheduler could have found: the
  // number of ingress ports with any work, capped by the number of
  // egress ports with any demand.
  always_comb begin
    automatic logic [7:0] ing_any = 8'd0;
    automatic logic [N_PORTS-1:0] egr_any = '0;
    for (int i = 0; i < N_PORTS; i++) begin
      if (voq_nonempty[i] != '0) ing_any = ing_any + 8'd1;
      egr_any = egr_any | voq_nonempty[i];
    end
    max_possible = (ing_any < 8'($countones(egr_any)))
                 ? ing_any : 8'($countones(egr_any));
  end

  assign rounds_configured = 8'(ROUNDS);

endmodule

// -----------------------------------------------------------------------
// hol_telemetry -- which of the three limits is binding?
//
// A switch below its line rate has three candidate explanations and they
// are fixed in three different places. Distinguishing them is the whole
// value of the module.
// -----------------------------------------------------------------------
module hol_telemetry
  import hol_pkg::*;
#(
  parameter int CNT_W = 32,
  parameter int WIN   = 1_000_000
)(
  input  logic             clk,
  input  logic             rst_n,

  input  queue_discipline_e discipline,
  input  logic [15:0]      throughput_pct,
  input  logic [7:0]       match_size,
  input  logic [7:0]       max_possible,
  input  logic [15:0]      second_order_pct,
  input  logic [15:0]      pairs_affected,
  input  logic [7:0]       rounds_configured,
  input  logic             slot,

  output logic             window_valid,
  output logic [15:0]      match_efficiency_pct,
  output logic             limited_by_discipline,   // FIFO -- 58.6%
  output logic             limited_by_scheduler,    // too few rounds
  output logic             limited_by_upstream,     // somebody else's congestion
  output logic             none_of_the_above,       // genuine offered load
  output logic [CNT_W-1:0] c_slots
);

  logic [CNT_W-1:0] win, win_match, win_max;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      win <= '0; win_match <= '0; win_max <= '0; c_slots <= '0;
      window_valid          <= 1'b0;
      match_efficiency_pct  <= 16'd100;
      limited_by_discipline <= 1'b0;
      limited_by_scheduler  <= 1'b0;
      limited_by_upstream   <= 1'b0;
      none_of_the_above     <= 1'b1;
    end else begin
      window_valid <= 1'b0;

      if (slot) begin
        win       <= win + 1'b1;
        c_slots   <= c_slots + 1'b1;
        win_match <= win_match + CNT_W'(match_size);
        win_max   <= win_max + CNT_W'(max_possible);
      end

      if (win >= CNT_W'(WIN)) begin
        match_efficiency_pct <= (win_max == '0) ? 16'd100
                              : 16'((win_match * CNT_W'(100)) / win_max);

        // THREE DIAGNOSES, MUTUALLY EXCLUSIVE. A FIFO near 58.6% is the
        // discipline. A VOQ with a poor match is the scheduler. Blocking
        // that is mostly second-order is somebody else's congestion
        // arriving through this switch.
        limited_by_discipline <= (discipline == QD_FIFO) &&
                                 (throughput_pct < 16'd65);
        limited_by_scheduler  <= (discipline == QD_VOQ) &&
                                 (match_efficiency_pct < 16'd90);
        limited_by_upstream   <= (second_order_pct > 16'd50);
        none_of_the_above     <= (throughput_pct >= 16'd90) &&
                                 (second_order_pct <= 16'd50);

        win <= '0; win_match <= '0; win_max <= '0;
        window_valid <= 1'b1;
      end
    end
  end

  wire _unused = |pairs_affected | |rounds_configured;

endmodule

// -----------------------------------------------------------------------
// hol_conformance_monitor -- checks properties of the COMPOSITION.
//
// Every component check in Modules 12 to 14 passes on a FIFO-ingress
// switch losing 41.4% of its capacity. What this module checks is the
// system-level condition those checks cannot see: an egress port idle
// while an ingress queue holds work for it.
// -----------------------------------------------------------------------
module hol_conformance_monitor
  import hol_pkg::*;
#(
  parameter int CNT_W = 32
)(
  input  logic                 clk,
  input  logic                 rst_n,

  input  queue_discipline_e    discipline,
  input  logic [N_PORTS-1:0]   egress_idle,
  input  logic [N_PORTS-1:0]   voq_nonempty [N_PORTS],
  input  logic [N_PORTS-1:0]   grant_egress [N_PORTS],
  input  logic [7:0]           match_size,
  input  logic [7:0]           max_possible,
  input  logic                 head_of_line_possible,

  output logic [CNT_W-1:0]     v_idle_with_work,     // THE system check
  output logic [CNT_W-1:0]     v_double_grant_ing,
  output logic [CNT_W-1:0]     v_double_grant_egr,
  output logic [CNT_W-1:0]     v_grant_without_work,
  output logic [CNT_W-1:0]     v_hol_in_voq,         // must be impossible
  output logic                 voq_removes_hol,      // a structural claim
  output logic                 conformant
);

  // A STRUCTURAL PROPERTY, not a history. With one queue per destination
  // there is no position in which a frame can be held behind a frame for
  // a different destination -- so head-of-line blocking is impossible by
  // construction rather than absent by observation.
  assign voq_removes_hol = (discipline == QD_VOQ) && !head_of_line_possible;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      v_idle_with_work     <= '0;
      v_double_grant_ing   <= '0;
      v_double_grant_egr   <= '0;
      v_grant_without_work <= '0;
      v_hol_in_voq         <= '0;
    end else begin
      // THE COMPOSITION CHECK. An egress port idle while SOME ingress
      // holds a frame for it. On a VOQ switch with a good scheduler this
      // must be zero; on a FIFO switch it is the 41.4%, and no
      // component-level check reports it.
      for (int e = 0; e < N_PORTS; e++) begin
        automatic logic wanted = 1'b0;
        for (int i = 0; i < N_PORTS; i++)
          if (voq_nonempty[i][e]) wanted = 1'b1;
        if (egress_idle[e] && wanted)
          if (!(&v_idle_with_work))
            v_idle_with_work <= v_idle_with_work + 1'b1;
      end

      // The matching is a matching: no ingress twice, no egress twice.
      for (int i = 0; i < N_PORTS; i++)
        if ($countones(grant_egress[i]) > 1)
          if (!(&v_double_grant_ing))
            v_double_grant_ing <= v_double_grant_ing + 1'b1;

      begin
        automatic logic [N_PORTS-1:0] egr_used = '0;
        for (int i = 0; i < N_PORTS; i++) begin
          if ((egr_used & grant_egress[i]) != '0)
            if (!(&v_double_grant_egr))
              v_double_grant_egr <= v_double_grant_egr + 1'b1;
          egr_used = egr_used | grant_egress[i];
        end
      end

      // A grant to a queue with nothing in it.
      for (int i = 0; i < N_PORTS; i++)
        if ((grant_egress[i] & ~voq_nonempty[i]) != '0)
          if (!(&v_grant_without_work))
            v_grant_without_work <= v_grant_without_work + 1'b1;

      // Head-of-line blocking observed on a VOQ switch is a structural
      // impossibility, so a non-zero count here means the queues are not
      // actually per-destination.
      if ((discipline == QD_VOQ) && head_of_line_possible)
        if (!(&v_hol_in_voq)) v_hol_in_voq <= v_hol_in_voq + 1'b1;
    end
  end

  assign conformant = (v_double_grant_ing   == '0) &&
                      (v_double_grant_egr   == '0) &&
                      (v_grant_without_work == '0) &&
                      (v_hol_in_voq         == '0) &&
                      ((discipline == QD_FIFO) || voq_removes_hol);

endmodule

// P1. The queue is WORK-CONSERVING: it presents its head whenever the
// head can be served. This holds, and it is not enough.
property p_fifo_is_work_conserving;
  @(posedge clk) disable iff (!rst_n)
  (head_valid && egress_available[head_dest]) |-> head_can_go;
endproperty
a_work_conserving: assert property (p_fifo_is_work_conserving);

// P2. A FIFO offers exactly ONE candidate. This is the constraint the
// bound is about, and it is a property of the structure.
property p_fifo_offers_one;
  @(posedge clk) disable iff (!rst_n)
  head_valid |-> ($countones(candidates) == 1);
endproperty
a_one_candidate: assert property (p_fifo_offers_one);

// P3. A blocked head blocks everything behind it, whatever its
// destination -- the definition of head-of-line blocking.
property p_blocked_head_blocks_all;
  @(posedge clk) disable iff (!rst_n)
  (head_valid && !head_can_go) |-> !head_taken;
endproperty
a_head_blocks: assert property (p_blocked_head_blocks_all);

// P4. THE MEASUREMENT. Runnable frames behind a blocked head are counted
// -- no other signal in a FIFO design reports the loss.
property p_runnable_counted;
  @(posedge clk) disable iff (!rst_n)
  (head_valid && !head_can_go && (runnable_behind_head != 8'd0))
    |=> (c_runnable_blocked > $past(c_runnable_blocked));
endproperty
a_runnable_counted: assert property (p_runnable_counted);

// P5. Enqueue is refused only when the queue is genuinely full.
property p_enq_refused_only_when_full;
  @(posedge clk) disable iff (!rst_n)
  (enq_valid && !enq_ready) |-> (count >= 8'(DEPTH));
endproperty
a_enq_full: assert property (p_enq_refused_only_when_full);

// P6. THE COMPOSITION CONDITION. An egress idle while some ingress holds
// work for it -- this is the capacity the bound describes, and no
// component-level check reports it.
property p_idle_with_work_detected;
  @(posedge clk) disable iff (!rst_n)
  (egress_idle[e] && some_ingress_wants[e])
    |=> (v_idle_with_work > $past(v_idle_with_work));
endproperty
a_idle_with_work: assert property (p_idle_with_work_detected);

// P7. At the bound and below it are DIFFERENT findings. At it, the
// traffic is uniform and the discipline is the limit; below it, the
// traffic is non-uniform, which is worse and is what real traffic does.
property p_bound_states_exclusive;
  @(posedge clk) disable iff (!rst_n)
  window_valid |-> !(at_the_bound && below_the_bound);
endproperty
a_bound_exclusive: assert property (p_bound_states_exclusive);

// P8. A FIFO switch near 58.6% is CONFORMANT. The bound is the
// discipline being what it is, not a fault.
property p_fifo_at_bound_is_conformant;
  @(posedge clk) disable iff (!rst_n)
  ((discipline == QD_FIFO) && at_the_bound) |-> conformant;
endproperty
a_bound_is_ok: assert property (p_fifo_at_bound_is_conformant);

// P9. The loss is reported as a percentage of slots, not as a drop
// count -- nothing was dropped.
property p_loss_is_not_drops;
  @(posedge clk) disable iff (!rst_n)
  (window_valid && (hol_loss_pct != 16'd0)) |-> (c_drops == $past(c_drops));
endproperty
a_loss_not_drops: assert property (p_loss_is_not_drops);

// P10. FIRST ORDER AND SECOND ORDER ARE SEPARATED. A head blocked by a
// congested destination is this switch's congestion; one blocked by a
// PAUSED destination is somebody else's, arriving here.
property p_block_reason_classified;
  @(posedge clk) disable iff (!rst_n)
  head_blocked[p] |-> (block_reason[p] inside {HB_EGRESS_BUSY, HB_EGRESS_XOFF});
endproperty
a_reason_classified: assert property (p_block_reason_classified);

// P11. A paused egress blocks a head exactly as a congested one does --
// the ingress cannot tell them apart, which is why the reason must be
// carried from the egress.
property p_pause_blocks_like_congestion;
  @(posedge clk) disable iff (!rst_n)
  (head_valid[p] && egress_paused[head_dest[p]] &&
   !egress_congested[head_dest[p]])
    |-> (head_blocked[p] && (block_reason[p] == HB_EGRESS_XOFF));
endproperty
a_pause_blocks: assert property (p_pause_blocks_like_congestion);

// P12. A full ingress queue pauses the link that feeds it -- one more
// hop of propagation, and the step is not a policy decision.
property p_full_ingress_pauses_upstream;
  @(posedge clk) disable iff (!rst_n)
  (ingress_occupancy[p] >= 16'(HIGH_CELLS)) |-> send_pause_upstream[p];
endproperty
a_propagates: assert property (p_full_ingress_pauses_upstream);

// P13. propagating is high when this switch is BOTH receiving and
// generating backpressure -- one link of the chain rather than an end.
property p_propagating_means_conduit;
  @(posedge clk) disable iff (!rst_n)
  propagating |-> ((|send_pause_upstream) && (|egress_paused));
endproperty
a_conduit: assert property (p_propagating_means_conduit);

// P14. second_order_pct says whether this switch is a cause or a
// conduit, and following it upstream reaches the origin.
property p_second_order_reported;
  @(posedge clk) disable iff (!rst_n)
  (c_blocked_by_pause > c_blocked_by_congestion) |-> (second_order_pct > 16'd50);
endproperty
a_second_order: assert property (p_second_order_reported);

// P15. Every blocked pair is recorded exactly once per event.
property p_pair_recorded_once;
  @(posedge clk) disable iff (!rst_n)
  (event_active && head_blocked[i]) |=> pair_seen[i][$past(head_dest[i])];
endproperty
a_pair_recorded: assert property (p_pair_recorded_once);

// P16. More pairs than this switch has ingress ports means several
// egress ports were unavailable at once -- on a switch that is not
// oversubscribed, that means they were PAUSED.
property p_wide_event_flagged;
  @(posedge clk) disable iff (!rst_n)
  (pairs_affected > 16'(N_PORTS)) |-> wide_event;
endproperty
a_wide_event: assert property (p_wide_event_flagged);

// P17. Pair-seconds integrate affected conversations over time -- the
// closest single number to "how bad was it" a switch can compute.
property p_pair_seconds_accumulates;
  @(posedge clk) disable iff (!rst_n)
  (event_active && (|head_blocked)) |=> (c_pair_seconds > $past(c_pair_seconds));
endproperty
a_pair_seconds: assert property (p_pair_seconds_accumulates);

// P18. THE STRUCTURAL CLAIM. With one queue per destination there is no
// position in which a frame waits behind one for elsewhere.
property p_voq_has_no_hol;
  @(posedge clk) disable iff (!rst_n)
  (discipline == QD_VOQ) |-> !head_of_line_possible;
endproperty
a_no_hol_in_voq: assert property (p_voq_has_no_hol);

// P19. A frame joins the queue for ITS destination and affects nothing
// else in the bank.
property p_enq_touches_one_queue;
  @(posedge clk) disable iff (!rst_n)
  enq_valid |=> ((cnt[$past(enq_dest)] == $past(cnt[$past(enq_dest)]) + 8'd1));
endproperty
a_one_queue_touched: assert property (p_enq_touches_one_queue);

// P20. The ingress offers N candidates, not one. This is the whole
// difference from P2.
property p_voq_offers_many;
  @(posedge clk) disable iff (!rst_n)
  (discipline == QD_VOQ) |-> (nonempty == candidates);
endproperty
a_many_candidates: assert property (p_voq_offers_many);

// P21. The queues are POINTER LISTS -- the frames stay in Chapter 14.1's
// pool and only their organisation changed.
property p_voq_state_is_pointers;
  @(posedge clk) disable iff (!rst_n)
  (bits_of_state == (CNT_W'(N_PORTS) * CNT_W'(N_PORTS) * CNT_W'(32)));
endproperty
a_pointer_state: assert property (p_voq_state_is_pointers);

// P22. THE MATCHING IS A MATCHING. No ingress appears twice.
property p_no_double_grant_ingress;
  @(posedge clk) disable iff (!rst_n)
  done |-> ($countones(grant_egress[i]) <= 1);
endproperty
a_ingress_once: assert property (p_no_double_grant_ingress);

// P23. No egress appears twice.
property p_no_double_grant_egress;
  @(posedge clk) disable iff (!rst_n)
  done |-> (v_double_grant_egr == $past(v_double_grant_egr));
endproperty
a_egress_once: assert property (p_no_double_grant_egress);

// P24. A grant goes only to a non-empty queue.
property p_grant_has_work;
  @(posedge clk) disable iff (!rst_n)
  done |-> ((grant_egress[i] & ~voq_nonempty[i]) == '0);
endproperty
a_grant_has_work: assert property (p_grant_has_work);

// P25. THE ROUND-ROBIN POINTERS ADVANCE. Without them the matching is
// stable and whoever loses the first tie loses every subsequent one --
// Chapter 12.1 Section 9's argument, one level up.
property p_pointers_advance;
  @(posedge clk) disable iff (!rst_n)
  (grant[e][i] && !ing_matched[i]) |=> (egr_ptr[e] != $past(i));
endproperty
a_pointers_advance: assert property (p_pointers_advance);

// P26. The scheduler completes within its configured rounds -- and the
// rounds must fit Chapter 12.1 Section 12's 28 ns budget.
property p_scheduler_completes;
  @(posedge clk) disable iff (!rst_n)
  start |-> ##[1:ROUNDS] done;
endproperty
a_scheduler_bounded: assert property (p_scheduler_completes);

// P27. One round produces a MAXIMAL matching, not a maximum one, and the
// difference is 36 percentage points.
property p_one_round_is_maximal_only;
  @(posedge clk) disable iff (!rst_n)
  ((ROUNDS == 1) && done) |-> (match_size <= max_possible);
endproperty
a_maximal_not_maximum: assert property (p_one_round_is_maximal_only);

// P28. THE THREE DIAGNOSES ARE MUTUALLY EXCLUSIVE. Discipline,
// scheduler and upstream are fixed in three different places.
property p_diagnoses_exclusive;
  @(posedge clk) disable iff (!rst_n)
  window_valid |-> ($countones({limited_by_discipline, limited_by_scheduler,
                                limited_by_upstream, none_of_the_above}) <= 1);
endproperty
a_diagnoses_exclusive: assert property (p_diagnoses_exclusive);

// P29. v_idle_with_work is OUTSIDE the conformance conjunction. On a
// FIFO switch it is non-zero constantly and the switch is correct.
property p_idle_with_work_not_a_violation;
  @(posedge clk) disable iff (!rst_n)
  ((discipline == QD_FIFO) && (v_idle_with_work != '0)) |-> conformant;
endproperty
a_capacity_not_correctness: assert property (p_idle_with_work_not_a_violation);

// P30. Conformance means the matching is valid and the structure is what
// it claims -- never that the throughput is good.
property p_conformant_definition;
  @(posedge clk) disable iff (!rst_n)
  conformant |-> ((v_double_grant_ing == '0) && (v_double_grant_egr == '0) &&
                  (v_grant_without_work == '0) && (v_hol_in_voq == '0));
endproperty
a_conformant_def: assert property (p_conformant_definition);

// P31. A design claiming VOQs must actually have them -- head-of-line
// blocking observed on a VOQ switch is a structural impossibility.
property p_voq_claim_is_checked;
  @(posedge clk) disable iff (!rst_n)
  ((discipline == QD_VOQ) && head_of_line_possible)
    |=> (v_hol_in_voq > $past(v_hol_in_voq));
endproperty
a_voq_claim_checked: assert property (p_voq_claim_is_checked);