Architecture and Integration Review

// ---------------------------------------------------------------------
// archreview_pkg -- the reference values Module 25 and Module 23
// derived, and the shape a review item must have to be checkable.
//
// Unit: Chapter 23.3 Section 2's bitcell equivalent.
//   1 BCE = 0.35 GE = one bit of usable on-die SRAM
//   1 flip-flop = 20 BCE
//   Chapter 19.7 Section 19's MAC receive datapath = 283 320 BCE
//   Chapter 23.3's 64-port switch = 5.62e8 BCE
// ---------------------------------------------------------------------
package archreview_pkg;

  localparam int unsigned DATAPATH_BCE  = 283_320;
  localparam int unsigned BCE_PER_FLOP  = 20;
  localparam int unsigned SWITCH_BCE_E4 = 56_200;      // 5.62e8 / 1e4

  localparam int unsigned ITEM_COUNT = 20;

  // ---- an item's four parts, Section 1's callout ------------------------
  typedef enum logic [1:0] {
    ITEM_ADJECTIVE  = 2'd0,   // a quality: no failing value
    ITEM_VALUED     = 2'd1,   // a number, no threshold
    ITEM_THRESHOLDED= 2'd2,   // a number and a bound
    ITEM_AUDITED    = 2'd3    // and a witness who is not its author
  } itemkind_e;

  typedef enum logic [1:0] {
    CLAIM_UNFALSIFIABLE = 2'd0,
    CLAIM_SELF_WITNESSED= 2'd1,
    CLAIM_AUDITABLE     = 2'd2
  } claimstate_e;

  // ---- the reference design's derived quantities ------------------------
  localparam int unsigned REF_PORTS        = 64;
  localparam int unsigned REF_GBPS         = 100;
  localparam int unsigned REF_CORE_MHZ     = 1_200;
  localparam int unsigned REF_AGG_PPS_K    = 9_524_000;   // Chapter 23.3 §2
  localparam int unsigned REF_PIPE_WIDTH   = 8;
  localparam int unsigned REF_TBL_ENTRIES  = 128 * 1024;
  localparam int unsigned REF_TBL_WAYS     = 4;
  localparam int unsigned REF_EFF_CAP_PCT  = 80;          // Chapter 12.5 §9
  localparam int unsigned REF_BUFFER_MB    = 64;          // Chapter 23.3 §9
  localparam int unsigned REF_PREFETCH     = 149;         // Chapter 23.4 §7
  localparam int unsigned REF_TAGS         = 196;         // Chapter 24.1 §4
  localparam int unsigned REF_MISS_CLIFF   = 39;          // Chapter 23.4 §10
  localparam int unsigned REF_PARSE_OCTETS = 22;          // Chapter 25.1 §3

  // ---- derived: an item's state from its three flags --------------------
  function automatic claimstate_e claim_state(bit has_value,
                                              bit has_threshold,
                                              bit has_witness);
    if (!has_value || !has_threshold) return CLAIM_UNFALSIFIABLE;
    if (!has_witness)                 return CLAIM_SELF_WITNESSED;
    return CLAIM_AUDITABLE;
  endfunction

  function automatic itemkind_e item_kind(bit has_value,
                                          bit has_threshold,
                                          bit has_witness);
    if (!has_value)     return ITEM_ADJECTIVE;
    if (!has_threshold) return ITEM_VALUED;
    if (!has_witness)   return ITEM_THRESHOLDED;
    return ITEM_AUDITED;
  endfunction

  // ---- derived: readiness ------------------------------------------------
  function automatic int unsigned readiness_ppm(int unsigned produced,
                                                int unsigned total);
    return (total == 0) ? 0 : ((produced * 1_000_000) / total);
  endfunction

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

  function automatic int unsigned switch_share_x100(int unsigned bce_e2);
    return (bce_e2 * 10_000) / (SWITCH_BCE_E4 * 100);
  endfunction

endpackage

// ---------------------------------------------------------------------
// review_item_model -- one row of Section 2's table, classified by
// whether it can fail.
//
// The output that matters is can_fail, which is low for an item that
// names a quality -- and Section 20's rejected property is the
// conjunction over a review made of them.
// ---------------------------------------------------------------------
module review_item_model
  import archreview_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,

  input  logic        eval,
  input  logic        has_value,
  input  logic        has_threshold,
  input  logic        has_witness,
  input  logic [31:0] value,
  input  logic [31:0] threshold,
  input  logic        threshold_is_upper_bound,
  input  logic [15:0] deriving_chapter_x10,

  output logic  [1:0] kind,
  output logic  [1:0] state,
  output logic        can_fail,
  output logic        item_passes,
  output logic        item_fails,
  output logic        provenance_recorded,
  output logic        is_decoration,
  output logic [31:0] c_items_evaluated,
  output logic [31:0] c_decoration
);
  always_comb begin
    kind  = 2'(item_kind(has_value, has_threshold, has_witness));
    state = 2'(claim_state(has_value, has_threshold, has_witness));

    // THE property of a usable item.
    can_fail = has_value && has_threshold;

    item_fails = can_fail && (threshold_is_upper_bound
                              ? (value > threshold) : (value < threshold));
    item_passes = can_fail && !item_fails;

    // Part four: somebody can check the number.
    provenance_recorded = (deriving_chapter_x10 != 16'd0);

    // An item that cannot fail and has no provenance is decoration.
    is_decoration = !can_fail;
  end

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

// ---------------------------------------------------------------------
// readiness_model -- how much of a review is load-bearing, and what a
// verdict is a conjunction over.
//
// The output that matters is verdict_information_bits, which is the
// count of items that could have failed -- and it is what a pass
// should be reported against.
// ---------------------------------------------------------------------
module readiness_model
  import archreview_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,
  input  logic        clear,

  input  logic        item_valid,
  input  logic  [1:0] item_kind_i,
  input  logic        item_passed,
  input  logic        item_failed,
  input  logic        value_is_reference_copy,

  output logic [15:0] c_items,
  output logic [15:0] c_adjectives,
  output logic [15:0] c_valued,
  output logic [15:0] c_thresholded,
  output logic [15:0] c_audited,
  output logic [15:0] c_can_fail,
  output logic [15:0] c_passed,
  output logic [15:0] c_failed,
  output logic [15:0] c_reference_copies,
  output logic [31:0] readiness_ppm_o,
  output logic [15:0] verdict_information_bits,
  output logic        verdict,
  output logic        verdict_is_diluted
);
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n || clear) begin
      c_items <= '0; c_adjectives <= '0; c_valued <= '0;
      c_thresholded <= '0; c_audited <= '0; c_can_fail <= '0;
      c_passed <= '0; c_failed <= '0; c_reference_copies <= '0;
    end else if (item_valid) begin
      c_items <= c_items + 16'd1;
      case (item_kind_i)
        2'(ITEM_ADJECTIVE):   c_adjectives  <= c_adjectives + 16'd1;
        2'(ITEM_VALUED):      c_valued      <= c_valued + 16'd1;
        2'(ITEM_THRESHOLDED): c_thresholded <= c_thresholded + 16'd1;
        default:              c_audited     <= c_audited + 16'd1;
      endcase
      if (item_kind_i >= 2'(ITEM_THRESHOLDED)) c_can_fail <= c_can_fail + 16'd1;
      if (item_passed) c_passed <= c_passed + 16'd1;
      if (item_failed) c_failed <= c_failed + 16'd1;
      if (value_is_reference_copy)
        c_reference_copies <= c_reference_copies + 16'd1;
    end
  end

  always_comb begin
    readiness_ppm_o = 32'(readiness_ppm(int'(c_items) - int'(c_adjectives),
                                        int'(c_items)));

    // THE number a pass should be reported against.
    verdict_information_bits = c_can_fail;

    // A review's verdict is the conjunction over its items.
    verdict = (c_failed == 16'd0);

    // And it is diluted whenever some items could not have failed.
    verdict_is_diluted = (c_can_fail < c_items);
  end
endmodule

// ---------------------------------------------------------------------
// area_reconciler -- the sum of a design's claimed structures against
// both a budget and an independent reference bill.
//
// The output that matters is below_reference_estimate, because a total
// that is too SMALL is the omission a block-by-block review cannot see.
// ---------------------------------------------------------------------
module area_reconciler
  import archreview_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,
  input  logic        clear,

  input  logic        entry_valid,
  input  logic [31:0] entry_bce_e2,          // BCE / 100
  input  logic        entry_is_diagnostic,
  input  logic [31:0] budget_bce_e2,
  input  logic [31:0] reference_bce_e2,
  input  logic [15:0] tolerance_pct,

  output logic [31:0] total_bce_e2,
  output logic [31:0] diagnostic_bce_e2,
  output logic [15:0] entries_counted,
  output logic [31:0] total_dp_milli,
  output logic [15:0] diagnostic_share_x100,
  output logic        exceeds_budget,
  output logic        below_reference_estimate,
  output logic [31:0] shortfall_bce_e2,
  output logic        reconciles,
  output logic [31:0] c_reconciliations
);
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n || clear) begin
      total_bce_e2 <= '0; diagnostic_bce_e2 <= '0; entries_counted <= '0;
      c_reconciliations <= '0;
    end else if (entry_valid) begin
      total_bce_e2    <= total_bce_e2 + entry_bce_e2;
      entries_counted <= entries_counted + 16'd1;
      if (entry_is_diagnostic)
        diagnostic_bce_e2 <= diagnostic_bce_e2 + entry_bce_e2;
      c_reconciliations <= c_reconciliations + 32'd1;
    end
  end

  always_comb begin
    total_dp_milli = 32'(datapaths_milli(total_bce_e2 * 32'd100));

    diagnostic_share_x100 = (total_bce_e2 == 0) ? 16'd0
                          : 16'((diagnostic_bce_e2 * 32'd10_000)
                                / total_bce_e2);

    exceeds_budget = (total_bce_e2 > budget_bce_e2);

    // THE check a block-by-block review cannot perform: is the total
    // implausibly SMALL against an independent bill of materials?
    shortfall_bce_e2 = (reference_bce_e2 > total_bce_e2)
                     ? (reference_bce_e2 - total_bce_e2) : 32'd0;

    below_reference_estimate =
      (reference_bce_e2 != 32'd0)
      && ((shortfall_bce_e2 * 32'd100)
          > (reference_bce_e2 * 32'(tolerance_pct)));

    reconciles = !exceeds_budget && !below_reference_estimate;
  end
endmodule

// ---------------------------------------------------------------------
// latency_reconciler -- a path's latency terms summed, with the share
// each party owns and the congested case as a separate column.
//
// The output that matters is design_owned_share_ppm, which is 88 000
// uncongested and near a million congested -- the same design, two
// completely different answers to "is this our problem".
// ---------------------------------------------------------------------
module latency_reconciler
  import archreview_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,
  input  logic        clear,

  input  logic        term_valid,
  input  logic [31:0] term_ns_x100,
  input  logic        term_is_design_owned,
  input  logic [15:0] hops,
  input  logic [31:0] buffer_max_queue_ns_x100,
  input  logic [31:0] budget_ns_x100,
  input  logic [15:0] specified_percentile,

  output logic [31:0] hop_total_ns_x100,
  output logic [31:0] design_owned_ns_x100,
  output logic [31:0] path_total_ns_x100,
  output logic [31:0] congested_total_ns_x100,
  output logic [31:0] design_owned_share_ppm,
  output logic [31:0] congested_ratio_x10,
  output logic        within_budget,
  output logic        percentile_specified,
  output logic        budget_is_uncongested_only,
  output logic [31:0] c_terms
);
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n || clear) begin
      hop_total_ns_x100 <= '0; design_owned_ns_x100 <= '0; c_terms <= '0;
    end else if (term_valid) begin
      hop_total_ns_x100 <= hop_total_ns_x100 + term_ns_x100;
      if (term_is_design_owned)
        design_owned_ns_x100 <= design_owned_ns_x100 + term_ns_x100;
      c_terms <= c_terms + 32'd1;
    end
  end

  always_comb begin
    path_total_ns_x100 = hop_total_ns_x100 * 32'(hops);

    // Chapter 23.3 Section 9: one congestion event dwarfs the structure.
    congested_total_ns_x100 = path_total_ns_x100 + buffer_max_queue_ns_x100;

    design_owned_share_ppm = (hop_total_ns_x100 == 0) ? 32'd0
                           : ((design_owned_ns_x100 * 1_000_000)
                              / hop_total_ns_x100);

    congested_ratio_x10 = (path_total_ns_x100 == 0) ? 32'd0
                        : ((congested_total_ns_x100 * 32'd10)
                           / path_total_ns_x100);

    within_budget = (path_total_ns_x100 <= budget_ns_x100);

    // THE two fields a review must record and usually does not.
    percentile_specified       = (specified_percentile != 16'd0);
    budget_is_uncongested_only = !percentile_specified;
  end
endmodule

// ---------------------------------------------------------------------
// claims_auditor -- the three-part test on each item, and the tally
// across a review.
//
// The output that matters is auditable_share_ppm, because a review's
// credibility is the share of its items a reader could have disputed.
// ---------------------------------------------------------------------
module claims_auditor
  import archreview_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,
  input  logic        clear,

  input  logic        item_valid,
  input  logic        has_value,
  input  logic        has_threshold,
  input  logic        has_witness,
  input  logic        witness_saw_design,
  input  logic        witness_is_citation,
  input  logic        threshold_declared_unknown,

  output logic  [1:0] state,
  output logic        witness_is_independent,
  output logic [15:0] c_items,
  output logic [15:0] c_unfalsifiable,
  output logic [15:0] c_self_witnessed,
  output logic [15:0] c_auditable,
  output logic [15:0] c_threshold_unknown,
  output logic [31:0] auditable_share_ppm,
  output logic        review_is_auditable,
  output logic        open_questions_visible
);
  always_comb begin
    // Chapter 24.3 Section 13's two conditions.
    witness_is_independent = has_witness
                          && (witness_is_citation || !witness_saw_design);

    state = 2'(claim_state(has_value, has_threshold, witness_is_independent));
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n || clear) begin
      c_items <= '0; c_unfalsifiable <= '0; c_self_witnessed <= '0;
      c_auditable <= '0; c_threshold_unknown <= '0;
    end else if (item_valid) begin
      c_items <= c_items + 16'd1;
      case (state)
        2'(CLAIM_UNFALSIFIABLE): c_unfalsifiable  <= c_unfalsifiable + 16'd1;
        2'(CLAIM_SELF_WITNESSED):c_self_witnessed <= c_self_witnessed + 16'd1;
        default:                 c_auditable      <= c_auditable + 16'd1;
      endcase
      if (threshold_declared_unknown)
        c_threshold_unknown <= c_threshold_unknown + 16'd1;
    end
  end

  always_comb begin
    auditable_share_ppm = (c_items == 16'd0) ? 32'd0
                        : ((32'(c_auditable) * 1_000_000) / 32'(c_items));

    review_is_auditable = (c_unfalsifiable == 16'd0)
                       && (c_self_witnessed == 16'd0);

    // Section 10's callout: an item that declares its threshold unknown
    // is honest and names a person to ask.
    open_questions_visible = (c_threshold_unknown != 16'd0)
                          || (c_unfalsifiable == 16'd0);
  end
endmodule

// ---------------------------------------------------------------------
// threshold_binder -- where each threshold comes from, and what happens
// to the ones nobody in the room owns.
//
// The output that matters is becomes_a_default, which is high for every
// deferred threshold that the design hard-codes -- and Section 12's
// callout lists four that did.
// ---------------------------------------------------------------------
module threshold_binder
  import archreview_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,
  input  logic        clear,

  input  logic        item_valid,
  input  logic        threshold_is_derived,
  input  logic        threshold_is_structural,
  input  logic        threshold_is_environmental,
  input  logic        owner_named,
  input  logic        design_exposes_parameter,
  input  logic        design_hardcodes_value,

  output logic  [1:0] outcome,
  output logic        deferred,
  output logic        becomes_a_default,
  output logic        deferred_correctly,
  output logic [15:0] c_derived,
  output logic [15:0] c_structural,
  output logic [15:0] c_environmental,
  output logic [15:0] c_deferred,
  output logic [15:0] c_silent_defaults,
  output logic [15:0] c_exposed,
  output logic [31:0] exposure_share_ppm
);
  // outcome: 0 pass, 1 fail, 2 unknown, 3 deferred.
  always_comb begin
    // Only an environmental threshold can be deferred; the other two
    // are the design's own to produce.
    deferred = threshold_is_environmental && !owner_named;

    outcome = deferred ? 2'd3 : 2'd0;

    // THE failure. A deferred threshold that the design hard-codes
    // becomes a deployment decision made at architecture time.
    becomes_a_default = threshold_is_environmental && design_hardcodes_value
                     && !design_exposes_parameter;

    // And the correct handling: expose it and name the owner.
    deferred_correctly = threshold_is_environmental
                      && design_exposes_parameter && owner_named;

    exposure_share_ppm = (c_environmental == 16'd0) ? 32'd0
                       : ((32'(c_exposed) * 1_000_000) / 32'(c_environmental));
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n || clear) begin
      c_derived <= '0; c_structural <= '0; c_environmental <= '0;
      c_deferred <= '0; c_silent_defaults <= '0; c_exposed <= '0;
    end else if (item_valid) begin
      if (threshold_is_derived)      c_derived       <= c_derived + 16'd1;
      if (threshold_is_structural)   c_structural    <= c_structural + 16'd1;
      if (threshold_is_environmental)c_environmental <= c_environmental + 16'd1;
      if (deferred)                  c_deferred      <= c_deferred + 16'd1;
      if (becomes_a_default)         c_silent_defaults <= c_silent_defaults + 16'd1;
      if (design_exposes_parameter)  c_exposed       <= c_exposed + 16'd1;
    end
  end
endmodule

// ---------------------------------------------------------------------
// review_telemetry -- what a review should report about itself, so a
// reader can weigh the verdict.
//
// Design rule: every number here is about the REVIEW rather than about
// the design, because a verdict's credibility is a property of the
// instrument that produced it.
// ---------------------------------------------------------------------
module review_telemetry
  import archreview_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,
  input  logic        clear,

  input  logic        item_valid,
  input  logic        can_fail_i,
  input  logic        passed_i,
  input  logic        failed_i,
  input  logic        deferred_i,
  input  logic        auditable_i,
  input  logic        reference_copy_i,
  input  logic        exposed_i,
  input  logic [15:0] milestone_id,

  output logic [15:0] c_items,
  output logic [15:0] c_can_fail,
  output logic [15:0] c_passed,
  output logic [15:0] c_failed,
  output logic [15:0] c_deferred,
  output logic [15:0] c_auditable,
  output logic [15:0] c_reference_copies,
  output logic [15:0] c_exposed,
  output logic [31:0] readiness_ppm_o,
  output logic [31:0] auditable_ppm,
  output logic [31:0] dilution_ppm,
  output logic        verdict_o,
  output logic        verdict_is_reportable
);
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n || clear) begin
      c_items <= '0; c_can_fail <= '0; c_passed <= '0; c_failed <= '0;
      c_deferred <= '0; c_auditable <= '0; c_reference_copies <= '0;
      c_exposed <= '0;
    end else if (item_valid) begin
      c_items <= c_items + 16'd1;
      if (can_fail_i)       c_can_fail         <= c_can_fail + 16'd1;
      if (passed_i)         c_passed           <= c_passed + 16'd1;
      if (failed_i)         c_failed           <= c_failed + 16'd1;
      if (deferred_i)       c_deferred         <= c_deferred + 16'd1;
      if (auditable_i)      c_auditable        <= c_auditable + 16'd1;
      if (reference_copy_i) c_reference_copies <= c_reference_copies + 16'd1;
      if (exposed_i)        c_exposed          <= c_exposed + 16'd1;
    end
  end

  always_comb begin
    readiness_ppm_o = 32'(readiness_ppm(int'(c_can_fail), int'(c_items)));

    auditable_ppm = (c_items == 16'd0) ? 32'd0
                  : ((32'(c_auditable) * 1_000_000) / 32'(c_items));

    // Section 5: how much of the verdict was not load-bearing.
    dilution_ppm = (c_items == 16'd0) ? 32'd0
                 : (((32'(c_items) - 32'(c_can_fail)) * 1_000_000)
                    / 32'(c_items));

    verdict_o = (c_failed == 16'd0);

    // THE rule: a verdict is reportable only with its denominator.
    verdict_is_reportable = (c_can_fail != 16'd0);
  end
endmodule

// ---------------------------------------------------------------------
// review_conformance -- the checks that hold a review to being an
// instrument rather than a ceremony.
//
// Every check here is about the review's own structure. There is no
// check that the design is good, because that is what the items are.
// ---------------------------------------------------------------------
module review_conformance
  import archreview_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,

  input  logic [15:0] items_total,
  input  logic [15:0] items_can_fail,
  input  logic [15:0] items_auditable,
  input  logic [15:0] items_unfalsifiable,
  input  logic        verdict_reported_with_denominator,
  input  logic        reconciled_against_reference,
  input  logic        reconciled_against_budget,
  input  logic [15:0] environmental_thresholds,
  input  logic [15:0] environmental_exposed,
  input  logic        latency_percentile_specified,

  output logic        v_no_failable_items,
  output logic        v_verdict_without_denominator,
  output logic        v_unfalsifiable_present,
  output logic        v_no_reference_bill,
  output logic        v_threshold_hardcoded,
  output logic        v_latency_uncongested_only,
  output logic  [5:0] violations,
  output logic        conformant
);
  always_comb begin
    // 1. Section 4's last row: a review with nothing that can fail.
    v_no_failable_items = (items_can_fail == 16'd0) && (items_total != 16'd0);

    // 2. Prohibition 2 -- class 120 in a management report.
    v_verdict_without_denominator = !verdict_reported_with_denominator;

    // 3. Section 10 -- an item nobody could dispute.
    v_unfalsifiable_present = (items_unfalsifiable != 16'd0);

    // 4. Section 6 -- a budget catches excess, a bill catches omission.
    v_no_reference_bill = reconciled_against_budget
                       && !reconciled_against_reference;

    // 5. Section 12 -- a deferred threshold that became a default.
    v_threshold_hardcoded = (environmental_exposed < environmental_thresholds);

    // 6. Section 8 -- a budget for a network with no traffic.
    v_latency_uncongested_only = !latency_percentile_specified;

    violations = { v_latency_uncongested_only, v_threshold_hardcoded,
                   v_no_reference_bill, v_unfalsifiable_present,
                   v_verdict_without_denominator, v_no_failable_items };
    conformant = (violations == 6'b000000);
  end
endmodule

// A1. An item can fail only with a value and a threshold.
p_it_can_fail: assert property (@(posedge clk) disable iff (!rst_n)
  (can_fail == (has_value && has_threshold)));

// A2. An item with no value is an adjective.
p_it_adjective: assert property (@(posedge clk) disable iff (!rst_n)
  !has_value |-> (kind == 2'(ITEM_ADJECTIVE)));

// A3. A value with no threshold is unfalsifiable.
p_it_unfalsifiable: assert property (@(posedge clk) disable iff (!rst_n)
  (has_value && !has_threshold) |-> (state == 2'(CLAIM_UNFALSIFIABLE)));

// A4. Both plus no witness is self-witnessed.
p_it_self: assert property (@(posedge clk) disable iff (!rst_n)
  (has_value && has_threshold && !has_witness)
    |-> (state == 2'(CLAIM_SELF_WITNESSED)));

// A5. Pass and fail are exclusive and need can_fail.
p_it_exclusive: assert property (@(posedge clk) disable iff (!rst_n)
  !(item_passes && item_fails));

// A6. Neither is asserted without can_fail.
p_it_gated: assert property (@(posedge clk) disable iff (!rst_n)
  !can_fail |-> (!item_passes && !item_fails));

// A7. A lower-bound item fails below its threshold.
p_it_lower: assert property (@(posedge clk) disable iff (!rst_n)
  (can_fail && !threshold_is_upper_bound && (value < threshold)) |-> item_fails);

// A8. Decoration is exactly the items that cannot fail.
p_it_decoration: assert property (@(posedge clk) disable iff (!rst_n)
  (is_decoration == !can_fail));

// A9. Provenance is recorded when a chapter is named.
p_it_provenance: assert property (@(posedge clk) disable iff (!rst_n)
  (deriving_chapter_x10 != 16'd0) |-> provenance_recorded);

// B1. Readiness is the share of items that are not adjectives.
p_rd_readiness: assert property (@(posedge clk) disable iff (!rst_n)
  (c_items != 16'd0) |-> (readiness_ppm_o ==
    32'(readiness_ppm(int'(c_items) - int'(c_adjectives), int'(c_items)))));

// B2. The verdict's information content is the failable count.
p_rd_information: assert property (@(posedge clk) disable iff (!rst_n)
  (verdict_information_bits == c_can_fail));

// B3. A verdict is diluted when some items cannot fail.
p_rd_diluted: assert property (@(posedge clk) disable iff (!rst_n)
  (c_can_fail < c_items) |-> verdict_is_diluted);

// B4. The kinds partition the items.
p_rd_partition: assert property (@(posedge clk) disable iff (!rst_n)
  (c_items == c_adjectives + c_valued + c_thresholded + c_audited));

// B5. Failable items are the thresholded and audited ones.
p_rd_failable: assert property (@(posedge clk) disable iff (!rst_n)
  (c_can_fail == c_thresholded + c_audited));

// B6. A passing verdict means no item failed.
p_rd_verdict: assert property (@(posedge clk) disable iff (!rst_n)
  verdict |-> (c_failed == 16'd0));

// B7. Passes and failures never exceed the failable count.
p_rd_bounded: assert property (@(posedge clk) disable iff (!rst_n)
  ((c_passed + c_failed) <= c_can_fail));

// B8. A reference copy is counted separately from an adjective.
p_rd_copies: assert property (@(posedge clk) disable iff (!rst_n)
  (item_valid && value_is_reference_copy) |=>
    (c_reference_copies == $past(c_reference_copies) + 16'd1));

// C1. The total is the sum of the entries.
p_ar_sum: assert property (@(posedge clk) disable iff (!rst_n)
  entry_valid |=> (total_bce_e2 == $past(total_bce_e2) + $past(entry_bce_e2)));

// C2. Diagnostics are a subset of the total.
p_ar_subset: assert property (@(posedge clk) disable iff (!rst_n)
  (diagnostic_bce_e2 <= total_bce_e2));

// C3. Exceeding the budget is reported.
p_ar_budget: assert property (@(posedge clk) disable iff (!rst_n)
  (total_bce_e2 > budget_bce_e2) |-> exceeds_budget);

// C4. THE check a per-block review cannot make.
p_ar_omission: assert property (@(posedge clk) disable iff (!rst_n)
  ((reference_bce_e2 != 32'd0) &&
   ((shortfall_bce_e2 * 32'd100) > (reference_bce_e2 * 32'(tolerance_pct))))
    |-> below_reference_estimate);

// C5. Reconciliation needs both checks to pass.
p_ar_reconciles: assert property (@(posedge clk) disable iff (!rst_n)
  reconciles |-> (!exceeds_budget && !below_reference_estimate));

// C6. A shortfall is zero when the total meets the reference.
p_ar_no_shortfall: assert property (@(posedge clk) disable iff (!rst_n)
  (total_bce_e2 >= reference_bce_e2) |-> (shortfall_bce_e2 == 32'd0));

// C7. The diagnostic share is bounded.
p_ar_share: assert property (@(posedge clk) disable iff (!rst_n)
  (diagnostic_share_x100 <= 16'd10_000));

// C8. Entries are counted.
p_ar_counted: assert property (@(posedge clk) disable iff (!rst_n)
  entry_valid |=> (entries_counted == $past(entries_counted) + 16'd1));

// C9. A thirteen-entry bill exceeds a five-entry one.
p_ar_completeness: assert property (@(posedge clk) disable iff (!rst_n)
  (entries_counted >= 16'd13) |-> !below_reference_estimate);

// D1. The path total is the hop total times the hops.
p_lt_path: assert property (@(posedge clk) disable iff (!rst_n)
  (path_total_ns_x100 == hop_total_ns_x100 * 32'(hops)));

// D2. The congested total includes the buffer's maximum.
p_lt_congested: assert property (@(posedge clk) disable iff (!rst_n)
  (congested_total_ns_x100 == path_total_ns_x100 + buffer_max_queue_ns_x100));

// D3. The design owns a minority uncongested.
p_lt_minority: assert property (@(posedge clk) disable iff (!rst_n)
  (c_terms >= 32'd7) |-> (design_owned_share_ppm < 32'd150_000));

// D4. And the congested case dwarfs the structural one.
p_lt_dwarfs: assert property (@(posedge clk) disable iff (!rst_n)
  (buffer_max_queue_ns_x100 > path_total_ns_x100) |->
    (congested_ratio_x10 > 32'd20));

// D5. A budget with no percentile is uncongested only.
p_lt_percentile: assert property (@(posedge clk) disable iff (!rst_n)
  (budget_is_uncongested_only == !percentile_specified));

// D6. Design-owned terms are a subset of the total.
p_lt_subset: assert property (@(posedge clk) disable iff (!rst_n)
  (design_owned_ns_x100 <= hop_total_ns_x100));

// D7. Within-budget compares the structural path only.
p_lt_budget: assert property (@(posedge clk) disable iff (!rst_n)
  within_budget |-> (path_total_ns_x100 <= budget_ns_x100));

// D8. Terms are counted.
p_lt_counted: assert property (@(posedge clk) disable iff (!rst_n)
  term_valid |=> (c_terms == $past(c_terms) + 32'd1));

// E1. A witness who saw the design is not independent unless cited.
p_ca_independent: assert property (@(posedge clk) disable iff (!rst_n)
  (has_witness && witness_saw_design && !witness_is_citation)
    |-> !witness_is_independent);

// E2. A citation is independent by construction.
p_ca_citation: assert property (@(posedge clk) disable iff (!rst_n)
  (has_witness && witness_is_citation) |-> witness_is_independent);

// E3. The three states partition the items.
p_ca_partition: assert property (@(posedge clk) disable iff (!rst_n)
  (c_items == c_unfalsifiable + c_self_witnessed + c_auditable));

// E4. A review is auditable only with no hollow items.
p_ca_auditable: assert property (@(posedge clk) disable iff (!rst_n)
  review_is_auditable |-> ((c_unfalsifiable == 16'd0) &&
                           (c_self_witnessed == 16'd0)));

// E5. Only an environmental threshold may be deferred.
p_tb_deferred: assert property (@(posedge clk) disable iff (!rst_n)
  deferred |-> threshold_is_environmental);

// E6. A hard-coded environmental threshold becomes a default.
p_tb_default: assert property (@(posedge clk) disable iff (!rst_n)
  (threshold_is_environmental && design_hardcodes_value
   && !design_exposes_parameter) |-> becomes_a_default);

// E7. And exposing it with an owner is the correct handling.
p_tb_correct: assert property (@(posedge clk) disable iff (!rst_n)
  deferred_correctly |-> (design_exposes_parameter && owner_named));

// E8. Exposure share is bounded.
p_tb_share: assert property (@(posedge clk) disable iff (!rst_n)
  (exposure_share_ppm <= 32'd1_000_000));

// E9. Silent defaults are counted.
p_tb_counted: assert property (@(posedge clk) disable iff (!rst_n)
  (item_valid && becomes_a_default) |=>
    (c_silent_defaults == $past(c_silent_defaults) + 16'd1));

// F1. A verdict is reportable only with a nonzero denominator.
p_tl_reportable: assert property (@(posedge clk) disable iff (!rst_n)
  (verdict_is_reportable == (c_can_fail != 16'd0)));

// F2. Dilution is the complement of readiness.
p_tl_dilution: assert property (@(posedge clk) disable iff (!rst_n)
  (c_items != 16'd0) |-> ((dilution_ppm + readiness_ppm_o) <= 32'd1_000_001));

// F3. A review with nothing failable is a violation.
p_cf_no_failable: assert property (@(posedge clk) disable iff (!rst_n)
  ((items_can_fail == 16'd0) && (items_total != 16'd0)) |-> v_no_failable_items);

// F4. A verdict without its denominator is a violation.
p_cf_denominator: assert property (@(posedge clk) disable iff (!rst_n)
  !verdict_reported_with_denominator |-> v_verdict_without_denominator);

// F5. A budget-only reconciliation is a violation.
p_cf_reference: assert property (@(posedge clk) disable iff (!rst_n)
  (reconciled_against_budget && !reconciled_against_reference)
    |-> v_no_reference_bill);

// F6. An unexposed environmental threshold is a violation.
p_cf_hardcoded: assert property (@(posedge clk) disable iff (!rst_n)
  (environmental_exposed < environmental_thresholds) |-> v_threshold_hardcoded);

// F7. A latency budget with no percentile is a violation.
p_cf_latency: assert property (@(posedge clk) disable iff (!rst_n)
  !latency_percentile_specified |-> v_latency_uncongested_only);

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

c_it_adjective:   cover property (@(posedge clk) kind == 2'(ITEM_ADJECTIVE));
c_it_audited:     cover property (@(posedge clk) kind == 2'(ITEM_AUDITED));
c_rd_diluted:     cover property (@(posedge clk) verdict_is_diluted);
c_rd_all_adject:  cover property (@(posedge clk) (c_can_fail == 16'd0) && (c_items != 16'd0));
c_rd_ready:       cover property (@(posedge clk) readiness_ppm_o == 32'd1_000_000);
c_ar_omission:    cover property (@(posedge clk) below_reference_estimate);
c_ar_excess:      cover property (@(posedge clk) exceeds_budget);
c_lt_no_pctile:   cover property (@(posedge clk) budget_is_uncongested_only);
c_ca_self:        cover property (@(posedge clk) state == 2'(CLAIM_SELF_WITNESSED));
c_ca_auditable:   cover property (@(posedge clk) review_is_auditable);
c_tb_default:     cover property (@(posedge clk) becomes_a_default);
c_tb_correct:     cover property (@(posedge clk) deferred_correctly);
c_tl_unreportable:cover property (@(posedge clk) !verdict_is_reportable);
c_cf_clean:       cover property (@(posedge clk) conformant);