Propagation Delay

copper, polyethylene:  v = 0.66 × 2.998e8 = 1.98e8 m/s  ->  5.05 ns per metre
fibre, group index 1.47: v = 2.998e8 / 1.47 = 2.04e8 m/s  ->  4.90 ns per metre

51.2 us / 10 ns per metre = 5120 metres of one-way distance

// SYNTHESIZABLE.
//
// Estimates a link's physical length from a measured round-trip time.
//
// The arithmetic is one division, and the interesting content is what it
// depends on:
//
//   the measured round trip     -- this design can measure it
//   the velocity factor         -- a property of the CABLE, not the link
//   the local turnaround delay  -- a property of the PEER, not the cable
//
// The last two are the reason the answer is an estimate. A design that
// reports a length without reporting the assumptions behind it has
// converted a measurement into a claim.
package prop_pkg;
 
  // Picoseconds per metre, one way. Derived rather than quoted:
  //   v = VF * c, delay = 1/v.
  // Polyethylene twisted pair: VF 0.66 -> 5052 ps/m.
  // Silica fibre, group index 1.47 -> 4903 ps/m.
  localparam int unsigned PS_PER_M_COPPER = 5052;
  localparam int unsigned PS_PER_M_FIBRE  = 4903;
 
  typedef enum logic [1:0] { MED_COPPER, MED_SMF, MED_MMF } medium_e;
 
  function automatic int unsigned ps_per_metre(input medium_e m);
    case (m)
      MED_COPPER: ps_per_metre = PS_PER_M_COPPER;
      MED_SMF:    ps_per_metre = PS_PER_M_FIBRE;
      MED_MMF:    ps_per_metre = 4943;
      default:    ps_per_metre = PS_PER_M_COPPER;
    endcase
  endfunction
 
endpackage
 
module link_length_estimator
  import prop_pkg::*;
#(
  // The peer's turnaround: the time between it receiving the last bit of
  // the probe and emitting the first bit of the response. Subtracted
  // before the length is inferred, because it is not cable.
  parameter int unsigned PEER_TURNAROUND_PS = 0
) (
  input  logic    clk,
  input  logic    rst_n,
 
  input  medium_e medium,
  input  logic    rt_valid,
  input  logic [39:0] round_trip_ps,
 
  output logic        est_valid,
  output logic [23:0] length_m,
  // The one-way delay, which is what a latency budget actually wants --
  // the length is a derived convenience.
  output logic [39:0] one_way_ps,
 
  // The measurement is invalid if the round trip is shorter than the
  // peer's own turnaround, which means the turnaround parameter is wrong
  // or the measurement did not span the link.
  output logic        implausible,
  // Reported alongside the answer, so a reader can see what it assumed.
  output logic [15:0] assumed_ps_per_m
);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      est_valid        <= 1'b0;
      length_m         <= '0;
      one_way_ps       <= '0;
      implausible      <= 1'b0;
      assumed_ps_per_m <= '0;
    end else begin
      est_valid   <= 1'b0;
      implausible <= 1'b0;
 
      if (rt_valid) begin
        automatic int unsigned ppm = ps_per_metre(medium);
        assumed_ps_per_m <= 16'(ppm);
 
        if (round_trip_ps <= 40'(PEER_TURNAROUND_PS)) begin
          // Not a cable-length measurement at all.
          implausible <= 1'b1;
        end else begin
          automatic logic [39:0] cable_rt =
              round_trip_ps - 40'(PEER_TURNAROUND_PS);
          one_way_ps <= cable_rt / 2;
          // Length from the one-way delay. The division is by a constant
          // per medium, so it synthesises to a multiply by a reciprocal.
          length_m   <= 24'((cable_rt / 2) / 40'(ppm));
          est_valid  <= 1'b1;
        end
      end
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// Detects and quantifies directional asymmetry, which a round-trip
// measurement alone cannot see.
//
// The method is the only one available: obtain the two one-way delays
// SEPARATELY, from a source that does not derive them from the round
// trip. In practice that means a peer that timestamps its own transmit
// and receive events and reports them -- so the asymmetry is computed
// from four timestamps rather than from one interval.
//
// Without that, asymmetry is not merely hard to measure: it is
// unobservable in principle, because the round trip is a sum and one
// equation cannot resolve two unknowns.
module delay_asymmetry_detector
  import prop_pkg::*;
#(
  parameter int unsigned CNT_W = 32,
  // Asymmetry above which the link is flagged. Derived from the timing
  // accuracy a design promises: an asymmetry of A costs A/2 of error.
  parameter int unsigned ASYM_THRESHOLD_PS = 20_000   // 20 ns -> 10 ns error
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  // Four timestamps, from a peer that reports its own. t1 and t4 are
  // local; t2 and t3 are the peer's.
  input  logic        ts_valid,
  input  logic [39:0] t1_local_tx,
  input  logic [39:0] t2_peer_rx,
  input  logic [39:0] t3_peer_tx,
  input  logic [39:0] t4_local_rx,
 
  output logic        result_valid,
  output logic [39:0] forward_ps,
  output logic [39:0] reverse_ps,
  output logic signed [40:0] asymmetry_ps,
  output logic [39:0] round_trip_ps,
 
  // The error a symmetric assumption would introduce, stated directly
  // rather than left for a reader to halve.
  output logic signed [40:0] time_transfer_error_ps,
 
  output logic             asymmetry_exceeded,
  output logic [CNT_W-1:0] c_exceeded,
  output logic signed [40:0] worst_asymmetry_ps
);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      result_valid <= 1'b0; forward_ps <= '0; reverse_ps <= '0;
      asymmetry_ps <= '0; round_trip_ps <= '0;
      time_transfer_error_ps <= '0;
      asymmetry_exceeded <= 1'b0; c_exceeded <= '0; worst_asymmetry_ps <= '0;
    end else begin
      result_valid       <= 1'b0;
      asymmetry_exceeded <= 1'b0;
 
      if (clear) begin
        c_exceeded <= '0;
        // worst_asymmetry_ps deliberately survives: it describes the
        // cabling, which does not change when a counter is cleared.
      end
 
      if (ts_valid) begin
        automatic logic [39:0] fwd = t2_peer_rx - t1_local_tx;
        automatic logic [39:0] rev = t4_local_rx - t3_peer_tx;
 
        forward_ps    <= fwd;
        reverse_ps    <= rev;
        round_trip_ps <= fwd + rev;
        asymmetry_ps  <= $signed({1'b0, fwd}) - $signed({1'b0, rev});
        // The whole point, stated as the consequence rather than as the
        // cause: a symmetric assumption is wrong by half the asymmetry.
        time_transfer_error_ps <=
            ($signed({1'b0, fwd}) - $signed({1'b0, rev})) / 2;
        result_valid  <= 1'b1;
 
        if (((fwd > rev) ? (fwd - rev) : (rev - fwd)) > 40'(ASYM_THRESHOLD_PS)) begin
          asymmetry_exceeded <= 1'b1;
          c_exceeded         <= c_exceeded + 1'b1;
        end
 
        if (((fwd > rev) ? $signed({1'b0, fwd - rev}) : $signed({1'b0, rev - fwd}))
            > ((worst_asymmetry_ps < 0) ? -worst_asymmetry_ps : worst_asymmetry_ps))
          worst_asymmetry_ps <= $signed({1'b0, fwd}) - $signed({1'b0, rev});
      end
    end
  end
 
endmodule

// SYNTHESIZABLE DIAGNOSTIC.
//
// Watches the measured one-way delay and reports when it moves.
//
// The quantity is supposed to be constant, which makes it an unusually
// good thing to monitor: any change has a cause, and the SIZE of the
// change names the cause.
//
//   a few hundred ps        -- temperature. Cable delay drifts with
//        thermal expansion and with the dielectric's permittivity, on a
//        daily cycle.
//   tens of nanoseconds     -- the cable was re-patched. Somebody moved
//        a jumper and the path is a few metres different.
//   hundreds of nanoseconds -- the route changed. A protection switch, a
//        repair splice, or a different fibre entirely.
//   erratic, large          -- the measurement is broken, not the cable.
module cable_length_change_monitor
  import prop_pkg::*;
#(
  parameter int unsigned CNT_W = 32,
  // Establish the baseline from this many measurements before judging
  // anything. A baseline of one sample turns measurement noise into a
  // cable-change report.
  parameter int unsigned BASELINE_N = 64,
  parameter int unsigned THERMAL_PS = 1_000,     // 1 ns
  parameter int unsigned REPATCH_PS = 50_000     // 50 ns -> ~10 m
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic        meas_valid,
  input  logic [39:0] one_way_ps,
 
  output logic        baseline_valid,
  output logic [39:0] baseline_ps,
  output logic signed [40:0] deviation_ps,
 
  output logic        drift_thermal,
  output logic        change_repatch,
  output logic        change_route,
  output logic        measurement_suspect,
 
  output logic [CNT_W-1:0] c_changes,
  output logic [39:0]      min_seen_ps,
  output logic [39:0]      max_seen_ps
);
 
  logic [39:0] sum_q;
  logic [CNT_W-1:0] n_q;
  logic [CNT_W-1:0] since_change_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      sum_q <= '0; n_q <= '0; since_change_q <= '0;
      baseline_valid <= 1'b0; baseline_ps <= '0; deviation_ps <= '0;
      drift_thermal <= 1'b0; change_repatch <= 1'b0;
      change_route <= 1'b0; measurement_suspect <= 1'b0;
      c_changes <= '0; min_seen_ps <= '1; max_seen_ps <= '0;
    end else begin
      drift_thermal       <= 1'b0;
      change_repatch      <= 1'b0;
      change_route        <= 1'b0;
      measurement_suspect <= 1'b0;
 
      if (clear) begin
        c_changes <= '0;
        // min and max deliberately survive: they bound what this link
        // has ever measured, which a counter clear must not erase.
      end
 
      if (meas_valid) begin
        if (one_way_ps < min_seen_ps) min_seen_ps <= one_way_ps;
        if (one_way_ps > max_seen_ps) max_seen_ps <= one_way_ps;
 
        if (!baseline_valid) begin
          // Build the baseline from several samples. A single-sample
          // baseline reports every subsequent measurement's noise as a
          // cable change.
          sum_q <= sum_q + one_way_ps;
          n_q   <= n_q + 1'b1;
          if (n_q == CNT_W'(BASELINE_N - 1)) begin
            baseline_ps    <= (sum_q + one_way_ps) / 40'(BASELINE_N);
            baseline_valid <= 1'b1;
          end
        end else begin
          automatic logic signed [40:0] dev =
              $signed({1'b0, one_way_ps}) - $signed({1'b0, baseline_ps});
          automatic logic [39:0] mag = (dev < 0) ? 40'(-dev) : 40'(dev);
          deviation_ps <= dev;
          since_change_q <= since_change_q + 1'b1;
 
          // The magnitude bands of the header comment, largest first.
          if (mag > 40'(REPATCH_PS) * 40'd10) begin
            // Very large. Distinguished from a route change by whether
            // it PERSISTS: a route change settles at a new value, a
            // measurement fault does not.
            if (since_change_q < CNT_W'(BASELINE_N)) measurement_suspect <= 1'b1;
            else begin
              change_route   <= 1'b1;
              c_changes      <= c_changes + 1'b1;
              since_change_q <= '0;
            end
          end else if (mag > 40'(REPATCH_PS)) begin
            change_repatch <= 1'b1;
            c_changes      <= c_changes + 1'b1;
            since_change_q <= '0;
          end else if (mag > 40'(THERMAL_PS)) begin
            drift_thermal <= 1'b1;
          end
        end
      end
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// Compares a link's measured propagation against the budget the
// deployment was designed to, and reports which constraint binds.
//
// There are three different limits and they are routinely confused:
//
//   REACH     -- the medium's attenuation limit. A physical property of
//        the cable and the optics (Chapters 3.1, 3.2). Exceeding it means
//        the signal does not arrive.
//   LATENCY   -- the application's budget. Exceeding it means the signal
//        arrives too late to be useful.
//   STANDARDS -- the horizontal cabling delay limit, about 570 ns for a
//        structured-wiring channel.
//
// A link can satisfy reach and violate latency, or the reverse. Merging
// them into "the link is too long" loses which one, and they have
// different fixes: better optics, a different application design, or a
// different cable route.
module propagation_budget_checker
  import prop_pkg::*;
(
  input  logic clk,
  input  logic rst_n,
 
  input  logic        meas_valid,
  input  logic [39:0] one_way_ps,
  input  logic [23:0] length_m,
 
  // The three limits, independently configured because they come from
  // three different documents.
  input  logic [23:0] reach_limit_m,
  input  logic [39:0] latency_budget_ps,
  input  logic [39:0] standards_limit_ps,
 
  output logic        result_valid,
  output logic        over_reach,
  output logic        over_latency,
  output logic        over_standards,
  // Which limit binds FIRST as the link grows. The actionable output:
  // it says which document to argue with.
  output logic [1:0]  binding_limit,
  output logic [39:0] headroom_ps
);
 
  localparam logic [1:0] B_REACH = 2'd0;
  localparam logic [1:0] B_LATENCY = 2'd1;
  localparam logic [1:0] B_STANDARDS = 2'd2;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      result_valid <= 1'b0; over_reach <= 1'b0; over_latency <= 1'b0;
      over_standards <= 1'b0; binding_limit <= B_REACH; headroom_ps <= '0;
    end else begin
      result_valid <= meas_valid;
 
      if (meas_valid) begin
        automatic logic [39:0] reach_ps =
            40'(reach_limit_m) * 40'(PS_PER_M_COPPER);
 
        over_reach     <= (length_m  > reach_limit_m);
        over_latency   <= (one_way_ps > latency_budget_ps);
        over_standards <= (one_way_ps > standards_limit_ps);
 
        // Whichever limit is SMALLEST in time is the one that binds as
        // the link grows -- which is not necessarily the one currently
        // being violated.
        if ((reach_ps <= latency_budget_ps) && (reach_ps <= standards_limit_ps)) begin
          binding_limit <= B_REACH;
          headroom_ps   <= (reach_ps > one_way_ps) ? (reach_ps - one_way_ps) : 40'd0;
        end else if (latency_budget_ps <= standards_limit_ps) begin
          binding_limit <= B_LATENCY;
          headroom_ps   <= (latency_budget_ps > one_way_ps)
                             ? (latency_budget_ps - one_way_ps) : 40'd0;
        end else begin
          binding_limit <= B_STANDARDS;
          headroom_ps   <= (standards_limit_ps > one_way_ps)
                             ? (standards_limit_ps - one_way_ps) : 40'd0;
        end
      end
    end
  end
 
endmodule

// SYNTHESIZABLE INSTRUMENTATION.
//
// Separates the error terms in a time transfer, so that the one which
// cannot be averaged away is visible rather than buried.
//
// Three of the terms shrink with more samples and one does not:
//
//   quantisation, noise  -- random. The mean converges as 1/sqrt(N).
//   clock drift          -- bounded by the measurement interval.
//   ASYMMETRY            -- systematic. Contributes exactly half the
//        asymmetry, as a constant offset, forever.
//
// A design that reports only a total error and observes it falling with
// more samples will conclude the measurement is converging. It is --
// onto the wrong answer, offset by half the asymmetry.
module time_transfer_error_accumulator
  import prop_pkg::*;
#(
  parameter int unsigned CNT_W = 32
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic        sample_valid,
  input  logic signed [40:0] asymmetry_ps,
  input  logic [39:0] quantisation_ps,
  input  logic [39:0] noise_estimate_ps,
  input  logic [39:0] drift_bound_ps,
 
  output logic        result_valid,
  // The systematic part. Constant with N, which is the whole point.
  output logic signed [40:0] systematic_error_ps,
  // The random part, which shrinks with the sample count.
  output logic [39:0] random_error_ps,
  output logic [39:0] total_bound_ps,
 
  output logic [CNT_W-1:0] samples,
  // High when the systematic term exceeds the random one -- the point at
  // which taking more samples stops helping, which is the single most
  // useful thing this module reports.
  output logic             systematic_dominates,
  output logic [CNT_W-1:0] samples_at_crossover
);
 
  logic [CNT_W-1:0] n_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      n_q <= '0; result_valid <= 1'b0;
      systematic_error_ps <= '0; random_error_ps <= '0; total_bound_ps <= '0;
      samples <= '0; systematic_dominates <= 1'b0; samples_at_crossover <= '0;
    end else begin
      result_valid <= 1'b0;
 
      if (clear) begin
        n_q <= '0; samples <= '0;
        // The crossover point deliberately survives: it describes the
        // link's cabling, not this measurement session.
      end else if (sample_valid) begin
        automatic logic signed [40:0] sysrr = asymmetry_ps / 2;
        automatic logic [39:0] rnd;
 
        n_q     <= n_q + 1'b1;
        samples <= n_q + 1'b1;
 
        // Random terms shrink as 1/sqrt(N). Approximated by a shift per
        // quadrupling, which is exact enough for a bound and needs no
        // square root.
        rnd = (quantisation_ps + noise_estimate_ps) >> (sqrt_shift(n_q + 1'b1));
 
        systematic_error_ps <= sysrr;
        random_error_ps     <= rnd + drift_bound_ps;
        total_bound_ps      <= ((sysrr < 0) ? 40'(-sysrr) : 40'(sysrr))
                               + rnd + drift_bound_ps;
        result_valid        <= 1'b1;
 
        if (((sysrr < 0) ? 40'(-sysrr) : 40'(sysrr)) > (rnd + drift_bound_ps)) begin
          if (!systematic_dominates) samples_at_crossover <= n_q + 1'b1;
          systematic_dominates <= 1'b1;
        end
      end
    end
  end
 
  // log4(N), so each quadrupling of the sample count halves the random
  // term -- the 1/sqrt(N) behaviour, as a shift.
  function automatic int unsigned sqrt_shift(input logic [CNT_W-1:0] n);
    sqrt_shift = 0;
    for (int i = 0; i < CNT_W/2; i++)
      if (n > (CNT_W'(1) << (2*i))) sqrt_shift = i + 1;
  endfunction
 
endmodule

// ---------------------------------------------------------------------
// P1 -- THE DEFINITION. Propagation is length times the medium's delay
// per metre, and the line rate appears nowhere in it.
// ---------------------------------------------------------------------
property p_delay_is_length_times_velocity;
  @(posedge clk) disable iff (!rst_n)
    est_valid |-> (one_way_ps == (40'(length_m) * 40'(assumed_ps_per_m)));
endproperty
a_delay_is_length_times_velocity: assert property (p_delay_is_length_times_velocity);
 
// ---------------------------------------------------------------------
// P2 -- The estimate reports the assumption it used. A length without a
// velocity factor is a claim rather than a measurement.
// ---------------------------------------------------------------------
property p_assumption_reported;
  @(posedge clk) disable iff (!rst_n)
    est_valid |-> (assumed_ps_per_m == 16'(ps_per_metre($past(medium))));
endproperty
a_assumption_reported: assert property (p_assumption_reported);
 
// ---------------------------------------------------------------------
// P3 -- A round trip shorter than the peer's own turnaround is not a
// cable measurement, and must be refused rather than converted.
// ---------------------------------------------------------------------
property p_implausible_refused;
  @(posedge clk) disable iff (!rst_n)
    (rt_valid && (round_trip_ps <= 40'(PEER_TURNAROUND_PS))) |=> implausible;
endproperty
a_implausible_refused: assert property (p_implausible_refused);
 
// ---------------------------------------------------------------------
// P4 -- An implausible measurement produces no estimate.
// ---------------------------------------------------------------------
property p_no_estimate_when_implausible;
  @(posedge clk) disable iff (!rst_n)
    implausible |-> !est_valid;
endproperty
a_no_estimate_when_implausible: assert property (p_no_estimate_when_implausible);
 
// ---------------------------------------------------------------------
// P5 -- Every medium's delay per metre is within the band this chapter
// derived. A constant outside it means somebody entered a velocity
// factor rather than a delay, or a metre rather than a foot.
// ---------------------------------------------------------------------
// synopsys translate_off
a_delay_constants_plausible: assert final
  ((PS_PER_M_COPPER > 3_300) && (PS_PER_M_COPPER < 5_600) &&
   (PS_PER_M_FIBRE  > 3_300) && (PS_PER_M_FIBRE  < 5_600))
  else $fatal(1, "a per-metre delay constant is outside the physically possible band");
// synopsys translate_on
 
// ---------------------------------------------------------------------
// P6 -- No medium is faster than light. The check that catches a
// velocity factor entered as a multiplier rather than a fraction.
// ---------------------------------------------------------------------
// synopsys translate_off
a_not_faster_than_light: assert final
  ((PS_PER_M_COPPER >= 3_336) && (PS_PER_M_FIBRE >= 3_336))
  else $fatal(1, "a per-metre delay implies a velocity above c");
// synopsys translate_on
 
// ---------------------------------------------------------------------
// P7 -- The round trip is the sum of the two one-way delays, which is
// the relation that makes asymmetry unobservable from it alone.
// ---------------------------------------------------------------------
property p_round_trip_is_sum;
  @(posedge clk) disable iff (!rst_n)
    result_valid |-> (round_trip_ps == (forward_ps + reverse_ps));
endproperty
a_round_trip_is_sum: assert property (p_round_trip_is_sum);
 
// ---------------------------------------------------------------------
// P8 -- The asymmetry is the difference, and the time-transfer error is
// exactly half of it. Stated so a reader cannot mistake one for the
// other.
// ---------------------------------------------------------------------
property p_error_is_half_asymmetry;
  @(posedge clk) disable iff (!rst_n)
    result_valid |-> (time_transfer_error_ps == (asymmetry_ps / 2));
endproperty
a_error_is_half_asymmetry: assert property (p_error_is_half_asymmetry);
 
// ---------------------------------------------------------------------
// P9 -- Asymmetry requires four timestamps. A result produced without
// them was derived from a round trip, which cannot resolve it.
// ---------------------------------------------------------------------
property p_asymmetry_needs_four_timestamps;
  @(posedge clk) disable iff (!rst_n)
    result_valid |-> $past(ts_valid);
endproperty
a_asymmetry_needs_four_timestamps: assert property (p_asymmetry_needs_four_timestamps);
 
// ---------------------------------------------------------------------
// P10 -- The worst asymmetry survives a counter clear: it describes the
// cabling, which a housekeeping action does not change.
// ---------------------------------------------------------------------
property p_worst_asymmetry_survives;
  @(posedge clk) disable iff (!rst_n)
    clear |=> $stable(worst_asymmetry_ps);
endproperty
a_worst_asymmetry_survives: assert property (p_worst_asymmetry_survives);
 
// ---------------------------------------------------------------------
// P11 -- The baseline is built from several samples. A single-sample
// baseline turns measurement noise into a cable-change report.
// ---------------------------------------------------------------------
property p_baseline_needs_samples;
  @(posedge clk) disable iff (!rst_n)
    $rose(baseline_valid) |-> ($past(n_q) == CNT_W'(BASELINE_N - 1));
endproperty
a_baseline_needs_samples: assert property (p_baseline_needs_samples);
 
// ---------------------------------------------------------------------
// P12 -- No change is reported before a baseline exists.
// ---------------------------------------------------------------------
property p_no_change_without_baseline;
  @(posedge clk) disable iff (!rst_n)
    (!baseline_valid) |-> (!drift_thermal && !change_repatch && !change_route);
endproperty
a_no_change_without_baseline: assert property (p_no_change_without_baseline);
 
// ---------------------------------------------------------------------
// P13 -- The change classes are exclusive, and ordered by magnitude.
// ---------------------------------------------------------------------
property p_change_classes_onehot;
  @(posedge clk) disable iff (!rst_n)
    meas_valid |=> $onehot0({drift_thermal, change_repatch, change_route,
                             measurement_suspect});
endproperty
a_change_classes_onehot: assert property (p_change_classes_onehot);
 
// ---------------------------------------------------------------------
// P14 -- The binding limit is the smallest of the three in time. It is
// reported whether or not any limit is currently violated.
// ---------------------------------------------------------------------
property p_binding_is_smallest;
  @(posedge clk) disable iff (!rst_n)
    result_valid |-> ((binding_limit == B_REACH)     ||
                      (binding_limit == B_LATENCY)   ||
                      (binding_limit == B_STANDARDS));
endproperty
a_binding_is_smallest: assert property (p_binding_is_smallest);
 
// ---------------------------------------------------------------------
// P15 -- The systematic error term does not shrink with the sample
// count. The property that makes Section 9's argument checkable.
// ---------------------------------------------------------------------
property p_systematic_does_not_average;
  @(posedge clk) disable iff (!rst_n)
    (result_valid && $stable(asymmetry_ps)) |-> $stable(systematic_error_ps);
endproperty
a_systematic_does_not_average: assert property (p_systematic_does_not_average);
 
// ---------------------------------------------------------------------
// P16 -- The random term does shrink, so the two behave differently and
// a design cannot conflate them.
// ---------------------------------------------------------------------
property p_random_does_average;
  @(posedge clk) disable iff (!rst_n)
    (result_valid && (samples > $past(samples)))
      |-> (random_error_ps <= $past(random_error_ps));
endproperty
a_random_does_average: assert property (p_random_does_average);
 
// ---------------------------------------------------------------------
// P17 -- The bandwidth-delay product scales with the rate even though
// the delay does not. Asserted as a relation, because it is the one
// quantity in this chapter that is NOT rate-independent.
// ---------------------------------------------------------------------
property p_bdp_scales_with_rate;
  @(posedge clk) disable iff (!rst_n)
    bdp_valid |-> (bdp_bytes == ((round_trip_ps * rate_bps) / 40'd8_000_000_000_000));
endproperty
a_bdp_scales_with_rate: assert property (p_bdp_scales_with_rate);
 
// ---------------------------------------------------------------------
// P18 -- Propagation itself does NOT change when the rate does. The
// chapter's central claim, checkable directly.
// ---------------------------------------------------------------------
property p_propagation_rate_independent;
  @(posedge clk) disable iff (!rst_n)
    (meas_valid && $stable(length_m) && !$stable(rate_bps))
      |-> $stable(one_way_ps);
endproperty
a_propagation_rate_independent: assert property (p_propagation_rate_independent)
  else $error("propagation delay moved when only the line rate changed");
 
// ---------------------------------------------------------------------
// P19 -- COVERAGE. Each change class, and the crossover at which more
// samples stop helping.
// ---------------------------------------------------------------------
c_thermal:     cover property (@(posedge clk) disable iff (!rst_n) drift_thermal);
c_repatch:     cover property (@(posedge clk) disable iff (!rst_n) change_repatch);
c_route:       cover property (@(posedge clk) disable iff (!rst_n) change_route);
c_crossover:   cover property (@(posedge clk) disable iff (!rst_n) $rose(systematic_dominates));
 
// ---------------------------------------------------------------------
// P20 -- COVERAGE. A genuinely asymmetric link, which a symmetric
// stimulus generator never produces.
// ---------------------------------------------------------------------
c_asymmetric_link: cover property (
  @(posedge clk) disable iff (!rst_n) (result_valid && (asymmetry_ps != 0))
);