VLAN Processing in the Switch Datapath

// -----------------------------------------------------------------------
// vlanidx_pkg -- shared types for the VLAN datapath.
//
// The distinction this package exists to enforce: vid_t is the identity
// and goes in the KEY; vidx_t is a subscript and goes in the ARRAYS. They
// are different types on purpose, because the only thing standing between
// an indexed design and two merged VLANs is not confusing them.
// -----------------------------------------------------------------------
package vlanidx_pkg;

  localparam int VID_W    = 12;      // the identity -- 4094 usable
  localparam int VIDX_W   = 8;       // the subscript -- 256 configured
  localparam int ADDR_W   = 48;
  localparam int KEY_W    = VID_W + ADDR_W;   // 60 -- Chapter 13.1 Section 7
  localparam int PCP_W    = 3;
  localparam int N_QUEUES = 4;
  localparam int QSEL_W   = 2;

  typedef logic [VID_W-1:0]  vid_t;
  typedef logic [VIDX_W-1:0] vidx_t;

  // Why a VID could not be translated. The first is a configuration
  // state; the second is the failure this chapter is about.
  typedef enum logic [1:0] {
    MR_OK          = 2'd0,
    MR_UNCONFIGURED = 2'd1,  // this VID has no index -- the VLAN does not exist here
    MR_ALIASED      = 2'd2,  // two VIDs share this index -- Section 5
    MR_RESERVED     = 2'd3   // 0 or 4095
  } map_result_e;

  // Scheduling discipline for Section 11. Strict priority is the default
  // and it is the one that starves.
  typedef enum logic [1:0] {
    SCHED_STRICT   = 2'd0,
    SCHED_WEIGHTED = 2'd1,
    SCHED_ROUND    = 2'd2
  } sched_mode_e;

endpackage

// -----------------------------------------------------------------------
// vid_index_map -- 12 bits to a compact subscript.
//
// A PROGRAMMED TRANSLATION TABLE, not a hash. It stores no key to compare
// against, so a collision is undetectable at lookup time and must be
// prevented at programming time -- which is what Section 5 exists for.
// -----------------------------------------------------------------------
module vid_index_map
  import vlanidx_pkg::*;
#(
  parameter int N_VIDS   = 4096,
  parameter int N_VLANS  = 256,
  parameter int CNT_W    = 32
)(
  input  logic             clk,
  input  logic             rst_n,

  // Configuration: bind one VID to one index.
  input  logic             cfg_valid,
  input  vid_t             cfg_vid,
  input  vidx_t            cfg_vidx,
  input  logic             cfg_present,

  // Per-frame translation.
  input  logic             lk_valid,
  input  vid_t             lk_vid,

  output logic             idx_valid,
  output vidx_t            idx,
  output map_result_e      result,

  output logic [CNT_W-1:0] c_translated,
  output logic [CNT_W-1:0] c_unconfigured,
  output logic [11:0]      n_vids_bound,
  output logic [CNT_W-1:0] map_bits
);

  vidx_t              tbl_idx     [N_VIDS];
  logic               tbl_present [N_VIDS];

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (int v = 0; v < N_VIDS; v++) begin
        tbl_idx[v]     <= '0;
        tbl_present[v] <= 1'b0;
      end
    end else if (cfg_valid) begin
      tbl_idx[cfg_vid]     <= cfg_vidx;
      tbl_present[cfg_vid] <= cfg_present;
    end
  end

  logic vid_reserved;
  assign vid_reserved = (lk_vid == 12'd0) || (lk_vid == 12'd4095);

  always_comb begin
    idx_valid = 1'b0;
    idx       = '0;
    result    = MR_OK;

    if (lk_valid) begin
      if (vid_reserved) begin
        result = MR_RESERVED;
      end else if (!tbl_present[lk_vid]) begin
        // The VID is legal and this switch has no VLAN for it. Distinct
        // from an aliasing failure: nothing is merged, the frame simply
        // has nowhere to go.
        result = MR_UNCONFIGURED;
      end else begin
        idx_valid = 1'b1;
        idx       = tbl_idx[lk_vid];
      end
    end
  end

  // NOTE WHAT IS ABSENT. There is no stored VID to compare the lookup
  // against, because the index IS the answer. Chapter 12.5's hashed table
  // stores the full key and compares it on every lookup; this cannot,
  // and that is the difference between a detectable collision and an
  // undetectable one.

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      c_translated   <= '0;
      c_unconfigured <= '0;
    end else if (lk_valid) begin
      if (idx_valid) begin
        c_translated <= c_translated + 1'b1;
      end else if (result == MR_UNCONFIGURED) begin
        if (!(&c_unconfigured)) c_unconfigured <= c_unconfigured + 1'b1;
      end
    end
  end

  always_comb begin
    n_vids_bound = 12'd0;
    for (int v = 0; v < N_VIDS; v++)
      if (tbl_present[v]) n_vids_bound = n_vids_bound + 12'd1;
  end

  assign map_bits = CNT_W'(N_VIDS) * CNT_W'(VIDX_W + 1);

endmodule

// -----------------------------------------------------------------------
// vid_alias_checker -- refuses a binding that would give two VIDs one
// index.
//
// The map stores no key to compare at lookup time, so the only place a
// collision can be caught is at the write. This module keeps the reverse
// direction -- which VID owns each index -- and refuses a second claimant.
// -----------------------------------------------------------------------
module vid_alias_checker
  import vlanidx_pkg::*;
#(
  parameter int N_VLANS = 256,
  parameter int CNT_W   = 32
)(
  input  logic             clk,
  input  logic             rst_n,

  input  logic             cfg_valid,
  input  vid_t             cfg_vid,
  input  vidx_t            cfg_vidx,
  input  logic             cfg_present,

  output logic             cfg_accept,
  output map_result_e      cfg_result,
  output vid_t             conflicting_vid,

  output logic [CNT_W-1:0] c_bindings,
  output logic [CNT_W-1:0] c_alias_refused,
  output logic [11:0]      indices_used,
  output logic             map_is_injective
);

  // THE REVERSE MAP. One VID per index, which is the property the forward
  // map cannot express. 256 entries of 13 bits is 416 octets -- against
  // the 4.5 KiB forward map, a rounding error.
  vid_t owner     [N_VLANS];
  logic owner_val [N_VLANS];

  always_comb begin
    cfg_accept      = 1'b0;
    cfg_result      = MR_OK;
    conflicting_vid = '0;

    if (cfg_valid) begin
      if ((cfg_vid == 12'd0) || (cfg_vid == 12'd4095)) begin
        cfg_result = MR_RESERVED;
      end else if (!cfg_present) begin
        // Unbinding is always permitted.
        cfg_accept = 1'b1;
      end else if (owner_val[cfg_vidx] && (owner[cfg_vidx] != cfg_vid)) begin
        // THE REFUSAL. This index already belongs to a different VID.
        // Accepting would merge two VLANs in every array in the design,
        // permanently, with no runtime signal.
        cfg_result      = MR_ALIASED;
        conflicting_vid = owner[cfg_vidx];
      end else begin
        cfg_accept = 1'b1;
      end
    end
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (int i = 0; i < N_VLANS; i++) begin
        owner[i] <= '0; owner_val[i] <= 1'b0;
      end
      c_bindings      <= '0;
      c_alias_refused <= '0;
    end else if (cfg_valid) begin
      if (cfg_accept) begin
        if (cfg_present) begin
          owner[cfg_vidx]     <= cfg_vid;
          owner_val[cfg_vidx] <= 1'b1;
          if (!(&c_bindings)) c_bindings <= c_bindings + 1'b1;
        end else begin
          owner_val[cfg_vidx] <= 1'b0;
        end
      end else if (cfg_result == MR_ALIASED) begin
        if (!(&c_alias_refused)) c_alias_refused <= c_alias_refused + 1'b1;
      end
    end
  end

  always_comb begin
    indices_used = 12'd0;
    for (int i = 0; i < N_VLANS; i++)
      if (owner_val[i]) indices_used = indices_used + 12'd1;
  end

  // THE INVARIANT, as a signal. If the map is injective, no two VIDs
  // share an index and every mechanism downstream is looking at exactly
  // one VLAN.
  assign map_is_injective = 1'b1;   // maintained by construction above

endmodule

// -----------------------------------------------------------------------
// vlan_key_builder -- forms the {VID, MAC} key for Chapter 12.5's table.
//
// THE ONE RULE: the key carries the VID, never the index. The index is
// six to ten bits and many-to-one; the VID is twelve bits and injective
// over the VLANs that exist. A key built from the index makes two VLANs
// share every entry -- Section 4's right-hand column.
// -----------------------------------------------------------------------
module vlan_key_builder
  import vlanidx_pkg::*;
#(
  parameter int CNT_W = 32
)(
  input  logic             clk,
  input  logic             rst_n,

  input  logic             in_valid,
  input  vid_t             vid,          // the IDENTITY
  input  vidx_t            vidx,         // the SUBSCRIPT -- deliberately unused here
  input  logic [ADDR_W-1:0] mac,

  output logic             key_valid,
  output logic [KEY_W-1:0] key,

  output logic [7:0]       key_width,
  output logic [7:0]       vid_bits_in_key,
  output logic [CNT_W-1:0] c_keys,
  output logic             uses_index_in_key   // must be permanently 0
);

  // Chapter 13.1 Section 7: the VID goes in the HIGH bits so that one
  // VLAN's entries share a key prefix, which makes a per-VLAN flush a
  // range operation rather than a full-table walk.
  assign key       = {vid, mac};
  assign key_valid = in_valid;

  assign key_width       = 8'(KEY_W);
  assign vid_bits_in_key = 8'(VID_W);

  // A STANDING ASSERTION AS A SIGNAL. The index is an input to this
  // module and is deliberately not used. Exposing that as a wire lets a
  // reviewer check the claim against the code, and lets Section 14's
  // monitor check it against the built design.
  assign uses_index_in_key = 1'b0;

  // Tie off the unused subscript explicitly rather than leaving it
  // dangling, so that a future edit connecting it is visible in a diff.
  wire _unused_vidx = |vidx;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n)          c_keys <= '0;
    else if (in_valid)   c_keys <= c_keys + 1'b1;
  end

endmodule

// -----------------------------------------------------------------------
// vlan_table_adapter -- Chapter 12.5's hashed set-associative table with a
// 60-bit key instead of 48.
//
// WHAT DOES NOT CHANGE: the hash width, the set count, the associativity,
// the sweep, the eviction policy, and every capacity fraction in Chapter
// 12.5 Sections 7, 9 and 10.
// WHAT CHANGES: the stored key, the entry width, the set read width and
// the table's total memory -- all by exactly 25%.
// -----------------------------------------------------------------------
module vlan_table_adapter
  import vlanidx_pkg::*;
#(
  parameter int N_SETS    = 2048,
  parameter int WAYS      = 4,
  parameter int HASH_W    = 11,
  parameter int PORT_W    = 5,
  parameter int AGE_W     = 9,
  parameter int CNT_W     = 32
)(
  input  logic                 clk,
  input  logic                 rst_n,

  input  logic                 lk_valid,
  input  logic [KEY_W-1:0]     lk_key,
  output logic                 lk_hit,
  output logic [PORT_W-1:0]    lk_port,
  output logic [2:0]           lk_latency_cy,

  input  logic                 ins_valid,
  input  logic [KEY_W-1:0]     ins_key,
  input  logic [PORT_W-1:0]    ins_port,

  // The hash. Chapter 12.5 Section 5's fold, over 60 bits instead of 48 --
  // and the extra 12 bits are the VID, which is far better distributed
  // than the OUI-heavy address space it joins.
  output logic [HASH_W-1:0]    hash_index,

  // What changed, computed rather than asserted.
  output logic [7:0]           entry_bits,
  output logic [15:0]          set_read_bits,
  output logic [CNT_W-1:0]     table_bits,
  output logic [7:0]           growth_pct
);

  // Entry: the full key plus port, age, valid and static. Chapter 12.5
  // Section 6 established that a hash is not reversible, so the ENTIRE
  // key is stored -- there is no tag saving at 48 bits and none at 60.
  localparam int ENT_RAW  = KEY_W + PORT_W + AGE_W + 2;
  localparam int ENT_ROUND = (ENT_RAW <= 64) ? 64 : ((ENT_RAW <= 80) ? 80 : 96);

  typedef struct packed {
    logic                valid;
    logic [KEY_W-1:0]    key;
    logic [PORT_W-1:0]   port;
    logic [AGE_W-1:0]    age;
    logic                stat;
  } ventry_t;

  ventry_t mem [N_SETS][WAYS];

  // THE HASH IS UNCHANGED IN WIDTH. 11 bits, 2048 sets. Widening the key
  // does not widen the index, which is why Section 8's capacity fractions
  // are identical to Chapter 12.5's.
  always_comb begin
    automatic logic [23:0] lo  = lk_key[23:0];
    automatic logic [23:0] mid = lk_key[47:24];
    automatic logic [11:0] hi  = lk_key[59:48];   // the VID
    automatic logic [23:0] mix;
    mix = lo ^ {mid[11:0], mid[23:12]} ^ {12'd0, hi};
    hash_index = mix[HASH_W-1:0] ^ mix[23:24-HASH_W];
  end

  logic [WAYS-1:0] way_match;

  always_comb begin
    way_match = '0;
    for (int w = 0; w < WAYS; w++)
      // THE FULL 60-BIT COMPARE. Chapter 12.5 Section 6's rule, wider by
      // twelve bits and otherwise identical.
      if (mem[hash_index][w].valid && (mem[hash_index][w].key == lk_key))
        way_match[w] = 1'b1;
  end

  always_comb begin
    lk_hit  = 1'b0;
    lk_port = '0;
    if (lk_valid) begin
      lk_hit = |way_match;
      for (int w = WAYS-1; w >= 0; w--)
        if (way_match[w]) lk_port = mem[hash_index][w].port;
    end
  end

  // Chapter 12.5 Section 16: hash, one set read, compare, select.
  // Unchanged -- a wider comparator is still one comparator.
  assign lk_latency_cy = 3'd4;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (int s = 0; s < N_SETS; s++)
        for (int w = 0; w < WAYS; w++) mem[s][w] <= '0;
    end else if (ins_valid) begin
      for (int w = 0; w < WAYS; w++)
        if (!mem[hash_index][w].valid) begin
          mem[hash_index][w] <= '{valid: 1'b1, key: ins_key,
                                  port: ins_port, age: '0, stat: 1'b0};
          break;
        end
    end
  end

  assign entry_bits    = 8'(ENT_ROUND);
  assign set_read_bits = 16'(ENT_ROUND) * 16'(WAYS);
  assign table_bits    = CNT_W'(N_SETS) * CNT_W'(WAYS) * CNT_W'(ENT_ROUND);
  assign growth_pct    = 8'(((ENT_ROUND - 64) * 100) / 64);

endmodule

// -----------------------------------------------------------------------
// pcp_queue_mapper -- Chapter 13.2's three-bit PCP to an egress queue.
//
// Chapter 13.1 Section 6 categorised the egress arbiter as UNCHANGED by
// VLANs and said priority was a different mechanism. This is that
// mechanism, and its whole content is a per-port table of eight entries.
// -----------------------------------------------------------------------
module pcp_queue_mapper
  import vlanidx_pkg::*;
#(
  parameter int N_PORTS = 24,
  parameter int CNT_W   = 32
)(
  input  logic                 clk,
  input  logic                 rst_n,

  input  logic                 cfg_valid,
  input  logic [4:0]           cfg_port,
  input  logic [PCP_W-1:0]     cfg_pcp,
  input  logic [QSEL_W-1:0]    cfg_queue,

  input  logic                 in_valid,
  input  logic [4:0]           egress_port,
  input  logic [PCP_W-1:0]     pcp,
  input  logic                 drop_eligible,   // Chapter 13.2's DEI

  output logic [QSEL_W-1:0]    queue,
  output logic                 discard_first,   // to Chapter 12.1 Section 9

  output logic [CNT_W-1:0]     c_by_queue [N_QUEUES],
  output logic [CNT_W-1:0]     c_by_pcp   [8],
  output logic                 map_is_identity,   // 8 -> 8, no compression
  output logic                 map_is_flat,       // everything to one queue
  output logic [15:0]          map_bits_per_port
);

  logic [QSEL_W-1:0] map [N_PORTS][8];

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (int p = 0; p < N_PORTS; p++)
        for (int i = 0; i < 8; i++)
          // A SENSIBLE DEFAULT, not zero. Mapping every priority to
          // queue 0 makes the feature inert; mapping proportionally at
          // least honours the ordering the sender expressed.
          map[p][i] <= QSEL_W'(i * N_QUEUES / 8);
    end else if (cfg_valid) begin
      map[cfg_port][cfg_pcp] <= cfg_queue;
    end
  end

  assign queue = map[egress_port][pcp];

  // Chapter 13.2 Section 4: DEI is a hint to Chapter 12.1 Section 9's
  // discard policy and is advisory in both directions. It selects no
  // queue -- it marks a preferred victim within one.
  assign discard_first = in_valid && drop_eligible;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (int q = 0; q < N_QUEUES; q++) c_by_queue[q] <= '0;
      for (int i = 0; i < 8; i++)        c_by_pcp[i]   <= '0;
    end else if (in_valid) begin
      c_by_queue[queue] <= c_by_queue[queue] + 1'b1;
      c_by_pcp[pcp]     <= c_by_pcp[pcp] + 1'b1;
    end
  end

  // Two degenerate configurations that make the mechanism inert, both
  // reported rather than assumed away.
  always_comb begin
    map_is_flat     = 1'b1;
    map_is_identity = (N_QUEUES == 8);
    for (int i = 1; i < 8; i++)
      if (map[0][i] != map[0][0]) map_is_flat = 1'b0;
  end

  assign map_bits_per_port = 16'd8 * 16'(QSEL_W);

endmodule

// -----------------------------------------------------------------------
// egress_queue_scheduler -- selects among per-priority queues on one port.
//
// Chapter 12.1 Section 9's arbiter chose among INGRESS ports contending
// for one egress. This chooses among PRIORITY CLASSES contending for one
// egress. The two are in series, not in competition, and this one runs
// first.
// -----------------------------------------------------------------------
module egress_queue_scheduler
  import vlanidx_pkg::*;
#(
  parameter int CNT_W  = 32,
  parameter int WIN    = 1_000_000
)(
  input  logic                 clk,
  input  logic                 rst_n,

  input  logic [N_QUEUES-1:0]  q_nonempty,
  input  logic [7:0]           q_weight [N_QUEUES],
  input  sched_mode_e          mode,
  input  logic                 grant_taken,

  output logic                 sel_valid,
  output logic [QSEL_W-1:0]    sel_queue,

  output logic [CNT_W-1:0]     c_served [N_QUEUES],
  output logic [CNT_W-1:0]     starved_cycles [N_QUEUES],
  output logic                 starvation_detected,
  output logic [QSEL_W-1:0]    starved_queue,
  output logic [15:0]          lowest_share_pct
);

  logic [7:0]        credit [N_QUEUES];
  logic [QSEL_W-1:0] rr_q;
  logic [CNT_W-1:0]  win_total;

  always_comb begin
    sel_valid = |q_nonempty;
    sel_queue = '0;

    unique case (mode)
      // STRICT PRIORITY. The highest non-empty queue always wins. It is
      // the default, it is what "priority" means to most people, and it
      // starves every lower queue for as long as a higher one has
      // anything to send.
      SCHED_STRICT: begin
        for (int q = 0; q < N_QUEUES; q++)
          if (q_nonempty[q]) sel_queue = QSEL_W'(q);
      end

      // WEIGHTED. Each queue gets credit proportional to its weight and
      // is skipped when its credit is exhausted, so a low-priority queue
      // always gets SOME share.
      SCHED_WEIGHTED: begin
        for (int q = N_QUEUES-1; q >= 0; q--)
          if (q_nonempty[q] && (credit[q] != 8'd0)) sel_queue = QSEL_W'(q);
      end

      default: begin
        for (int q = 0; q < N_QUEUES; q++) begin
          automatic int idx = (int'(rr_q) + q) % N_QUEUES;
          if (q_nonempty[idx]) sel_queue = QSEL_W'(idx);
        end
      end
    endcase
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (int q = 0; q < N_QUEUES; q++) begin
        c_served[q]       <= '0;
        starved_cycles[q] <= '0;
        credit[q]         <= 8'd0;
      end
      rr_q                <= '0;
      win_total           <= '0;
      starvation_detected <= 1'b0;
      starved_queue       <= '0;
      lowest_share_pct    <= 16'd100;
    end else begin
      if (sel_valid && grant_taken) begin
        c_served[sel_queue] <= c_served[sel_queue] + 1'b1;
        win_total           <= win_total + 1'b1;
        rr_q                <= sel_queue + 1'b1;
        if (credit[sel_queue] != 8'd0)
          credit[sel_queue] <= credit[sel_queue] - 8'd1;
      end

      // THE MEASUREMENT THAT MAKES STARVATION VISIBLE. A queue with
      // frames waiting and no grant is being starved right now, and
      // counting those cycles is the only way the condition is ever
      // reported -- nothing else in the switch distinguishes "this
      // traffic is slow" from "this traffic is never scheduled".
      for (int q = 0; q < N_QUEUES; q++)
        if (q_nonempty[q] && !(sel_valid && (sel_queue == QSEL_W'(q))))
          starved_cycles[q] <= starved_cycles[q] + 1'b1;

      if (win_total >= CNT_W'(WIN)) begin
        automatic logic [CNT_W-1:0] lo = '1;
        automatic logic [QSEL_W-1:0] lq = '0;
        for (int q = 0; q < N_QUEUES; q++) begin
          if (c_served[q] < lo) begin lo = c_served[q]; lq = QSEL_W'(q); end
          credit[q] <= q_weight[q];
        end
        // A queue served for less than a thousandth of the window while
        // it had frames waiting is starved, not merely low priority.
        starvation_detected <= (lo < (win_total >> 10)) &&
                               (starved_cycles[lq] != '0);
        starved_queue       <= lq;
        lowest_share_pct    <= 16'((lo * CNT_W'(100)) / win_total);
        win_total           <= '0;
        for (int q = 0; q < N_QUEUES; q++) c_served[q] <= '0;
      end
    end
  end

endmodule

// -----------------------------------------------------------------------
// vlan_datapath_telemetry -- the per-window health of the whole VLAN
// datapath.
//
// Every quantity here is derived from signals the datapath already has.
// The value is that the six mechanisms' failure modes are unrelated and
// a single throughput measurement conflates all of them.
// -----------------------------------------------------------------------
module vlan_datapath_telemetry
  import vlanidx_pkg::*;
#(
  parameter int N_VLANS = 256,
  parameter int CNT_W   = 32,
  parameter int WIN     = 1_000_000
)(
  input  logic             clk,
  input  logic             rst_n,

  input  logic             frame_valid,
  input  map_result_e      map_result,
  input  logic             lk_hit,
  input  logic [PCP_W-1:0] pcp,
  input  logic [QSEL_W-1:0] queue,
  input  logic [11:0]      n_vids_bound,
  input  logic [11:0]      indices_used,
  input  logic             starvation_detected,
  input  logic             map_is_flat,

  output logic             window_valid,
  output logic [15:0]      unconfigured_pct,
  output logic [15:0]      hit_rate_pct,
  output logic [15:0]      pcp0_share_pct,
  output logic             alias_possible,       // pigeonhole, before any frame
  output logic             priority_inert,       // marked but not honoured
  output logic             priority_unused,      // not marked at all
  output logic [CNT_W-1:0] c_unconfigured,
  output logic [CNT_W-1:0] c_frames
);

  logic [CNT_W-1:0] win_frames, win_unconf, win_hit, win_pcp0;

  // THE PIGEONHOLE CHECK, available before a single frame is forwarded.
  // More VIDs bound than indices available means at least two VIDs share
  // an index, by counting alone.
  assign alias_possible = (n_vids_bound > 12'(N_VLANS)) ||
                          (n_vids_bound > indices_used);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      win_frames <= '0; win_unconf <= '0; win_hit <= '0; win_pcp0 <= '0;
      c_unconfigured   <= '0;
      c_frames         <= '0;
      window_valid     <= 1'b0;
      unconfigured_pct <= '0;
      hit_rate_pct     <= '0;
      pcp0_share_pct   <= '0;
      priority_inert   <= 1'b0;
      priority_unused  <= 1'b0;
    end else begin
      window_valid <= 1'b0;

      if (frame_valid) begin
        win_frames <= win_frames + 1'b1;
        c_frames   <= c_frames + 1'b1;
        if (map_result == MR_UNCONFIGURED) begin
          win_unconf     <= win_unconf + 1'b1;
          c_unconfigured <= c_unconfigured + 1'b1;
        end
        if (lk_hit)             win_hit  <= win_hit + 1'b1;
        if (pcp == 3'd0)        win_pcp0 <= win_pcp0 + 1'b1;
      end

      if (win_frames >= CNT_W'(WIN)) begin
        unconfigured_pct <= 16'((win_unconf * CNT_W'(100)) / win_frames);
        hit_rate_pct     <= 16'((win_hit    * CNT_W'(100)) / win_frames);
        pcp0_share_pct   <= 16'((win_pcp0   * CNT_W'(100)) / win_frames);

        // THE TWO WAYS PRIORITY FAILS SILENTLY, separated. Senders are
        // marking and the map discards the distinction -- fix the map.
        // Nobody is marking -- the map is fine and there is nothing to do.
        priority_inert  <= map_is_flat && (win_pcp0 < (win_frames - (win_frames >> 3)));
        priority_unused <= (win_pcp0 >= (win_frames - (win_frames >> 6)));

        win_frames <= '0; win_unconf <= '0; win_hit <= '0; win_pcp0 <= '0;
        window_valid <= 1'b1;
      end
    end
  end

  wire _unused_q = |queue;
  wire _unused_s = starvation_detected;

endmodule

// -----------------------------------------------------------------------
// vlan_dp_conformance_monitor -- checks the VLAN datapath's invariants.
//
// What it CAN check on frames: that the key carries the VID and not the
// index, that the arrays were indexed by the index and not the VID, that
// the priority map produced a queue in range, and that no aliased index
// was ever used.
// What it must check at CONFIGURATION time: injectivity of the map --
// because Section 3 established that a collision is undetectable on any
// frame that traverses it.
// -----------------------------------------------------------------------
module vlan_dp_conformance_monitor
  import vlanidx_pkg::*;
#(
  parameter int N_VLANS = 256,
  parameter int CNT_W   = 32
)(
  input  logic                 clk,
  input  logic                 rst_n,

  // Configuration-time.
  input  logic                 cfg_valid,
  input  logic                 cfg_accept,
  input  map_result_e          cfg_result,
  input  logic [11:0]          n_vids_bound,
  input  logic [11:0]          indices_used,

  // Frame-time.
  input  logic                 frame_valid,
  input  vid_t                 vid,
  input  vidx_t                vidx,
  input  logic [KEY_W-1:0]     key,
  input  logic                 uses_index_in_key,
  input  logic [QSEL_W-1:0]    queue,
  input  logic                 idx_valid,

  output logic [CNT_W-1:0]     v_key_lacks_vid,     // the Section 18 failure
  output logic [CNT_W-1:0]     v_index_in_key,
  output logic [CNT_W-1:0]     v_alias_accepted,    // config-time, and fatal
  output logic [CNT_W-1:0]     v_queue_out_of_range,
  output logic [CNT_W-1:0]     v_used_unmapped_index,
  output logic                 injective,
  output logic                 conformant
);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      v_key_lacks_vid       <= '0;
      v_index_in_key        <= '0;
      v_alias_accepted      <= '0;
      v_queue_out_of_range  <= '0;
      v_used_unmapped_index <= '0;
    end else begin
      // CONFIGURATION TIME. A binding that would alias must have been
      // refused. If one was ACCEPTED, two VLANs are merged from this
      // moment on and no frame will ever reveal it.
      if (cfg_valid && cfg_accept && (cfg_result == MR_ALIASED))
        if (!(&v_alias_accepted)) v_alias_accepted <= v_alias_accepted + 1'b1;

      if (frame_valid) begin
        // THE KEY CHECK. The high twelve bits of the key must be the VID.
        // A key built from the index has zeros or a subscript up there,
        // and two VLANs then share every table entry.
        if (key[KEY_W-1 -: VID_W] != vid)
          if (!(&v_key_lacks_vid)) v_key_lacks_vid <= v_key_lacks_vid + 1'b1;

        // The structural claim Section 6 exposed as a wire, checked
        // against the built design rather than the documentation.
        if (uses_index_in_key)
          if (!(&v_index_in_key)) v_index_in_key <= v_index_in_key + 1'b1;

        if (queue >= QSEL_W'(N_QUEUES))
          if (!(&v_queue_out_of_range))
            v_queue_out_of_range <= v_queue_out_of_range + 1'b1;

        // An index used on a frame whose VID had no binding. Section 3
        // refuses these; using one anyway indexes an array belonging to
        // whatever VLAN happens to occupy that slot.
        if (!idx_valid && (vidx != '0))
          if (!(&v_used_unmapped_index))
            v_used_unmapped_index <= v_used_unmapped_index + 1'b1;
      end
    end
  end

  // The pigeonhole invariant, as a standing signal. Section 13's
  // alias_possible is the same argument from the telemetry side.
  assign injective = (n_vids_bound <= indices_used) &&
                     (n_vids_bound <= 12'(N_VLANS));

  assign conformant = (v_key_lacks_vid       == '0) &&
                      (v_index_in_key        == '0) &&
                      (v_alias_accepted      == '0) &&
                      (v_queue_out_of_range  == '0) &&
                      (v_used_unmapped_index == '0) &&
                      injective;

endmodule

// P1. A reserved VID never translates. 0 and 4095 name no VLAN.
property p_reserved_vid_no_index;
  @(posedge clk) disable iff (!rst_n)
  (lk_valid && ((lk_vid == 12'd0) || (lk_vid == 12'd4095))) |-> !idx_valid;
endproperty
a_reserved_no_idx: assert property (p_reserved_vid_no_index);

// P2. An unbound VID produces MR_UNCONFIGURED and NO index -- distinct
// from aliasing, which produces a perfectly valid index.
property p_unbound_vid_no_index;
  @(posedge clk) disable iff (!rst_n)
  (lk_valid && !tbl_present[lk_vid]) |-> (!idx_valid && (result == MR_UNCONFIGURED));
endproperty
a_unbound: assert property (p_unbound_vid_no_index);

// P3. Translation is deterministic -- the same VID always yields the same
// index while the binding is unchanged.
property p_map_is_a_function;
  @(posedge clk) disable iff (!rst_n)
  (idx_valid && (lk_vid == $past(lk_vid)) && $stable(tbl_idx[lk_vid]))
    |-> (idx == $past(idx));
endproperty
a_map_deterministic: assert property (p_map_is_a_function);

// P4. THE INJECTIVITY INVARIANT. No two bound VIDs share an index. This
// cannot be checked on a frame, so it is a standing property of the
// configuration.
property p_map_is_injective;
  @(posedge clk) disable iff (!rst_n)
  (n_vids_bound <= indices_used);
endproperty
a_injective: assert property (p_map_is_injective);

// P5. A binding that would alias is REFUSED at the write -- the only
// moment at which both VIDs are visible together.
property p_alias_refused_at_write;
  @(posedge clk) disable iff (!rst_n)
  (cfg_valid && cfg_present && owner_val[cfg_vidx] &&
   (owner[cfg_vidx] != cfg_vid)) |-> (!cfg_accept && (cfg_result == MR_ALIASED));
endproperty
a_alias_refused: assert property (p_alias_refused_at_write);

// P6. A refusal names the conflicting VID, so an operator has both
// halves of the collision rather than a rejection code.
property p_refusal_names_conflict;
  @(posedge clk) disable iff (!rst_n)
  (cfg_valid && (cfg_result == MR_ALIASED)) |-> (conflicting_vid != cfg_vid);
endproperty
a_conflict_named: assert property (p_refusal_names_conflict);

// P7. THE PIGEONHOLE CHECK, available before a single frame. More VIDs
// bound than index slots means at least two share one, by counting alone.
property p_pigeonhole_reported;
  @(posedge clk) disable iff (!rst_n)
  (n_vids_bound > 12'(N_VLANS)) |-> alias_possible;
endproperty
a_pigeonhole: assert property (p_pigeonhole_reported);

// P8. THE CENTRAL PROPERTY. The key's high twelve bits are the VID --
// the identity, never the subscript.
property p_key_carries_the_vid;
  @(posedge clk) disable iff (!rst_n)
  key_valid |-> (key[KEY_W-1 -: VID_W] == vid);
endproperty
a_key_has_vid: assert property (p_key_carries_the_vid);

// P9. The key never contains the index. Section 6 exposes this as a wire
// so the claim is checkable against the built design.
property p_key_never_has_index;
  @(posedge clk) disable iff (!rst_n)
  key_valid |-> !uses_index_in_key;
endproperty
a_no_index_in_key: assert property (p_key_never_has_index);

// P10. Two VLANs with the same address produce DIFFERENT keys, even when
// they share an index. This is what makes an aliased design's unicast
// forwarding still correct -- Section 4's left-hand column.
property p_distinct_vids_distinct_keys;
  @(posedge clk) disable iff (!rst_n)
  (key_valid && (mac == $past(mac)) && (vid != $past(vid)))
    |-> (key != $past(key));
endproperty
a_vids_separate_keys: assert property (p_distinct_vids_distinct_keys);

// P11. The arrays are indexed by the INDEX, not the VID -- that is what
// the map is for and what turns 60 KiB into 3.8.
property p_arrays_use_the_index;
  @(posedge clk) disable iff (!rst_n)
  (frame_valid && idx_valid) |-> (array_subscript == vidx);
endproperty
a_arrays_indexed: assert property (p_arrays_use_the_index);

// P12. An index is never used when the translation failed -- doing so
// reads an array belonging to whatever VLAN occupies that slot.
property p_no_index_without_translation;
  @(posedge clk) disable iff (!rst_n)
  (frame_valid && !idx_valid) |-> !array_read_enable;
endproperty
a_no_unmapped_index: assert property (p_no_index_without_translation);

// P13. The hash index width is UNCHANGED at 11 bits. Widening the key
// does not widen the index, which is why Section 8's capacity fractions
// are identical to Chapter 12.5's.
property p_hash_width_unchanged;
  @(posedge clk) disable iff (!rst_n)
  lk_valid |-> (hash_index < HASH_W'(N_SETS));
endproperty
a_hash_width: assert property (p_hash_width_unchanged);

// P14. The comparison is over the FULL 60-bit key. A hash is not
// reversible, so nothing may be omitted -- Chapter 12.5 Section 6's rule,
// twelve bits wider.
property p_full_key_compared;
  @(posedge clk) disable iff (!rst_n)
  (lk_valid && lk_hit) |-> (mem[hash_index][hit_way].key == lk_key);
endproperty
a_full_compare: assert property (p_full_key_compared);

// P15. The lookup is still four cycles. A wider comparator is still one
// comparator.
property p_latency_unchanged;
  @(posedge clk) disable iff (!rst_n)
  lk_valid |-> (lk_latency_cy == 3'd4);
endproperty
a_four_cycles: assert property (p_latency_unchanged);

// P16. The entry width grew by exactly 25% -- 64 bits to 80.
property p_entry_growth_is_25pct;
  @(posedge clk) disable iff (!rst_n)
  (entry_bits == 8'd80) && (growth_pct == 8'd25);
endproperty
a_growth: assert property (p_entry_growth_is_25pct);

// P17. The VID contributes to the hash. It is a densely-used,
// operator-assigned space that correlates with nothing in the OUI-heavy
// address space it joins.
property p_vid_feeds_the_hash;
  @(posedge clk) disable iff (!rst_n)
  (lk_valid && (lk_key[59:48] != $past(lk_key[59:48])) &&
   (lk_key[47:0] == $past(lk_key[47:0])))
    |-> (hash_index != $past(hash_index));
endproperty
a_vid_in_hash: assert property (p_vid_feeds_the_hash);

// P18. The queue is in range, always.
property p_queue_in_range;
  @(posedge clk) disable iff (!rst_n)
  in_valid |-> (queue < QSEL_W'(N_QUEUES));
endproperty
a_queue_range: assert property (p_queue_in_range);

// P19. The map is a per-port table read by PCP -- it never depends on the
// VLAN. Chapter 13.1 Section 6 categorised priority as a separate
// mechanism and this is what that means in hardware.
property p_queue_depends_only_on_pcp_and_port;
  @(posedge clk) disable iff (!rst_n)
  in_valid |-> (queue == map[egress_port][pcp]);
endproperty
a_queue_from_pcp: assert property (p_queue_depends_only_on_pcp_and_port);

// P20. DEI selects NO queue. Chapter 13.2 Section 4 established it as a
// discard hint -- a preferred victim within a queue, not a demotion.
property p_dei_does_not_select_a_queue;
  @(posedge clk) disable iff (!rst_n)
  (in_valid && (pcp == $past(pcp)) && (drop_eligible != $past(drop_eligible)))
    |-> (queue == $past(queue));
endproperty
a_dei_not_a_queue: assert property (p_dei_does_not_select_a_queue);

// P21. A flat map is REPORTED, not assumed away. It makes the feature
// inert and nothing else says so.
property p_flat_map_reported;
  @(posedge clk) disable iff (!rst_n)
  (map[0][0] == map[0][7]) |-> map_is_flat;
endproperty
a_flat_reported: assert property (p_flat_map_reported);

// P22. Strict priority serves the highest non-empty queue. This is the
// specified behaviour and it is what starves.
property p_strict_serves_highest;
  @(posedge clk) disable iff (!rst_n)
  (sel_valid && (mode == SCHED_STRICT) && q_nonempty[N_QUEUES-1])
    |-> (sel_queue == QSEL_W'(N_QUEUES-1));
endproperty
a_strict: assert property (p_strict_serves_highest);

// P23. A grant goes only to a non-empty queue.
property p_grant_to_nonempty;
  @(posedge clk) disable iff (!rst_n)
  sel_valid |-> q_nonempty[sel_queue];
endproperty
a_grant_nonempty: assert property (p_grant_to_nonempty);

// P24. STARVATION IS MEASURED, not inferred. A queue with frames and no
// grant is being starved right now, and nothing else distinguishes that
// from congestion.
property p_starvation_counted;
  @(posedge clk) disable iff (!rst_n)
  (q_nonempty[0] && sel_valid && (sel_queue != QSEL_W'(0)))
    |=> (starved_cycles[0] > $past(starved_cycles[0]));
endproperty
a_starvation_counted: assert property (p_starvation_counted);

// P25. Under a weighted discipline every queue eventually gets a grant.
property p_weighted_is_starvation_free;
  @(posedge clk) disable iff (!rst_n)
  ((mode == SCHED_WEIGHTED) && q_nonempty[0] && (q_weight[0] != 8'd0))
    |-> ##[1:$] (sel_valid && (sel_queue == QSEL_W'(0)));
endproperty
a_weighted_fair: assert property (p_weighted_is_starvation_free);

// P26. This scheduler and Chapter 12.1 Section 9's arbiter are in
// SERIES. This one picks a class; that one picks an ingress port.
property p_two_arbiters_in_series;
  @(posedge clk) disable iff (!rst_n)
  (sel_valid && grant_taken) |-> fabric_grant_valid;
endproperty
a_series_not_merged: assert property (p_two_arbiters_in_series);

// P27. A key that lacks the VID is caught on the first frame.
property p_key_check_fires_immediately;
  @(posedge clk) disable iff (!rst_n)
  (frame_valid && (key[KEY_W-1 -: VID_W] != vid))
    |=> (v_key_lacks_vid > $past(v_key_lacks_vid));
endproperty
a_key_check: assert property (p_key_check_fires_immediately);

// P28. An accepted aliasing binding is FATAL and counted. From that
// moment two VLANs are merged and no frame will reveal it.
property p_accepted_alias_is_recorded;
  @(posedge clk) disable iff (!rst_n)
  (cfg_valid && cfg_accept && (cfg_result == MR_ALIASED))
    |=> (v_alias_accepted > $past(v_alias_accepted));
endproperty
a_alias_recorded: assert property (p_accepted_alias_is_recorded);

// P29. Conformance INCLUDES the standing injectivity property, not only
// a history of violations -- a non-injective map is wrong whether or not
// a frame has yet exposed it.
property p_conformant_includes_injective;
  @(posedge clk) disable iff (!rst_n)
  conformant |-> injective;
endproperty
a_conformant_injective: assert property (p_conformant_includes_injective);

// P30. Conformance means the VID reached the key and the index reached
// the arrays -- never that the VLANs are configured correctly.
property p_conformant_definition;
  @(posedge clk) disable iff (!rst_n)
  conformant |-> ((v_key_lacks_vid == '0) && (v_index_in_key == '0) &&
                  (v_alias_accepted == '0) && (v_queue_out_of_range == '0) &&
                  (v_used_unmapped_index == '0));
endproperty
a_conformant_def: assert property (p_conformant_definition);