How Ethernet Is Actually Probed

// ---------------------------------------------------------------------
// probe_pkg -- the grading vocabulary of this chapter, the twelve
// taxonomy groups of the rejected-property series, and the constants
// Sections 6 to 12 count with.
//
// The unit throughout is the REFUTATION COUNT: the number of distinct
// observations that would have changed the answer. Section 4 defends
// it. It is zero for a recitation and for all 124 rejected classes.
// ---------------------------------------------------------------------
package probe_pkg;

  // What an answer is made of. These are not quality levels; they are
  // structurally different kinds of utterance.
  typedef enum logic [2:0] {
    ANS_ABSENT,        // no answer
    ANS_RECITATION,    // correct words, no claim about the world
    ANS_CLAIM,         // a claim, no quantity
    ANS_QUANTIFIED,    // a claim with a number
    ANS_DERIVED,       // and the number follows from something named
    ANS_COMPOSED       // and it composes two or more chapters
  } answer_kind_e;

  // The twelve groups of the rejected-property taxonomy. Group 1 to 6
  // were derived in Chapter 20.2 Section 8; 7 in 20.4, 8 in 21.2,
  // 9 in 21.5, 10 in 21.8, 11 in 21.9, 12 in 22.2.
  typedef enum logic [3:0] {
    GRP_NONE,
    GRP_SUBJECT,       // 1  wrong subject
    GRP_SCOPE,         // 2  wrong scope
    GRP_TIME,          // 3  wrong time
    GRP_UNEVALUABLE,   // 4  unevaluable
    GRP_PREMISE,       // 5  unknowable premise
    GRP_DESIGNED,      // 6  designed-for behaviour
    GRP_ARRANGED,      // 7  satisfaction the environment can arrange
    GRP_SIDE,          // 8  bound to the wrong side of a function
    GRP_EVALCOUNT,     // 9  who controls the evaluation count
    GRP_BOUNDARY,      // 10 boundaries that are not boundaries
    GRP_OBSERVER,      // 11 the observer is inside the system
    GRP_RELATION       // 12 a relation between nodes, evaluated at one
  } tax_group_e;

  localparam int N_GROUPS  = 12;
  localparam int N_CLASSES = 124;   // the series, complete

  // Section 6's census. These are the classes with an EXPLICIT group
  // assignment in the text, not an inferred one -- which is why the
  // number is 35 and not 124.
  localparam int N_ASSIGNED    = 35;
  localparam int N_ASSIGNMENTS = 36;   // one class has two groups
  localparam int N_UNASSIGNED  = 89;

  // Section 10's five producers of an outcome that carries no
  // information about the design. Note that PROD_SPEC does not always
  // produce a PASS: class 49's property fails, and it fails because
  // the design is correct, which is the same defect mirrored.
  typedef enum logic [2:0] {
    PROD_FORM,       // the expression does not denote the requirement
    PROD_STIMULUS,   // the property stops being evaluated
    PROD_OBSERVER,   // the instrument is part of the subject
    PROD_CUSTODIAN,  // nobody can constitute the premise
    PROD_SPEC        // the design's own specification decides it
  } producer_e;

  function automatic producer_e producer_of(tax_group_e g);
    case (g)
      GRP_EVALCOUNT, GRP_ARRANGED    : return PROD_STIMULUS;
      GRP_OBSERVER,  GRP_UNEVALUABLE : return PROD_OBSERVER;
      GRP_PREMISE                    : return PROD_CUSTODIAN;
      GRP_DESIGNED                   : return PROD_SPEC;
      default                        : return PROD_FORM;
    endcase
  endfunction

endpackage

// ---------------------------------------------------------------------
// answer_model -- grade one answer by what would have refuted it.
//
// The module deliberately has NO input for whether the answer contains
// any particular term. Section 13 shows what a keyword grader does on
// the same four answers, and it ranks them in the wrong order.
// ---------------------------------------------------------------------
module answer_model
  import probe_pkg::*;
(
  input  logic          clk,
  input  logic          rst_n,

  input  logic          ans_valid,
  // The observations the answer's claim would be contradicted by. This
  // is the whole input; everything else is derived from it.
  input  logic [7:0]    n_refuting_observations,
  input  logic          has_quantity,
  input  logic          quantity_is_derived,     // follows from a named source
  input  logic [3:0]    n_chapters_composed,
  input  logic          quantity_copied,         // a reference value, unadapted

  output logic          out_valid,
  output answer_kind_e  kind,
  output logic [7:0]    refutation_count,
  output logic          is_falsifiable,
  output logic          is_recitation,
  output logic          reference_value_risk
);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      out_valid            <= 1'b0;
      kind                 <= ANS_ABSENT;
      refutation_count     <= '0;
      is_falsifiable       <= 1'b0;
      is_recitation        <= 1'b0;
      reference_value_risk <= 1'b0;
    end else begin
      out_valid        <= ans_valid;
      refutation_count <= n_refuting_observations;
      is_falsifiable   <= (n_refuting_observations != 8'd0);
      // A recitation has the words and no refuting observation. It is
      // not wrong; it simply cannot be wrong.
      is_recitation    <= (n_refuting_observations == 8'd0);
      // Chapter 23.4 Section 7's 149 descriptors is correct at
      // 100 Gb/s and 595 at 400. A copied quantity looks derived.
      reference_value_risk <= has_quantity && quantity_copied;

      if (ans_valid) begin
        if (n_refuting_observations == 8'd0)
          kind <= has_quantity ? ANS_RECITATION : ANS_ABSENT;
        else if (!has_quantity)
          kind <= ANS_CLAIM;
        else if (!quantity_is_derived)
          kind <= ANS_QUANTIFIED;
        else if (n_chapters_composed <= 4'd1)
          kind <= ANS_DERIVED;
        else
          kind <= ANS_COMPOSED;
      end
    end
  end

endmodule

// ---------------------------------------------------------------------
// refutation_counter -- count the observations an answer names that
// would genuinely have refuted its claim, discarding those for which
// no mechanism is given.
//
// Section 4's weakness is the reason the module has two inputs per
// observation rather than one.
// ---------------------------------------------------------------------
module refutation_counter
  import probe_pkg::*;
#(
  parameter int unsigned MAX_OBS = 16
)(
  input  logic         clk,
  input  logic         rst_n,
  input  logic         answer_start,

  input  logic         obs_valid,
  input  logic         obs_has_mechanism,   // the candidate said HOW
  input  logic         obs_bears_on_claim,  // and it touches the claim
  input  logic         obs_is_duplicate,    // of one already counted

  input  logic         answer_end,

  output logic [7:0]   n_offered,
  output logic [7:0]   n_counted,
  output logic [7:0]   n_no_mechanism,
  output logic [7:0]   n_irrelevant,
  output logic [7:0]   n_duplicate,
  output logic [19:0]  precision_ppm,       // counted / offered
  output logic         answer_is_falsifiable,
  output logic         padding_detected
);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n || answer_start) begin
      n_offered      <= '0;
      n_counted      <= '0;
      n_no_mechanism <= '0;
      n_irrelevant   <= '0;
      n_duplicate    <= '0;
    end else if (obs_valid && (n_offered < 8'(MAX_OBS))) begin
      n_offered <= n_offered + 8'd1;
      // The three ways an offered observation fails to count, checked
      // in the order that gives the most informative diagnosis.
      if (!obs_has_mechanism)
        n_no_mechanism <= n_no_mechanism + 8'd1;
      else if (!obs_bears_on_claim)
        n_irrelevant <= n_irrelevant + 8'd1;
      else if (obs_is_duplicate)
        n_duplicate <= n_duplicate + 8'd1;
      else
        n_counted <= n_counted + 8'd1;
    end
  end

  always_comb begin
    precision_ppm = (n_offered == 8'd0) ? 20'd0
                  : 20'((int'(n_counted) * 1000000) / int'(n_offered));
    answer_is_falsifiable = (n_counted != 8'd0);
    // Padding: many offered, few counted. The ratio is the signal and
    // the absolute numbers are not -- a candidate who offers two and
    // counts two is stronger than one who offers eight and counts two.
    padding_detected = (n_offered >= 8'd4) &&
                       (precision_ppm < 20'd500000);
  end

endmodule

// ---------------------------------------------------------------------
// class_census -- walk the rejected-property series and count group
// memberships, keeping assignments and classes as SEPARATE totals
// because one class carries two groups.
//
// Chapter 26.2 Section 20's class 122 is the reason the module counts
// members rather than only totalling: a cardinality is invariant under
// a swap, and this census is about which classes are where.
// ---------------------------------------------------------------------
module class_census
  import probe_pkg::*;
(
  input  logic          clk,
  input  logic          rst_n,
  input  logic          census_start,

  input  logic          entry_valid,
  input  logic [7:0]    class_num,       // 1 to 124
  input  tax_group_e    group_id,
  input  logic          is_explicit,     // stated in the callout itself
  input  logic          is_second_group, // this class already had one

  output logic [7:0]    n_classes_seen,
  output logic [7:0]    n_assignments,
  output logic [7:0]    n_explicit,
  output logic [7:0]    n_multi_group,
  output logic [7:0]    n_unassigned,
  output logic [7:0]    per_group [N_GROUPS + 1],
  output logic [19:0]   explicit_share_ppm,
  output logic [3:0]    largest_group,
  output logic          census_is_over_explicit   // the denominator flag
);

  logic [7:0] biggest;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n || census_start) begin
      n_classes_seen <= '0;
      n_assignments  <= '0;
      n_explicit     <= '0;
      n_multi_group  <= '0;
      largest_group  <= '0;
      biggest        <= '0;
      for (int g = 0; g <= N_GROUPS; g = g + 1) per_group[g] <= '0;
    end else if (entry_valid) begin
      // A class is counted once; an assignment is counted every time.
      // Keeping these apart is the whole reason the module exists.
      if (!is_second_group)
        n_classes_seen <= n_classes_seen + 8'd1;
      else
        n_multi_group <= n_multi_group + 8'd1;

      n_assignments <= n_assignments + 8'd1;
      if (is_explicit) n_explicit <= n_explicit + 8'd1;

      per_group[int'(group_id)] <= per_group[int'(group_id)] + 8'd1;

      if ((per_group[int'(group_id)] + 8'd1) > biggest) begin
        biggest       <= per_group[int'(group_id)] + 8'd1;
        largest_group <= 4'(group_id);
      end
    end
  end

  always_comb begin
    n_unassigned = 8'(N_CLASSES) - n_classes_seen;
    explicit_share_ppm = 20'((int'(n_classes_seen) * 1000000) / N_CLASSES);
    // The flag that keeps Section 6's honesty: this census's denominator
    // is the explicit assignments, not the series.
    census_is_over_explicit = (n_explicit == n_assignments);
  end

endmodule

// ---------------------------------------------------------------------
// group_auditor -- detect what Section 7's census can only report: a
// class assigned to more than one group, and a group with no founding
// chapter recorded.
//
// The module is the one place in this chapter that treats the taxonomy
// as DATA to be checked rather than as a framework to classify with.
// ---------------------------------------------------------------------
module group_auditor
  import probe_pkg::*;
#(
  parameter int unsigned MAX_CLASS = 124
)(
  input  logic          clk,
  input  logic          rst_n,
  input  logic          audit_start,

  input  logic          entry_valid,
  input  logic [7:0]    class_num,
  input  tax_group_e    group_id,

  // Per-group provenance, loaded once.
  input  logic          prov_valid,
  input  tax_group_e    prov_group,
  input  logic          prov_founded,     // a chapter states the opening
  input  logic          prov_settled,     // and the argument was closed

  output logic [7:0]    n_multi_assigned,
  output logic [7:0]    first_multi_class,
  output logic [3:0]    n_founded,
  output logic [3:0]    n_unsettled,
  output logic          taxonomy_is_partition,
  output logic          every_group_founded,
  output logic          priority_rule_required
);

  // One bit per class per group. At 124 by 13 this is a testbench
  // structure, not silicon.
  logic seen [MAX_CLASS + 1][N_GROUPS + 1];
  logic [3:0] count_for_class;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n || audit_start) begin
      for (int c = 0; c <= MAX_CLASS; c = c + 1)
        for (int g = 0; g <= N_GROUPS; g = g + 1)
          seen[c][g] <= 1'b0;
      n_multi_assigned  <= '0;
      first_multi_class <= '0;
      n_founded         <= '0;
      n_unsettled       <= '0;
    end else begin
      if (entry_valid && (class_num <= 8'(MAX_CLASS))) begin
        // Already in some group? Then this class has two.
        count_for_class = '0;
        for (int g = 1; g <= N_GROUPS; g = g + 1)
          if (seen[class_num][g]) count_for_class = count_for_class + 4'd1;

        if (count_for_class != 4'd0 && !seen[class_num][int'(group_id)]) begin
          n_multi_assigned <= n_multi_assigned + 8'd1;
          if (first_multi_class == 8'd0)
            first_multi_class <= class_num;
        end
        seen[class_num][int'(group_id)] <= 1'b1;
      end

      if (prov_valid) begin
        if (prov_founded)  n_founded   <= n_founded   + 4'd1;
        if (prov_founded && !prov_settled)
          n_unsettled <= n_unsettled + 4'd1;
      end
    end
  end

  always_comb begin
    // A partition requires every member in exactly one class. One
    // double assignment is enough to destroy it -- which is the point.
    taxonomy_is_partition  = (n_multi_assigned == 8'd0);
    every_group_founded    = (n_founded == 4'(N_GROUPS));
    // And when it is not a partition, a priority rule is not optional:
    // something has to decide which group a dual member reports under.
    priority_rule_required = !taxonomy_is_partition;
  end

endmodule

// ---------------------------------------------------------------------
// question_model -- given a question, decide what it probes and whether
// a strong answer to it is even possible.
//
// The module's purpose is to catch a question that CANNOT discriminate
// before it is asked, which is Section 14's first prohibition and the
// interview form of Chapter 26.1 Section 20's class 121.
// ---------------------------------------------------------------------
module question_model
  import probe_pkg::*;
(
  input  logic          clk,
  input  logic          rst_n,

  input  logic          q_valid,
  input  logic          answer_is_a_fact,      // one correct string
  input  logic          answer_has_derivation,
  input  logic [3:0]    chapters_required,
  input  logic          common_wrong_answer_exists,
  input  logic [7:0]    max_refutation_count,  // of the best answer

  output logic          out_valid,
  output logic          probes_recall,
  output logic          probes_derivation,
  output logic          probes_composition,
  output logic          question_can_discriminate,
  output logic [7:0]    discrimination_range,
  output logic          is_usable
);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      out_valid                 <= 1'b0;
      probes_recall             <= 1'b0;
      probes_derivation         <= 1'b0;
      probes_composition        <= 1'b0;
      question_can_discriminate <= 1'b0;
      discrimination_range      <= '0;
      is_usable                 <= 1'b0;
    end else begin
      out_valid <= q_valid;
      if (q_valid) begin
        // A question with one correct string probes preparation. That
        // is real information and it is not engineering information.
        probes_recall      <= answer_is_a_fact && !answer_has_derivation;
        probes_derivation  <= answer_has_derivation &&
                              (chapters_required <= 4'd1);
        probes_composition <= answer_has_derivation &&
                              (chapters_required >= 4'd2);

        // The range of refutation counts the question admits. A fact
        // admits exactly one value -- zero -- so its range is zero and
        // it cannot separate two candidates who both know it.
        discrimination_range <= answer_is_a_fact ? 8'd0
                                                 : max_refutation_count;
        question_can_discriminate <= (max_refutation_count > 8'd1) &&
                                     !answer_is_a_fact;

        // Section 2's four-row usability test, as one conjunction.
        is_usable <= common_wrong_answer_exists &&
                     answer_has_derivation &&
                     (max_refutation_count > 8'd1);
      end
    end
  end

endmodule

// ---------------------------------------------------------------------
// vocabulary_detector -- score one answer two ways and report when the
// two disagree.
//
// The keyword score is included precisely so that its failure is
// visible: it is what an automated screen computes, and Section 4's
// four answers are ranked by it in almost the reverse order.
// ---------------------------------------------------------------------
module vocabulary_detector
  import probe_pkg::*;
(
  input  logic         clk,
  input  logic         rst_n,

  input  logic         ans_valid,
  input  logic [7:0]   n_expected_terms_present,   // the keyword score
  input  logic [7:0]   n_expected_terms_total,
  input  logic [7:0]   refutation_count,           // Section 5
  input  logic [7:0]   n_quantities,
  input  logic         quantity_adapted_to_inputs, // the rate was applied

  output logic         out_valid,
  output logic [19:0]  keyword_score_ppm,
  output logic [7:0]   falsifiability_score,
  output logic         graders_disagree,
  output logic         is_vocabulary,      // high words, zero refutation
  output logic         is_model,           // refutation, whatever the words
  output logic         recites_reference   // a quantity that did not move
);

  logic [19:0] kw;

  always_comb begin
    kw = (n_expected_terms_total == 8'd0) ? 20'd0
       : 20'((int'(n_expected_terms_present) * 1000000)
             / int'(n_expected_terms_total));
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      out_valid            <= 1'b0;
      keyword_score_ppm    <= '0;
      falsifiability_score <= '0;
      graders_disagree     <= 1'b0;
      is_vocabulary        <= 1'b0;
      is_model             <= 1'b0;
      recites_reference    <= 1'b0;
    end else begin
      out_valid            <= ans_valid;
      keyword_score_ppm    <= kw;
      falsifiability_score <= refutation_count;

      // The two failure modes the keyword grader cannot see.
      is_vocabulary <= (kw >= 20'd800000) && (refutation_count == 8'd0);
      is_model      <= (refutation_count >= 8'd2);

      // Chapter 23.4 Section 7's 149: correct at 100 Gb/s, wrong at 400.
      // A quantity that does not move with the inputs is a recitation
      // with a number in it, which scores highest of all on keywords.
      recites_reference <= (n_quantities != 8'd0) &&
                           !quantity_adapted_to_inputs;

      // The headline: the two graders rank this answer differently.
      graders_disagree <= ((kw >= 20'd800000) && (refutation_count < 8'd2))
                       || ((kw <  20'd400000) && (refutation_count >= 8'd3));
    end
  end

endmodule

// ---------------------------------------------------------------------
// probe_telemetry -- what a panel should be able to read about its own
// process, as counters rather than impressions.
//
// Every output here is a property of the INTERVIEW rather than of the
// candidate, which is the distinction Section 14 is built on.
// ---------------------------------------------------------------------
module probe_telemetry
  import probe_pkg::*;
(
  input  logic          clk,
  input  logic          rst_n,
  input  logic          session_start,

  input  logic          q_asked,
  input  logic          q_can_discriminate,   // Section 11
  input  logic          q_inputs_supplied,    // prohibition 2 violated
  input  logic          ans_valid,
  input  logic [7:0]    ans_refutation_count,
  input  logic          ans_is_vocabulary,
  input  logic          ans_recites_reference,
  input  logic          graded_by_keyword,    // prohibition 3 violated
  input  logic          graded_as_adjective,  // prohibition 5 violated
  input  logic          reference_input_changed,

  output logic [7:0]    c_questions,
  output logic [7:0]    c_discriminating,
  output logic [7:0]    c_inputs_supplied,
  output logic [15:0]   sum_refutation,
  output logic [7:0]    c_vocabulary_answers,
  output logic [7:0]    c_reference_recitations,
  output logic [19:0]   discriminating_share_ppm,
  output logic [15:0]   mean_refutation_x100,
  output logic          v_nondiscriminating_question,
  output logic          v_inputs_supplied,
  output logic          v_keyword_grading,
  output logic          v_adjective_recorded,
  output logic          v_reference_untested,
  output logic          session_is_informative
);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n || session_start) begin
      c_questions             <= '0;
      c_discriminating        <= '0;
      c_inputs_supplied       <= '0;
      sum_refutation          <= '0;
      c_vocabulary_answers    <= '0;
      c_reference_recitations <= '0;
    end else begin
      if (q_asked) begin
        c_questions <= c_questions + 8'd1;
        if (q_can_discriminate)
          c_discriminating <= c_discriminating + 8'd1;
        if (q_inputs_supplied)
          c_inputs_supplied <= c_inputs_supplied + 8'd1;
      end
      if (ans_valid) begin
        sum_refutation <= sum_refutation + 16'(ans_refutation_count);
        if (ans_is_vocabulary)
          c_vocabulary_answers <= c_vocabulary_answers + 8'd1;
        if (ans_recites_reference)
          c_reference_recitations <= c_reference_recitations + 8'd1;
      end
    end
  end

  always_comb begin
    discriminating_share_ppm = (c_questions == 8'd0) ? 20'd0
      : 20'((int'(c_discriminating) * 1000000) / int'(c_questions));
    mean_refutation_x100 = (c_questions == 8'd0) ? 16'd0
      : 16'((int'(sum_refutation) * 100) / int'(c_questions));

    v_nondiscriminating_question = (c_discriminating < c_questions);
    v_inputs_supplied            = (c_inputs_supplied != 8'd0);
    v_keyword_grading            = graded_by_keyword;
    v_adjective_recorded         = graded_as_adjective;
    // A quantity accepted without moving an input. Prohibition 4.
    v_reference_untested         = (c_reference_recitations != 8'd0) &&
                                   !reference_input_changed;
    // A session is informative when its questions could separate
    // candidates and its record is numeric.
    session_is_informative = (c_questions != 8'd0) &&
                             !v_nondiscriminating_question &&
                             !v_adjective_recorded;
  end

endmodule

// ---------------------------------------------------------------------
// probe_conformance -- the sign-off gate for an interview process,
// in the same shape as Chapter 26.1 Section 16, Chapter 26.2 Section 16
// and Chapter 26.3 Section 16.
//
// The design rule is identical and it is the track's last statement of
// it: every check must be able to fail on a process somebody would
// really run, and the gate must say so about itself.
// ---------------------------------------------------------------------
module probe_conformance
  import probe_pkg::*;
(
  input  logic          clk,
  input  logic          rst_n,
  input  logic          evaluate,

  input  logic [7:0]    c_questions,
  input  logic [7:0]    c_discriminating,
  input  logic [7:0]    c_inputs_supplied,
  input  logic [7:0]    c_reference_recitations,
  input  logic          reference_input_changed,
  input  logic          graded_by_keyword,
  input  logic          graded_as_adjective,
  input  logic          diagnostic_question_asked,   // Section 12
  input  logic          mechanisms_requested,        // the "how?" follow-up
  input  logic [15:0]   sum_refutation,

  output logic          c1_questions_discriminate,
  output logic          c2_inputs_withheld,
  output logic          c3_not_keyword_graded,
  output logic          c4_references_tested,
  output logic          c5_record_is_numeric,
  output logic          c6_diagnostic_asked,
  output logic          c7_mechanisms_requested,
  output logic [2:0]    n_failures,
  output logic          conformant,
  output logic          gate_can_fail
);

  logic [2:0] fails;

  always_comb begin
    // 1. Every question could separate two candidates. Section 11.
    c1_questions_discriminate = (c_questions != 8'd0) &&
                                (c_discriminating == c_questions);

    // 2. No question had its own inputs supplied. Prohibition 2.
    c2_inputs_withheld        = (c_inputs_supplied == 8'd0);

    // 3. Grading was not by term presence. Prohibition 3.
    c3_not_keyword_graded     = !graded_by_keyword;

    // 4. Every reference value was tested by moving an input, or none
    //    was offered. Prohibition 4.
    c4_references_tested      = (c_reference_recitations == 8'd0) ||
                                reference_input_changed;

    // 5. The record is integers. Prohibition 5.
    c5_record_is_numeric      = !graded_as_adjective;

    // 6. Section 12's question was asked at least once.
    c6_diagnostic_asked       = diagnostic_question_asked;

    // 7. And its list was tested for mechanisms. Section 4's weakness.
    c7_mechanisms_requested   = !diagnostic_question_asked ||
                                mechanisms_requested;

    fails = 3'(!c1_questions_discriminate) + 3'(!c2_inputs_withheld)
          + 3'(!c3_not_keyword_graded)     + 3'(!c4_references_tested)
          + 3'(!c5_record_is_numeric)      + 3'(!c6_diagnostic_asked)
          + 3'(!c7_mechanisms_requested);

    // A session with no questions passes checks 2 to 5 trivially and
    // fails 1 and 6, which is the correct outcome -- but the bit is
    // here because the track's last gate should state its own premise.
    gate_can_fail = (c_questions != 8'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. Falsifiability is exactly a non-zero refutation count.
p_falsifiable_iff_nonzero: assert property (@(posedge clk) disable iff (!rst_n)
  out_valid |-> (is_falsifiable == (refutation_count != 8'd0)));

// 2. And recitation is exactly its complement.
p_recitation_complement: assert property (@(posedge clk) disable iff (!rst_n)
  out_valid |-> (is_recitation != is_falsifiable));

// 3. A zero count with a quantity is a recitation, not an absence --
//    the most deceptive kind, because it looks quantitative.
p_zero_with_quantity: assert property (@(posedge clk) disable iff (!rst_n)
  (out_valid && $past(n_refuting_observations) == 8'd0 && $past(has_quantity))
    |-> (kind == ANS_RECITATION));

// 4. A derived quantity composing two or more chapters is COMPOSED.
p_composed_needs_two: assert property (@(posedge clk) disable iff (!rst_n)
  (out_valid && kind == ANS_COMPOSED) |-> ($past(n_chapters_composed) >= 4'd2));

// 5. The reference-value flag needs a quantity that did not adapt.
p_ref_risk_definition: assert property (@(posedge clk) disable iff (!rst_n)
  out_valid |-> (reference_value_risk ==
                 ($past(has_quantity) && $past(quantity_copied))));

// 6. The grade never depends on any term being present -- there is no
//    such input. Expressed as: two answers with equal structure grade
//    equally.
p_grade_is_structural: assert property (@(posedge clk) disable iff (!rst_n)
  ($past(n_refuting_observations) == $past(n_refuting_observations, 2) &&
   $past(has_quantity) == $past(has_quantity, 2) &&
   $past(quantity_is_derived) == $past(quantity_is_derived, 2) &&
   $past(n_chapters_composed) == $past(n_chapters_composed, 2) &&
   out_valid && $past(out_valid))
    |-> (kind == $past(kind)));

// 7. Every producer of the taxonomy maps to exactly one group family.
p_producer_total: assert property (@(posedge clk) disable iff (!rst_n)
  out_valid |-> (producer_of(GRP_PREMISE) == PROD_CUSTODIAN));

// 8. And group 6 maps to the specification, which is the producer whose
//    members do not pass. Section 10.
p_designed_is_spec: assert property (@(posedge clk) disable iff (!rst_n)
  out_valid |-> (producer_of(GRP_DESIGNED) == PROD_SPEC));

c_recitation_seen: cover property (@(posedge clk) out_valid && is_recitation);
c_composed_seen: cover property (@(posedge clk) out_valid && kind == ANS_COMPOSED);

// 9. The four dispositions partition the offers.
p_offers_partition: assert property (@(posedge clk) disable iff (!rst_n)
  (n_counted + n_no_mechanism + n_irrelevant + n_duplicate == n_offered));

// 10. Counted never exceeds offered.
p_counted_le_offered: assert property (@(posedge clk) disable iff (!rst_n)
  (n_counted <= n_offered));

// 11. An observation with no mechanism never counts, whatever else is
//     true of it. Section 4's padding defence.
p_no_mechanism_never_counts: assert property (@(posedge clk) disable iff (!rst_n)
  (obs_valid && !obs_has_mechanism)
    |-> ##1 (n_counted == $past(n_counted)));

// 12. Precision is bounded and is a proper fraction.
p_precision_bounded: assert property (@(posedge clk) disable iff (!rst_n)
  (precision_ppm <= 20'd1000000));

// 13. Falsifiability follows the counted total, not the offered one.
p_falsifiable_from_counted: assert property (@(posedge clk) disable iff (!rst_n)
  (answer_is_falsifiable == (n_counted != 8'd0)));

// 14. Padding needs volume as well as a poor ratio -- two offers and
//     one hit is not padding.
p_padding_needs_volume: assert property (@(posedge clk) disable iff (!rst_n)
  padding_detected |-> (n_offered >= 8'd4));

// 15. A restart clears everything.
p_restart_clears: assert property (@(posedge clk) disable iff (!rst_n)
  answer_start |-> ##1 (n_offered == 8'd0 && n_counted == 8'd0));

c_padding_seen: cover property (@(posedge clk) padding_detected);
c_perfect_precision: cover property (@(posedge clk)
  n_offered >= 8'd3 && precision_ppm == 20'd1000000);

// 16. Classes and assignments are counted separately and assignments
//     never fall below classes. Chapter 26.2 Section 20's class 122 is
//     the reason both exist.
p_assignments_ge_classes: assert property (@(posedge clk) disable iff (!rst_n)
  (n_assignments >= n_classes_seen));

// 17. Their difference is exactly the multi-group count.
p_difference_is_multi: assert property (@(posedge clk) disable iff (!rst_n)
  (n_assignments - n_classes_seen == n_multi_group));

// 18. The unassigned count closes the series.
p_unassigned_closes: assert property (@(posedge clk) disable iff (!rst_n)
  (n_classes_seen + n_unassigned == 8'(N_CLASSES)));

// 19. The explicit share is a proper fraction of 124.
p_explicit_share: assert property (@(posedge clk) disable iff (!rst_n)
  (explicit_share_ppm <= 20'd1000000));

// 20. The per-group totals sum to the assignment count.
p_groups_sum: assert property (@(posedge clk) disable iff (!rst_n)
  census_start |-> ##1 (per_group[1] + per_group[2] + per_group[3] +
                        per_group[4] + per_group[5] + per_group[6] +
                        per_group[7] + per_group[8] + per_group[9] +
                        per_group[10] + per_group[11] + per_group[12]
                        == n_assignments));

// 21. The denominator flag is exactly the explicit equality.
p_denominator_flag: assert property (@(posedge clk) disable iff (!rst_n)
  (census_is_over_explicit == (n_explicit == n_assignments)));

c_multi_group_seen: cover property (@(posedge clk) n_multi_group != 8'd0);

// 22. A partition means no class has two groups.
p_partition_definition: assert property (@(posedge clk) disable iff (!rst_n)
  (taxonomy_is_partition == (n_multi_assigned == 8'd0)));

// 23. And when it is not a partition, a priority rule is required.
p_rule_required: assert property (@(posedge clk) disable iff (!rst_n)
  (priority_rule_required != taxonomy_is_partition));

// 24. The first multi-assigned class is recorded, because "which one"
//     is the whole finding and a count does not say.
p_first_multi_recorded: assert property (@(posedge clk) disable iff (!rst_n)
  (n_multi_assigned != 8'd0) |-> (first_multi_class != 8'd0));

// 25. An unsettled group is a founded group, always.
p_unsettled_subset: assert property (@(posedge clk) disable iff (!rst_n)
  (n_unsettled <= n_founded));

// 26. Every group founded means twelve.
p_all_founded: assert property (@(posedge clk) disable iff (!rst_n)
  (every_group_founded == (n_founded == 4'(N_GROUPS))));

// 27. Re-asserting a class into a group it already has changes nothing.
p_idempotent: assert property (@(posedge clk) disable iff (!rst_n)
  (entry_valid && seen[class_num][int'(group_id)])
    |-> ##1 (n_multi_assigned == $past(n_multi_assigned)));

c_not_partition: cover property (@(posedge clk) !taxonomy_is_partition);
c_unsettled_group: cover property (@(posedge clk) n_unsettled != 4'd0);

// 28. A factual question has a discrimination range of zero.
p_fact_range_zero: assert property (@(posedge clk) disable iff (!rst_n)
  (out_valid && $past(answer_is_a_fact)) |-> (discrimination_range == 8'd0));

// 29. And therefore cannot discriminate.
p_fact_cannot_discriminate: assert property (@(posedge clk) disable iff (!rst_n)
  (out_valid && $past(answer_is_a_fact)) |-> !question_can_discriminate);

// 30. The three probe kinds are mutually exclusive.
p_probe_exclusive: assert property (@(posedge clk) disable iff (!rst_n)
  out_valid |-> $onehot0({probes_recall, probes_derivation,
                          probes_composition}));

// 31. Usability requires all three of Section 2's conditions.
p_usable_conjunction: assert property (@(posedge clk) disable iff (!rst_n)
  (out_valid && is_usable) |-> ($past(common_wrong_answer_exists) &&
                                $past(answer_has_derivation) &&
                                ($past(max_refutation_count) > 8'd1)));

// 32. Composition needs two chapters.
p_composition_two: assert property (@(posedge clk) disable iff (!rst_n)
  (out_valid && probes_composition) |-> ($past(chapters_required) >= 4'd2));

// 33. Vocabulary is high keyword score and zero refutation.
p_vocabulary_definition: assert property (@(posedge clk) disable iff (!rst_n)
  (out_valid && is_vocabulary) |-> (keyword_score_ppm >= 20'd800000) &&
                                   (falsifiability_score == 8'd0));

// 34. Model and vocabulary are never both high.
p_model_xor_vocabulary: assert property (@(posedge clk) disable iff (!rst_n)
  out_valid |-> !(is_model && is_vocabulary));

// 35. A quantity that did not move with the inputs is flagged.
p_reference_recited: assert property (@(posedge clk) disable iff (!rst_n)
  (out_valid && $past(n_quantities) != 8'd0 &&
   !$past(quantity_adapted_to_inputs)) |-> recites_reference);

// 36. The keyword score is a proper fraction.
p_keyword_bounded: assert property (@(posedge clk) disable iff (!rst_n)
  (keyword_score_ppm <= 20'd1000000));

c_graders_disagree: cover property (@(posedge clk) out_valid && graders_disagree);
c_low_words_high_refutation: cover property (@(posedge clk)
  out_valid && keyword_score_ppm < 20'd400000 && falsifiability_score >= 8'd3);

// 37. Discriminating questions are a subset of questions asked.
p_disc_subset: assert property (@(posedge clk) disable iff (!rst_n)
  (c_discriminating <= c_questions));

// 38. And the flag is the strict inequality.
p_nondisc_flag: assert property (@(posedge clk) disable iff (!rst_n)
  (v_nondiscriminating_question == (c_discriminating < c_questions)));

// 39. The share is a proper fraction.
p_share_bounded: assert property (@(posedge clk) disable iff (!rst_n)
  (discriminating_share_ppm <= 20'd1000000));

// 40. Supplying a question's own inputs is counted, every time.
p_inputs_counted: assert property (@(posedge clk) disable iff (!rst_n)
  (q_asked && q_inputs_supplied)
    |-> ##1 (c_inputs_supplied == $past(c_inputs_supplied) + 8'd1));

// 41. A session with an adjective record is never informative.
p_adjective_not_informative: assert property (@(posedge clk) disable iff (!rst_n)
  graded_as_adjective |-> !session_is_informative);

// 42. No output of the telemetry depends on the candidate's score.
p_telemetry_ignores_score: assert property (@(posedge clk) disable iff (!rst_n)
  (session_is_informative == ((c_questions != 8'd0) &&
                              !v_nondiscriminating_question &&
                              !v_adjective_recorded)));

// 43. Gate check 1 fails on any non-discriminating question.
p_c1_fails: assert property (@(posedge clk) disable iff (!rst_n)
  (evaluate && c_discriminating < c_questions)
    |-> ##1 !c1_questions_discriminate);

// 44. Check 4 passes when no reference value was offered.
p_c4_vacuous_ok: assert property (@(posedge clk) disable iff (!rst_n)
  (evaluate && c_reference_recitations == 8'd0) |-> ##1 c4_references_tested);

// 45. Check 7's implication passes when the question was not asked --
//     check 6 already owns that failure and stacking it double-counts.
p_c7_implication: assert property (@(posedge clk) disable iff (!rst_n)
  (evaluate && !diagnostic_question_asked) |-> ##1 c7_mechanisms_requested);

// 46. And check 6 fails in exactly that case.
p_c6_fails_then: assert property (@(posedge clk) disable iff (!rst_n)
  (evaluate && !diagnostic_question_asked) |-> ##1 !c6_diagnostic_asked);

// 47. A session with no questions is never conformant.
p_no_questions_fails: assert property (@(posedge clk) disable iff (!rst_n)
  (evaluate && c_questions == 8'd0) |-> ##1 !conformant);

// 48. Conformance requires the gate to be non-trivial.
p_conformant_needs_gate: assert property (@(posedge clk) disable iff (!rst_n)
  conformant |-> $past(gate_can_fail));

// 49. The gate reads no candidate score. sum_refutation is unused and
//     the property records that deliberately.
p_gate_ignores_candidate: assert property (@(posedge clk) disable iff (!rst_n)
  (evaluate && $past(sum_refutation) != sum_refutation)
    |-> ##1 (conformant == $past(conformant, 1) || $past(evaluate)));

// 50. And the verdict holds between evaluations.
p_verdict_stable: assert property (@(posedge clk) disable iff (!rst_n)
  !evaluate |-> ##1 (conformant == $past(conformant)));

c_session_conformant: cover property (@(posedge clk) evaluate && conformant);
c_inputs_supplied: cover property (@(posedge clk) v_inputs_supplied);
c_keyword_graded: cover property (@(posedge clk) v_keyword_grading);
c_reference_untested: cover property (@(posedge clk) v_reference_untested);