Assertion-Based Verification

Assertions in UVM · Module 21 · Page 21.3

The Engineering Problem

The prior chapters integrated assertions (21.1) and wrote them (21.2) — the mechanics. This chapter steps back to the methodology: what is assertion-based verification as an approach, and where does it fit? The questions are strategic, not syntactic. Who should write an assertion — the design engineer who knows the internal micro-architecture, or the verification engineer who knows the external protocol? How is an assertion checked — only in simulation (on the stimulus you happen to run), or formally proven for all inputs? When is an assertion the right tool versus the transaction-level scoreboard — and what happens when you force the wrong one (a complex data computation into an assertion, or a protocol timing rule into a scoreboard)? And the most dangerous misconception: a team with a thorough, all-passing assertion suite in simulation assumes the protocol is proven — when the assertions only checked the paths the stimulus exercised, leaving a latent violation in an un-driven path to ship. The problem this chapter solves is ABV as a methodology: assertions as executable specification, who writes them, dynamic versus formal, the trade-off with scoreboard checking, and ABV's place in the complete strategy.

Assertion-based verification (ABV) is the methodology of capturing the design's intended behavior as assertions — executable specification — and using them throughout the flow. An assertion is the spec rule written formally: unambiguous (a precise property, not ambiguous English), checkable (verified automatically every run), self-documenting (the property is the rule), and design-resident (it lives with the RTL). Who writes them depends on what they check: design engineers write white-box assertions on internal invariants (a FIFO never overflows, an FSM is one-hot) — caught early, at the source; verification engineers write black-box assertions on external protocol/spec behavior. How they're checked spans two engines: dynamic (simulation — checked on the stimulus you run, scenario-bound) and formal (property checking — a tool proves the property for all inputs or finds a counterexample, exhaustive). ABV trades off with the scoreboard: assertions for local, temporal, protocol/invariant rules (precise, early, formal-amenable); the scoreboard for end-to-end data computation (a reference model). And ABV layers into the constrained-random, coverage-driven flow — assertions check protocol/invariant rules continuously, the scoreboard checks function, coverage measures thoroughness — as one part of a complete checking strategy. This chapter is ABV the methodology: executable spec, who writes, dynamic vs formal, the scoreboard trade-off, and the layered strategy.

What is assertion-based verification as a methodology — how are assertions executable specification, who writes them (design's internal invariants versus verification's external protocol), how do dynamic simulation and formal property checking differ, when are assertions the right tool versus the scoreboard, and how does ABV layer into the complete coverage-driven flow?

Motivation — why capture the spec as assertions

A spec in English is intent; assertions turn that intent into something enforceable. The reasons ABV is a methodology, not just a technique:

• English specs are ambiguous and un-checkable. A prose rule ("the bus must not be granted to two masters") is open to interpretation and checked only by human review. An assertion is the same rule written formally — unambiguous and checked automatically, every run.
• Assertions are executable specification. The property is the rule — so it documents the exact intended behavior (self-documenting) and enforces it (checkable). The spec becomes executable, bridging intent and implementation.
• The right author knows the rule. A design engineer knows the internal invariants (the micro-architecture's assumptions); a verification engineer knows the external protocol (the spec's interface contract). Who writes an assertion follows who knows what it checks — and both contribute layered coverage.
• Dynamic and formal are two engines for the same assertions. The same property can be simulated (checked on your stimulus) and formally proven (exhaustive, all inputs). ABV spans both — and understanding the difference prevents the fatal assumption that passing in simulation means proven.
• Assertions and the scoreboard are complementary tools. Assertions excel at local, temporal rules; the scoreboard excels at end-to-end data. Choosing the right tool (and not forcing the wrong one) is part of the methodology.

The motivation, in one line: a spec in English is ambiguous intent, but assertions make it executable specification — unambiguous, checkable, self-documenting, design-resident — written by whoever knows the rule (design's internal invariants, DV's external protocol), checked by two engines (dynamic simulation, formal proof), and complementary to the scoreboard — so ABV is a methodology for capturing and enforcing the design's intent across the whole flow.

Mental Model

Hold ABV as turning the spec's contract clauses into enforceable, machine-checkable form, embedded with the design — enforced by spot-checking the runs (dynamic) or proving the perimeter (formal):

A specification is a contract describing how the design must behave, but written in English it's just intent — ambiguous, and enforced only by humans reading it. Assertion-based verification turns each contract clause into an enforceable, machine-checkable statement — a formal property — and embeds it with the design, so the contract is enforced automatically instead of trusted. Who drafts each clause depends on who knows it: the designer drafts the internal clauses about the micro-architecture's own assumptions, the verifier drafts the external clauses about the protocol the design presents to the world. And the contract can be enforced two ways: you spot-check it against the transactions you actually run (dynamic simulation — fast, but only as thorough as what you exercise), or you prove it holds for every possible input (formal — exhaustive, but bounded by the tool's reach). A contract you only spot-check is enforced where you looked; a contract you prove is enforced everywhere — and mistaking the first for the second is how a clause-violating case slips through unlooked-at. Picture the specification as a contract describing how the design must behave. Written in English, it's just intent — ambiguous, and enforced only by humans reading it. ABV turns each contract clause into an enforceable, machine-checkable statement — a formal property — and embeds it with the design, so the contract is enforced automatically instead of trusted. Who drafts each clause depends on who knows it: the designer drafts the internal clauses (the micro-architecture's own assumptions — this FIFO never overflows, this state is one-hot), the verifier drafts the external clauses (the protocol the design presents to the world). And the contract can be enforced two ways: you spot-check it against the transactions you actually run (dynamic simulation — fast, but only as thorough as what you exercise), or you prove it holds for every possible input (formal — exhaustive, but bounded by the tool's reach). A contract you only spot-check is enforced where you looked; a contract you prove is enforced everywhere — and mistaking the first for the second is how a clause-violating case slips through unlooked-at (the dynamic-isn't-proof trap). The scoreboard, by contrast, is not a clause-checker — it's the auditor computing the expected final result; you use clauses (assertions) for the protocol and invariant rules, and the auditor (scoreboard) for the end-to-end data computation.

So ABV is turning the spec's contract clauses into enforceable, machine-checkable form, embedded with the design: unambiguous (formal), enforced automatically (every run), self-documenting (the clause is the rule), drafted by whoever knows it (design: internal invariants; DV: external protocol), and enforced two ways — spot-checked on the runs (dynamic, thorough-as-your-stimulus) or proven for all inputs (formal, exhaustive). Don't mistake spot-checking for proof, and use clauses for rules, the auditor (scoreboard) for end-to-end computation. Make the spec's clauses enforceable and embedded, draft each by who knows it, and know whether you spot-checked or proved.

Visual Explanation — assertions as executable specification

The defining picture is the transformation: an English spec rule (ambiguous, human-checked) becomes a formal assertion (unambiguous, machine-checked, self-documenting, design-resident).

The figure shows the transformation of a spec rule into executable specification. An English spec rule (the warning-colored start — ambiguous, human-checked) becomes a formal assertion (the brand-colored center — executable specification) with four properties: unambiguous (a precise property, not open to interpretation), checkable (verified automatically every run, not by human review), self-documenting (the property is the rule — reading it tells you the intended behavior), and design-resident (lives with the RTL and travels with it). The crucial reading is what each property buys. Unambiguous: an English rule like "the grant must follow the request promptly" has no precise meaning (how prompt?), but req |-> ##[1:3] ack is exact — the formalization forces precision (and exposes spec ambiguities). Checkable: the rule is enforced automatically on every simulation (and formally), not dependent on a human remembering to check it. Self-documenting: the assertion documents the exact intended behavior — a new engineer reading the assertions learns the protocol (the assertions are the spec, executable). Design-resident: the assertion lives with the design (bound or inline), so it travels with the RTL across reuse, refactors, and projects — the contract follows the design. The warning-colored ambiguous spec maps through the brand-colored assertion to the success-colored properties — and together they make the assertion executable specification: it both documents and enforces the intended behavior, bridging the gap between the specification (intent) and the implementation (RTL). This is the central idea of ABV: the spec stops being a document humans interpret and becomes a contract the machine enforces. The diagram is the executable-spec transformation: English rule → formal assertion → (unambiguous, checkable, self-documenting, design-resident) — the spec made executable. An assertion is the spec rule made formal — it documents and enforces the intended behavior at once.

RTL / Simulation Perspective — who writes what, and the two engines

In code, who writes an assertion follows what it checks (internal vs external), and the same assertion serves both simulation and formal. The example shows design and DV assertions, and the dynamic/formal duality.

// === DESIGN-WRITTEN: white-box assertions on INTERNAL invariants (caught early, at the source) ===
module fifo(...);
  // the designer knows the micro-architecture — these are INTERNAL assumptions
  a_no_overflow:  assert property (@(posedge clk) (wr_en && full) |-> 0)   // never write when full
    else $error("FIFO overflow");
  a_ptr_onehot:   assert property (@(posedge clk) $onehot(state));         // FSM state is one-hot
  // a violation FIRES at the EXACT internal event → debugged at the SOURCE, during design
endmodule
 
// === VERIFICATION-WRITTEN: black-box assertions on the EXTERNAL protocol (the spec contract) ===
module bus_protocol_checker(...);   // bound to the DUT (Module 21.1)
  a_handshake:    assert property (@(posedge clk) req |-> ##[1:3] ack);    // external protocol rule
  a_mutex_grant:  assert property (@(posedge clk) !(grant0 && grant1));    // spec: one grant at a time
endmodule
 
// === THE SAME ASSERTION, TWO ENGINES ===
//  DYNAMIC (simulation): a_handshake is checked on the stimulus you RUN
//    → catches violations IN THE PATHS EXERCISED — scenario-bound (only as good as the stimulus)
//  FORMAL (property checking): a tool PROVES a_handshake holds for ALL inputs, or finds a counterexample
//    → EXHAUSTIVE — no stimulus needed — but bounded by complexity/convergence
 
// ✗ MISTAKE: a_handshake PASSES in simulation → "the protocol is proven" → NO. Only the exercised paths
//            were checked; an un-driven path may hide a latent violation (DebugLab) — cover + formal-prove

The code shows who writes what and the two engines. Design-written assertions (in the fifo module) are white-box, on internal invariants: a_no_overflow (never write when full — (wr_en && full) |-> 0) and a_ptr_onehot ($onehot(state)). The designer knows the micro-architecture, so these are internal assumptions — and a violation fires at the exact internal event, debugged at the source, during design. Verification-written assertions (in the bound bus_protocol_checker, Module 21.1) are black-box, on the external protocol: a_handshake (req |-> ##[1:3] ack) and a_mutex_grant (!(grant0 && grant1)) — the spec's interface contract. The same assertion, two engines: dynamic (simulation) checks a_handshake on the stimulus you run — catching violations in the paths exercised (scenario-bound); formal (property checking) proves a_handshake for all inputs (or finds a counterexample) — exhaustive, no stimulus, but bounded by complexity. The mistake (commented) is the cardinal one: a_handshake passing in simulation does not mean "the protocol is proven" — only the exercised paths were checked; an un-driven path may hide a latent violation (the DebugLab). The shape to carry: who writes an assertion follows what it checks — design writes internal invariants (white-box, caught early at the source), DV writes external protocol (black-box, the spec contract) — and the same assertion serves two engines: dynamic (simulation, scenario-bound) and formal (proof, exhaustive). The design assertions are especially valuable because they catch an internal bug at its source (the overflow itself) rather than late (when it corrupts an output the scoreboard sees) — early, local, pinpointed. And the dynamic/formal duality is why the same assertion library serves both the simulation and formal flows — write once, check two ways. Design writes internal invariants, DV writes external protocol — and the same assertion is simulated and formally proven.

Verification Perspective — assertions versus the scoreboard

The methodology decision is when to use an assertion versus the scoreboard — and forcing the wrong tool is a common error. Seeing the trade-off clarifies the complementary roles.

The figure shows the assertion-versus-scoreboard trade-off. Assertions fit local, temporal, protocol and invariant rules: a handshake window, a stability hold, a one-hot state, a mutual-exclusion rule — checks that are precise, fire early at the exact cycle, are cheap, and are amenable to formal proof. The scoreboard fits end-to-end data computation: the transformed output of a datapath, ordering across the whole DUT, anything needing a reference model to compute the expected result. The verification insight is that each tool has a natural domain, and forcing the wrong one fails: forcing a complex data computation into an assertion is unwieldy (an assertion can't easily compute the expected output of a multi-stage datapath — that's a reference model's job, and expressing it in SVA would be monstrous); forcing a protocol timing rule into the scoreboard misses it (the scoreboard's transaction abstraction can't see the cycle-by-cycle handshake — Module 21.1). So the decision rule is: is this a local/temporal rule about signal behavior (→ assertion) or an end-to-end computation of expected data (→ scoreboard)? A handshake, a hold, a one-hot, an ordering window → assertion (precise, early, cheap, formal-amenable). A datapath result, a transformed payload, a cross-DUT ordering of data → scoreboard (reference model). The warning-colored "rule to check" routes to the brand-colored tool by its nature, yielding the success-colored fit. This is the methodology's tool-choice: not "assertions vs scoreboard" as rivals, but complementary tools each best for a class of check — and using each for what it's good at (and not forcing the wrong one) is part of ABV as a methodology. The diagram is the tool-choice: local/temporal/protocol → assertion, end-to-end data computation → scoreboard — complementary domains, each for what it's good at. Assertions for temporal/local rules, the scoreboard for end-to-end data — don't force either into the other's domain.

Runtime / Execution Flow — ABV layered into the complete strategy

At the strategy level, ABV is one layer of a complete checking flow — combined with CRV, the scoreboard, and coverage, spanning dynamic and formal. The flow shows the integration.

The flow shows ABV layered into the complete strategy. CRV (step 1): the coverage-driven constrained-random flow (Module 20) generates and steers the stimulus. Check (step 2): on every transaction, assertions verify protocol/invariant rules (precisely, early) and the scoreboard verifies end-to-end function. Measure (step 3): coverage — functional coverage plus assertion coverage (antecedents fired) — measures thoroughness (Modules 19, 21.5). Formal (step 4): the same assertions, formally proven for all inputs — exhaustive coverage of the critical properties. The runtime insight is that ABV is not a standalone methodology — it's one layer of a complete checking strategy that combines: CRV (stimulus), assertions (protocol/invariants — this module), scoreboard (function — Module 18), coverage (thoroughness — Module 19), and formal (exhaustiveness). Each covers a role: CRV drives, assertions catch protocol/invariant bugs precisely and early, the scoreboard catches functional data bugs end-to-end, coverage measures completeness (including assertion coverage — did the assertions actually fire their checks), and formal proves the critical properties exhaustively (beyond what any stimulus exercises). The power of the combination is defense in depth across abstractions and methods: a bug escapes only if it evades all the layers. And the dynamic/formal span is key: dynamic ABV (in the CRV flow) catches what the stimulus exercises; formal ABV proves the critical properties for all inputs — together covering both the exercised and the un-exercised space. So ABV contributes the protocol/invariant checking and the formal exhaustiveness to the whole. The flow is the complete strategy: CRV (drive) → assertions + scoreboard (check) → coverage (measure) → formal (prove) — ABV as one integrated layer, spanning dynamic and formal. ABV layers into the whole: assertions for protocol and invariants, scoreboard for function, coverage for completeness, formal for exhaustiveness.

Waveform Perspective — dynamic ABV is only as good as the stimulus

The dynamic-versus-formal distinction is visible on a timeline: a dynamic assertion only checks where the stimulus drives its antecedent — an un-driven path leaves it unchecked (a latent violation hidden), while formal would prove it everywhere. The waveform shows it.

The waveform shows that dynamic ABV is scenario-bound. The handshake assertion (req |-> ack within the window) only does real work when req is driven. Where the stimulus drives req (the checked windows), the assertion actively checks and passes. But in a path the stimulus never drives req (the vacuous region), the assertion passes vacuously — it checks nothing there. A latent violation in that un-driven path (latent_bug) is never triggered by simulation, so the dynamic assertion passes overall while the bug hides. Formal property checking would prove the assertion for all inputs, catching the latent violation the stimulus never reached (formal_only). The crucial reading is the fundamental limit of dynamic ABV: an assertion in simulation is only checked where the stimulus exercises its antecedent — and where the antecedent is never driven, the assertion passes vacuously, providing zero protection there. So an all-passing assertion suite in simulation means "no violation in the paths the stimulus exercised", not "the property holds for all inputs" — and a latent violation in an un-exercised path ships, despite the passing assertions. This is exactly the coverage lesson (Module 19.1) applied to assertions: passing isn't proven unless you exercised the scenario — which is why covering the antecedents (knowing which assertions actually fired) and formally proving the critical ones are part of ABV. The picture to carry is that dynamic ABV inherits the stimulus's blind spots: it's as good as what you run, no better — while formal is exhaustive (it proves for all inputs, independent of stimulus). Reading the waveform this way — is the assertion actively checking, or vacuously passing because the stimulus never drove its antecedent? — is understanding dynamic ABV's limit. The vacuous region hiding a latent bug that formal would catch is the signature of the dynamic-isn't-proof truth: simulation checks where you looked; formal proves everywhere. A dynamic assertion is only as good as the stimulus that drives its antecedent — passing in simulation is not proof; cover the antecedents and formally prove the critical properties.

DebugLab — the all-passing assertion suite that wasn't a proof

✗ TREAT passing assertions in SIMULATION as a proof:
  // dozens of spec-faithful assertions, all PASSING, millions of cycles → "protocol proven correct"
  // BUT: the assertion for the retry-back-to-back rule passed VACUOUSLY — its antecedent was
  //      NEVER driven by the random stimulus → it checked NOTHING on that path
  // a real violation on that un-exercised path → simulation never triggered it → SHIPS
  // dynamic ABV is only as good as the stimulus; passing != proven
 
✓ COVER the antecedents + FORMALLY prove the critical assertions:
  // (a) cover property for each assertion's antecedent → know which assertions ACTUALLY fired (21.5)
  //     the retry-back-to-back cover would show 0 hits → the assertion never checked → a GAP, flagged
  // (b) formally prove the critical protocol assertions → exhaustive, all inputs, no stimulus needed
  //     formal would find the retry-back-to-back counterexample → caught before tapeout
  // passing in sim = "no violation in exercised paths"; proven = formal or covered-and-exercised

Common Mistakes

• Equating passing assertions in simulation with proof. Dynamic ABV only checks exercised paths; cover antecedents and formally prove critical properties for real assurance.
• Not covering antecedents. A passing assertion whose antecedent never fired verified nothing; cover property confirms it actually checked.
• Forcing a data computation into an assertion. Complex end-to-end expected-output computation belongs in a scoreboard reference model, not an unwieldy SVA property.
• Forcing a protocol timing rule into the scoreboard. The transaction abstraction can't see cycle-by-cycle protocol; use an assertion for it.
• Skipping design-written assertions. Internal invariants caught only at the interface are debugged late and far from the source; design should assert internal invariants.
• Treating assertions and the scoreboard as rivals. They're complementary tools for different check classes; use each for what it's good at.

Senior Design Review Notes

Interview Insights

Exercises

1. Classify the authorship. For a FIFO-overflow invariant and an external handshake rule, say who writes each assertion and why.
2. Dynamic versus formal. Explain why an all-passing assertion suite in simulation is not a proof, and what makes it one.
3. Choose the tool. For a one-hot state check and a datapath-output check, pick assertion or scoreboard for each and justify.
4. Close the gap. An assertion's antecedent cover shows 0 hits. Explain what that means and the two ways to address it.

Summary

• Assertion-based verification (ABV) is the methodology of capturing the design's intended behavior as assertions — executable specification (unambiguous, checkable, self-documenting, design-resident) — and using them throughout the flow.
• Who writes them follows what they check: design writes white-box assertions on internal invariants (caught early, at the source), verification writes black-box assertions on the external protocol — both layers make the assertion coverage complete.
• How they're checked spans two engines: dynamic (simulation — scenario-bound: passing means no violation in the exercised paths, not proven) and formal (property checking — exhaustive: proven for all inputs or a counterexample); the same assertion serves both.
• ABV trades off with the scoreboard — assertions for local, temporal, protocol/invariant rules (precise, early, formal-amenable), the scoreboard for end-to-end data computation (reference model) — and layers into the CRV + coverage flow as one part of a complete checking strategy.
• The durable rule of thumb: treat assertions as executable specification — the spec's contract clauses made formal and enforceable — written by whoever knows the rule (design's internal invariants, DV's external protocol), used for local/temporal/protocol checks while the scoreboard handles end-to-end data, and checked by two engines; never mistake passing in simulation for proof, because dynamic ABV only checks the paths the stimulus exercises, so cover the antecedents to know what actually fired and formally prove the critical properties — simulation checks where you looked, formal proves everywhere.

Next — Assertion Debug: when an assertion fires, you have to debug it — and an assertion failure points precisely at a cycle and a rule, which is both its strength and its subtlety. The next chapter covers debugging assertion failures: reading the failure report and the property, finding the exact cycle and the signals involved, distinguishing a real DUT bug from a wrong or too-strict assertion, handling vacuous passes and antecedent-never-fired gaps, and the systematic process from a fired assertion to its true cause.