assert, assume, cover, restrict

Module 12 · Page 12.10

Four Constructs, One Property Language

Modules 12.4–12.9 built the property and sequence vocabulary — the contracts. This page covers the four constructs that use those contracts: assert, assume, cover, and restrict. They share one property language: any property you can write goes inside any of the four constructs. The construct decides what the simulator (or formal tool) does when the property is true or false.

The four constructs encode four distinct verification roles:

• assert property (p) — catch design bugs. Fires when p is false.
• cover property (p) — measure scenario exercise. Records a hit when p is true.
• assume property (p) — constrain the input environment for formal tools. Tells the engine "the environment guarantees p is true."
• restrict property (p) — scope the formal proof search. Limits which input sequences the formal engine considers.

In simulation, three of these behave like assertions: assert, assume, and restrict all fire when the property is false. Only cover is structurally different in simulation — it counts hits rather than fires fails. In formal verification, the four diverge sharply: assert is what's proved, assume is what's assumed about inputs, cover is what's checked for reachability, restrict is what's excluded from consideration. The simulation-vs-formal semantic split is the most consequential SVA-mechanic detail at this layer.

assert property — The Bug Catcher

The assert property construct is the most common SVA verb. It fires the fail action when its property is false at the next sampling event after the property's antecedent (or starting cycle) matches.

property p_req_ack;
    @(posedge clk) disable iff (rst)
        req |=> ack;
endproperty
 
a_req_ack:
assert property (p_req_ack)
    else $error("[%0t] req-ack handshake violation", $time);

The discipline from Modules 12.4–12.9 carries forward: every assertion is named with an a_ prefix; every property includes disable iff; the fail message includes $time and the offending signal context.

The simulation semantic: at each sampling event, the property's antecedent is checked. If it matches and the consequent fails, the else action runs and the simulator's error counter increments. If the antecedent doesn't match, the assertion is vacuously true and silent. The pattern across thousands of assertions in a regression: each one runs continuously, surfaces its specific contract violation with full context, and survives refactors that would break inline procedural checks.

cover property — The Scenario Counter

cover property is the opposite of assert in one structural sense: it records a hit when the property is true. The construct measures whether the regression actually exercised the scenario the property describes.

property p_req_ack;
    @(posedge clk) disable iff (rst)
        req |=> ack;
endproperty
 
// ── The assertion catches violations ────────────────────────────
a_req_ack:
assert property (p_req_ack)
    else $error("[%0t] req-ack violation", $time);
 
// ── The cover proves the regression exercised the scenario ──────
c_req_ack_seen:
cover property (p_req_ack);

The simulation semantic: at each sampling event where the property's antecedent matches, the property's consequent is checked. If the property is true (the consequent holds), the cover's hit count increments and the cover statement is "covered." The cover doesn't fire any action — it just counts.

The assert+cover pairing pattern (Module 12.4 introduced this) is the single most important discipline rule at this layer:

The third row is the one that matters most. An assertion that "passes" without ever being exercised is meaningless evidence; the cover is the diagnostic that distinguishes the green state from the bug-hiding state.

assume property — The Formal Input Constraint

In simulation, assume property (p) behaves identically to assert property (p) — it fires the fail action when the property is false. In formal verification, assume has a fundamentally different meaning: it tells the formal engine "the input environment is guaranteed to satisfy this property — do not consider input sequences that violate it."

// ── Environment guarantee — the testbench will never drive both R and W ──
m_no_simultaneous_rw:
assume property (@(posedge clk) disable iff (rst)
    !(read && write));
 
// In simulation: fires $error if the testbench accidentally drives both high.
// In formal:     the engine restricts its search to input sequences where
//                read and write are NEVER simultaneously high.

The formal semantic is the dangerous one. A assume property tells the formal engine "the environment guarantees this." If the engineer's assumption is wrong — the real environment can produce inputs that violate the assumption — the formal proof passes for a design that ships actual bugs the constrained-out inputs would have triggered. The formal output looks like clean evidence; the design still ships the bug.

The discipline rule that prevents this: every assume property in a formal-targeted property file is paired with a cited environmental guarantee. The citation explains why the constraint reflects a real environmental rule (typically a clause in the integration spec, the testbench architecture document, or the design's assume-style boundary contract). Code review verifies the citation matches reality; an unjustified assume is one of the most expensive verification mistakes.

// ── Environment guarantee per Integration Spec §3.2: ─────────────
//      "The bus matrix arbiter ensures READ and WRITE
//       are mutually exclusive for any single port."
//
m_arbiter_mutex:
assume property (@(posedge clk) disable iff (rst)
    !(read && write));
// Reviewer verifies: does Integration Spec §3.2 actually say this?
// If yes — assumption is justified. If no — the assume is a hidden bug.

restrict property — The Formal Search Scope

restrict property is the most specialised of the four constructs — it has no effect in simulation and is only meaningful in formal verification. The construct tells the formal engine to limit its proof search to input sequences where the property holds.

// ── Formal-only — only consider sequences where reset goes low at time 0 ──
r_reset_initialised:
restrict property (@(posedge clk)
    $past(rst) ##1 !rst);
 
// In simulation: no-op. The construct has no effect.
// In formal:     the engine considers only input sequences where reset
//                is initially asserted and then deasserted.
//                Sequences that never deassert reset are excluded from
//                the proof search.

The construct is typically used to encode the initialization sequence a formal proof should consider — "the design starts in reset, then reset is deasserted, then normal operation begins." Without restrict, the formal engine would consider input sequences that never apply reset at all, producing proofs against unreachable states.

The simulation semantic is restrict property doing nothing. Production assertion files that target both simulation and formal verification use restrict only inside // pragma formal-only blocks or equivalent vendor-specific markers, so the construct is visible in formal flows but skipped in simulation tooling.

A Complete Working Example — APB Property File With All Four Constructs

The pattern below shows production discipline: a property file that uses all four constructs deliberately, with assume citations and pairing patterns documented inline.

package apb_verification;
    default clocking @(posedge pclk); endclocking
    default disable iff (!presetn);
 
    // ── Property 1: PREADY must arrive within 16 cycles ──────────
    property p_pready_within_16(input bit psel, penable, pready);
        (psel && penable) |-> ##[0:15] pready;
    endproperty
 
    // ── Property 2: PSEL must rise before PENABLE ────────────────
    property p_psel_before_penable(input bit psel, penable);
        $rose(penable) |-> $past(psel);
    endproperty
 
    // ── Property 3: PREADY response window ───────────────────────
    property p_pready_window(input bit psel, penable, pready);
        $rose(penable) ##[0:15] pready;
    endproperty
 
    // ── Property 4: PADDR/PWDATA must not change during ACCESS ───
    property p_signals_stable(
        input bit psel, penable,
        input bit [31:0] paddr, pwdata
    );
        (psel && penable && $past(psel) && !$past(penable)) |->
            ($stable(paddr) && $stable(pwdata));
    endproperty
endpackage
 
// ── Assertion module using all four constructs ───────────────────
module apb_slave_assertions (
    input  bit pclk, presetn,
    input  bit psel, penable, pready,
    input  bit [31:0] paddr, pwdata
);
    import apb_verification::*;
 
    // ── assert: catch DUT bugs ───────────────────────────────────
    a_pready_within_16:
    assert property (p_pready_within_16(psel, penable, pready))
        else $error("[%0t] PREADY > 16 cycles after ACCESS", $time);
 
    a_psel_before_penable:
    assert property (p_psel_before_penable(psel, penable))
        else $error("[%0t] PENABLE rose without PSEL last cycle", $time);
 
    a_signals_stable:
    assert property (p_signals_stable(psel, penable, paddr, pwdata))
        else $error("[%0t] PADDR/PWDATA changed in ACCESS phase", $time);
 
    // ── cover: measure regression's reach ────────────────────────
    c_pready_window_seen:
    cover property (p_pready_window(psel, penable, pready));
 
    c_psel_before_penable_seen:
    cover property (@(posedge pclk) disable iff (!presetn)
        $rose(penable));
 
    // ── assume: formal-only environmental guarantee ──────────────
    // Per Integration Spec §3.1: "The bus master will never assert
    //     PSEL without intent to drive a transfer within 16 cycles."
    m_psel_eventually_drives_transfer:
    assume property (@(posedge pclk) disable iff (!presetn)
        $rose(psel) |-> ##[1:16] penable);
 
    // ── restrict: formal-only initialization scope ───────────────
    // Formal proof considers only sequences with proper reset
    r_reset_initialised:
    restrict property (@(posedge pclk)
        $past(presetn, 5) == 0 ##1 presetn);
endmodule

What this code does. Four assert constructs catch DUT bugs in the APB slave's protocol compliance. Two cover constructs confirm the regression exercises the protocol scenarios. One assume documents an environmental guarantee with a spec citation (critical for any formal flow). One restrict scopes the formal proof to sequences that start in reset. Every construct has a named identifier (a_*, c_*, m_*, r_*) that surfaces in regression logs.

Expected output (fragment).

# *E,ASRTST: [142] a_signals_stable failed at 142ns
#   PADDR changed: 0x40 → 0x44 during ACCESS phase
#
# Coverage summary:
#   c_pready_window_seen:      87 hits
#   c_psel_before_penable_seen: 87 hits
#
# Total assertion failures: 1

The regression produces a clear, actionable signal: one real protocol violation localised to a specific time and signal pair, with coverage evidence confirming the regression exercised both critical scenarios. The assume constraint behaves like an assert in simulation — it would also have fired if the testbench had violated the environmental rule, surfacing a testbench bug rather than a DUT bug.

Construct Selection — Which Verb for Which Verification Role

The four constructs are not interchangeable; each has a specific verification role. The selection rule maps verification intent to construct.

The most common selection mistakes:

• Using assert where cover was meant. An engineer wants to know "did the regression hit this scenario?" but writes assert property (p_scenario). The assertion fires every cycle the scenario doesn't happen (because the property is vacuously true on those cycles, or false if the antecedent is unconditional), flooding the log. The right tool is cover, which silently counts hits.
• Using assert where assume was meant in formal flows. An engineer wants the formal engine to consider only sequences where read and write are mutually exclusive, but writes assert property (!(read && write)). The formal tool now treats the property as a proof obligation — it will try to find an input sequence that violates the property, then report it as a counterexample. The engineer reads "formal found a violation" and thinks the design is broken; really, the formal tool was correctly finding a sequence that breaks the engineer's intent. The right tool is assume, which tells the formal tool "I guarantee this — don't search for violations."
• Using assume where assert was meant in formal flows. The expensive opposite. The engineer marks a design contract as assume instead of assert; the formal engine respects the assumption and never tests whether the design satisfies it. The proof passes; the design ships; bring-up surfaces the bug. This is the most expensive failure mode.

The discipline rule: at code review, every construct selection is explicitly justified against the intent. The reviewer asks "what does this construct express?" and the engineer's answer must match the construct's actual semantics — both in simulation and (where relevant) in formal.

Common Pitfalls

Pitfall 1 — assume without environmental citation

Already covered above. Every assume property cites the environmental guarantee it encodes. Without the citation, the assumption is presumed accidental and the formal proof is presumed wrong.

Pitfall 2 — Confusing assert with cover

// Intent: "did the regression exercise the back-to-back-write scenario?"
 
// Wrong: fires on every cycle the scenario doesn't happen
a_back_to_back_writes:
assert property (@(posedge clk) write ##1 write);
 
// Right: silently counts hits when the scenario does happen
c_back_to_back_writes:
cover property (@(posedge clk) write ##1 write);

Fix: "the regression should exercise X" maps to cover, not assert. The cover construct counts hits; the assert construct fires on failures.

Pitfall 3 — restrict in a simulation-only flow

r_reset_init:
restrict property (...);
// In simulation, this construct does nothing. If the engineer
// expected it to enforce the constraint, they'll be surprised when
// the testbench drives sequences that violate the restriction.
// The simulation runs without any error reported.

Fix: if the intent is to enforce a constraint in simulation, use assume (which fires in simulation when the constraint is violated). Use restrict only when the intent is genuinely formal-only scope. Production codebases mark restrict constructs in formal-only sections so simulation engineers know to skip them.

Pitfall 4 — Forgetting that cover property matches sequences, not just booleans

// Sequences match starting at any cycle; `cover` records every match
c_two_cycle_handshake:
cover property (@(posedge clk) req ##1 ack);
 
// In a 1000-cycle regression with 87 req-ack pairs, this cover
// reports 87 hits — one per pair. NOT one hit for the regression as a whole.

Fix: cover property counts every matching cycle, not just the first. If the verification intent is "did the regression ever exercise this scenario?", the answer is "the cover reports N hits — exercised N times." For "did the scenario start at the time we're measuring?", use the appropriate sampling event or first_match.

Debug Lab — "Formal Says The Design Is Bug-Free, But Silicon Has The Bug"

The most expensive SVA-related verification mistake. A formal proof passes; the design ships; bring-up surfaces a bug the formal engine should have caught. The root cause is an assume that constrained out the buggy input space.

// Verification engineer writes:
m_no_simultaneous_rw:
assume property (@(posedge clk) disable iff (rst)
    !(read && write));
 
// Formal proof:
a_data_consistency:
assert property (@(posedge clk) disable iff (rst)
    write |=> (read_data == $past(write_data)));
// "If a write happens, the next read returns the written data."
//
// Formal engine respects the assumption: it will NOT consider
// input sequences where read and write are simultaneously high.
// The data-consistency proof passes because in all considered
// sequences, the writes and reads are serialised.

// Removed:
// m_no_simultaneous_rw:
// assume property (!(read && write));
 
// Replaced with:
a_no_simultaneous_rw:
assert property (@(posedge clk) disable iff (rst)
    !(read && write));
// Now the formal engine will SEARCH FOR input sequences where read
// and write are simultaneously high — and report each as a violation.
// If the environment can produce such sequences, the formal proof
// will surface them as counterexamples.
 
// And the data-consistency check now correctly tests against all
// input sequences, including the simultaneous-read-write case:
a_data_consistency:
assert property (@(posedge clk) disable iff (rst)
    write |=> (read_data == $past(write_data)));

Industry Context — Where the Four Constructs Live

• AMBA protocol VIPs. Every shipping AMBA VIP uses all four constructs. assert for protocol-compliance rules. cover for transaction-coverage metrics. assume for environmental guarantees (with citations to AMBA-specific integration constraints). restrict for formal-only initialization sequences.
• Formal verification flows (JasperGold, VC Formal, OneSpin). Formal engines distinguish the four constructs sharply. assert is the proof obligation; assume is the input constraint; cover is the reachability target; restrict is the search scope. The tool's output reports each construct separately — "12 properties proved, 3 assumptions accepted, 8 cover targets reachable, 1 restrict applied."
• PCIe / USB / Ethernet protocol verification. Spec-conformance properties become assert; sign-off coverage targets become cover; environment-side spec rules become assume. The three layers map directly to the spec's structure: "the device must do X" → assert; "the device must support Y scenarios" → cover; "the host will provide Z inputs" → assume.
• UVM RAL register-model verification. RAL assert properties enforce register-access semantics (RO writes are no-ops, W1C bits clear-on-write); RAL cover properties measure register-coverage closure; RAL assume properties document environmental guarantees about the bus master's access patterns.
• Safety-critical / DO-254 / ISO 26262 / ARP4754A flows. Auditors verify that every assume has an environmental citation that traces to a section of the integration spec. An unjustified assume is a certification finding; teams maintain explicit assume registers as part of certification evidence.
• CDC / RDC verification. Vendor tools emit assume templates for source-domain signals (the CDC analysis tool guarantees the signal is glitch-free at the crossing); the integrator marks each assume as accepted or replaces with assert depending on whether the source-side signal generator truly satisfies the property.

The pattern across these uses: production verification environments treat the construct selection as a first-class architectural decision, not a stylistic choice. The four constructs encode four distinct verification roles; mixing them produces verification evidence that doesn't mean what it appears to mean.

Interview Q&A — Ten Questions You Will Be Asked

Coding Guidelines — Seven Rules for Construct-Selection Discipline

1. Pair every spec-critical assert with a cover of the same scenario. "0 assertion failures" is ambiguous evidence; the cover hit count distinguishes "clean run, contracts honored" from "clean run, scenarios never reached."
2. Every assume property in a formal-targeted file carries a written environmental citation. The citation explains why the constraint reflects a real environmental rule. Code review verifies the citation matches the integration spec.
3. Use assume for environment contracts; use assert for design contracts. Design contracts the DUT must honor are proof obligations (assert); environmental contracts the testbench provides are input constraints (assume). The line between them is the design boundary.
4. Use restrict property only for formal-engine scoping that has no simulation analog. If the constraint should also be enforced in simulation, use assume instead. restrict is a no-op in simulation and easy for simulation engineers to miss.
5. Use cover property for "did the regression exercise this scenario?" — not assert. Asserts fire on violations; covers count hits. Mixing them produces logs flooded with false failures for scenarios the regression didn't even attempt.
6. At code review, justify every construct selection against the verification intent. The reviewer asks "what does this construct express?" and the engineer's answer must match the construct's actual semantics in both simulation and (where applicable) formal.
7. When a formal proof passes, audit the assumptions before celebrating. The proof's validity depends entirely on the assumptions; an incorrect assumption renders every assertion result meaningless. Verification engineers' first review step after a clean formal run is the assume-citation audit.

Summary

The four SVA constructs — assert, cover, assume, restrict — share one property language but encode four distinct verification roles. assert catches violations; cover measures exercise; assume constrains formal inputs; restrict scopes formal proof search. In simulation, three behave like asserts and only cover is structurally different. In formal verification, all four diverge sharply, and assume is the most dangerous — an incorrect assumption renders the formal proof meaningless while looking like clean evidence. Pair every spec-critical assert with a cover of the same scenario; cite every assume with an environmental-spec citation; reserve restrict for formal-only initialization scope. Module 12.11 builds on this with severity levels and action blocks — what happens when an assertion fires.