Address Filtering in Hardware

// SYNTHESIZABLE.
//
// Exact match against the station's own addresses. A small table, and
// the smallness is the design:
//
//   a station has ONE burned-in address, plus a few more for virtual
//   interfaces, containers, or a management identity. Eight to sixteen
//   entries covers essentially every real device.
//
// Chapter 5.4 §3 showed why the GROUP case cannot be done this way -- a
// station may subscribe to hundreds of groups and the comparison must
// finish within a frame time. That is the hash's job, not this table's.
//
// The comparison is STREAMING, per Chapter 5.3 §6: octets are compared
// as they arrive and a mismatch retires an entry immediately. On traffic
// whose addresses are unrelated the first octet retires almost every
// entry, so the average work is one octet rather than six.
package rxfilter_pkg;
 
  typedef enum logic [2:0] {
    AR_NONE,
    AR_PROMISCUOUS,   // the filter was not filtering
    AR_PERFECT,       // this station's own address
    AR_BROADCAST,     // the all-ones address
    AR_ALL_MULTICAST, // every group address accepted
    AR_HASH           // a subscribed group -- possibly a false positive
  } accept_reason_e;
 
  localparam int unsigned ADDR_OCTETS = 6;
 
endpackage
 
module perfect_match_table
  import rxfilter_pkg::*;
  import macaddr_pkg::*;
#(
  parameter int unsigned ENTRIES = 8
) (
  input  logic clk,
  input  logic rst_n,
 
  // Entry programming. An entry is only live once BOTH the address and
  // its valid bit are written -- a half-programmed entry that matches on
  // a partial address is the failure this ordering prevents.
  input  logic                        prog_valid,
  input  logic [$clog2(ENTRIES)-1:0]  prog_index,
  input  mac_addr_t                   prog_addr,
  input  logic                        prog_enable,
 
  input  logic       addr_start,
  input  logic       oct_valid,
  input  logic [7:0] oct_data,
 
  output logic                        match_valid,
  output logic                        match_found,
  output logic [$clog2(ENTRIES)-1:0]  match_index,
  // Octets consumed before the verdict. Telemetry, not control: it
  // measures how well early rejection is working on this segment.
  output logic [2:0]                  octets_compared
);
 
  mac_addr_t          entry_addr [ENTRIES];
  logic [ENTRIES-1:0] entry_live;
  logic [ENTRIES-1:0] alive_q;      // entries still matching this frame
  logic [2:0]         idx_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      entry_live      <= '0;
      alive_q         <= '0;
      idx_q           <= '0;
      match_valid     <= 1'b0;
      match_found     <= 1'b0;
      match_index     <= '0;
      octets_compared <= '0;
      for (int i = 0; i < ENTRIES; i++) entry_addr[i] <= '0;
    end else begin
      match_valid <= 1'b0;
 
      if (prog_valid) begin
        entry_addr[prog_index] <= prog_addr;
        entry_live[prog_index] <= prog_enable;
      end
 
      if (addr_start) begin
        // Every live entry is a candidate until an octet retires it.
        alive_q <= entry_live;
        idx_q   <= '0;
      end else if (oct_valid && (|alive_q)) begin
        for (int i = 0; i < ENTRIES; i++)
          if (alive_q[i] && (entry_addr[i][8*idx_q +: 8] != oct_data))
            alive_q[i] <= 1'b0;
 
        if (idx_q == 3'(ADDR_OCTETS - 1)) begin
          match_valid     <= 1'b1;
          match_found     <= |next_alive();
          match_index     <= first_alive();
          octets_compared <= 3'(ADDR_OCTETS);
        end else begin
          idx_q <= idx_q + 1'b1;
        end
      end else if (oct_valid && !(|alive_q)) begin
        // Every entry retired. The verdict is already known and the
        // remaining octets are consumed without comparison -- which is
        // the whole point of a streaming compare.
        if (idx_q == 3'(ADDR_OCTETS - 1)) begin
          match_valid     <= 1'b1;
          match_found     <= 1'b0;
          octets_compared <= idx_q + 3'd1;
        end else begin
          idx_q <= idx_q + 1'b1;
        end
      end
    end
  end
 
  function automatic logic [ENTRIES-1:0] next_alive();
    for (int i = 0; i < ENTRIES; i++)
      next_alive[i] = alive_q[i] && (entry_addr[i][8*idx_q +: 8] == oct_data);
  endfunction
 
  function automatic logic [$clog2(ENTRIES)-1:0] first_alive();
    first_alive = '0;
    for (int i = ENTRIES-1; i >= 0; i--) if (next_alive()[i]) first_alive = i[$clog2(ENTRIES)-1:0];
  endfunction
 
endmodule

// SYNTHESIZABLE.
//
// Composes the five accept reasons. Two outputs from the same inputs,
// answering two different questions:
//
//   accept  -- the OR. Any reason suffices, so this is a union and never
//              an intersection or a selection.
//   reason  -- a PRIORITY selection among the reasons that applied.
//
// The priority order is a design decision and every position is argued:
//
//   1. PROMISCUOUS   -- reported first because it is the most alarming.
//        If the filter is not filtering, that is the finding, whatever
//        else also matched.
//   2. PERFECT       -- the frame really is this station's. The most
//        specific reason, and the one a client cares about.
//   3. BROADCAST     -- explicit, so a broadcast frame is never reported
//        as generic multicast (Chapter 5.4 §10 kept them distinct).
//   4. ALL_MULTICAST -- a mode, so it outranks the hash: if all-multicast
//        is on, the hash's opinion was not needed.
//   5. HASH          -- the only reason that may be a FALSE POSITIVE
//        (Chapter 5.4 §4), so it is reported last and should be treated
//        as provisional by anything reading it.
module filter_mode_composer
  import rxfilter_pkg::*;
(
  input  logic clk,
  input  logic rst_n,
 
  // Independent enables. NOT an enumerated mode -- Section 4 explains
  // why a selector cannot express a promiscuous port that still needs to
  // recognise its own address.
  input  logic en_promiscuous,
  input  logic en_all_multicast,
  input  logic en_broadcast,
  input  logic en_hash,
  input  logic en_perfect,
 
  input  logic verdict_valid,
  input  logic is_group,
  input  logic is_broadcast,
  input  logic perfect_hit,
  input  logic hash_hit,
 
  output logic           accept,
  output accept_reason_e reason,
  output logic           reason_valid,
  // All reasons that applied, not only the reported one. Kept because a
  // frame accepted for three reasons is a different situation from one
  // accepted for a single reason, and the priority output hides that.
  output logic [4:0]     reasons_applied
);
 
  wire r_promisc = en_promiscuous;
  wire r_perfect = en_perfect       && perfect_hit;
  wire r_bcast   = en_broadcast     && is_broadcast;
  wire r_allmc   = en_all_multicast && is_group;
  wire r_hash    = en_hash          && is_group && hash_hit;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      accept          <= 1'b0;
      reason          <= AR_NONE;
      reason_valid    <= 1'b0;
      reasons_applied <= '0;
    end else begin
      reason_valid <= verdict_valid;
 
      if (verdict_valid) begin
        // THE UNION. Any reason suffices.
        accept          <= r_promisc || r_perfect || r_bcast || r_allmc || r_hash;
        reasons_applied <= {r_hash, r_allmc, r_bcast, r_perfect, r_promisc};
 
        // THE PRIORITY. Exactly one reported, and the order is the
        // header comment's.
        if      (r_promisc) reason <= AR_PROMISCUOUS;
        else if (r_perfect) reason <= AR_PERFECT;
        else if (r_bcast)   reason <= AR_BROADCAST;
        else if (r_allmc)   reason <= AR_ALL_MULTICAST;
        else if (r_hash)    reason <= AR_HASH;
        else                reason <= AR_NONE;
      end
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// Carries the accept reason alongside the frame and accumulates the
// per-reason statistics that answer "why am I receiving this traffic".
//
// The counters are the point. A receive path that counts only "frames
// accepted" can report a load and nothing about its cause; one that
// counts by reason distinguishes:
//
//   a monitoring tool left in promiscuous mode
//   an all-multicast bit set by a daemon that has since exited
//   a stale perfect-match entry from a torn-down virtual interface
//   a hash false positive rate that has drifted (Chapter 5.4 §8)
//
// All four present identically as "receive load is higher than expected".
module accept_reason_encoder
  import rxfilter_pkg::*;
#(
  parameter int unsigned CNT_W = 32
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic           reason_valid,
  input  logic           accept,
  input  accept_reason_e reason,
  input  logic [4:0]     reasons_applied,
  input  logic [13:0]    frame_octets,
 
  output logic [CNT_W-1:0] c_by_reason  [6],
  output logic [CNT_W-1:0] o_by_reason  [6],   // octets, not frames
  output logic [CNT_W-1:0] c_rejected,
 
  // Frames accepted for more than one reason. A configuration signal
  // rather than a traffic one: it means an enabled mode is subsuming
  // another, which is usually not what somebody intended.
  output logic [CNT_W-1:0] c_multi_reason,
  output logic [4:0]       most_recent_multi,
 
  // Sticky: promiscuous mode ever having accepted a frame is worth
  // keeping across a counter clear, because it is a configuration event
  // and not a rate.
  output logic             promiscuous_ever_used
);
 
  function automatic logic [CNT_W-1:0] bump(input logic [CNT_W-1:0] v);
    bump = (&v) ? v : (v + 1'b1);
  endfunction
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (int i = 0; i < 6; i++) begin
        c_by_reason[i] <= '0;
        o_by_reason[i] <= '0;
      end
      c_rejected            <= '0;
      c_multi_reason        <= '0;
      most_recent_multi     <= '0;
      promiscuous_ever_used <= 1'b0;
    end else begin
      if (clear) begin
        for (int i = 0; i < 6; i++) begin
          c_by_reason[i] <= '0;
          o_by_reason[i] <= '0;
        end
        c_rejected     <= '0;
        c_multi_reason <= '0;
        // promiscuous_ever_used deliberately survives.
      end else if (reason_valid) begin
        if (accept) begin
          c_by_reason[reason] <= bump(c_by_reason[reason]);
          // Octets as well as frames, because a reason accepting a few
          // large frames and one accepting many small ones are different
          // findings that a frame count alone cannot separate.
          o_by_reason[reason] <= o_by_reason[reason] + CNT_W'(frame_octets);
 
          if ($countones(reasons_applied) > 1) begin
            c_multi_reason    <= bump(c_multi_reason);
            most_recent_multi <= reasons_applied;
          end
 
          if (reason == AR_PROMISCUOUS) promiscuous_ever_used <= 1'b1;
        end else begin
          c_rejected <= bump(c_rejected);
        end
      end
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// Delivers a narrow set of frames to the management client regardless of
// the filter's verdict, and cannot be widened at run time.
//
// Three guards, and each closes a different way for this to become a
// general promiscuous mode:
//
//   1. the address set is a PARAMETER, not a table software writes.
//      A software-writable bypass list is a second perfect-match table
//      that ignores the filter -- which is a filter, badly.
//   2. the destination is the management client only. A bypassed frame
//      never reaches the data path, so a bypass cannot widen the filter
//      for ordinary traffic.
//   3. the feature is counted separately and its rate is bounded, so a
//      bypass carrying volume is visible rather than absorbed.
module mgmt_bypass_path
  import rxfilter_pkg::*;
  import macaddr_pkg::*;
#(
  // The reserved destinations this device honours. Fixed at integration
  // because the set is a property of which protocols the device
  // participates in, not of its runtime configuration.
  parameter int unsigned BYPASS_ENTRIES = 4,
  // Frames per window above which the bypass is considered abused. A
  // control-plane path carries a trickle; volume means something else.
  parameter int unsigned BYPASS_RATE_LIMIT = 64,
  parameter int unsigned WINDOW_BITS = 20,
  parameter int unsigned CNT_W = 32
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  mac_addr_t  bypass_addr [BYPASS_ENTRIES],
  input  logic [BYPASS_ENTRIES-1:0] bypass_live,
 
  input  logic       verdict_valid,
  input  mac_addr_t  dest_addr,
  input  logic       filter_accept,
 
  // To the management client ONLY. There is deliberately no data-path
  // output on this module.
  output logic       mgmt_deliver,
  output logic       bypassed,          // accepted only because of this
 
  output logic [CNT_W-1:0] c_bypassed,
  output logic [CNT_W-1:0] win_bypassed,
  output logic             bypass_rate_exceeded,
  output logic             bypass_ever_used
);
 
  logic [WINDOW_BITS-1:0] win_q;
  logic [CNT_W-1:0]       wcnt_q;
 
  logic hit;
  always_comb begin
    hit = 1'b0;
    for (int i = 0; i < BYPASS_ENTRIES; i++)
      if (bypass_live[i] && (dest_addr == bypass_addr[i])) hit = 1'b1;
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      mgmt_deliver         <= 1'b0;
      bypassed             <= 1'b0;
      c_bypassed           <= '0;
      win_bypassed         <= '0;
      wcnt_q               <= '0;
      win_q                <= '0;
      bypass_rate_exceeded <= 1'b0;
      bypass_ever_used     <= 1'b0;
    end else begin
      mgmt_deliver <= 1'b0;
      bypassed     <= 1'b0;
 
      if (clear) begin
        c_bypassed <= '0;
        // bypass_ever_used and bypass_rate_exceeded deliberately survive.
      end
 
      if (verdict_valid && hit) begin
        mgmt_deliver <= 1'b1;
        // `bypassed` marks only the frames the filter would have
        // REJECTED. A reserved-address frame the filter accepted anyway
        // is not a bypass event, and counting it as one would make the
        // bypass counter track ordinary control traffic.
        if (!filter_accept) begin
          bypassed         <= 1'b1;
          bypass_ever_used <= 1'b1;
          if (!(&c_bypassed)) c_bypassed <= c_bypassed + 1'b1;
          wcnt_q <= wcnt_q + 1'b1;
        end
      end
 
      if (&win_q) begin
        win_bypassed <= wcnt_q;
        if (wcnt_q > CNT_W'(BYPASS_RATE_LIMIT)) bypass_rate_exceeded <= 1'b1;
        wcnt_q <= '0;
        win_q  <= '0;
      end else begin
        win_q <= win_q + 1'b1;
      end
    end
  end
 
endmodule

// SYNTHESIZABLE MONITOR.
//
// Verifies that each mode means what it is documented to mean, stated as
// a relation between an enable and an outcome.
//
// The failures this catches are composition failures rather than lookup
// failures: every individual reason can be correct while the union is
// wrong, because the union is where a design accidentally implements a
// selector instead (Section 4).
//
// And it checks the one relation that is NOT symmetric: broadcast
// acceptance being disabled is legal and consequential, so it is
// reported rather than forbidden (Chapter 5.4 §10).
module filter_conformance_monitor
  import rxfilter_pkg::*;
#(
  parameter int unsigned CNT_W = 32
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic en_promiscuous,
  input  logic en_all_multicast,
  input  logic en_broadcast,
  input  logic en_hash,
  input  logic en_perfect,
 
  input  logic           reason_valid,
  input  logic           accept,
  input  accept_reason_e reason,
  input  logic [4:0]     reasons_applied,
  input  logic           is_group,
  input  logic           is_broadcast,
  input  logic           perfect_hit,
 
  output logic             semantic_error,
  output logic [CNT_W-1:0] c_semantic_error,
  output logic [2:0]       first_error_kind,
 
  // Not an error. A configuration this device is in, reported because a
  // station that declines broadcast appears healthy and can reach
  // nothing it has not already learned.
  output logic             broadcast_declined_mode,
  output logic [CNT_W-1:0] c_broadcast_declined,
 
  output logic             any_violation      // sticky
);
 
  localparam logic [2:0] E_PROMISC_REJECTED = 3'd1;
  localparam logic [2:0] E_ALLMC_REJECTED   = 3'd2;
  localparam logic [2:0] E_PERFECT_REJECTED = 3'd3;
  localparam logic [2:0] E_ACCEPT_NO_REASON = 3'd4;
  localparam logic [2:0] E_REASON_NOT_APPLIED = 3'd5;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      semantic_error <= 1'b0; c_semantic_error <= '0; first_error_kind <= '0;
      broadcast_declined_mode <= 1'b0; c_broadcast_declined <= '0;
      any_violation <= 1'b0;
    end else begin
      semantic_error          <= 1'b0;
      broadcast_declined_mode <= 1'b0;
 
      if (clear) begin
        c_semantic_error <= '0; c_broadcast_declined <= '0;
        // first_error_kind and any_violation deliberately survive.
      end else if (reason_valid) begin
        automatic logic [2:0] kind = 3'd0;
 
        // Promiscuous means NOTHING is rejected. The strongest relation
        // and the one a selector-shaped design breaks first.
        if (en_promiscuous && !accept) kind = E_PROMISC_REJECTED;
 
        // All-multicast means no GROUP frame is rejected.
        else if (en_all_multicast && is_group && !accept) kind = E_ALLMC_REJECTED;
 
        // A perfect-match hit, with perfect matching enabled, is always
        // accepted -- whatever else is or is not on.
        else if (en_perfect && perfect_hit && !accept) kind = E_PERFECT_REJECTED;
 
        // An acceptance with no reason applied is a decision with no
        // justification, which means the union and the priority encoder
        // were computed from different inputs.
        else if (accept && (reasons_applied == 5'd0)) kind = E_ACCEPT_NO_REASON;
 
        // And the reported reason must be one that actually applied.
        else if (accept && (reason != AR_NONE) &&
                 !reasons_applied[reason_index(reason)]) kind = E_REASON_NOT_APPLIED;
 
        if (kind != 3'd0) begin
          semantic_error   <= 1'b1;
          c_semantic_error <= c_semantic_error + 1'b1;
          any_violation    <= 1'b1;
          if (first_error_kind == 3'd0) first_error_kind <= kind;
        end
 
        // Reported, not forbidden.
        if (is_broadcast && !en_broadcast && !accept) begin
          broadcast_declined_mode <= 1'b1;
          c_broadcast_declined    <= c_broadcast_declined + 1'b1;
        end
      end
    end
  end
 
  function automatic int unsigned reason_index(input accept_reason_e r);
    case (r)
      AR_PROMISCUOUS:   reason_index = 0;
      AR_PERFECT:       reason_index = 1;
      AR_BROADCAST:     reason_index = 2;
      AR_ALL_MULTICAST: reason_index = 3;
      default:          reason_index = 4;
    endcase
  endfunction
 
endmodule

// ---------------------------------------------------------------------
// P1 -- THE UNION. Accept is the OR of the reasons. Not a selection, not
// an intersection -- Section 5's central relation.
// ---------------------------------------------------------------------
property p_accept_is_union;
  @(posedge clk) disable iff (!rst_n)
    reason_valid |-> (accept == (|reasons_applied));
endproperty
a_accept_is_union: assert property (p_accept_is_union)
  else $error("accept is not the OR of the applicable reasons");
 
// ---------------------------------------------------------------------
// P2 -- The reported reason is one that actually applied.
// ---------------------------------------------------------------------
property p_reported_reason_applied;
  @(posedge clk) disable iff (!rst_n)
    (reason_valid && accept) |-> reasons_applied[reason_index(reason)];
endproperty
a_reported_reason_applied: assert property (p_reported_reason_applied);
 
// ---------------------------------------------------------------------
// P3 -- THE PRIORITY. The reported reason is the HIGHEST-priority one
// that applied. This is the correct shape -- compare the rejected
// property below, which asks for exclusivity instead.
// ---------------------------------------------------------------------
property p_reason_is_highest_priority;
  @(posedge clk) disable iff (!rst_n)
    (reason_valid && accept) |-> (reason == highest_priority(reasons_applied));
endproperty
a_reason_is_highest_priority: assert property (p_reason_is_highest_priority);
 
// ---------------------------------------------------------------------
// P4 -- No reasons applied means no acceptance.
// ---------------------------------------------------------------------
property p_no_reason_no_accept;
  @(posedge clk) disable iff (!rst_n)
    (reason_valid && (reasons_applied == 5'd0)) |-> !accept;
endproperty
a_no_reason_no_accept: assert property (p_no_reason_no_accept);
 
// ---------------------------------------------------------------------
// P5 -- PROMISCUOUS MEANS PROMISCUOUS. Nothing is rejected. The relation
// a selector-shaped design breaks first.
// ---------------------------------------------------------------------
property p_promiscuous_accepts_everything;
  @(posedge clk) disable iff (!rst_n)
    (reason_valid && en_promiscuous) |-> accept;
endproperty
a_promiscuous_accepts_everything: assert property (p_promiscuous_accepts_everything)
  else $error("a frame was rejected while promiscuous mode was enabled");
 
// ---------------------------------------------------------------------
// P6 -- All-multicast accepts every group frame.
// ---------------------------------------------------------------------
property p_all_multicast_accepts_groups;
  @(posedge clk) disable iff (!rst_n)
    (reason_valid && en_all_multicast && is_group) |-> accept;
endproperty
a_all_multicast_accepts_groups: assert property (p_all_multicast_accepts_groups);
 
// ---------------------------------------------------------------------
// P7 -- A perfect-match hit is always accepted when perfect matching is
// enabled, regardless of any other mode.
// ---------------------------------------------------------------------
property p_perfect_hit_accepted;
  @(posedge clk) disable iff (!rst_n)
    (reason_valid && en_perfect && perfect_hit) |-> accept;
endproperty
a_perfect_hit_accepted: assert property (p_perfect_hit_accepted);
 
// ---------------------------------------------------------------------
// P8 -- A promiscuous port still recognises its own address. The
// perfect-match verdict is not discarded when promiscuous is on, which
// is Section 4's bridge-port case.
// ---------------------------------------------------------------------
property p_perfect_visible_under_promiscuous;
  @(posedge clk) disable iff (!rst_n)
    (reason_valid && en_promiscuous && en_perfect && perfect_hit)
      |-> reasons_applied[1];
endproperty
a_perfect_visible_under_promiscuous: assert property (p_perfect_visible_under_promiscuous);
 
// ---------------------------------------------------------------------
// P9 -- The hash reason only ever applies to group addresses. Chapter
// 5.3: the individual/group bit selects the pipeline.
// ---------------------------------------------------------------------
property p_hash_only_for_groups;
  @(posedge clk) disable iff (!rst_n)
    (reason_valid && reasons_applied[4]) |-> is_group;
endproperty
a_hash_only_for_groups: assert property (p_hash_only_for_groups);
 
// ---------------------------------------------------------------------
// P10 -- Broadcast is a group address, so anything reporting it as an
// individual address 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);
 
// ---------------------------------------------------------------------
// P11 -- A half-programmed perfect-match entry never matches. Address
// and enable arrive together, so an entry cannot be live with a partial
// address (Section 3).
// ---------------------------------------------------------------------
property p_no_partial_entry_match;
  @(posedge clk) disable iff (!rst_n)
    (match_valid && match_found) |-> entry_live[match_index];
endproperty
a_no_partial_entry_match: assert property (p_no_partial_entry_match);
 
// ---------------------------------------------------------------------
// P12 -- The streaming compare never consumes more than the address.
// ---------------------------------------------------------------------
property p_compare_bounded;
  @(posedge clk) disable iff (!rst_n)
    match_valid |-> (octets_compared <= 3'(ADDR_OCTETS));
endproperty
a_compare_bounded: assert property (p_compare_bounded);
 
// ---------------------------------------------------------------------
// P13 -- THE BYPASS GUARD. A bypassed frame reaches the management
// client and nothing else. Written as an absence, because the module has
// no data-path output at all (Section 8).
// ---------------------------------------------------------------------
property p_bypass_is_mgmt_only;
  @(posedge clk) disable iff (!rst_n)
    bypassed |-> (mgmt_deliver && !data_path_deliver);
endproperty
a_bypass_is_mgmt_only: assert property (p_bypass_is_mgmt_only)
  else $error("a bypassed frame reached the data path");
 
// ---------------------------------------------------------------------
// P14 -- The bypass only fires on the reserved address set.
// ---------------------------------------------------------------------
property p_bypass_only_reserved;
  @(posedge clk) disable iff (!rst_n)
    bypassed |-> bypass_hit;
endproperty
a_bypass_only_reserved: assert property (p_bypass_only_reserved);
 
// ---------------------------------------------------------------------
// P15 -- A frame the filter accepted anyway is not a bypass event. The
// counter must not track ordinary control traffic (Section 8).
// ---------------------------------------------------------------------
property p_bypass_only_when_filter_rejected;
  @(posedge clk) disable iff (!rst_n)
    bypassed |-> !filter_accept;
endproperty
a_bypass_only_when_filter_rejected: assert property (p_bypass_only_when_filter_rejected);
 
// ---------------------------------------------------------------------
// P16 -- Configuration events survive a counter clear.
// ---------------------------------------------------------------------
property p_config_events_survive_clear;
  @(posedge clk) disable iff (!rst_n)
    clear |=> ($stable(promiscuous_ever_used) && $stable(bypass_ever_used));
endproperty
a_config_events_survive_clear: assert property (p_config_events_survive_clear);
 
// ---------------------------------------------------------------------
// P17 -- COVERAGE. A frame accepted for more than one reason, which is
// the state the rejected property below would forbid.
// ---------------------------------------------------------------------
c_multi_reason_accept: cover property (
  @(posedge clk) disable iff (!rst_n)
    (reason_valid && accept && ($countones(reasons_applied) > 1))
);
 
// ---------------------------------------------------------------------
// P18 -- COVERAGE. Each reason reported at least once, including the
// bypass and the promiscuous case.
// ---------------------------------------------------------------------
c_reason_promiscuous: cover property (@(posedge clk) disable iff (!rst_n) (reason == AR_PROMISCUOUS));
c_reason_perfect:     cover property (@(posedge clk) disable iff (!rst_n) (reason == AR_PERFECT));
c_reason_broadcast:   cover property (@(posedge clk) disable iff (!rst_n) (reason == AR_BROADCAST));
c_reason_allmc:       cover property (@(posedge clk) disable iff (!rst_n) (reason == AR_ALL_MULTICAST));
c_reason_hash:        cover property (@(posedge clk) disable iff (!rst_n) (reason == AR_HASH));
c_bypass_used:        cover property (@(posedge clk) disable iff (!rst_n) bypassed);