Latency Decomposition

// SYNTHESIZABLE INSTRUMENTATION.
//
// Timestamps a frame at each stage boundary and reports the intervals
// between them, so that each latency term is measured rather than
// inferred.
//
// The boundaries are chosen so that each interval contains EXACTLY ONE
// mechanism:
//
//   arrival -> dequeue    : queueing. Nothing else happens here.
//   dequeue -> proc_done  : per-frame processing. Lookup, filter,
//                           descriptor -- the pipeline.
//   proc_done -> tx_start : store-and-forward wait, if any.
//   tx_start -> tx_last   : serialization. Chapter 8.1's term, measured
//                           rather than computed, so the two can be
//                           cross-checked.
//
// Propagation is NOT measurable here: it happens outside the device.
// Chapter 8.2's estimator supplies it, and this module leaves a port for
// it rather than pretending to observe it.
package latency_pkg;
 
  typedef enum logic [2:0] {
    LT_QUEUEING,
    LT_PROCESSING,
    LT_STORE_FORWARD,
    LT_SERIALIZATION,
    LT_PROPAGATION,     // supplied, not measured
    LT_NUM
  } lat_term_e;
 
  localparam int unsigned TERMS = 5;
 
endpackage
 
module stage_latency_accumulator
  import latency_pkg::*;
#(
  parameter int unsigned TS_W  = 40,     // picoseconds
  parameter int unsigned CNT_W = 48
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  // Stage-boundary events for one frame, with their timestamps.
  input  logic          ev_arrival,
  input  logic          ev_dequeue,
  input  logic          ev_proc_done,
  input  logic          ev_tx_start,
  input  logic          ev_tx_last,
  input  logic [TS_W-1:0] timestamp_ps,
 
  // Supplied from outside the device (Chapter 8.2).
  input  logic [TS_W-1:0] propagation_ps,
 
  output logic            frame_valid,
  output logic [TS_W-1:0] term_ps [TERMS],
  output logic [TS_W-1:0] total_ps,
 
  output logic [CNT_W-1:0] sum_ps  [TERMS],
  output logic [CNT_W-1:0] frames,
  output logic [TS_W-1:0]  worst_ps [TERMS]
);
 
  logic [TS_W-1:0] t_arr_q, t_deq_q, t_prc_q, t_txs_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      t_arr_q <= '0; t_deq_q <= '0; t_prc_q <= '0; t_txs_q <= '0;
      frame_valid <= 1'b0; total_ps <= '0; frames <= '0;
      for (int i = 0; i < TERMS; i++) begin
        term_ps[i] <= '0; sum_ps[i] <= '0; worst_ps[i] <= '0;
      end
    end else begin
      frame_valid <= 1'b0;
 
      if (clear) begin
        frames <= '0;
        for (int i = 0; i < TERMS; i++) sum_ps[i] <= '0;
        // worst_ps deliberately survives: the worst each term has ever
        // been is a design input, not a measurement window.
      end
 
      if (ev_arrival)   t_arr_q <= timestamp_ps;
      if (ev_dequeue)   t_deq_q <= timestamp_ps;
      if (ev_proc_done) t_prc_q <= timestamp_ps;
      if (ev_tx_start)  t_txs_q <= timestamp_ps;
 
      if (ev_tx_last) begin
        automatic logic [TS_W-1:0] q  = t_deq_q - t_arr_q;
        automatic logic [TS_W-1:0] pr = t_prc_q - t_deq_q;
        automatic logic [TS_W-1:0] sf = t_txs_q - t_prc_q;
        automatic logic [TS_W-1:0] sz = timestamp_ps - t_txs_q;
 
        term_ps[LT_QUEUEING]      <= q;
        term_ps[LT_PROCESSING]    <= pr;
        term_ps[LT_STORE_FORWARD] <= sf;
        term_ps[LT_SERIALIZATION] <= sz;
        term_ps[LT_PROPAGATION]   <= propagation_ps;
 
        total_ps    <= q + pr + sf + sz + propagation_ps;
        frame_valid <= 1'b1;
        frames      <= frames + 1'b1;
 
        sum_ps[LT_QUEUEING]      <= sum_ps[LT_QUEUEING]      + CNT_W'(q);
        sum_ps[LT_PROCESSING]    <= sum_ps[LT_PROCESSING]    + CNT_W'(pr);
        sum_ps[LT_STORE_FORWARD] <= sum_ps[LT_STORE_FORWARD] + CNT_W'(sf);
        sum_ps[LT_SERIALIZATION] <= sum_ps[LT_SERIALIZATION] + CNT_W'(sz);
        sum_ps[LT_PROPAGATION]   <= sum_ps[LT_PROPAGATION]   + CNT_W'(propagation_ps);
 
        if (q  > worst_ps[LT_QUEUEING])      worst_ps[LT_QUEUEING]      <= q;
        if (pr > worst_ps[LT_PROCESSING])    worst_ps[LT_PROCESSING]    <= pr;
        if (sf > worst_ps[LT_STORE_FORWARD]) worst_ps[LT_STORE_FORWARD] <= sf;
        if (sz > worst_ps[LT_SERIALIZATION]) worst_ps[LT_SERIALIZATION] <= sz;
      end
    end
  end
 
endmodule

// SYNTHESIZABLE INSTRUMENTATION.
//
// Estimates latency percentiles from a fixed amount of state.
//
// The method is a histogram with LOGARITHMIC bucket edges, and the edges
// are the whole design:
//
//   uniform edges over 0..1 ms with 16 buckets gives 62.5 us resolution,
//     which puts fifteen buckets in a range the distribution never
//     visits and lumps everything interesting into the first one.
//
//   logarithmic edges give constant RELATIVE resolution, which is what a
//     percentile question actually wants: "is the tail at 90 us or at
//     900 us" matters, "is it at 90 or 95" usually does not.
//
// The estimate is accurate to within one bucket width, at any sample
// count, from sixteen counters -- and no exact method beats that trade
// for the decision the number feeds.
module latency_percentile_estimator
  import latency_pkg::*;
#(
  parameter int unsigned NBUCKET = 16,
  parameter int unsigned CNT_W   = 40,
  // Lowest bucket's upper edge, in picoseconds. Each subsequent bucket
  // doubles, so 16 buckets span 2^15 = 32768x -- from 1 us to 32 ms.
  parameter int unsigned BASE_PS = 1_000_000
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic            sample_valid,
  input  logic [39:0]     latency_ps,
 
  // Which percentile to report, in tenths of a percent: 999 is the
  // 99.9th. A parameter would fix it at build time; an input lets one
  // instrument answer several questions.
  input  logic [9:0]      percentile_tenths,
 
  output logic [CNT_W-1:0] bucket [NBUCKET],
  output logic [CNT_W-1:0] samples,
 
  output logic             estimate_valid,
  // The bucket's upper edge: the estimate is "at most this".
  output logic [39:0]      percentile_upper_ps,
  output logic [3:0]       percentile_bucket,
  // True when the requested percentile falls in the top bucket, which
  // means the range was too small and the answer is a lower bound only.
  output logic             saturated
);
 
  // Logarithmic bucket selection: which power of two the sample exceeds.
  function automatic int unsigned bucket_of(input logic [39:0] v);
    bucket_of = 0;
    for (int i = 0; i < NBUCKET; i++)
      if (v >= (40'(BASE_PS) << i)) bucket_of = i + 1;
    if (bucket_of > NBUCKET-1) bucket_of = NBUCKET-1;
  endfunction
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (int i = 0; i < NBUCKET; i++) bucket[i] <= '0;
      samples <= '0; estimate_valid <= 1'b0;
      percentile_upper_ps <= '0; percentile_bucket <= '0; saturated <= 1'b0;
    end else begin
      estimate_valid <= 1'b0;
 
      if (clear) begin
        for (int i = 0; i < NBUCKET; i++) bucket[i] <= '0;
        samples <= '0;
      end else if (sample_valid) begin
        automatic int unsigned b = bucket_of(latency_ps);
        bucket[b] <= bucket[b] + 1'b1;
        samples   <= samples + 1'b1;
 
        // Walk the buckets accumulating counts until the requested
        // fraction is passed. Sixteen iterations, once per sample --
        // affordable, and it keeps the answer always current rather than
        // available only at a window boundary.
        begin
          automatic logic [CNT_W-1:0] acc = '0;
          automatic logic [CNT_W-1:0] target =
              ((samples + 1'b1) * CNT_W'(percentile_tenths)) / CNT_W'(1000);
          automatic int unsigned found = NBUCKET-1;
          for (int i = 0; i < NBUCKET; i++) begin
            acc = acc + ((i == b) ? (bucket[i] + 1'b1) : bucket[i]);
            if ((acc >= target) && (found == NBUCKET-1) && (i < NBUCKET-1))
              found = i;
          end
          percentile_bucket   <= 4'(found);
          percentile_upper_ps <= (40'(BASE_PS) << found);
          saturated           <= (found == NBUCKET-1);
          estimate_valid      <= 1'b1;
        end
      end
    end
  end
 
endmodule

// SYNTHESIZABLE INSTRUMENTATION.
//
// Isolates the queueing term and relates it to the utilisation that
// produced it, so the relationship of Section 3 becomes observable
// rather than assumed.
//
// Two things are reported and they answer different questions:
//
//   the queueing delay itself     -- what this frame experienced
//   the delay against utilisation -- whether the queue is behaving as a
//        queue should, or whether something else is wrong
//
// The second matters because a queueing delay far above what the
// utilisation predicts is NOT a load problem. It is a scheduling
// problem, a head-of-line block, or a drain that has stalled -- and the
// prediction is the only way to tell those from ordinary busyness.
module queueing_delay_isolator
  import latency_pkg::*;
#(
  parameter int unsigned CNT_W = 40,
  // Service time in picoseconds at this link's rate for a mean-size
  // frame. Supplied rather than computed: Chapter 8.1 owns it.
  parameter int unsigned SERVICE_PS = 12_304_000
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic             sample_valid,
  input  logic [39:0]      queueing_ps,
  // Utilisation in per mille, from Chapter 8.3's accounting.
  input  logic [CNT_W-1:0] utilisation_permille,
  input  logic [CNT_W-1:0] occupancy_frames,
 
  output logic             result_valid,
  // rho/(1-rho) multiplied by the service time. The delay a simple queue
  // at this utilisation would produce.
  output logic [CNT_W-1:0] predicted_ps,
  output logic [CNT_W-1:0] observed_ps,
 
  // Observed far above predicted: not a load problem.
  output logic             excess_beyond_model,
  output logic [CNT_W-1:0] c_excess,
  output logic [CNT_W-1:0] worst_ratio_permille,
 
  // The utilisation at which the queueing term first exceeded the sum of
  // the four constant terms. The single most useful operating figure in
  // this chapter: above it, the link's own load dominates its latency.
  input  logic [CNT_W-1:0] constant_terms_ps,
  output logic [CNT_W-1:0] crossover_utilisation_permille,
  output logic             crossover_seen
);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      result_valid <= 1'b0; predicted_ps <= '0; observed_ps <= '0;
      excess_beyond_model <= 1'b0; c_excess <= '0;
      worst_ratio_permille <= '0;
      crossover_utilisation_permille <= '0; crossover_seen <= 1'b0;
    end else begin
      result_valid        <= 1'b0;
      excess_beyond_model <= 1'b0;
 
      if (clear) begin
        c_excess <= '0;
        // The worst ratio and the crossover deliberately survive: both
        // characterise the link rather than the measurement window.
      end else if (sample_valid) begin
        // rho/(1-rho) in per mille, guarded against rho = 1 which the
        // model sends to infinity and the arithmetic sends to a divide
        // by zero. A saturated link reports the cap, honestly.
        automatic logic [CNT_W-1:0] denom =
            (utilisation_permille >= CNT_W'(1000)) ? CNT_W'(1)
                                                   : (CNT_W'(1000) - utilisation_permille);
        automatic logic [CNT_W-1:0] mult = (utilisation_permille * 1000) / denom;
        automatic logic [CNT_W-1:0] pred = (CNT_W'(SERVICE_PS) / 1000) * mult;
 
        predicted_ps <= pred;
        observed_ps  <= CNT_W'(queueing_ps);
        result_valid <= 1'b1;
 
        // Four times the prediction is well outside anything a simple
        // queue produces, so it points at a mechanism rather than at
        // load.
        if (CNT_W'(queueing_ps) > (pred * 4)) begin
          excess_beyond_model <= 1'b1;
          c_excess            <= c_excess + 1'b1;
        end
 
        if (pred != '0) begin
          automatic logic [CNT_W-1:0] r = (CNT_W'(queueing_ps) * 1000) / pred;
          if (r > worst_ratio_permille) worst_ratio_permille <= r;
        end
 
        // The operating point at which load starts to dominate.
        if (!crossover_seen && (CNT_W'(queueing_ps) > constant_terms_ps)) begin
          crossover_utilisation_permille <= utilisation_permille;
          crossover_seen                 <= 1'b1;
        end
      end
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// Reports which term dominates and, separately, whether the dominance is
// large enough to be a lever.
//
// The output is deliberately a pair, because "which term is largest" is
// not by itself actionable:
//
//   dominant at 700 per mille -> a lever. Halving it halves the total.
//   dominant at 260 per mille -> a report. Four terms of roughly equal
//        size have a largest one and no fix worth making.
//
// And the OWNER is reported alongside, because that is the field a
// finding gets routed on. A latency problem owned by "the load" goes to
// a different person from one owned by "the pipeline".
module latency_attribution_reporter
  import latency_pkg::*;
#(
  parameter int unsigned CNT_W = 40
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic             frame_valid,
  input  logic [39:0]      term_ps [TERMS],
  input  logic [39:0]      total_ps,
 
  output logic             report_valid,
  output lat_term_e        dominant_term,
  output logic [CNT_W-1:0] dominant_permille,
  output logic             dominant_is_lever,
 
  // How often each term was the dominant one. A distribution over
  // owners, which is more useful than any single frame's answer.
  output logic [CNT_W-1:0] dominance_count [TERMS],
  output lat_term_e        most_often_dominant,
  output logic [CNT_W-1:0] frames_reported
);
 
  localparam int unsigned LEVER_PERMILLE = 500;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      report_valid <= 1'b0; dominant_term <= LT_QUEUEING;
      dominant_permille <= '0; dominant_is_lever <= 1'b0;
      most_often_dominant <= LT_QUEUEING; frames_reported <= '0;
      for (int i = 0; i < TERMS; i++) dominance_count[i] <= '0;
    end else begin
      report_valid <= 1'b0;
 
      if (clear) begin
        frames_reported <= '0;
        for (int i = 0; i < TERMS; i++) dominance_count[i] <= '0;
      end else if (frame_valid) begin
        automatic logic [39:0] mx = '0;
        automatic int unsigned ix = 0;
        for (int i = 0; i < TERMS; i++)
          if (term_ps[i] > mx) begin mx = term_ps[i]; ix = i; end
 
        dominant_term     <= lat_term_e'(ix);
        dominant_permille <= (total_ps == '0) ? '0
                             : ((CNT_W'(mx) * 1000) / CNT_W'(total_ps));
        // A term is a lever only if halving it would visibly move the
        // total. Below half the budget it is a report.
        dominant_is_lever <= (total_ps != '0) &&
                             (((CNT_W'(mx) * 1000) / CNT_W'(total_ps))
                              >= CNT_W'(LEVER_PERMILLE));
        dominance_count[ix] <= dominance_count[ix] + 1'b1;
        frames_reported     <= frames_reported + 1'b1;
        report_valid        <= 1'b1;
 
        begin
          automatic logic [CNT_W-1:0] best = '0;
          automatic int unsigned bi = 0;
          for (int i = 0; i < TERMS; i++) begin
            automatic logic [CNT_W-1:0] cnt =
                (i == ix) ? (dominance_count[i] + 1'b1) : dominance_count[i];
            if (cnt > best) begin best = cnt; bi = i; end
          end
          most_often_dominant <= lat_term_e'(bi);
        end
      end
    end
  end
 
endmodule

// SYNTHESIZABLE MONITOR.
//
// Checks a latency budget stated as SEVERAL constraints rather than one,
// because a real requirement usually is:
//
//   a per-term ceiling  -- "processing must not exceed 2 us"
//   a total ceiling     -- "end to end under 100 us"
//   a TAIL ceiling      -- "99.9th percentile under 250 us"
//
// The third is the one a mean cannot verify (Section 5) and the one this
// chapter's rejected property tries to replace with a mean.
//
// And the module reports which constraint was violated, because the
// three point at different owners: a per-term violation is a design
// fault, a total violation may be a path problem, and a tail violation
// is almost always load.
module latency_budget_conformance
  import latency_pkg::*;
#(
  parameter int unsigned CNT_W = 40
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic        frame_valid,
  input  logic [39:0] term_ps [TERMS],
  input  logic [39:0] total_ps,
 
  input  logic        percentile_valid,
  input  logic [39:0] percentile_ps,
 
  // The three kinds of ceiling, independently configured.
  input  logic [39:0] term_limit_ps [TERMS],
  input  logic [39:0] total_limit_ps,
  input  logic [39:0] tail_limit_ps,
 
  output logic             term_violation,
  output lat_term_e        violating_term,
  output logic             total_violation,
  output logic             tail_violation,
 
  output logic [CNT_W-1:0] c_term_violations,
  output logic [CNT_W-1:0] c_total_violations,
  output logic [CNT_W-1:0] c_tail_violations,
 
  // Which constraint is TIGHTEST relative to what is observed. Reported
  // whether or not anything is violated, because it says where the
  // margin is thinnest before it runs out.
  output logic [1:0]       tightest_constraint,
  output logic [CNT_W-1:0] tightest_margin_permille
);
 
  localparam logic [1:0] TC_TERM  = 2'd0;
  localparam logic [1:0] TC_TOTAL = 2'd1;
  localparam logic [1:0] TC_TAIL  = 2'd2;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      term_violation <= 1'b0; violating_term <= LT_QUEUEING;
      total_violation <= 1'b0; tail_violation <= 1'b0;
      c_term_violations <= '0; c_total_violations <= '0; c_tail_violations <= '0;
      tightest_constraint <= TC_TOTAL; tightest_margin_permille <= '0;
    end else begin
      term_violation  <= 1'b0;
      total_violation <= 1'b0;
      tail_violation  <= 1'b0;
 
      if (clear) begin
        c_term_violations <= '0; c_total_violations <= '0; c_tail_violations <= '0;
      end
 
      if (frame_valid) begin
        automatic logic        tv = 1'b0;
        automatic int unsigned ti = 0;
        automatic logic [CNT_W-1:0] worst_use = '0;
        automatic logic [1:0]       worst_which = TC_TOTAL;
 
        for (int i = 0; i < TERMS; i++) begin
          if ((term_limit_ps[i] != '0) && (term_ps[i] > term_limit_ps[i])) begin
            tv = 1'b1; ti = i;
          end
          if (term_limit_ps[i] != '0) begin
            automatic logic [CNT_W-1:0] use =
                (CNT_W'(term_ps[i]) * 1000) / CNT_W'(term_limit_ps[i]);
            if (use > worst_use) begin worst_use = use; worst_which = TC_TERM; end
          end
        end
 
        if (tv) begin
          term_violation    <= 1'b1;
          violating_term    <= lat_term_e'(ti);
          c_term_violations <= c_term_violations + 1'b1;
        end
 
        if ((total_limit_ps != '0) && (total_ps > total_limit_ps)) begin
          total_violation    <= 1'b1;
          c_total_violations <= c_total_violations + 1'b1;
        end
        if (total_limit_ps != '0) begin
          automatic logic [CNT_W-1:0] use =
              (CNT_W'(total_ps) * 1000) / CNT_W'(total_limit_ps);
          if (use > worst_use) begin worst_use = use; worst_which = TC_TOTAL; end
        end
 
        tightest_constraint      <= worst_which;
        tightest_margin_permille <= (worst_use >= CNT_W'(1000)) ? '0
                                     : (CNT_W'(1000) - worst_use);
      end
 
      // The tail is checked on the ESTIMATE, not on individual frames --
      // a percentile is a property of a distribution and no single
      // sample can violate it.
      if (percentile_valid && (tail_limit_ps != '0) &&
          (percentile_ps > tail_limit_ps)) begin
        tail_violation    <= 1'b1;
        c_tail_violations <= c_tail_violations + 1'b1;
      end
    end
  end
 
endmodule

// ---------------------------------------------------------------------
// P1 -- CONSERVATION. The terms sum to the total. A decomposition whose
// parts do not add up is measuring overlapping intervals.
// ---------------------------------------------------------------------
property p_terms_sum_to_total;
  @(posedge clk) disable iff (!rst_n)
    frame_valid |-> (total_ps == (term_ps[LT_QUEUEING] + term_ps[LT_PROCESSING] +
                                  term_ps[LT_STORE_FORWARD] + term_ps[LT_SERIALIZATION] +
                                  term_ps[LT_PROPAGATION]));
endproperty
a_terms_sum_to_total: assert property (p_terms_sum_to_total)
  else $error("latency terms do not sum to the total -- intervals overlap or a gap exists");
 
// ---------------------------------------------------------------------
// P2 -- Stage boundaries are ordered. A timestamp out of order means an
// event fired in the wrong place.
// ---------------------------------------------------------------------
property p_boundaries_ordered;
  @(posedge clk) disable iff (!rst_n)
    frame_valid |-> ((t_deq_q >= t_arr_q) && (t_prc_q >= t_deq_q) && (t_txs_q >= t_prc_q));
endproperty
a_boundaries_ordered: assert property (p_boundaries_ordered);
 
// ---------------------------------------------------------------------
// P3 -- CROSS-CHECK. Measured serialization equals the value Chapter 8.1
// computes. The one term whose correct answer is known independently,
// and therefore the one that validates the instrument.
// ---------------------------------------------------------------------
property p_serialization_matches_computed;
  @(posedge clk) disable iff (!rst_n)
    frame_valid |-> (term_ps[LT_SERIALIZATION] inside
                     {[computed_serialization_ps - 40'd2000 :
                       computed_serialization_ps + 40'd2000]});
endproperty
a_serialization_matches_computed: assert property (p_serialization_matches_computed)
  else $error("measured serialization disagrees with arithmetic -- a boundary event is misplaced");
 
// ---------------------------------------------------------------------
// P4 -- Propagation is supplied, never measured. Written as an interface
// property: no measured interval may be attributed to it.
// ---------------------------------------------------------------------
property p_propagation_is_supplied;
  @(posedge clk) disable iff (!rst_n)
    frame_valid |-> (term_ps[LT_PROPAGATION] == $past(propagation_ps));
endproperty
a_propagation_is_supplied: assert property (p_propagation_is_supplied);
 
// ---------------------------------------------------------------------
// P5 -- The four constant terms do not vary with utilisation. The
// chapter's central claim, checkable directly.
// ---------------------------------------------------------------------
property p_constants_are_constant;
  @(posedge clk) disable iff (!rst_n)
    (frame_valid && $stable(frame_octets) && !$stable(utilisation_permille))
      |-> ($stable(term_ps[LT_SERIALIZATION]) && $stable(term_ps[LT_PROPAGATION]));
endproperty
a_constants_are_constant: assert property (p_constants_are_constant);
 
// ---------------------------------------------------------------------
// P6 -- Extremes survive a counter clear: the worst each term has been
// is a design input, not a measurement window.
// ---------------------------------------------------------------------
property p_worst_survives_clear;
  @(posedge clk) disable iff (!rst_n)
    clear |=> ($stable(worst_ps[LT_QUEUEING]) && $stable(worst_ps[LT_PROCESSING]));
endproperty
a_worst_survives_clear: assert property (p_worst_survives_clear);
 
// ---------------------------------------------------------------------
// P7 -- Every sample lands in exactly one bucket.
// ---------------------------------------------------------------------
property p_one_bucket_per_sample;
  @(posedge clk) disable iff (!rst_n)
    sample_valid |=> (bucket_sum == $past(bucket_sum) + 1);
endproperty
a_one_bucket_per_sample: assert property (p_one_bucket_per_sample);
 
// ---------------------------------------------------------------------
// P8 -- Bucket edges are monotonically increasing. A histogram whose
// edges are not ordered produces percentiles that are not percentiles.
// ---------------------------------------------------------------------
// synopsys translate_off
a_bucket_edges_monotonic: assert final
  ((40'(BASE_PS) << 1) > 40'(BASE_PS) &&
   (40'(BASE_PS) << (NBUCKET-1)) > (40'(BASE_PS) << (NBUCKET-2)))
  else $fatal(1, "histogram bucket edges are not monotonic");
// synopsys translate_on
 
// ---------------------------------------------------------------------
// P9 -- THE HONESTY PROPERTY. A percentile in the top bucket is a lower
// bound, and the design says so rather than reporting the edge as an
// answer it does not have.
// ---------------------------------------------------------------------
property p_saturation_reported;
  @(posedge clk) disable iff (!rst_n)
    (estimate_valid && (percentile_bucket == 4'(NBUCKET-1))) |-> saturated;
endproperty
a_saturation_reported: assert property (p_saturation_reported);
 
// ---------------------------------------------------------------------
// P10 -- The percentile estimate is monotonic in the requested
// percentile: a higher percentile is never a smaller value.
// ---------------------------------------------------------------------
property p_percentile_monotonic;
  @(posedge clk) disable iff (!rst_n)
    (estimate_valid && (percentile_tenths > $past(percentile_tenths)) &&
     $stable(samples))
      |-> (percentile_upper_ps >= $past(percentile_upper_ps));
endproperty
a_percentile_monotonic: assert property (p_percentile_monotonic);
 
// ---------------------------------------------------------------------
// P11 -- The queueing prediction is guarded against a saturated link.
// rho = 1 sends the model to infinity and the arithmetic to a divide by
// zero; the design must report the cap rather than fault.
// ---------------------------------------------------------------------
property p_prediction_guarded;
  @(posedge clk) disable iff (!rst_n)
    (result_valid && ($past(utilisation_permille) >= CNT_W'(1000)))
      |-> !$isunknown(predicted_ps);
endproperty
a_prediction_guarded: assert property (p_prediction_guarded);
 
// ---------------------------------------------------------------------
// P12 -- excess_beyond_model requires a prediction to compare against.
// ---------------------------------------------------------------------
property p_excess_needs_prediction;
  @(posedge clk) disable iff (!rst_n)
    excess_beyond_model |-> (predicted_ps != '0);
endproperty
a_excess_needs_prediction: assert property (p_excess_needs_prediction);
 
// ---------------------------------------------------------------------
// P13 -- The crossover is captured once and survives a clear: it is an
// operating characteristic of the link.
// ---------------------------------------------------------------------
property p_crossover_stable;
  @(posedge clk) disable iff (!rst_n)
    crossover_seen |=> $stable(crossover_utilisation_permille);
endproperty
a_crossover_stable: assert property (p_crossover_stable);
 
// ---------------------------------------------------------------------
// P14 -- The dominant term really is the largest.
// ---------------------------------------------------------------------
property p_dominant_is_largest;
  @(posedge clk) disable iff (!rst_n)
    report_valid |-> (term_ps[dominant_term] == max_term_ps);
endproperty
a_dominant_is_largest: assert property (p_dominant_is_largest);
 
// ---------------------------------------------------------------------
// P15 -- A term is only a lever when it is at least half the budget.
// Reporting an identity without a fraction produces engineers chasing
// terms that cannot pay.
// ---------------------------------------------------------------------
property p_lever_requires_majority;
  @(posedge clk) disable iff (!rst_n)
    dominant_is_lever |-> (dominant_permille >= CNT_W'(LEVER_PERMILLE));
endproperty
a_lever_requires_majority: assert property (p_lever_requires_majority);
 
// ---------------------------------------------------------------------
// P16 -- THE TAIL CONSTRAINT IS CHECKED ON THE ESTIMATE. A percentile is
// a property of a distribution, so no individual frame can violate it.
// ---------------------------------------------------------------------
property p_tail_checked_on_estimate;
  @(posedge clk) disable iff (!rst_n)
    tail_violation |-> $past(percentile_valid);
endproperty
a_tail_checked_on_estimate: assert property (p_tail_checked_on_estimate)
  else $error("a tail limit was violated by a single frame -- a percentile is not a per-frame bound");
 
// ---------------------------------------------------------------------
// P17 -- The tightest constraint is reported whether or not anything is
// violated, which is what makes it a planning output.
// ---------------------------------------------------------------------
property p_tightest_always_reported;
  @(posedge clk) disable iff (!rst_n)
    frame_valid |=> (tightest_margin_permille <= CNT_W'(1000));
endproperty
a_tightest_always_reported: assert property (p_tightest_always_reported);
 
// ---------------------------------------------------------------------
// P18 -- COVERAGE. Each term dominant at least once, and a saturated
// percentile estimate.
// ---------------------------------------------------------------------
c_dom_queueing:   cover property (@(posedge clk) disable iff (!rst_n) (report_valid && dominant_term == LT_QUEUEING));
c_dom_processing: cover property (@(posedge clk) disable iff (!rst_n) (report_valid && dominant_term == LT_PROCESSING));
c_dom_sf:         cover property (@(posedge clk) disable iff (!rst_n) (report_valid && dominant_term == LT_STORE_FORWARD));
c_percentile_sat: cover property (@(posedge clk) disable iff (!rst_n) saturated);
c_excess_seen:    cover property (@(posedge clk) disable iff (!rst_n) excess_beyond_model);