RTL and Verification Review

// ---------------------------------------------------------------------
// verifreview_pkg -- the coverage model's axes, the four outcomes a bin
// can have, and the constants Sections 4 to 8 derive.
//
// The axes are taken from chapters that already own them rather than
// invented here: the seven RMON size buckets from Chapter 19.7 Section 2,
// the twelve error classes from Chapter 21.2 Section 1, three tag depths
// and two directions. Seven times thirteen times three times two is the
// 546 bins Section 4 counts.
// ---------------------------------------------------------------------
package verifreview_pkg;

  // The four axes. ERR_NONE is the thirteenth value of the error axis:
  // twelve classes plus "no error", which is the bin most frames land in.
  typedef enum logic [2:0] {
    SZ_LE64, SZ_65_127, SZ_128_255, SZ_256_511,
    SZ_512_1023, SZ_1024_1518, SZ_GE1519
  } size_bucket_e;                       // 7 -- Chapter 19.7 Section 2

  typedef enum logic [3:0] {
    ERR_NONE,  ERR_FCS,      ERR_ALIGN,   ERR_RUNT,
    ERR_GIANT, ERR_SYMBOL,   ERR_DROP,    ERR_FIFO_OVF,
    ERR_DESC,  ERR_FILTER,   ERR_VLANMEM, ERR_MTUMIS,
    ERR_JABBER
  } err_class_e;                         // 13 -- Chapter 21.2 Section 1

  typedef enum logic [1:0] { TAG_NONE, TAG_SINGLE, TAG_DOUBLE } tag_e;
  typedef enum logic       { DIR_RX, DIR_TX }                   dir_e;

  localparam int N_SIZE = 7;
  localparam int N_ERR  = 13;
  localparam int N_TAG  = 3;
  localparam int N_DIR  = 2;
  localparam int N_BINS = N_SIZE * N_ERR * N_TAG * N_DIR;   // 546

  // The four outcomes of Section 1's table. UNCLASSIFIED is the default
  // and it is the one the review exists to count.
  typedef enum logic [1:0] {
    BIN_UNCLASSIFIED,   // nobody looked -- the finding
    BIN_HIT,            // covered
    BIN_UNREACHABLE,    // an argument exists, and is recorded
    BIN_DIRECTED        // reachable, too rare, a test exists
  } bin_outcome_e;

  // Why a bin is unreachable. A reason is not a boolean: a reviewer
  // attacks the REASON, so the reason has to be nameable.
  typedef enum logic [2:0] {
    UR_NONE,
    UR_LENGTH,        // the class needs a length this bucket excludes
    UR_DIRECTION,     // the class is a receive-side decision
    UR_CONFIG,        // excluded only at this build's parameters
    UR_ENVIRONMENT    // excluded only at this deployment's parameters
  } unreach_reason_e;

  // A bin, flattened. The index is the review's identifier for it and
  // the exclusion list is a list of these indices.
  typedef struct packed {
    size_bucket_e    sz;
    err_class_e      ec;
    tag_e            tg;
    dir_e            dr;
  } bin_key_t;

  function automatic int unsigned bin_index(bin_key_t k);
    return ((int'(k.sz) * N_ERR + int'(k.ec)) * N_TAG + int'(k.tg))
           * N_DIR + int'(k.dr);
  endfunction

  // Section 6: the peer MTU decides where an MTU-mismatch bin becomes
  // reachable, and it is Chapter 26.1 Section 12's environmental
  // threshold appearing inside a coverage model.
  localparam int MTU_BUCKET_576  = 4;   // mismatch visible from SZ_512_1023
  localparam int MTU_BUCKET_1024 = 5;   // from SZ_1024_1518
  localparam int MTU_BUCKET_1500 = 6;   // SZ_GE1519 only

endpackage

// ---------------------------------------------------------------------
// bin_model -- one bin in, one outcome out, with the reason attached.
//
// The module's whole value is that it separates UNREACHABLE from
// UNCLASSIFIED. A coverage tool reports both as "not hit".
// ---------------------------------------------------------------------
module bin_model
  import verifreview_pkg::*;
#(
  // The peer's maximum transmission unit, expressed as the first size
  // bucket in which a mismatch can be observed. Section 6 shows the
  // exclusion count moving by six as this parameter moves.
  parameter int MTU_BUCKET = MTU_BUCKET_1024
)(
  input  logic            clk,
  input  logic            rst_n,

  input  logic            bin_valid,
  input  bin_key_t        bin_key,
  input  logic            was_hit,        // the coverage tool's report
  input  logic            has_directed,   // a directed test names it
  input  logic            has_argument,   // an exclusion argument exists

  output logic            out_valid,
  output bin_outcome_e    outcome,
  output unreach_reason_e reason,
  output logic            reason_is_soft  // CONFIG or ENVIRONMENT
);

  // Structural unreachability. Every arm here is a fact about the frame
  // definition or the direction, and each cites the chapter that owns it.
  function automatic unreach_reason_e structural(bin_key_t k);
    // A runt is shorter than 64 octets, so it lives in one bucket only.
    if (k.ec == ERR_RUNT && k.sz != SZ_LE64)
      return UR_LENGTH;
    // A giant and a jabber are longer than the MTU. Chapter 21.2 Sec 1.
    if ((k.ec == ERR_GIANT || k.ec == ERR_JABBER) && k.sz != SZ_GE1519)
      return UR_LENGTH;
    // Five classes are receive-side facts. A transmitter emits whole
    // octets by construction, so an alignment error has no TX form.
    if (k.dr == DIR_TX &&
        (k.ec == ERR_SYMBOL   || k.ec == ERR_ALIGN ||
         k.ec == ERR_FIFO_OVF || k.ec == ERR_FILTER ||
         k.ec == ERR_VLANMEM))
      return UR_DIRECTION;
    return UR_NONE;
  endfunction

  // Environmental unreachability. This arm is the one Section 6 is
  // about: it is true at this build's parameter and false at another.
  function automatic unreach_reason_e environmental(bin_key_t k);
    if (k.ec == ERR_MTUMIS && int'(k.sz) < MTU_BUCKET)
      return UR_ENVIRONMENT;
    return UR_NONE;
  endfunction

  unreach_reason_e r_struct, r_env;

  always_comb begin
    r_struct = structural(bin_key);
    r_env    = environmental(bin_key);
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      out_valid      <= 1'b0;
      outcome        <= BIN_UNCLASSIFIED;
      reason         <= UR_NONE;
      reason_is_soft <= 1'b0;
    end else begin
      out_valid <= bin_valid;
      if (bin_valid) begin
        if (was_hit) begin
          outcome        <= BIN_HIT;
          reason         <= UR_NONE;
          reason_is_soft <= 1'b0;
        end else if (r_struct != UR_NONE) begin
          outcome        <= BIN_UNREACHABLE;
          reason         <= r_struct;
          reason_is_soft <= 1'b0;
        end else if (r_env != UR_NONE) begin
          outcome        <= BIN_UNREACHABLE;
          reason         <= r_env;
          reason_is_soft <= 1'b1;      // Section 6 counts these
        end else if (has_directed) begin
          outcome        <= BIN_DIRECTED;
          reason         <= UR_NONE;
          reason_is_soft <= 1'b0;
        end else begin
          // Not hit, no structural reason, no environmental reason,
          // no directed test. The honest outcome, and the finding.
          outcome        <= has_argument ? BIN_UNREACHABLE
                                         : BIN_UNCLASSIFIED;
          reason         <= has_argument ? UR_CONFIG : UR_NONE;
          reason_is_soft <= has_argument;
        end
      end
    end
  end

endmodule

// ---------------------------------------------------------------------
// reachability_classifier -- sweep all 546 bins, count the four
// outcomes, and expose the two coverage fractions separately.
//
// The module exists to make the two denominators VISIBLE AT ONCE.
// A flow that can only express one of them forces a choice that then
// gets defended rather than examined.
// ---------------------------------------------------------------------
module reachability_classifier
  import verifreview_pkg::*;
#(
  parameter int MTU_BUCKET = MTU_BUCKET_1024
)(
  input  logic         clk,
  input  logic         rst_n,

  input  logic         sweep_start,
  // One bit per bin from the coverage tool, and two from the plan.
  input  logic         hit_vec       [N_BINS],
  input  logic         directed_vec  [N_BINS],
  input  logic         argument_vec  [N_BINS],

  output logic         sweep_done,
  output logic [15:0]  n_declared,
  output logic [15:0]  n_unreachable,
  output logic [15:0]  n_reachable,
  output logic [15:0]  n_hit,
  output logic [15:0]  n_directed,
  output logic [15:0]  n_unclassified,
  output logic [15:0]  n_soft_exclusions,   // Section 6's six
  // The two fractions, in parts per million so both fit one unit.
  output logic [19:0]  cov_vs_declared_ppm,
  output logic [19:0]  cov_vs_reachable_ppm
);

  logic [15:0] idx;
  logic        running;

  // The bin at the current index, reconstructed from the flat index.
  bin_key_t k;
  always_comb begin
    k.dr = dir_e'( idx % N_DIR );
    k.tg = tag_e'((idx / N_DIR) % N_TAG );
    k.ec = err_class_e'((idx / (N_DIR*N_TAG)) % N_ERR );
    k.sz = size_bucket_e'( idx / (N_DIR*N_TAG*N_ERR) );
  end

  logic            this_unreach, this_soft;
  always_comb begin
    this_unreach = 1'b0;
    this_soft    = 1'b0;
    if (k.ec == ERR_RUNT && k.sz != SZ_LE64)
      this_unreach = 1'b1;
    else if ((k.ec == ERR_GIANT || k.ec == ERR_JABBER) &&
             k.sz != SZ_GE1519)
      this_unreach = 1'b1;
    else if (k.dr == DIR_TX &&
             (k.ec == ERR_SYMBOL || k.ec == ERR_ALIGN ||
              k.ec == ERR_FIFO_OVF || k.ec == ERR_FILTER ||
              k.ec == ERR_VLANMEM))
      this_unreach = 1'b1;
    else if (k.ec == ERR_MTUMIS && int'(k.sz) < MTU_BUCKET) begin
      this_unreach = 1'b1;
      this_soft    = 1'b1;          // moves with the deployment
    end
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      idx               <= '0;
      running           <= 1'b0;
      sweep_done        <= 1'b0;
      n_declared        <= '0;
      n_unreachable     <= '0;
      n_reachable       <= '0;
      n_hit             <= '0;
      n_directed        <= '0;
      n_unclassified    <= '0;
      n_soft_exclusions <= '0;
    end else begin
      sweep_done <= 1'b0;
      if (sweep_start) begin
        idx               <= '0;
        running           <= 1'b1;
        n_declared        <= '0;
        n_unreachable     <= '0;
        n_reachable       <= '0;
        n_hit             <= '0;
        n_directed        <= '0;
        n_unclassified    <= '0;
        n_soft_exclusions <= '0;
      end else if (running) begin
        n_declared <= n_declared + 16'd1;
        if (this_unreach) begin
          n_unreachable     <= n_unreachable + 16'd1;
          n_soft_exclusions <= n_soft_exclusions +
                               16'(this_soft ? 1 : 0);
        end else begin
          n_reachable <= n_reachable + 16'd1;
          if (hit_vec[idx])
            n_hit <= n_hit + 16'd1;
          else if (directed_vec[idx])
            n_directed <= n_directed + 16'd1;
          else if (!argument_vec[idx])
            // Reachable, not hit, no test, no argument. The finding.
            n_unclassified <= n_unclassified + 16'd1;
        end

        if (idx == 16'(N_BINS - 1)) begin
          running    <= 1'b0;
          sweep_done <= 1'b1;
        end else begin
          idx <= idx + 16'd1;
        end
      end
    end
  end

  // Both fractions, always, and never one of them.
  always_comb begin
    cov_vs_declared_ppm  = (n_declared  == 0) ? 20'd0
                         : 20'((int'(n_hit) * 1000000) / int'(n_declared));
    cov_vs_reachable_ppm = (n_reachable == 0) ? 20'd0
                         : 20'((int'(n_hit) * 1000000) / int'(n_reachable));
  end

endmodule

// ---------------------------------------------------------------------
// exclusion_auditor -- compares the exclusion file against the
// classifier's own rules and reports four disagreements, three of which
// no standard flow produces.
//
// It is the only module in this chapter that treats the exclusion list
// as EVIDENCE rather than as configuration.
// ---------------------------------------------------------------------
module exclusion_auditor
  import verifreview_pkg::*;
(
  input  logic         clk,
  input  logic         rst_n,

  input  logic         entry_valid,
  input  bin_key_t     entry_key,
  input  logic         entry_has_argument,   // the file's reason field
  input  unreach_reason_e entry_claimed,     // the reason it claims

  // The classifier's independent opinion of the same bin.
  input  logic            model_unreachable,
  input  unreach_reason_e model_reason,
  input  logic            model_soft,

  output logic [15:0]  n_entries,
  output logic [15:0]  n_with_argument,
  output logic [15:0]  n_soft,             // depends on a deployment
  output logic [15:0]  n_reason_mismatch,  // file and model disagree
  output logic [15:0]  n_model_disagrees,  // file excludes, model does not
  output logic         file_is_reviewed,   // every entry has an argument
  output logic         file_is_sound       // and the model agrees with all
);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      n_entries         <= '0;
      n_with_argument   <= '0;
      n_soft            <= '0;
      n_reason_mismatch <= '0;
      n_model_disagrees <= '0;
    end else if (entry_valid) begin
      n_entries <= n_entries + 16'd1;

      // Item 7 of Section 2: an entry without a sentence is an entry
      // nobody can attack.
      if (entry_has_argument)
        n_with_argument <= n_with_argument + 16'd1;

      // The six. An exclusion whose truth depends on a number outside
      // the room is the reviewer's whole budget.
      if (model_soft || entry_claimed == UR_ENVIRONMENT)
        n_soft <= n_soft + 16'd1;

      // The file says one thing and the rules say another. Both may be
      // defensible; the point is that nobody has ever compared them.
      if (model_unreachable && (entry_claimed != model_reason))
        n_reason_mismatch <= n_reason_mismatch + 16'd1;

      // The file excludes a bin the rules say is reachable. This is the
      // silent error of Section 6, and this counter is the only place
      // in the flow where it becomes a number.
      if (!model_unreachable)
        n_model_disagrees <= n_model_disagrees + 16'd1;
    end
  end

  // Two verdicts, and they are deliberately different questions.
  always_comb begin
    file_is_reviewed = (n_entries == n_with_argument);
    file_is_sound    = file_is_reviewed && (n_model_disagrees == 16'd0);
  end

endmodule

// ---------------------------------------------------------------------
// stimulus_budget -- given a bin's probability and the farm's frame
// budget, decide whether random stimulus will reach it and, if not,
// require a directed test.
//
// The arithmetic is deliberately the 95%-confidence form rather than
// the expectation form: a bin whose EXPECTED hit count is one is missed
// about 37% of the time, and a plan built on expectations is wrong on a
// third of its rarest bins.
// ---------------------------------------------------------------------
module stimulus_budget #(
  // Probabilities arrive scaled by 1e12 so that 1e-10 is 100 and the
  // whole range of interest fits in 40 bits without a real type.
  parameter longint unsigned FRAMES_PER_WEEK = 64'd2_940_700_000,
  // ln(0.05) / ln(1-p) is about 3/p for small p. The 3 is exact enough
  // below p = 1e-3 and this model is only used below 1e-6.
  parameter int unsigned     CONF_MULT       = 3
)(
  input  logic          clk,
  input  logic          rst_n,

  input  logic          bin_valid,
  input  logic [39:0]   bin_p_e12,        // probability x 1e12
  input  logic          has_directed_test,

  output logic          out_valid,
  output logic          reachable_by_random,
  output logic          needs_directed,
  output logic          gap,              // needs one and has none
  output logic [47:0]   frames_needed_e0,
  output logic [31:0]   weeks_needed,
  output logic [15:0]   n_needing_directed,
  output logic [15:0]   n_directed_present,
  output logic [15:0]   n_gaps
);

  // 3 / p, with p expressed times 1e12. The divide is by the scaled
  // probability, so the 1e12 cancels into the numerator.
  function automatic longint unsigned frames_for(logic [39:0] p_e12);
    if (p_e12 == 40'd0) return 64'hFFFF_FFFF_FFFF;   // never
    return (64'(CONF_MULT) * 64'd1_000_000_000_000) / 64'(p_e12);
  endfunction

  longint unsigned need;

  always_comb begin
    need = frames_for(bin_p_e12);
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      out_valid           <= 1'b0;
      reachable_by_random <= 1'b0;
      needs_directed      <= 1'b0;
      gap                 <= 1'b0;
      frames_needed_e0    <= '0;
      weeks_needed        <= '0;
      n_needing_directed  <= '0;
      n_directed_present  <= '0;
      n_gaps              <= '0;
    end else begin
      out_valid <= bin_valid;
      if (bin_valid) begin
        frames_needed_e0 <= 48'(need);
        weeks_needed     <= 32'((need + FRAMES_PER_WEEK - 1)
                                / FRAMES_PER_WEEK);

        if (need <= FRAMES_PER_WEEK) begin
          reachable_by_random <= 1'b1;
          needs_directed      <= 1'b0;
          gap                 <= 1'b0;
        end else begin
          reachable_by_random <= 1'b0;
          needs_directed      <= 1'b1;
          n_needing_directed  <= n_needing_directed + 16'd1;
          if (has_directed_test) begin
            n_directed_present <= n_directed_present + 16'd1;
            gap                <= 1'b0;
          end else begin
            // Section 2's items 5 and 6 differing. The plan believes
            // this bin is covered and nothing will cover it.
            n_gaps <= n_gaps + 16'd1;
            gap    <= 1'b1;
          end
        end
      end
    end
  end

endmodule

// ---------------------------------------------------------------------
// bound_covered_reconciler -- walk the regression's property table and
// separate the properties that never fired into the three outcomes of
// Section 10, so that "bound minus covered" becomes a classified list
// rather than a number to be explained away.
// ---------------------------------------------------------------------
module bound_covered_reconciler (
  input  logic         clk,
  input  logic         rst_n,

  input  logic         prop_valid,
  input  logic         prop_bound,          // survived elaboration
  input  logic [31:0]  prop_cover_count,    // times the antecedent fired
  input  logic [31:0]  prop_pass_count,
  input  logic [31:0]  prop_fail_count,
  input  logic         prop_excluded_by_cfg,// a generate removed its peer
  input  logic         prop_has_argument,   // somebody wrote the reason
  input  logic         prop_needs_traffic,  // Chapter 21.4's category

  output logic [15:0]  n_bound,
  output logic [15:0]  n_covered,
  output logic [15:0]  n_silent,            // bound, never evaluated
  output logic [15:0]  n_silent_explained,  // and classified
  output logic [15:0]  n_silent_unexplained,
  output logic [15:0]  n_traffic_dependent,
  output logic [19:0]  traffic_dep_ppm,
  output logic         suite_is_reconciled,
  output logic         report_is_honest     // pass count has a denominator
);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      n_bound              <= '0;
      n_covered            <= '0;
      n_silent             <= '0;
      n_silent_explained   <= '0;
      n_silent_unexplained <= '0;
      n_traffic_dependent  <= '0;
    end else if (prop_valid && prop_bound) begin
      n_bound <= n_bound + 16'd1;

      if (prop_needs_traffic)
        n_traffic_dependent <= n_traffic_dependent + 16'd1;

      if (prop_cover_count != 32'd0) begin
        n_covered <= n_covered + 16'd1;
      end else begin
        // Bound and never evaluated. A pass count of zero here is
        // indistinguishable from a pass count of zero on a property
        // that fired and never held -- except that fail_count settles it.
        n_silent <= n_silent + 16'd1;
        if (prop_excluded_by_cfg || prop_has_argument)
          n_silent_explained <= n_silent_explained + 16'd1;
        else
          n_silent_unexplained <= n_silent_unexplained + 16'd1;
      end
    end
  end

  always_comb begin
    traffic_dep_ppm = (n_bound == 0) ? 20'd0
                    : 20'((int'(n_traffic_dependent) * 1000000)
                          / int'(n_bound));
    // The useful verdict is not "everything fired" -- it is "everything
    // that did not fire has a sentence attached".
    suite_is_reconciled = (n_silent_unexplained == 16'd0);
    // And a pass count means nothing without the cover count beside it.
    report_is_honest    = suite_is_reconciled && (n_covered != 16'd0);
  end

endmodule

// ---------------------------------------------------------------------
// effort_reconciler -- hold the four units side by side without ever
// summing them, and report the one relationship that is real: what each
// route costs in the calendar.
//
// The module's central refusal is that it has NO output combining a
// simulation-hour with an engineer-day. Section 12 is the reason.
// ---------------------------------------------------------------------
module effort_reconciler #(
  parameter int unsigned FARM_HOURS_PER_WEEK   = 20000,
  parameter int unsigned ENG_DAYS_PER_TEST_X10 = 15,    // 1.5 days
  parameter int unsigned ENG_DAYS_PER_WEEK     = 5
)(
  input  logic         clk,
  input  logic         rst_n,

  input  logic         reconcile,
  input  logic [15:0]  bins_declared,
  input  logic [15:0]  bins_reachable,
  input  logic [15:0]  bins_hit,
  input  logic [15:0]  bins_needing_directed,
  input  logic [47:0]  frames_to_close_by_random,
  input  logic [31:0]  sim_frames_per_hour,
  input  logic [15:0]  props_bound,
  input  logic [15:0]  props_silent,

  // Four outputs in four units. None of them is a sum of the others.
  output logic [15:0]  u_bins_outstanding,
  output logic [31:0]  u_sim_hours_to_close,
  output logic [15:0]  u_eng_weeks_to_close,
  output logic [15:0]  u_props_unevaluated,

  // And two dimensionless ratios, which are the only figures that
  // transfer to another programme.
  output logic [19:0]  unreachable_share_ppm,
  output logic [19:0]  silent_share_ppm,

  // The calendar comparison: the two routes, in weeks, side by side.
  output logic [31:0]  weeks_if_random,
  output logic [15:0]  weeks_if_directed,
  output logic         directed_is_cheaper
);

  logic [31:0] sim_hours;
  logic [31:0] eng_days_x10;

  always_comb begin
    sim_hours = (sim_frames_per_hour == 0) ? 32'hFFFF_FFFF
              : 32'(frames_to_close_by_random / 48'(sim_frames_per_hour));
    eng_days_x10 = 32'(bins_needing_directed) * 32'(ENG_DAYS_PER_TEST_X10);
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      u_bins_outstanding    <= '0;
      u_sim_hours_to_close  <= '0;
      u_eng_weeks_to_close  <= '0;
      u_props_unevaluated   <= '0;
      weeks_if_random       <= '0;
      weeks_if_directed     <= '0;
    end else if (reconcile) begin
      u_bins_outstanding   <= bins_reachable - bins_hit;
      u_sim_hours_to_close <= sim_hours;
      // Round up: a fraction of an engineer-week is a whole week of
      // somebody's calendar.
      u_eng_weeks_to_close <= 16'((eng_days_x10 +
                                   (10*ENG_DAYS_PER_WEEK) - 1)
                                  / (10*ENG_DAYS_PER_WEEK));
      u_props_unevaluated  <= props_silent;

      weeks_if_random   <= (sim_hours + FARM_HOURS_PER_WEEK - 1)
                           / FARM_HOURS_PER_WEEK;
      weeks_if_directed <= 16'((eng_days_x10 +
                                (10*ENG_DAYS_PER_WEEK) - 1)
                               / (10*ENG_DAYS_PER_WEEK));
    end
  end

  always_comb begin
    unreachable_share_ppm =
      (bins_declared == 0) ? 20'd0
      : 20'((int'(bins_declared - bins_reachable) * 1000000)
            / int'(bins_declared));
    silent_share_ppm =
      (props_bound == 0) ? 20'd0
      : 20'((int'(props_silent) * 1000000) / int'(props_bound));
    // The only legitimate comparison between the two routes: which one
    // occupies fewer weeks of the project's calendar.
    directed_is_cheaper = (32'(weeks_if_directed) < weeks_if_random);
  end

endmodule

// ---------------------------------------------------------------------
// verif_telemetry -- the numbers a verification review should be able
// to read at any moment, not only at sign-off.
//
// Everything here is a count or a ratio of counts. Nothing here is a
// verdict; Section 16 owns those.
// ---------------------------------------------------------------------
module verif_telemetry (
  input  logic         clk,
  input  logic         rst_n,
  input  logic         clear,

  // From the classifier, Section 5.
  input  logic         sweep_done,
  input  logic [15:0]  bins_declared,
  input  logic [15:0]  bins_unreachable,
  input  logic [15:0]  bins_reachable,
  input  logic [15:0]  bins_hit,
  input  logic [15:0]  bins_directed,
  input  logic [15:0]  bins_unclassified,
  input  logic [15:0]  soft_exclusions,

  // From the exclusion auditor, Section 7.
  input  logic [15:0]  excl_entries,
  input  logic [15:0]  excl_with_argument,
  input  logic [15:0]  excl_model_disagrees,

  // From the reconciler, Section 11.
  input  logic [15:0]  props_bound,
  input  logic [15:0]  props_silent,
  input  logic [15:0]  props_silent_unexplained,

  // Events the review wants counted over time rather than at the end.
  input  logic         excl_added,
  input  logic         directed_test_added,

  output logic [19:0]  cov_declared_ppm,
  output logic [19:0]  cov_reachable_ppm,
  output logic [19:0]  unreachable_ppm,
  output logic [19:0]  excl_reviewed_ppm,
  output logic [19:0]  silent_ppm,
  output logic [15:0]  c_exclusions_added,
  output logic [15:0]  c_directed_added,
  output logic [15:0]  c_unclassified,
  output logic         v_denominator_missing,
  output logic         v_exclusion_unargued,
  output logic         v_exclusion_contradicted,
  output logic         v_silent_unexplained,
  output logic         v_closed_by_editing,
  output logic         v_soft_exclusion_present
);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n || clear) begin
      c_exclusions_added <= '0;
      c_directed_added   <= '0;
    end else begin
      if (excl_added)          c_exclusions_added <= c_exclusions_added + 16'd1;
      if (directed_test_added) c_directed_added   <= c_directed_added   + 16'd1;
    end
  end

  always_comb begin
    cov_declared_ppm  = (bins_declared  == 0) ? 20'd0
                      : 20'((int'(bins_hit) * 1000000) / int'(bins_declared));
    cov_reachable_ppm = (bins_reachable == 0) ? 20'd0
                      : 20'((int'(bins_hit) * 1000000) / int'(bins_reachable));
    unreachable_ppm   = (bins_declared  == 0) ? 20'd0
                      : 20'((int'(bins_unreachable) * 1000000)
                            / int'(bins_declared));
    excl_reviewed_ppm = (excl_entries   == 0) ? 20'd1000000
                      : 20'((int'(excl_with_argument) * 1000000)
                            / int'(excl_entries));
    silent_ppm        = (props_bound    == 0) ? 20'd0
                      : 20'((int'(props_silent) * 1000000) / int'(props_bound));

    c_unclassified = bins_unclassified;

    // Six flags. Each one names a specific sentence somebody must add.
    v_denominator_missing    = (bins_reachable == 16'd0) &&
                               (bins_declared != 16'd0);
    v_exclusion_unargued     = (excl_with_argument < excl_entries);
    v_exclusion_contradicted = (excl_model_disagrees != 16'd0);
    v_silent_unexplained     = (props_silent_unexplained != 16'd0);
    // The prohibition-3 detector: exclusions grew faster than tests.
    v_closed_by_editing      = (c_exclusions_added > c_directed_added) &&
                               (c_exclusions_added > 16'd0);
    v_soft_exclusion_present = (soft_exclusions != 16'd0);
  end

endmodule

// ---------------------------------------------------------------------
// verif_conformance -- the sign-off gate for Section 2's twenty items,
// expressed as seven checks over the outputs of Sections 5, 7, 11 and 13.
//
// The gate's design rule: every check must be able to FAIL on a plan
// that a project would actually submit. A check that no real plan fails
// is Section 20's refused property with a different name.
// ---------------------------------------------------------------------
module verif_conformance (
  input  logic         clk,
  input  logic         rst_n,

  input  logic         evaluate,

  // Section 5.
  input  logic [15:0]  bins_declared,
  input  logic [15:0]  bins_reachable,
  input  logic [15:0]  bins_hit,
  input  logic [15:0]  bins_unclassified,

  // Section 7.
  input  logic [15:0]  excl_entries,
  input  logic [15:0]  excl_with_argument,
  input  logic [15:0]  excl_model_disagrees,
  input  logic [15:0]  excl_soft,
  input  logic         excl_soft_owners_named,

  // Section 9.
  input  logic [15:0]  bins_needing_directed,
  input  logic [15:0]  directed_tests_present,

  // Section 11.
  input  logic [15:0]  props_bound,
  input  logic [15:0]  props_covered,
  input  logic [15:0]  props_silent_unexplained,

  // Section 13 -- present so the report cannot omit a unit.
  input  logic         both_denominators_reported,

  output logic         c1_denominators_reported,
  output logic         c2_model_classified,
  output logic         c3_exclusions_argued,
  output logic         c4_exclusions_uncontradicted,
  output logic         c5_soft_exclusions_owned,
  output logic         c6_directed_tests_match,
  output logic         c7_suite_reconciled,
  output logic [2:0]   n_failures,
  output logic         conformant,
  output logic         gate_can_fail        // the self-check
);

  logic [2:0] fails;

  always_comb begin
    // 1. Section 4: the report carries both fractions, or it carries
    //    an editorial decision.
    c1_denominators_reported = both_denominators_reported &&
                               (bins_reachable != 16'd0);

    // 2. Section 5: no bin is reachable, unhit and unclassified.
    c2_model_classified      = (bins_unclassified == 16'd0);

    // 3. Section 7, item 7 of Section 2.
    c3_exclusions_argued     = (excl_with_argument == excl_entries);

    // 4. Section 6's silent error: the file excludes what the rules
    //    say is reachable.
    c4_exclusions_uncontradicted = (excl_model_disagrees == 16'd0);

    // 5. Section 7: the six that depend on a deployment have owners.
    c5_soft_exclusions_owned = (excl_soft == 16'd0) ||
                               excl_soft_owners_named;

    // 6. Section 2, item 5 against item 6. A shortfall here is the
    //    difference that got closed with an editor.
    c6_directed_tests_match  = (directed_tests_present >=
                                bins_needing_directed);

    // 7. Section 11: every silent property has a sentence.
    c7_suite_reconciled      = (props_silent_unexplained == 16'd0) &&
                               (props_covered <= props_bound);

    fails = 3'(!c1_denominators_reported)     + 3'(!c2_model_classified)
          + 3'(!c3_exclusions_argued)         + 3'(!c4_exclusions_uncontradicted)
          + 3'(!c5_soft_exclusions_owned)     + 3'(!c6_directed_tests_match)
          + 3'(!c7_suite_reconciled);

    // Every check above compares two quantities the plan supplies, so
    // a plan exists that fails each one. This bit records that the gate
    // is not Section 20's refused property.
    gate_can_fail = (bins_declared != 16'd0) && (props_bound != 16'd0);
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      n_failures <= '0;
      conformant <= 1'b0;
    end else if (evaluate) begin
      n_failures <= fails;
      conformant <= (fails == 3'd0) && gate_can_fail;
    end
  end

endmodule

// 1. A hit bin is never also classified unreachable. If it is, one of
//    the two inputs is lying and the exclusion file is the suspect.
p_hit_not_unreachable: assert property (@(posedge clk) disable iff (!rst_n)
  (out_valid && was_hit) |-> (outcome == BIN_HIT));

// 2. Every unreachable outcome carries a reason. A reason is what a
//    reviewer attacks; an outcome without one cannot be argued with.
p_unreachable_has_reason: assert property (@(posedge clk) disable iff (!rst_n)
  (out_valid && outcome == BIN_UNREACHABLE) |-> (reason != UR_NONE));

// 3. And a reachable outcome carries none, so the two are exclusive.
p_reachable_no_reason: assert property (@(posedge clk) disable iff (!rst_n)
  (out_valid && outcome != BIN_UNREACHABLE) |-> (reason == UR_NONE));

// 4. reason_is_soft is set exactly for the two deployment-dependent
//    reasons. Section 6's six bins are found by this bit.
p_soft_iff_env: assert property (@(posedge clk) disable iff (!rst_n)
  out_valid |-> (reason_is_soft ==
                 (reason == UR_ENVIRONMENT || reason == UR_CONFIG)));

// 5. A runt outside the smallest bucket is unreachable for a LENGTH
//    reason, never for a direction one.
p_runt_reason: assert property (@(posedge clk) disable iff (!rst_n)
  (out_valid && bin_key.ec == ERR_RUNT && bin_key.sz != SZ_LE64)
    |-> (outcome == BIN_UNREACHABLE && reason == UR_LENGTH));

// 6. A transmit-side alignment error is unreachable for a DIRECTION
//    reason at every size.
p_tx_align_reason: assert property (@(posedge clk) disable iff (!rst_n)
  (out_valid && bin_key.ec == ERR_ALIGN && bin_key.dr == DIR_TX)
    |-> (outcome == BIN_UNREACHABLE && reason == UR_DIRECTION));

// 7. The default, and the finding: not hit, no rule, no test, no
//    sentence is UNCLASSIFIED and nothing else.
p_default_unclassified: assert property (@(posedge clk) disable iff (!rst_n)
  (out_valid && !was_hit && !has_directed && !has_argument &&
   reason == UR_NONE) |-> (outcome == BIN_UNCLASSIFIED));

// 8. Structural reasons never depend on a parameter.
p_structural_stable: assert property (@(posedge clk) disable iff (!rst_n)
  (out_valid && (reason == UR_LENGTH || reason == UR_DIRECTION))
    |-> !reason_is_soft);

c_each_outcome_seen: cover property (@(posedge clk)
  out_valid && outcome == BIN_UNCLASSIFIED);

// 9. The three counts partition the declared model exactly.
p_counts_partition: assert property (@(posedge clk) disable iff (!rst_n)
  sweep_done |-> (n_unreachable + n_reachable == n_declared));

// 10. And the declared count is the model's size, not a running total.
p_declared_is_model: assert property (@(posedge clk) disable iff (!rst_n)
  sweep_done |-> (n_declared == 16'(N_BINS)));

// 11. The reachable bins partition into the three dispositions.
p_reachable_partition: assert property (@(posedge clk) disable iff (!rst_n)
  sweep_done |-> (n_hit + n_directed + n_unclassified <= n_reachable));

// 12. Both fractions are produced, and neither is produced alone.
p_both_fractions: assert property (@(posedge clk) disable iff (!rst_n)
  (sweep_done && n_declared != 0 && n_reachable != 0)
    |-> (cov_vs_declared_ppm <= cov_vs_reachable_ppm));

// 13. The declared fraction can never exceed the reachable one, which
//     is the arithmetic form of "excluding bins raises coverage".
p_declared_le_reachable: assert property (@(posedge clk) disable iff (!rst_n)
  sweep_done |-> (cov_vs_declared_ppm <= cov_vs_reachable_ppm));

// 14. Soft exclusions are a subset of exclusions.
p_soft_subset: assert property (@(posedge clk) disable iff (!rst_n)
  sweep_done |-> (n_soft_exclusions <= n_unreachable));

// 15. A sweep that starts finishes, in a bounded number of cycles.
p_sweep_terminates: assert property (@(posedge clk) disable iff (!rst_n)
  sweep_start |-> ##[1:N_BINS+2] sweep_done);

c_sweep_completed: cover property (@(posedge clk) sweep_done);
c_unclassified_nonzero: cover property (@(posedge clk)
  sweep_done && n_unclassified != 16'd0);

// 16. Entries with an argument never exceed entries.
p_argued_subset: assert property (@(posedge clk) disable iff (!rst_n)
  (n_with_argument <= n_entries));

// 17. file_is_reviewed is exactly the equality, not a threshold.
p_reviewed_is_equality: assert property (@(posedge clk) disable iff (!rst_n)
  file_is_reviewed == (n_entries == n_with_argument));

// 18. Soundness implies reviewedness, and never the converse.
p_sound_implies_reviewed: assert property (@(posedge clk) disable iff (!rst_n)
  file_is_sound |-> file_is_reviewed);

// 19. A disagreement between the file and the model is recorded, and
//     this is the ONLY place Section 6's silent error becomes visible.
p_disagreement_counted: assert property (@(posedge clk) disable iff (!rst_n)
  (entry_valid && !model_unreachable)
    |-> ##1 (n_model_disagrees == $past(n_model_disagrees) + 16'd1));

// 20. An entry the model calls soft is counted soft regardless of what
//     the file claims, because the file is the thing under audit.
p_soft_from_model: assert property (@(posedge clk) disable iff (!rst_n)
  (entry_valid && model_soft)
    |-> ##1 (n_soft == $past(n_soft) + 16'd1));

// 21. A sound file has no disagreements, by construction.
p_sound_no_disagree: assert property (@(posedge clk) disable iff (!rst_n)
  file_is_sound |-> (n_model_disagrees == 16'd0));

c_file_unsound: cover property (@(posedge clk)
  n_entries != 16'd0 && !file_is_sound);
c_soft_present: cover property (@(posedge clk) n_soft != 16'd0);

// 22. A bin reachable by random never also needs a directed test.
p_random_xor_directed: assert property (@(posedge clk) disable iff (!rst_n)
  out_valid |-> (reachable_by_random != needs_directed));

// 23. A gap is exactly "needs one and has none".
p_gap_definition: assert property (@(posedge clk) disable iff (!rst_n)
  out_valid |-> (gap == (needs_directed && !has_directed_test)));

// 24. Zero probability is never reachable by random, however long the
//     run. This is the bin that a coverage model should not contain.
p_zero_p_never: assert property (@(posedge clk) disable iff (!rst_n)
  (out_valid && $past(bin_p_e12) == 40'd0) |-> !reachable_by_random);

// 25. Frames needed falls as probability rises -- monotonicity, which
//     is the cheapest guard against a scaling error in the divide.
p_frames_monotone: assert property (@(posedge clk) disable iff (!rst_n)
  (out_valid && $past(bin_p_e12) > $past(bin_p_e12, 2) &&
   $past(bin_p_e12, 2) != 40'd0)
    |-> (frames_needed_e0 <= $past(frames_needed_e0)));

// 26. Weeks needed is at least one whenever frames needed is non-zero.
p_weeks_ceiling: assert property (@(posedge clk) disable iff (!rst_n)
  (out_valid && frames_needed_e0 != 48'd0) |-> (weeks_needed >= 32'd1));

// 27. Gaps are a subset of the bins needing a directed test.
p_gaps_subset: assert property (@(posedge clk) disable iff (!rst_n)
  (n_gaps <= n_needing_directed));

c_gap_seen: cover property (@(posedge clk) gap);