The Forwarding Decision

// -----------------------------------------------------------------------
// fwd_decision_pkg -- shared types for the forwarding decision.
//
// The action encoding is SEVEN-valued on purpose. Section 3 explains why
// a three-valued encoding makes a real failure unobservable.
// -----------------------------------------------------------------------
package fwd_decision_pkg;
 
  typedef enum logic [2:0] {
    A_FORWARD          = 3'd0,  // one egress port
    A_FLOOD            = 3'd1,  // all ports except ingress
    A_FILTER           = 3'd2,  // hit, and the answer is the ingress port
    A_BLOCKED_INGRESS  = 3'd3,  // ingress port not in a forwarding state
    A_BLOCKED_EGRESS   = 3'd4,  // the named egress must not carry this
    A_UNRESOLVED       = 3'd5,  // lookup missed its deadline -- floods, but
                                // is COUNTED separately
    A_INELIGIBLE       = 3'd6   // the frame was never forwardable
  } fwd_action_e;
 
  // A lookup's answer is THREE-valued. HIT and MISS are answers;
  // TIMEOUT is the absence of one, and it is not a miss.
  typedef enum logic [1:0] {
    LK_HIT     = 2'd0,
    LK_MISS    = 2'd1,
    LK_TIMEOUT = 2'd2,
    LK_IDLE    = 2'd3
  } lookup_answer_e;
 
  // 802.1D port states. Two of five permit learning; ONE permits
  // forwarding.
  typedef enum logic [2:0] {
    PS_DISABLED   = 3'd0,
    PS_BLOCKING   = 3'd1,
    PS_LISTENING  = 3'd2,
    PS_LEARNING   = 3'd3,   // learns, does NOT forward
    PS_FORWARDING = 3'd4
  } port_state_e;
 
  localparam int ADDR_W = 48;
 
endpackage

// -----------------------------------------------------------------------
// destination_lookup -- issues the lookup and enforces its deadline.
//
// Chapter 12.1 Section 12 derived the budget: 24 gigabit ports of minimum
// frames need one answer every 28 ns, which is 14 cycles at 500 MHz. This
// module does not make the lookup fast -- Chapter 12.5 does that. It makes
// the deadline VISIBLE, which is the difference between a switch that is
// slow and a switch that is slow and nobody knows.
// -----------------------------------------------------------------------
module destination_lookup
  import fwd_decision_pkg::*;
#(
  parameter int PORT_BITS   = 5,
  parameter int DEADLINE_CY = 14,       // 28 ns at 500 MHz
  parameter int CNT_W       = 32
)(
  input  logic                 clk,
  input  logic                 rst_n,
 
  input  logic                 req_valid,
  input  logic [ADDR_W-1:0]    req_addr,
 
  // To the table -- Chapter 12.2's store.
  output logic                 tbl_req,
  output logic [ADDR_W-1:0]    tbl_addr,
  input  logic                 tbl_ack,
  input  logic                 tbl_hit,
  input  logic [PORT_BITS-1:0] tbl_port,
 
  output logic                 ans_valid,
  output lookup_answer_e       ans,
  output logic [PORT_BITS-1:0] ans_port,
  output logic [3:0]           ans_latency_cy,
 
  output logic [CNT_W-1:0]     c_hit,
  output logic [CNT_W-1:0]     c_miss,
  output logic [CNT_W-1:0]     c_timeout,
  output logic [3:0]           worst_latency_cy,
  output logic                 over_budget
);
 
  logic [3:0] cy_q;
  logic       busy_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      busy_q           <= 1'b0;
      cy_q             <= '0;
      tbl_req          <= 1'b0;
      tbl_addr         <= '0;
      ans_valid        <= 1'b0;
      ans              <= LK_IDLE;
      ans_port         <= '0;
      ans_latency_cy   <= '0;
      c_hit            <= '0;
      c_miss           <= '0;
      c_timeout        <= '0;
      worst_latency_cy <= '0;
      over_budget      <= 1'b0;
    end else begin
      ans_valid <= 1'b0;
      tbl_req   <= 1'b0;
 
      if (!busy_q && req_valid) begin
        busy_q   <= 1'b1;
        cy_q     <= '0;
        tbl_req  <= 1'b1;
        tbl_addr <= req_addr;
      end else if (busy_q) begin
        cy_q <= cy_q + 1'b1;
 
        if (tbl_ack) begin
          busy_q         <= 1'b0;
          ans_valid      <= 1'b1;
          ans            <= tbl_hit ? LK_HIT : LK_MISS;
          ans_port       <= tbl_port;
          ans_latency_cy <= cy_q;
          if (tbl_hit) begin
            if (!(&c_hit))  c_hit  <= c_hit  + 1'b1;
          end else begin
            if (!(&c_miss)) c_miss <= c_miss + 1'b1;
          end
          if (cy_q > worst_latency_cy) worst_latency_cy <= cy_q;
          over_budget <= (cy_q >= 4'(DEADLINE_CY));
 
        end else if (cy_q >= 4'(DEADLINE_CY)) begin
          // THE DEADLINE. Not a failure of the table -- the answer may
          // still arrive. It is a failure to answer IN TIME, and the
          // frame cannot wait: the next one is 672 ns behind.
          busy_q         <= 1'b0;
          ans_valid      <= 1'b1;
          ans            <= LK_TIMEOUT;
          ans_port       <= '0;
          ans_latency_cy <= cy_q;
          if (!(&c_timeout)) c_timeout <= c_timeout + 1'b1;
          over_budget    <= 1'b1;
        end
      end
    end
  end
 
endmodule

// -----------------------------------------------------------------------
// ingress_port_filter -- decides between FORWARD and FILTER on a hit.
//
// A lookup that returns the INGRESS port is a SUCCESS, not a failure. The
// switch knows exactly where the destination is, and knows the frame has
// already been delivered there. The correct action is to emit nothing.
//
// The bug this module exists to prevent: treating "the answer is the
// ingress port" as "no useful answer" and falling back on a flood.
// -----------------------------------------------------------------------
module ingress_port_filter
  import fwd_decision_pkg::*;
#(
  parameter int PORT_BITS = 5,
  parameter int CNT_W     = 32
)(
  input  logic                 clk,
  input  logic                 rst_n,
 
  input  logic                 ans_valid,
  input  lookup_answer_e       ans,
  input  logic [PORT_BITS-1:0] ans_port,
  input  logic [PORT_BITS-1:0] ingress_port,
 
  output logic                 dec_valid,
  output fwd_action_e          dec_action,
  output logic [PORT_BITS-1:0] dec_port,
 
  output logic [CNT_W-1:0]     c_forward,
  output logic [CNT_W-1:0]     c_filter,
  output logic [CNT_W-1:0]     c_flood_miss,
  output logic [CNT_W-1:0]     c_flood_unresolved
);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      dec_valid          <= 1'b0;
      dec_action         <= A_FLOOD;
      dec_port           <= '0;
      c_forward          <= '0;
      c_filter           <= '0;
      c_flood_miss       <= '0;
      c_flood_unresolved <= '0;
    end else begin
      dec_valid <= 1'b0;
 
      if (ans_valid) begin
        dec_valid <= 1'b1;
        dec_port  <= ans_port;
 
        unique case (ans)
          LK_HIT: begin
            if (ans_port == ingress_port) begin
              // THE FILTER. The destination shares a segment with the
              // sender -- a hub, an unmanaged switch, two virtual
              // machines on one host bridge. The frame ALREADY reached
              // it. Emitting anything would duplicate it.
              dec_action <= A_FILTER;
              if (!(&c_filter)) c_filter <= c_filter + 1'b1;
            end else begin
              dec_action <= A_FORWARD;
              if (!(&c_forward)) c_forward <= c_forward + 1'b1;
            end
          end
 
          LK_MISS: begin
            // The switch does not KNOW. Section 2: five reasons, four of
            // which have the station present. Flood.
            dec_action <= A_FLOOD;
            if (!(&c_flood_miss)) c_flood_miss <= c_flood_miss + 1'b1;
          end
 
          LK_TIMEOUT: begin
            // Same egress behaviour as a miss, DIFFERENT action code.
            // Section 3: collapsing these makes an over-budget lookup
            // engine indistinguishable from a network of unknown
            // stations.
            dec_action <= A_UNRESOLVED;
            if (!(&c_flood_unresolved))
              c_flood_unresolved <= c_flood_unresolved + 1'b1;
          end
 
          default: begin
            dec_valid  <= 1'b0;
            dec_action <= A_FLOOD;
          end
        endcase
      end
    end
  end
 
endmodule

// -----------------------------------------------------------------------
// port_state_gate -- applies 802.1D port state to both ends of a decision.
//
// Five states. TWO permit learning; ONE permits forwarding. The gate is
// asymmetric on purpose: a port in LEARNING contributes evidence to
// Chapter 12.2's table while carrying no traffic, which is what makes a
// state transition safe rather than disruptive.
// -----------------------------------------------------------------------
module port_state_gate
  import fwd_decision_pkg::*;
#(
  parameter int N_PORTS   = 24,
  parameter int PORT_BITS = 5,
  parameter int CNT_W     = 32
)(
  input  logic                 clk,
  input  logic                 rst_n,
 
  input  port_state_e          state [N_PORTS],
 
  input  logic                 dec_valid,
  input  fwd_action_e          dec_action,
  input  logic [PORT_BITS-1:0] dec_port,
  input  logic [PORT_BITS-1:0] ingress_port,
 
  output logic                 gated_valid,
  output fwd_action_e          gated_action,
  output logic [PORT_BITS-1:0] gated_port,
  output logic [N_PORTS-1:0]   forwarding_mask,   // ports that may transmit
  output logic                 may_learn,         // for Chapter 12.2
 
  output logic [CNT_W-1:0]     c_blocked_ingress,
  output logic [CNT_W-1:0]     c_blocked_egress
);
 
  // ONE state forwards. Two learn. The asymmetry is the whole point of
  // having five states rather than two.
  function automatic logic can_forward(input port_state_e s);
    can_forward = (s == PS_FORWARDING);
  endfunction
 
  function automatic logic can_learn(input port_state_e s);
    can_learn = (s == PS_LEARNING) || (s == PS_FORWARDING);
  endfunction
 
  always_comb begin
    for (int p = 0; p < N_PORTS; p++)
      forwarding_mask[p] = can_forward(state[p]);
  end
 
  assign may_learn = can_learn(state[ingress_port]);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      gated_valid       <= 1'b0;
      gated_action      <= A_FLOOD;
      gated_port        <= '0;
      c_blocked_ingress <= '0;
      c_blocked_egress  <= '0;
    end else begin
      gated_valid  <= 1'b0;
      gated_port   <= dec_port;
      gated_action <= dec_action;
 
      if (dec_valid) begin
        gated_valid <= 1'b1;
 
        // GATE 2 -- the ingress end. A frame arriving on a port that is
        // not forwarding is not forwarded ANYWHERE, whatever the table
        // says. Note that it may still be LEARNED from: a port in
        // LEARNING exists precisely to populate the table before it
        // starts carrying traffic.
        if (!can_forward(state[ingress_port])) begin
          gated_action <= A_BLOCKED_INGRESS;
          if (!(&c_blocked_ingress))
            c_blocked_ingress <= c_blocked_ingress + 1'b1;
 
        // GATE 5 -- the egress end, for a unicast forward. The table's
        // answer is correct and the port still must not carry it.
        end else if ((dec_action == A_FORWARD) &&
                     !can_forward(state[dec_port])) begin
          gated_action <= A_BLOCKED_EGRESS;
          if (!(&c_blocked_egress))
            c_blocked_egress <= c_blocked_egress + 1'b1;
        end
        // A FLOOD is NOT blocked here -- it is REDUCED. Section 9's mask
        // builder intersects the flood with forwarding_mask, so a flood
        // reaches every port that may carry it and no others.
      end
    end
  end
 
endmodule

// -----------------------------------------------------------------------
// egress_mask_builder -- action plus port states to a set of egress ports.
//
// Every action maps to a mask. The two that are easy to get wrong:
//   FLOOD  -- all forwarding ports EXCEPT the ingress. Both conditions,
//             not either.
//   FILTER -- the empty mask, which must be reached deliberately rather
//             than by a flood that happens to exclude everything.
// -----------------------------------------------------------------------
module egress_mask_builder
  import fwd_decision_pkg::*;
#(
  parameter int N_PORTS   = 24,
  parameter int PORT_BITS = 5
)(
  input  logic                 clk,
  input  logic                 rst_n,
 
  input  logic                 gated_valid,
  input  fwd_action_e          gated_action,
  input  logic [PORT_BITS-1:0] gated_port,
  input  logic [PORT_BITS-1:0] ingress_port,
  input  logic [N_PORTS-1:0]   forwarding_mask,
 
  output logic                 mask_valid,
  output logic [N_PORTS-1:0]   egress_mask,
  output fwd_action_e          mask_action,
  output logic                 flood_reduced   // some ports excluded by state
);
 
  logic [N_PORTS-1:0] all_but_ingress;
  logic [N_PORTS-1:0] full_flood;
 
  assign all_but_ingress = ~(N_PORTS'(1) << ingress_port);
  // BOTH conditions. A flood goes to every port that MAY forward AND is
  // not the ingress port -- not to every port that may forward, and not
  // to every port except the ingress.
  assign full_flood      = forwarding_mask & all_but_ingress;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      mask_valid    <= 1'b0;
      egress_mask   <= '0;
      mask_action   <= A_FILTER;
      flood_reduced <= 1'b0;
    end else begin
      mask_valid    <= 1'b0;
      flood_reduced <= 1'b0;
 
      if (gated_valid) begin
        mask_valid  <= 1'b1;
        mask_action <= gated_action;
 
        unique case (gated_action)
          A_FORWARD: begin
            egress_mask <= (N_PORTS'(1) << gated_port);
          end
 
          // A miss and an unresolved lookup produce the SAME mask and
          // are still distinct actions -- Section 3.
          A_FLOOD, A_UNRESOLVED: begin
            egress_mask   <= full_flood;
            flood_reduced <= (full_flood != all_but_ingress);
          end
 
          // Every remaining action emits nothing, and each is reached by
          // its own branch so that no case falls through to a default
          // that floods.
          A_FILTER,
          A_BLOCKED_INGRESS,
          A_BLOCKED_EGRESS,
          A_INELIGIBLE: begin
            egress_mask <= '0;
          end
 
          default: begin
            // Unreachable by construction. It emits NOTHING rather than
            // flooding, because a default that floods turns an encoding
            // error into a domain-wide broadcast.
            egress_mask <= '0;
            mask_valid  <= 1'b0;
          end
        endcase
      end
    end
  end
 
endmodule

// -----------------------------------------------------------------------
// decision_composer -- runs the gates in order and records WHICH one
// decided.
//
// The ordering matters and is not arbitrary: cheap and absolute checks
// first, expensive and conditional ones last. A frame rejected by gate 1
// never consumes a lookup slot, which matters when the lookup engine is
// the bottleneck -- Chapter 12.1 Section 12.
// -----------------------------------------------------------------------
module decision_composer
  import fwd_decision_pkg::*;
#(
  parameter int N_PORTS   = 24,
  parameter int PORT_BITS = 5,
  parameter int CNT_W     = 32
)(
  input  logic                 clk,
  input  logic                 rst_n,
 
  input  logic                 frame_valid,
  input  logic                 frame_eligible,     // gate 1
  input  logic                 ingress_forwarding, // gate 2
  input  logic                 dst_is_group,
  input  logic                 ans_valid,          // gate 3
  input  lookup_answer_e       ans,
  input  logic [PORT_BITS-1:0] ans_port,
  input  logic [PORT_BITS-1:0] ingress_port,
  input  logic                 egress_forwarding,  // gate 5
  input  logic                 egress_has_room,    // gate 6
 
  output logic                 out_valid,
  output fwd_action_e          out_action,
  output logic [PORT_BITS-1:0] out_port,
  output logic [2:0]           deciding_gate,      // 1..6, 0 = permitted
  output logic                 lookup_needed,
 
  output logic [CNT_W-1:0]     by_gate [7]
);
 
  // Gate 3 is skipped entirely for a group destination -- Chapter 12.1
  // Section 8 established that broadcast and multicast have a known
  // answer, so consulting the table wastes a lookup slot the engine is
  // short of.
  assign lookup_needed = frame_valid && frame_eligible &&
                         ingress_forwarding && !dst_is_group;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      out_valid     <= 1'b0;
      out_action    <= A_INELIGIBLE;
      out_port      <= '0;
      deciding_gate <= 3'd0;
      for (int g = 0; g < 7; g++) by_gate[g] <= '0;
    end else begin
      out_valid <= 1'b0;
      out_port  <= ans_port;
 
      if (frame_valid) begin
        out_valid <= 1'b1;
 
        // GATE 1 -- eligibility. Cheapest, most absolute, first.
        if (!frame_eligible) begin
          out_action    <= A_INELIGIBLE;
          deciding_gate <= 3'd1;
          by_gate[1]    <= by_gate[1] + 1'b1;
 
        // GATE 2 -- ingress port state.
        end else if (!ingress_forwarding) begin
          out_action    <= A_BLOCKED_INGRESS;
          deciding_gate <= 3'd2;
          by_gate[2]    <= by_gate[2] + 1'b1;
 
        // A group destination bypasses gate 3 and gate 4 entirely.
        end else if (dst_is_group) begin
          out_action    <= A_FLOOD;
          deciding_gate <= 3'd0;
          by_gate[0]    <= by_gate[0] + 1'b1;
 
        // GATE 3 -- the lookup's three-valued answer.
        end else if (ans_valid && (ans == LK_TIMEOUT)) begin
          out_action    <= A_UNRESOLVED;
          deciding_gate <= 3'd3;
          by_gate[3]    <= by_gate[3] + 1'b1;
 
        end else if (ans_valid && (ans == LK_MISS)) begin
          out_action    <= A_FLOOD;
          deciding_gate <= 3'd0;
          by_gate[0]    <= by_gate[0] + 1'b1;
 
        // GATE 4 -- the ingress filter.
        end else if (ans_valid && (ans_port == ingress_port)) begin
          out_action    <= A_FILTER;
          deciding_gate <= 3'd4;
          by_gate[4]    <= by_gate[4] + 1'b1;
 
        // GATE 5 -- egress port state.
        end else if (!egress_forwarding) begin
          out_action    <= A_BLOCKED_EGRESS;
          deciding_gate <= 3'd5;
          by_gate[5]    <= by_gate[5] + 1'b1;
 
        // GATE 6 -- admission. Chapter 12.1 Section 9 owns the policy;
        // this is only where it sits in the order.
        end else if (!egress_has_room) begin
          out_action    <= A_FORWARD;     // the decision was to forward
          deciding_gate <= 3'd6;          // and the queue refused it
          by_gate[6]    <= by_gate[6] + 1'b1;
 
        end else begin
          out_action    <= A_FORWARD;
          deciding_gate <= 3'd0;
          by_gate[0]    <= by_gate[0] + 1'b1;
        end
      end
    end
  end
 
endmodule

// -----------------------------------------------------------------------
// ordering_guard -- prevents a variable-latency decision path from
// reordering frames between the same source and destination.
//
// The hazard: frame 1 misses (14 cycles), frame 2 from the same source to
// the same destination hits (4 cycles). Frame 2's decision completes 10
// cycles -- 20 ns at 500 MHz -- before frame 1's. Without this guard, the
// second frame reaches the wire first.
//
// Ethernet has no sequence number and no reassembly. A receiver cannot
// detect or correct a reorder; it simply hands the frames up in the wrong
// order, and every protocol above assumes it did not.
// -----------------------------------------------------------------------
module ordering_guard
  import fwd_decision_pkg::*;
#(
  parameter int DEPTH  = 8,
  parameter int TAG_W  = 3,
  parameter int CNT_W  = 32
)(
  input  logic             clk,
  input  logic             rst_n,
 
  // Issue side -- one tag per frame entering the decision pipeline.
  input  logic             issue_valid,
  output logic [TAG_W-1:0] issue_tag,
  output logic             issue_ready,
 
  // Completion side -- decisions may complete OUT OF ORDER.
  input  logic             done_valid,
  input  logic [TAG_W-1:0] done_tag,
 
  // Release side -- strictly IN ORDER.
  output logic             release_valid,
  output logic [TAG_W-1:0] release_tag,
 
  output logic [CNT_W-1:0] c_held,          // completed early, waited
  output logic [3:0]       max_hold_depth,
  output logic [CNT_W-1:0] c_released
);
 
  logic [DEPTH-1:0]   done_q;
  logic [TAG_W-1:0]   head_q, tail_q;
  logic [TAG_W:0]     count_q;
 
  assign issue_ready = (count_q < (TAG_W+1)'(DEPTH));
  assign issue_tag   = tail_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      done_q         <= '0;
      head_q         <= '0;
      tail_q         <= '0;
      count_q        <= '0;
      release_valid  <= 1'b0;
      release_tag    <= '0;
      c_held         <= '0;
      c_released     <= '0;
      max_hold_depth <= '0;
    end else begin
      release_valid <= 1'b0;
 
      if (issue_valid && issue_ready) begin
        done_q[tail_q] <= 1'b0;
        tail_q         <= tail_q + 1'b1;
        count_q        <= count_q + 1'b1;
      end
 
      if (done_valid) begin
        done_q[done_tag] <= 1'b1;
        // A completion that is NOT at the head has finished early and
        // must wait. Counting these measures how much reordering the
        // decision path is actually producing.
        if (done_tag != head_q)
          if (!(&c_held)) c_held <= c_held + 1'b1;
      end
 
      // Release strictly in issue order, one per cycle.
      if ((count_q != '0) && done_q[head_q]) begin
        release_valid  <= 1'b1;
        release_tag    <= head_q;
        done_q[head_q] <= 1'b0;
        head_q         <= head_q + 1'b1;
        count_q        <= count_q - 1'b1;
        if (!(&c_released)) c_released <= c_released + 1'b1;
      end
 
      if (count_q[3:0] > max_hold_depth) max_hold_depth <= count_q[3:0];
    end
  end
 
endmodule

// -----------------------------------------------------------------------
// forwarding_telemetry -- a histogram over deciding_gate, plus the derived
// ratios that make it readable.
//
// Seven counters. Their SHAPE, not their absolute values, is what tells an
// operator whether the switch is healthy.
// -----------------------------------------------------------------------
module forwarding_telemetry
  import fwd_decision_pkg::*;
#(
  parameter int N_PORTS   = 24,
  parameter int PORT_BITS = 5,
  parameter int CNT_W     = 32,
  parameter int WINDOW    = 1_000_000
)(
  input  logic                 clk,
  input  logic                 rst_n,
 
  input  logic                 out_valid,
  input  fwd_action_e          out_action,
  input  logic [2:0]           deciding_gate,
  input  logic [PORT_BITS-1:0] ingress_port,
 
  output logic [CNT_W-1:0]     c_action  [7],
  output logic [CNT_W-1:0]     c_gate    [7],
  output logic [CNT_W-1:0]     filter_by_port [N_PORTS],
 
  output logic                 window_valid,
  output logic                 flood_dominant,      // acting like a hub
  output logic                 timeout_present,     // lookup over budget
  output logic                 blocked_significant, // stale table or config
  output logic [2:0]           top_gate
);
 
  logic [CNT_W-1:0] win_total;
  logic [CNT_W-1:0] win_gate [7];
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (int i = 0; i < 7; i++) begin
        c_action[i] <= '0; c_gate[i] <= '0; win_gate[i] <= '0;
      end
      for (int p = 0; p < N_PORTS; p++) filter_by_port[p] <= '0;
      win_total           <= '0;
      window_valid        <= 1'b0;
      flood_dominant      <= 1'b0;
      timeout_present     <= 1'b0;
      blocked_significant <= 1'b0;
      top_gate            <= 3'd0;
    end else begin
      window_valid <= 1'b0;
 
      if (out_valid) begin
        c_action[out_action[2:0]] <= c_action[out_action[2:0]] + 1'b1;
        c_gate[deciding_gate]     <= c_gate[deciding_gate]     + 1'b1;
        win_gate[deciding_gate]   <= win_gate[deciding_gate]   + 1'b1;
        win_total                 <= win_total + 1'b1;
 
        // Filtering is a PER-PORT property: it fires only on ports with a
        // shared segment behind them, so the distribution across ports is
        // the useful form, not the total.
        if (out_action == A_FILTER)
          filter_by_port[ingress_port] <= filter_by_port[ingress_port] + 1'b1;
      end
 
      if (win_total >= CNT_W'(WINDOW)) begin
        automatic logic [CNT_W-1:0] hi = '0;
        automatic logic [2:0]       hg = 3'd0;
        for (int g = 0; g < 7; g++)
          if (win_gate[g] > hi) begin hi = win_gate[g]; hg = 3'(g); end
        top_gate <= hg;
 
        // Floods above a quarter of all decisions is hub-like behaviour.
        flood_dominant <=
          ((c_action[A_FLOOD] + c_action[A_UNRESOLVED]) > (win_total >> 2));
 
        // ANY timeout is a finding. This is not a rate threshold.
        timeout_present <= (win_gate[3] != '0);
 
        // Blocked frames above a thousandth means a table entry names a
        // port that is not forwarding, persistently.
        blocked_significant <=
          ((win_gate[2] + win_gate[5]) > (win_total >> 10));
 
        for (int g = 0; g < 7; g++) win_gate[g] <= '0;
        win_total    <= '0;
        window_valid <= 1'b1;
      end
    end
  end
 
endmodule

// -----------------------------------------------------------------------
// forwarding_conformance_monitor -- checks the decision against its inputs.
//
// The central check is EXHAUSTIVENESS: every frame that entered the
// decision left it through exactly one gate, and the gate accounts sum to
// the frame count. A missing frame means a path exists that nobody
// enumerated -- which is Section 16's rejected property, made observable.
// -----------------------------------------------------------------------
module forwarding_conformance_monitor
  import fwd_decision_pkg::*;
#(
  parameter int N_PORTS   = 24,
  parameter int PORT_BITS = 5,
  parameter int CNT_W     = 32
)(
  input  logic                 clk,
  input  logic                 rst_n,
 
  input  logic                 frame_in,           // entered the decision
  input  logic                 out_valid,
  input  fwd_action_e          out_action,
  input  logic [2:0]           deciding_gate,
  input  logic [N_PORTS-1:0]   egress_mask,
  input  logic [PORT_BITS-1:0] ingress_port,
  input  logic [N_PORTS-1:0]   forwarding_mask,
 
  output logic [CNT_W-1:0]     v_unaccounted,      // in, never out
  output logic [CNT_W-1:0]     v_ingress_echo,     // egress includes ingress
  output logic [CNT_W-1:0]     v_blocked_egress,   // egress not forwarding
  output logic [CNT_W-1:0]     v_mask_mismatch,    // mask disagrees w/ action
  output logic [CNT_W-1:0]     v_gate_unknown,     // gate outside 0..6
  output logic                 conformant
);
 
  logic [CNT_W-1:0] n_in, n_out;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      n_in <= '0; n_out <= '0;
      v_unaccounted    <= '0;
      v_ingress_echo   <= '0;
      v_blocked_egress <= '0;
      v_mask_mismatch  <= '0;
      v_gate_unknown   <= '0;
    end else begin
      if (frame_in)  n_in  <= n_in  + 1'b1;
      if (out_valid) n_out <= n_out + 1'b1;
 
      // EXHAUSTIVENESS. Every frame that entered produced a decision.
      // A frame that entered and never left took a path the enumeration
      // does not contain.
      if (n_in > (n_out + CNT_W'(16)))
        if (!(&v_unaccounted)) v_unaccounted <= v_unaccounted + 1'b1;
 
      if (out_valid) begin
        // THE ABSOLUTE INVARIANT -- Chapter 12.1's P9, restated at the
        // point where the mask is built rather than where it is used.
        if (egress_mask[ingress_port])
          if (!(&v_ingress_echo)) v_ingress_echo <= v_ingress_echo + 1'b1;
 
        // No frame reaches a port that may not forward.
        if ((egress_mask & ~forwarding_mask) != '0)
          if (!(&v_blocked_egress)) v_blocked_egress <= v_blocked_egress + 1'b1;
 
        // The mask must match what the action claims.
        unique case (out_action)
          A_FORWARD:
            if (deciding_gate == 3'd0 && $countones(egress_mask) != 1)
              if (!(&v_mask_mismatch)) v_mask_mismatch <= v_mask_mismatch + 1'b1;
          A_FLOOD, A_UNRESOLVED:
            if (egress_mask == '0)
              if (!(&v_mask_mismatch)) v_mask_mismatch <= v_mask_mismatch + 1'b1;
          A_FILTER, A_BLOCKED_INGRESS, A_BLOCKED_EGRESS, A_INELIGIBLE:
            if (egress_mask != '0)
              if (!(&v_mask_mismatch)) v_mask_mismatch <= v_mask_mismatch + 1'b1;
          default:
            if (!(&v_mask_mismatch)) v_mask_mismatch <= v_mask_mismatch + 1'b1;
        endcase
 
        // A gate value outside the enumerated range means the composer
        // took a branch that was not written down.
        if (deciding_gate > 3'd6)
          if (!(&v_gate_unknown)) v_gate_unknown <= v_gate_unknown + 1'b1;
      end
    end
  end
 
  assign conformant = (v_unaccounted    == '0) &&
                      (v_ingress_echo   == '0) &&
                      (v_blocked_egress == '0) &&
                      (v_mask_mismatch  == '0) &&
                      (v_gate_unknown   == '0);
 
endmodule

// P1. A lookup answers within the deadline OR reports that it did not.
// It never simply fails to answer.
property p_lookup_always_answers;
  @(posedge clk) disable iff (!rst_n)
  tbl_req |-> ##[1:DEADLINE_CY] ans_valid;
endproperty
a_lookup_answers: assert property (p_lookup_always_answers);
 
// P2. A timeout is reported as a TIMEOUT, never as a miss. One encoding
// value separates a network problem from a design problem.
property p_timeout_not_a_miss;
  @(posedge clk) disable iff (!rst_n)
  (ans_valid && (ans_latency_cy >= 4'(DEADLINE_CY)) && !tbl_ack)
    |-> (ans == LK_TIMEOUT);
endproperty
a_timeout_distinct: assert property (p_timeout_not_a_miss);
 
// P3. A hit reports a port; a miss and a timeout do not pretend to.
property p_miss_has_no_port;
  @(posedge clk) disable iff (!rst_n)
  (ans_valid && (ans != LK_HIT)) |-> (ans_port == '0);
endproperty
a_no_phantom_port: assert property (p_miss_has_no_port);
 
// P4. The worst-case latency is retained, not averaged away.
property p_worst_latency_monotonic;
  @(posedge clk) disable iff (!rst_n)
  $stable(rst_n) |-> (worst_latency_cy >= $past(worst_latency_cy));
endproperty
a_worst_retained: assert property (p_worst_latency_monotonic);
 
// P5. A group destination consumes NO lookup slot -- Section 11's
// throughput lever.
property p_group_skips_lookup;
  @(posedge clk) disable iff (!rst_n)
  (frame_valid && dst_is_group) |-> !lookup_needed;
endproperty
a_group_no_lookup: assert property (p_group_skips_lookup);

// P6. THE FILTER. A hit whose port equals the ingress port produces
// A_FILTER -- never a flood, never a forward.
property p_hit_on_ingress_filters;
  @(posedge clk) disable iff (!rst_n)
  (ans_valid && (ans == LK_HIT) && (ans_port == ingress_port))
    |=> (dec_action == A_FILTER);
endproperty
a_filter_on_self: assert property (p_hit_on_ingress_filters);
 
// P7. A filter emits NOTHING. The empty mask is reached deliberately.
property p_filter_empty_mask;
  @(posedge clk) disable iff (!rst_n)
  (mask_valid && (mask_action == A_FILTER)) |-> (egress_mask == '0);
endproperty
a_filter_no_egress: assert property (p_filter_empty_mask);
 
// P8. A hit on ANOTHER port forwards to exactly one port.
property p_hit_elsewhere_forwards_one;
  @(posedge clk) disable iff (!rst_n)
  (mask_valid && (mask_action == A_FORWARD)) |-> $onehot(egress_mask);
endproperty
a_forward_one_port: assert property (p_hit_elsewhere_forwards_one);
 
// P9. A filter is NOT counted as a miss, and a miss is NOT counted as a
// filter. They are opposite conclusions from opposite evidence.
property p_filter_and_miss_distinct;
  @(posedge clk) disable iff (!rst_n)
  (dec_valid && (dec_action == A_FILTER)) |-> $stable(c_flood_miss);
endproperty
a_filter_not_miss: assert property (p_filter_and_miss_distinct);

// P10. NEVER out the ingress port -- Chapter 12.1's P9, re-asserted at
// the point the mask is built.
property p_never_egress_on_ingress;
  @(posedge clk) disable iff (!rst_n)
  mask_valid |-> !egress_mask[ingress_port];
endproperty
a_no_ingress_echo: assert property (p_never_egress_on_ingress);
 
// P11. NEVER to a port that may not forward, whatever the table says.
property p_never_to_blocked_port;
  @(posedge clk) disable iff (!rst_n)
  mask_valid |-> ((egress_mask & ~forwarding_mask) == '0);
endproperty
a_no_blocked_egress: assert property (p_never_to_blocked_port);
 
// P12. A flood is the INTERSECTION of both conditions, not either.
property p_flood_is_intersection;
  @(posedge clk) disable iff (!rst_n)
  (mask_valid && (mask_action inside {A_FLOOD, A_UNRESOLVED}))
    |-> (egress_mask == (forwarding_mask & ~(N_PORTS'(1) << ingress_port)));
endproperty
a_flood_intersection: assert property (p_flood_is_intersection);
 
// P13. Every non-emitting action produces an EMPTY mask -- no partial
// emission from an action that decided to emit nothing.
property p_non_emitting_actions_empty;
  @(posedge clk) disable iff (!rst_n)
  (mask_valid && (mask_action inside {A_FILTER, A_BLOCKED_INGRESS,
                                      A_BLOCKED_EGRESS, A_INELIGIBLE}))
    |-> (egress_mask == '0);
endproperty
a_non_emitting_empty: assert property (p_non_emitting_actions_empty);

// P14. Gate 1 precedes everything. An ineligible frame consumes no
// lookup slot.
property p_ineligible_no_lookup;
  @(posedge clk) disable iff (!rst_n)
  (frame_valid && !frame_eligible) |-> !lookup_needed;
endproperty
a_ineligible_no_lookup: assert property (p_ineligible_no_lookup);
 
// P15. Gate 2 precedes the lookup for the same reason.
property p_blocked_ingress_no_lookup;
  @(posedge clk) disable iff (!rst_n)
  (frame_valid && !ingress_forwarding) |-> !lookup_needed;
endproperty
a_blocked_no_lookup: assert property (p_blocked_ingress_no_lookup);
 
// P16. Exactly ONE gate is credited per decision.
property p_one_gate_per_decision;
  @(posedge clk) disable iff (!rst_n)
  out_valid |-> (deciding_gate <= 3'd6);
endproperty
a_gate_in_range: assert property (p_one_gate_per_decision);
 
// P17. Gate 6 does not change the ACTION. The decision was to forward;
// the resource refused it, and both facts survive.
property p_admission_preserves_action;
  @(posedge clk) disable iff (!rst_n)
  (out_valid && (deciding_gate == 3'd6)) |-> (out_action == A_FORWARD);
endproperty
a_gate6_action: assert property (p_admission_preserves_action);
 
// P18. A frame blocked at the ingress may STILL be learned from -- gates
// on forwarding and gates on learning are independent.
property p_blocked_ingress_may_learn;
  @(posedge clk) disable iff (!rst_n)
  (ingress_state == PS_LEARNING) |-> (may_learn && !ingress_forwarding);
endproperty
a_learning_state: assert property (p_blocked_ingress_may_learn);

// P19. Frames are RELEASED in issue order, whatever order they complete
// in. Ethernet carries no sequence number, so a reorder is undetectable
// and therefore forbidden.
property p_release_in_order;
  @(posedge clk) disable iff (!rst_n)
  release_valid |=> (release_tag != $past(release_tag));
endproperty
a_in_order_release: assert property (p_release_in_order);
 
// P20. A completion out of order is HELD, not dropped.
property p_early_completion_held;
  @(posedge clk) disable iff (!rst_n)
  (done_valid && (done_tag != head_q)) |-> ##[1:DEPTH] release_valid;
endproperty
a_early_held: assert property (p_early_completion_held);
 
// P21. The reordering the guard prevented is COUNTED. A c_held of zero
// on a pipelined lookup means the guard is not wired up.
property p_held_counted;
  @(posedge clk) disable iff (!rst_n)
  (done_valid && (done_tag != head_q)) |=> (c_held > $past(c_held));
endproperty
a_held_counted: assert property (p_held_counted);

// P22. THE EXHAUSTIVENESS PROPERTY. Every frame that entered the
// decision produced a decision. This is the constructive replacement for
// the rejected property below: it catches an unenumerated path without
// naming it.
property p_every_frame_decided;
  @(posedge clk) disable iff (!rst_n)
  frame_in |-> ##[1:MAX_DECISION_CY] out_valid;
endproperty
a_all_frames_decided: assert property (p_every_frame_decided);
 
// P23. The gate histogram sums to the decision count. A shortfall means
// a decision was reached by a path with no gate credited to it.
property p_gate_accounts_balance;
  @(posedge clk) disable iff (!rst_n)
  window_valid |-> ((c_gate[0] + c_gate[1] + c_gate[2] + c_gate[3] +
                     c_gate[4] + c_gate[5] + c_gate[6]) == n_out);
endproperty
a_gates_balance: assert property (p_gate_accounts_balance);
 
// P24. The mask agrees with the action -- the two halves of the decision
// are cross-checked against each other.
property p_mask_matches_action;
  @(posedge clk) disable iff (!rst_n)
  out_valid |-> (v_mask_mismatch == $past(v_mask_mismatch));
endproperty
a_mask_action_agree: assert property (p_mask_matches_action);
 
// P25. ANY timeout is reported. Not a rate -- a presence bit, because a
// design that misses its deadline once misses it.
property p_timeout_presence_reported;
  @(posedge clk) disable iff (!rst_n)
  (window_valid && (c_gate[3] != '0)) |-> timeout_present;
endproperty
a_timeout_reported: assert property (p_timeout_presence_reported);
 
// P26. Filtering is attributed to a PORT. The distribution across ports
// is the useful form; the total says nothing.
property p_filter_attributed_to_port;
  @(posedge clk) disable iff (!rst_n)
  (out_valid && (out_action == A_FILTER))
    |=> (filter_by_port[$past(ingress_port)] >
         $past(filter_by_port[$past(ingress_port)]));
endproperty
a_filter_by_port: assert property (p_filter_attributed_to_port);
 
// P27. Conformance means the decision followed from its inputs -- never
// that the frame was delivered, and never that the table was right.
property p_conformant_definition;
  @(posedge clk) disable iff (!rst_n)
  conformant |-> ((v_unaccounted == '0) && (v_ingress_echo == '0) &&
                  (v_blocked_egress == '0) && (v_mask_mismatch == '0) &&
                  (v_gate_unknown == '0));
endproperty
a_conformant_def: assert property (p_conformant_definition);