CHI Assertions

Module 17 · Chapter 17.5 · CHI Verification

Project thread — 17.4 built the reference model. 17.5 formalizes rules as SVA; 17.6 measures coverage.

1. Learning Outcomes

By the end of this chapter you should be able to:

• Explain that an SVA assertion encodes a rule as a property that fires on a violation.
• Name the building blocks — implication (|->, |=>), disable iff, $past/$stable.
• State that an implication is vacuously true when its antecedent is false.
• Explain why an assertion whose antecedent never fires passes while checking nothing.
• Diagnose a vacuous ordering assertion that reports green over a real violation.
• Implement a representative checker (with a fired-counter) in SystemVerilog, Verilog-2001, and VHDL.

2. Why Should I Learn This?

Assertions are the most direct way to check a rule: instead of building a model, you state the rule as a temporal property that the simulator evaluates every cycle and fires the instant it is broken. CHI's protocol and ordering rules — a response follows its request, a barrier orders what precedes it, a field is stable while held — are naturally expressed as SVA. A good assertion is a precise, always-on checker.

But an assertion has a failure mode that makes it uniquely treacherous: vacuity. An implication antecedent |-> consequent is considered true whenever the antecedent is false — the simulator never evaluates the consequent. So an assertion whose antecedent never becomes true — because of a typo, an over-constrained condition, or the wrong signal — passes every cycle while checking nothing. A vacuous pass is indistinguishable from a real pass in the report, so it gives false confidence that a rule is verified when it was never evaluated. This chapter teaches how to write CHI assertions and how to detect vacuity — because a passing assertion whose trigger never fired is not a check at all.

3. Key Terms

4. Previous Chapter Connection

This chapter gives the language for the temporal checks the whole module has used. The $stable in Chapter 17.1, the SWMR properties in Chapter 17.2, the correlation properties in Chapter 17.3 — all were SVA, written informally. This chapter is SVA itself: implication, sampled-value functions, and the vacuity trap that lurks in every one of them.

It also sharpens Chapter 17.1's lesson. There, an accept-only checker had a temporal blind spot — it checked the wrong window. Vacuity is a related but distinct failure: the assertion's window may be right, but its trigger never fires, so the window is never entered. Both produce a green report over a real bug, and both are invisible in the pass itself — you cannot tell a rigorous assertion from a vacuous one by looking at "PASS." This chapter is the tool (SVA) and the discipline (cover the antecedent) that keeps the tool honest, setting up Chapter 17.6, where coverage extends the same idea to the whole test suite.

5. Core Concept — a passing assertion is worthless if it never fired

An SVA assertion encodes a rule as a property, but an implication is vacuously true when its antecedent is false — so a passing assertion means nothing unless its antecedent actually fired.

• An assertion is a property. It states a rule — often an implication: when the antecedent holds, the consequent must hold (same cycle |-> or next cycle |=>), suppressed during reset by disable iff.
• Implication is vacuously true on a false antecedent. When the antecedent is false, the implication is true by definition — the consequent is never evaluated. This is normal and intended.
• A never-firing antecedent passes forever. If the antecedent never becomes true (a typo, an impossible condition, the wrong signal), the assertion is vacuously true every cycle — it passes while checking nothing.
• Cover the antecedent. A passing assertion is only meaningful if its antecedent fired at least once. Pair each assertion with a cover of the antecedent; a zero-hit antecedent is a red flag — the assertion is vacuous.

The synthesis:

An SVA implication antecedent |-> consequent is vacuously true whenever the antecedent is false — the consequent is not evaluated. So an assertion whose antecedent never fires (typo, over-constraint, wrong signal) passes every cycle while checking nothing — a vacuous pass indistinguishable from a real one. A passing assertion is worthless unless its antecedent actually fired; cover the antecedent and require it to hit.

6. Engineering Mental Model — a smoke alarm that never gets tested

Think of a smoke alarm (the assertion) that is supposed to sound when there is smoke (the antecedent) — and if it does, it must alert everyone (the consequent).

• The alarm's job is conditional: if smoke, then alert. When there is no smoke, the alarm is silent — and "silent with no smoke" is exactly correct behavior. It "passes."
• Now suppose the alarm is wired to the wrong sensor — one that can never detect smoke (a broken antecedent). There is a fire every week, but this alarm's sensor never trips, so the alarm stays silent and reports itself healthy on every self-check.
• The building manager sees a green light on the alarm panel and concludes the alarm is working. But it has never once responded to actual smoke — it is silent because its trigger is dead, not because there is no danger.
• The only way to know the alarm actually works is to test its trigger: release test smoke and confirm it sounds. An alarm that has never been triggered, however green, is unverified.

The green light is a passing assertion; the dead sensor is a never-firing antecedent. You must test the trigger — cover the antecedent — or a green alarm can be one that never responds to a real fire.

7. Anatomy of a CHI Assertion

A CHI ordering assertion, built from its parts — and paired with a cover of its antecedent.

// A CHI ordering rule as SVA: a response must follow (not precede) its request.
// Anatomy: clock, disable-iff (reset), antecedent |=> consequent, sampled-value funcs.
property p_resp_follows_req;
  @(posedge clk) disable iff (!rst_n)      // sample on clk; ignore during reset
    (resp_valid && (resp_txnid == T))      // ANTECEDENT: a response for txn T is seen
    |->                                    // implication (same-cycle here)
    (req_seen[T]);                         // CONSEQUENT: T's request was already seen
endproperty
a_resp_follows_req: assert property (p_resp_follows_req);
 
// CRUCIAL COMPANION: prove the antecedent actually OCCURS, or the assert is vacuous.
c_resp_seen: cover property (@(posedge clk) disable iff (!rst_n)
                             (resp_valid && (resp_txnid == T)));

The parts: @(posedge clk) sets the sampling clock; disable iff (!rst_n) suppresses the check during reset; the antecedent (resp_valid && ...) is the trigger; |-> (or |=> for next-cycle) is the implication; the consequent (req_seen[T]) is the obligation. Sampled-value functions — $past(x) (value N cycles ago), $rose/$fell (edges), $stable (unchanged), $onehot — express behavior over time. The cover is not optional decoration: it is what proves the assertion's antecedent fires, so a pass is meaningful rather than vacuous.

8. Sampled-Value Functions and Implication

The core SVA vocabulary and the vacuity each can hide.

The rule to carry: every implication carries a vacuity risk, and every disable iff can silently switch a check off. An antecedent that is too specific (a wrong constant, a signal never driven in the test) never fires; a disable iff that is too broad (gated on a condition that is always true) suppresses the whole assertion. Both leave the assertion green and inert. The vocabulary that makes SVA powerful — conditional, temporal, resettable — is the same vocabulary that makes it easy to write a check that never runs.

9. Detecting Vacuity

How to tell a real pass from a vacuous one.

• A pass is ambiguous. "PASS" means either "the rule held every time it was checked" or "the rule was never checked." The report cannot distinguish them.
• Cover the antecedent. Add a cover property on the antecedent. If the cover hits, the antecedent fired and the assertion actually evaluated its consequent. If the cover has zero hits, the assertion is vacuous.
• Require antecedent coverage. Treat a passing assertion with a zero-hit antecedent as a failure of the verification, not a success — the rule is unverified.
• Use tool vacuity analysis. Formal and simulation tools can report vacuous passes directly; enable and act on that reporting. Do not accept a green assertion run without antecedent coverage.

The point to carry:

Vacuity is the assertion-level instance of the module's recurring theme — the health of a check is invisible in its passing output — and it is perhaps the sharpest instance, because an assertion is supposed to be the rigorous, machine-checked heart of verification, so a vacuous one betrays exactly where the team's confidence is highest. The deeper point is that an implication has two ways to be true — the consequent held, or the antecedent never fired — and only the first is verification; the second is absence of verification wearing the same green color. So a passing assertion is a claim with a precondition: "the rule held whenever it was tested," and that claim is only valuable if the rule was tested, which is precisely what antecedent coverage establishes. This reframes assertion writing as a two-part obligation: write the property and prove its trigger fires — an assertion without a covered antecedent is a half-written check. It generalizes to a verification-wide discipline: never trust a pass without evidence that the passing check ran on the interesting case. Chapter 17.6 makes this systematic — coverage is, at bottom, the discipline of proving your checks actually exercised the cases that matter.

10. Two Ordering Assertions — real vs vacuous

The same ordering rule, written two ways.

1. Real assertion — antecedent fires. (resp_valid && resp_txnid == T) |-> req_seen[T]. In the test, responses for T occur, so the antecedent fires — the consequent (req_seen[T]) is evaluated each time. If a response ever precedes its request, the assertion fails. The rule is checked.
2. Cover confirms it. The companion cover property on (resp_valid && resp_txnid == T) hits — proving the antecedent fired. The pass is meaningful.
3. Vacuous assertion — typo'd antecedent. A typo gates the antecedent on a signal that is never asserted in the test (say resp_valid && dbg_mode where dbg_mode is tied low). The antecedent never becomes true.
4. Vacuous — passes forever. The implication is vacuously true every cycle (antecedent false), so the assertion reports PASS — while never evaluating req_seen[T]. A real ordering violation (a response preceding its request) escapes, because the consequent was never checked.
5. Cover exposes it. The companion cover on the antecedent has zero hits — the red flag that the assertion is vacuous and the ordering rule is unverified.

The real assertion's covered, firing antecedent made its pass meaningful; the vacuous one's dead antecedent passed while checking nothing. The DebugLab is steps 3–4, undetected because no one checked the cover.

11. Checker / Monitor View — a rule checker with a fired-counter

The SV version is the SVA property plus its cover; the synthesizable versions flag violations and count antecedent firings, so vacuity is detectable without SVA. Representative.

// Representative CHI ordering assertion (educational) -- SVA + vacuity cover.
// Rule: a response for txn T must not precede T's request (req_seen[T] before resp).
property p_resp_follows_req;
  @(posedge clk) disable iff (!rst_n)
    (resp_valid && (resp_txnid == T)) |-> req_seen[T];   // antecedent |-> consequent
endproperty
a_order: assert property (p_resp_follows_req);
// Vacuity guard: the antecedent MUST occur, or the assertion checks nothing.
c_order: cover property (@(posedge clk) disable iff (!rst_n)
                         (resp_valid && (resp_txnid == T)));

The same rule as a Verilog-2001 synthesizable checker, with an explicit antecedent-fired counter (so vacuity is visible in tools without SVA):

// Representative ordering checker (Verilog-2001) with a vacuity counter.
module chi_order_check (
  input             clk, rst_n, resp_valid, req_seen_T,
  input             ante,          // antecedent: resp_valid && (resp_txnid==T)
  output reg        violation,
  output reg [31:0] ante_fired     // how many times the antecedent triggered (vacuity check)
);
  always @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      violation  <= 1'b0;
      ante_fired <= 32'd0;
    end else begin
      // Only evaluate the rule when the antecedent fires -- and COUNT the firing.
      if (ante) begin
        ante_fired <= ante_fired + 1'b1;         // proves the check actually ran
        violation  <= ~req_seen_T;               // consequent: request must precede
      end else begin
        violation  <= 1'b0;
      end
    end
  end
  // ante_fired == 0 at end-of-test => the checker is VACUOUS (never evaluated).
endmodule

And in VHDL:

-- Representative ordering checker (VHDL) with a vacuity counter.
library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;
 
entity chi_order_check is
  port (
    clk, rst_n   : in  std_logic;
    resp_valid   : in  std_logic;
    req_seen_T   : in  std_logic;
    ante         : in  std_logic;                  -- antecedent trigger
    violation    : out std_logic;
    ante_fired   : out unsigned(31 downto 0)       -- antecedent firings (vacuity check)
  );
end entity;
 
architecture rtl of chi_order_check is
  signal fired_q : unsigned(31 downto 0) := (others => '0');
begin
  ante_fired <= fired_q;
  process (clk, rst_n)
  begin
    if rst_n = '0' then
      fired_q   <= (others => '0');
      violation <= '0';
    elsif rising_edge(clk) then
      if ante = '1' then
        fired_q   <= fired_q + 1;          -- count each real evaluation
        violation <= not req_seen_T;       -- consequent obligation
      else
        violation <= '0';
      end if;
    end if;
  end process;
  -- fired_q = 0 at end-of-test => VACUOUS checker.
end architecture;

In all three, the rule is only evaluated when the antecedent fires, and the synthesizable versions count the firings — so a ante_fired == 0 at end-of-test reveals a vacuous checker. The DebugLab has a never-firing antecedent, so violation stays low and the count stays zero, unnoticed.

12. Assertion View — the antecedent must be covered

The properties formalize the discipline: the rule holds when triggered, and the trigger is covered.

// The ordering rule and its mandatory vacuity guard.
// 1. The rule: a response never precedes its request.
property p_order;
  @(posedge clk) disable iff (!rst_n)
    (resp_valid && (resp_txnid == T)) |-> req_seen[T];
endproperty
a_order: assert property (p_order);
 
// 2. The antecedent MUST be covered -- else a_order is vacuous.
c_ante: cover property (@(posedge clk) disable iff (!rst_n)
                        (resp_valid && (resp_txnid == T)));
 
// 3. End-of-test check: fail the run if the antecedent never fired.
//    if (c_ante.hits == 0) -> the assertion is vacuous -> verification GAP.

The system point, beyond the checks:

The pairing of an assert with a cover of its antecedent is a small pattern with an outsized payoff, and it should be as automatic as the assertion itself. The assert answers "did the rule ever break?"; the cover answers "was the rule ever tested?" — and both answers are required for the assertion to mean anything. A verification methodology that tracks only assertion pass/fail and not antecedent coverage is systematically blind to vacuity, and vacuity accumulates silently: every typo, every over-constrained trigger, every stale signal name adds another green-but-inert assertion, and the suite's apparent coverage drifts further from its real coverage with no visible symptom. The mature discipline is to make antecedent coverage a first-class metric, reported and gated alongside pass/fail, so that a passing assertion with an uncovered trigger is flagged as loudly as a failing one. This is the same principle that governs the whole module: a check's output (pass) is not evidence the check works — you need independent evidence that it ran on the interesting case. Assertions make this concrete because vacuity is so easy to introduce and so invisible without coverage; the fix is cheap (one cover per assert) and the cost of skipping it is a false-green suite.

• What it proves: the rule holds when triggered; the trigger is covered (non-vacuous).
• What it does not prove: the antecedent covers every interesting case — that is functional coverage (Chapter 17.6).
• Bug signature: a passing assertion whose antecedent cover has zero hits — vacuous.

13. Testbench — a never-firing antecedent must be exposed

Runs a checker whose antecedent never fires and confirms the fired-counter stays zero (vacuous), then one that fires.

module tb_chi_order_check;
  logic clk = 0, rst_n = 0, resp_valid, req_seen_T, ante;
  logic violation;
  logic [31:0] ante_fired;
  int errors = 0;
 
  chi_order_check dut (.*);
  always #5 clk = ~clk;
 
  initial begin
    resp_valid = 0; req_seen_T = 0; ante = 0;
    @(posedge clk) rst_n = 1;
 
    // VACUOUS phase: the antecedent NEVER fires (e.g. gated on a dead signal).
    repeat (10) begin
      @(posedge clk);
      resp_valid = $urandom_range(0,1); req_seen_T = 1; ante = 1'b0;  // ante tied low
    end
    #1;
    // A never-firing antecedent -> no violation ever, but ALSO zero evaluations = vacuous.
    if (violation) begin errors++; $display("FAIL spurious violation"); end
    if (ante_fired != 0) begin errors++; $display("FAIL ante_fired nonzero in vacuous phase"); end
    else $display("PASS vacuity detected: ante_fired = %0d (checker never ran!)", ante_fired);
 
    // REAL phase: the antecedent fires; the rule is genuinely evaluated.
    @(posedge clk) begin ante = 1; req_seen_T = 1; end   // request precedes -> legal
    @(posedge clk) ante = 0;
    #1;
    if (ante_fired == 0) begin errors++; $display("FAIL antecedent did not fire in real phase"); end
    else $display("PASS antecedent fired: ante_fired = %0d (checker ran)", ante_fired);
 
    // A genuine violation: antecedent fires but request NOT seen -> must flag.
    @(posedge clk) begin ante = 1; req_seen_T = 0; end   // response precedes request!
    #1;
    if (!violation) begin errors++; $display("FAIL real ordering violation not flagged"); end
    else $display("PASS ordering violation flagged (antecedent fired, consequent false)");
    @(posedge clk) ante = 0;
 
    if (errors == 0) $display("ALL TESTS PASSED");
    else             $display("%0d FAILURE(S)", errors);
    $finish;
  end
endmodule

Expected output:

PASS vacuity detected: ante_fired = 0 (checker never ran!)
PASS antecedent fired: ante_fired = 1 (checker ran)
PASS ordering violation flagged (antecedent fired, consequent false)
ALL TESTS PASSED

14. DebugLab — a vacuous ordering assertion

assertion: (resp_valid && dbg_mode) |-> req_seen[T]     // dbg_mode tied LOW in tests
antecedent = resp_valid && dbg_mode = resp_valid && 0 = ALWAYS FALSE
  -> implication vacuously TRUE every cycle -> assertion PASSES forever
  -> consequent req_seen[T] NEVER evaluated
DUT produces a response before its request (ordering violation)
  -> antecedent still false (dbg_mode low) -> assertion does NOT fire -> ESCAPES
cover on the antecedent: 0 hits  <-- the red flag (checker never ran)
correct: antecedent (resp_valid && resp_txnid==T) fires -> consequent checked -> violation caught

15. Common Mistakes

• Trusting a passing assertion. Assumption: green means verified. Bug: vacuous pass (the DebugLab). Prevention: cover the antecedent.
• Over-constrained antecedent. Assumption: a specific trigger is precise. Bug: it never fires. Prevention: check antecedent coverage.
• Over-broad disable iff. Assumption: suppress edge cases. Bug: the whole check is off. Prevention: minimal disable condition.
• Wrong sampled-value index. Assumption: $past(x, n) with any n. Bug: masks the trigger. Prevention: verify the timing.
• No vacuity analysis. Assumption: tools handle it. Bug: silent vacuous passes. Prevention: enable and gate on it.
• Assertion without a cover. Assumption: the property is enough. Bug: half a check. Prevention: assert + cover as a pair.

16. Engineering Checklist

• Write each rule as an SVA property with the correct implication and disable iff.
• Use sampled-value functions ($past/$rose/$stable/$onehot) for temporal behavior.
• Pair every assertion with a cover of its antecedent.
• Require the antecedent cover to hit — a zero-hit antecedent is vacuous.
• Enable tool vacuity analysis and act on it.
• Treat a passing assertion with an uncovered antecedent as a gap, not a success.

17. Key Takeaways

• An SVA assertion encodes a rule as a property that fires on a violation.
• An implication is vacuously true when its antecedent is false.
• An assertion whose antecedent never fires passes while checking nothing.
• A vacuous pass is indistinguishable from a real one in the report.
• Cover every antecedent and require it to hit — else the assertion is unverified.
• A pass is only meaningful if the check ran; the model here is representative.

18. Quick Revision

CHI assertions. SVA encodes a CHI protocol or ordering rule as a property — usually an implication antecedent |-> consequent (same cycle) or |=> (next cycle), sampled on a clock, suppressed during reset by disable iff, using sampled-value functions ($past, $rose, $stable, $onehot) for temporal behavior — that the simulator evaluates every cycle and fires on a violation. The trap is vacuity: an implication is true whenever its antecedent is false (the consequent is not evaluated), so an assertion whose antecedent never becomes true — a typo, an over-constrained condition, the wrong signal, or an over-broad disable iff — passes every cycle while checking nothing. A vacuous pass is indistinguishable from a real one in the report, giving false confidence exactly where the team trusts the check most. An implication has two ways to be true — the consequent held, or the antecedent never fired — and only the first is verification. The failure to avoid: a vacuous ordering assertion that reports green while the real ordering violation escapes. The discipline: pair every assertion with a cover property on its antecedent, require the cover to hit, enable vacuity analysis, and treat a passing assertion with a zero-hit antecedent as a gap. Write the property and prove its trigger fires. Representative model; 17.6 extends this to functional coverage.

Coming Next

Chapter 17.6 — CHI Functional Coverage. Assertions prove rules held where they were checked; coverage measures what the tests actually exercised. Chapter 17.6 covers functional coverage — coverpoints for opcodes, states, and responses, and why cross-coverage of interacting dimensions is essential, since covering each dimension alone reports 100% while a dangerous opcode-in-a-rare-state combination was never hit.