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
  // State the invariant directly. The `|-> 0` form some guides use is legal,
  // but it reads as a puzzle and is one keystroke away from a consequent that
  // can never fail.
  a_no_overflow:  assert property (@(posedge clk) disable iff (!rst_n)
                    !(wr_en && full))                     // never write when full
    else $error("FIFO overflow");
  // `disable iff` is not decoration here: during reset `state` is 0 or X, and
  // $onehot is false for both. Without it this fires on every reset of every
  // test, someone waives it, and the waiver then hides the real failures.
  a_ptr_onehot:   assert property (@(posedge clk) disable iff (!rst_n)
                    $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) disable iff (!rst_n)
                    req |-> ##[1:3] ack);                 // external protocol rule
  a_mutex_grant:  assert property (@(posedge clk) disable iff (!rst_n)
                    !(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 split is what matters. Design-written assertions are white-box, on internal invariants: a_no_overflow and a_ptr_onehot encode micro-architectural assumptions only the designer knows, and a violation fires at the exact internal event — debugged at its source, during design, rather than later when it has already corrupted an output the scoreboard sees. Verification-written assertions are black-box, on the external protocol: a_handshake and a_mutex_grant encode the interface contract from the spec, bound to the DUT without touching its RTL.

The same assertion then serves two engines. Dynamic checking evaluates it against the stimulus you actually run, so it catches violations on exercised paths and says nothing about the rest. Formal property checking proves it for all inputs or returns a counterexample — exhaustive and stimulus-free, but bounded by convergence. Write once, check two ways.

That duality is also where the cardinal mistake lives, and it is the subject of the Debug Lab below: a_handshake passing in simulation does not mean the protocol is proven. It means the paths your tests drove did not violate it.

Wiring the Checker Into UVM — where an assertion failure actually gets counted

The bus_protocol_checker above is only half the integration. Writing the properties themselves is covered in concurrent assertions and, for this bus, in AHB assertions; what follows is the part that decides whether anyone finds out when one fires. An assertion that fires is worthless if nothing downstream notices, and the default $error action block is exactly that hazard: $error is a SystemVerilog severity task, not a UVM one. It prints, and it increments the simulator's error count — but the UVM report server never sees it. uvm_report_summarize() at the end of the test still prints UVM_ERROR : 0, set_max_quit_count never trips, and any regression script that decides pass/fail from the UVM error count marks the test PASSED while the transcript above it is full of protocol violations.

Route the action block through UVM instead. The checker below is complete enough to bind and run:

// Compiled as a standalone module, bound into the DUT. It imports uvm_pkg only
// to report; it instantiates nothing, extends nothing, and joins no phase.
module ahb_protocol_checker (
  input logic        HCLK,
  input logic        HRESETn,
  input logic [1:0]  HTRANS,
  input logic        HWRITE,
  input logic [31:0] HADDR,
  input logic        HREADY,
  input logic [1:0]  HRESP
);
  import uvm_pkg::*;
  `include "uvm_macros.svh"
 
  localparam logic [1:0] IDLE = 2'b00, BUSY = 2'b01, NONSEQ = 2'b10, SEQ = 2'b11;
 
  // One place to write the reporting call. `uvm_file and `uvm_line expand to
  // `__FILE__ / `__LINE__, so the report points at the failing assertion rather
  // than at this macro.
  `define SVA_ERR(ID, MSG) \
    uvm_report_error(ID, MSG, UVM_NONE, `uvm_file, `uvm_line)
 
  // AMBA AHB: during a wait state (HREADY low) the address-phase controls must
  // hold. `disable iff` handles the reset window; it does not need $assertoff.
  a_addr_stable_in_wait: assert property (
    @(posedge HCLK) disable iff (!HRESETn)
      (HTRANS inside {NONSEQ, SEQ} && !HREADY)
        |=> $stable(HADDR) && $stable(HWRITE) && $stable(HTRANS)
  ) else `SVA_ERR("AHB_SVA/ADDR_UNSTABLE",
        $sformatf("address phase changed during a wait state: HADDR %0h->%0h, HWRITE %0b->%0b",
                  $past(HADDR), HADDR, $past(HWRITE), HWRITE));
 
  // A two-cycle ERROR response must be preceded by HRESP=ERROR with HREADY low.
  a_error_two_cycle: assert property (
    @(posedge HCLK) disable iff (!HRESETn)
      (HRESP == 2'b01 && HREADY) |-> $past(HRESP == 2'b01 && !HREADY)
  ) else `SVA_ERR("AHB_SVA/ERROR_ONE_CYCLE",
        "ERROR response completed in one cycle; AHB requires the two-cycle sequence");
 
  // The antecedent coverage that makes the pass meaningful. Without these, a
  // green run cannot distinguish "checked and held" from "never evaluated".
  c_wait_state_seen: cover property (
    @(posedge HCLK) disable iff (!HRESETn)
      HTRANS inside {NONSEQ, SEQ} && !HREADY);
  c_error_resp_seen: cover property (
    @(posedge HCLK) disable iff (!HRESETn)
      HRESP == 2'b01 && !HREADY ##1 HRESP == 2'b01 && HREADY);
 
  `undef SVA_ERR
endmodule
 
// Bound from the testbench: no DUT edit, no port list change, and the checker
// can be excluded from synthesis by simply not compiling this file.
bind ahb_slave ahb_protocol_checker u_ahb_sva (
  .HCLK(HCLK), .HRESETn(HRESETn), .HTRANS(HTRANS), .HWRITE(HWRITE),
  .HADDR(HADDR), .HREADY(HREADY), .HRESP(HRESP)
);

Three things in that file carry their weight.

uvm_report_error instead of $error. It is a global function in uvm_pkg, callable from a module — you cannot use the `uvm_error macro here, because that macro resolves an implicit uvm_report_object that a module does not have. The global function has no such dependency. Because the call is a void function with no timing controls, it is legal in an assertion action block, which executes in the Observed region when the property fails.

A structured message ID. "AHB_SVA/ADDR_UNSTABLE" is what a uvm_report_catcher matches on, so a known-failing check can be demoted to a warning for one test without editing the checker or commenting the assertion out. An $error string offers nothing to hook.

cover property beside each assert property. These are the antecedent counters that answer the question the Debug Lab below is about — the assertion/coverage pairing in full. a_error_two_cycle passing tells you nothing on its own; a_error_two_cycle passing while c_error_resp_seen has a non-zero count tells you the check ran and held.

// ✗ fires, prints, and is invisible to the verdict
a_addr_stable: assert property (p_addr_stable)
  else $error("address changed during wait state");
 
// ✓ the same failure, counted by the UVM report server, catchable, demotable
a_addr_stable: assert property (p_addr_stable)
  else uvm_report_error("AHB_SVA/ADDR_UNSTABLE",
                        "address changed during wait state",
                        UVM_NONE, `uvm_file, `uvm_line);

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.

Where This Is Specified

• IEEE 1800-2023 (SystemVerilog), clause 16 — Assertions. Concurrent and immediate assertions, the assert / assume / cover property statements, action blocks, and disable iff. §16.14.6 covers the assertion control tasks ($assertoff, $asserton, $assertkill).
• IEEE 1800-2023, §22.13 — Source file and line macros. `__FILE__ and `__LINE__, which UVM's `uvm_file / `uvm_line expand to.
• IEEE 1800-2023, §23.11 — Binding auxiliary code to scopes. The bind construct that attaches a checker to a design instance without editing its source.
• IEEE 1800.2-2020 (UVM) / Accellera UVM Reference — reporting. The global uvm_report_error / uvm_report_warning functions, uvm_report_server severity counts, uvm_report_catcher, and uvm_report_summarize().

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.
• A checker only counts if its failures reach the verdict: $error in an action block is a SystemVerilog severity task that the UVM report server never sees, so a run full of real assertion failures can still print UVM_ERROR : 0 and pass. Report through uvm_report_error with a structured ID, and pair every non-trivial assert property with a cover property on its antecedent so a pass carries information.
• 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.