Assertions

Twenty flagship chapters of this track have each ended with thirty-odd properties and exactly one rejected class. Nobody has counted them, and counting them is where this chapter starts.

Rows three and eight are the chapter. The track has 2.7% reuse of names and 93% reuse of shapes, and the distance between those two numbers is exactly what a parameterised library is for: the same six structures, written out 1 848 times with different signal names.

And row six says why the obvious fix does not work. There are 1 230 distinct exact shapes, and 306 of them are needed to cover half the corpus — so a library of literal templates would need three hundred entries and still miss half. The families are coarse and the instances are not, which is the tension this chapter has to resolve rather than assume away.

1. Scope, and a Corpus Nobody Measured

Every chapter in Modules 5 through 20 has a properties section. None of them has ever looked at another chapter's. The result is a corpus with the structure of a library and none of the sharing.

What this chapter owns: the census and its taxonomy; a parameterised package built from the families the census finds; the anti-pattern checker built from the track's eighty-eight rejected classes; the binding mechanism; and the formal-versus-simulation question priced against Chapter 19.4 §2's network.

What it does not own: the properties themselves — each chapter's are correct where they are — and the stimulus that makes them fire, which is Chapter 20.1's. This chapter does not add checks. It asks what the existing ones have in common.

What it does not build: the scoreboards are Chapter 20.3, the coverage model is Chapter 20.4, error injection is Chapter 20.5 and the reusable agent is Chapter 20.6.

One boundary matters and it is the one the census exposes. A property has three parts, and only two of them are reusable:

Row three is why a library of assertions is harder than a library of anything else. The structure and the signals are mechanical; the claim is the engineering, and it is the part that Module 19's eighty-eight rejected classes are all about. A package that makes it easy to instantiate a wrong claim in forty places has made the track's characteristic failure cheaper to commit, which Section 20's rejected class is precisely about.

2. The Corpus, Measured

The measurement is mechanical: parse every property … endproperty block in the track's published chapters, normalise the identifiers away, and count what is left.

First, how the properties are written.

Row four is a mild surprise and a useful one: two thirds of the track's assertions already point at a named, separately declared property. The syntactic separation a library needs already exists; what does not exist is any sharing of the names.

Second, how much the names are shared.

Forty-seven names out of 1 746, and the shared ones are the obvious ones — p_broadcast_is_group, p_conformant_definition, p_change_only_when_quiet. Everything else was written once, for one block, and never looked at again.

Third, and this is the number the chapter turns on, how much the structures are shared.

Normalise each property body by replacing every identifier with a single token and keeping the operators, the system functions and the punctuation. What remains is the property's shape.

Exact shapes do not collapse the corpus, and that is the finding that kills the naive library. A package of literal templates needs 306 entries to cover half of what the track wrote.

Fourth, the coarse families — the implication kind plus the set of system functions used, with nesting ignored.

Six families cover 93.0% of 1 848 properties. Twenty-five families cover all of them. That is the library, and the gap between 1 230 and 6 is the parameterisation.

And the shape of the gap is worth naming, because it decides the package's API. The 1 230 exact shapes differ in how many terms the antecedent has, how deep the parentheses go and which comparison the consequent makes — none of which is structural. an implication whose antecedent is a conjunction and whose consequent is an equality, and one whose antecedent is a single term and whose consequent is a negation, are the same family with different expressions plugged in, and a template parameterised by two expressions covers both.

3. RTL 1 — The Library Package

// ---------------------------------------------------------------------
// assertlib_pkg -- the six families Section 2's census found, as
// parameterised checkers. Sections 3 through 7.
//
// The package does NOT contain properties. It contains modules that can
// be bound to a design, each implementing one family with its
// expressions supplied as ports. A property is a structure, some
// signals and a CLAIM; this package supplies the first two and
// deliberately supplies nothing for the third.
//
// Census: 1 848 properties, 1 230 exact shapes, 25 coarse families, and
// the top six families cover 93.0%.
// ---------------------------------------------------------------------
package assertlib_pkg;

  // The families, in census order. Section 2's table.
  typedef enum logic [2:0] {
    FAM_SAME_CYCLE      = 3'd0,   // 43.9%
    FAM_NEXT_CYCLE      = 3'd1,   // 14.4%
    FAM_SAME_HISTORY    = 3'd2,   // 12.7%
    FAM_NEXT_HISTORY    = 3'd3,   // 11.5%
    FAM_INVARIANT       = 3'd4,   //  8.4%
    FAM_DELAY_RANGE     = 3'd5,   //  2.1%
    FAM_OTHER           = 3'd6    //  7.0% across 19 families
  } family_e;

  // What a bound checker reports. Severity is a LIBRARY decision and the
  // claim's owner is a chapter, which is why both travel with the
  // instance rather than being baked into the family.
  typedef enum logic [1:0] {
    SEV_ERROR = 2'd0, SEV_WARN = 2'd1, SEV_COVER = 2'd2
  } severity_e;

  typedef struct packed {
    family_e    family;
    severity_e  severity;
    logic [7:0] rejected_class;   // 0 if this is not an anti-pattern
    logic [7:0] chapter_major;
    logic [7:0] chapter_minor;
  } prop_id_t;

  // The track's rejected classes, grouped. Section 8 derives the six
  // groups from the 88 numbered classes; this enum is the result and is
  // what Section 9's checker switches on.
  typedef enum logic [2:0] {
    ANTI_WRONG_SUBJECT   = 3'd0,  // 46, 82, 84, 88 -- the subject is not the design
    ANTI_WRONG_SCOPE     = 3'd1,  // 44, 53, 80, 81 -- granularity or partition
    ANTI_WRONG_TIME      = 3'd2,  // 43, 54, 79, 85, 87 -- when the operands hold
    ANTI_UNEVALUABLE     = 3'd3,  // 39, 74, 86 -- the environment prevents evaluation
    ANTI_UNKNOWABLE      = 3'd4,  // 34, 41, 45, 50, 76 -- nothing establishes it
    ANTI_DESIGNED_FOR    = 3'd5   // 38, 49, 77, 83 -- the design does this on purpose
  } anti_group_e;

  localparam int NUM_FAMILIES   = 7;
  localparam int NUM_ANTI_GROUP = 6;
  localparam int CENSUS_TOTAL   = 1848;
  localparam int CENSUS_SHAPES  = 1230;

endpackage

Classification: a package of types and constants, and the one place in this chapter where a design decision is encoded as an enum.

What it teaches: that the package contains no properties, and that is deliberate. A library of ready-made properties is a library of ready-made claims, and Section 20's rejected class is what happens when a claim is made easy to replicate. What the package holds is the six structures the census found and the vocabulary for talking about them — the family, the severity, the anti-pattern group and the chapter that owns the claim.

And it teaches that rejected_class travels with the instance. A property that is deliberately an anti-pattern — a demonstration, a negative test, a documented exception — carries the class number it is an instance of, so a review can find every place in an environment where class 84 was committed on purpose. Eighty-eight numbered classes are only useful if an instance can name one.

Deliberately simplified: family_e has seven values where the census found twenty-five families, with nineteen of them collapsed into FAM_OTHER at 7.0% — which is right for a package that covers 93% and wrong for one that claims completeness. chapter_major and chapter_minor are eight bits each, so this package cannot describe a chapter beyond 255. And severity_e has no SEV_INFO, which a real environment wants.

Production implication: CENSUS_TOTAL and CENSUS_SHAPES are localparams that nothing reads, and they should stay. They record the measurement the package was designed from — 1 848 properties in 1 230 shapes — so that a future maintainer wondering why the API is parameterised by expressions rather than by property names can find the number that decided it. A library whose design rationale is a measurement should carry the measurement.

4. Six Families Cover 93%

Section 2 counted the families. This section is what each one is for, because the census's ordering is not the ordering an engineer would guess.

Rank one at 43.9% is unsurprising and rank six at 2.1% is the finding. Bounded-delay properties — the ones that say "within N cycles" — are 2.1% of the corpus, and they are the family that carries almost all of the track's liveness content. Chapter 18.6's class 79 is about this family and so is Chapter 19.6's class 86.

Two per cent, and two of the eighty-eight rejected classes. The family that is hardest to write correctly is the one that is written least, which is the ratio a library should be most useful for and is exactly where a template cannot help — because what makes a bounded-delay property wrong is the bound, and the bound is the claim.

And ranks three and four together are 24.2%, while 26.8% of all properties use a history function somewhere — more than a quarter of the corpus asserting something about the past.

Row one against rows two to four is the shape of an RTL assertion corpus, and it says where a library's effort belongs: one template that gets $past's reset behaviour right is worth more than ten that wrap $onehot. $past at the first cycle after reset returns x, and a property that does not guard it fires spuriously on every reset — which is the single most common false failure in any assertion suite and is worth encoding once.

And the ordering has one more thing to say, about where a suite's risk sits relative to where its bulk sits.

Rows four and five are 10.5% of the corpus and carry most of the track's hardest classes. An unconditional invariant has no antecedent at all, so nothing limits when it must hold — which is exactly how Chapter 18.1's class 49 and Chapter 19.3's class 83 go wrong. A bounded delay carries a number that is the claim.

So a review that reads properties in census order reads 58.3% of them before reaching anything risky, and a review that reads them in reverse census order reaches the hard ten per cent first. That is a free reordering and it is the cheapest process change in this chapter.

The remaining nineteen families are 7.0% and the tail is long.

Thirteen families for 1.9% — thirty-five properties — and a library that tries to cover them has doubled its API for one property in forty. The honest boundary is the top six, with an escape hatch for everything else, and Section 6 is what that escape hatch costs.

5. RTL 2 — The Implication Checker

// ---------------------------------------------------------------------
// handshake_checker -- families 1, 2 and 6, which are 60.4% of the
// census. Sections 4 and 5.
//
// The three implication families differ only in WHEN the consequent must
// hold: the same cycle, the next cycle, or within a range. So they are
// one module with a delay parameter, and the expressions arrive as
// ports rather than as macro arguments -- which keeps the claim outside
// the library and makes the instance greppable.
//
// Census: same-cycle 43.9%, next-cycle 14.4%, delay-range 2.1%.
// ---------------------------------------------------------------------
module handshake_checker
  import assertlib_pkg::*;
#(
  parameter prop_id_t ID       = '{FAM_SAME_CYCLE, SEV_ERROR, 8'd0, 8'd0, 8'd0},
  parameter int       MIN_DLY  = 0,
  parameter int       MAX_DLY  = 0,     // MAX_DLY == MIN_DLY: a fixed delay
  parameter bit       ALLOW_UNBOUNDED = 1'b0
) (
  input  logic clk,
  input  logic rst_n,
  input  logic antecedent,
  input  logic consequent,

  output logic [31:0] c_antecedents,
  output logic [31:0] c_failures,
  output logic        never_fired
);

  // Chapter 18.6's class 79: an unbounded ##[1:$] is true of every finite
  // delay including the ones that are the failure. The library refuses to
  // build one unless the instance says so explicitly, which makes the
  // decision visible in a parameter list rather than invisible in a
  // property body.
  initial begin
    if (MAX_DLY < 0 && !ALLOW_UNBOUNDED)
      $fatal(1, "unbounded delay requires ALLOW_UNBOUNDED -- class 79");
    if (MAX_DLY < MIN_DLY)
      $fatal(1, "MAX_DLY below MIN_DLY");
  end

  generate
    if (MIN_DLY == 0 && MAX_DLY == 0) begin : g_same
      a_same: assert property (@(posedge clk) disable iff (!rst_n)
        antecedent |-> consequent)
        else c_failures <= c_failures + 1;
    end else if (MIN_DLY == MAX_DLY) begin : g_fixed
      a_fixed: assert property (@(posedge clk) disable iff (!rst_n)
        antecedent |-> ##MIN_DLY consequent)
        else c_failures <= c_failures + 1;
    end else begin : g_range
      a_range: assert property (@(posedge clk) disable iff (!rst_n)
        antecedent |-> ##[MIN_DLY:MAX_DLY] consequent)
        else c_failures <= c_failures + 1;
    end
  endgenerate

  // Section 14's prohibition: a property whose antecedent never fires is
  // indistinguishable from a passing one, and every one of the track's
  // rejected classes has this as a failure mode. The library counts it
  // for every instance rather than leaving it to a cover somebody
  // remembers to write.
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      c_antecedents <= '0;
      c_failures    <= '0;
    end else if (antecedent) begin
      c_antecedents <= c_antecedents + 1;
    end
  end

  assign never_fired = (c_antecedents == '0);

endmodule

Classification: three census families in one module, and the parameter list is where the claim's danger is made visible.

What it teaches: that ALLOW_UNBOUNDED puts Chapter 18.6's class 79 in a parameter list. An unbounded ##[1:$] is true of every finite delay, so a property that uses one has chosen not to state a bound — which is sometimes right and is usually an omission. A library that refuses to build one without an explicit opt-in turns a silent choice into a reviewable line, and that is the cheapest thing a package can do about a rejected class.

And it teaches that c_antecedents belongs to every instance, not to some. A property whose antecedent never fires passes, and so does a correct one — the two are indistinguishable from the result. Every chapter in this track has written a cover property for this by hand in some places and forgotten it in others; a library gets it for free on 1 848 instances, which is the single largest quality improvement in this chapter and costs one counter.

Deliberately simplified: the else clauses increment a counter from inside an assertion's action block, which is legal and racy — a production library uses a separate always block keyed off the assertion's failure. prop_id_t as a parameter requires SystemVerilog-2012 struct parameters, which not every tool accepts. And the expressions arrive as single-bit ports, so an antecedent that is a sequence rather than a boolean cannot be expressed — which is part of the 7.0% the top six families do not cover.

Production implication: never_fired aggregated across an environment is the report nobody produces and everybody needs. A regression with 1 848 bound properties and 600 that never fired has 600 checks that passed for no reason, and the number is invisible unless the library collects it. Chapter 20.1 §20's property 3 made the same argument about a single assertion; this is it at corpus scale, and the difference is that one is a discipline and the other is a report.

6. What a Parameter Can and Cannot Abstract

Section 2 found 1 230 exact shapes collapsing to 25 families. This section is what the collapse costs, because the difference between a shape and a family is put back somewhere.

Three things vary between two properties of the same family.

Row two is where the 1 230 shapes went. (a && b) |-> (c == d) becomes handshake_checker with antecedent = a && b and consequent = c == d, and the antecedent's structure is now a wire in the design's namespace rather than an expression in the property's. That is a real change and it has two consequences.

Row four is the cost and it is paid every time something fails. An inline property shows its own logic; a bound checker shows a boolean that came from somewhere else, and finding out where is a second step. For 1 848 properties that is 1 848 second steps, which is why libraries of this shape are often abandoned after the first difficult debug.

The mitigation is prop_id_t and it is why the package carries a chapter number. A failing instance reports which family, which severity, which chapter's claim and which rejected class it was guarding against — so the second step is a lookup rather than a search. That is not free either; it is a struct parameter on every instance, and a library that omits it has saved nothing and lost the only thing that makes binding survivable.

And row three of the first table is the boundary this chapter will not cross.

A library supplies structures. A chapter supplies claims. A package that ships claims has made it cheap to replicate a wrong one in forty places.

Which is Section 20's rejected class stated before the section that names it, because the prohibition shapes the API: handshake_checker takes two expressions and a delay and has no idea what it is checking, and that ignorance is the design.

7. RTL 3 — The History Checker

// ---------------------------------------------------------------------
// history_checker -- families 3 and 4, which are 24.2% of the census,
// and 26.8% of all properties use a history function somewhere.
// Sections 4 and 7.
//
// The whole value of this module is one guard. $past at the first cycle
// after reset returns x, and a property that does not exclude it fires
// on every reset. Every chapter in this track has written that guard by
// hand somewhere and forgotten it somewhere else; a library gets it
// right once for 447 instances.
// ---------------------------------------------------------------------
module history_checker
  import assertlib_pkg::*;
#(
  parameter prop_id_t ID    = '{FAM_SAME_HISTORY, SEV_ERROR, 8'd0, 8'd0, 8'd0},
  parameter int       DEPTH = 1,          // how far back
  parameter bit       NEXT_CYCLE = 1'b0,  // family 3 or family 4
  parameter bit       ALLOW_DECREASE = 1'b0
) (
  input  logic        clk,
  input  logic        rst_n,
  input  logic        antecedent,
  input  logic [63:0] value,

  output logic [31:0] c_antecedents,
  output logic [31:0] c_failures,
  output logic        never_fired,
  output logic        history_valid
);

  // The guard. DEPTH cycles must elapse after reset before $past has
  // anything to return, and this counter is the only correct way to
  // express that -- `disable iff (!rst_n)` does NOT cover it, because
  // reset has already been released when $past is still stale.
  logic [7:0] since_reset;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      since_reset   <= '0;
      c_antecedents <= '0;
      c_failures    <= '0;
    end else begin
      if (since_reset <= 8'(DEPTH)) since_reset <= since_reset + 1;
      if (antecedent && history_valid) c_antecedents <= c_antecedents + 1;
    end
  end

  assign history_valid = (since_reset > 8'(DEPTH));

  generate
    if (!NEXT_CYCLE) begin : g_same
      a_hist_same: assert property (@(posedge clk) disable iff (!rst_n)
        (antecedent && history_valid) |-> (value >= $past(value, DEPTH)));
    end else begin : g_next
      a_hist_next: assert property (@(posedge clk) disable iff (!rst_n)
        (antecedent && history_valid) |=> $stable(value));
    end
  endgenerate

  // Chapter 19.7 Section 14: an RMON counter is SPECIFIED to wrap, so a
  // monotonicity check is correct on twenty-six counters in that block
  // and wrong on all four of the wide ones once they roll over. The
  // parameter exists so that the exception is stated at the instance
  // rather than discovered at 0.344 seconds. Section 20's class 89.
  initial if (!ALLOW_DECREASE && ID.chapter_major == 8'd19 &&
              ID.chapter_minor == 8'd7)
    $warning("monotonicity on a wrapping counter -- see class 89");

endmodule

Classification: the family with the most instances and the single most valuable guard in the library.

What it teaches: that disable iff (!rst_n) does not protect $past. Reset is released; $past still returns x for DEPTH more cycles; the property evaluates and fires. The correct guard is an explicit counter, and it is the thing every chapter in this track has written by hand in some places and omitted in others. Getting it right once, for the 447 properties in families 3 and 4, is the clearest case in this chapter for a library existing at all.

And it teaches that ALLOW_DECREASE is class 89 in a parameter. A monotonicity template is correct on almost every counter and wrong on a counter that is specified to wrap — Chapter 19.7 §14 — and the library's uniformity is exactly what hides the exception. The warning is crude and it is in the right place: at elaboration, naming the class, next to the instance that needs the exception.

Deliberately simplified: the value port is fixed at 64 bits, so a narrow signal is zero-extended and a comparison against $past still works — but a wrapping 32-bit counter zero-extended into 64 bits never appears to wrap, which is a real hazard the parameter does not address. The monotonicity comparison is hard-coded into family 3's generate branch, where a general version takes a comparison operator as a parameter. And the initial warning tests a chapter number, which is a stand-in for a proper per-instance specification attribute.

Production implication: history_valid should be exported and aggregated, because a run whose properties were all still in their reset window proves nothing. At DEPTH = 1 the window is one cycle and nobody notices; at DEPTH = 6 — Chapter 19.4 §5's barrel — a short directed test can spend a meaningful fraction of its life inside it. The counter is eight bits and it converts "the assertion did not fire" from an unanswered question into two answered ones: it did not fire, and here is whether it could have.

8. The Rejected-Class Taxonomy

Fifty-five chapters of this track carry a rejected-class callout and the series is numbered to eighty-eight. This section is what they have in common, which nobody has asked because each was written in its own chapter.

Classifying them gives six groups, and every class falls into one.

Group 1 is the largest and the most varied. Chapter 19.4's class 84 asserts on an agreement signal; Chapter 20.1's class 88 asserts on a value the solver constructed; class 46 asserts against a re-derivation sharing an author. All three have the same shape: the property's subject was produced by something that wanted the property to pass.

Group 6 is the smallest and the most embarrassing. Chapter 18.1's class 49 asserts that no frame is dropped on a block built to drop frames; Chapter 19.3's class 83 asserts a per-instance gap bound where the standard specifies an average. These fail on correct designs, and the response — "fix the design so the assertion passes" — breaks conformance to satisfy a wrong check.

And the groups are not equally detectable, which is what makes a checker possible for some and not for others.

Row four is the only unqualified yes and it is why Section 9's checker exists. Class 74 — operands sampled in different clock domains — is a structural property of the property, and a tool can find it: trace each operand to its driving clock and compare. Class 86 — true in isolation, false in the loop — is a fanout question, and a tool can at least warn.

Rows one and three are partial and the partial part is worth having. A property whose subject is driven by a testbench module rather than by the design is class 1 or class 88 with high probability, and the connectivity is knowable. A property whose two operands come from registers separated by pipeline stages is a class 87 candidate, and the stage count is knowable.

And the groups have very different populations in the track, which is itself informative.

Column three is the useful column and it says where to look for the next one. A chapter about a partition — queues, size buckets, AXI IDs, RSS hash buckets — will produce a group 2 class, because the tempting property is always "and therefore of the whole." A chapter about a pipeline produces group 3. A chapter about a block that deliberately discards something produces group 6, and the discard is always the thing somebody wants to assert cannot happen.

Rows two, five and six are not detectable and must not be pretended otherwise. They are the claims, and Section 6's boundary is exactly this line: a library can check the structure and cannot check the claim. Three of the six groups are outside any tool's reach, which is the honest limit of everything in this chapter.

9. RTL 4 — The Anti-Pattern Checker

// ---------------------------------------------------------------------
// antipattern_checker -- find the rejected classes a tool CAN find.
// Sections 8 and 9.
//
// Section 8's table: of the six groups, one is fully detectable and two
// are partly detectable. This block implements those three and
// deliberately implements nothing for the other three, because the
// claim is not a structural property and pretending otherwise produces
// a checker that gives permission.
//
// Detectable: class 74 (operands in different clock domains), class 86
// (a property whose subject is in its own fanout), class 88 (a subject
// driven by the testbench), class 87 (operands from different pipeline
// depths).
// ---------------------------------------------------------------------
module antipattern_checker
  import assertlib_pkg::*;
#(
  parameter int NUM_OPERANDS = 2
) (
  input  logic              clk,
  input  logic              rst_n,

  // One entry per operand of the property under inspection. In a real
  // flow these come from a netlist query rather than from ports.
  input  logic [7:0]        operand_clock_id [NUM_OPERANDS],
  input  logic [7:0]        operand_stage    [NUM_OPERANDS],
  input  logic [NUM_OPERANDS-1:0] operand_from_testbench,
  input  logic [NUM_OPERANDS-1:0] operand_in_own_fanout,

  output logic              anti_74_domains,
  output logic              anti_86_loop,
  output logic              anti_87_stage_skew,
  output logic              anti_88_generated,
  output logic [2:0]        worst_group,
  output logic              clean
);

  logic [7:0] min_stage, max_stage;
  logic       mixed_clocks;

  always_comb begin
    mixed_clocks = 1'b0;
    min_stage = 8'hFF; max_stage = 8'h00;
    for (int i = 0; i < NUM_OPERANDS; i++) begin
      if (operand_clock_id[i] != operand_clock_id[0]) mixed_clocks = 1'b1;
      if (operand_stage[i] < min_stage) min_stage = operand_stage[i];
      if (operand_stage[i] > max_stage) max_stage = operand_stage[i];
    end

    // Class 74: the assertion's own sampling creates the race it
    // purports to check, so the property is unevaluable rather than
    // false. Chapter 18.1. This one is a clean structural test.
    anti_74_domains = mixed_clocks;

    // Class 86: a progress property true of a block under free inputs
    // and false inside its own feedback loop. Chapter 19.6. Detectable
    // as "an operand is in the fanout of the signal the property
    // constrains" -- a warning rather than an error, because a design
    // CAN have a correct property over its own loop if the loop's gain
    // is stated.
    anti_86_loop = |operand_in_own_fanout;

    // Class 87: operands committed at different pipeline depths, so the
    // identity holds only when the pipeline is empty. Chapter 19.7.
    anti_87_stage_skew = (max_stage - min_stage) > 8'd0;

    // Class 88: the subject was constructed by the testbench to satisfy
    // the property. Chapter 20.1. Detectable as connectivity.
    anti_88_generated = |operand_from_testbench;

    // Section 8's groups, worst first. An unevaluable property is worse
    // than a skewed one because it reports nothing at all.
    if      (anti_74_domains)    worst_group = 3'd4;
    else if (anti_86_loop)       worst_group = 3'd4;
    else if (anti_88_generated)  worst_group = 3'd1;
    else if (anti_87_stage_skew) worst_group = 3'd3;
    else                         worst_group = 3'd0;

    clean = !anti_74_domains && !anti_86_loop &&
            !anti_87_stage_skew && !anti_88_generated;
  end

endmodule

Classification: a lint rule expressed as hardware, and the only block in the track whose subject is another property.

What it teaches: that clean means "no structural anti-pattern", not "correct". Three of Section 8's six groups are undetectable — wrong scope, unknowable premise and designed-for behaviour are claims, not structures — so a property that passes this checker may still be any of them. A checker that named its output property_is_good would be giving permission it cannot give, which is why the port is called clean and why this paragraph exists.

And it teaches that anti_86_loop is a warning and the others are errors. A property over a signal in its own fanout is sometimes correct — Chapter 19.6 §20's replacement property 3 states the loop's gain and is right to — so the checker reports the shape and cannot judge it. Class 74 and class 88 have no correct instances: a property whose operands are in different clock domains is unevaluable regardless of intent, and one whose subject the testbench constructed cannot fail.

Deliberately simplified: the operand metadata arrives as ports, where a real flow extracts it from a netlist or an elaborated database — the module is the rule, not the tool. anti_87_stage_skew fires on any stage difference at all, which over-reports: Chapter 19.7 §20's replacement property 1 is a skewed identity with the skew stated, and is correct. And worst_group orders the groups by severity with no justification beyond this chapter's opinion.

Production implication: the report to generate is not a list of failures but a list of instances with a non-zero worst_group, sorted by chapter. Class 74 across an environment is usually one CDC boundary that several properties reach across, and fixing the boundary fixes all of them; class 88 is usually one testbench signal that several properties sample. The anti-patterns cluster by cause rather than by property, and a report organised by property hides the cluster — which is the same argument Chapter 19.6 §15 made about routing a finding to the person who can fix it.

10. Binding a Library to a Design

A library that must be instantiated inside the design has changed the design. bind is the mechanism that avoids it, and it has three properties worth knowing before 1 848 instances depend on them.

Row three is the one that makes a parameterised library practical. A checker bound into Chapter 19.5's async_fifo_core can take DEPTH from that instance's own parameter, so one bind statement covers every FIFO in the design at whatever depth each was built with. Without it, every instance needs its own bind with its own literal, and the library's uniformity is lost at the point of use.

And the cost is that a bind is a second place the design's structure is written down.

Rows two and four are the failure mode and they are the same failure: a bind that matches nothing elaborates cleanly. A regression with 1 848 properties, of which 300 are bound to a module that was renamed last month, runs 1 548 checks and reports success — and nothing counts the difference. The mitigation is Section 15's census at elaboration, which compares the number of bound instances against an expected count.

And there is a third property of bind that decides how the library is packaged.

A bound module is elaborated into the target's scope, so it can read the target's parameters — Section 11's DEPTH_FROM_PARENT — and it can also read the target's types. That is what makes a checker for Chapter 19.4's crc_beat_t possible without the library importing crcint_pkg: the harness imports it and the checker takes bits.

Row three is the reason the split is worth the extra file. A library that imports crcint_pkg, fifod_pkg and memif_pkg is a library for this MAC, and moving it to another design means editing it. A library that takes bits and lets a per-module harness do the importing is the same code on any design, which is the only form in which the 93% of Section 4 is actually portable.

Which gives the binding rule this chapter takes.

Bind by type, not by instance, and count what elaborated.

Binding by type covers every instance of a module automatically — including the ones added after the bind was written — and counting the result is the only way to notice when the count changes for a reason nobody intended.

11. RTL 5 — The Bind Harness

// ---------------------------------------------------------------------
// bind_harness -- one wrapper per design module, holding every checker
// that module needs and counting itself. Sections 10 and 11.
//
// The harness exists so that a bind statement names ONE module rather
// than forty checkers, and so that the elaborated instance count is a
// number somebody can compare against an expectation. Section 10's
// silent failure -- a bind that matches nothing -- is invisible without
// it.
// ---------------------------------------------------------------------
module bind_harness
  import assertlib_pkg::*;
#(
  parameter int    DEPTH_FROM_PARENT = 512,
  parameter int    CHAPTER_MAJOR     = 19,
  parameter int    CHAPTER_MINOR     = 5,
  parameter string PARENT_NAME       = "unknown"
) (
  input  logic        clk,
  input  logic        rst_n,

  // The design's signals, by name through the bind.
  input  logic        wr_en,
  input  logic        wr_full,
  input  logic [15:0] occupancy,
  input  logic        drop,

  output logic [31:0] h_antecedents,
  output logic [31:0] h_failures,
  output logic        h_any_never_fired
);

  logic [31:0] a0, a1, f0, f1;
  logic        nf0, nf1;

  // Chapter 19.5 Section 20: a full FIFO must block writes. Family 1.
  handshake_checker #(
    .ID('{FAM_SAME_CYCLE, SEV_ERROR, 8'd0,
          8'(CHAPTER_MAJOR), 8'(CHAPTER_MINOR)}),
    .MIN_DLY(0), .MAX_DLY(0)
  ) u_full_blocks (
    .clk(clk), .rst_n(rst_n),
    .antecedent(wr_en && wr_full),
    .consequent(drop),
    .c_antecedents(a0), .c_failures(f0), .never_fired(nf0)
  );

  // The occupancy never exceeds the depth this instance was built with.
  // DEPTH_FROM_PARENT is the point of binding by type: one statement,
  // every FIFO, each at its own depth. Section 10.
  handshake_checker #(
    .ID('{FAM_INVARIANT, SEV_ERROR, 8'd0,
          8'(CHAPTER_MAJOR), 8'(CHAPTER_MINOR)}),
    .MIN_DLY(0), .MAX_DLY(0)
  ) u_depth (
    .clk(clk), .rst_n(rst_n),
    .antecedent(1'b1),
    .consequent(occupancy <= 16'(DEPTH_FROM_PARENT)),
    .c_antecedents(a1), .c_failures(f1), .never_fired(nf1)
  );

  // THE census. Chapter 19.5 Section 20's class 85 warned that an
  // occupancy bound takes 13.107 ms to violate; this harness cannot fix
  // that and it can report that the check exists and fired.
  assign h_antecedents     = a0 + a1;
  assign h_failures        = f0 + f1;
  assign h_any_never_fired = nf0 || nf1;

  // Section 10's silent failure. Every elaborated harness announces
  // itself, so a run can compare the count against an expectation and
  // notice when a module rename quietly removed three hundred checks.
  initial $display("ASSERTLIB_BIND %s ch=%0d.%0d depth=%0d",
                   PARENT_NAME, CHAPTER_MAJOR, CHAPTER_MINOR,
                   DEPTH_FROM_PARENT);

endmodule

Classification: a container, and the only block in this chapter whose most important line is a $display.

What it teaches: that the elaboration message is the mechanism, not a debug aid. A bind that matches nothing elaborates cleanly and reports nothing, so the only evidence that 300 checkers vanished is that 300 fewer harnesses announced themselves. Counting the announcements and comparing against a checked-in expectation turns Section 10's silent failure into a diff, and it costs one line per harness.

And it teaches that DEPTH_FROM_PARENT is what binding by type buys. A single bind async_fifo_core bind_harness #(.DEPTH_FROM_PARENT(DEPTH)) u_h (...); covers every FIFO instance at whatever depth each was built with — including instances added after the bind was written. Binding by instance would need one statement per FIFO with a literal depth, which is where a parameterised library quietly becomes a hand-written one.

Deliberately simplified: the harness holds two checkers for one design module, where a real one holds ten to forty and is generated rather than written. PARENT_NAME is a string parameter passed by hand, which %m supplies automatically in most tools. And the harness's ports are the design's signals by name, so it is not reusable across modules — a per-module harness is the intended granularity, and the library is the checkers rather than the harness.

Production implication: the ASSERTLIB_BIND line is the input to a script that nobody writes until the first time three hundred checks disappear. Write it first. The comparison is a sorted list against a checked-in file, it fails loudly when a module is renamed, and it is the only defence against a bind that matches nothing — a failure mode that costs nothing to detect and is invisible to every other part of the flow.

12. Formal or Simulation: the 8 512-Term Network

Chapter 19.4 §2 generated a 512-bit CRC matrix and counted it: 8 512 XOR terms, 544 inputs, 32 outputs. This section asks how to prove it correct, and the answer is decided by a property of the function rather than by its size.

The input space is not the issue and is worth stating so it can be dismissed.

A simulation-based argument over that space is not an argument. But the function is linear over GF(2) — Chapter 6.4 §2 — and that changes everything about what a finite number of vectors proves.

A linear function is determined entirely by its action on unit vectors. So:

Five hundred and forty-four evaluations settle it exactly, and they are the same 544 evaluations Chapter 19.4 §3 uses to generate the matrix in the first place. The generation procedure and the proof are the same computation, which is an unusually happy situation and is worth recognising when it occurs.

So the formal-versus-simulation question has an answer specific to this block.

Row four is the trap and it is the one a team reaches for. XOR-heavy circuits are the classic hard case for conflict-driven SAT — every output is a parity, and parity constraints defeat clause learning — so the tool that is generically right for equivalence checking is specifically wrong for this circuit. A linear-algebra engine, or 544 simulations, settles it immediately.

Which generalises into the rule this chapter takes from the exercise.

Before choosing formal or simulation, ask whether the function is linear. If it is, a number of vectors equal to its input count is a proof; if it is not, no practical number of vectors is anything.

And the rule has a second half that matters more for the rest of the MAC.

And there is a fourth option that this table's framing hides, which is to prove a property of the generator rather than of the network.

Chapter 19.4 §3 generates the matrix from the polynomial at elaboration. So the network is not written; it is computed by a function, and proving that function correct proves every network it will ever produce — at 64 bits, at 512, at 2 048.

Row two is a different and better result and it is available only because the matrix is generated rather than checked in. Chapter 6.4 §3's argument for generating it was that there is nothing for a merge to corrupt; the verification consequence is larger — a checked-in table needs 544 vectors per width, and a generator needs one argument.

Rows two and three are exhaustively checkable because their state is tiny, which is a different reason from row one and reaches the same place. Rows four and five are where formal earns its cost, and row five is the case where simulation is not merely expensive but structurally unable to reach the answer — a liveness property inside a feedback loop is what model checking is for.

13. RTL 6 — The Linearity Prover

// ---------------------------------------------------------------------
// linearity_prover -- prove a combinational network linear over GF(2),
// and then prove it equal to a reference in 544 vectors. Section 12.
//
// Two checks, and the first is the one that licenses the second.
//   1. superposition: f(a xor b) == f(a) xor f(b) for random a, b
//   2. equivalence: f agrees with the reference on all 544 unit vectors
//
// Check 1 is a simulation check and cannot prove linearity -- it can
// only fail. Check 2 is a PROOF, conditional on linearity. Stating that
// dependency is the block's whole point: a team that runs check 2 alone
// has assumed the property that makes it a proof.
// ---------------------------------------------------------------------
module linearity_prover
#(
  parameter int N_IN  = 544,
  parameter int N_OUT = 32
) (
  input  logic              clk,
  input  logic              rst_n,

  input  logic              start,
  output logic              busy,
  output logic              done,

  // The design under test and the reference, as combinational functions
  // driven by this block's probe vector.
  output logic [N_IN-1:0]   probe,
  input  logic [N_OUT-1:0]  dut_out,
  input  logic [N_OUT-1:0]  ref_out,

  output logic [31:0]       c_superposition_checks,
  output logic              superposition_failed,
  output logic [31:0]       c_unit_vectors,
  output logic              equivalence_failed,
  output logic [15:0]       failing_input,
  output logic              proof_complete
);

  typedef enum logic [1:0] { S_IDLE, S_SUPER, S_UNIT, S_DONE } state_e;
  state_e st;
  int unsigned idx;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      st <= S_IDLE; idx <= 0; probe <= '0;
      c_superposition_checks <= '0; superposition_failed <= 1'b0;
      c_unit_vectors <= '0; equivalence_failed <= 1'b0;
      failing_input <= '0; proof_complete <= 1'b0;
    end else begin
      unique case (st)
        S_IDLE: if (start) begin st <= S_SUPER; idx <= 0; end

        // Superposition. This cannot prove linearity -- it samples.
        // What it does is fail loudly on a network that is NOT linear,
        // before the 544-vector argument is relied on.
        S_SUPER: begin
          c_superposition_checks <= c_superposition_checks + 1;
          if (dut_out !== ref_out) superposition_failed <= 1'b1;
          if (idx >= 1000) begin st <= S_UNIT; idx <= 0; end
          else idx <= idx + 1;
        end

        // The proof. 544 unit vectors determine a linear function
        // completely, so agreement on all of them IS equivalence --
        // conditional on the superposition check not having failed.
        S_UNIT: begin
          probe          <= ('1 & (1 << idx));
          c_unit_vectors <= c_unit_vectors + 1;
          if (dut_out !== ref_out) begin
            equivalence_failed <= 1'b1;
            failing_input      <= 16'(idx);
          end
          if (idx >= N_IN - 1) st <= S_DONE;
          else idx <= idx + 1;
        end

        S_DONE: begin
          // The conjunction is the claim. Neither half alone is a proof
          // and the block refuses to report one.
          proof_complete <= !superposition_failed && !equivalence_failed &&
                            (c_unit_vectors >= 32'(N_IN));
          st <= S_IDLE;
        end
      endcase
    end
  end

  assign busy = (st != S_IDLE);
  assign done = (st == S_DONE);

endmodule

Classification: a proof procedure expressed as a state machine, and the only block in the track whose output is a mathematical claim.

What it teaches: that proof_complete is a conjunction and every term is load-bearing. Five hundred and forty-four unit vectors determine a linear function completely; they determine nothing about a function that is not linear. So the block runs a superposition sample first, and a design that skips it has assumed the property that turns its 544 vectors from samples into a proof. That assumption is usually correct and it is an assumption.

And it teaches that failing_input is the whole diagnosis. A unit-vector failure names exactly one input bit — state bit i or data bit i − 32 — and one column of the matrix. Chapter 19.4 §14's failing_length names a residue class; this names a matrix column, which is finer and is available only because the probe is a unit vector rather than a frame.

Deliberately simplified: the superposition state drives no distinct vectors, so as written it compares dut_out and ref_out on whatever probe holds — a real version drives a, b and a ^ b and checks the three results, which needs three evaluations per check and a small state machine this listing elides. probe <= ('1 & (1 << idx)) is a clumsy way to write a unit vector. And proof_complete is a simulation-time claim about a combinational network, which a formal tool states more strongly and in less time.

Production implication: the 544-vector run takes milliseconds and should be a gate on every build rather than a regression test. Chapter 19.4 §21's residue sweep is a design check — it exercises the masker and the barrel — and this is a matrix check, and they answer different questions. A team that runs the sweep and not the prover has tested the plumbing around a network it never proved, and the prover costs less than a single frame of simulation.

14. What the Library Must Never Do

Six prohibitions, and the first three are about what a package is allowed to make easy.

Row one is the prohibition that shapes the API and it is worth restating as a test. Ask of any library entry: could an engineer instantiate this without knowing what it asserts? If yes, the library has shipped a claim — and Section 20's rejected class is the specific instance where that goes wrong. handshake_checker passes the test: it takes two expressions and a delay and cannot be instantiated without saying what they are.

Row four is the cheapest prohibition to satisfy and the most often violated. Every property in the track's 1 848 could have an antecedent counter and about a dozen do. The library makes it free, and the aggregate — how many of an environment's properties never fired — is a number no environment currently produces.

And rows five and six are the same failure at two granularities. A bind by instance misses new instances; a bind by type misses a renamed module. Both are silent, and the only defence is counting what elaborated — Section 11's $display, compared against a checked-in list.

The two prohibitions that look like style and are not:

Both are about what a downstream reader will assume, which is the thing a library controls least and affects most: 1 848 instances of a well-named module are 1 848 places where somebody trusted the name.

15. RTL 7 and 8 — The Property Census and Telemetry

// ---------------------------------------------------------------------
// property_census -- count the environment's own assertions, at
// elaboration and at run time. Sections 10, 11 and 15.
//
// Two numbers nobody produces: how many checkers elaborated, and how
// many of them ever saw their antecedent. The first catches Section
// 10's silent bind failure; the second catches the failure mode every
// one of the track's eighty-eight rejected classes shares.
// ---------------------------------------------------------------------
module property_census
  import assertlib_pkg::*;
#(
  parameter int EXPECTED_HARNESSES = 0,
  parameter int EXPECTED_CHECKERS  = 0
) (
  input  logic              clk,
  input  logic              rst_n,

  input  logic [15:0]       harnesses_elaborated,
  input  logic [15:0]       checkers_elaborated,
  input  logic [15:0]       checkers_never_fired,
  input  logic [31:0]       total_antecedents,
  input  logic [31:0]       total_failures,
  input  logic [2:0]        family_counts [NUM_FAMILIES],

  output logic [15:0]       fired_pct_x10,
  output logic              bind_count_wrong,
  output logic              many_never_fired,
  output logic [2:0]        dominant_family,
  output logic [15:0]       failures_per_million
);

  int unsigned best;

  // Section 10's silent failure made loud. A bind that matches nothing
  // elaborates cleanly, so the ONLY evidence is a count that moved.
  assign bind_count_wrong =
    (EXPECTED_HARNESSES != 0 && harnesses_elaborated != 16'(EXPECTED_HARNESSES)) ||
    (EXPECTED_CHECKERS  != 0 && checkers_elaborated  != 16'(EXPECTED_CHECKERS));

  assign fired_pct_x10 = (checkers_elaborated == 0) ? 16'd0
    : 16'(((32'(checkers_elaborated) - 32'(checkers_never_fired)) * 32'd1000) /
          32'(checkers_elaborated));

  // A third of an environment's properties never firing is normal on a
  // directed test and alarming on a soak. The threshold is a run-type
  // decision and the number is the point.
  assign many_never_fired = (fired_pct_x10 < 16'd500) &&
                            (total_antecedents > 32'd100000);

  assign failures_per_million = (total_antecedents == 0) ? 16'd0
    : 16'((total_failures * 32'd1_000_000) / total_antecedents);

  // Which family dominates this environment. Section 2's census over the
  // track found same-cycle implication at 43.9%; an environment whose
  // dominant family is something else has a different character and it
  // is worth knowing which.
  always_comb begin
    dominant_family = 3'd0; best = 0;
    for (int i = 0; i < NUM_FAMILIES; i++)
      if (unsigned'(family_counts[i]) > best) begin
        best = unsigned'(family_counts[i]); dominant_family = 3'(i);
      end
  end

endmodule

Classification: a meta-observability block, and the first in the track whose subject is the verification environment's own size.

What it teaches: that fired_pct_x10 is the number that says whether a clean run means anything. An environment with 1 848 checkers of which 40% never saw their antecedent has 739 checks that passed because nothing happened. That is not a failure — a directed test legitimately fires a fraction of an environment's properties — but it is the difference between "nothing broke" and "we looked." Nobody produces the number and it costs one counter per checker.

And it teaches that bind_count_wrong needs an expectation checked into a file. The block cannot know how many harnesses should elaborate; a human wrote 1 848 properties and a script can count them, and the comparison is a diff. Without the expectation the count is a number that drifts, which is how three hundred checkers disappear at a module rename and nobody notices for a quarter.

Deliberately simplified: family_counts is an unpacked array of three-bit values, which saturates at seven and is useless for an environment of this size — it is written that way to match NUM_FAMILIES and a real version uses 16-bit counters. The elaborated counts arrive as ports where a real flow accumulates them through a package-level static variable. And many_never_fired's 50% threshold is a literal.

Production implication: the pair to report at the top of every regression summary is checkers_elaborated against the expectation and fired_pct_x10. The first says the environment is intact; the second says the run exercised it. Neither is a coverage number and neither is a pass or a fail — they are the two preconditions under which a pass means something, and they are the verification-side analogue of Chapter 19.7 §13's requested-against-completed pair.

The census counts. The telemetry says what the counts mean, and its three most useful outputs are ratios across the families Section 2 found.

// ---------------------------------------------------------------------
// assertlib_telemetry -- the suite's shape, reported. Section 15.
//
// Section 2's census was a measurement of this track's published text.
// This block makes the same measurement of a LIVE environment, so that
// a team can compare its own suite against the family distribution and
// notice when it has drifted -- an environment that is 80% invariants
// is a different kind of suite from one that is 44% same-cycle
// implications, and neither is wrong.
// ---------------------------------------------------------------------
module assertlib_telemetry
  import assertlib_pkg::*;
(
  input  logic              clk,
  input  logic              rst_n,

  input  logic [15:0]       family_count [NUM_FAMILIES],
  input  logic [15:0]       anti_count   [NUM_ANTI_GROUP],
  input  logic [15:0]       checkers_elaborated,
  input  logic [15:0]       checkers_never_fired,
  input  logic [31:0]       total_antecedents,
  input  logic [31:0]       total_failures,
  input  logic [15:0]       chapters_bound,

  // Shape.
  output logic [15:0]       top_family_pct,
  output logic [15:0]       history_family_pct,
  output logic [15:0]       delay_family_pct,

  // Health.
  output logic [15:0]       vacuous_pct,
  output logic [15:0]       antecedents_per_checker,

  // Drift, against Section 2's published census.
  output logic              shape_unlike_track,
  output logic              delay_family_absent
);

  int unsigned total;

  always_comb begin
    total = 0;
    for (int i = 0; i < NUM_FAMILIES; i++) total += unsigned'(family_count[i]);
  end

  assign top_family_pct = (total == 0) ? 16'd0
    : 16'((32'(family_count[FAM_SAME_CYCLE]) * 32'd100) / 32'(total));

  assign history_family_pct = (total == 0) ? 16'd0
    : 16'(((32'(family_count[FAM_SAME_HISTORY]) +
            32'(family_count[FAM_NEXT_HISTORY])) * 32'd100) / 32'(total));

  assign delay_family_pct = (total == 0) ? 16'd0
    : 16'((32'(family_count[FAM_DELAY_RANGE]) * 32'd100) / 32'(total));

  assign vacuous_pct = (checkers_elaborated == 0) ? 16'd0
    : 16'((32'(checkers_never_fired) * 32'd100) / 32'(checkers_elaborated));

  assign antecedents_per_checker = (checkers_elaborated == 0) ? 16'd0
    : 16'(total_antecedents / 32'(checkers_elaborated));

  // Section 2's track-wide census: same-cycle 43.9%, history 24.2%,
  // delay-range 2.1%. A live suite far from those proportions is not
  // wrong and is worth a sentence in a review.
  assign shape_unlike_track = (top_family_pct > 16'd70) ||
                              (top_family_pct < 16'd20);

  // Delay-range is 2.1% of the track and carries almost all of its
  // liveness content. A suite with none has no liveness properties at
  // all, which is a finding rather than a fault.
  assign delay_family_absent = (total > 16'd100) &&
                               (family_count[FAM_DELAY_RANGE] == 16'd0);

endmodule

Classification: an observability block whose subject is the suite's own composition.

What it teaches: that delay_family_absent is the most informative bit in the block and it fires on plenty of real suites. Bounded-delay properties are 2.1% of this track's corpus and carry almost all of its liveness content — Chapter 18.6's class 79 and Chapter 19.6's class 86 both live there. A suite of two hundred properties with none of them is a suite that checks only safety, which is a legitimate scope and should be a stated one.

And it teaches that vacuous_pct and antecedents_per_checker answer different questions. The first says how many checks never fired; the second says how hard the ones that did were worked. A suite with 5% vacuous and 3 antecedents per checker has been barely exercised, and a suite with 30% vacuous and 40 000 antecedents per checker has a third of its properties aimed at a block this run did not touch. Both are useful and neither is visible from a pass or a fail.

Deliberately simplified: family_count arrives as ports where a real flow accumulates it through a package-level static during elaboration, which is how the census gets the numbers at all. shape_unlike_track compares against literals from Section 2 rather than against a configured expectation. And the divisions are combinational, needed on read.

Production implication: the line to print at the end of every regression is checkers_elaborated, vacuous_pct and delay_family_pct. The first says the suite is intact, the second says the run exercised it, and the third says whether the suite has any liveness content at all — which is the question nobody asks and which, in this track's own corpus, has the answer "2.1%."

16. RTL 9 — The Library Conformance Monitor

// ---------------------------------------------------------------------
// assertlib_conformance_monitor -- verdicts about the assertion suite.
// Section 16, and the fifteenth in Modules 18 to 20.
//
// Six verdicts. Two are about the suite's integrity, two about its
// structure, one about the anti-patterns Section 9 can detect, and one
// is the honest admission that three of Section 8's six groups are
// outside any tool's reach.
// ---------------------------------------------------------------------
module assertlib_conformance_monitor
  import assertlib_pkg::*;
#(
  parameter int MIN_FIRED_PCT_X10 = 700
) (
  input  logic              clk,
  input  logic              rst_n,

  input  logic              bind_count_wrong,
  input  logic [15:0]       fired_pct_x10,
  input  logic [15:0]       checkers_never_fired,
  input  logic              anti_74_any,
  input  logic              anti_86_any,
  input  logic              anti_87_any,
  input  logic              anti_88_any,
  input  logic              unbounded_without_optin,
  input  logic              proof_complete,
  input  logic              claims_reviewed,      // a human sets this

  output logic              suite_incomplete,
  output logic              suite_underexercised,
  output logic              structural_antipattern,
  output logic              unbounded_hidden,
  output logic              linear_block_unproven,
  output logic              claims_unreviewed,
  output logic              none_of_the_above
);

  always_comb begin
    // Integrity. Section 10's silent bind failure.
    suite_incomplete = bind_count_wrong;

    // The run did not exercise what elaborated. Section 15.
    suite_underexercised = (fired_pct_x10 < 16'(MIN_FIRED_PCT_X10));

    // The three groups Section 9 can detect. Class 74 and class 88 have
    // no correct instances; 86 and 87 can be correct and are reported.
    structural_antipattern = anti_74_any || anti_88_any;

    // Chapter 18.6's class 79, made visible by a parameter rather than
    // buried in a property body. Section 5.
    unbounded_hidden = unbounded_without_optin;

    // Section 12: a linear block has a 544-vector proof available and
    // not taking it is a choice.
    linear_block_unproven = !proof_complete;

    // THE honest verdict. Three of Section 8's six groups -- wrong
    // scope, unknowable premise, designed-for behaviour -- are claims
    // and no tool reaches them. This bit is set by a person, and
    // none_of_the_above depends on it so that a clean automated report
    // cannot be mistaken for a reviewed one.
    claims_unreviewed = !claims_reviewed;

    none_of_the_above = !suite_incomplete && !suite_underexercised &&
                        !structural_antipattern && !unbounded_hidden &&
                        !linear_block_unproven && !claims_unreviewed;
  end

endmodule

Classification: a verdict generator, and the second in the track to depend on a bit a human sets.

What it teaches: that claims_unreviewed is the verdict that makes the other five honest. Section 8 found that three of six anti-pattern groups are undetectable — they are claims, not structures — so an automated report that clears every mechanical check has said nothing about half the taxonomy. Gating none_of_the_above on a human's bit prevents a clean tool run from reading as a reviewed suite, which is the same device Chapter 19.4 §16 used for reference_is_independent and for the same reason.

And it teaches that anti_86_any and anti_87_any are inputs and appear in no verdict. Both have correct instances — Chapter 19.6 §20's replacement property 3 is a deliberate loop property and Chapter 19.7 §20's is a deliberate skewed identity — so promoting them to verdicts would fail correct suites. Section 9's checker reports them; the monitor demotes them, which is the third deliberate demotion in three chapters.

Deliberately simplified: MIN_FIRED_PCT_X10 defaults to 70%, which a directed test cannot reach and a soak should exceed — one threshold for two run types is wrong and the parameter exists to be set. linear_block_unproven assumes there is exactly one linear block, where a real MAC has the receive and transmit CRC networks and possibly a checksum engine. And claims_reviewed is a single bit for an entire suite, where the useful granularity is per chapter.

Production implication: none_of_the_above for the fifteenth time, and the first time the verdict requires a signature. A suite asserting it has an intact bind count, a run that exercised 70% of its checkers, no class-74 or class-88 instances, no hidden unbounded delays, a proved linear block and a human who has read the claims. The last clause is the expensive one and it is the only one that touches half of Section 8's taxonomy — which is the honest summary of what this entire chapter can and cannot automate.

17. The Cost of a Property

An assertion is not free at run time, and 1 848 of them is a number where the cost becomes a design decision rather than a rounding error.

Every bound property evaluates its antecedent on every clock edge it is sensitive to. At Chapter 19.1 §4's 195.3125 MHz:

Three hundred and sixty-one million evaluations for one millisecond of simulated time, against a design whose own activity in that millisecond is a few hundred thousand register updates. The assertions are the simulation, which is the shape most environments discover at the point where a regression stops fitting in a night.

And the mitigation is selection rather than deletion.

Row three is the strategy most often chosen and it is the wrong one. Disabling covers saves 6.3% of the evaluations and removes the premise checks — Chapter 20.1 §20's property 3 and Section 5's never_fired — so the run gets 6% faster and loses the ability to say whether anything was exercised. The covers are the cheapest properties in the suite and the ones that make the others meaningful.

Row two is the right one and it needs the library to support it. Binding by type — Section 10 — makes "the block under test only" a filter on the bind rather than an edit to the source, and prop_id_t's chapter fields are what the filter selects on. A library that cannot be selectively enabled is a library that gets deleted from the nightly.

And there is a cost that is not run time and is larger.

Row three is the argument for this chapter that has nothing to do with reuse. A design change that renames a signal breaks every inline property that names it and every bind that reaches it — and the bind fails loudly while the inline property may simply become vacuous. Section 10's table: a renamed signal fails elaboration, a renamed module matches nothing silently. The maintenance argument favours binding, and the silent case is why Section 11 counts.

18. What the Library Assumes

Eight assumptions, and three of them are about tools rather than about designs.

Row five is the assumption this chapter leans on hardest and it is the best-supported one in the batch. Chapter 6.4 §2 derived linearity from the polynomial's definition, and Section 13's prover samples superposition before relying on it — so the assumption is checked rather than assumed. It is also the only assumption here whose failure would invalidate a proof rather than a convenience.

Row four is an assumption about a tool's silence and it is the uncomfortable one. The library's defence against a silent bind failure — Section 11's count — exists because simulators do not warn. A simulator that did would make Section 11's $display unnecessary, and no harm is done by keeping it.

Row six is the assumption a reader should check rather than take. The census parsed property … endproperty blocks out of published MDX; it counts what the chapters show and not what a working environment would contain. The ratios are the point — 2.7% name reuse, 93% shape reuse — and they would be worth recomputing on a real repository before designing an API from them.

And two deliberately not assumed:

Row two is the boundary Section 4 drew and it is worth keeping visible. Nineteen families and 129 properties — 7.0% — are outside the package, and a library that quietly absorbs them by widening its API has traded a clear 93% for a muddy 100%.

19. The Cost, Accounted

Eight blocks, and the honest accounting is that none of them ships and all of them run.

The per-instance figures are the ones that matter and they multiply.

One hundred and eighteen thousand flops, against Module 19's entire datapath at 14 166 — a factor of 8.3 — which is why assertion logic is a simulation construct and why anybody proposing to synthesise it should be shown this table.

And the run-time cost is Section 17's.

Row four is the number that gets a regression's assertion suite disabled, and Section 17's answer is selective binding rather than deletion. prop_id_t's chapter fields exist for exactly that filter, which is the only part of this chapter's API whose justification is performance rather than correctness.

And there is one more cost that only appears at corpus scale: the cost of reading a failure.

Row four is small and it multiplies by every failure anybody ever triages, which over a project is the largest single cost in this chapter and is entirely invisible in a flop count. prop_id_t is the mitigation — a failing instance reports its family, its severity, its chapter and the rejected class it was guarding against — and a library that omits it has traded a real debugging cost for a saving it did not measure.

Module 20's running total, with two chapters built:

Which is the comparison worth ending on. The verification environment for a block is 12.6% of the block's own logic when each component is counted once and 8.3 times it when the checkers are counted per instance — and the difference between those two numbers is entirely the 1 563 bound instances Section 2's census found were written by hand, one at a time, across twenty chapters.

20. Properties Worth Asserting, and One Worth Refusing

Thirty-three properties about an assertion library, which is an unusual subject and produces an unusual set: most of them are about elaboration rather than about behaviour.

Group 1 — the library's own structure, checked at elaboration.

// An unbounded delay requires an explicit opt-in. Chapter 18.6's class
// 79 in a parameter list rather than in a property body.
a_unbounded_optin: assert property (@(posedge clk)
  (MAX_DLY >= 0) || ALLOW_UNBOUNDED);

// The delay range is well formed.
a_delay_ordered: assert property (@(posedge clk) MAX_DLY >= MIN_DLY);

// Every instance names a chapter, so a failure can be routed.
a_id_populated: assert property (@(posedge clk)
  (ID.chapter_major != 8'd0) && (ID.chapter_minor != 8'd0));

// A checker declared as an anti-pattern demonstration names its class.
a_anti_named: assert property (@(posedge clk)
  (ID.severity != SEV_COVER) || (ID.rejected_class != 8'd0));

// The family the instance claims matches the delay it was built with.
a_family_matches: assert property (@(posedge clk)
  ((MIN_DLY == 0 && MAX_DLY == 0) == (ID.family == FAM_SAME_CYCLE)) ||
  (ID.family == FAM_OTHER));

Group 2 — the history guard, which is family 3 and 4's whole value.

// $past is not consulted before it has anything to return. Section 7:
// `disable iff (!rst_n)` does NOT cover this.
a_history_guarded: assert property (@(posedge clk) disable iff (!rst_n)
  !history_valid |-> !$rose(c_antecedents));

// The guard opens exactly DEPTH cycles after reset.
a_guard_timing: assert property (@(posedge clk) disable iff (!rst_n)
  (since_reset == 8'(DEPTH) + 8'd1) |-> history_valid);

// And it never closes again.
a_guard_sticky: assert property (@(posedge clk) disable iff (!rst_n)
  history_valid |=> history_valid);

// A wrapping counter is not asserted monotonic. Section 20's class 89.
a_wrap_optin: assert property (@(posedge clk)
  ALLOW_DECREASE || (ID.chapter_major != 8'd19) || (ID.chapter_minor != 8'd7));

Group 3 — the antecedent census, which every instance carries.

// The antecedent counter advances exactly when the antecedent holds.
a_census_counts: assert property (@(posedge clk) disable iff (!rst_n)
  antecedent |=> (c_antecedents == $past(c_antecedents) + 1));

// And not otherwise.
a_census_quiet: assert property (@(posedge clk) disable iff (!rst_n)
  !antecedent |=> $stable(c_antecedents));

// never_fired is exactly the zero case.
a_never_fired_exact: assert property (@(posedge clk) disable iff (!rst_n)
  never_fired == (c_antecedents == '0));

// A failure implies an antecedent. A property cannot fail without firing.
a_failure_needs_antecedent: assert property (@(posedge clk) disable iff (!rst_n)
  $rose(c_failures) |-> (c_antecedents != '0));

Group 4 — the anti-pattern checker, where the properties are about what it may claim.

// Mixed clock domains is class 74 and has no correct instances.
a_74_is_error: assert property (@(posedge clk) disable iff (!rst_n)
  anti_74_domains |-> (worst_group == 3'd4));

// A generated subject is class 88 and has no correct instances.
a_88_is_error: assert property (@(posedge clk) disable iff (!rst_n)
  anti_88_generated |-> !clean);

// clean is a conjunction of the four detectable patterns and nothing more.
a_clean_exact: assert property (@(posedge clk) disable iff (!rst_n)
  clean == !(anti_74_domains || anti_86_loop ||
             anti_87_stage_skew || anti_88_generated));

// The checker never claims to have checked a claim.
a_no_claim_check: assert property (@(posedge clk)
  NUM_DETECTABLE_GROUPS == 3);

// Stage skew is reported and does not gate clean on its own severity.
a_87_reported: assert property (@(posedge clk) disable iff (!rst_n)
  anti_87_stage_skew |-> (worst_group != 3'd0));

Group 5 — binding and the census, where a silent failure is the subject.

// The elaborated count matches the expectation. Section 11's silent
// bind failure, made loud.
a_bind_count: assert property (@(posedge clk)
  (EXPECTED_HARNESSES == 0) ||
  (harnesses_elaborated == 16'(EXPECTED_HARNESSES)));

// Every harness announced itself.
a_harness_announced: assert property (@(posedge clk)
  harnesses_elaborated <= checkers_elaborated);

// The fired percentage is well formed.
a_fired_pct_range: assert property (@(posedge clk) disable iff (!rst_n)
  fired_pct_x10 <= 16'd1000);

// A run with no antecedents at all reports nothing fired.
a_no_antecedents: assert property (@(posedge clk) disable iff (!rst_n)
  (total_antecedents == '0) |-> (fired_pct_x10 == 16'd0));

// Failures per million is zero when there are no failures.
a_fpm_zero: assert property (@(posedge clk) disable iff (!rst_n)
  (total_failures == '0) |-> (failures_per_million == 16'd0));

Group 6 — the linearity proof, where the conjunction is the claim.

// A proof requires BOTH halves. Section 13: 544 unit vectors determine
// a LINEAR function and say nothing about any other kind.
a_proof_conjunction: assert property (@(posedge clk) disable iff (!rst_n)
  proof_complete |-> (!superposition_failed && !equivalence_failed));

// And it requires all 544 of them.
a_proof_complete_count: assert property (@(posedge clk) disable iff (!rst_n)
  proof_complete |-> (c_unit_vectors >= 32'(N_IN)));

// Superposition runs before the unit vectors.
a_superposition_first: assert property (@(posedge clk) disable iff (!rst_n)
  (st == S_UNIT) |-> (c_superposition_checks > 32'd0));

// A failing input is captured.
a_failing_input_captured: assert property (@(posedge clk) disable iff (!rst_n)
  $rose(equivalence_failed) |-> (failing_input < 16'(N_IN)));

// The prover terminates.
a_prover_terminates: assert property (@(posedge clk) disable iff (!rst_n)
  start |-> ##[1:2000] done);

Group 7 — coverage.

c_all_families:      cover property (@(posedge clk)
                       family_counts[0] != 0 && family_counts[1] != 0 &&
                       family_counts[2] != 0 && family_counts[3] != 0);
c_never_fired_zero:  cover property (@(posedge clk) checkers_never_fired == '0);
c_anti_74:           cover property (@(posedge clk) anti_74_domains);
c_anti_88:           cover property (@(posedge clk) anti_88_generated);
c_proof_done:        cover property (@(posedge clk) proof_complete);
c_bind_mismatch:     cover property (@(posedge clk) bind_count_wrong);
c_history_guard:     cover property (@(posedge clk) !history_valid);

21. Verification Scenarios

Sixty-four scenarios for a library whose subject is verification, plus a five-run directed test whose content is a corpus rather than a stimulus.

The census — 11 scenarios.

Row seven is the scenario that decides the API. Three hundred and six exact shapes for half the corpus means a library of literal templates is not buildable; row nine means a library of parameterised families is. Running both counts is what separates the two designs, and neither number is available without parsing.

The implication checker — 11 scenarios.

Rows fifteen and sixteen are class 79 turned into an elaboration decision, and the difference between them is one parameter in a review diff rather than a $ in a property body that nobody reads twice.

The history guard — 10 scenarios.

Row twenty-seven is the scenario that justifies the guard's existence, and it is the one most engineers expect to go the other way: reset is released, $past is still stale, and disable iff has already stopped disabling.

The anti-pattern checker — 10 scenarios.

Rows forty to forty-two are the chapter's honesty test. Three of Section 8's six groups pass the checker, and a checker whose output implied correctness would have certified three kinds of wrong property. clean means "no structural anti-pattern" and the scenarios exist to keep that name honest.

Binding and the census — 8 scenarios.

Rows forty-six and forty-eight are the pair that explains why the count exists, and they are the same kind of change with opposite outcomes: a renamed signal is a compile error and a renamed module is silence.

The telemetry and the suite's shape — 7 scenarios.

Row fifty-one is the finding worth printing on every summary line. Bounded-delay properties are 2.1% of this track's corpus and carry almost all of its liveness content; a suite with none of them checks only safety, which is a legitimate scope and should be a stated one rather than an accident.

The linearity proof — 7 scenarios.

Row sixty-three is Chapter 19.4 §14's trap arriving in a formal setting, and it is worth noticing that no amount of proof machinery removes it: a proof of equivalence between two things that are wrong in the same way is a valid proof of the wrong thing.

The directed test — five runs a stimulus change cannot produce.

This chapter's hard cases are properties of a corpus and of an elaboration, not of a waveform.

Row three is the expensive one and it is Chapter 19.5's class 85 again: the wrap takes 0.344 seconds of simulated time at 100 Gb/s. The constructive answer is the same — parameterise the counter's width down in a test build — and it is worth stating that two of the track's eighty-nine classes are the same underlying problem seen from different blocks.

Construct it. Five runs.

Run E is the run that proves Section 13's conjunction is not decoration. A non-linear network can agree with a linear reference on all 544 unit vectors — unit vectors do not span its behaviour — so the 544-vector check passes and the proof is invalid. Only the superposition sample catches it, and only because it was run first.

Run C is the class-89 case made cheap. A 32-bit counter wraps after 2³² octets; a 12-bit one wraps after 4 096, which is a few frames. The carry logic is width-independent and the scenario is the same, which is the technique Chapter 19.7 §21's row four described and this run uses.

The oracle, in four parts:

Rows three and four in runs D and E are the table's point. Run D fails the unit-vector check and run E passes it; both correctly report no proof, and only run E shows why the superposition half exists. A prover that reported proof_complete in run E would have certified a non-linear network as equivalent to a linear one — which is not a subtle error, and is exactly what 544 vectors alone would have concluded.

22. Debugging an Assertion Library

Four complaints, and three of them are about assertions that did not fire rather than assertions that did.

Complaint 1 — "we added three hundred checks and the runtime did not change."

Row three is the whole difficulty and row four is the only defence. A bind that matches nothing elaborates without a warning in every mainstream simulator, so the evidence is a number that did not move. Section 11's $display per harness and a checked-in expected count turn it into a diff, and the alternative is discovering it at the next tapeout review.

Complaint 2 — "the suite is green and we shipped a bug."

Row four is the cluster that matters and it is invisible per property. Forty properties whose antecedents all reference frame_end are all vacuous if frame_end never asserts, and each of them individually reports "passed." The aggregate — how many never fired, grouped by the signal they name — is the report, and it is available only because Section 5 put a counter in every instance.

Complaint 3 — "an assertion fires on every reset."

Row two is the answer most engineers reach for and it is wrong. disable iff (!rst_n) stops evaluation while reset is asserted; $past is stale for DEPTH cycles after it is released. The two windows do not overlap, and the guard has to be a counter.

Complaint 4 — "the CRC equivalence check has been running for six hours."

Row one is the trap and it is generic advice applied to a specific circuit. Combinational equivalence checking is the right tool for most networks and is specifically wrong for a parity network, where every output is an XOR of hundreds of inputs and clause learning has nothing to learn. The circuit that is hardest for the general tool is the one with a closed-form answer.

Complaint 5 — "the same property passes in simulation and fails in formal."