"Full-Duplex Ethernet Uses CSMA/CD"

slotTime > round-trip propagation of the collision domain + maximum jam time

round trip available = slotTime − jamTime
one-way budget       = (slotTime − jamTime) ÷ 2
maximum diameter     = one-way budget ÷ propagation delay per metre

// ---------------------------------------------------------------------
// slotmyth_pkg -- the constants for converting a timing parameter into
// a distance, and for following the minimum frame forward into silicon.
//
// Unit: Chapter 23.3 Section 2's bitcell equivalent.
//   1 BCE = 0.35 GE = one bit of usable on-die SRAM
//   1 flip-flop = 20 BCE
//   Chapter 19.7 Section 19's MAC receive datapath = 283 320 BCE
// ---------------------------------------------------------------------
package slotmyth_pkg;

  localparam int unsigned DATAPATH_BCE = 283_320;
  localparam int unsigned BCE_PER_FLOP = 20;

  // ---- Chapter 1.2's normative parameters ------------------------------
  localparam int unsigned SLOT_TIME_BITS      = 512;
  localparam int unsigned SLOT_TIME_BITS_EXT  = 4_096;   // carrier extension
  localparam int unsigned JAM_SIZE_BITS       = 32;
  localparam int unsigned MIN_FRAME_OCTETS    = 64;      // 512 bits
  localparam int unsigned ATTEMPT_LIMIT       = 16;

  // ---- Chapter 24.3 Section 1's framing ---------------------------------
  localparam int unsigned OCT_PREAMBLE = 8;
  localparam int unsigned OCT_IFG      = 12;
  localparam int unsigned OCT_FIXED    = 38;

  // ---- Chapter 8.2 Section 3's velocity, hundredths of ns per metre -----
  localparam int unsigned NS_PER_M_CU_X100 = 505;
  localparam int unsigned NS_PER_M_FI_X100 = 490;

  // ---- Chapter 23.3 Section 2's part ------------------------------------
  localparam int unsigned SWITCH_PORTS   = 64;
  localparam int unsigned CORE_MHZ       = 1_200;

  typedef enum logic [1:0] {
    LINK_SHARED_HALF = 2'd0,   // a collision domain exists
    LINK_P2P_HALF    = 2'd1,   // two stations, one cable
    LINK_P2P_FULL    = 2'd2    // Chapter 1.5's deletion applies
  } linkmode_e;

  // ---- derived: a slot time is a distance -------------------------------
  // bit_time_ps: picoseconds per bit at a given rate in Mb/s.
  function automatic int unsigned bit_time_ps(int unsigned mbps);
    return 1_000_000 / mbps;
  endfunction

  function automatic int unsigned slot_ps(int unsigned mbps,
                                          int unsigned slot_bits);
    return slot_bits * bit_time_ps(mbps);
  endfunction

  function automatic int unsigned round_trip_ps(int unsigned mbps,
                                                int unsigned slot_bits);
    // Chapter 1.2 Section 3: the budget is the slot less the jam.
    return slot_ps(mbps, slot_bits) - (JAM_SIZE_BITS * bit_time_ps(mbps));
  endfunction

  function automatic int unsigned diameter_cm(int unsigned mbps,
                                              int unsigned slot_bits);
    // one-way picoseconds / (ns per metre x 100) gives centimetres x 10,
    // so divide once more by 10.
    return (round_trip_ps(mbps, slot_bits) / 2) * 100
         / (NS_PER_M_CU_X100 * 10);
  endfunction

  // ---- derived: the minimum frame's wire cost ---------------------------
  function automatic int unsigned min_wire_slot();
    return MIN_FRAME_OCTETS + OCT_PREAMBLE + OCT_IFG;    // 84
  endfunction

  function automatic int unsigned framing_tax_ppm(int unsigned payload);
    return (OCT_FIXED * 1_000_000) / (payload + OCT_FIXED);
  endfunction

  // ---- derived: the packet rate the minimum frame sets ------------------
  function automatic int unsigned pps_k(int unsigned gbps,
                                        int unsigned slot_oct);
    return (gbps * 1_000_000) / (slot_oct * 8);
  endfunction

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

endpackage

// ---------------------------------------------------------------------
// slot_diameter_model -- a bit-time budget expressed as the distance
// it was chosen to bound.
//
// The output that matters is diameter_cm_o, because it makes visible
// what no design reports: the parameter is a length, and it divides by
// ten every time the rate multiplies by ten.
// ---------------------------------------------------------------------
module slot_diameter_model
  import slotmyth_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,

  input  logic [31:0] rate_mbps,
  input  logic [15:0] slot_bits,
  input  logic [15:0] link_metres,
  input  logic  [1:0] link_mode,           // linkmode_e

  output logic [31:0] slot_ps_o,
  output logic [31:0] round_trip_ps_o,
  output logic [31:0] diameter_cm_o,
  output logic [31:0] link_round_trip_ps,
  output logic [31:0] margin_x10,
  output logic        bound_is_satisfied,
  output logic        bound_is_meaningful,
  output logic        mechanism_is_reachable,
  output logic [31:0] c_evaluations
);
  always_comb begin
    slot_ps_o       = 32'(slot_ps(int'(rate_mbps), int'(slot_bits)));
    round_trip_ps_o = 32'(round_trip_ps(int'(rate_mbps), int'(slot_bits)));
    diameter_cm_o   = 32'(diameter_cm(int'(rate_mbps), int'(slot_bits)));

    // This link's actual round trip.
    link_round_trip_ps = (32'(link_metres) * 32'(NS_PER_M_CU_X100) * 32'd2)
                       / 32'd100 * 32'd1000;

    margin_x10 = (link_round_trip_ps == 0) ? 32'hFFFF_FFFF
               : ((round_trip_ps_o * 32'd10) / link_round_trip_ps);

    bound_is_satisfied = (link_round_trip_ps <= round_trip_ps_o);

    // THE distinction. A bound on medium acquisition is meaningful only
    // where a medium is acquired -- which needs a second transmitter.
    bound_is_meaningful = (link_mode == 2'(LINK_SHARED_HALF));

    // Chapter 1.5 Section 2: five of six blocks become unreachable.
    mechanism_is_reachable = (link_mode != 2'(LINK_P2P_FULL));
  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

// ---------------------------------------------------------------------
// point_to_point_bound -- whether a link's slot-time constraint is
// satisfied, and whether it constrains anything.
//
// The two outputs are deliberately separate. A design that reports
// only the first has told an operator that a vacuous constraint is
// being met, which is Section 20's rejected property.
// ---------------------------------------------------------------------
module point_to_point_bound
  import slotmyth_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,

  input  logic [15:0] link_metres,
  input  logic [31:0] rate_mbps,
  input  logic [15:0] slot_bits,
  input  logic        separate_tx_rx_pairs,
  input  logic [15:0] stations_on_segment,

  output logic [31:0] link_round_trip_ns_x10,
  output logic [31:0] budget_ns_x10,
  output logic [31:0] margin_x10,
  output logic        bound_satisfied,
  output logic        collisions_possible,
  output logic        bound_constrains_anything,
  output logic        slot_counter_reachable,
  output logic        backoff_reachable,
  output logic  [1:0] mode,
  output logic [31:0] c_vacuous_evaluations
);
  always_comb begin
    link_round_trip_ns_x10 = (32'(link_metres) * 32'(NS_PER_M_CU_X100) * 32'd2)
                           / 32'd10;

    budget_ns_x10 = 32'(round_trip_ps(int'(rate_mbps), int'(slot_bits)))
                  / 32'd100;

    margin_x10 = (link_round_trip_ns_x10 == 0) ? 32'hFFFF_FFFF
               : ((budget_ns_x10 * 32'd10) / link_round_trip_ns_x10);

    bound_satisfied = (link_round_trip_ns_x10 <= budget_ns_x10);

    // THE question the margin does not answer. Two transmitters that
    // can be active at once is what makes a collision possible, and
    // separate pairs remove it regardless of the station count.
    collisions_possible = !separate_tx_rx_pairs && (stations_on_segment >= 16'd2);

    bound_constrains_anything = collisions_possible;

    mode = separate_tx_rx_pairs ? 2'(LINK_P2P_FULL)
         : (stations_on_segment <= 16'd2) ? 2'(LINK_P2P_HALF)
                                          : 2'(LINK_SHARED_HALF);

    // Chapter 1.5 Section 2's deletion, as reachability.
    slot_counter_reachable = collisions_possible;
    backoff_reachable      = collisions_possible;
  end

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

// ---------------------------------------------------------------------
// min_frame_cost -- what the 64-octet minimum costs on the wire, and
// what its timing justification is worth on this link.
//
// The output that matters is justification_still_applies, which is
// low on every link anybody deploys -- and the constant is there
// anyway, because Chapter 5.10's runt check is in every MAC.
// ---------------------------------------------------------------------
module min_frame_cost
  import slotmyth_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,

  input  logic [15:0] payload_octets,
  input  logic [15:0] min_frame_octets,
  input  logic        collisions_possible_i,
  input  logic [15:0] rate_gbps,

  output logic [15:0] padded_payload,
  output logic [15:0] frame_octets,
  output logic [31:0] wire_slot,
  output logic [31:0] useful_ppm,
  output logic [31:0] pad_octets,
  output logic [31:0] framing_tax_ppm_o,
  output logic [31:0] pps_k_o,
  output logic [31:0] ns_per_frame_x100,
  output logic        justification_still_applies,
  output logic        constant_is_frozen,
  output logic [31:0] c_padded_frames
);
  always_comb begin
    // Chapter 5.6: short payloads are padded, not shortened.
    padded_payload = (payload_octets < (min_frame_octets - 16'd18))
                   ? (min_frame_octets - 16'd18) : payload_octets;

    pad_octets   = 32'(padded_payload) - 32'(payload_octets);
    frame_octets = padded_payload + 16'd18;
    wire_slot    = 32'(frame_octets) + 32'(OCT_PREAMBLE) + 32'(OCT_IFG);

    useful_ppm = (wire_slot == 0) ? 32'd0
               : ((32'(payload_octets) * 1_000_000) / wire_slot);

    framing_tax_ppm_o = 32'(framing_tax_ppm(int'(padded_payload)));

    pps_k_o = 32'(pps_k(int'(rate_gbps), int'(wire_slot)));
    ns_per_frame_x100 = (pps_k_o == 0) ? 32'd0
                      : (100_000_000 / pps_k_o);

    // Section 4: the timing reason needs a collision domain.
    justification_still_applies = collisions_possible_i;

    // And Chapter 5.10's runt check holds it in place regardless.
    constant_is_frozen = 1'b1;
  end

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

packets per second = rate ÷ (wire slot × 8)
at 84 octets:  100 Gb/s → 148.81 Mpps
               400 Gb/s → 595.24 Mpps
               800 Gb/s → 1 190.48 Mpps

64 × 148.81 Mpps = 9.524 Gpps
at a 1.2 GHz core clock: 9.524 ÷ 1.2 = 7.94 packets per cycle
→ an eight-wide pipeline

// ---------------------------------------------------------------------
// pipeline_width_model -- the chain from a 1980 timing parameter to a
// 2026 pipeline width, with every step visible.
//
// The output that matters is width_traceable_to_slot_time, which is
// high: every term between the two is a division.
// ---------------------------------------------------------------------
module pipeline_width_model
  import slotmyth_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,

  input  logic [15:0] min_frame_octets,
  input  logic [15:0] ports,
  input  logic [15:0] port_gbps,
  input  logic [15:0] core_mhz,

  output logic [31:0] wire_slot_o,
  output logic [31:0] port_pps_k,
  output logic [31:0] aggregate_pps_k,
  output logic [31:0] packets_per_cycle_x100,
  output logic [15:0] pipeline_width,
  output logic [31:0] width_if_128,
  output logic [31:0] width_if_256,
  output logic        width_traceable_to_slot_time,
  output logic [31:0] c_evaluations
);
  logic [31:0] slot_128, slot_256, pps_128, pps_256;

  always_comb begin
    wire_slot_o = 32'(min_frame_octets) + 32'(OCT_PREAMBLE) + 32'(OCT_IFG);

    port_pps_k      = 32'(pps_k(int'(port_gbps), int'(wire_slot_o)));
    aggregate_pps_k = port_pps_k * 32'(ports);

    packets_per_cycle_x100 = (core_mhz == 0) ? 32'd0
                           : ((aggregate_pps_k * 32'd100)
                              / (32'(core_mhz) * 32'd1000));

    pipeline_width = 16'((packets_per_cycle_x100 + 32'd99) / 32'd100);

    // The counterfactuals, computed rather than asserted.
    slot_128 = 32'd128 + 32'(OCT_PREAMBLE) + 32'(OCT_IFG);
    slot_256 = 32'd256 + 32'(OCT_PREAMBLE) + 32'(OCT_IFG);
    pps_128  = 32'(pps_k(int'(port_gbps), int'(slot_128))) * 32'(ports);
    pps_256  = 32'(pps_k(int'(port_gbps), int'(slot_256))) * 32'(ports);

    width_if_128 = ((pps_128 * 32'd100) / (32'(core_mhz) * 32'd1000)
                    + 32'd99) / 32'd100;
    width_if_256 = ((pps_256 * 32'd100) / (32'(core_mhz) * 32'd1000)
                    + 32'd99) / 32'd100;

    // Every term between the slot time and the width is a division.
    width_traceable_to_slot_time = 1'b1;
  end

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

// ---------------------------------------------------------------------
// vestige_auditor -- every structure whose size the minimum frame
// sets, and whether the parameter's justification still applies.
//
// The output that matters is cost_is_legacy, which is high on every
// deployed link -- and the costs are real and paid anyway.
// ---------------------------------------------------------------------
module vestige_auditor
  import slotmyth_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,

  input  logic [15:0] min_frame_octets,
  input  logic [15:0] cell_octets,
  input  logic [15:0] descriptor_octets,
  input  logic [15:0] port_gbps,
  input  logic        collisions_possible_i,

  output logic [31:0] wire_tax_ppm,
  output logic [31:0] cell_waste_ppm,
  output logic [31:0] descriptor_bw_ppm,
  output logic [31:0] pps_k_o,
  output logic [15:0] structures_affected,
  output logic        justification_applies,
  output logic        cost_is_legacy,
  output logic        smaller_would_be_worse,
  output logic [31:0] c_audits
);
  logic [31:0] wire_slot;

  always_comb begin
    wire_slot = 32'(min_frame_octets) + 32'(OCT_PREAMBLE) + 32'(OCT_IFG);

    // Chapter 24.3 Section 1's framing tax at the minimum.
    wire_tax_ppm = (wire_slot == 0) ? 32'd0
                 : ((32'(OCT_FIXED) * 1_000_000) / wire_slot);

    // Chapter 23.3 Section 9: a frame occupies a whole cell.
    cell_waste_ppm = (cell_octets == 0) ? 32'd0
                   : (((32'(cell_octets) - 32'(min_frame_octets)) * 1_000_000)
                      / 32'(cell_octets));

    pps_k_o = 32'(pps_k(int'(port_gbps), int'(wire_slot)));

    // Chapter 23.4 Section 5: one descriptor per frame, as a share of
    // the payload bandwidth.
    descriptor_bw_ppm = (min_frame_octets <= 16'd18) ? 32'd0
      : ((32'(descriptor_octets) * 1_000_000)
         / (32'(min_frame_octets) - 32'd18));

    // Section 10's table.
    structures_affected = 16'd5;

    justification_applies = collisions_possible_i;
    cost_is_legacy        = !collisions_possible_i;

    // And the direction that would help is the one people do not
    // propose: a LARGER minimum lowers every cost above.
    smaller_would_be_worse = 1'b1;
  end

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

// ---------------------------------------------------------------------
// half_duplex_detector -- whether the CSMA/CD machinery is reachable
// in this configuration, and whether the evidence agrees.
//
// The output that matters is evidence_contradicts_mode: a link
// configured full duplex that is reporting collisions is Chapter
// 11.4's duplex mismatch, and the slot-time margin says so.
// ---------------------------------------------------------------------
module half_duplex_detector
  import slotmyth_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,

  input  logic        configured_full_duplex,
  input  logic        peer_full_duplex_advertised,
  input  logic        collision_observed,
  input  logic        late_collision_observed,
  input  logic [31:0] margin_x10_i,
  input  logic [31:0] c_fcs_errors,
  input  logic [31:0] c_late_collisions,

  output logic        machinery_reachable,
  output logic        evidence_contradicts_mode,
  output logic        duplex_mismatch_suspected,
  output logic        distance_is_the_cause,
  output logic        mode_disagreement_is_the_cause,
  output logic  [1:0] recommended_check,
  output logic [31:0] c_contradictions
);
  // recommended_check: 1 = cable length, 2 = duplex negotiation,
  //                    3 = neither -- the machinery is unreachable.
  always_comb begin
    // Chapter 1.5 Section 2: full duplex makes them unreachable.
    machinery_reachable = !configured_full_duplex;

    // A collision on a link that cannot have one.
    evidence_contradicts_mode = configured_full_duplex && collision_observed;

    // Chapter 11.4's signature: one end full, the other half.
    duplex_mismatch_suspected = evidence_contradicts_mode
                             || (configured_full_duplex
                                 && !peer_full_duplex_advertised);

    // Section 4: a margin in the thousands rules distance out.
    distance_is_the_cause = late_collision_observed
                         && (margin_x10_i < 32'd20);   // margin below 2x

    mode_disagreement_is_the_cause = late_collision_observed
                                  && (margin_x10_i >= 32'd20);

    recommended_check = distance_is_the_cause          ? 2'd1
                      : mode_disagreement_is_the_cause ? 2'd2
                      : !machinery_reachable           ? 2'd3
                                                       : 2'd0;
  end

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

// ---------------------------------------------------------------------
// slotmyth_telemetry -- what a link should report about a mechanism
// it does not use, and about the constant that mechanism left behind.
//
// Design rule: a counter that should always read zero is worth keeping
// precisely because it should always read zero.
// ---------------------------------------------------------------------
module slotmyth_telemetry
  import slotmyth_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,
  input  logic        clear,

  input  logic        frame_tx,
  input  logic [15:0] frame_octets,
  input  logic        frame_padded,
  input  logic [15:0] pad_octets_i,
  input  logic        collision_observed_i,
  input  logic        late_collision_i,
  input  logic        configured_full_duplex_i,
  input  logic        fcs_error_i,

  output logic [47:0] c_frames,
  output logic [47:0] c_min_size_frames,
  output logic [47:0] c_padded,
  output logic [47:0] c_pad_octets,
  output logic [47:0] c_collisions,
  output logic [47:0] c_late_collisions_o,
  output logic [47:0] c_fcs_errors_o,
  output logic [47:0] c_impossible_collisions,
  output logic [31:0] min_size_share_ppm,
  output logic [31:0] pad_waste_ppm,
  output logic        should_always_be_zero,
  output logic        mismatch_evidence_present
);
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n || clear) begin
      c_frames <= '0; c_min_size_frames <= '0; c_padded <= '0;
      c_pad_octets <= '0; c_collisions <= '0; c_late_collisions_o <= '0;
      c_fcs_errors_o <= '0; c_impossible_collisions <= '0;
    end else begin
      if (frame_tx) begin
        c_frames <= c_frames + 48'd1;
        if (frame_octets <= 16'(MIN_FRAME_OCTETS))
          c_min_size_frames <= c_min_size_frames + 48'd1;
        if (frame_padded) begin
          c_padded     <= c_padded + 48'd1;
          c_pad_octets <= c_pad_octets + 48'(pad_octets_i);
        end
      end
      if (collision_observed_i) begin
        c_collisions <= c_collisions + 48'd1;
        // THE counter. On a full-duplex link this cannot happen, and
        // that is why it is worth one AND gate to record it.
        if (configured_full_duplex_i)
          c_impossible_collisions <= c_impossible_collisions + 48'd1;
      end
      if (late_collision_i) c_late_collisions_o <= c_late_collisions_o + 48'd1;
      if (fcs_error_i)      c_fcs_errors_o      <= c_fcs_errors_o + 48'd1;
    end
  end

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

    // Section 6: the pad is wire the payload did not use.
    pad_waste_ppm = (c_frames == 0) ? 32'd0
                  : 32'((c_pad_octets * 48'd1_000_000)
                        / (c_frames * 48'(min_wire_slot())));

    should_always_be_zero = configured_full_duplex_i;

    // Chapter 11.4's signature, as far as one end can see it.
    mismatch_evidence_present = (c_impossible_collisions != 48'd0)
                             || (c_late_collisions_o != 48'd0);
  end
endmodule

// ---------------------------------------------------------------------
// slotmyth_conformance -- the checks that hold a design's claims about
// CSMA/CD to the configuration it actually runs in.
//
// Note what is absent: there is no check that collisions do not occur,
// because on a full-duplex link the signal is tied low and the check
// would be Section 20's class 120.
// ---------------------------------------------------------------------
module slotmyth_conformance
  import slotmyth_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,

  input  logic        configured_full_duplex_i,
  input  logic        csma_cd_properties_bound,
  input  logic [31:0] csma_cd_cover_hits,
  input  logic        claims_csma_cd,
  input  logic [47:0] c_impossible_collisions_i,
  input  logic [31:0] margin_x10_i,
  input  logic        late_collision_i,
  input  logic        min_frame_reported,
  input  logic        diameter_reported,

  output logic        v_vacuous_properties,
  output logic        v_claims_csma_cd,
  output logic        v_impossible_collision,
  output logic        v_distance_blamed,
  output logic        v_min_frame_unreported,
  output logic        v_diameter_unreported,
  output logic  [5:0] violations,
  output logic        conformant
);
  always_comb begin
    // 1. Section 20's class 120: properties bound in a configuration
    //    that cannot reach their antecedents, with an empty cover.
    v_vacuous_properties = configured_full_duplex_i
                        && csma_cd_properties_bound
                        && (csma_cd_cover_hits == 32'd0);

    // 2. Prohibition 2 -- Chapter 1.5 Section 2's deletion.
    v_claims_csma_cd = configured_full_duplex_i && claims_csma_cd;

    // 3. A collision on a link that cannot have one.
    v_impossible_collision = (c_impossible_collisions_i != 48'd0);

    // 4. Prohibition 3 -- a margin in the thousands rules distance out.
    v_distance_blamed = late_collision_i && (margin_x10_i >= 32'd20);

    // 5 and 6. The two quantities a design should expose so the
    //    parameter's cost is auditable rather than folklore.
    v_min_frame_unreported = !min_frame_reported;
    v_diameter_unreported  = !diameter_reported;

    violations = { v_diameter_unreported, v_min_frame_unreported,
                   v_distance_blamed, v_impossible_collision,
                   v_claims_csma_cd, v_vacuous_properties };
    conformant = (violations == 6'b000000);
  end
endmodule

// A1. A bit time is the reciprocal of the rate.
p_sd_bit_time: assert property (@(posedge clk) disable iff (!rst_n)
  (rate_mbps != 32'd0) |-> (slot_ps_o == 32'(slot_bits) * (32'd1_000_000 / rate_mbps)));

// A2. The round-trip budget is the slot less the jam.
p_sd_budget: assert property (@(posedge clk) disable iff (!rst_n)
  (round_trip_ps_o == slot_ps_o - (32'(JAM_SIZE_BITS)
                                   * (32'd1_000_000 / rate_mbps))));

// A3. The diameter falls by ten for every factor of ten in rate.
p_sd_scales: assert property (@(posedge clk) disable iff (!rst_n)
  (rate_mbps == 32'd10 * $past(rate_mbps)) |->
    (diameter_cm_o <= $past(diameter_cm_o) / 32'd9));

// A4. At 10 Mb/s with 512 bit times the diameter is about 4 752 m.
p_sd_10m: assert property (@(posedge clk) disable iff (!rst_n)
  ((rate_mbps == 32'd10) && (slot_bits == 16'd512))
    |-> ((diameter_cm_o > 32'd470_000) && (diameter_cm_o < 32'd480_000)));

// A5. Carrier extension restores roughly eight times the diameter.
p_sd_extension: assert property (@(posedge clk) disable iff (!rst_n)
  ((rate_mbps == 32'd1000) && (slot_bits == 16'd4096))
    |-> (diameter_cm_o > 32'd40_000));

// A6. A full-duplex link cannot reach the mechanism.
p_sd_unreachable: assert property (@(posedge clk) disable iff (!rst_n)
  (link_mode == 2'(LINK_P2P_FULL)) |-> !mechanism_is_reachable);

// A7. And the bound means nothing there.
p_sd_meaningless: assert property (@(posedge clk) disable iff (!rst_n)
  (link_mode != 2'(LINK_SHARED_HALF)) |-> !bound_is_meaningful);

// A8. A shorter link has a larger margin.
p_sd_margin: assert property (@(posedge clk) disable iff (!rst_n)
  (link_metres < $past(link_metres)) |-> (margin_x10 >= $past(margin_x10)));

// A9. The slot time is always larger than the jam.
p_sd_jam_fits: assert property (@(posedge clk) disable iff (!rst_n)
  (slot_ps_o > 32'(JAM_SIZE_BITS) * (32'd1_000_000 / rate_mbps)));

// B1. A 3 m link satisfies the 10 Mb/s budget by over a thousand.
p_pp_margin: assert property (@(posedge clk) disable iff (!rst_n)
  ((link_metres == 16'd3) && (rate_mbps == 32'd10) && (slot_bits == 16'd512))
    |-> (margin_x10 > 32'd15_000));

// B2. Collisions need two transmitters sharing a medium.
p_pp_collisions: assert property (@(posedge clk) disable iff (!rst_n)
  separate_tx_rx_pairs |-> !collisions_possible);

// B3. And the station count alone does not create them.
p_pp_stations: assert property (@(posedge clk) disable iff (!rst_n)
  (separate_tx_rx_pairs && (stations_on_segment >= 16'd2))
    |-> !collisions_possible);

// B4. A two-station half-duplex link DOES have them.
p_pp_p2p_half: assert property (@(posedge clk) disable iff (!rst_n)
  (!separate_tx_rx_pairs && (stations_on_segment == 16'd2))
    |-> collisions_possible);

// B5. The bound constrains something only when collisions are possible.
p_pp_constrains: assert property (@(posedge clk) disable iff (!rst_n)
  (bound_constrains_anything == collisions_possible));

// B6. Both counters follow the same condition.
p_pp_reachable: assert property (@(posedge clk) disable iff (!rst_n)
  (slot_counter_reachable == backoff_reachable));

// B7. A satisfied and vacuous bound is counted.
p_pp_vacuous: assert property (@(posedge clk) disable iff (!rst_n)
  (bound_satisfied && !bound_constrains_anything)
    |=> (c_vacuous_evaluations == $past(c_vacuous_evaluations) + 32'd1));

// B8. The mode follows the two inputs.
p_pp_mode: assert property (@(posedge clk) disable iff (!rst_n)
  separate_tx_rx_pairs |-> (mode == 2'(LINK_P2P_FULL)));

// C1. A short payload is padded, never shortened.
p_mf_padded: assert property (@(posedge clk) disable iff (!rst_n)
  (payload_octets < (min_frame_octets - 16'd18))
    |-> (padded_payload == min_frame_octets - 16'd18));

// C2. A long payload is untouched.
p_mf_untouched: assert property (@(posedge clk) disable iff (!rst_n)
  (payload_octets >= (min_frame_octets - 16'd18))
    |-> (padded_payload == payload_octets));

// C3. The wire slot adds preamble and gap.
p_mf_slot: assert property (@(posedge clk) disable iff (!rst_n)
  (wire_slot == 32'(frame_octets) + 32'(OCT_PREAMBLE) + 32'(OCT_IFG)));

// C4. A one-octet payload uses 1.19% of its wire.
p_mf_one_octet: assert property (@(posedge clk) disable iff (!rst_n)
  ((payload_octets == 16'd1) && (min_frame_octets == 16'd64))
    |-> (useful_ppm == 32'd11_904));

// C5. The framing tax at minimum size is 45.24%.
p_mf_tax: assert property (@(posedge clk) disable iff (!rst_n)
  ((padded_payload == 16'd46)) |-> (framing_tax_ppm_o == 32'd452_380));

// C6. The justification needs a collision domain.
p_mf_justification: assert property (@(posedge clk) disable iff (!rst_n)
  (justification_still_applies == collisions_possible_i));

// C7. And the constant is frozen regardless.
p_mf_frozen: assert property (@(posedge clk) disable iff (!rst_n)
  constant_is_frozen);

// C8. Pad octets are the difference.
p_mf_pad: assert property (@(posedge clk) disable iff (!rst_n)
  (pad_octets == 32'(padded_payload) - 32'(payload_octets)));

// C9. Padded frames are counted.
p_mf_counted: assert property (@(posedge clk) disable iff (!rst_n)
  (pad_octets != 32'd0) |=> (c_padded_frames == $past(c_padded_frames) + 32'd1));

// D1. The packet rate is the line rate over the wire slot.
p_pw_rate: assert property (@(posedge clk) disable iff (!rst_n)
  (wire_slot_o != 32'd0) |->
    (port_pps_k == 32'(pps_k(int'(port_gbps), int'(wire_slot_o)))));

// D2. The aggregate is the per-port rate times the ports.
p_pw_aggregate: assert property (@(posedge clk) disable iff (!rst_n)
  (aggregate_pps_k == port_pps_k * 32'(ports)));

// D3. At 64 ports, 100 Gb/s and 64 octets, eight lanes.
p_pw_eight: assert property (@(posedge clk) disable iff (!rst_n)
  ((ports == 16'd64) && (port_gbps == 16'd100) &&
   (min_frame_octets == 16'd64) && (core_mhz == 16'd1200))
    |-> (pipeline_width == 16'd8));

// D4. A 128-octet minimum would give five.
p_pw_five: assert property (@(posedge clk) disable iff (!rst_n)
  ((ports == 16'd64) && (port_gbps == 16'd100) && (core_mhz == 16'd1200))
    |-> (width_if_128 == 32'd5));

// D5. The width never falls as the rate rises.
p_pw_monotone: assert property (@(posedge clk) disable iff (!rst_n)
  (port_gbps > $past(port_gbps)) |-> (pipeline_width >= $past(pipeline_width)));

// D6. A larger minimum frame narrows the pipeline.
p_pw_larger_narrower: assert property (@(posedge clk) disable iff (!rst_n)
  (width_if_256 <= width_if_128));

// D7. The chain is traceable to the slot time.
p_pw_traceable: assert property (@(posedge clk) disable iff (!rst_n)
  width_traceable_to_slot_time);

// D8. The width is a ceiling, never a floor.
p_pw_ceiling: assert property (@(posedge clk) disable iff (!rst_n)
  ((32'(pipeline_width) * 32'd100) >= packets_per_cycle_x100));

// E1. Five structures carry the parameter.
p_va_five: assert property (@(posedge clk) disable iff (!rst_n)
  (structures_affected == 16'd5));

// E2. The cost is legacy on a full-duplex link.
p_va_legacy: assert property (@(posedge clk) disable iff (!rst_n)
  !collisions_possible_i |-> cost_is_legacy);

// E3. A smaller minimum would be worse.
p_va_smaller_worse: assert property (@(posedge clk) disable iff (!rst_n)
  smaller_would_be_worse);

// E4. Cell waste is the cell less the frame.
p_va_cell: assert property (@(posedge clk) disable iff (!rst_n)
  ((cell_octets == 16'd256) && (min_frame_octets == 16'd64))
    |-> (cell_waste_ppm == 32'd750_000));

// E5. The machinery is reachable only in half duplex.
p_hd_reachable: assert property (@(posedge clk) disable iff (!rst_n)
  (machinery_reachable == !configured_full_duplex));

// E6. A collision on a full-duplex link contradicts the mode.
p_hd_contradiction: assert property (@(posedge clk) disable iff (!rst_n)
  (configured_full_duplex && collision_observed) |-> evidence_contradicts_mode);

// E7. And suggests a duplex mismatch.
p_hd_mismatch: assert property (@(posedge clk) disable iff (!rst_n)
  evidence_contradicts_mode |-> duplex_mismatch_suspected);

// E8. A large margin rules distance out.
p_hd_not_distance: assert property (@(posedge clk) disable iff (!rst_n)
  (late_collision_observed && (margin_x10_i >= 32'd20))
    |-> mode_disagreement_is_the_cause);

// E9. A recommendation is always produced.
p_hd_recommend: assert property (@(posedge clk) disable iff (!rst_n)
  (late_collision_observed || !machinery_reachable)
    |-> (recommended_check != 2'd0));

// F1. The impossible-collision counter is the mismatch detector.
p_tl_impossible: assert property (@(posedge clk) disable iff (!rst_n)
  (collision_observed_i && configured_full_duplex_i) |=>
    (c_impossible_collisions == $past(c_impossible_collisions) + 48'd1));

// F2. And on a correct full-duplex link it stays zero.
p_tl_zero: assert property (@(posedge clk) disable iff (!rst_n)
  should_always_be_zero && !mismatch_evidence_present
    |-> (c_impossible_collisions == 48'd0));

// F3. Minimum-size frames are a subset of frames.
p_tl_subset: assert property (@(posedge clk) disable iff (!rst_n)
  (c_min_size_frames <= c_frames));

// F4. Pad octets accumulate with padded frames.
p_tl_pad: assert property (@(posedge clk) disable iff (!rst_n)
  (frame_tx && frame_padded) |=>
    (c_pad_octets == $past(c_pad_octets) + 48'($past(pad_octets_i))));

// F5. Bound-but-uncovered properties are a violation.
p_cf_vacuous: assert property (@(posedge clk) disable iff (!rst_n)
  (configured_full_duplex_i && csma_cd_properties_bound &&
   (csma_cd_cover_hits == 32'd0)) |-> v_vacuous_properties);

// F6. A CSMA/CD claim on a full-duplex link is a violation.
p_cf_claim: assert property (@(posedge clk) disable iff (!rst_n)
  (configured_full_duplex_i && claims_csma_cd) |-> v_claims_csma_cd);

// F7. Blaming distance with a large margin is a violation.
p_cf_distance: assert property (@(posedge clk) disable iff (!rst_n)
  (late_collision_i && (margin_x10_i >= 32'd20)) |-> v_distance_blamed);

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

c_sd_10mbps:     cover property (@(posedge clk) rate_mbps == 32'd10);
c_sd_1gbps:      cover property (@(posedge clk) rate_mbps == 32'd1000);
c_sd_extended:   cover property (@(posedge clk) slot_bits == 16'd4096);
c_pp_shared:     cover property (@(posedge clk) mode == 2'(LINK_SHARED_HALF));
c_pp_p2p_half:   cover property (@(posedge clk) mode == 2'(LINK_P2P_HALF));
c_pp_vacuous:    cover property (@(posedge clk) bound_satisfied && !bound_constrains_anything);
c_mf_one_octet:  cover property (@(posedge clk) payload_octets == 16'd1);
c_mf_no_pad:     cover property (@(posedge clk) pad_octets == 32'd0);
c_pw_eight:      cover property (@(posedge clk) pipeline_width == 16'd8);
c_pw_five:       cover property (@(posedge clk) width_if_128 == 32'd5);
c_hd_collision:  cover property (@(posedge clk) collision_observed);
c_hd_impossible: cover property (@(posedge clk) evidence_contradicts_mode);
c_hd_late:       cover property (@(posedge clk) late_collision_observed);
c_cf_vacuous:    cover property (@(posedge clk) v_vacuous_properties);