Unicast, Multicast and Broadcast

// SYNTHESIZABLE. Group-address filtering by hash.
//
// Chapter 2.7 §4 used an exact-match table and said production designs
// hash. This is that, and the naming is deliberate:
//
//   THE OUTPUT IS `maybe_subscribed`, NOT `subscribed`.
//
// A consumer that reads a signal called `subscribed` will treat it as
// exact. One that reads `maybe_subscribed` cannot. The name is doing real
// work -- it is the interface where the imprecision becomes visible, and
// Section 4 showed what goes wrong when it is not.
//
// THE ONE-SIDED GUARANTEE, and it holds by construction:
//   a subscribed address sets its bit when programmed, so a frame carrying
//   that address always finds the bit set. NO SUBSCRIBED ADDRESS CAN EVER
//   BE REJECTED. Collisions produce false positives only.
package group_filter_pkg;
  // Vector width. Larger means fewer collisions and more flops -- Section 6
  // does the arithmetic. 64 and 512 are both common.
  parameter int unsigned HASH_BITS = 64;
  parameter int unsigned HASH_W    = $clog2(HASH_BITS);
endpackage
 
module group_hash_filter
  import macaddr_pkg::*;
  import group_filter_pkg::*;
#(
  parameter int unsigned CNT_W = 24
) (
  input  logic        clk,
  input  logic        rst_n,
 
  // From Chapter 5.3's decomposer.
  input  logic        addr_valid,
  input  logic [47:0] address,
  input  logic        is_group,
  input  logic        is_broadcast,
 
  // The subscription vector, programmed by software (Section 6).
  input  logic [HASH_BITS-1:0] hash_vector,
  // Accept every group address regardless of the vector. A real mode, and
  // distinct from promiscuous -- Chapter 2.7 §4 kept those apart and so
  // does this.
  input  logic        accept_all_multicast,
 
  output logic        result_valid,
 
  // ── The three outcomes, deliberately not two ────────────────────────────
  // Broadcast is accepted unconditionally and BYPASSES the filter entirely.
  // Section 10 explains why it is not "multicast to everyone".
  output logic        accept_broadcast,
  // The honest name. Software must still compare exactly.
  output logic        maybe_subscribed,
  // A definite answer, and the one that disposes of most traffic.
  output logic        definitely_not_subscribed,
 
  output logic [HASH_W-1:0] hash_index,
 
  output logic [CNT_W-1:0] c_group_frames,
  output logic [CNT_W-1:0] c_hardware_rejected,
  output logic [CNT_W-1:0] c_delivered_maybe
);
 
  function automatic logic [CNT_W-1:0] bump(input logic [CNT_W-1:0] v,
                                            input logic             en);
    bump = (en && !(&v)) ? (v + 1'b1) : v;   // saturating
  endfunction
 
  // The hash. A CRC over the address, of which some bits index the vector,
  // is the conventional choice -- it spreads structured addresses well,
  // and group addresses are HEAVILY structured (Section 8), so a naive
  // hash such as the low bits would collide catastrophically.
  //
  // This is a compact CRC-style reduction, not any specific standard's.
  function automatic logic [HASH_W-1:0] addr_hash(input logic [47:0] a);
    automatic logic [31:0] crc = 32'hFFFF_FFFF;
    for (int unsigned i = 0; i < 48; i++) begin
      automatic logic fb = crc[31] ^ a[i];
      crc = {crc[30:0], 1'b0};
      if (fb) crc = crc ^ 32'h04C1_1DB7;
    end
    addr_hash = crc[31 -: HASH_W];
  endfunction
 
  logic [HASH_W-1:0] idx_c;
  assign idx_c = addr_hash(address);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      result_valid              <= 1'b0;
      accept_broadcast          <= 1'b0;
      maybe_subscribed          <= 1'b0;
      definitely_not_subscribed <= 1'b0;
      hash_index                <= '0;
      c_group_frames            <= '0;
      c_hardware_rejected       <= '0;
      c_delivered_maybe         <= '0;
    end else begin
      result_valid              <= 1'b0;
      accept_broadcast          <= 1'b0;
      maybe_subscribed          <= 1'b0;
      definitely_not_subscribed <= 1'b0;
 
      if (addr_valid && is_group) begin
        result_valid   <= 1'b1;
        hash_index     <= idx_c;
        c_group_frames <= bump(c_group_frames, 1'b1);
 
        if (is_broadcast) begin
          // Unconditional, and it does not consult the vector at all.
          accept_broadcast <= 1'b1;
        end else if (accept_all_multicast) begin
          maybe_subscribed  <= 1'b1;
          c_delivered_maybe <= bump(c_delivered_maybe, 1'b1);
        end else if (hash_vector[idx_c]) begin
          // SOME subscribed address maps here. Possibly this one.
          maybe_subscribed  <= 1'b1;
          c_delivered_maybe <= bump(c_delivered_maybe, 1'b1);
        end else begin
          // NO subscribed address maps here. Definite, and cheap.
          definitely_not_subscribed <= 1'b1;
          c_hardware_rejected       <= bump(c_hardware_rejected, 1'b1);
        end
      end
    end
  end
 
endmodule

P(bit set) = 1 − (1 − 1/m)^k  ≈  1 − exp(−k/m)

m = 64,  k =  4  →  about 6%
m = 64,  k = 16  →  about 22%
m = 64,  k = 32  →  about 39%
m = 64,  k = 64  →  about 63%
 
m = 512, k = 16  →  about 3%
m = 512, k = 64  →  about 12%

// SYNTHESIZABLE. Subscription state and vector maintenance.
//
// SUBSCRIBING IS EASY: set the bit the address hashes to.
//
// UNSUBSCRIBING IS NOT, and this is the module's reason for existing.
// Several subscribed addresses can hash to the same bit. Clearing that bit
// when one of them unsubscribes SILENTLY UNSUBSCRIBES THE OTHERS -- and
// the failure is invisible, because the filter then correctly rejects
// frames the station still wanted. Section 4's unrecoverable direction.
//
// So the exact list must be kept and the vector REBUILT from it. The vector
// is a derived cache, never the source of truth.
module subscription_manager
  import macaddr_pkg::*;
  import group_filter_pkg::*;
#(
  parameter int unsigned MAX_GROUPS = 32,
  parameter int unsigned IDX_W      = $clog2(MAX_GROUPS),
  parameter int unsigned CNT_W      = 16
) (
  input  logic        clk,
  input  logic        rst_n,
 
  input  logic        subscribe_req,
  input  logic        unsubscribe_req,
  input  logic [47:0] group_address,
  output logic        req_done,
  output logic        req_rejected,     // the list is full
 
  // The derived vector, consumed by Section 5's filter.
  output logic [HASH_BITS-1:0] hash_vector,
  output logic                 vector_rebuilding,
 
  // The exact list, which software uses to complete the match (Section 8).
  output logic [47:0]      group_list  [MAX_GROUPS],
  output logic [MAX_GROUPS-1:0] group_valid,
 
  output logic [CNT_W-1:0] c_subscribed,
  output logic [CNT_W-1:0] c_unsubscribed,
  output logic [CNT_W-1:0] c_rebuilds,
 
  // Subscriptions currently held, and how full the vector is. Section 6
  // showed the false-positive rate follows from both, so a design that
  // cannot read them cannot know its own rate.
  output logic [IDX_W:0]        active_groups,
  output logic [$clog2(HASH_BITS+1)-1:0] vector_bits_set
);
 
  logic [47:0]           list_q [MAX_GROUPS];
  logic [MAX_GROUPS-1:0] valid_q;
  logic [HASH_BITS-1:0]  vector_q;
  logic [IDX_W:0]        rebuild_idx_q;
  logic                  rebuilding_q;
 
  function automatic logic [CNT_W-1:0] bump(input logic [CNT_W-1:0] v,
                                            input logic             en);
    bump = (en && !(&v)) ? (v + 1'b1) : v;
  endfunction
 
  function automatic logic [HASH_W-1:0] addr_hash(input logic [47:0] a);
    automatic logic [31:0] crc = 32'hFFFF_FFFF;
    for (int unsigned i = 0; i < 48; i++) begin
      automatic logic fb = crc[31] ^ a[i];
      crc = {crc[30:0], 1'b0};
      if (fb) crc = crc ^ 32'h04C1_1DB7;
    end
    addr_hash = crc[31 -: HASH_W];
  endfunction
 
  logic                found_c;
  logic [IDX_W-1:0]    found_idx_c;
  logic                free_c;
  logic [IDX_W-1:0]    free_idx_c;
 
  always_comb begin
    found_c = 1'b0; found_idx_c = '0;
    free_c  = 1'b0; free_idx_c  = '0;
    for (int unsigned i = 0; i < MAX_GROUPS; i++) begin
      if (valid_q[i] && (list_q[i] == group_address)) begin
        found_c     = 1'b1;
        found_idx_c = (IDX_W)'(i);
      end
      if (!valid_q[i] && !free_c) begin
        free_c     = 1'b1;
        free_idx_c = (IDX_W)'(i);
      end
    end
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (int unsigned i = 0; i < MAX_GROUPS; i++) list_q[i] <= '0;
      valid_q        <= '0;
      vector_q       <= '0;
      rebuilding_q   <= 1'b0;
      rebuild_idx_q  <= '0;
      req_done       <= 1'b0;
      req_rejected   <= 1'b0;
      c_subscribed   <= '0;
      c_unsubscribed <= '0;
      c_rebuilds     <= '0;
    end else begin
      req_done     <= 1'b0;
      req_rejected <= 1'b0;
 
      if (rebuilding_q) begin
        // Rebuild the vector from the exact list, one entry per cycle.
        // DURING THE REBUILD THE VECTOR IS INCOMPLETE, which would drop
        // wanted frames -- so Section 5's filter must be told. That is what
        // vector_rebuilding is for, and Section 11 asserts it.
        if (rebuild_idx_q == (IDX_W+1)'(MAX_GROUPS)) begin
          rebuilding_q <= 1'b0;
          req_done     <= 1'b1;
        end else begin
          if (valid_q[rebuild_idx_q[IDX_W-1:0]])
            vector_q[addr_hash(list_q[rebuild_idx_q[IDX_W-1:0]])] <= 1'b1;
          rebuild_idx_q <= rebuild_idx_q + 1'b1;
        end
      end else if (subscribe_req) begin
        if (found_c) begin
          req_done <= 1'b1;              // already subscribed
        end else if (free_c) begin
          list_q[free_idx_c]  <= group_address;
          valid_q[free_idx_c] <= 1'b1;
          // Adding is safe to do incrementally: setting a bit can only
          // create false positives, never false negatives.
          vector_q[addr_hash(group_address)] <= 1'b1;
          c_subscribed <= bump(c_subscribed, 1'b1);
          req_done     <= 1'b1;
        end else begin
          req_rejected <= 1'b1;
        end
      end else if (unsubscribe_req && found_c) begin
        valid_q[found_idx_c] <= 1'b0;
        c_unsubscribed       <= bump(c_unsubscribed, 1'b1);
        // THE POINT OF THE MODULE. The bit cannot simply be cleared --
        // another subscribed address may hash to it. Clear the whole
        // vector and rebuild from the list that remains.
        vector_q      <= '0;
        rebuilding_q  <= 1'b1;
        rebuild_idx_q <= '0;
        c_rebuilds    <= bump(c_rebuilds, 1'b1);
      end
    end
  end
 
  assign hash_vector       = vector_q;
  assign vector_rebuilding = rebuilding_q;
  assign group_list        = list_q;
  assign group_valid       = valid_q;
 
  always_comb begin
    active_groups   = '0;
    vector_bits_set = '0;
    for (int unsigned i = 0; i < MAX_GROUPS; i++)
      if (valid_q[i]) active_groups = active_groups + 1'b1;
    for (int unsigned b = 0; b < HASH_BITS; b++)
      if (vector_q[b]) vector_bits_set = vector_bits_set + 1'b1;
  end
 
endmodule

// SYNTHESIZABLE. The completion stage, and the measurement that matters.
//
// Hardware said "maybe". This resolves it against the exact list, and --
// more importantly -- COUNTS THE OUTCOME.
//
// Section 6 showed the design-time false-positive formula assumes uniform
// hashing, which real group addresses violate. So the true rate cannot be
// calculated; it must be measured HERE, where both the hardware verdict
// and the exact answer are available together.
module group_match_completion
  import macaddr_pkg::*;
  import group_filter_pkg::*;
#(
  parameter int unsigned MAX_GROUPS = 32,
  parameter int unsigned CNT_W      = 24
) (
  input  logic        clk,
  input  logic        rst_n,
  input  logic        clear,
 
  input  logic        maybe_subscribed,
  input  logic [47:0] address,
  input  logic [47:0] group_list [MAX_GROUPS],
  input  logic [MAX_GROUPS-1:0] group_valid,
 
  output logic        deliver,          // exactly matched: genuinely wanted
  output logic        false_positive,   // hardware said maybe, list says no
 
  output logic [CNT_W-1:0] c_true_positive,
  output logic [CNT_W-1:0] c_false_positive,
 
  // The measured rate, scaled by 256. THE number that says whether the
  // vector is wide enough for THIS deployment -- which Section 6's formula
  // cannot know, because it assumes a uniformity real addresses lack.
  output logic [15:0] false_positive_rate_x256,
 
  // Worst rate seen over any window since reset. Survives `clear`: a rate
  // that was fine at install and is not now means the subscription set or
  // the traffic mix has changed.
  output logic [15:0] worst_rate_x256
);
 
  function automatic logic [CNT_W-1:0] bump(input logic [CNT_W-1:0] v,
                                            input logic             en);
    bump = (en && !(&v)) ? (v + 1'b1) : v;
  endfunction
 
  logic exact_hit_c;
  always_comb begin
    exact_hit_c = 1'b0;
    for (int unsigned i = 0; i < MAX_GROUPS; i++)
      if (group_valid[i] && (group_list[i] == address)) exact_hit_c = 1'b1;
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      deliver          <= 1'b0;
      false_positive   <= 1'b0;
      c_true_positive  <= '0;
      c_false_positive <= '0;
      worst_rate_x256  <= '0;
    end else begin
      deliver        <= 1'b0;
      false_positive <= 1'b0;
 
      if (clear) begin
        c_true_positive  <= '0;
        c_false_positive <= '0;
        // worst_rate_x256 deliberately survives.
      end else if (maybe_subscribed) begin
        if (exact_hit_c) begin
          deliver         <= 1'b1;
          c_true_positive <= bump(c_true_positive, 1'b1);
        end else begin
          // Hardware was wrong, in the survivable direction. Not an error.
          false_positive   <= 1'b1;
          c_false_positive <= bump(c_false_positive, 1'b1);
        end
      end
 
      if (false_positive_rate_x256 > worst_rate_x256)
        worst_rate_x256 <= false_positive_rate_x256;
    end
  end
 
  always_comb begin
    automatic logic [CNT_W:0] total = c_true_positive + c_false_positive;
    false_positive_rate_x256 = (total == 0) ? 16'd0
                             : 16'((c_false_positive * 256) / total);
  end
 
endmodule

// SYNTHESIZABLE INSTRUMENTATION.
//
// The three types cost differently and scale differently (Section 2), so
// the RATIO between them is the diagnostic, not any one count:
//
//   unicast dominant          -> normal. Cost bounded by senders' intent.
//   multicast dominant        -> check the false-positive rate: is this
//                                real subscription traffic or filter noise?
//   BROADCAST dominant        -> every station in the domain is paying, and
//                                the cost scales with domain size rather
//                                than with anything a sender controls.
//
// Broadcast gets its own rate measurement because it is the only type a
// station cannot decline, so it is the only one whose cost is entirely
// outside this station's control.
module address_type_accounting
  import macaddr_pkg::*;
#(
  parameter int unsigned CNT_W  = 32,
  parameter int unsigned WINDOW = 1_000_000,
  parameter int unsigned WIN_W  = $clog2(WINDOW + 1),
  // Broadcast frames per window above which the domain is considered to be
  // in a storm. Illustrative -- a real threshold comes from the deployment.
  parameter int unsigned STORM_THRESHOLD = 1000
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic frame_valid,
  input  logic is_group,
  input  logic is_broadcast,
  input  logic unicast_matched,      // this station's own address
  input  logic delivered,            // survived the exact match
  input  logic false_positive,
 
  output logic [CNT_W-1:0] c_unicast_mine,
  output logic [CNT_W-1:0] c_unicast_other,
  output logic [CNT_W-1:0] c_multicast_delivered,
  output logic [CNT_W-1:0] c_multicast_false,
  output logic [CNT_W-1:0] c_broadcast,
 
  // Broadcast frames in the window that just closed. A RATE, because
  // Chapter 2.7 §12 showed broadcast cost scales with domain size -- so an
  // absolute count says nothing without the interval.
  output logic [CNT_W-1:0] window_broadcast,
  output logic             window_valid,
  output logic             storm_suspected,
 
  // Highest broadcast rate ever seen. Survives `clear`: it describes the
  // domain this station sits in, not a measurement interval.
  output logic [CNT_W-1:0] worst_broadcast_rate
);
 
  logic [WIN_W-1:0]  win_q;
  logic [CNT_W-1:0]  bcast_win_q;
 
  function automatic logic [CNT_W-1:0] bump(input logic [CNT_W-1:0] v,
                                            input logic             en);
    bump = (en && !(&v)) ? (v + 1'b1) : v;
  endfunction
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      c_unicast_mine        <= '0;
      c_unicast_other       <= '0;
      c_multicast_delivered <= '0;
      c_multicast_false     <= '0;
      c_broadcast           <= '0;
      win_q                 <= '0;
      bcast_win_q           <= '0;
      window_broadcast      <= '0;
      window_valid          <= 1'b0;
      storm_suspected       <= 1'b0;
      worst_broadcast_rate  <= '0;
    end else begin
      window_valid <= 1'b0;
 
      if (clear) begin
        c_unicast_mine        <= '0;
        c_unicast_other       <= '0;
        c_multicast_delivered <= '0;
        c_multicast_false     <= '0;
        c_broadcast           <= '0;
        // worst_broadcast_rate deliberately survives.
      end else if (frame_valid) begin
        if (is_broadcast) begin
          c_broadcast <= bump(c_broadcast, 1'b1);
          bcast_win_q <= bump(bcast_win_q, 1'b1);
        end else if (is_group) begin
          c_multicast_delivered <= bump(c_multicast_delivered, delivered);
          c_multicast_false     <= bump(c_multicast_false,     false_positive);
        end else begin
          c_unicast_mine  <= bump(c_unicast_mine,  unicast_matched);
          c_unicast_other <= bump(c_unicast_other, !unicast_matched);
        end
      end
 
      if (win_q == WIN_W'(WINDOW - 1)) begin
        window_broadcast <= bcast_win_q;
        window_valid     <= 1'b1;
        storm_suspected  <= (bcast_win_q >= CNT_W'(STORM_THRESHOLD));
        if (bcast_win_q > worst_broadcast_rate) worst_broadcast_rate <= bcast_win_q;
        bcast_win_q <= '0;
        win_q       <= '0;
      end else begin
        win_q <= win_q + 1'b1;
      end
    end
  end
 
endmodule

// SYNTHESIZABLE DIAGNOSTIC.
//
// The chapter's entire design rests on ONE property:
//
//     every subscribed address hashes to a bit that is SET
//
// A false positive is a cost. A FALSE NEGATIVE is a lost frame, and no
// later stage can recover it -- so this is the only fatal failure mode in
// the receive filter, and it is invisible in traffic: the frame simply
// never arrives, and the station has no record that it existed.
//
// This module walks the subscription list in the background and re-checks
// each entry against the live vector. It is a CONSISTENCY check, not a
// traffic check, which is why it can find the fault before any frame is
// lost rather than after.
module filter_false_negative_monitor
  import macaddr_pkg::*;
#(
  parameter int unsigned MAX_GROUPS = 256,
  parameter int unsigned IDX_W      = $clog2(MAX_GROUPS),
  parameter int unsigned VEC_W      = 512,
  parameter int unsigned HASH_W     = $clog2(VEC_W),
  // Cycles between successive entry checks. The walk is deliberately slow:
  // it must not compete with the receive path for the vector's read port.
  parameter int unsigned PACE       = 64,
  parameter int unsigned PACE_W     = $clog2(PACE + 1)
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  // Subscription list (source of truth).
  input  logic [MAX_GROUPS-1:0]  entry_occupied,
  input  mac_addr_t              entry_addr [MAX_GROUPS],
 
  // Live vector (the derived cache).
  input  logic [VEC_W-1:0]       vector,
 
  // Held low while the vector is being rebuilt: an incomplete vector is
  // EXPECTED to be inconsistent, so checking it would report a fault that
  // is not one.
  input  logic                   vector_stable,
 
  output logic                   inconsistent,       // sticky
  output logic [IDX_W-1:0]       first_bad_entry,    // first cause
  output mac_addr_t              first_bad_addr,
  output logic [HASH_W-1:0]      first_bad_index,
  output logic [31:0]            sweeps_completed
);
 
  logic [IDX_W-1:0] cursor_q;
  logic [PACE_W-1:0] pace_q;
 
  // Same hash the filter uses. Sharing the function is deliberate: a
  // monitor with its own copy of the hash would silently stop checking the
  // thing that matters the moment the two drifted apart.
  function automatic logic [HASH_W-1:0] hash_addr(input mac_addr_t a);
    logic [HASH_W-1:0] h;
    h = '0;
    for (int unsigned i = 0; i < 48; i++)
      h[i % HASH_W] = h[i % HASH_W] ^ a[i];
    hash_addr = h;
  endfunction
 
  wire logic [HASH_W-1:0] cur_index = hash_addr(entry_addr[cursor_q]);
  wire logic              cur_ok    = vector[cur_index];
  wire logic              cur_check = vector_stable && entry_occupied[cursor_q];
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      cursor_q         <= '0;
      pace_q           <= '0;
      inconsistent     <= 1'b0;
      first_bad_entry  <= '0;
      first_bad_addr   <= '0;
      first_bad_index  <= '0;
      sweeps_completed <= '0;
    end else if (clear) begin
      // sweeps_completed is cleared; `inconsistent` is NOT. A filter that
      // was ever inconsistent has already lost frames, and clearing a
      // counter must not erase that.
      sweeps_completed <= '0;
    end else begin
      if (pace_q != PACE_W'(PACE - 1)) begin
        pace_q <= pace_q + 1'b1;
      end else begin
        pace_q <= '0;
 
        if (cur_check && !cur_ok && !inconsistent) begin
          inconsistent    <= 1'b1;
          first_bad_entry <= cursor_q;
          first_bad_addr  <= entry_addr[cursor_q];
          first_bad_index <= cur_index;
        end
 
        if (cursor_q == IDX_W'(MAX_GROUPS - 1)) begin
          cursor_q         <= '0;
          sweeps_completed <= sweeps_completed + 1'b1;
        end else begin
          cursor_q <= cursor_q + 1'b1;
        end
      end
    end
  end
 
endmodule

// ---------------------------------------------------------------------
// P1 -- THE ONLY FATAL PROPERTY.
// A subscribed address must never be rejected. Everything else in this
// chapter is a cost; this is a lost frame.
// ---------------------------------------------------------------------
property p_no_false_negative;
  @(posedge clk) disable iff (!rst_n)
    (frame_valid && is_group && !is_broadcast && addr_is_subscribed && vector_stable)
      |-> maybe_subscribed;
endproperty
a_no_false_negative: assert property (p_no_false_negative)
  else $error("FATAL: subscribed group address rejected by the filter");
 
// ---------------------------------------------------------------------
// P2 -- Broadcast bypasses the filter entirely (Section 10). A station
// must not be able to configure itself into not receiving broadcast.
// ---------------------------------------------------------------------
property p_broadcast_always_accepted;
  @(posedge clk) disable iff (!rst_n)
    (frame_valid && is_broadcast) |-> accept;
endproperty
a_broadcast_always_accepted: assert property (p_broadcast_always_accepted);
 
// ---------------------------------------------------------------------
// P3 -- A clear bit is a DEFINITE answer, so it must dispose of the frame
// in hardware. If a cleared bit still reached software, the cheap stage
// would not be saving anything.
// ---------------------------------------------------------------------
property p_clear_bit_drops_in_hardware;
  @(posedge clk) disable iff (!rst_n)
    (frame_valid && is_group && !is_broadcast && !maybe_subscribed)
      |-> !deliver_to_software;
endproperty
a_clear_bit_drops_in_hardware: assert property (p_clear_bit_drops_in_hardware);
 
// ---------------------------------------------------------------------
// P4 -- Subscribing takes effect immediately: one write, and the bit is
// set on the next cycle (Section 11's short path out of STABLE).
// ---------------------------------------------------------------------
property p_subscribe_sets_bit;
  @(posedge clk) disable iff (!rst_n)
    (subscribe_valid && !list_full)
      |=> vector[$past(hash_of_request)];
endproperty
a_subscribe_sets_bit: assert property (p_subscribe_sets_bit);
 
// ---------------------------------------------------------------------
// P5 -- Unsubscribing does NOT take effect immediately, and the assertion
// says so rather than pretending otherwise: the vector is unstable until
// the rebuild completes.
// ---------------------------------------------------------------------
property p_unsubscribe_enters_rebuild;
  @(posedge clk) disable iff (!rst_n)
    unsubscribe_valid |=> !vector_stable;
endproperty
a_unsubscribe_enters_rebuild: assert property (p_unsubscribe_enters_rebuild);
 
// ---------------------------------------------------------------------
// P6 -- The rebuild must be PERMISSIVE, not restrictive (Section 11). An
// unstable vector may over-accept; it must never under-accept.
// ---------------------------------------------------------------------
property p_rebuild_is_permissive;
  @(posedge clk) disable iff (!rst_n)
    (!vector_stable && frame_valid && is_group) |-> deliver_to_software;
endproperty
a_rebuild_is_permissive: assert property (p_rebuild_is_permissive);
 
// ---------------------------------------------------------------------
// P7 -- The rebuild terminates. An unbounded rebuild leaves the filter
// permanently permissive, which is not a lost frame but is a permanent
// software cost that looks like a traffic problem.
// ---------------------------------------------------------------------
property p_rebuild_terminates;
  @(posedge clk) disable iff (!rst_n)
    $fell(vector_stable) |-> ##[1:REBUILD_BOUND] vector_stable;
endproperty
a_rebuild_terminates: assert property (p_rebuild_terminates);
 
// ---------------------------------------------------------------------
// P8 -- A false positive is by definition a frame the filter admitted and
// the exact comparison rejected. It cannot be reported on a frame that
// was never admitted.
// ---------------------------------------------------------------------
property p_false_positive_implies_admitted;
  @(posedge clk) disable iff (!rst_n)
    false_positive |-> (maybe_subscribed && !exact_match);
endproperty
a_false_positive_implies_admitted: assert property (p_false_positive_implies_admitted);
 
// ---------------------------------------------------------------------
// P9 -- Delivered and false-positive are mutually exclusive on one frame.
// Section 9's two counters are only interpretable if they partition.
// ---------------------------------------------------------------------
property p_delivered_xor_false;
  @(posedge clk) disable iff (!rst_n)
    (frame_valid && is_group && !is_broadcast && maybe_subscribed)
      |-> (delivered ^ false_positive);
endproperty
a_delivered_xor_false: assert property (p_delivered_xor_false);
 
// ---------------------------------------------------------------------
// P10 -- The I/G bit alone decides which pipeline runs (Chapter 5.3).
// A group frame must never be resolved by the unicast comparator.
// ---------------------------------------------------------------------
property p_group_never_uses_unicast_path;
  @(posedge clk) disable iff (!rst_n)
    (frame_valid && is_group) |-> !unicast_matched;
endproperty
a_group_never_uses_unicast_path: assert property (p_group_never_uses_unicast_path);
 
// ---------------------------------------------------------------------
// P11 -- Broadcast is a group address, so anything that classifies it as
// individual has mis-decoded the first bit.
// ---------------------------------------------------------------------
property p_broadcast_is_group;
  @(posedge clk) disable iff (!rst_n)
    is_broadcast |-> is_group;
endproperty
a_broadcast_is_group: assert property (p_broadcast_is_group);
 
// ---------------------------------------------------------------------
// P12 -- The false-negative monitor is sticky. A filter that was ever
// inconsistent has already lost frames, and `clear` must not erase it.
// ---------------------------------------------------------------------
property p_inconsistent_is_sticky;
  @(posedge clk) disable iff (!rst_n)
    inconsistent |=> inconsistent;
endproperty
a_inconsistent_is_sticky: assert property (p_inconsistent_is_sticky);
 
// ---------------------------------------------------------------------
// P13 -- First cause is captured once. The address that broke the
// guarantee is the one worth having, not the tenth one found.
// ---------------------------------------------------------------------
property p_first_bad_addr_stable;
  @(posedge clk) disable iff (!rst_n)
    inconsistent |=> $stable(first_bad_addr);
endproperty
a_first_bad_addr_stable: assert property (p_first_bad_addr_stable);
 
// ---------------------------------------------------------------------
// P14 -- The monitor must not report a fault while the vector is being
// rebuilt (Section 12). A diagnostic that fires during a known transient
// gets disabled, and then the real fault is invisible.
// ---------------------------------------------------------------------
property p_monitor_quiet_during_rebuild;
  @(posedge clk) disable iff (!rst_n)
    (!vector_stable && !$past(inconsistent)) |-> !inconsistent;
endproperty
a_monitor_quiet_during_rebuild: assert property (p_monitor_quiet_during_rebuild);
 
// ---------------------------------------------------------------------
// P15 -- Broadcast rate is measured per window (Section 9), so the
// reported value must never exceed the window length.
// ---------------------------------------------------------------------
property p_broadcast_rate_bounded;
  @(posedge clk) disable iff (!rst_n)
    window_valid |-> (window_broadcast <= WINDOW);
endproperty
a_broadcast_rate_bounded: assert property (p_broadcast_rate_bounded);
 
// ---------------------------------------------------------------------
// P16 -- The worst rate survives `clear`, because it describes the
// DOMAIN this station sits in, not a measurement interval.
// ---------------------------------------------------------------------
property p_worst_rate_monotonic;
  @(posedge clk) disable iff (!rst_n)
    ##1 (worst_broadcast_rate >= $past(worst_broadcast_rate));
endproperty
a_worst_rate_monotonic: assert property (p_worst_rate_monotonic);
 
// ---------------------------------------------------------------------
// P17 -- COVERAGE, not assertion. A verification run that never produced
// a false positive never exercised the path this chapter is about.
// ---------------------------------------------------------------------
c_false_positive_seen: cover property (
  @(posedge clk) disable iff (!rst_n) false_positive
);
 
// ---------------------------------------------------------------------
// P18 -- COVERAGE. A frame arriving DURING a rebuild is the interesting
// corner and random stimulus reaches it rarely.
// ---------------------------------------------------------------------
c_frame_during_rebuild: cover property (
  @(posedge clk) disable iff (!rst_n) (frame_valid && is_group && !vector_stable)
);