SystemVerilog Assertions introduced assert, assume, cover, and restrict at a glance. This article goes deeper into the three that matter for a typical simulation-plus-coverage-plus-formal flow — restrict is deliberately left out, since it's formal-only and simulators ignore it entirely.
11 min read | Intermediate Level
What You'll Learn
- The exact syntax and semantics of
assert,assume, andcoveras separate statement types - Why the same property can be checked with
assertin simulation but treated as a constraint by a formal tool underassume - What
cover propertyactually tracks, and why "never failed" and "actually got exercised" are two different things - How to declare a property once and reuse it across all three statement types, keeping the underlying check perfectly consistent
assert property: Checking a Property Holds
This is the statement type used throughout every other article in this chapter — it verifies that a property is true, and reports a failure when it isn't:
assert property (@(posedge clk) req |=> gnt);
cover property: Tracking How Often a Property Is Exercised
cover property takes the exact same kind of property, but instead of flagging failures, it tracks how many times the property actually succeeded during the run — contributing to a functional coverage report entirely independent of any pass/fail result from an assert:
property p_burst;
@(posedge clk) $rose(burst_req) ##[1:8] burst_ack;
endproperty
cover property (p_burst);
This tracks how many times a burst request was actually followed by an acknowledge within the expected window. If this count stays at zero across an entire regression, that's a real coverage gap — the scenario this property describes was never even exercised, regardless of whether any assertion ever failed.
This is exactly the situation covered in SystemVerilog Property Implication: an antecedent that never fires produces only vacuous successes from assert, which look identical to genuine, meaningful passes. cover property is the concrete tool that actually distinguishes the two — a property can pass every single time an assert checks it, purely because it was never given the chance to fail.
Quick Check
Q: If a test runs for a long time and assert property(p_burst) never reports a single failure, does that guarantee p_burst's scenario was actually tested?
Show Answer
No. It only guarantees the property was never violated — possibly because burst_req simply never rose during the entire test, in which case every check was vacuously true. cover property(p_burst) is what would reveal whether the scenario actually occurred at all.
assume property: A Constraint for Formal, a Check for Simulation
assume property has a genuinely dual nature depending on how it's used:
assume property (@(posedge clk) disable iff (!rst_n) req_valid !== 1'bx);
To a formal tool, this isn't something to verify — it's told to treat the property as a given fact, and to only explore input combinations consistent with it, constraining the state space it searches through. To a simulator, assume is typically checked in much the same way assert is, and a violation is still reported.
This matters because if a simulation testbench actually violates something declared as an assume, that's a real problem worth knowing about: it means the assumption a formal proof would rely on doesn't even match how the testbench itself drives the design in simulation — undermining confidence in both the formal result and the simulation runs.
Quick Check
Q: Why would a violated assume in simulation be worth investigating, rather than just being expected behavior?
Show Answer
Because the same property is likely also being handed to a formal tool as a constraint on its input space. If simulation itself violates that constraint, the formal analysis built on top of it is reasoning about inputs that don't actually reflect how the real testbench behaves — a mismatch worth catching early.
Using the Same Property With All Three
Rather than writing the same temporal pattern three separate times, declare it once as a named property and reuse it across statement types as needed:
property p_check;
@(posedge clk) disable iff (!rst_n) req |=> ack;
endproperty
// Check it in simulation
assert property (p_check);
// Track how often it's actually exercised
cover property (p_check);
Both statements reference the exact same underlying temporal logic — there's no risk of the assert-side and cover-side definitions drifting apart, since there's only one property definition to maintain.
Where Is This Used?
Formal verification teams frequently take properties already written for simulation and add assume statements around the environment's own input constraints — reusing the exact same property declarations across both simulation and formal, rather than rewriting the temporal logic separately for each flow. This dual-use is a major reason SVA properties are written as standalone, named declarations instead of being inlined directly into a single assert statement.
Common Beginner Mistakes
Mistake #1: Assuming assume does nothing in simulation
It's typically checked in simulation too, not just treated as inert documentation for formal tools. Why? A violated assume in simulation is a genuine signal that the testbench doesn't honor an assumption a formal proof is relying on — worth investigating, not ignoring.
Mistake #2: Treating cover property as dependent on assert
A property can be covered without ever being asserted, and asserted without ever being covered — they're entirely independent statement types. Why? Some properties are purely tracked for coverage purposes with no corresponding correctness check at all, and vice versa.
Mistake #3: Confusing "never failed" with "actually exercised"
As the note above explains, these are genuinely different things. Why? An assertion that's never had the chance to fail (because its antecedent never fired) provides zero actual verification value, even though it reports nothing but passes — only cover property can confirm the scenario was genuinely exercised.
Mistake #4: Writing the same temporal logic three separate times
Duplicating a property's logic across separate assert, assume, and cover statements risks the copies drifting out of sync if only one is ever updated. Why? Declaring the property once and referencing it from each statement type guarantees they always stay perfectly consistent with each other.
Practice Exercise
Challenge: Predict assert vs cover on the Same Trace
A property p_check: req |=> ack is checked against three separate occurrences of req during a test. Two of them are correctly followed by ack; the third is not. What would assert property(p_check) report, and what would cover property(p_check) report?
Hint
One of these two statement types cares about the failure; the other only cares about counting successes.
Solution
assert property(p_check) reports one failure — specifically, the occurrence where ack didn't follow req as required. cover property(p_check) reports a coverage count of 2 — the two occurrences where the property actually succeeded — completely independent of the fact that a third occurrence failed. The failed occurrence simply doesn't count toward coverage; it isn't treated as a negative event by cover at all.
Summary
In this tutorial, you learned:
assert propertychecks that a property holds and reports a failure when it doesn'tcover propertytracks how many times a property actually succeeded, independent of anyasserton the same propertyassume propertyis a constraint on input generation for formal tools, but is typically still checked (and can still fail) in simulation- A property that never fails isn't necessarily meaningful — if its antecedent never fires, every check is vacuously true, and
cover propertyis what actually reveals that - Declaring a property once and reusing it across
assert,assume, andcoverstatements keeps simulation checking, formal constraints, and coverage tracking permanently consistent with each other
