"MAC Addresses Are Globally Unique Forever"

50% collision probability at N = 2^24 occurs at n ≈ 4 823
50% collision probability at N = 2^46 occurs at n ≈ 9 876 831

// ---------------------------------------------------------------------
// uniqmyth_pkg -- the address-space and collision arithmetic, with the
// free-bit count DERIVED from what a generator fixes rather than taken
// from the field width.
//
// Unit: Chapter 23.3 Section 2's bitcell equivalent.
//   1 BCE = one bit of usable on-die SRAM = 0.35 GE
//   1 flip-flop = 20 BCE
//   Chapter 19.7 Section 19's MAC receive datapath = 283 320 BCE
//   Chapter 23.3's MAC table = 128k x 96 b = 1.26e7 BCE
// ---------------------------------------------------------------------
package uniqmyth_pkg;

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

  localparam int unsigned ADDR_BITS = 48;
  localparam int unsigned BIT_IG    = 0;   // Chapter 5.3 Section 2
  localparam int unsigned BIT_UL    = 1;

  // Chapter 12.5's default aging interval.
  localparam int unsigned AGING_SECONDS = 300;

  typedef enum logic [1:0] {
    GEN_UNIFORM_46  = 2'd0,   // the arithmetic everybody quotes
    GEN_FIXED_OCTET = 2'd1,   // first octet pinned to 0x02
    GEN_VENDOR_PFX  = 2'd2,   // plus a 24-bit product prefix
    GEN_STRUCTURED  = 2'd3    // plus an 8-bit host or slot field
  } generator_e;

  // ---- derived: how many bits a generator actually leaves free -------
  function automatic int unsigned free_bits(generator_e g);
    case (g)
      GEN_UNIFORM_46:  return 46;   // 48 less I/G and U/L
      GEN_FIXED_OCTET: return 40;   // less the whole first octet
      GEN_VENDOR_PFX:  return 24;   // less a 24-bit prefix
      default:         return 16;   // less an 8-bit structured field
    endcase
  endfunction

  // ---- derived: the birthday bound -----------------------------------
  // P ~ 1 - exp(-n^2 / 2N). Integer hardware cannot evaluate exp, so
  // the model reports the EXPONENT's argument scaled, and a comparison
  // against thresholds gives the regime. The exact figure belongs in a
  // report, not in a datapath.
  //
  //   ratio_milli = 1000 * n^2 / (2 * 2^free_bits)
  //
  // ratio_milli >= 1386 corresponds to P >= 0.75
  // ratio_milli >=  693 corresponds to P >= 0.50
  // ratio_milli >=  105 corresponds to P >= 0.10
  function automatic int unsigned collision_ratio_milli(int unsigned n,
                                                        int unsigned bits);
    // n^2 can be large; shift the denominator instead of squaring up.
    int unsigned num;
    num = (n * n) / 1000;                  // keep the product in range
    if (bits >= 40) return 0;              // vanishing at this scale
    return (num * 1_000_000) >> (bits - 1);
  endfunction

  function automatic int unsigned half_point(int unsigned bits);
    // n at which P ~ 0.5 is sqrt(2 ln2 * N) ~ 1.1774 * 2^(bits/2).
    return (11_774 * (1 << (bits / 2))) / 10_000;
  endfunction

  // ---- derived: detector cost -----------------------------------------
  function automatic int unsigned detector_bce(int unsigned bits_per_entry);
    return MAC_TBL_ENTRIES * bits_per_entry;    // an array: 1 BCE/bit
  endfunction

  function automatic int unsigned table_bce();
    return MAC_TBL_ENTRIES * MAC_TBL_WIDTH;
  endfunction

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

endpackage

// ---------------------------------------------------------------------
// address_space_model -- the space a generator draws from, against the
// space the arithmetic assumes.
//
// The output that matters is bits_lost_to_structure. Every one of them
// is a deliberate, defensible design decision, and together they move
// the collision probability by six orders of magnitude.
// ---------------------------------------------------------------------
module address_space_model
  import uniqmyth_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,

  input  logic  [1:0] generator,        // generator_e
  input  logic [31:0] population,

  output logic [15:0] free_bits_o,
  output logic [15:0] bits_lost_to_structure,
  output logic [31:0] quoted_free_bits,
  output logic [31:0] half_point_n,
  output logic [31:0] ratio_milli,
  output logic        regime_negligible,
  output logic        regime_material,
  output logic        regime_likely,
  output logic        arithmetic_is_on_the_wrong_space,
  output logic [31:0] c_evaluations
);
  always_comb begin
    free_bits_o            = 16'(free_bits(generator_e'(generator)));
    quoted_free_bits       = 32'd46;
    bits_lost_to_structure = 16'(quoted_free_bits) - free_bits_o;

    half_point_n = 32'(half_point(int'(free_bits_o)));

    ratio_milli = 32'(collision_ratio_milli(int'(population),
                                            int'(free_bits_o)));

    regime_negligible = (ratio_milli <  32'd105);
    regime_material   = (ratio_milli >= 32'd105) && (ratio_milli < 32'd693);
    regime_likely     = (ratio_milli >= 32'd693);

    // THE finding, as one bit.
    arithmetic_is_on_the_wrong_space = (bits_lost_to_structure != 16'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

// ---------------------------------------------------------------------
// collision_model -- the birthday bound over the IMPLEMENTED space,
// reported as a regime and a headroom rather than as a probability.
//
// The output that matters is population_headroom: how many more
// addresses a deployment can add before it crosses the half point.
// ---------------------------------------------------------------------
module collision_model
  import uniqmyth_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,

  input  logic [15:0] free_bits_i,
  input  logic [31:0] population,
  input  logic [31:0] population_growth_per_year,

  output logic [31:0] half_point_o,
  output logic [31:0] population_headroom,
  output logic [15:0] years_of_headroom,
  output logic [31:0] ratio_milli_o,
  output logic  [1:0] regime,           // 0 negligible, 1 material, 2 likely
  output logic        past_half_point,
  output logic        allocation_recommended,
  output logic [31:0] c_regime_changes
);
  logic [1:0] regime_q;

  always_comb begin
    half_point_o  = 32'(half_point(int'(free_bits_i)));
    ratio_milli_o = 32'(collision_ratio_milli(int'(population),
                                              int'(free_bits_i)));

    past_half_point     = (population >= half_point_o);
    population_headroom = past_half_point ? 32'd0
                                          : (half_point_o - population);

    years_of_headroom = (population_growth_per_year == 0) ? 16'hFFFF
                      : 16'(population_headroom / population_growth_per_year);

    regime = (ratio_milli_o >= 32'd693) ? 2'd2
           : (ratio_milli_o >= 32'd105) ? 2'd1
                                        : 2'd0;

    // Section 2's callout: past the material regime, randomness is the
    // wrong mechanism and allocation is the right one.
    allocation_recommended = (regime != 2'd0);
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      regime_q <= 2'd0; c_regime_changes <= '0;
    end else begin
      regime_q <= regime;
      if (regime != regime_q) c_regime_changes <= c_regime_changes + 32'd1;
    end
  end
endmodule

// ---------------------------------------------------------------------
// correlation_model -- the process-failure term the birthday bound has
// no representation for, and which dominates at small populations.
//
// The output that matters is dominant_mechanism: at a given population
// and space, is the likelier cause chance or a tool? The two have
// different fixes and nothing else distinguishes them.
// ---------------------------------------------------------------------
module correlation_model
  import uniqmyth_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,

  input  logic [31:0] population,
  input  logic [15:0] free_bits_i,
  input  logic [31:0] failure_rate_ppb,     // per device, parts per billion
  input  logic        same_lot_observed,
  input  logic        same_prefix_observed,
  input  logic        virtual_interfaces,

  output logic [31:0] birthday_ratio_milli,
  output logic [31:0] process_ratio_milli,
  output logic        process_dominates,
  output logic  [1:0] dominant_mechanism,   // 0 chance, 1 process, 2 merge
  output logic  [2:0] recommended_action,
  output logic        duplicates_are_co_located,
  output logic [31:0] c_diagnoses
);
  // recommended_action: 1 audit manufacturing, 2 widen the space,
  //                     3 fix the generator, 4 allocate prefixes.
  always_comb begin
    birthday_ratio_milli = 32'(collision_ratio_milli(int'(population),
                                                     int'(free_bits_i)));

    // 1 - exp(-rN) ~ rN for small rN. Scaled to the same milli units.
    process_ratio_milli = (failure_rate_ppb * population) / 32'd1_000_000;

    process_dominates = (process_ratio_milli > birthday_ratio_milli);

    dominant_mechanism = same_prefix_observed ? 2'd2
                       : process_dominates    ? 2'd1
                                              : 2'd0;

    recommended_action = same_prefix_observed ? 3'd4
                       : virtual_interfaces   ? 3'd3
                       : process_dominates    ? 3'd1
                                              : 3'd2;

    // THE fact the birthday bound has no term for: a lot ships to one
    // customer, so a process duplicate arrives pre-paired.
    duplicates_are_co_located = same_lot_observed;
  end

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

teardown interval = 3 600 ÷ churn per hour
stale entries at any instant = 300 ÷ teardown interval

// ---------------------------------------------------------------------
// recycle_model -- what "forever" means in a fleet that reissues
// addresses, and how many forwarding entries refer to stations that no
// longer exist.
//
// The output that matters is entry_may_be_inherited: a reissued address
// whose predecessor's entry is still live is indistinguishable from a
// station that moved.
// ---------------------------------------------------------------------
module recycle_model
  import uniqmyth_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,

  input  logic [31:0] churn_per_hour,
  input  logic [15:0] aging_seconds,
  input  logic [31:0] table_entries,
  input  logic        old_holder_still_transmitting,

  output logic [31:0] teardown_interval_ms,
  output logic [31:0] stale_entries_x100,
  output logic [15:0] stale_share_ppm,
  output logic        entry_may_be_inherited,
  output logic        genuine_duplicate,
  output logic [31:0] recommended_aging_s,
  output logic        aging_is_too_long,
  output logic [31:0] c_inheritances
);
  always_comb begin
    teardown_interval_ms = (churn_per_hour == 0) ? 32'hFFFF_FFFF
                         : (32'd3_600_000 / churn_per_hour);

    // 300 s / interval, in hundredths so a sub-unit answer survives.
    stale_entries_x100 = (teardown_interval_ms == 0) ? 32'd0
                       : ((32'(aging_seconds) * 32'd100_000)
                          / teardown_interval_ms);

    stale_share_ppm = (table_entries == 0) ? 16'd0
                    : 16'(((stale_entries_x100 / 32'd100) * 32'd1_000_000)
                          / table_entries);

    // An address reissued inside the aging window inherits an entry.
    entry_may_be_inherited = (teardown_interval_ms
                              < (32'(aging_seconds) * 32'd1000));

    // And if the previous holder is still alive, it is not an
    // inheritance at all -- it is Section 4's duplicate.
    genuine_duplicate = entry_may_be_inherited
                     && old_holder_still_transmitting;

    // The derivation the callout argued for: a small multiple of the
    // recycle interval rather than a constant from 1990.
    recommended_aging_s = (teardown_interval_ms * 32'd10) / 32'd1000;
    aging_is_too_long   = (32'(aging_seconds) > recommended_aging_s)
                       && (recommended_aging_s != 32'd0);
  end

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

// ---------------------------------------------------------------------
// move_tracker -- twenty bits beside each forwarding entry, and the
// rate test that separates a failover from a duplicate.
//
// Chapter 5.3 Section 9 built this over sixteen entries as a teaching
// model. This is the version a 128k-entry table would carry, and the
// difference is that the storage is now a real number.
// ---------------------------------------------------------------------
module move_tracker
  import uniqmyth_pkg::*;
#(
  parameter int unsigned ENTRIES        = 128 * 1024,
  parameter int unsigned IDX_W          = 17,
  parameter int unsigned FLAP_THRESHOLD = 8,
  parameter int unsigned WINDOW_S       = 10
)(
  input  logic             clk,
  input  logic             rst_n,
  input  logic             tick_s,

  input  logic             learn_valid,
  input  logic [IDX_W-1:0] entry_idx,
  input  logic      [15:0] port_now,
  input  logic      [15:0] port_stored,
  input  logic             entry_present,

  output logic             is_move,
  output logic             duplicate_suspected,
  output logic       [3:0] move_count_o,
  output logic      [15:0] last_move_s_o,
  output logic      [15:0] previous_port_o,
  output logic [31:0]      detector_bce_o,
  output logic [31:0]      detector_dp_milli,
  output logic [15:0]      table_overhead_pct_x10,
  output logic [31:0]      c_moves,
  output logic [31:0]      c_duplicates
);
  logic  [3:0] move_count [ENTRIES];
  logic [15:0] last_move  [ENTRIES];
  logic [15:0] prev_port  [ENTRIES];
  logic [15:0] now_s;

  always_comb begin
    // Twenty bits of history, plus sixteen for the previous port.
    detector_bce_o    = 32'(detector_bce(4 + 16 + 16));
    detector_dp_milli = 32'(datapaths_milli(detector_bce_o));
    table_overhead_pct_x10 = 16'((detector_bce_o * 32'd1000)
                                 / 32'(table_bce()));

    is_move = learn_valid && entry_present && (port_now != port_stored);

    // Chapter 5.3 Section 9's rate test: a failover moves once and
    // stops; a duplicate moves continuously while both stations send.
    duplicate_suspected =
      is_move
      && (move_count[entry_idx] >= 4'(FLAP_THRESHOLD))
      && ((now_s - last_move[entry_idx]) <= 16'(WINDOW_S));

    move_count_o    = move_count[entry_idx];
    last_move_s_o   = last_move[entry_idx];
    previous_port_o = prev_port[entry_idx];
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      now_s <= '0; c_moves <= '0; c_duplicates <= '0;
      for (int i = 0; i < ENTRIES; i++) begin
        move_count[i] <= '0; last_move[i] <= '0; prev_port[i] <= '0;
      end
    end else begin
      if (tick_s) now_s <= now_s + 16'd1;

      if (is_move) begin
        // The port that is about to be overwritten -- Section 12's
        // whole subject, preserved for the cost of one field.
        prev_port[entry_idx]  <= port_stored;
        last_move[entry_idx]  <= now_s;
        c_moves               <= c_moves + 32'd1;

        if ((now_s - last_move[entry_idx]) <= 16'(WINDOW_S)) begin
          if (move_count[entry_idx] != 4'hF)
            move_count[entry_idx] <= move_count[entry_idx] + 4'd1;
        end else begin
          // Outside the window, the history is stale: a failover a day
          // ago says nothing about today.
          move_count[entry_idx] <= 4'd1;
        end

        if (duplicate_suspected) c_duplicates <= c_duplicates + 32'd1;
      end
    end
  end
endmodule

to distinguish the fault from the normal case you need the RATE
to compute the rate you need the PREVIOUS event's time
the previous event's record was overwritten by the current one
and overwriting is the structure's specified behaviour

// ---------------------------------------------------------------------
// shadow_witness -- the second, independent record that Section 12's
// argument requires.
//
// The point is what it is NOT indexed by. A structure keyed on the
// address inherits the address's ambiguity; this one is keyed on the
// EVENT, so two stations sharing an address produce two records.
// ---------------------------------------------------------------------
module shadow_witness
  import uniqmyth_pkg::*;
#(
  parameter int unsigned DEPTH = 64,
  parameter int unsigned PTR_W = 6
)(
  input  logic        clk,
  input  logic        rst_n,
  input  logic        tick_s,
  input  logic        clear,

  input  logic        move_event,
  input  logic [47:0] address,
  input  logic [15:0] port_from,
  input  logic [15:0] port_to,

  input  logic        read_en,
  input  logic [PTR_W-1:0] read_idx,

  output logic [47:0] r_address,
  output logic [15:0] r_port_from,
  output logic [15:0] r_port_to,
  output logic [15:0] r_time_s,
  output logic        r_valid,
  output logic [PTR_W-1:0] entries_used,
  output logic        wrapped,
  output logic        keyed_by_address,
  output logic [31:0] witness_bce_o,
  output logic [31:0] c_events,
  output logic [31:0] c_lost_to_wrap
);
  logic [47:0] a_addr [DEPTH];
  logic [15:0] a_from [DEPTH];
  logic [15:0] a_to   [DEPTH];
  logic [15:0] a_time [DEPTH];
  logic        a_val  [DEPTH];
  logic [PTR_W-1:0] wptr;
  logic [15:0] now_s;

  always_comb begin
    // 48 + 16 + 16 + 16 + 1 bits per entry.
    witness_bce_o = 32'(DEPTH) * 32'd97;

    // THE structural property. A log keyed on the event cannot lose an
    // entry to a key collision, because it has no key.
    keyed_by_address = 1'b0;

    r_address   = a_addr[read_idx];
    r_port_from = a_from[read_idx];
    r_port_to   = a_to[read_idx];
    r_time_s    = a_time[read_idx];
    r_valid     = a_val[read_idx] && read_en;
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n || clear) begin
      wptr <= '0; now_s <= '0; entries_used <= '0; wrapped <= 1'b0;
      c_events <= '0; c_lost_to_wrap <= '0;
      for (int i = 0; i < DEPTH; i++) a_val[i] <= 1'b0;
    end else begin
      if (tick_s) now_s <= now_s + 16'd1;

      if (move_event) begin
        a_addr[wptr] <= address;
        a_from[wptr] <= port_from;
        a_to[wptr]   <= port_to;
        a_time[wptr] <= now_s;
        a_val[wptr]  <= 1'b1;

        // Chapter 21.9 Section 2's warning, honoured: a finite sink
        // must count what it could not keep.
        if (a_val[wptr]) c_lost_to_wrap <= c_lost_to_wrap + 32'd1;

        wptr <= wptr + 1'b1;
        if (wptr == PTR_W'(DEPTH - 1)) wrapped <= 1'b1;
        if (!wrapped && (entries_used != PTR_W'(DEPTH - 1)))
          entries_used <= entries_used + 1'b1;

        c_events <= c_events + 32'd1;
      end
    end
  end
endmodule

// ---------------------------------------------------------------------
// uniq_telemetry -- the counters that make a uniqueness claim
// falsifiable on a live switch.
//
// Design rule: the chapter's three errors -- the space, the
// distribution and the lifetime -- each need a different counter, and
// none of them is the drop counter anybody looks at.
// ---------------------------------------------------------------------
module uniq_telemetry
  import uniqmyth_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,
  input  logic        clear,
  input  logic        tick_s,

  input  logic        learn_valid,
  input  logic        is_move_i,
  input  logic        duplicate_suspected_i,
  input  logic        entry_inherited_i,
  input  logic [47:0] address,
  input  logic [31:0] distinct_addresses,

  output logic [47:0] c_learns,
  output logic [47:0] c_moves_o,
  output logic [47:0] c_duplicates_o,
  output logic [47:0] c_inherited,
  output logic [47:0] c_laa_seen,
  output logic [47:0] c_global_seen,
  output logic [31:0] move_rate_per_s,
  output logic [31:0] laa_share_ppm,
  output logic [31:0] population_o,
  output logic        laa_dominant,
  output logic        move_rate_is_pathological
);
  logic [31:0] moves_this_s;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n || clear) begin
      c_learns <= '0; c_moves_o <= '0; c_duplicates_o <= '0;
      c_inherited <= '0; c_laa_seen <= '0; c_global_seen <= '0;
      moves_this_s <= '0; move_rate_per_s <= '0;
    end else begin
      if (learn_valid) begin
        c_learns <= c_learns + 48'd1;
        // Chapter 5.3 Section 2: the U/L bit is bit 1 of octet 0.
        if (address[41]) c_laa_seen    <= c_laa_seen + 48'd1;
        else             c_global_seen <= c_global_seen + 48'd1;
      end
      if (is_move_i)             c_moves_o      <= c_moves_o + 48'd1;
      if (duplicate_suspected_i) c_duplicates_o <= c_duplicates_o + 48'd1;
      if (entry_inherited_i)     c_inherited    <= c_inherited + 48'd1;

      if (is_move_i) moves_this_s <= moves_this_s + 32'd1;
      if (tick_s) begin
        move_rate_per_s <= moves_this_s;
        moves_this_s    <= '0;
      end
    end
  end

  always_comb begin
    laa_share_ppm = (c_learns == 0) ? 32'd0
                  : 32'((c_laa_seen * 48'd1_000_000) / c_learns);

    population_o = distinct_addresses;

    // A segment dominated by locally administered addresses is a
    // segment where Section 2's arithmetic applies.
    laa_dominant = (laa_share_ppm >= 32'd500_000);

    // Section 4's callout: a duplicate flaps at the stations' combined
    // transmission rate, which is orders above any legitimate move.
    move_rate_is_pathological = (move_rate_per_s > 32'd100);
  end
endmodule

// ---------------------------------------------------------------------
// uniq_conformance -- the checks that hold a uniqueness claim to what
// the evidence supports.
//
// Note what is absent: there is no check that addresses ARE unique,
// because Section 12 established that the structure cannot represent
// the violation. Every check here is about the DETECTION instead.
// ---------------------------------------------------------------------
module uniq_conformance
  import uniqmyth_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,

  input  logic        claims_unique,
  input  logic [31:0] population,
  input  logic [15:0] free_bits_i,
  input  logic        history_present,
  input  logic        witness_present,
  input  logic        generator_reports_entropy,
  input  logic        is_move_i,
  input  logic        move_recorded,
  input  logic [31:0] move_rate,
  input  logic        duplicate_suspected_i,
  input  logic        both_ports_reported,

  output logic        v_claim_without_detection,
  output logic        v_evidence_overwritten,
  output logic        v_unauditable_generator,
  output logic        v_population_past_half,
  output logic        v_alarm_without_ports,
  output logic  [4:0] violations,
  output logic        conformant
);
  always_comb begin
    // 1. A uniqueness claim with no way to detect a violation.
    v_claim_without_detection = claims_unique && !history_present;

    // 2. Section 12: a move that overwrote the previous record and
    //    nothing kept it.
    v_evidence_overwritten = is_move_i && !move_recorded && !witness_present;

    // 3. Section 2: a generator that cannot say where its bits came
    //    from has an unauditable claim.
    v_unauditable_generator = claims_unique && !generator_reports_entropy;

    // 4. Section 5: past the half point, randomness is the wrong
    //    mechanism.
    v_population_past_half = (population >= 32'(half_point(int'(free_bits_i))));

    // 5. Section 10: an alarm that does not name both ports is an
    //    alarm rather than an instruction.
    v_alarm_without_ports = duplicate_suspected_i && !both_ports_reported;

    violations = { v_alarm_without_ports, v_population_past_half,
                   v_unauditable_generator, v_evidence_overwritten,
                   v_claim_without_detection };
    conformant = (violations == 5'b00000);
  end
endmodule

// A1. The quoted space is 46 bits and the model says so.
p_as_quoted: assert property (@(posedge clk) disable iff (!rst_n)
  (quoted_free_bits == 32'd46));

// A2. A vendor-prefixed generator leaves 24.
p_as_prefix: assert property (@(posedge clk) disable iff (!rst_n)
  (generator == 2'(GEN_VENDOR_PFX)) |-> (free_bits_o == 16'd24));

// A3. Bits lost is the difference, and it is never negative.
p_as_lost: assert property (@(posedge clk) disable iff (!rst_n)
  (bits_lost_to_structure == (16'(quoted_free_bits) - free_bits_o)));

// A4. Any structure at all makes the quoted arithmetic wrong.
p_as_wrong_space: assert property (@(posedge clk) disable iff (!rst_n)
  (bits_lost_to_structure != 16'd0) |-> arithmetic_is_on_the_wrong_space);

// A5. The half point falls as the space shrinks.
p_as_half_point_monotone: assert property (@(posedge clk) disable iff (!rst_n)
  (free_bits_o < $past(free_bits_o)) |-> (half_point_n <= $past(half_point_n)));

// A6. At 24 bits the half point is near 4 823.
p_as_half_24: assert property (@(posedge clk) disable iff (!rst_n)
  (free_bits_o == 16'd24) |-> ((half_point_n > 32'd4700) &&
                               (half_point_n < 32'd4950)));

// A7. Exactly one regime is reported.
p_as_one_regime: assert property (@(posedge clk) disable iff (!rst_n)
  $onehot({regime_negligible, regime_material, regime_likely}));

// A8. A larger population never moves to a safer regime.
p_as_monotone: assert property (@(posedge clk) disable iff (!rst_n)
  (population > $past(population)) |-> (ratio_milli >= $past(ratio_milli)));

// A9. At 40 free bits or more the model reports negligible.
p_as_large_space: assert property (@(posedge clk) disable iff (!rst_n)
  (free_bits_o >= 16'd40) |-> regime_negligible);

// B1. Headroom is zero past the half point.
p_co_headroom: assert property (@(posedge clk) disable iff (!rst_n)
  past_half_point |-> (population_headroom == 32'd0));

// B2. And is the difference otherwise.
p_co_headroom_value: assert property (@(posedge clk) disable iff (!rst_n)
  !past_half_point |-> (population_headroom == (half_point_o - population)));

// B3. Allocation is recommended from the material regime onward.
p_co_allocation: assert property (@(posedge clk) disable iff (!rst_n)
  (regime != 2'd0) |-> allocation_recommended);

// B4. The process term is linear in the population.
p_cr_linear: assert property (@(posedge clk) disable iff (!rst_n)
  (process_ratio_milli ==
   (failure_rate_ppb * population) / 32'd1_000_000));

// B5. And the birthday term is quadratic, so one must overtake.
p_cr_crossover_exists: assert property (@(posedge clk) disable iff (!rst_n)
  ((population > 32'd1_000_000) && (free_bits_i <= 16'd24))
    |-> !process_dominates);

// B6. A shared prefix overrides both and names a merge.
p_cr_merge: assert property (@(posedge clk) disable iff (!rst_n)
  same_prefix_observed |-> (dominant_mechanism == 2'd2));

// B7. Virtual interfaces point at the generator.
p_cr_generator: assert property (@(posedge clk) disable iff (!rst_n)
  (virtual_interfaces && !same_prefix_observed) |->
    (recommended_action == 3'd3));

// B8. A lot-mate duplicate is co-located.
p_cr_colocated: assert property (@(posedge clk) disable iff (!rst_n)
  same_lot_observed |-> duplicates_are_co_located);

// B9. Exactly one action is recommended.
p_cr_one_action: assert property (@(posedge clk) disable iff (!rst_n)
  (recommended_action != 3'd0));

// C1. The teardown interval is the churn's reciprocal.
p_rc_interval: assert property (@(posedge clk) disable iff (!rst_n)
  (churn_per_hour != 0) |->
    (teardown_interval_ms == (32'd3_600_000 / churn_per_hour)));

// C2. Inheritance happens when the interval is inside the aging window.
p_rc_inherit: assert property (@(posedge clk) disable iff (!rst_n)
  (teardown_interval_ms < (32'(aging_seconds) * 32'd1000))
    |-> entry_may_be_inherited);

// C3. A genuine duplicate needs the old holder alive.
p_rc_duplicate: assert property (@(posedge clk) disable iff (!rst_n)
  genuine_duplicate |-> (entry_may_be_inherited &&
                         old_holder_still_transmitting));

// C4. Stale entries rise with churn.
p_rc_stale_rises: assert property (@(posedge clk) disable iff (!rst_n)
  (churn_per_hour > $past(churn_per_hour)) |->
    (stale_entries_x100 >= $past(stale_entries_x100)));

// C5. The recommendation is derived, not constant.
p_rc_derived: assert property (@(posedge clk) disable iff (!rst_n)
  (recommended_aging_s == (teardown_interval_ms * 32'd10) / 32'd1000));

// C6. A 300-second default is too long above a threshold churn.
p_rc_default_too_long: assert property (@(posedge clk) disable iff (!rst_n)
  ((aging_seconds == 16'd300) && (churn_per_hour >= 32'd120))
    |-> aging_is_too_long);

// C7. Stale share never exceeds the table.
p_rc_share_bounded: assert property (@(posedge clk) disable iff (!rst_n)
  (stale_share_ppm <= 16'd1_000_000));

// C8. Zero churn means no inheritance.
p_rc_zero_churn: assert property (@(posedge clk) disable iff (!rst_n)
  (churn_per_hour == 32'd0) |-> !entry_may_be_inherited);

// D1. A move is a learn on a different port.
p_mv_definition: assert property (@(posedge clk) disable iff (!rst_n)
  is_move |-> (learn_valid && entry_present && (port_now != port_stored)));

// D2. A suspicion needs the count AND the window -- a rate, not a total.
p_mv_rate_not_total: assert property (@(posedge clk) disable iff (!rst_n)
  duplicate_suspected |-> ((move_count[entry_idx] >= 4'(FLAP_THRESHOLD)) &&
                           ((now_s - last_move[entry_idx]) <= 16'(WINDOW_S))));

// D3. A single move is never a suspicion.
p_mv_single_move_ok: assert property (@(posedge clk) disable iff (!rst_n)
  (is_move && (move_count[entry_idx] == 4'd0)) |-> !duplicate_suspected);

// D4. The previous port is preserved before the overwrite.
p_mv_prev_preserved: assert property (@(posedge clk) disable iff (!rst_n)
  is_move |=> (previous_port_o == $past(port_stored)));

// D5. The timestamp advances to now on every move.
p_mv_timestamp: assert property (@(posedge clk) disable iff (!rst_n)
  is_move |=> (last_move_s_o == $past(now_s)));

// D6. A move outside the window resets the count to one.
p_mv_window_resets: assert property (@(posedge clk) disable iff (!rst_n)
  (is_move && ((now_s - last_move[entry_idx]) > 16'(WINDOW_S))) |=>
    (move_count_o == 4'd1));

// D7. The count saturates rather than wrapping.
p_mv_saturates: assert property (@(posedge clk) disable iff (!rst_n)
  (move_count_o == 4'hF) |=> (move_count_o == 4'hF));

// D8. Every move is counted.
p_mv_counted: assert property (@(posedge clk) disable iff (!rst_n)
  is_move |=> (c_moves == $past(c_moves) + 32'd1));

// D9. The overhead is 37.5% of the table it instruments.
p_mv_overhead: assert property (@(posedge clk) disable iff (!rst_n)
  (table_overhead_pct_x10 == 16'd375));

// E1. The log has no key, which is the whole design.
p_sw_keyless: assert property (@(posedge clk) disable iff (!rst_n)
  (keyed_by_address == 1'b0));

// E2. Every move event writes an entry.
p_sw_writes: assert property (@(posedge clk) disable iff (!rst_n)
  move_event |=> (c_events == $past(c_events) + 32'd1));

// E3. Overwriting a valid entry counts a loss.
p_sw_loss_counted: assert property (@(posedge clk) disable iff (!rst_n)
  (move_event && a_val[wptr]) |=>
    (c_lost_to_wrap == $past(c_lost_to_wrap) + 32'd1));

// E4. The write pointer advances by one and wraps.
p_sw_pointer: assert property (@(posedge clk) disable iff (!rst_n)
  move_event |=> (wptr == PTR_W'($past(wptr) + 1)));

// E5. A read returns the recorded transition.
p_sw_read: assert property (@(posedge clk) disable iff (!rst_n)
  (read_en && a_val[read_idx]) |-> r_valid);

// E6. The same address may appear twice with different destinations --
//     which a keyed structure could not represent.
p_sw_two_records: assert property (@(posedge clk) disable iff (!rst_n)
  (r_valid && (r_address == $past(r_address)) &&
   (r_port_to != $past(r_port_to))) |-> 1'b1);

// E7. Entries used never exceeds the depth.
p_sw_bounded: assert property (@(posedge clk) disable iff (!rst_n)
  (entries_used < PTR_W'(DEPTH)));

// E8. Clearing invalidates everything.
p_sw_clear: assert property (@(posedge clk) disable iff (!rst_n)
  clear |=> (entries_used == '0));

// F1. The U/L bit classifies every learned address.
p_tl_classify: assert property (@(posedge clk) disable iff (!rst_n)
  (c_learns == c_laa_seen + c_global_seen));

// F2. A locally administered majority selects the birthday arithmetic.
p_tl_laa_dominant: assert property (@(posedge clk) disable iff (!rst_n)
  (laa_share_ppm >= 32'd500_000) |-> laa_dominant);

// F3. A pathological move rate is orders above a legitimate one.
p_tl_rate: assert property (@(posedge clk) disable iff (!rst_n)
  move_rate_is_pathological |-> (move_rate_per_s > 32'd100));

// F4. A claim with no detection is a violation.
p_cf_claim_needs_detection: assert property (@(posedge clk) disable iff (!rst_n)
  (claims_unique && !history_present) |-> v_claim_without_detection);

// F5. A move with nothing recorded and no witness loses the evidence.
p_cf_evidence: assert property (@(posedge clk) disable iff (!rst_n)
  (is_move_i && !move_recorded && !witness_present) |-> v_evidence_overwritten);

// F6. A generator that cannot report its entropy is unauditable.
p_cf_generator: assert property (@(posedge clk) disable iff (!rst_n)
  (claims_unique && !generator_reports_entropy) |-> v_unauditable_generator);

// F7. An alarm without both ports is an alarm, not an instruction.
p_cf_ports: assert property (@(posedge clk) disable iff (!rst_n)
  (duplicate_suspected_i && !both_ports_reported) |-> v_alarm_without_ports);

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

c_as_prefixed:     cover property (@(posedge clk) free_bits_o == 16'd24);
c_as_structured:   cover property (@(posedge clk) free_bits_o == 16'd16);
c_as_material:     cover property (@(posedge clk) regime_material);
c_as_likely:       cover property (@(posedge clk) regime_likely);
c_cr_process:      cover property (@(posedge clk) process_dominates);
c_cr_merge:        cover property (@(posedge clk) dominant_mechanism == 2'd2);
c_rc_inherited:    cover property (@(posedge clk) entry_may_be_inherited);
c_rc_duplicate:    cover property (@(posedge clk) genuine_duplicate);
c_mv_failover:     cover property (@(posedge clk) is_move && !duplicate_suspected);
c_mv_duplicate:    cover property (@(posedge clk) duplicate_suspected);
c_mv_saturated:    cover property (@(posedge clk) move_count_o == 4'hF);
c_sw_wrapped:      cover property (@(posedge clk) wrapped);
c_sw_lost:         cover property (@(posedge clk) c_lost_to_wrap != 32'd0);
c_cf_unauditable:  cover property (@(posedge clk) v_unauditable_generator);