"VLANs Improve Performance Automatically"

a switch with aggregate capacity C, offered load L
divide its ports into V VLANs
the capacity is still C and the offered load is still L
Δ throughput = 0

// ---------------------------------------------------------------------
// vlanperf_pkg -- the constants a conservation argument needs, with
// every derived figure computed here rather than written as a literal.
//
// Unit: Chapter 23.3 Section 2's bitcell equivalent.
//   1 BCE = 0.35 GE = one bit of usable on-die SRAM
//   1 flip-flop = 20 BCE
//   Chapter 19.7 Section 19's MAC receive datapath = 283 320 BCE
//   Chapter 23.3's 64-port switch = 5.62e8 BCE, table 128k x 96 b
// ---------------------------------------------------------------------
package vlanperf_pkg;

  localparam int unsigned DATAPATH_BCE  = 283_320;
  localparam int unsigned BCE_PER_FLOP  = 20;
  localparam int unsigned SWITCH_BCE_E4 = 56_200;      // 5.62e8 / 1e4
  localparam int unsigned TBL_ENTRIES   = 128 * 1024;
  localparam int unsigned TBL_WIDTH     = 96;

  // ---- Chapter 24.3 Section 1's framing tax ---------------------------
  localparam int unsigned OCT_FIXED = 38;   // preamble 8, gap 12,
                                            // addresses 12, FCS 4, type 2
  // ---- Chapter 13.2's tag ----------------------------------------------
  localparam int unsigned OCT_TAG   = 4;    // TPID 2 + TCI 2
  localparam int unsigned VID_BITS  = 12;
  localparam int unsigned VID_USABLE = 4094;   // 0 and 4095 reserved

  // ---- Chapter 12.4 Section 10's domain arithmetic ---------------------
  localparam int unsigned DEFAULT_B_PER_S = 5;   // broadcasts per station

  typedef enum logic [1:0] {
    PORT_ACCESS = 2'd0,       // Chapter 13.3
    PORT_TRUNK  = 2'd1,
    PORT_HYBRID = 2'd2
  } portmode_e;

  // ---- derived: wire cost ----------------------------------------------
  function automatic int unsigned wire_slot(int unsigned payload,
                                            bit tagged);
    return payload + OCT_FIXED + (tagged ? OCT_TAG : 0);
  endfunction

  function automatic int unsigned tag_cost_ppm(int unsigned payload);
    return (OCT_TAG * 1_000_000) / wire_slot(payload, 1'b0);
  endfunction

  function automatic int unsigned efficiency_ppm(int unsigned payload,
                                                 bit tagged);
    return (payload * 1_000_000) / wire_slot(payload, tagged);
  endfunction

  // ---- derived: flood width --------------------------------------------
  function automatic int unsigned ports_per_vlan(int unsigned ports,
                                                 int unsigned vlans);
    return (vlans == 0) ? ports : (ports / vlans);
  endfunction

  function automatic int unsigned flood_copies(int unsigned ports,
                                               int unsigned vlans);
    int unsigned p;
    p = ports_per_vlan(ports, vlans);
    return (p == 0) ? 0 : (p - 1);
  endfunction

  // ---- derived: per-station broadcast rate ------------------------------
  function automatic int unsigned station_rx_per_s(int unsigned ports,
                                                   int unsigned vlans,
                                                   int unsigned b_per_s);
    return flood_copies(ports, vlans) * b_per_s;
  endfunction

  // ---- derived: the trunk, which segmentation does not reduce -----------
  function automatic int unsigned trunk_per_s(int unsigned ports,
                                              int unsigned vlans,
                                              int unsigned b_per_s);
    // every VLAN's stations, all of them, cross the trunk.
    return ports_per_vlan(ports, vlans) * vlans * b_per_s;
  endfunction

  function automatic int unsigned datapaths_milli(int unsigned bce);
    return (bce * 1000) / DATAPATH_BCE;
  endfunction

endpackage

// ---------------------------------------------------------------------
// tag_cost_model -- what four octets cost, and the conservation law
// that says nothing else about bandwidth changed.
//
// The output that matters is throughput_delta_ppm, which is zero for
// every configuration. The tag's cost is the only nonzero bandwidth
// figure in this chapter and it has the wrong sign.
// ---------------------------------------------------------------------
module tag_cost_model
  import vlanperf_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,

  input  logic [15:0] payload_octets,
  input  logic        tagged,
  input  logic [15:0] ports,
  input  logic [15:0] vlans,
  input  logic [15:0] port_rate_gbps,

  output logic [31:0] slot_untagged,
  output logic [31:0] slot_tagged,
  output logic [31:0] tag_cost_ppm_o,
  output logic [31:0] eff_untagged_ppm,
  output logic [31:0] eff_tagged_ppm,
  output logic [31:0] aggregate_gbps_before,
  output logic [31:0] aggregate_gbps_after,
  output logic signed [31:0] throughput_delta_ppm,
  output logic        capacity_is_conserved,
  output logic        only_effect_is_negative,
  output logic [31:0] c_evaluations
);
  always_comb begin
    slot_untagged = 32'(wire_slot(int'(payload_octets), 1'b0));
    slot_tagged   = 32'(wire_slot(int'(payload_octets), 1'b1));

    tag_cost_ppm_o   = 32'(tag_cost_ppm(int'(payload_octets)));
    eff_untagged_ppm = 32'(efficiency_ppm(int'(payload_octets), 1'b0));
    eff_tagged_ppm   = 32'(efficiency_ppm(int'(payload_octets), 1'b1));

    // Section 2's conservation law, evaluated rather than asserted.
    aggregate_gbps_before = 32'(ports) * 32'(port_rate_gbps);
    aggregate_gbps_after  = 32'(ports) * 32'(port_rate_gbps);
    throughput_delta_ppm  = 32'sd0;

    capacity_is_conserved = (aggregate_gbps_after == aggregate_gbps_before);

    // And the one bandwidth figure that does move.
    only_effect_is_negative = tagged
                           && (eff_tagged_ppm < eff_untagged_ppm);
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) c_evaluations <= '0;
    else        c_evaluations <= c_evaluations + 32'd1;
  end
endmodule

// ---------------------------------------------------------------------
// flood_width_model -- Chapter 12.4 Section 3's amplification with the
// port count replaced by a VLAN's member count, and the flood share
// that bounds what the reduction is worth.
//
// The output that matters is improvement_ppm, because it is zero when
// nothing was flooding -- which is the condition the myth omits.
// ---------------------------------------------------------------------
module flood_width_model
  import vlanperf_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,

  input  logic [15:0] ports,
  input  logic [15:0] vlans,
  input  logic [31:0] flood_share_ppm,
  input  logic [31:0] port_pps_k,          // thousands of frames/s
  input  logic [31:0] switch_budget_pps_k,

  output logic [15:0] members_per_vlan,
  output logic [15:0] copies_segmented,
  output logic [15:0] copies_flat,
  output logic [31:0] width_share_ppm,
  output logic [31:0] emissions_flat_k,
  output logic [31:0] emissions_segmented_k,
  output logic [31:0] budget_share_flat_ppm,
  output logic [31:0] budget_share_seg_ppm,
  output logic [31:0] mean_copies_flat_x1000,
  output logic [31:0] mean_copies_seg_x1000,
  output logic [31:0] improvement_ppm,
  output logic        improvement_needs_flooding,
  output logic [31:0] c_evaluations
);
  always_comb begin
    members_per_vlan = 16'(ports_per_vlan(int'(ports), int'(vlans)));
    copies_segmented = 16'(flood_copies(int'(ports), int'(vlans)));
    copies_flat      = 16'(flood_copies(int'(ports), 1));

    width_share_ppm = (copies_flat == 0) ? 32'd0
                    : ((32'(copies_segmented) * 1_000_000) / 32'(copies_flat));

    emissions_flat_k      = port_pps_k * 32'(copies_flat);
    emissions_segmented_k = port_pps_k * 32'(copies_segmented);

    budget_share_flat_ppm = (switch_budget_pps_k == 0) ? 32'd0
                          : ((emissions_flat_k * 1_000_000)
                             / switch_budget_pps_k);
    budget_share_seg_ppm  = (switch_budget_pps_k == 0) ? 32'd0
                          : ((emissions_segmented_k * 1_000_000)
                             / switch_budget_pps_k);

    // Mean egress copies per frame: 1 normally, copies when flooding.
    mean_copies_flat_x1000 = 32'd1000
      + ((flood_share_ppm * (32'(copies_flat) - 32'd1)) / 32'd1000);
    mean_copies_seg_x1000  = 32'd1000
      + ((flood_share_ppm * (32'(copies_segmented) - 32'd1)) / 32'd1000);

    improvement_ppm = (mean_copies_flat_x1000 == 0) ? 32'd0
                    : (((mean_copies_flat_x1000 - mean_copies_seg_x1000)
                        * 1_000_000) / mean_copies_flat_x1000);

    // THE condition the myth omits.
    improvement_needs_flooding = (flood_share_ppm != 32'd0);
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) c_evaluations <= '0;
    else        c_evaluations <= c_evaluations + 32'd1;
  end
endmodule

station budget ÷ B = stations per domain
64 ports ÷ stations per domain = VLANs required

// ---------------------------------------------------------------------
// domain_rate_model -- Chapter 12.4 Section 10's arithmetic with the
// VLAN count as the free variable, and the CPU budget as the bound.
//
// The output that matters is domain_spans_switches, which is an input
// the switch cannot determine and which changes the answer by a factor
// of the fabric's size.
// ---------------------------------------------------------------------
module domain_rate_model
  import vlanperf_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,

  input  logic [15:0] ports_per_switch,
  input  logic [15:0] switches_in_domain,
  input  logic [15:0] vlans,
  input  logic [15:0] b_per_station_s,
  input  logic [15:0] cpu_budget_fps,
  input  logic [15:0] us_per_frame,

  output logic [31:0] stations_in_domain,
  output logic [31:0] rx_per_station_s,
  output logic [31:0] cpu_us_per_s,
  output logic [15:0] core_share_ppm,
  output logic        within_budget,
  output logic [15:0] vlans_required,
  output logic        domain_spans_switches,
  output logic        switch_can_determine_this,
  output logic [31:0] c_over_budget
);
  logic [31:0] stations_per_vlan;

  always_comb begin
    // The domain is the fabric, not the switch -- Chapter 12.4 Sec 10.
    stations_in_domain = 32'(ports_per_switch) * 32'(switches_in_domain);

    stations_per_vlan = (vlans == 0) ? stations_in_domain
                      : (stations_in_domain / 32'(vlans));

    rx_per_station_s = (stations_per_vlan == 0) ? 32'd0
                     : ((stations_per_vlan - 32'd1) * 32'(b_per_station_s));

    cpu_us_per_s   = rx_per_station_s * 32'(us_per_frame);
    core_share_ppm = 16'(cpu_us_per_s / 32'd1);   // us/s is ppm of a core

    within_budget = (rx_per_station_s <= 32'(cpu_budget_fps));

    // How many VLANs the budget demands.
    vlans_required = (cpu_budget_fps == 0) ? 16'hFFFF
                   : 16'((stations_in_domain * 32'(b_per_station_s)
                          + 32'(cpu_budget_fps) - 32'd1)
                         / 32'(cpu_budget_fps));

    domain_spans_switches = (switches_in_domain > 16'd1);

    // THE gap. A switch learns what it hears; nothing tells it how many
    // other switches share its broadcast domain.
    switch_can_determine_this = 1'b0;
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n)              c_over_budget <= '0;
    else if (!within_budget) c_over_budget <= c_over_budget + 32'd1;
  end
endmodule

// ---------------------------------------------------------------------
// trunk_load_model -- what the uplink carries before and after
// segmentation, which is the same thing plus a tag.
//
// The output that matters is trunk_relief_ppm, which is zero or
// negative for every configuration. It is the chapter's conservation
// law measured on the link a deployment cares about.
// ---------------------------------------------------------------------
module trunk_load_model
  import vlanperf_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,

  input  logic [15:0] ports,
  input  logic [15:0] vlans,
  input  logic [15:0] b_per_station_s,
  input  logic [15:0] mean_frame_octets,
  input  logic [15:0] trunk_rate_gbps,

  output logic [31:0] stations,
  output logic [31:0] trunk_bcast_flat,
  output logic [31:0] trunk_bcast_segmented,
  output logic signed [31:0] trunk_relief_ppm,
  output logic [31:0] trunk_tag_cost_ppm,
  output logic [31:0] trunk_bcast_bps,
  output logic [31:0] trunk_bcast_share_ppm,
  output logic        segmentation_relieves_trunk,
  output logic        trunk_pays_the_tag,
  output logic [31:0] c_evaluations
);
  always_comb begin
    stations = 32'(ports_per_vlan(int'(ports), int'(vlans)))
             * ((vlans == 0) ? 32'd1 : 32'(vlans));

    // Chapter 12.4 Section 10's rate, summed over every VLAN.
    trunk_bcast_flat      = 32'(trunk_per_s(int'(ports), 1, int'(b_per_station_s)));
    trunk_bcast_segmented = 32'(trunk_per_s(int'(ports), int'(vlans),
                                            int'(b_per_station_s)));

    trunk_relief_ppm = (trunk_bcast_flat == 0) ? 32'sd0
                     : $signed((32'(trunk_bcast_flat)
                                - 32'(trunk_bcast_segmented)) * 1_000_000)
                       / $signed(32'(trunk_bcast_flat));

    // And the tag, which the trunk pays and the access ports do not.
    trunk_tag_cost_ppm = 32'(tag_cost_ppm(int'(mean_frame_octets)));

    // Broadcast bandwidth on the trunk, for scale.
    trunk_bcast_bps = trunk_bcast_segmented
                    * (32'(mean_frame_octets) + 32'(OCT_FIXED) + 32'(OCT_TAG))
                    * 32'd8;
    trunk_bcast_share_ppm = (trunk_rate_gbps == 0) ? 32'd0
                          : (trunk_bcast_bps / (32'(trunk_rate_gbps) * 1000));

    // THE two structural facts.
    segmentation_relieves_trunk = (trunk_relief_ppm > 32'sd0);
    trunk_pays_the_tag          = 1'b1;
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) c_evaluations <= '0;
    else        c_evaluations <= c_evaluations + 32'd1;
  end
endmodule

// ---------------------------------------------------------------------
// tag_realign_cost -- what inserting four octets mid-frame costs a
// datapath, and what the widened key costs a table at Chapter 23.3's
// scale.
//
// The output that matters is on_critical_path, which is high: the
// realignment sits in the middle of the fastest path in the design,
// and its cost is a timing margin rather than an area.
// ---------------------------------------------------------------------
module tag_realign_cost
  import vlanperf_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,

  input  logic [15:0] datapath_bits,
  input  logic [15:0] max_tags,
  input  logic [31:0] table_entries,
  input  logic [15:0] key_bits_before,
  input  logic [15:0] key_bits_after,

  output logic [15:0] shift_positions,
  output logic [15:0] mux_ways,
  output logic [31:0] realign_ge,
  output logic [31:0] holdover_flops,
  output logic [31:0] key_growth_bits,
  output logic [31:0] table_growth_bce,
  output logic [31:0] table_growth_dp_milli,
  output logic [15:0] table_growth_pct,
  output logic        on_critical_path,
  output logic        occupancy_fractions_move,
  output logic [31:0] c_evaluations
);
  always_comb begin
    // A tag stack of 0..max_tags means a shift of 0, 4, 8, ... octets.
    shift_positions = max_tags + 16'd1;
    mux_ways        = shift_positions;

    // One mux per datapath bit, about 3 GE per 2:1 way.
    realign_ge = 32'(datapath_bits) * 32'(mux_ways - 16'd1) * 32'd3;

    // The octets carried across a beat boundary.
    holdover_flops = 32'(max_tags) * 32'd32;

    // Chapter 13.4 Section 8's widening, at Chapter 23.3's scale.
    key_growth_bits  = 32'(key_bits_after) - 32'(key_bits_before);
    table_growth_bce = table_entries * key_growth_bits;
    table_growth_dp_milli = 32'(datapaths_milli(table_growth_bce));
    table_growth_pct = (key_bits_before == 0) ? 16'd0
                     : 16'((key_growth_bits * 32'd100) / 32'(key_bits_before));

    // Chapter 13.2 Section 2: four octets is a fraction of a word on
    // every datapath wider than 32 bits, so it misaligns everything
    // after it -- in the middle of the fastest path in the design.
    on_critical_path = (datapath_bits > 16'd32);

    // Chapter 13.4 Section 8's structural result: the key's width
    // appears nowhere in a balls-in-bins calculation.
    occupancy_fractions_move = 1'b0;
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) c_evaluations <= '0;
    else        c_evaluations <= c_evaluations + 32'd1;
  end
endmodule

improvement ≈ flood_share × (copies_flat − copies_segmented) ÷ mean_copies_flat
and the tag costs 4.76% of the trunk's wire at minimum frame size
so segmentation pays when   flood_share × (copies_flat − copies_segmented)
                          > tag_cost × mean_copies_flat

// ---------------------------------------------------------------------
// benefit_auditor -- which of segmentation's claimed benefits this
// deployment will actually receive, given its own counters.
//
// The output that matters is bandwidth_benefit, which is hard-wired
// zero. Every other benefit this module reports is about a scope.
// ---------------------------------------------------------------------
module benefit_auditor
  import vlanperf_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,

  input  logic [47:0] c_flooded,
  input  logic [47:0] c_forwarded,
  input  logic [15:0] ports,
  input  logic [15:0] vlans,
  input  logic [15:0] mean_frame_octets,
  input  logic [15:0] b_per_station_s,
  input  logic [15:0] cpu_budget_fps,

  output logic [31:0] flood_share_ppm,
  output logic [31:0] egress_improvement_ppm,
  output logic [31:0] tag_cost_ppm_o,
  output logic signed [31:0] net_ppm,
  output logic        worth_the_tag,
  output logic [31:0] cpu_improvement_ppm,
  output logic        cpu_benefit_unconditional,
  output logic [31:0] blast_radius_before,
  output logic [31:0] blast_radius_after,
  output logic        bandwidth_benefit,
  output logic [31:0] c_audits
);
  logic [31:0] copies_flat, copies_seg, mean_flat_x1000, mean_seg_x1000;

  always_comb begin
    flood_share_ppm = (c_forwarded == 0) ? 32'd0
                    : 32'((c_flooded * 48'd1_000_000) / c_forwarded);

    copies_flat = 32'(flood_copies(int'(ports), 1));
    copies_seg  = 32'(flood_copies(int'(ports), int'(vlans)));

    mean_flat_x1000 = 32'd1000
                    + ((flood_share_ppm * (copies_flat - 32'd1)) / 32'd1000);
    mean_seg_x1000  = 32'd1000
                    + ((flood_share_ppm * (copies_seg - 32'd1)) / 32'd1000);

    egress_improvement_ppm = (mean_flat_x1000 == 0) ? 32'd0
      : (((mean_flat_x1000 - mean_seg_x1000) * 1_000_000) / mean_flat_x1000);

    tag_cost_ppm_o = 32'(tag_cost_ppm(int'(mean_frame_octets)));

    net_ppm = $signed(egress_improvement_ppm) - $signed(tag_cost_ppm_o);
    worth_the_tag = (net_ppm > 32'sd0);

    // The unconditional benefit: a broadcast is always flooded, so the
    // per-station CPU load falls with the domain size regardless of
    // what the flood share is.
    cpu_improvement_ppm = (copies_flat == 0) ? 32'd0
      : (((copies_flat - copies_seg) * 1_000_000) / copies_flat);
    cpu_benefit_unconditional = 1'b1;

    blast_radius_before = copies_flat + 32'd1;
    blast_radius_after  = copies_seg + 32'd1;

    // THE constant. Section 2's conservation law, as a bit.
    bandwidth_benefit = 1'b0;
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) c_audits <= '0;
    else        c_audits <= c_audits + 32'd1;
  end
endmodule

// ---------------------------------------------------------------------
// vlanperf_telemetry -- the counters that make a segmentation claim
// checkable against the deployment it was made about.
//
// Design rule: every claimed benefit gets a counter, and the claim
// that has no counter is the one to disbelieve.
// ---------------------------------------------------------------------
module vlanperf_telemetry
  import vlanperf_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,
  input  logic        clear,

  input  logic        frame_valid,
  input  logic        frame_tagged,
  input  logic        frame_flooded,
  input  logic        frame_broadcast,
  input  logic        frame_unknown_unicast,
  input  logic        frame_crossed_router,
  input  logic        on_trunk,
  input  logic [15:0] frame_octets,
  input  logic [15:0] copies_emitted,

  output logic [47:0] c_frames,
  output logic [47:0] c_tagged,
  output logic [47:0] c_flooded_o,
  output logic [47:0] c_broadcast,
  output logic [47:0] c_unknown_unicast,
  output logic [47:0] c_cross_vlan,
  output logic [47:0] c_trunk_frames,
  output logic [47:0] c_trunk_tag_octets,
  output logic [47:0] c_copies,
  output logic [31:0] flood_share_ppm_o,
  output logic [31:0] mean_copies_x1000,
  output logic [31:0] cross_vlan_ppm,
  output logic [31:0] trunk_tag_overhead_ppm,
  output logic        flood_is_unknown_unicast_dominated
);
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n || clear) begin
      c_frames <= '0; c_tagged <= '0; c_flooded_o <= '0;
      c_broadcast <= '0; c_unknown_unicast <= '0; c_cross_vlan <= '0;
      c_trunk_frames <= '0; c_trunk_tag_octets <= '0; c_copies <= '0;
    end else if (frame_valid) begin
      c_frames <= c_frames + 48'd1;
      c_copies <= c_copies + 48'(copies_emitted);
      if (frame_tagged)          c_tagged          <= c_tagged + 48'd1;
      if (frame_flooded)         c_flooded_o       <= c_flooded_o + 48'd1;
      if (frame_broadcast)       c_broadcast       <= c_broadcast + 48'd1;
      if (frame_unknown_unicast) c_unknown_unicast <= c_unknown_unicast + 48'd1;
      if (frame_crossed_router)  c_cross_vlan      <= c_cross_vlan + 48'd1;
      if (on_trunk) begin
        c_trunk_frames     <= c_trunk_frames + 48'd1;
        c_trunk_tag_octets <= c_trunk_tag_octets + 48'(OCT_TAG);
      end
    end
  end

  always_comb begin
    flood_share_ppm_o = (c_frames == 0) ? 32'd0
                      : 32'((c_flooded_o * 48'd1_000_000) / c_frames);

    mean_copies_x1000 = (c_frames == 0) ? 32'd0
                      : 32'((c_copies * 48'd1000) / c_frames);

    // Section 2's callout: a split conversation costs the switch twice.
    cross_vlan_ppm = (c_frames == 0) ? 32'd0
                   : 32'((c_cross_vlan * 48'd1_000_000) / c_frames);

    // Section 8: the trunk pays 4 octets a frame and nothing else does.
    trunk_tag_overhead_ppm = (c_trunk_frames == 0) ? 32'd0
      : 32'((c_trunk_tag_octets * 48'd1_000_000)
            / (c_trunk_frames * 48'd84));

    // Section 5's production note: three flood causes, three verdicts.
    flood_is_unknown_unicast_dominated =
      (c_flooded_o != 48'd0) && (c_unknown_unicast > c_broadcast);
  end
endmodule

// ---------------------------------------------------------------------
// vlanperf_conformance -- the checks that hold a segmentation claim to
// the quantity it actually moved.
//
// There is no check that throughput improved, because Section 2
// establishes it cannot. Every check here is about a claim's shape.
// ---------------------------------------------------------------------
module vlanperf_conformance
  import vlanperf_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,

  input  logic        claims_bandwidth_gain,
  input  logic        claims_trunk_relief,
  input  logic        claims_flood_reduction,
  input  logic        flood_share_measured,
  input  logic [31:0] flood_share_ppm_i,
  input  logic        segmented_to_fix_unknown_unicast,
  input  logic        flood_is_uu_dominated_i,
  input  logic [31:0] cross_vlan_ppm_i,
  input  logic [31:0] cross_vlan_budget_ppm,
  input  logic signed [31:0] net_ppm_i,

  output logic        v_bandwidth_claim,
  output logic        v_trunk_relief_claim,
  output logic        v_flood_claim_unmeasured,
  output logic        v_symptom_treated,
  output logic        v_cross_vlan_excessive,
  output logic        v_net_negative,
  output logic  [5:0] violations,
  output logic        conformant
);
  always_comb begin
    // 1. Section 2 -- there is no term for it.
    v_bandwidth_claim = claims_bandwidth_gain;

    // 2. Section 8 -- 320/s at every VLAN count.
    v_trunk_relief_claim = claims_trunk_relief;

    // 3. Section 5 -- a width reduction is worth the flood share.
    v_flood_claim_unmeasured = claims_flood_reduction && !flood_share_measured;

    // 4. Section 10 -- the cause is the table.
    v_symptom_treated = segmented_to_fix_unknown_unicast
                     && flood_is_uu_dominated_i;

    // 5. Section 2's callout -- a split conversation costs twice.
    v_cross_vlan_excessive = (cross_vlan_ppm_i > cross_vlan_budget_ppm);

    // 6. Section 12 -- the tag is not free.
    v_net_negative = flood_share_measured && (net_ppm_i <= 32'sd0);

    violations = { v_net_negative, v_cross_vlan_excessive, v_symptom_treated,
                   v_flood_claim_unmeasured, v_trunk_relief_claim,
                   v_bandwidth_claim };
    conformant = (violations == 6'b000000);
  end
endmodule

read c_flooded ÷ c_forwarded
above about 0.1%, segmentation pays for its tag
below it, segment for scope, containment and policy — not for throughput

// A1. Aggregate capacity does not depend on the VLAN count.
p_cn_conserved: assert property (@(posedge clk) disable iff (!rst_n)
  (aggregate_gbps_after == aggregate_gbps_before));

// A2. And the delta is zero, always.
p_cn_delta_zero: assert property (@(posedge clk) disable iff (!rst_n)
  (throughput_delta_ppm == 32'sd0));

// A3. The model reports conservation.
p_cn_reports: assert property (@(posedge clk) disable iff (!rst_n)
  capacity_is_conserved);

// A4. A tagged slot is four octets longer.
p_cn_slot: assert property (@(posedge clk) disable iff (!rst_n)
  (slot_tagged == slot_untagged + 32'(OCT_TAG)));

// A5. Tagging always lowers efficiency.
p_cn_eff_falls: assert property (@(posedge clk) disable iff (!rst_n)
  (eff_tagged_ppm < eff_untagged_ppm));

// A6. And the model says the only bandwidth effect is negative.
p_cn_negative: assert property (@(posedge clk) disable iff (!rst_n)
  tagged |-> only_effect_is_negative);

// A7. The tag's cost falls as the frame grows -- Chapter 8.3's curve.
p_cn_hyperbola: assert property (@(posedge clk) disable iff (!rst_n)
  (payload_octets > $past(payload_octets)) |->
    (tag_cost_ppm_o <= $past(tag_cost_ppm_o)));

// A8. At minimum frame size it is 47 619 ppm.
p_cn_min_frame: assert property (@(posedge clk) disable iff (!rst_n)
  (payload_octets == 16'd46) |-> (tag_cost_ppm_o == 32'd47_619));

// A9. The VLAN count enters no capacity expression.
p_cn_vlans_absent: assert property (@(posedge clk) disable iff (!rst_n)
  (vlans != $past(vlans)) |-> (aggregate_gbps_after == $past(aggregate_gbps_after)));

// B1. Copies are the member count less one.
p_fw_copies: assert property (@(posedge clk) disable iff (!rst_n)
  (copies_segmented == members_per_vlan - 16'd1));

// B2. Segmenting never raises the copy count.
p_fw_monotone: assert property (@(posedge clk) disable iff (!rst_n)
  (vlans >= 16'd1) |-> (copies_segmented <= copies_flat));

// B3. One VLAN is the flat case.
p_fw_one_vlan: assert property (@(posedge clk) disable iff (!rst_n)
  (vlans == 16'd1) |-> (copies_segmented == copies_flat));

// B4. The width share is the ratio of the two.
p_fw_share: assert property (@(posedge clk) disable iff (!rst_n)
  (copies_flat != 16'd0) |->
    (width_share_ppm == (32'(copies_segmented) * 1_000_000) / 32'(copies_flat)));

// B5. THE qualifier: no flooding, no improvement.
p_fw_needs_flooding: assert property (@(posedge clk) disable iff (!rst_n)
  (flood_share_ppm == 32'd0) |-> (improvement_ppm == 32'd0));

// B6. And with flooding there is one.
p_fw_has_improvement: assert property (@(posedge clk) disable iff (!rst_n)
  ((flood_share_ppm != 32'd0) && (vlans > 16'd1)) |-> (improvement_ppm != 32'd0));

// B7. The improvement never exceeds unity.
p_fw_bounded: assert property (@(posedge clk) disable iff (!rst_n)
  (improvement_ppm <= 32'd1_000_000));

// B8. Emissions are copies times the port rate.
p_fw_emissions: assert property (@(posedge clk) disable iff (!rst_n)
  (emissions_flat_k == port_pps_k * 32'(copies_flat)));

// B9. One flooding port at 64 ports takes most of the budget.
p_fw_budget: assert property (@(posedge clk) disable iff (!rst_n)
  ((ports == 16'd64) && (port_pps_k == 32'd148_810) &&
   (switch_budget_pps_k == 32'd9_524_000))
    |-> (budget_share_flat_ppm >= 32'd980_000));

// C1. The domain is the fabric, not the switch.
p_dr_domain: assert property (@(posedge clk) disable iff (!rst_n)
  (stations_in_domain == 32'(ports_per_switch) * 32'(switches_in_domain)));

// C2. Each station receives the others' broadcasts.
p_dr_rx: assert property (@(posedge clk) disable iff (!rst_n)
  (stations_in_domain != 0) |-> (rx_per_station_s <
    (stations_in_domain * 32'(b_per_station_s)) + 32'd1));

// C3. More VLANs never raises the per-station rate.
p_dr_monotone: assert property (@(posedge clk) disable iff (!rst_n)
  (vlans > $past(vlans)) |-> (rx_per_station_s <= $past(rx_per_station_s)));

// C4. The switch cannot determine the domain's extent.
p_dr_unknowable: assert property (@(posedge clk) disable iff (!rst_n)
  (switch_can_determine_this == 1'b0));

// C5. Spanning switches is reported.
p_dr_spans: assert property (@(posedge clk) disable iff (!rst_n)
  (switches_in_domain > 16'd1) |-> domain_spans_switches);

// C6. Within budget is a comparison and nothing else.
p_dr_budget: assert property (@(posedge clk) disable iff (!rst_n)
  within_budget |-> (rx_per_station_s <= 32'(cpu_budget_fps)));

// C7. Over budget is counted.
p_dr_counted: assert property (@(posedge clk) disable iff (!rst_n)
  !within_budget |=> (c_over_budget == $past(c_over_budget) + 32'd1));

// C8. CPU microseconds follow the frame rate.
p_dr_cpu: assert property (@(posedge clk) disable iff (!rst_n)
  (cpu_us_per_s == rx_per_station_s * 32'(us_per_frame)));

// D1. The trunk's broadcast load is the station count times B.
p_tk_load: assert property (@(posedge clk) disable iff (!rst_n)
  (trunk_bcast_segmented == 32'(trunk_per_s(int'(ports), int'(vlans),
                                            int'(b_per_station_s)))));

// D2. And it does not depend on the VLAN count.
p_tk_invariant: assert property (@(posedge clk) disable iff (!rst_n)
  (trunk_bcast_segmented == trunk_bcast_flat));

// D3. So the relief is zero.
p_tk_no_relief: assert property (@(posedge clk) disable iff (!rst_n)
  (trunk_relief_ppm == 32'sd0));

// D4. And the model says so.
p_tk_reports: assert property (@(posedge clk) disable iff (!rst_n)
  !segmentation_relieves_trunk);

// D5. The trunk pays the tag.
p_tk_pays: assert property (@(posedge clk) disable iff (!rst_n)
  trunk_pays_the_tag);

// D6. The tag cost is Chapter 24.3's arithmetic with four octets.
p_tk_tag_cost: assert property (@(posedge clk) disable iff (!rst_n)
  (trunk_tag_cost_ppm == 32'(tag_cost_ppm(int'(mean_frame_octets)))));

// D7. Broadcast bandwidth is a small share of a fast trunk.
p_tk_small: assert property (@(posedge clk) disable iff (!rst_n)
  ((trunk_rate_gbps >= 16'd100) && (trunk_bcast_segmented <= 32'd1000))
    |-> (trunk_bcast_share_ppm <= 32'd100));

// D8. Station count is preserved across segmentation.
p_tk_stations: assert property (@(posedge clk) disable iff (!rst_n)
  (vlans != 16'd0) |-> (stations == 32'(ports)));

// E1. Shift positions are the tag depth plus one.
p_rl_positions: assert property (@(posedge clk) disable iff (!rst_n)
  (shift_positions == max_tags + 16'd1));

// E2. The realignment is on the critical path above 32 bits.
p_rl_critical: assert property (@(posedge clk) disable iff (!rst_n)
  (datapath_bits > 16'd32) |-> on_critical_path);

// E3. The key's width does not move the occupancy fractions.
p_rl_fractions: assert property (@(posedge clk) disable iff (!rst_n)
  (occupancy_fractions_move == 1'b0));

// E4. Table growth is entries times the added bits.
p_rl_growth: assert property (@(posedge clk) disable iff (!rst_n)
  (table_growth_bce == table_entries * key_growth_bits));

// E5. A 48-to-60-bit key is a 25% growth.
p_rl_25pct: assert property (@(posedge clk) disable iff (!rst_n)
  ((key_bits_before == 16'd48) && (key_bits_after == 16'd60))
    |-> (table_growth_pct == 16'd25));

// E6. The auditor's bandwidth benefit is zero.
p_au_no_bandwidth: assert property (@(posedge clk) disable iff (!rst_n)
  (bandwidth_benefit == 1'b0));

// E7. And the CPU benefit is unconditional.
p_au_cpu: assert property (@(posedge clk) disable iff (!rst_n)
  cpu_benefit_unconditional);

// E8. Worth-the-tag requires a positive net.
p_au_worth: assert property (@(posedge clk) disable iff (!rst_n)
  worth_the_tag |-> (net_ppm > 32'sd0));

// E9. The blast radius shrinks with the VLAN count.
p_au_radius: assert property (@(posedge clk) disable iff (!rst_n)
  (vlans > 16'd1) |-> (blast_radius_after <= blast_radius_before));

// F1. Flooded frames are a subset of frames.
p_tl_subset: assert property (@(posedge clk) disable iff (!rst_n)
  (c_flooded_o <= c_frames));

// F2. The flood share is the ratio the decision rule needs.
p_tl_share: assert property (@(posedge clk) disable iff (!rst_n)
  (c_frames != 48'd0) |->
    (flood_share_ppm_o == 32'((c_flooded_o * 48'd1_000_000) / c_frames)));

// F3. Mean copies is at least one.
p_tl_mean: assert property (@(posedge clk) disable iff (!rst_n)
  (c_frames != 48'd0) |-> (mean_copies_x1000 >= 32'd1000));

// F4. A bandwidth claim is always a violation.
p_cf_bandwidth: assert property (@(posedge clk) disable iff (!rst_n)
  claims_bandwidth_gain |-> v_bandwidth_claim);

// F5. So is a trunk-relief claim.
p_cf_trunk: assert property (@(posedge clk) disable iff (!rst_n)
  claims_trunk_relief |-> v_trunk_relief_claim);

// F6. A flood claim needs the share measured.
p_cf_measured: assert property (@(posedge clk) disable iff (!rst_n)
  (claims_flood_reduction && !flood_share_measured) |-> v_flood_claim_unmeasured);

// F7. Segmenting to fix unknown unicast treats a symptom.
p_cf_symptom: assert property (@(posedge clk) disable iff (!rst_n)
  (segmented_to_fix_unknown_unicast && flood_is_uu_dominated_i)
    |-> v_symptom_treated);

// F8. Conformance is the disjunction of its six checks.
p_cf_vector: assert property (@(posedge clk) disable iff (!rst_n)
  conformant |-> (violations == 6'b000000));

c_cn_min_frame:  cover property (@(posedge clk) payload_octets <= 16'd46);
c_cn_jumbo:      cover property (@(posedge clk) payload_octets >= 16'd9000);
c_fw_no_flood:   cover property (@(posedge clk) flood_share_ppm == 32'd0);
c_fw_heavy:      cover property (@(posedge clk) flood_share_ppm >= 32'd195_000);
c_fw_32_vlans:   cover property (@(posedge clk) vlans == 16'd32);
c_dr_multiswitch:cover property (@(posedge clk) switches_in_domain >= 16'd4);
c_dr_over:       cover property (@(posedge clk) !within_budget);
c_tk_relief:     cover property (@(posedge clk) segmentation_relieves_trunk);
c_rl_two_tags:   cover property (@(posedge clk) max_tags == 16'd2);
c_rl_1024:       cover property (@(posedge clk) datapath_bits == 16'd1024);
c_au_marginal:   cover property (@(posedge clk) (net_ppm > 32'sd0) && (net_ppm < 32'sd10_000));
c_au_negative:   cover property (@(posedge clk) net_ppm <= 32'sd0);
c_tl_uu_dom:     cover property (@(posedge clk) flood_is_unknown_unicast_dominated);
c_cf_symptom:    cover property (@(posedge clk) v_symptom_treated);