The 48-Bit MAC Address — OUI, I/G and U/L

first octet, as a value:   b7 b6 b5 b4 b3 b2 b1 b0
transmitted LSB first:     b0 b1 b2 b3 b4 b5 b6 b7
                           ^^ ^^
                           |  +-- U/L: second bit on the wire
                           +----- I/G: FIRST bit on the wire

// SYNTHESIZABLE. Address decomposition, streaming.
//
// A decomposer that takes a completed 48-bit address is easy to write and
// throws away this chapter's entire point. The flags are in the first two
// bit positions SO THAT A RECEIVER CAN BRANCH BEFORE THE ADDRESS ARRIVES --
// and a module that requires the whole address first cannot express that.
//
// So this consumes the address octet by octet and produces:
//   flags_valid after the FIRST octet   (both flags are inside it)
//   oui_valid   after the THIRD octet
//   addr_valid  after the SIXTH
//
// Each output is available at the earliest moment it can be, which is what
// lets the receive path select a pipeline early.
package macaddr_pkg;
  // Bit positions within the first octet, as published. Under LSB-first
  // transmission these are the first and second bits on the wire.
  localparam int unsigned BIT_IG = 0;
  localparam int unsigned BIT_UL = 1;
 
  localparam logic [47:0] ADDR_BROADCAST = 48'hFFFF_FFFF_FFFF;
 
  typedef enum logic [1:0] {
    ADDR_UNICAST_GLOBAL,   // I/G = 0, U/L = 0
    ADDR_UNICAST_LOCAL,    // I/G = 0, U/L = 1
    ADDR_GROUP_GLOBAL,     // I/G = 1, U/L = 0
    ADDR_GROUP_LOCAL       // I/G = 1, U/L = 1
  } addr_class_e;
endpackage
 
module mac_address_decomposer
  import macaddr_pkg::*;
(
  input  logic       clk,
  input  logic       rst_n,
 
  input  logic       octet_valid,
  input  logic [7:0] octet_in,
  input  logic       addr_start,     // first octet of an address
 
  // ── Available after ONE octet. The reason the flags are where they are.
  output logic        flags_valid,
  output logic        is_group,
  output logic        is_local,
  output addr_class_e addr_class,
 
  // ── Available after THREE octets.
  output logic        oui_valid,
  output logic [23:0] oui,
 
  // ── Available after SIX.
  output logic        addr_valid,
  output logic [47:0] address,
  output logic        is_broadcast,
 
  // How many octets into the address we are. Exposed so a consumer can
  // reason about what is and is not yet known.
  output logic [2:0]  octet_count
);
 
  logic [47:0] shift_q;
  logic [2:0]  count_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      shift_q      <= '0;
      count_q      <= '0;
      flags_valid  <= 1'b0;
      is_group     <= 1'b0;
      is_local     <= 1'b0;
      oui_valid    <= 1'b0;
      addr_valid   <= 1'b0;
      is_broadcast <= 1'b0;
    end else begin
      flags_valid <= 1'b0;
      oui_valid   <= 1'b0;
      addr_valid  <= 1'b0;
 
      if (octet_valid) begin
        shift_q <= {shift_q[39:0], octet_in};
 
        if (addr_start) begin
          count_q <= 3'd1;
          // THE EARLY BRANCH. Both flags are inside this octet, so the
          // coarse classification is complete here -- five octets before
          // the address is.
          flags_valid <= 1'b1;
          is_group    <= octet_in[BIT_IG];
          is_local    <= octet_in[BIT_UL];
        end else begin
          count_q <= count_q + 3'd1;
 
          if (count_q == 3'd2) oui_valid  <= 1'b1;   // third octet complete
          if (count_q == 3'd5) addr_valid <= 1'b1;   // sixth octet complete
        end
      end
    end
  end
 
  always_comb begin
    unique case ({is_group, is_local})
      2'b00:   addr_class = ADDR_UNICAST_GLOBAL;
      2'b01:   addr_class = ADDR_UNICAST_LOCAL;
      2'b10:   addr_class = ADDR_GROUP_GLOBAL;
      default: addr_class = ADDR_GROUP_LOCAL;
    endcase
  end
 
  assign oui         = shift_q[23:0];
  assign address     = shift_q;
  assign octet_count = count_q;
  // Broadcast is a group address with every bit set -- so it satisfies the
  // group test and is ALSO an exact value. Chapter 5.4 owns why that
  // double membership matters; here it is one comparison.
  assign is_broadcast = (shift_q == ADDR_BROADCAST);
 
endmodule

// SYNTHESIZABLE. Staged address comparison with early rejection.
//
// `a == b` on 48 bits is a wide AND reduction over 48 XNORs. A tool will
// balance it into a tree, and at line rate the tree depth is a real path.
//
// But a STREAMING comparison can do something the operator cannot: reject
// as soon as any octet differs, which on unrelated traffic is almost always
// the first one. The average comparison then costs one octet rather than
// six, and the worst case is unchanged.
//
// That matters because a receive path compares every arriving frame against
// its own address, and the overwhelming majority do not match.
module mac_address_compare #(
  parameter int unsigned CNT_W = 24
) (
  input  logic        clk,
  input  logic        rst_n,
  input  logic        clear,
 
  input  logic        octet_valid,
  input  logic [7:0]  octet_in,
  input  logic        addr_start,
  input  logic [47:0] local_address,
 
  // Rejected as soon as an octet differs. On a mismatching address this
  // fires early, and everything downstream can stop.
  output logic       mismatch,
  output logic [2:0] mismatch_octet,
 
  // Confirmed only when all six have matched.
  output logic       match,
 
  // Distribution of how many octets were needed to reject. On unrelated
  // traffic this is heavily weighted to one, and a shift toward six means
  // the addresses on this segment share prefixes -- which is a real
  // property of a deployment and changes the timing argument.
  output logic [CNT_W-1:0] reject_at_octet [6],
  output logic [CNT_W-1:0] c_match
);
 
  logic [2:0] idx_q;
  logic       failed_q;
  logic       active_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;   // saturating
  endfunction
 
  // The octet of the local address to compare against, most significant
  // first -- addresses are transmitted in that octet order.
  logic [7:0] local_octet_c;
  always_comb begin
    unique case (idx_q)
      3'd0:    local_octet_c = local_address[47:40];
      3'd1:    local_octet_c = local_address[39:32];
      3'd2:    local_octet_c = local_address[31:24];
      3'd3:    local_octet_c = local_address[23:16];
      3'd4:    local_octet_c = local_address[15:8];
      default: local_octet_c = local_address[7:0];
    endcase
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      idx_q          <= '0;
      failed_q       <= 1'b0;
      active_q       <= 1'b0;
      mismatch       <= 1'b0;
      match          <= 1'b0;
      mismatch_octet <= '0;
      for (int unsigned i = 0; i < 6; i++) reject_at_octet[i] <= '0;
      c_match <= '0;
    end else begin
      mismatch <= 1'b0;
      match    <= 1'b0;
 
      if (clear) begin
        for (int unsigned i = 0; i < 6; i++) reject_at_octet[i] <= '0;
        c_match <= '0;
      end
 
      if (octet_valid && addr_start) begin
        idx_q    <= 3'd1;
        active_q <= 1'b1;
        if (octet_in != local_address[47:40]) begin
          failed_q           <= 1'b1;
          mismatch           <= 1'b1;
          mismatch_octet     <= 3'd0;
          reject_at_octet[0] <= bump(reject_at_octet[0], 1'b1);
        end else begin
          failed_q <= 1'b0;
        end
      end else if (octet_valid && active_q) begin
        if (!failed_q && (octet_in != local_octet_c)) begin
          failed_q               <= 1'b1;
          mismatch               <= 1'b1;
          mismatch_octet         <= idx_q;
          reject_at_octet[idx_q] <= bump(reject_at_octet[idx_q], 1'b1);
        end
 
        if (idx_q == 3'd5) begin
          active_q <= 1'b0;
          if (!failed_q && (octet_in == local_octet_c)) begin
            match   <= 1'b1;
            c_match <= bump(c_match, 1'b1);
          end
        end else begin
          idx_q <= idx_q + 3'd1;
        end
      end
    end
  end
 
endmodule

// SYNTHESIZABLE. Locally administered address generation, auditable.
//
// Setting the U/L bit is trivial. The module exists because Section 4
// showed the real collision risk is a BAD SEED, not the birthday bound --
// and a generator that does not report its entropy source cannot be
// checked by anyone.
//
// So it takes a seed and a declaration of what that seed IS, and exposes
// both. An operator can then tell whether this deployment's addresses are
// derived from something genuinely unique or from a boot counter that every
// machine restarts at the same value.
package laa_pkg;
  typedef enum logic [2:0] {
    SEED_UNIQUE_HW,      // a device-unique value: a fuse, a serial number
    SEED_ASSIGNED_ADDR,  // derived from an existing globally assigned one
    SEED_CENTRAL,        // allocated by an authority for this deployment
    SEED_RANDOM,         // a hardware random source
    SEED_COUNTER,        // a boot-time counter -- NOT UNIQUE ACROSS MACHINES
    SEED_CONSTANT        // a fixed default -- guaranteed collision
  } seed_kind_e;
endpackage
 
module laa_generator
  import macaddr_pkg::*;
  import laa_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,
 
  input  logic        generate_req,
  input  logic [45:0] seed,           // 46 free bits: 48 less the two flags
  input  seed_kind_e  seed_kind,
  input  logic        make_group,     // a locally administered GROUP address
 
  output logic        addr_valid,
  output logic [47:0] address,
 
  // The audit outputs. A deployment can read these and know whether its
  // addresses are safe or merely untested.
  output seed_kind_e  address_seed_kind,
  output logic        seed_is_trustworthy,
  output logic        seed_guarantees_collision
);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      addr_valid        <= 1'b0;
      address           <= '0;
      address_seed_kind <= SEED_CONSTANT;
    end else begin
      addr_valid <= 1'b0;
 
      if (generate_req) begin
        addr_valid        <= 1'b1;
        address_seed_kind <= seed_kind;
 
        // The two flags occupy the low bits of the FIRST octet, which is
        // address[47:40]. Everything else comes from the seed.
        address <= {
          seed[45:40],            // top six bits of the first octet
          make_group,             // I/G, at bit position 0 of that octet
          1'b1,                   // U/L set: this is locally administered
          seed[39:0]              // the remaining five octets
        };
      end
    end
  end
 
  always_comb begin
    // A seed that is unique per machine gives an address that is too.
    seed_is_trustworthy = (address_seed_kind == SEED_UNIQUE_HW)
                       || (address_seed_kind == SEED_ASSIGNED_ADDR)
                       || (address_seed_kind == SEED_CENTRAL)
                       || (address_seed_kind == SEED_RANDOM);
 
    // A constant seed is not a risk -- it is a certainty. Every machine
    // built from this image has the same address, and the fault appears
    // the moment two of them share a segment.
    seed_guarantees_collision = (address_seed_kind == SEED_CONSTANT);
  end
 
endmodule

// SYNTHESIZABLE INSTRUMENTATION.
//
// Recording which assigned prefixes are seen sounds like inventory. It is
// diagnostic, for three reasons this chapter has already established:
//
//   Section 6 -- a segment dominated by one prefix defeats early rejection,
//                because the first octets match on most frames.
//   Section 4 -- locally administered addresses have NO prefix guarantee,
//                so their share of traffic is a risk measurement.
//   Section 9 -- a duplicate address is far more likely WITHIN one prefix
//                than across two, so the mix informs the search.
//
// It is a small associative structure, not a full table -- the goal is the
// SHAPE of the distribution, not an exhaustive inventory.
module prefix_telemetry
  import macaddr_pkg::*;
#(
  parameter int unsigned SLOTS = 8,
  parameter int unsigned CNT_W = 24
) (
  input  logic        clk,
  input  logic        rst_n,
  input  logic        clear,
 
  input  logic        oui_valid,
  input  logic [23:0] oui,
  input  logic        is_local,
  input  logic        is_group,
 
  output logic [23:0]      slot_oui   [SLOTS],
  output logic [CNT_W-1:0] slot_count [SLOTS],
  output logic [SLOTS-1:0] slot_used,
 
  // Traffic whose prefix did not fit in the tracked set. A large residue
  // means the segment is diverse; a small one means a few prefixes
  // dominate, which is what Section 6's early rejection cares about.
  output logic [CNT_W-1:0] c_untracked,
 
  // Locally administered share. Rising means more virtual interfaces or
  // more mobility, and Section 4 showed those carry no uniqueness
  // guarantee -- so this is a risk measurement, not an inventory line.
  output logic [CNT_W-1:0] c_local_admin,
  output logic [CNT_W-1:0] c_global_admin,
 
  // Distinct prefixes seen. One dominant prefix defeats early rejection;
  // this is the number that says whether that is happening.
  output logic [$clog2(SLOTS+1)-1:0] distinct_prefixes
);
 
  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                     hit_c;
  logic [$clog2(SLOTS)-1:0] hit_slot_c;
  logic                     free_c;
  logic [$clog2(SLOTS)-1:0] free_slot_c;
 
  always_comb begin
    hit_c       = 1'b0;
    hit_slot_c  = '0;
    free_c      = 1'b0;
    free_slot_c = '0;
    for (int unsigned i = 0; i < SLOTS; i++) begin
      if (slot_used[i] && (slot_oui[i] == oui)) begin
        hit_c      = 1'b1;
        hit_slot_c = ($clog2(SLOTS))'(i);
      end
      if (!slot_used[i] && !free_c) begin
        free_c      = 1'b1;
        free_slot_c = ($clog2(SLOTS))'(i);
      end
    end
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (int unsigned i = 0; i < SLOTS; i++) begin
        slot_oui[i]   <= '0;
        slot_count[i] <= '0;
      end
      slot_used      <= '0;
      c_untracked    <= '0;
      c_local_admin  <= '0;
      c_global_admin <= '0;
    end else begin
      if (clear) begin
        for (int unsigned i = 0; i < SLOTS; i++) slot_count[i] <= '0;
        c_untracked    <= '0;
        c_local_admin  <= '0;
        c_global_admin <= '0;
        // slot_used and slot_oui deliberately survive: which prefixes are
        // present is a property of the segment, not of a measurement window.
      end else if (oui_valid) begin
        // Group addresses are excluded: their leading octets are not a
        // manufacturer identifier, and counting them would corrupt the
        // distribution with values that mean something else entirely.
        if (!is_group) begin
          if (is_local) c_local_admin  <= bump(c_local_admin,  1'b1);
          else          c_global_admin <= bump(c_global_admin, 1'b1);
 
          if (hit_c) begin
            slot_count[hit_slot_c] <= bump(slot_count[hit_slot_c], 1'b1);
          end else if (free_c) begin
            slot_used[free_slot_c]  <= 1'b1;
            slot_oui[free_slot_c]   <= oui;
            slot_count[free_slot_c] <= bump(slot_count[free_slot_c], 1'b1);
          end else begin
            c_untracked <= bump(c_untracked, 1'b1);
          end
        end
      end
    end
  end
 
  always_comb begin
    distinct_prefixes = '0;
    for (int unsigned i = 0; i < SLOTS; i++)
      if (slot_used[i]) distinct_prefixes = distinct_prefixes + 1'b1;
  end
 
endmodule

// SYNTHESIZABLE INSTRUMENTATION.
//
// A duplicate address shows as one source address arriving on two ports.
// SO DOES A LEGITIMATE MOVE -- a service address failing over between
// machines does exactly this, deliberately, and must not be flagged.
//
// The distinguishing feature is RATE, not occurrence:
//
//   a MOVE      -- the address appears on the new port and stays there.
//                  One transition, then stability.
//   a DUPLICATE -- the address alternates between ports continuously,
//                  because both stations keep transmitting. The learning
//                  table flaps at the traffic rate.
//
// So the module counts TRANSITIONS over a window rather than reporting the
// first one, and Section 11's rejected property is the assertion that
// treats a single occurrence as the fault.
module duplicate_address_detector
  import macaddr_pkg::*;
#(
  parameter int unsigned ENTRIES = 16,
  parameter int unsigned PORT_W  = 4,
  parameter int unsigned CNT_W   = 16,
  // Port changes within a window above which it is a duplicate rather than
  // a move. A failover moves once; a duplicate moves continuously.
  parameter int unsigned FLAP_THRESHOLD = 8,
  parameter int unsigned WINDOW = 1_000_000,
  parameter int unsigned WIN_W  = $clog2(WINDOW + 1)
) (
  input  logic              clk,
  input  logic              rst_n,
  input  logic              clear,
 
  input  logic              sa_valid,
  input  logic [47:0]       source_address,
  input  logic [PORT_W-1:0] ingress_port,
 
  // A move: one transition, then stable. Normal, and counted not flagged.
  output logic        move_observed,
  output logic [47:0] moved_address,
 
  // A duplicate: sustained flapping. This is the fault.
  output logic              duplicate_suspected,
  output logic [47:0]       duplicate_address,
  output logic [PORT_W-1:0] duplicate_port_a,
  output logic [PORT_W-1:0] duplicate_port_b,
 
  output logic [CNT_W-1:0] c_moves,
  output logic [CNT_W-1:0] c_duplicates,
 
  // Whether the duplicated address is locally administered. Section 4
  // showed those carry no uniqueness guarantee, so a duplicate among them
  // points at a generator rather than at a manufacturer -- a completely
  // different investigation.
  output logic duplicate_is_local_admin
);
 
  logic [47:0]        addr_q  [ENTRIES];
  logic [PORT_W-1:0]  port_q  [ENTRIES];
  logic [CNT_W-1:0]   flaps_q [ENTRIES];
  logic [ENTRIES-1:0] used_q;
  logic [WIN_W-1:0]   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
 
  logic                       hit_c;
  logic [$clog2(ENTRIES)-1:0] hit_idx_c;
  logic                       free_c;
  logic [$clog2(ENTRIES)-1:0] free_idx_c;
 
  always_comb begin
    hit_c      = 1'b0; hit_idx_c  = '0;
    free_c     = 1'b0; free_idx_c = '0;
    for (int unsigned i = 0; i < ENTRIES; i++) begin
      if (used_q[i] && (addr_q[i] == source_address)) begin
        hit_c     = 1'b1;
        hit_idx_c = ($clog2(ENTRIES))'(i);
      end
      if (!used_q[i] && !free_c) begin
        free_c     = 1'b1;
        free_idx_c = ($clog2(ENTRIES))'(i);
      end
    end
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (int unsigned i = 0; i < ENTRIES; i++) begin
        addr_q[i]  <= '0;
        port_q[i]  <= '0;
        flaps_q[i] <= '0;
      end
      used_q                   <= '0;
      win_q                    <= '0;
      move_observed            <= 1'b0;
      duplicate_suspected      <= 1'b0;
      c_moves                  <= '0;
      c_duplicates             <= '0;
      duplicate_is_local_admin <= 1'b0;
    end else begin
      move_observed       <= 1'b0;
      duplicate_suspected <= 1'b0;
 
      if (clear) begin
        c_moves      <= '0;
        c_duplicates <= '0;
      end
 
      // The window bounds the flap count, which is what makes it a RATE.
      if (win_q == WIN_W'(WINDOW - 1)) begin
        win_q <= '0;
        for (int unsigned i = 0; i < ENTRIES; i++) flaps_q[i] <= '0;
      end else begin
        win_q <= win_q + 1'b1;
      end
 
      if (sa_valid) begin
        if (hit_c) begin
          if (port_q[hit_idx_c] != ingress_port) begin
            port_q[hit_idx_c]  <= ingress_port;
            flaps_q[hit_idx_c] <= bump(flaps_q[hit_idx_c], 1'b1);
 
            if (flaps_q[hit_idx_c] + 1'b1 >= CNT_W'(FLAP_THRESHOLD)) begin
              duplicate_suspected <= 1'b1;
              duplicate_address   <= source_address;
              duplicate_port_a    <= port_q[hit_idx_c];
              duplicate_port_b    <= ingress_port;
              // Section 4: a local-admin duplicate points at a generator,
              // a global one points at a manufacturer. Different searches.
              duplicate_is_local_admin <= source_address[41];
              c_duplicates             <= bump(c_duplicates, 1'b1);
            end else begin
              move_observed <= 1'b1;
              moved_address <= source_address;
              c_moves       <= bump(c_moves, 1'b1);
            end
          end
        end else if (free_c) begin
          used_q[free_idx_c]  <= 1'b1;
          addr_q[free_idx_c]  <= source_address;
          port_q[free_idx_c]  <= ingress_port;
          flaps_q[free_idx_c] <= '0;
        end
      end
    end
  end
 
endmodule

// ─── ADDRESS PROPERTY: the flags are in the first octet's low two bits ─────
// Published positions. Catches a decomposer reading them from the wrong end
// of the octet, which classifies every address wrongly while producing
// plausible-looking output.
property p_flag_bit_positions;
  @(posedge clk) disable iff (!rst_n)
  (flags_valid) |-> ((is_group == $past(octet_in)[0])
                  && (is_local == $past(octet_in)[1]));
endproperty
 
// ─── Causation: the flags are available after ONE octet ────────────────────
// The chapter's central structural claim, asserted. Catches a decomposer
// that waits for the whole address, which discards the early branch the
// layout exists to enable.
property p_flags_after_one_octet;
  @(posedge clk) disable iff (!rst_n)
  flags_valid |-> ($past(addr_start) && $past(octet_valid));
endproperty
 
// ─── Ordering: validity signals fire in increasing octet order ─────────────
// Catches a decomposer that can report the prefix before the flags, which
// means its counter has a path the address does not.
property p_validity_order;
  @(posedge clk) disable iff (!rst_n)
  oui_valid |-> (octet_count >= 3);
endproperty
 
// ─── Conservation: the four address classes are exhaustive ─────────────────
// Two flags, four classes, no fifth. Catches an enum gaining a state that
// no combination of bits produces.
property p_address_class_exhaustive;
  @(posedge clk) disable iff (!rst_n)
  flags_valid |-> ((addr_class == ADDR_UNICAST_GLOBAL)
                || (addr_class == ADDR_UNICAST_LOCAL)
                || (addr_class == ADDR_GROUP_GLOBAL)
                || (addr_class == ADDR_GROUP_LOCAL));
endproperty
 
// ─── ADDRESS PROPERTY: broadcast is also a group address ───────────────────
// All ones sets the I/G bit, so broadcast satisfies the group test AND is an
// exact value. Catches logic treating them as disjoint, which loses
// broadcast frames on a receiver that checks group membership first.
property p_broadcast_is_group;
  @(posedge clk) disable iff (!rst_n)
  (addr_valid && is_broadcast) |-> is_group;
endproperty
 
// ─── Safety: comparison rejects at the first differing octet ───────────────
// Catches a comparison that continues after a mismatch, which wastes the
// early-out the streaming structure exists for.
property p_reject_is_early;
  @(posedge clk) disable iff (!rst_n)
  mismatch |-> !$past(failed_q);
endproperty
 
// ─── Conservation: a match requires all six octets ─────────────────────────
// Catches a match declared on a prefix alone, which accepts every address
// from the same manufacturer.
property p_match_requires_all_octets;
  @(posedge clk) disable iff (!rst_n)
  match |-> (idx_q == 3'd5);
endproperty
 
// ─── Mutual exclusion: a comparison matches or rejects, never both ─────────
property p_match_xor_mismatch;
  @(posedge clk) disable iff (!rst_n)
  !(match && mismatch);
endproperty
 
// ─── ADDRESS PROPERTY: a generated LAA has the U/L bit set ─────────────────
// Catches the bit placed at the wrong end of the octet -- which produces an
// address that is NOT locally administered, carries someone else's prefix,
// and may collide with a real device.
property p_generated_address_is_local;
  @(posedge clk) disable iff (!rst_n)
  addr_valid |-> address[41];
endproperty
 
// ─── Causation: the group flag follows the request ─────────────────────────
// Catches the two flag positions transposed, which produces group addresses
// when unicast was asked for.
property p_generated_group_flag_follows_request;
  @(posedge clk) disable iff (!rst_n)
  addr_valid |-> (address[40] == $past(make_group));
endproperty
 
// ─── Safety: a constant seed is reported as certain, not risky ─────────────
// Catches SEED_CONSTANT being treated as merely weak, which turns a
// guaranteed collision into a probabilistic-looking one.
property p_constant_seed_is_certain;
  @(posedge clk) disable iff (!rst_n)
  (address_seed_kind == SEED_CONSTANT) |-> seed_guarantees_collision;
endproperty
 
// ─── Causation: group addresses are excluded from prefix telemetry ─────────
// Catches them being counted, which corrupts the distribution with values
// that are not manufacturer identifiers at all.
property p_group_excluded_from_prefix_stats;
  @(posedge clk) disable iff (!rst_n)
  (oui_valid && is_group) |=> ((c_local_admin == $past(c_local_admin))
                            && (c_global_admin == $past(c_global_admin)));
endproperty
 
// ─── Ordering: a duplicate requires sustained flapping, not one move ───────
// THE property of Section 9. Catches a detector that flags the first port
// change, which fires on every legitimate failover and gets disabled --
// taking the genuine detection with it.
property p_duplicate_requires_flapping;
  @(posedge clk) disable iff (!rst_n)
  duplicate_suspected |-> ($past(flaps_q[hit_idx_c]) + 1 >= FLAP_THRESHOLD);
endproperty
 
// ─── Mutual exclusion: a move and a duplicate are not both reported ────────
property p_move_xor_duplicate;
  @(posedge clk) disable iff (!rst_n)
  !(move_observed && duplicate_suspected);
endproperty
 
// ─── Stability: the prefix set survives a clear ────────────────────────────
// Catches slot_used folded into the clear branch, destroying the record of
// which prefixes this segment carries.
property p_prefix_set_survives_clear;
  @(posedge clk) disable iff (!rst_n)
  clear |=> $stable(slot_used);
endproperty