Ethernet against Proprietary Fabrics

// ---------------------------------------------------------------------
// propfab_pkg -- constants for comparing a standard frame format
// against a fabric that has left the standard.
//
// 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 64-port 6.4 Tb/s switch = 5.62e8 BCE
// ---------------------------------------------------------------------
package propfab_pkg;

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

  // ---- the Ethernet frame's fixed octets -------------------------------
  localparam int unsigned OCT_PREAMBLE  = 8;    // Chapter 5.2
  localparam int unsigned OCT_IFG       = 12;   // Chapter 5.9
  localparam int unsigned OCT_ADDRESSES = 12;   // Chapter 5.3
  localparam int unsigned OCT_FCS       = 4;    // Chapter 5.8
  localparam int unsigned OCT_ETHERTYPE = 2;    // Chapter 5.5
  localparam int unsigned OCT_FIXED     = OCT_PREAMBLE + OCT_IFG
                                        + OCT_ADDRESSES + OCT_FCS
                                        + OCT_ETHERTYPE;   // 38

  // Which of them a proprietary fabric can actually delete. The
  // preamble and the FCS cannot go; the gap can only be shortened.
  localparam int unsigned OCT_DELETABLE = OCT_ADDRESSES + OCT_ETHERTYPE;

  // ---- Chapter 23.3's forwarding state, in BCE -------------------------
  // The three arrays a source-routed fabric does not need.
  localparam int unsigned ACL_TCAM_BCE_E4 = 2_100;   // 2.10e7 / 1e4
  localparam int unsigned L3_LPM_BCE_E4   = 1_680;   // 1.68e7
  localparam int unsigned MAC_TBL_BCE_E4  = 1_260;   // 1.26e7
  localparam int unsigned SWITCH_BCE_E4   = 56_200;  // 5.62e8

  // ---- the pipeline ----------------------------------------------------
  localparam int unsigned LOOKUP_STAGES   = 36;      // Chapter 23.3 Sec 2
  localparam int unsigned SR_STAGES       = 3;       // shift and demux
  localparam int unsigned CORE_MHZ        = 1_200;

  typedef enum logic [1:0] {
    ADDRESSING_NAME  = 2'd0,   // a 48-bit name, looked up
    ADDRESSING_ROUTE = 2'd1,   // a port index per hop
    ADDRESSING_ID    = 2'd2    // a short endpoint identifier
  } addressing_e;

  // ---- derived: framing ------------------------------------------------
  function automatic int unsigned wire_octets(int unsigned payload);
    // payload + 14 header + 4 FCS + 8 preamble + 12 gap
    return payload + OCT_FIXED;
  endfunction

  function automatic int unsigned tax_ppm(int unsigned payload);
    return (OCT_FIXED * 1_000_000) / wire_octets(payload);
  endfunction

  function automatic int unsigned deletable_ppm(int unsigned payload);
    return (OCT_DELETABLE * 1_000_000) / wire_octets(payload);
  endfunction

  // ---- derived: a source route ------------------------------------------
  function automatic int unsigned bits_per_hop(int unsigned radix);
    int unsigned b; int unsigned n;
    b = 0; n = radix - 1;
    while (n > 0) begin b = b + 1; n = n >> 1; end
    return b;
  endfunction

  function automatic int unsigned route_bits(int unsigned radix,
                                             int unsigned hops);
    return bits_per_hop(radix) * hops;
  endfunction

  // ---- derived: latency -------------------------------------------------
  function automatic int unsigned stage_ns_x100(int unsigned stages);
    return (stages * 100_000) / CORE_MHZ;
  endfunction

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

endpackage

// ---------------------------------------------------------------------
// framing_tax_model -- what a frame format costs at a given payload,
// and how much of that a fabric can actually escape.
//
// The output that matters is undeletable_ppm: the preamble and the
// check sequence survive any protocol change, so the saving is always
// smaller than the tax and usually by a factor of nearly three.
// ---------------------------------------------------------------------
module framing_tax_model
  import propfab_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,

  input  logic [15:0] payload_octets,
  input  logic [15:0] rate_gbps,
  input  logic  [1:0] addressing,         // addressing_e
  input  logic [15:0] route_octets,       // if a route replaces addresses

  output logic [31:0] wire_octets_o,
  output logic [31:0] tax_ppm_o,
  output logic [31:0] deletable_ppm_o,
  output logic [31:0] undeletable_ppm,
  output logic [31:0] actual_saving_ppm,
  output logic [31:0] packet_ns_x100,
  output logic [31:0] packets_per_s_k,
  output logic        preamble_is_deletable,
  output logic        fcs_is_deletable,
  output logic [31:0] c_frames_modelled
);
  always_comb begin
    wire_octets_o   = 32'(wire_octets(int'(payload_octets)));
    tax_ppm_o       = 32'(tax_ppm(int'(payload_octets)));
    deletable_ppm_o = 32'(deletable_ppm(int'(payload_octets)));
    undeletable_ppm = tax_ppm_o - deletable_ppm_o;

    // A route REPLACES the addresses rather than removing them, so the
    // saving is the difference, not the whole field.
    actual_saving_ppm =
      (addressing == 2'(ADDRESSING_NAME)) ? 32'd0
      : ((32'(OCT_DELETABLE) > 32'(route_octets))
         ? (((32'(OCT_DELETABLE) - 32'(route_octets)) * 1_000_000)
            / wire_octets_o)
         : 32'd0);

    // Chapter 8.3's other quantity: the frame RATE, which is what
    // decides the pipeline width rather than the efficiency.
    packet_ns_x100 = (rate_gbps == 0) ? 32'd0
                   : (wire_octets_o * 8 * 100) / 32'(rate_gbps);
    packets_per_s_k = (packet_ns_x100 == 0) ? 32'd0
                    : (100_000_000 / packet_ns_x100);

    // The two that survive any protocol change.
    preamble_is_deletable = 1'b0;
    fcs_is_deletable      = 1'b0;
  end

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

a 64-port switch needs 6 bits to name an egress port
5 hops x 6 bits = 30 bits of route

// ---------------------------------------------------------------------
// source_route_decoder -- the whole forwarding decision of a
// proprietary fabric, in three pipeline stages.
//
// Set this against Chapter 23.3's thirty-six. The module is short
// because that IS the comparison: the decision is a shift.
// ---------------------------------------------------------------------
module source_route_decoder
  import propfab_pkg::*;
#(
  parameter int unsigned RADIX      = 64,
  parameter int unsigned MAX_HOPS   = 5,
  parameter int unsigned ROUTE_BITS = 30
)(
  input  logic        clk,
  input  logic        rst_n,

  input  logic                  hdr_valid,
  input  logic [ROUTE_BITS-1:0] route_in,
  input  logic            [3:0] hops_remaining_in,

  output logic                  egress_valid,
  output logic            [5:0] egress_port,
  output logic [ROUTE_BITS-1:0] route_out,
  output logic            [3:0] hops_remaining_out,
  output logic                  route_exhausted,
  output logic                  lookup_needed,
  output logic [31:0] stages_used,
  output logic [31:0] latency_ns_x100,
  output logic [31:0] named_latency_ns_x100,
  output logic [31:0] latency_ratio_x10,
  output logic [31:0] c_hops_decoded,
  output logic [31:0] c_exhausted
);
  localparam int unsigned HOP_BITS = 6;   // bits_per_hop(64)

  // Stage 1: register the header. Stage 2: select. Stage 3: shift.
  logic [ROUTE_BITS-1:0] route_s1, route_s2;
  logic            [3:0] hops_s1,  hops_s2;
  logic                  valid_s1, valid_s2;

  always_comb begin
    stages_used           = 32'(SR_STAGES);
    latency_ns_x100       = 32'(stage_ns_x100(int'(SR_STAGES)));
    named_latency_ns_x100 = 32'(stage_ns_x100(int'(LOOKUP_STAGES)));
    latency_ratio_x10     = (latency_ns_x100 == 0) ? 32'd0
                          : (named_latency_ns_x100 * 32'd10)
                            / latency_ns_x100;

    // THE comparison, as a constant. A source-routed fabric performs
    // no lookup at all, so no table can miss and none needs to exist.
    lookup_needed = 1'b0;

    route_exhausted = valid_s2 && (hops_s2 == 4'd0);
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      route_s1 <= '0; route_s2 <= '0; hops_s1 <= '0; hops_s2 <= '0;
      valid_s1 <= 1'b0; valid_s2 <= 1'b0;
      egress_valid <= 1'b0; egress_port <= '0; route_out <= '0;
      hops_remaining_out <= '0;
      c_hops_decoded <= '0; c_exhausted <= '0;
    end else begin
      // Stage 1 -- capture.
      valid_s1 <= hdr_valid;
      route_s1 <= route_in;
      hops_s1  <= hops_remaining_in;

      // Stage 2 -- select this hop's port from the low bits.
      valid_s2 <= valid_s1;
      route_s2 <= route_s1;
      hops_s2  <= hops_s1;

      // Stage 3 -- emit and shift the route down by one hop.
      egress_valid       <= valid_s2 && (hops_s2 != 4'd0);
      egress_port        <= route_s2[HOP_BITS-1:0];
      route_out          <= route_s2 >> HOP_BITS;
      hops_remaining_out <= (hops_s2 == 4'd0) ? 4'd0 : (hops_s2 - 4'd1);

      if (valid_s2 && (hops_s2 != 4'd0))
        c_hops_decoded <= c_hops_decoded + 32'd1;
      if (valid_s2 && (hops_s2 == 4'd0))
        c_exhausted <= c_exhausted + 32'd1;
    end
  end
endmodule

// ---------------------------------------------------------------------
// fabric_area_model -- what a switch costs with and without the
// general forwarding mechanisms, in BCE.
//
// The output that matters is undeletable_share_pct, which stays above
// ninety whatever the protocol, because the packet buffer is sized by
// the traffic rather than by the frame format.
// ---------------------------------------------------------------------
module fabric_area_model
  import propfab_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,

  input  logic  [1:0] addressing,          // addressing_e
  input  logic [15:0] replacement_rules,   // a fabric still classifies
  input  logic [15:0] rule_width_bits,

  output logic [31:0] deleted_bce_e4,
  output logic [31:0] reintroduced_bce_e4,
  output logic [31:0] net_saving_bce_e4,
  output logic [15:0] net_saving_pct_x10,
  output logic [31:0] undeletable_bce_e4,
  output logic [15:0] undeletable_share_pct,
  output logic [31:0] saving_datapaths_milli,
  output logic        buffer_is_protocol_independent,
  output logic        serdes_is_shared,
  output logic [31:0] c_configs_modelled
);
  always_comb begin
    // The three arrays a route makes unnecessary.
    deleted_bce_e4 = (addressing == 2'(ADDRESSING_NAME))
                   ? 32'd0
                   : (32'(ACL_TCAM_BCE_E4) + 32'(L3_LPM_BCE_E4)
                      + 32'(MAC_TBL_BCE_E4));

    // And what a fabric still needs: a small classifier.
    reintroduced_bce_e4 = (32'(replacement_rules)
                           * 32'(rule_width_bits)) / 32'd10_000;

    net_saving_bce_e4 = (deleted_bce_e4 > reintroduced_bce_e4)
                      ? (deleted_bce_e4 - reintroduced_bce_e4) : 32'd0;

    net_saving_pct_x10 = 16'((net_saving_bce_e4 * 32'd1000)
                             / 32'(SWITCH_BCE_E4));

    undeletable_bce_e4    = 32'(SWITCH_BCE_E4) - net_saving_bce_e4;
    undeletable_share_pct = 16'((undeletable_bce_e4 * 32'd100)
                                / 32'(SWITCH_BCE_E4));

    saving_datapaths_milli = 32'(datapaths_milli(net_saving_bce_e4
                                                 * 32'd10_000));

    // The two facts that cap the saving, stated as constants because
    // they are true of every protocol rather than of this one.
    buffer_is_protocol_independent = 1'b1;
    serdes_is_shared               = 1'b1;
  end

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

// ---------------------------------------------------------------------
// ecosystem_cost_model -- what a fabric must supply for itself, counted
// in mechanisms rather than in area, because none of it is on the die.
//
// The output that matters is independent_implementations, which is
// one, and which is the input to every other conclusion in Section 8.
// ---------------------------------------------------------------------
module ecosystem_cost_model
  import propfab_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,

  input  logic        is_standard,
  input  logic [15:0] mechanisms_needed,     // discovery, time, etc.
  input  logic [15:0] mechanisms_supplied,   // by the standard
  input  logic [15:0] vendors,

  output logic [15:0] mechanisms_to_build,
  output logic [15:0] independent_implementations,
  output logic        spec_ambiguity_is_discoverable,
  output logic        conformance_has_an_oracle,
  output logic        capture_tooling_exists,
  output logic [15:0] second_source_count,
  output logic        single_vendor_risk,
  output logic [31:0] c_mechanisms_unsupplied
);
  always_comb begin
    mechanisms_to_build = is_standard
                        ? ((mechanisms_needed > mechanisms_supplied)
                           ? (mechanisms_needed - mechanisms_supplied)
                           : 16'd0)
                        : mechanisms_needed;

    independent_implementations = is_standard ? vendors : 16'd1;

    // THE consequence. A specification needs two independent readings
    // before anybody can discover that it has two readings.
    spec_ambiguity_is_discoverable = (independent_implementations >= 16'd2);

    // And a conformance check needs an oracle its own author did not
    // write. Section 20's rejected property is exactly this.
    conformance_has_an_oracle = (independent_implementations >= 16'd2);

    // Chapter 21.9's apparatus presumes a decoder somebody sells.
    capture_tooling_exists = is_standard;

    second_source_count = is_standard ? vendors : 16'd1;
    single_vendor_risk  = (second_source_count < 16'd2);
  end

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

// ---------------------------------------------------------------------
// undeletable_core -- what both fabrics must contain, priced so the
// differentiated fraction can be stated honestly.
//
// The outputs that matter are shared_share_pct and the two booleans
// that explain it: the buffer is sized by traffic and the SerDes by
// physics, and neither cares about the header.
// ---------------------------------------------------------------------
module undeletable_core
  import propfab_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,

  input  logic [31:0] buffer_bce_e4,
  input  logic [31:0] forwarding_bce_e4,
  input  logic [31:0] other_bce_e4,
  input  logic [15:0] serdes_lanes,
  input  logic        fabric_is_proprietary,

  output logic [31:0] total_bce_e4,
  output logic [31:0] shared_bce_e4,
  output logic [31:0] differentiated_bce_e4,
  output logic [15:0] shared_share_pct,
  output logic [15:0] differentiated_share_pct_x10,
  output logic        buffer_sized_by_traffic,
  output logic        serdes_sized_by_physics,
  output logic        serdes_is_standard_ip,
  output logic [15:0] shared_serdes_lanes,
  output logic [31:0] c_evaluations
);
  always_comb begin
    total_bce_e4 = buffer_bce_e4 + forwarding_bce_e4 + other_bce_e4;

    // A proprietary fabric deletes the forwarding state and keeps the
    // rest. A standard one keeps everything.
    shared_bce_e4 = fabric_is_proprietary
                  ? (buffer_bce_e4 + other_bce_e4)
                  : total_bce_e4;

    differentiated_bce_e4 = total_bce_e4 - shared_bce_e4;

    shared_share_pct = (total_bce_e4 == 0) ? 16'd100
                     : 16'((shared_bce_e4 * 32'd100) / total_bce_e4);

    differentiated_share_pct_x10 =
      (total_bce_e4 == 0) ? 16'd0
                          : 16'((differentiated_bce_e4 * 32'd1000)
                                / total_bce_e4);

    // The three facts that cap every proprietary fabric's advantage.
    buffer_sized_by_traffic = 1'b1;
    serdes_sized_by_physics = 1'b1;
    serdes_is_standard_ip   = 1'b1;

    // And the lane count is the same on both sides at the same rate.
    shared_serdes_lanes = serdes_lanes;
  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

// ---------------------------------------------------------------------
// second_source_model -- the consequences of independent_implementations
// being one, made into signals.
//
// There is no datapath here and that is deliberate: every risk this
// module reports is real, none of it is on the die, and a design
// review that only looks at silicon sees none of it.
// ---------------------------------------------------------------------
module second_source_model
  import propfab_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,

  input  logic [15:0] implementations,
  input  logic [15:0] spec_amendments_since_freeze,
  input  logic [15:0] amendment_budget,
  input  logic        independent_model_exists,
  input  logic        model_authors_saw_design,

  output logic        oracle_is_independent,
  output logic        conformance_is_meaningful,
  output logic        ambiguity_discoverable,
  output logic        spec_churn_exceeded,
  output logic        price_negotiable,
  output logic        supply_has_fallback,
  output logic        roadmap_is_coupled,
  output logic  [3:0] risks,
  output logic [31:0] c_amendments
);
  always_comb begin
    // An oracle is independent only if somebody wrote it from the
    // document WITHOUT seeing the design. Seeing the design converts
    // the model into a second description of the same artefact.
    oracle_is_independent = independent_model_exists
                         && !model_authors_saw_design;

    conformance_is_meaningful = oracle_is_independent
                             || (implementations >= 16'd2);

    ambiguity_discoverable = (implementations >= 16'd2);

    spec_churn_exceeded = (spec_amendments_since_freeze > amendment_budget);

    price_negotiable    = (implementations >= 16'd2);
    supply_has_fallback = (implementations >= 16'd2);
    roadmap_is_coupled  = (implementations < 16'd2);

    risks = { roadmap_is_coupled, spec_churn_exceeded,
              !conformance_is_meaningful, !ambiguity_discoverable };
  end

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

// ---------------------------------------------------------------------
// propfab_telemetry -- what a fabric with no external instrumentation
// must report about itself, and the one field that says whether the
// report can be trusted.
//
// Design rule: on a fabric with no second implementation, every
// counter is also a claim, so each one carries its provenance.
// ---------------------------------------------------------------------
module propfab_telemetry
  import propfab_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,
  input  logic        clear,

  input  logic        hop_decoded,
  input  logic        route_exhausted_i,
  input  logic        frame_rx,
  input  logic [15:0] frame_octets,
  input  logic        frame_dropped,
  input  logic        mirror_active,
  input  logic        capture_armed,
  input  logic        injector_used,
  input  logic        external_decoder_present,

  output logic [47:0] c_hops,
  output logic [47:0] c_route_errors,
  output logic [47:0] c_frames,
  output logic [47:0] c_octets,
  output logic [47:0] c_drops,
  output logic [47:0] c_mirror_frames,
  output logic [31:0] mean_frame_octets,
  output logic [31:0] framing_tax_ppm_measured,
  output logic        self_witnessed_only,
  output logic        capture_path_present
);
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n || clear) begin
      c_hops <= '0; c_route_errors <= '0; c_frames <= '0;
      c_octets <= '0; c_drops <= '0; c_mirror_frames <= '0;
    end else begin
      if (hop_decoded)       c_hops         <= c_hops + 48'd1;
      if (route_exhausted_i) c_route_errors <= c_route_errors + 48'd1;
      if (frame_rx) begin
        c_frames <= c_frames + 48'd1;
        c_octets <= c_octets + 48'(frame_octets);
      end
      if (frame_dropped)     c_drops         <= c_drops + 48'd1;
      if (mirror_active && frame_rx)
                             c_mirror_frames <= c_mirror_frames + 48'd1;
    end
  end

  always_comb begin
    mean_frame_octets = (c_frames == 0) ? 32'd0
                      : 32'(c_octets / c_frames);

    // The tax, measured on the traffic that actually ran, rather than
    // quoted at minimum frame size.
    framing_tax_ppm_measured =
      (mean_frame_octets == 0) ? 32'd0
                               : 32'(tax_ppm(int'(mean_frame_octets)));

    // THE field. Without an external decoder, every number above is a
    // claim the design makes about itself.
    self_witnessed_only = !external_decoder_present;

    capture_path_present = mirror_active || capture_armed || injector_used;
  end
endmodule

// ---------------------------------------------------------------------
// propfab_conformance -- the checks that survive Section 20's problem,
// because they follow from arithmetic rather than from a document.
//
// Every check here is chosen for one property: the specification
// cannot be amended to make it pass.
// ---------------------------------------------------------------------
module propfab_conformance
  import propfab_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,

  input  logic [47:0] octets_in,
  input  logic [47:0] octets_out,
  input  logic [47:0] octets_dropped,
  input  logic [47:0] octets_resident,
  input  logic        window_end,

  input  logic [15:0] route_bits_used,
  input  logic [15:0] radix,
  input  logic [15:0] max_hops,
  input  logic        hop_decoded_i,
  input  logic  [3:0] hops_remaining_i,
  input  logic        egress_valid_i,

  input  logic        claims_conformance,
  input  logic        oracle_independent_i,

  output logic        v_conservation,
  output logic        v_route_too_short,
  output logic        v_hop_after_exhaustion,
  output logic        v_conformance_unfounded,
  output logic  [3:0] violations,
  output logic        conformant
);
  always_comb begin
    // 1. Nothing is created or destroyed. Arithmetic, not a document.
    v_conservation = window_end
                  && (octets_in != (octets_out + octets_dropped
                                    + octets_resident));

    // 2. The route field must be able to name every hop. Arithmetic
    //    again: ceil(log2(radix)) x max_hops.
    v_route_too_short = (32'(route_bits_used)
                         < 32'(route_bits(int'(radix), int'(max_hops))));

    // 3. A packet whose route is exhausted must not be forwarded.
    v_hop_after_exhaustion = egress_valid_i && (hops_remaining_i == 4'd0);

    // 4. Section 20's class 114, as a check: a conformance claim needs
    //    an oracle its own authors did not write.
    v_conformance_unfounded = claims_conformance && !oracle_independent_i;

    violations = { v_conformance_unfounded, v_hop_after_exhaustion,
                   v_route_too_short, v_conservation };
    conformant = (violations == 4'b0000);
  end
endmodule

// A1. The wire slot is the payload plus thirty-eight fixed octets.
p_ft_wire_slot: assert property (@(posedge clk) disable iff (!rst_n)
  (wire_octets_o == 32'(payload_octets) + 32'(OCT_FIXED)));

// A2. The tax falls as the payload grows -- Chapter 8.3's hyperbola.
p_ft_monotone: assert property (@(posedge clk) disable iff (!rst_n)
  (payload_octets > $past(payload_octets)) |->
    (tax_ppm_o <= $past(tax_ppm_o)));

// A3. Only the addresses and the type are deletable.
p_ft_deletable_set: assert property (@(posedge clk) disable iff (!rst_n)
  (deletable_ppm_o == ((32'(OCT_DELETABLE) * 1_000_000) / wire_octets_o)));

// A4. The preamble survives any protocol change.
p_ft_preamble_stays: assert property (@(posedge clk) disable iff (!rst_n)
  (preamble_is_deletable == 1'b0));

// A5. And so does the check sequence.
p_ft_fcs_stays: assert property (@(posedge clk) disable iff (!rst_n)
  (fcs_is_deletable == 1'b0));

// A6. So the undeletable part is always the larger share.
p_ft_undeletable_larger: assert property (@(posedge clk) disable iff (!rst_n)
  (undeletable_ppm > deletable_ppm_o));

// A7. A route REPLACES rather than removes, so the saving is a
//     difference and never the whole field.
p_ft_route_replaces: assert property (@(posedge clk) disable iff (!rst_n)
  ((addressing != 2'(ADDRESSING_NAME)) && (route_octets >= 16'(OCT_DELETABLE)))
    |-> (actual_saving_ppm == 32'd0));

// A8. A named-addressing fabric saves nothing by definition.
p_ft_named_saves_nothing: assert property (@(posedge clk) disable iff (!rst_n)
  (addressing == 2'(ADDRESSING_NAME)) |-> (actual_saving_ppm == 32'd0));

// A9. The packet rate is the wire slot divided into the line rate.
p_ft_packet_rate: assert property (@(posedge clk) disable iff (!rst_n)
  (rate_gbps != 0) |->
    (packet_ns_x100 == (wire_octets_o * 8 * 100) / 32'(rate_gbps)));

// B1. No lookup is performed, ever.
p_sr_no_lookup: assert property (@(posedge clk) disable iff (!rst_n)
  (lookup_needed == 1'b0));

// B2. The decode is three stages.
p_sr_three_stages: assert property (@(posedge clk) disable iff (!rst_n)
  (stages_used == 32'(SR_STAGES)));

// B3. And twelve times faster than a lookup pipeline.
p_sr_ratio: assert property (@(posedge clk) disable iff (!rst_n)
  (latency_ratio_x10 == 32'd120));

// B4. The egress port is the route's low bits.
p_sr_port_is_low_bits: assert property (@(posedge clk) disable iff (!rst_n)
  egress_valid |-> (egress_port == $past(route_s2[5:0])));

// B5. The route shifts down by exactly one hop.
p_sr_shift: assert property (@(posedge clk) disable iff (!rst_n)
  egress_valid |-> (route_out == ($past(route_s2) >> 6)));

// B6. Hops remaining decrements by one and never wraps.
p_sr_hops_decrement: assert property (@(posedge clk) disable iff (!rst_n)
  (egress_valid && ($past(hops_s2) != 4'd0)) |->
    (hops_remaining_out == $past(hops_s2) - 4'd1));

// B7. An exhausted route is not forwarded.
p_sr_no_forward_exhausted: assert property (@(posedge clk) disable iff (!rst_n)
  route_exhausted |-> !egress_valid);

// B8. And it is counted.
p_sr_exhausted_counted: assert property (@(posedge clk) disable iff (!rst_n)
  route_exhausted |=> (c_exhausted == $past(c_exhausted) + 32'd1));

// B9. The route field is wide enough for the topology. An elaboration
//     check, written as a property so it appears in the report.
p_sr_route_wide_enough: assert property (@(posedge clk) disable iff (!rst_n)
  (ROUTE_BITS >= route_bits(RADIX, MAX_HOPS)));

// C1. A named-addressing fabric deletes nothing.
p_ar_named_deletes_nothing: assert property (@(posedge clk) disable iff (!rst_n)
  (addressing == 2'(ADDRESSING_NAME)) |-> (deleted_bce_e4 == 32'd0));

// C2. A routed one deletes exactly the three arrays.
p_ar_routed_deletes_three: assert property (@(posedge clk) disable iff (!rst_n)
  (addressing != 2'(ADDRESSING_NAME)) |->
    (deleted_bce_e4 == (32'(ACL_TCAM_BCE_E4) + 32'(L3_LPM_BCE_E4)
                        + 32'(MAC_TBL_BCE_E4))));

// C3. The reintroduced classifier is charged back.
p_ar_reintroduction_charged: assert property (@(posedge clk) disable iff (!rst_n)
  (replacement_rules != 16'd0) |-> (reintroduced_bce_e4 != 32'd0));

// C4. The net saving never exceeds the gross.
p_ar_net_bounded: assert property (@(posedge clk) disable iff (!rst_n)
  (net_saving_bce_e4 <= deleted_bce_e4));

// C5. And it is a single-digit percentage of the switch.
p_ar_single_digit: assert property (@(posedge clk) disable iff (!rst_n)
  (net_saving_pct_x10 <= 16'd100));

// C6. The undeletable share is above ninety, always.
p_ar_undeletable_dominates: assert property (@(posedge clk) disable iff (!rst_n)
  (undeletable_share_pct >= 16'd90));

// C7. The buffer is sized by traffic rather than by the header.
p_ar_buffer_independent: assert property (@(posedge clk) disable iff (!rst_n)
  (buffer_sized_by_traffic == 1'b1));

// C8. And the SerDes is the same on both sides at the same rate.
p_ar_serdes_shared: assert property (@(posedge clk) disable iff (!rst_n)
  (serdes_is_shared && serdes_is_standard_ip &&
   (shared_serdes_lanes == serdes_lanes)));

// D1. A proprietary fabric has one implementation by definition.
p_ec_one_impl: assert property (@(posedge clk) disable iff (!rst_n)
  !is_standard |-> (independent_implementations == 16'd1));

// D2. Ambiguity needs two readings to be discoverable.
p_ec_ambiguity: assert property (@(posedge clk) disable iff (!rst_n)
  (independent_implementations < 16'd2) |-> !ambiguity_discoverable);

// D3. And so does a conformance oracle.
p_ec_oracle: assert property (@(posedge clk) disable iff (!rst_n)
  (independent_implementations < 16'd2) |-> !conformance_has_an_oracle);

// D4. Capture tooling exists only for a standard.
p_ec_capture: assert property (@(posedge clk) disable iff (!rst_n)
  (capture_tooling_exists == is_standard));

// D5. A single implementation couples the roadmap.
p_ec_roadmap: assert property (@(posedge clk) disable iff (!rst_n)
  (second_source_count < 16'd2) |-> single_vendor_risk);

// D6. Every mechanism the standard does not supply must be built.
p_ec_build_the_rest: assert property (@(posedge clk) disable iff (!rst_n)
  is_standard |-> (mechanisms_to_build ==
    ((mechanisms_needed > mechanisms_supplied)
     ? (mechanisms_needed - mechanisms_supplied) : 16'd0)));

// D7. A model whose authors saw the design is not an oracle.
p_ec_model_blind: assert property (@(posedge clk) disable iff (!rst_n)
  model_authors_saw_design |-> !oracle_is_independent);

// D8. Spec churn past its budget is a reportable condition.
p_ec_churn: assert property (@(posedge clk) disable iff (!rst_n)
  (spec_amendments_since_freeze > amendment_budget) |-> spec_churn_exceeded);

// E1. The measured tax follows the measured mean frame.
p_tl_measured_tax: assert property (@(posedge clk) disable iff (!rst_n)
  (mean_frame_octets != 32'd0) |->
    (framing_tax_ppm_measured == 32'(tax_ppm(int'(mean_frame_octets)))));

// E2. Without an external decoder, the fabric witnesses only itself.
p_tl_self_witness: assert property (@(posedge clk) disable iff (!rst_n)
  (self_witnessed_only == !external_decoder_present));

// E3. A capture path is present if any of the three mechanisms is.
p_tl_capture_path: assert property (@(posedge clk) disable iff (!rst_n)
  (capture_path_present == (mirror_active || capture_armed || injector_used)));

// E4. Octets accumulate with frames.
p_tl_octets_track: assert property (@(posedge clk) disable iff (!rst_n)
  frame_rx |=> (c_octets == $past(c_octets) + 48'($past(frame_octets))));

// E5. Mirrored frames never exceed received frames.
p_tl_mirror_bounded: assert property (@(posedge clk) disable iff (!rst_n)
  (c_mirror_frames <= c_frames));

// E6. A route error is counted exactly once.
p_tl_route_error_once: assert property (@(posedge clk) disable iff (!rst_n)
  route_exhausted_i |=> (c_route_errors == $past(c_route_errors) + 48'd1));

// E7. Clearing zeroes every counter.
p_tl_clear: assert property (@(posedge clk) disable iff (!rst_n)
  clear |=> ((c_frames == 48'd0) && (c_octets == 48'd0) &&
             (c_drops == 48'd0)));

// E8. The mean is bounded by the maximum frame.
p_tl_mean_bounded: assert property (@(posedge clk) disable iff (!rst_n)
  (c_frames != 0) |-> (mean_frame_octets <= 32'd9018));

// F1. Conservation. Arithmetic, not a document.
p_cf_conservation: assert property (@(posedge clk) disable iff (!rst_n)
  window_end |-> (octets_in == octets_out + octets_dropped
                              + octets_resident));

// F2. The route field must name every hop.
p_cf_route_width: assert property (@(posedge clk) disable iff (!rst_n)
  !v_route_too_short);

// F3. An exhausted route must not be forwarded.
p_cf_no_forward: assert property (@(posedge clk) disable iff (!rst_n)
  !v_hop_after_exhaustion);

// F4. A conformance claim needs an oracle its authors did not write.
p_cf_oracle_required: assert property (@(posedge clk) disable iff (!rst_n)
  claims_conformance |-> oracle_independent_i);

// F5. The violation vector is the monitor's own disjunction.
p_cf_vector: assert property (@(posedge clk) disable iff (!rst_n)
  conformant |-> (violations == 4'b0000));

// F6. Conservation is checked only at a consistent sample point --
//     Chapter 19.7 Section 19's class 87 as a guard rather than a trap.
p_cf_sample_consistent: assert property (@(posedge clk) disable iff (!rst_n)
  window_end |-> $stable(snapshot_taken));

// F7. The reference model's version is pinned at sign-off.
p_cf_version_pinned: assert property (@(posedge clk) disable iff (!rst_n)
  signoff_requested |-> (reference_version == SIGNOFF_SPEC_VERSION));

// F8. And an independently written model agrees.
p_cf_independent_agrees: assert property (@(posedge clk) disable iff (!rst_n)
  transaction_observed |-> (observed == independent_model_predicts));

// F9. Amendments after freeze are budgeted.
p_cf_amendment_budget: assert property (@(posedge clk) disable iff (!rst_n)
  signoff_requested |-> (spec_amendments_since_freeze <= AMENDMENT_BUDGET));

c_ft_min_frame:    cover property (@(posedge clk) payload_octets <= 16'd46);
c_ft_jumbo:        cover property (@(posedge clk) payload_octets >= 16'd9000);
c_ft_route_bigger: cover property (@(posedge clk) route_octets >= 16'd14);
c_sr_exhausted:    cover property (@(posedge clk) route_exhausted);
c_sr_max_hops:     cover property (@(posedge clk) hops_remaining_in == 4'd5);
c_ar_reintroduced: cover property (@(posedge clk) reintroduced_bce_e4 != 32'd0);
c_ar_small_table:  cover property (@(posedge clk) net_saving_pct_x10 <= 16'd20);
c_ec_no_oracle:    cover property (@(posedge clk) !oracle_is_independent);
c_ec_churn:        cover property (@(posedge clk) spec_churn_exceeded);
c_ec_blind_model:  cover property (@(posedge clk) !model_authors_saw_design);
c_tl_self_only:    cover property (@(posedge clk) self_witnessed_only);
c_tl_no_capture:   cover property (@(posedge clk) !capture_path_present);
c_cf_conservation: cover property (@(posedge clk) v_conservation);
c_cf_unfounded:    cover property (@(posedge clk) v_conformance_unfounded);