Ethernet against InfiniBand

credit loop = 2 x propagation + credit turnaround + one maximum frame

// ---------------------------------------------------------------------
// ibcmp_pkg -- the constants for a lossless-link comparison, with every
// derived figure computed rather than written as a literal.
//
// 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 ibcmp_pkg;

  localparam int unsigned DATAPATH_BCE   = 283_320;
  localparam int unsigned BCE_PER_FLOP   = 20;
  localparam int unsigned SWITCH_BCE_E5  = 5_620;   // 5.62e8 / 1e5
  localparam int unsigned SWITCH_PORTS   = 64;
  localparam int unsigned SWITCH_BUF_MB  = 64;

  // Chapter 8.2 Section 3's velocity figures, in hundredths of a
  // nanosecond per metre, so integer arithmetic keeps the precision.
  localparam int unsigned NS_PER_M_CU_X100 = 505;   // 5.05 ns/m
  localparam int unsigned NS_PER_M_FI_X100 = 490;   // 4.90 ns/m

  // The credit turnaround: detect, build, transmit, consume. Both
  // implementations contribute and neither publishes it.
  localparam int unsigned CREDIT_TURNAROUND_NS = 300;

  // The frame already committed when the credit arrived.
  localparam int unsigned MAX_FRAME_OCTETS = 9_000;

  typedef enum logic [1:0] {
    MEDIA_COPPER = 2'd0,
    MEDIA_FIBRE  = 2'd1
  } media_e;

  // ---- the credit loop -------------------------------------------------
  function automatic int unsigned prop_ns_x100(int unsigned metres,
                                               media_e m);
    return metres * ((m == MEDIA_COPPER) ? NS_PER_M_CU_X100
                                         : NS_PER_M_FI_X100);
  endfunction

  function automatic int unsigned frame_ns(int unsigned gbps);
    // octets x 8 bits / Gb/s gives nanoseconds directly.
    return (MAX_FRAME_OCTETS * 8) / gbps;
  endfunction

  function automatic int unsigned credit_loop_ns(int unsigned metres,
                                                 media_e m,
                                                 int unsigned gbps);
    return ((2 * prop_ns_x100(metres, m)) / 100)
         + CREDIT_TURNAROUND_NS
         + frame_ns(gbps);
  endfunction

  // ---- the reservation -------------------------------------------------
  // rate x time: Gb/s x ns / 8 gives bytes.
  function automatic int unsigned reserved_bytes(int unsigned metres,
                                                 media_e m,
                                                 int unsigned gbps);
    return (gbps * credit_loop_ns(metres, m, gbps)) / 8;
  endfunction

  function automatic int unsigned reserved_bce(int unsigned metres,
                                               media_e m,
                                               int unsigned gbps,
                                               int unsigned lanes);
    return reserved_bytes(metres, m, gbps) * 8 * lanes;
  endfunction

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

  // Share of Chapter 23.3's switch, in hundredths of a per cent, so a
  // fraction below one per cent is still a nonzero integer.
  function automatic int unsigned switch_share_x100(int unsigned bce_e2);
    // bce_e2 is the figure divided by 100, to keep the product in range.
    return (bce_e2 * 10_000) / (SWITCH_BCE_E5 * 1_000);
  endfunction

endpackage

// ---------------------------------------------------------------------
// credit_loop_model -- what a lossless link must reserve, derived from
// the medium rather than configured.
//
// The output that matters is reservation_is_a_floor, which is always
// high: a buffer below the loop does not risk overflow, it guarantees
// a stall, and the two failures look nothing alike.
// ---------------------------------------------------------------------
module credit_loop_model
  import ibcmp_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,

  input  logic [15:0] metres,
  input  logic  [1:0] media,            // media_e
  input  logic [15:0] rate_gbps,
  input  logic [31:0] buffer_bytes,     // what the design implements

  output logic [31:0] loop_ns,
  output logic [31:0] prop_share_pct,
  output logic [31:0] reserved_bytes_o,
  output logic [31:0] reserved_bce_o,
  output logic        reservation_is_a_floor,
  output logic        buffer_insufficient,
  output logic [15:0] achievable_gbps,
  output logic [31:0] ethernet_reservation_bce,
  output logic [31:0] c_stall_events
);
  always_comb begin
    loop_ns          = 32'(credit_loop_ns(int'(metres), media_e'(media),
                                          int'(rate_gbps)));
    reserved_bytes_o = 32'(reserved_bytes(int'(metres), media_e'(media),
                                          int'(rate_gbps)));
    reserved_bce_o   = reserved_bytes_o * 32'd8;

    // How much of the loop is physics. Above 2 km it is essentially all
    // of it, which is why no implementation choice helps.
    prop_share_pct = (loop_ns == 0) ? 32'd0
                   : ((2 * 32'(prop_ns_x100(int'(metres), media_e'(media))))
                      / 100) * 32'd100 / loop_ns;

    // THE structural point of the chapter.
    reservation_is_a_floor = 1'b1;
    buffer_insufficient    = (buffer_bytes < reserved_bytes_o);

    // Chapter 21.8 Section 5's ceiling: if the buffer is short, the
    // rate is the buffer divided by the loop.
    achievable_gbps = (loop_ns == 0) ? rate_gbps
                    : (buffer_insufficient
                       ? 16'((buffer_bytes * 32'd8) / loop_ns)
                       : rate_gbps);

    // An Ethernet link reserves nothing. It drops instead.
    ethernet_reservation_bce = 32'd0;
  end

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

// ---------------------------------------------------------------------
// reservation_model -- the fabric-scale figure, and the comparison
// against a switch that exists.
//
// The output that matters is over_commitment_allowed, which is 0.
// Every other buffer in this track is affordable because it is shared
// against a statistical argument; this one is not.
// ---------------------------------------------------------------------
module reservation_model
  import ibcmp_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,

  input  logic [15:0] ports,
  input  logic [31:0] per_link_bce,
  input  logic [31:0] switch_buffer_mb,

  output logic [31:0] fabric_reservation_e2,   // BCE / 100
  output logic [31:0] reservation_dp_milli,
  output logic [15:0] share_of_switch_x100,
  output logic        exceeds_switch,
  output logic [31:0] ports_a_buffer_serves,
  output logic        over_commitment_allowed,
  output logic [31:0] lossy_equivalent_bce,
  output logic [31:0] c_infeasible_configs
);
  always_comb begin
    fabric_reservation_e2 = (per_link_bce / 32'd100) * 32'(ports);

    reservation_dp_milli  = 32'(datapaths_milli(
                                 (fabric_reservation_e2 * 32'd100)));

    share_of_switch_x100  = 16'(switch_share_x100(fabric_reservation_e2));
    exceeds_switch        = (share_of_switch_x100 >= 16'd10_000);

    // How many ports the switch's existing buffer could reserve for.
    ports_a_buffer_serves = (per_link_bce == 0) ? 32'd0
                          : ((switch_buffer_mb * 1024 * 1024 * 8)
                             / per_link_bce);

    // THE structural difference from every other buffer in this track.
    over_commitment_allowed = 1'b0;

    // A lossy fabric reserves nothing and drops instead.
    lossy_equivalent_bce = 32'd0;
  end

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

// ---------------------------------------------------------------------
// vl_partition -- independent credit pools, and the reservation each
// one obliges.
//
// The output that matters is borrow_permitted, which is 0. A lane with
// spare promised space may not lend it to a starving neighbour, and
// that single fact is why the reservation is a sum rather than a max.
// ---------------------------------------------------------------------
module vl_partition
  import ibcmp_pkg::*;
#(
  parameter int unsigned LANES = 8
)(
  input  logic        clk,
  input  logic        rst_n,

  input  logic [31:0] per_lane_reserved_bytes,
  input  logic [31:0] total_buffer_bytes,
  input  logic  [3:0] lane_sel,
  input  logic        packet_arrives,
  input  logic        packet_drains,
  input  logic [15:0] packet_bytes,

  output logic [31:0] reservation_total_bytes,
  output logic [31:0] reservation_total_bce,
  output logic        fits_in_buffer,
  output logic [15:0] buffer_used_pct,
  output logic        borrow_permitted,
  output logic        lane_blocked,
  output logic        head_of_line_across_lanes,
  output logic [31:0] occupancy [LANES],
  output logic [31:0] c_lane_blocks,
  output logic [31:0] c_wasted_reserved_bytes
);
  always_comb begin
    reservation_total_bytes = per_lane_reserved_bytes * 32'(LANES);
    reservation_total_bce   = reservation_total_bytes * 32'd8;

    fits_in_buffer  = (reservation_total_bytes <= total_buffer_bytes);
    buffer_used_pct = (total_buffer_bytes == 0) ? 16'd0
                    : 16'((reservation_total_bytes * 32'd100)
                          / total_buffer_bytes);

    // THE reason the reservation is a sum. Chapter 23.3 Section 9's
    // dynamic threshold lends idle space between ports; a credit
    // promise cannot be lent, because it was already promised.
    borrow_permitted = 1'b0;

    lane_blocked = (occupancy[lane_sel] + 32'(packet_bytes))
                 > per_lane_reserved_bytes;

    // And the reason lanes exist: a block on one lane does not stop
    // the others, which a single pool could not offer.
    head_of_line_across_lanes = 1'b0;
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (int i = 0; i < LANES; i++) occupancy[i] <= '0;
      c_lane_blocks <= '0; c_wasted_reserved_bytes <= '0;
    end else begin
      if (packet_arrives && !lane_blocked)
        occupancy[lane_sel] <= occupancy[lane_sel] + 32'(packet_bytes);
      if (packet_drains && (occupancy[lane_sel] >= 32'(packet_bytes)))
        occupancy[lane_sel] <= occupancy[lane_sel] - 32'(packet_bytes);
      if (packet_arrives && lane_blocked)
        c_lane_blocks <= c_lane_blocks + 32'd1;

      // The quantity nobody reports: space that was promised, is empty,
      // and cannot be used by the lane that needs it.
      c_wasted_reserved_bytes <= '0;
      for (int i = 0; i < LANES; i++)
        c_wasted_reserved_bytes <= c_wasted_reserved_bytes
                                 + (per_lane_reserved_bytes - occupancy[i]);
    end
  end
endmodule

// ---------------------------------------------------------------------
// congestion_tree -- how far a stall reaches and how long it takes to
// get there and back.
//
// Chapter 14.3 Section 9 measured a blast radius as a bitmap of
// affected pairs. This does the same for a fabric where the spread is
// certain rather than probable, and adds the two things that changes:
// a growth RATE, and a drain time.
// ---------------------------------------------------------------------
module congestion_tree
  import ibcmp_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,
  input  logic        tick_100ns,

  input  logic [15:0] radix,             // ports per switch
  input  logic [15:0] stages,
  input  logic [31:0] credit_loop_ns_i,
  input  logic        congestion_start,
  input  logic        congestion_clear,

  output logic [15:0] hops_reached,
  output logic [31:0] pairs_affected,
  output logic [31:0] full_stall_ns,
  output logic [31:0] drain_ns,
  output logic        tree_is_deterministic,
  output logic        fully_stalled,
  output logic [31:0] c_tree_events,
  output logic [31:0] c_stall_ns_total
);
  logic [31:0] elapsed_ns;
  logic        active;

  always_comb begin
    // Chapter 14.3 Section 8's counts: one switch's ingresses, then
    // their upstreams, then theirs.
    pairs_affected = (hops_reached == 16'd0) ? 32'(radix) - 32'd1
                   : ((hops_reached == 16'd1)
                      ? (32'(radix) - 32'd1) * (32'(radix) - 32'd1)
                      : (32'(radix) - 32'd1) * (32'(radix) - 32'd1)
                        * (32'(radix) - 32'd1));

    full_stall_ns = credit_loop_ns_i * 32'(stages);

    // The tree unwinds the same way it grew.
    drain_ns = full_stall_ns;

    // THE difference from Chapter 14.3. There, backpressure MIGHT
    // spread. Here the upstream is REQUIRED to stop.
    tree_is_deterministic = 1'b1;

    fully_stalled = active && (elapsed_ns >= full_stall_ns);
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      elapsed_ns <= '0; hops_reached <= '0; active <= 1'b0;
      c_tree_events <= '0; c_stall_ns_total <= '0;
    end else begin
      if (congestion_start && !active) begin
        active <= 1'b1; elapsed_ns <= '0; hops_reached <= '0;
        c_tree_events <= c_tree_events + 32'd1;
      end
      if (congestion_clear) begin
        active <= 1'b0;
      end
      if (active && tick_100ns) begin
        elapsed_ns       <= elapsed_ns + 32'd100;
        c_stall_ns_total <= c_stall_ns_total + 32'd100;
        if ((elapsed_ns + 32'd100) >= (credit_loop_ns_i
                                       * (32'(hops_reached) + 32'd1))
            && (hops_reached < stages))
          hops_reached <= hops_reached + 16'd1;
      end
    end
  end
endmodule

// ---------------------------------------------------------------------
// roce_window -- what a drop costs a transport that assumed it would
// not happen, and what the repair costs.
//
// The output that matters is link_losslessness_is_configured, which is
// an INPUT masquerading as a property: the transport cannot determine
// it and behaves as though it were true.
// ---------------------------------------------------------------------
module roce_window
  import ibcmp_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,

  input  logic [15:0] rate_gbps,
  input  logic [15:0] rtt_ns,
  input  logic [15:0] mtu_octets,
  input  logic        selective_repeat,
  input  logic [15:0] queue_pairs,
  input  logic        pfc_configured_everywhere,   // nobody can verify this

  input  logic        packet_lost,

  output logic [31:0] window_bytes,
  output logic [15:0] window_packets,
  output logic [31:0] retransmit_bytes,
  output logic [15:0] amplification_x10,
  output logic [31:0] bitmap_bits,
  output logic [31:0] bitmap_bce,
  output logic        link_losslessness_is_configured,
  output logic        transport_assumes_lossless,
  output logic [31:0] c_retransmit_bytes,
  output logic [31:0] c_losses
);
  always_comb begin
    window_bytes   = (32'(rate_gbps) * 32'(rtt_ns)) / 32'd8;
    window_packets = (mtu_octets == 0) ? 16'd0
                   : 16'(window_bytes / 32'(mtu_octets));

    // Go-back-N discards the whole window; selective repeat does not.
    retransmit_bytes = selective_repeat ? 32'(mtu_octets) : window_bytes;

    amplification_x10 = (mtu_octets == 0) ? 16'd0
                      : 16'((retransmit_bytes * 32'd10) / 32'(mtu_octets));

    // One bit per packet in the window, per queue pair.
    bitmap_bits = selective_repeat
                ? ((32'(window_packets) + 32'd1) * 32'(queue_pairs))
                : 32'd0;
    bitmap_bce  = bitmap_bits;     // an array: 1 BCE per bit

    // THE honest signal. It is wired from configuration because no
    // measurement in the transport can establish it.
    link_losslessness_is_configured = pfc_configured_everywhere;

    // And this is always true, whatever the link actually does.
    transport_assumes_lossless = 1'b1;
  end

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

// ---------------------------------------------------------------------
// deadlock_detector -- the mechanism that makes a lossless fabric
// survivable, and the admission that it is not lossless.
//
// The output that matters is is_still_lossless, which goes LOW the
// first time the detector fires. A fabric that has never fired it is
// lossless; one that has is a fabric with a long timeout.
// ---------------------------------------------------------------------
module deadlock_detector
  import ibcmp_pkg::*;
#(
  parameter int unsigned LANES = 8
)(
  input  logic        clk,
  input  logic        rst_n,
  input  logic        tick_us,

  input  logic [31:0] credit_loop_ns_i,
  input  logic [15:0] timeout_multiplier,   // x the credit loop
  input  logic  [7:0] lane_has_work,        // one bit per lane
  input  logic  [7:0] lane_has_credit,

  output logic [31:0] timeout_us,
  output logic [15:0] loops_before_discard,
  output logic  [7:0] lane_starved,
  output logic        discard_required,
  output logic  [2:0] discard_lane,
  output logic        is_still_lossless,
  output logic [31:0] c_discards,
  output logic [31:0] c_starved_us
);
  logic [31:0] starved_us [LANES];
  logic        fired;

  always_comb begin
    timeout_us = ((credit_loop_ns_i * 32'(timeout_multiplier)) + 32'd999)
               / 32'd1000;

    loops_before_discard = timeout_multiplier;

    // A lane with work and no credit is starved. It may be a normal
    // congestion stall or the head of a cycle, and nothing here can
    // tell the difference -- which is why the remedy is a timeout.
    lane_starved = lane_has_work & ~lane_has_credit;

    // THE admission.
    is_still_lossless = !fired;
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (int i = 0; i < LANES; i++) starved_us[i] <= '0;
      discard_required <= 1'b0; discard_lane <= '0;
      fired <= 1'b0; c_discards <= '0; c_starved_us <= '0;
    end else begin
      discard_required <= 1'b0;
      if (tick_us) begin
        for (int i = 0; i < LANES; i++) begin
          if (lane_starved[i]) begin
            starved_us[i]  <= starved_us[i] + 32'd1;
            c_starved_us   <= c_starved_us + 32'd1;
            if ((starved_us[i] + 32'd1) >= timeout_us) begin
              discard_required <= 1'b1;
              discard_lane     <= 3'(i);
              starved_us[i]    <= '0;
              fired            <= 1'b1;
              c_discards       <= c_discards + 32'd1;
            end
          end else begin
            starved_us[i] <= '0;
          end
        end
      end
    end
  end
endmodule

// ---------------------------------------------------------------------
// ib_cmp_telemetry -- the counters a lossless fabric needs and does
// not usually have.
//
// The design rule: on a fabric that does not drop, the loss-equivalent
// quantity is TIME, so every counter here is a duration or a rate
// rather than an event count.
// ---------------------------------------------------------------------
module ib_cmp_telemetry
  import ibcmp_pkg::*;
#(
  parameter int unsigned LANES = 8
)(
  input  logic        clk,
  input  logic        rst_n,
  input  logic        clear,
  input  logic        tick_us,

  input  logic  [7:0] lane_starved_i,
  input  logic        credit_returned,
  input  logic        packet_sent,
  input  logic        discard_fired,
  input  logic        tree_active,
  input  logic [31:0] reserved_bytes_i,
  input  logic [31:0] occupied_bytes_i,

  output logic [47:0] c_starved_us_total,
  output logic [47:0] c_lane_starved_us [LANES],
  output logic [47:0] c_credits_returned,
  output logic [47:0] c_packets_sent,
  output logic [47:0] c_tree_us,
  output logic [47:0] c_discards_o,
  output logic [31:0] elapsed_us,
  output logic [15:0] stalled_pct,
  output logic [15:0] reservation_idle_pct,
  output logic        drop_counter_is_meaningful
);
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n || clear) begin
      c_starved_us_total <= '0; c_credits_returned <= '0;
      c_packets_sent <= '0; c_tree_us <= '0; c_discards_o <= '0;
      elapsed_us <= '0;
      for (int i = 0; i < LANES; i++) c_lane_starved_us[i] <= '0;
    end else begin
      if (credit_returned) c_credits_returned <= c_credits_returned + 48'd1;
      if (packet_sent)     c_packets_sent     <= c_packets_sent + 48'd1;
      if (discard_fired)   c_discards_o       <= c_discards_o + 48'd1;
      if (tick_us) begin
        elapsed_us <= elapsed_us + 32'd1;
        if (tree_active) c_tree_us <= c_tree_us + 48'd1;
        for (int i = 0; i < LANES; i++) begin
          if (lane_starved_i[i]) begin
            c_lane_starved_us[i] <= c_lane_starved_us[i] + 48'd1;
            c_starved_us_total   <= c_starved_us_total + 48'd1;
          end
        end
      end
    end
  end

  always_comb begin
    // THE number. On a lossless fabric this is the loss rate.
    stalled_pct = (elapsed_us == 0) ? 16'd0
                : 16'((c_tree_us * 48'd100) / 48'(elapsed_us));

    // Section 7's wasted promise, as a percentage.
    reservation_idle_pct = (reserved_bytes_i == 0) ? 16'd0
                         : 16'(((reserved_bytes_i - occupied_bytes_i)
                                * 32'd100) / reserved_bytes_i);

    // And the honest label on the counter everybody reads.
    drop_counter_is_meaningful = 1'b0;
  end
endmodule

// ---------------------------------------------------------------------
// ib_cmp_conformance -- the checks that hold a lossless claim to what
// it actually promises.
//
// Every check here exists because "lossless" is a narrower claim than
// the word suggests, and the narrowing is what the monitor enforces.
// ---------------------------------------------------------------------
module ib_cmp_conformance
  import ibcmp_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,

  input  logic [31:0] advertised_credit_bytes,
  input  logic [31:0] backing_buffer_bytes,
  input  logic [31:0] reserved_bytes_i,
  input  logic [31:0] required_bytes_i,
  input  logic        lane_borrowed,
  input  logic        discard_fired,
  input  logic        claims_lossless,
  input  logic [31:0] timeout_us_i,
  input  logic [31:0] credit_loop_ns_i,
  input  logic        packet_sent,
  input  logic        credits_available_i,

  output logic        v_overadvertised,
  output logic        v_under_reserved,
  output logic        v_lane_borrow,
  output logic        v_lossless_claim_stale,
  output logic        v_timeout_too_short,
  output logic        v_sent_without_credit,
  output logic  [5:0] violations,
  output logic        conformant
);
  always_comb begin
    // 1. Prohibition 1 -- the promise must be backed.
    v_overadvertised = (advertised_credit_bytes > backing_buffer_bytes);

    // 2. Section 2 -- the reservation is a floor, not a target.
    v_under_reserved = (reserved_bytes_i < required_bytes_i);

    // 3. Prohibition 2 -- a lane may not draw on a neighbour's promise.
    v_lane_borrow = lane_borrowed;

    // 4. Section 13 -- a fabric that has discarded is not lossless,
    //    and must stop saying it is.
    v_lossless_claim_stale = claims_lossless && discard_fired;

    // 5. Prohibition 4 -- the timeout must exceed the loop it is
    //    protecting, with margin.
    v_timeout_too_short = ((timeout_us_i * 32'd1000)
                           < (credit_loop_ns_i * 32'd10));

    // 6. The gate itself.
    v_sent_without_credit = packet_sent && !credits_available_i;

    violations = { v_sent_without_credit, v_timeout_too_short,
                   v_lossless_claim_stale, v_lane_borrow,
                   v_under_reserved, v_overadvertised };
    conformant = (violations == 6'b000000);
  end
endmodule

// A1. The loop is propagation, turnaround and one frame, and nothing else.
p_cl_composition: assert property (@(posedge clk) disable iff (!rst_n)
  (metres != 0) |-> (loop_ns ==
    (((2 * 32'(prop_ns_x100(int'(metres), media_e'(media)))) / 100)
     + 32'(CREDIT_TURNAROUND_NS) + 32'(frame_ns(int'(rate_gbps))))));

// A2. The reservation is the loop times the rate.
p_cl_reservation: assert property (@(posedge clk) disable iff (!rst_n)
  (reserved_bytes_o == (32'(rate_gbps) * loop_ns) / 32'd8));

// A3. It is a floor, always, and never a target.
p_cl_is_floor: assert property (@(posedge clk) disable iff (!rst_n)
  (reservation_is_a_floor == 1'b1));

// A4. A short buffer caps the rate rather than risking overflow.
p_cl_short_caps: assert property (@(posedge clk) disable iff (!rst_n)
  buffer_insufficient |-> (achievable_gbps < rate_gbps));

// A5. And an adequate buffer does not.
p_cl_adequate: assert property (@(posedge clk) disable iff (!rst_n)
  !buffer_insufficient |-> (achievable_gbps == rate_gbps));

// A6. Propagation dominates the loop on long links.
p_cl_prop_dominates: assert property (@(posedge clk) disable iff (!rst_n)
  (metres >= 16'd1000) |-> (prop_share_pct >= 32'd90));

// A7. And does not on short ones.
p_cl_prop_minor: assert property (@(posedge clk) disable iff (!rst_n)
  (metres <= 16'd10) |-> (prop_share_pct <= 32'd20));

// A8. An Ethernet link reserves nothing.
p_cl_ethernet_zero: assert property (@(posedge clk) disable iff (!rst_n)
  (ethernet_reservation_bce == 32'd0));

// A9. A shortfall is counted every cycle it persists.
p_cl_stall_counted: assert property (@(posedge clk) disable iff (!rst_n)
  buffer_insufficient |=> (c_stall_events == $past(c_stall_events) + 32'd1));

// B1. The fabric figure is the per-link figure times the ports.
p_rs_scales: assert property (@(posedge clk) disable iff (!rst_n)
  (fabric_reservation_e2 == (per_link_bce / 32'd100) * 32'(ports)));

// B2. Over-commitment is never permitted.
p_rs_no_borrow: assert property (@(posedge clk) disable iff (!rst_n)
  (over_commitment_allowed == 1'b0));

// B3. A lossy fabric reserves nothing.
p_rs_lossy_zero: assert property (@(posedge clk) disable iff (!rst_n)
  (lossy_equivalent_bce == 32'd0));

// B4. Exceeding the switch is flagged rather than silently accepted.
p_rs_exceeds_flagged: assert property (@(posedge clk) disable iff (!rst_n)
  (share_of_switch_x100 >= 16'd10_000) |-> exceeds_switch);

// B5. And counted.
p_rs_infeasible_counted: assert property (@(posedge clk) disable iff (!rst_n)
  exceeds_switch |=> (c_infeasible_configs ==
                      $past(c_infeasible_configs) + 32'd1));

// B6. The ports a buffer serves falls as the reservation rises.
p_rs_monotone: assert property (@(posedge clk) disable iff (!rst_n)
  (per_link_bce > $past(per_link_bce)) |->
    (ports_a_buffer_serves <= $past(ports_a_buffer_serves)));

// B7. Zero ports is never reported for a nonzero buffer.
p_rs_nonzero: assert property (@(posedge clk) disable iff (!rst_n)
  ((switch_buffer_mb != 0) && (per_link_bce <= 32'd1_000_000)) |->
    (ports_a_buffer_serves != 32'd0));

// B8. The datapath figure follows the BCE figure.
p_rs_dp_follows: assert property (@(posedge clk) disable iff (!rst_n)
  (fabric_reservation_e2 == 32'd0) |-> (reservation_dp_milli == 32'd0));

// C1. The total is the sum over lanes, never the maximum.
p_vl_sum_not_max: assert property (@(posedge clk) disable iff (!rst_n)
  (reservation_total_bytes == per_lane_reserved_bytes * 32'(LANES)));

// C2. Borrowing is forbidden, which is why C1 is a sum.
p_vl_no_borrow: assert property (@(posedge clk) disable iff (!rst_n)
  (borrow_permitted == 1'b0));

// C3. A lane never exceeds its own reservation.
p_vl_within_lane: assert property (@(posedge clk) disable iff (!rst_n)
  (occupancy[lane_sel] <= per_lane_reserved_bytes));

// C4. An arrival that would exceed it is blocked rather than accepted.
p_vl_block: assert property (@(posedge clk) disable iff (!rst_n)
  (packet_arrives && ((occupancy[lane_sel] + 32'(packet_bytes))
                      > per_lane_reserved_bytes)) |-> lane_blocked);

// C5. And is counted.
p_vl_block_counted: assert property (@(posedge clk) disable iff (!rst_n)
  (packet_arrives && lane_blocked) |=>
    (c_lane_blocks == $past(c_lane_blocks) + 32'd1));

// C6. Lanes do not head-of-line block one another -- the guarantee
//     they were bought for, stated so a scheduler cannot quietly break it.
p_vl_independent: assert property (@(posedge clk) disable iff (!rst_n)
  (head_of_line_across_lanes == 1'b0));

// C7. The reservation fits or the configuration is rejected.
p_vl_fits: assert property (@(posedge clk) disable iff (!rst_n)
  fits_in_buffer |-> (reservation_total_bytes <= total_buffer_bytes));

// C8. Occupancy never goes negative on a drain.
p_vl_no_underflow: assert property (@(posedge clk) disable iff (!rst_n)
  (packet_drains && (occupancy[lane_sel] < 32'(packet_bytes))) |=>
    (occupancy[lane_sel] == $past(occupancy[lane_sel])));

// D1. The spread is certain, not probable.
p_ct_deterministic: assert property (@(posedge clk) disable iff (!rst_n)
  (tree_is_deterministic == 1'b1));

// D2. Full stall is the loop times the depth.
p_ct_stall_time: assert property (@(posedge clk) disable iff (!rst_n)
  (full_stall_ns == credit_loop_ns_i * 32'(stages)));

// D3. The drain takes as long as the growth.
p_ct_drain_symmetry: assert property (@(posedge clk) disable iff (!rst_n)
  (drain_ns == full_stall_ns));

// D4. Hops never exceed the fabric's depth.
p_ct_hops_bounded: assert property (@(posedge clk) disable iff (!rst_n)
  (hops_reached <= stages));

// D5. Hops never go backwards while the tree is active.
p_ct_monotone: assert property (@(posedge clk) disable iff (!rst_n)
  (tree_is_deterministic && !congestion_clear) |=>
    (hops_reached >= $past(hops_reached)));

// D6. A new event is counted once, not per cycle.
p_ct_event_once: assert property (@(posedge clk) disable iff (!rst_n)
  (congestion_start && $past(congestion_start)) |=>
    (c_tree_events == $past(c_tree_events)));

// D7. Stalled time accrues only while active.
p_ct_time_accrues: assert property (@(posedge clk) disable iff (!rst_n)
  (!tree_is_deterministic || congestion_clear) |=>
    (c_stall_ns_total == $past(c_stall_ns_total)));

// D8. Full stall is reached only after the whole depth's worth of loops.
p_ct_full_after: assert property (@(posedge clk) disable iff (!rst_n)
  fully_stalled |-> (hops_reached == stages));

// E1. The window is the bandwidth-delay product.
p_rc_window: assert property (@(posedge clk) disable iff (!rst_n)
  (window_bytes == (32'(rate_gbps) * 32'(rtt_ns)) / 32'd8));

// E2. Go-back-N retransmits the window.
p_rc_gbn: assert property (@(posedge clk) disable iff (!rst_n)
  !selective_repeat |-> (retransmit_bytes == window_bytes));

// E3. Selective repeat retransmits one packet.
p_rc_sr: assert property (@(posedge clk) disable iff (!rst_n)
  selective_repeat |-> (retransmit_bytes == 32'(mtu_octets)));

// E4. And costs a bit per packet in the window, per queue pair.
p_rc_bitmap: assert property (@(posedge clk) disable iff (!rst_n)
  selective_repeat |-> (bitmap_bits ==
    ((32'(window_packets) + 32'd1) * 32'(queue_pairs))));

// E5. Go-back-N costs no bitmap.
p_rc_no_bitmap: assert property (@(posedge clk) disable iff (!rst_n)
  !selective_repeat |-> (bitmap_bits == 32'd0));

// E6. A larger MTU reduces the amplification.
p_rc_mtu_helps: assert property (@(posedge clk) disable iff (!rst_n)
  (!selective_repeat && (mtu_octets > $past(mtu_octets))) |->
    (amplification_x10 <= $past(amplification_x10)));

// E7. The transport assumes lossless regardless of the link.
p_rc_assumes: assert property (@(posedge clk) disable iff (!rst_n)
  (transport_assumes_lossless == 1'b1));

// E8. And the link's actual state is a configuration input.
p_rc_config_input: assert property (@(posedge clk) disable iff (!rst_n)
  (link_losslessness_is_configured == pfc_configured_everywhere));

// E9. Retransmitted bytes accumulate at the amplified rate.
p_rc_accumulate: assert property (@(posedge clk) disable iff (!rst_n)
  packet_lost |=> (c_retransmit_bytes ==
                   $past(c_retransmit_bytes) + $past(retransmit_bytes)));

// F1. The timeout exceeds the credit loop with margin.
p_dl_timeout_margin: assert property (@(posedge clk) disable iff (!rst_n)
  ((timeout_us * 32'd1000) >= (credit_loop_ns_i * 32'd10)));

// F2. A starved lane is one with work and no credit.
p_dl_starved_def: assert property (@(posedge clk) disable iff (!rst_n)
  (lane_starved == (lane_has_work & ~lane_has_credit)));

// F3. A discard clears the lane's starvation timer.
p_dl_discard_clears: assert property (@(posedge clk) disable iff (!rst_n)
  discard_required |=> (starved_us[$past(discard_lane)] == 32'd0));

// F4. And permanently retires the lossless claim.
p_dl_claim_retired: assert property (@(posedge clk) disable iff (!rst_n)
  discard_required |=> !is_still_lossless);

// F5. The claim, once retired, never returns.
p_dl_claim_sticky: assert property (@(posedge clk) disable iff (!rst_n)
  !is_still_lossless |=> !is_still_lossless);

// F6. A fabric claiming lossless after a discard is a violation.
p_cf_stale_claim: assert property (@(posedge clk) disable iff (!rst_n)
  (claims_lossless && discard_fired) |-> v_lossless_claim_stale);

// F7. The drop counter is labelled as uninformative.
p_tl_drop_label: assert property (@(posedge clk) disable iff (!rst_n)
  (drop_counter_is_meaningful == 1'b0));

// F8. Stalled percentage is bounded by 100.
p_tl_pct_bounded: assert property (@(posedge clk) disable iff (!rst_n)
  (stalled_pct <= 16'd100));

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

c_cl_short_buffer:  cover property (@(posedge clk) buffer_insufficient);
c_cl_long_link:     cover property (@(posedge clk) metres >= 16'd1000);
c_rs_exceeds:       cover property (@(posedge clk) exceeds_switch);
c_vl_blocked:       cover property (@(posedge clk) lane_blocked);
c_vl_one_lane_hot:  cover property (@(posedge clk)
                      (occupancy[0] > (per_lane_reserved_bytes / 32'd2)) &&
                      (occupancy[1] == 32'd0));
c_ct_full_stall:    cover property (@(posedge clk) fully_stalled);
c_ct_two_hops:      cover property (@(posedge clk) hops_reached >= 16'd2);
c_rc_gbn_loss:      cover property (@(posedge clk) packet_lost && !selective_repeat);
c_rc_sr_loss:       cover property (@(posedge clk) packet_lost && selective_repeat);
c_dl_starved:       cover property (@(posedge clk) lane_starved != 8'd0);
c_dl_discard:       cover property (@(posedge clk) discard_required);
c_dl_not_lossless:  cover property (@(posedge clk) !is_still_lossless);
c_tl_stalled_high:  cover property (@(posedge clk) stalled_pct >= 16'd5);
c_cf_stale:         cover property (@(posedge clk) v_lossless_claim_stale);