Assertion coverage tracks whether the temporal scenarios described by your SystemVerilog Assertions (SVA) were actually exercised during simulation. It answers a question that structural coverage metrics cannot: not just "was this line of code reached?" but "did this specific sequence of events — request followed by grant within four cycles — ever actually happen?" Every unexercised assertion scenario is a verification gap, regardless of how high your line or branch coverage numbers are.
What You'll Learn
- The difference between
assert,cover, andassumeand what each contributes to coverage - How assertion coverage is measured and what the simulator reports
- How assertion coverage complements structural code coverage
- How to interpret assertion coverage holes and respond to them
The Three SVA Statement Types
SVA provides three statement types that serve distinct roles in a coverage-driven verification flow. Understanding the difference is essential before discussing assertion coverage.
assert property
An assert property is a correctness check. It defines a temporal sequence that must always hold during simulation. If the property is ever violated, the simulator reports a failure. The assertion fires every time its triggering condition occurs, and the simulator checks whether the specified outcome follows.
// Assert: whenever a request is made, an acknowledge must follow within 4 cycles
property p_req_ack;
@(posedge clk) disable iff (!rst_n)
req |-> ##[1:4] ack;
endproperty
assert property (p_req_ack)
else $error("Request not acknowledged within 4 cycles");
From an assertion coverage perspective, the simulator tracks two statistics for every assert property:
- Attempt count: how many times the antecedent (
req) was true — i.e., how many times the property was triggered and evaluated - Pass/fail count: how many evaluations passed vs failed
An assertion with zero attempts is a coverage hole — the triggering condition was never met, so the property was never checked. It provided no verification value whatsoever.
cover property
A cover property is a reachability check. It defines a temporal sequence that you want to observe at least once — not a requirement, but a scenario you are specifically targeting. The simulator counts how many times the sequence was seen without reporting any failure.
// Cover: verify that a back-to-back request scenario actually occurred
property p_back_to_back_req;
@(posedge clk) disable iff (!rst_n)
req ##1 req;
endproperty
cover property (p_back_to_back_req);
A cover property with a hit count of zero means the scenario was never observed. This is a direct coverage hole — your testbench never generated back-to-back requests, so you have no evidence that the design handles them correctly.
assume property
An assume property constrains the legal input space. In simulation it behaves like an assertion (it fires if violated), but its primary role is in formal verification, where it restricts the tool to only consider input sequences that satisfy the assumption. In a simulation context, assume statements contribute to coverage by confirming that the testbench respected its own constraints throughout the run.
// Assume: the arbiter protocol requires req to be held stable until ack
property p_req_stable;
@(posedge clk) disable iff (!rst_n)
(req && !ack) |-> ##1 req;
endproperty
assume property (p_req_stable);
In simulation, assume property violations are typically reported as warnings rather than errors, since they indicate the testbench violated a protocol constraint rather than the design itself. In formal verification, assumptions are treated as axioms that bound the proof space.
Quick Check
Q: A cover property ends the regression with a hit count of zero. Does this mean the design has a bug?
Show Answer
Not necessarily. A zero-hit cover property means the scenario was never observed — but this could be because the testbench never generated the stimulus to trigger it, not because the design responded incorrectly. The correct response is to add directed stimulus that exercises the scenario, then check whether the design handles it correctly. Zero hits indicate a verification gap, not a confirmed design bug.
How Assertion Coverage Is Measured
The simulator collects assertion coverage statistics automatically whenever SVA statements are present and simulation is run with coverage enabled. After merging the regression databases, the coverage report shows per-property statistics. A typical report entry looks like this:
-- Assertion Coverage Report: arbiter.sv --
Property Type Attempts Passed Failed Coverage
--------- ---- -------- ------ ------ --------
p_req_ack assert 1423 1423 0 ACTIVE
p_no_double_grant assert 0 0 0 NEVER TRIGGERED **
p_back_to_back_req cover 0 -- -- NOT COVERED **
p_grant_with_req cover 847 -- -- COVERED
p_req_stable assume 1423 1423 0 ACTIVE
Two problems are visible immediately. p_no_double_grant was never triggered — the antecedent condition (whatever causes a double-grant scenario) never occurred, so the assertion never evaluated. It was written but provided zero verification value. p_back_to_back_req was never observed — the scenario was targeted but never generated by the testbench.
Both are high-priority holes. A never-triggered assert property in particular is a false sense of security: the team may believe a safety-critical protocol property is being checked, when in reality it was never evaluated once.
A never-triggered assert property is not a passing assertion — it is an untested assertion. Zero attempts means zero verification. It must be treated as a coverage hole and resolved by generating stimulus that triggers the antecedent.
Assertion Coverage vs Structural Code Coverage
Assertion coverage and structural code coverage (statement, branch, toggle) measure orthogonal properties of the verification. Both are necessary; neither subsumes the other.
| What It Measures | Structural Coverage | Assertion Coverage |
|---|---|---|
| Lines of RTL executed | Yes (statement) | No |
| Decision paths taken | Yes (branch) | No |
| Signal transitions observed | Yes (toggle) | No |
| Temporal sequences verified | No | Yes (assert) |
| Protocol scenarios exercised | No | Yes (cover) |
| Output correctness checked | No | Yes (assert) |
The key distinction: structural coverage tells you which RTL constructs were exercised. Assertion coverage tells you which protocol behaviors were verified. You can achieve 100% branch coverage while the assertion that checks the handshake timing between two blocks was never triggered — because the triggering sequence requires a specific multi-cycle scenario that random stimulus never produced.
Assertion Coverage in Protocol Verification
Bus protocol verification — AXI, AHB, PCIe, and similar interfaces — relies heavily on assertion coverage to confirm that both the legal and error-handling protocol sequences were exercised. A typical AXI verification environment has dozens of properties covering ordering rules, response timing windows, and exclusive access sequences. Tracking assertion coverage across the regression confirms which of these protocol scenarios were actually observed, and which remain untested despite high structural coverage numbers.
Writing Assertions That Generate Useful Coverage
Assertion coverage is only as useful as the assertions themselves. Poorly written assertions either never trigger or trigger so frequently that the statistics become noise.
Pair assert and cover for every protocol rule
For each protocol rule, write both an assert property (to catch violations) and a cover property (to confirm the scenario was exercised). This pairing ensures that a passing assertion genuinely means the scenario was tested:
// The rule: grant must not be asserted without a pending request
property p_no_spurious_grant;
@(posedge clk) disable iff (!rst_n)
grant |-> req;
endproperty
// Assert: the rule must never be violated
assert property (p_no_spurious_grant)
else $error("Grant asserted without request");
// Cover: confirm that a grant-with-request scenario was actually seen
property p_grant_seen;
@(posedge clk) disable iff (!rst_n)
grant && req;
endproperty
cover property (p_grant_seen);
Use disable iff for reset handling
An assertion without reset qualification will trigger during reset, producing spurious failures and polluting the attempt count with meaningless evaluations. Always use disable iff to gate assertions on active reset:
// Without reset qualification — fires during reset, pollutes statistics
property p_bad;
@(posedge clk) req |-> ##[1:4] ack;
endproperty
// Correct — disabled during reset
property p_good;
@(posedge clk) disable iff (!rst_n)
req |-> ##[1:4] ack;
endproperty
An assertion that fires thousands of times during reset and zero times in functional mode will show a high attempt count but no meaningful verification. Review the attempt-count breakdown per simulation phase if your tool supports it, or simply always use disable iff on all RTL assertions.
Target specific corner cases with cover properties
The most valuable cover property statements target scenarios that random stimulus is unlikely to generate naturally — boundary conditions, back-pressure events, error recoveries, and simultaneous edge cases:
// Cover: FIFO-full condition during an active write request
property p_write_when_full;
@(posedge clk) disable iff (!rst_n)
wr_en && full;
endproperty
cover property (p_write_when_full);
// Cover: simultaneous read and write (port contention)
property p_simultaneous_rw;
@(posedge clk) disable iff (!rst_n)
rd_en && wr_en;
endproperty
cover property (p_simultaneous_rw);
// Cover: read from empty FIFO (underflow scenario)
property p_read_when_empty;
@(posedge clk) disable iff (!rst_n)
rd_en && empty;
endproperty
cover property (p_read_when_empty);
Each of these targets a scenario the design must handle gracefully. If any cover property ends the regression with zero hits, the corresponding error-handling path was never exercised — regardless of what structural coverage reports.
Quick Check
Q: An assert property has 5000 attempts and 5000 passes. Does this guarantee the property is correctly written and covers the intended scenario?
Show Answer
No. High attempt and pass counts confirm the antecedent fired often and the consequent always followed — but they say nothing about whether the assertion captures the right protocol requirement. An assertion could have 5000 passes because it is trivially weak (e.g., checking that 1 == 1 after every clock). Always pair assertions with a code review to confirm they encode meaningful protocol rules, and use cover property to verify that the interesting outcome scenarios (not just the common path) were also observed.
Common Mistakes
Mistake #1: Treating a never-triggered assertion as a passing assertion
An assert property with zero attempts has not passed — it has simply never been evaluated. This is among the most dangerous false positives in verification: a team believes a critical safety property is being monitored, but the triggering scenario was never generated. Always review assertion attempt counts alongside pass/fail counts, and treat zero-attempt assertions as high-priority coverage holes.
Mistake #2: Writing only assert property and no cover property
An assertion alone cannot tell you whether the scenario it checks was actually exercised in a meaningful way. A grant assertion that only fires during the common happy-path case has never been stress-tested against back-pressure, simultaneous requests, or error recovery. Pairing each assertion with targeted cover property statements closes this gap by explicitly tracking whether the edge-case scenarios were generated.
Mistake #3: Omitting disable iff on RTL assertions
Assertions without reset qualification fire during the reset phase of simulation, generating a burst of attempt counts before functional simulation even begins. This inflates the attempt counter with non-functional evaluations and can make an assertion appear well-exercised when its functional trigger conditions were rarely or never met. Always qualify RTL assertions with disable iff (!rst_n) or the appropriate active reset polarity.
Mistake #4: Only tracking assert pass/fail and ignoring cover hit counts
A passing regression with no assertion failures is not the same as a complete regression. cover property hit counts reveal which protocol scenarios were actually observed. A zero-hit cover property means the scenario was never generated — and the corresponding assertion that guards it was therefore never stress-tested under that condition. Review both assertion pass rates and cover hit counts as separate closure criteria.
Summary
In this tutorial, you learned:
assert propertychecks correctness — it must hold on every trigger; a zero-attempt count means the property was never evaluated and provides no verification valuecover propertychecks reachability — it tracks whether a targeted scenario was observed; a zero hit count is a direct verification gap- Assertion coverage complements structural coverage by verifying temporal protocol sequences and output correctness, which line, branch, and toggle metrics cannot capture
- Every protocol rule should be paired with an
assert propertyfor correctness checking and acover propertyfor scenario reachability, and all RTL assertions should usedisable iffto exclude reset-phase evaluations
