Concurrent Assertions

Module 12 · Page 12.4

The Workhorse Form of SVA

Module 12.1 introduced SVA as the temporal-contract layer. Modules 12.2 and 12.3 covered the immediate family — same-instant checks for value validity and combinational invariants. This page introduces the concurrent family — the form that runs in parallel with the design across every clock cycle, checking temporal properties that span multiple cycles.

Most of what production engineers think of as "SVA" is the concurrent form. AXI's awvalid must be held until awready rises. AHB's htrans must be NONSEQ after IDLE. APB's psel must rise one cycle before penable. Every one of these contracts is a temporal property — it cannot be checked at a single instant. The concurrent assertion is the right tool because it is the only form that can.

Anatomy of a Concurrent Assertion

A concurrent assertion has three syntactic parts: the construct (assert property, cover property, assume property), the clocking specification (@(posedge clk) or equivalent), and the property expression (the contract to check). An optional disable iff clause turns the assertion off during reset or other don't-care windows.

// ── Anatomy of the full form ─────────────────────────────────────
property_name:                       // optional name; almost always present in production
assert property (                    // construct: assert / assume / cover / restrict
    @(posedge clk)                   // clocking — when to sample and evaluate
    disable iff (rst)                // optional — turn off during reset
    req |=> ack                      // property expression — the contract
)
else $error("[%0t] req=%b but ack didn't follow", $time, req);  // fail action

Each piece is fixed in position. The clocking goes first inside the property; disable iff next; the property expression after. The fail action (else $error(...)) is optional but production discipline requires it on every named assertion.

Property expressions — what goes after the clocking

The property expression is the contract. It can be:

• A boolean expression — req && ack — true if both signals are high in the current cycle.
• A sequence — req ##1 ack — req high in cycle N, ack high in cycle N+1.
• An implication — req |=> ack — if req is high in cycle N, then ack must be high in cycle N+1.
• A named property — p_handshake — references a property declared elsewhere.

Modules 12.5 (Sequences) and 12.6 (Properties) build out the full vocabulary. For this page, the four shapes above cover most introductory cases.

// ── 1. Boolean — same cycle ───────────────────────────────────────
a_no_simultaneous_rw:
assert property (@(posedge clk) !(read && write))
    else $error("[%0t] read and write both high", $time);
 
// ── 2. Sequence — fixed-delay temporal ────────────────────────────
a_two_cycle_pipeline:
assert property (@(posedge clk) start ##2 done)
    else $error("[%0t] done didn't follow start by exactly 2 cycles", $time);
 
// ── 3. Implication — conditional temporal ────────────────────────
a_req_ack:
assert property (@(posedge clk) disable iff (rst) req |=> ack)
    else $error("[%0t] req=1 but ack=0 next cycle", $time);
 
// ── 4. Named property ────────────────────────────────────────────
property p_handshake;
    @(posedge clk) disable iff (rst)
        req |=> ack ##1 done;
endproperty
 
a_handshake:
assert property (p_handshake)
    else $error("[%0t] handshake violation", $time);

The implication form (|-> or |=>) is the most common shape in production assertion files. Most spec contracts are conditional — "if A happens, then B must happen" — and implication is how SVA expresses conditional temporal properties.

The Concurrent Assertion Timing Model

The single most important thing to understand about concurrent assertions is when they sample and evaluate. Concurrent assertions split into two phases that live in two different simulation regions.

Preponed sampling

At the start of each time step where the clocking event fires (@(posedge clk)), the simulator samples the values of every signal referenced by the property. Sampling happens in the Preponed region — before any other process runs for that time step. The values the assertion will use are the values these signals had at the END of the PREVIOUS time step.

This is the SVA equivalent of how a flip-flop captures its D input — it sees the value that was stable just before the clock edge, not whatever value D happens to have at the clock edge or after it.

Observed evaluation

After Preponed sampling, the simulator's normal processing runs — Active region (combinational and always_ff), NBA region (<= updates apply), etc. Then in the Observed region, the simulator evaluates the property using the sampled (Preponed) values. The fail action runs here if the property is false.

T = 50ns (posedge clk fires):
 
   ┌─ Preponed ──┐    ← Concurrent assertion SAMPLES req, ack here
   │             │       (sees end-of-T=49ns values — pre-clock-edge)
   ├─ Active ────┤    ← always_ff, always_comb run; signals update
   ├─ NBA ───────┤    ← <= updates apply
   ├─ Observed ──┤    ← Concurrent assertion EVALUATES here
   │             │       (using the values it sampled in Preponed)
   └─ Final ─────┘    ← assert final immediate (from Module 12.3)

The implication for the verification engineer: a concurrent assertion sees pre-clock-edge values, not values that result from this clock-edge's updates. This is almost always what you want — it matches how the RTL behaves at the clock edge. But it is a frequent source of confusion when an immediate-assertion writer expects a concurrent assertion to see "the new value after this clock edge."

Placement — Three Forms

A concurrent assertion can live in three places. The choice affects the assertion's scope, ownership, and review process.

Inline — inside the module being verified

module apb_slave (
    input  bit clk, rst,
    input  bit psel, penable,
    output bit pready
);
    // ── DUT logic ────────────────────────────────────────────────
    // ... (omitted) ...
 
    // ── Inline concurrent assertion — APB setup phase rule ──────
    a_psel_before_penable:
    assert property (@(posedge clk) disable iff (rst)
        $rose(penable) |-> psel)
        else $error("[%0t] penable rose without psel held", $time);
endmodule

When to use. When the assertion is part of the module's contract — co-owned by the RTL designer and the verification engineer. The assertion is in the same file as the RTL it protects, so contract drift is visible at PR review.

Separate assertions.sv file

// File: apb_slave_assertions.sv
module apb_slave_assertions (
    input  bit clk, rst, psel, penable, pready
);
    a_psel_before_penable:
    assert property (@(posedge clk) disable iff (rst)
        $rose(penable) |-> psel)
        else $error("[%0t] penable rose without psel held", $time);
 
    a_pready_after_penable:
    assert property (@(posedge clk) disable iff (rst)
        penable |-> ##[1:16] pready)
        else $error("[%0t] pready didn't arrive within 16 cycles", $time);
endmodule

When to use. When the assertions are co-owned by a verification team independent of the RTL team — typical of large IP integrations. The separate file is reviewable on its own; the RTL team doesn't have to approve every assertion change.

Bind — assertions attached to existing RTL without modification

// File: tb/binds.sv (testbench-only)
bind apb_slave apb_slave_assertions u_apb_slave_assertions (
    .clk     (clk),
    .rst     (rst),
    .psel    (psel),
    .penable (penable),
    .pready  (pready)
);

When to use. When the RTL is closed (third-party IP, legacy code, or a signed-off block) and adding assertions inline would require re-signing. bind declarations attach assertion modules to existing module instances without modifying the target module's source. The assertions run as if they were inline; the target module's source stays untouched.

The bind pattern is the canonical way to add SVA to vendor IP and legacy blocks. ARM, Synopsys, and Cadence VIPs ship assertion bundles designed to be bind-ed to integrator-side instances.

disable iff — The Reset-Window Necessity

During reset, signals are usually X, in default values, or in a quiescent state that doesn't satisfy the contract you're verifying. A concurrent assertion that doesn't disable during reset will fire constantly during reset, drowning the log in noise and hiding the failures that matter after reset.

Every concurrent assertion that touches reset-sensitive signals carries a disable iff (reset_expression) clause.

// ── Without disable iff — assertion fires during reset ──────────
a_no_disable:
assert property (@(posedge clk) req |=> ack);
// During reset, req and ack may be X. The assertion's antecedent (req)
// may be X. Depending on the simulator's X-handling, the implication
// may fire spuriously. Log noise during reset hides real post-reset bugs.
 
// ── With disable iff — assertion skipped during reset ───────────
a_with_disable:
assert property (@(posedge clk) disable iff (rst)
    req |=> ack);
// During reset, the assertion is skipped entirely — no evaluation,
// no log entry. Once rst goes low, the assertion runs normally.

The disable iff expression can reference any signal — common forms are disable iff (rst), disable iff (!rst_n), disable iff (rst || scan_mode), or compound disable iff (rst || powerdown_state == OFF). Module 12.7 covers disable iff and clocking in depth.

The discipline rule that follows: every concurrent assertion in a clocked-RTL environment includes a disable iff clause covering reset and any other don't-care window. The exception is rare (assertions on signals that are guaranteed non-X during reset, like grounded inputs); when omitted, the omission is documented in a comment.

A Complete Working Example — APB Slave Protocol Compliance

The pattern below shows the canonical production shape: a small set of named, well-formatted concurrent assertions enforcing one protocol's spec rules.

module apb_slave_assertions (
    input  bit clk, rst_n,
    input  bit psel, penable, pwrite, pready,
    input  bit [31:0] paddr, pwdata, prdata
);
    // ── Rule 1: penable must be held until pready rises ──────────
    a_penable_held_until_pready:
    assert property (@(posedge clk) disable iff (!rst_n)
        (psel && penable) |=> (pready || (psel && penable)))
        else $error("[%0t] penable dropped before pready (psel=%b penable=%b pready=%b)",
                     $time, psel, penable, pready);
 
    // ── Rule 2: psel must rise one cycle before penable ──────────
    a_psel_before_penable:
    assert property (@(posedge clk) disable iff (!rst_n)
        $rose(penable) |-> $past(psel))
        else $error("[%0t] penable rose without psel high last cycle", $time);
 
    // ── Rule 3: pready must arrive within 16 cycles of penable ──
    a_pready_timeout:
    assert property (@(posedge clk) disable iff (!rst_n)
        $rose(penable) |-> ##[1:16] pready)
        else $error("[%0t] pready timeout — > 16 cycles since penable rose", $time);
 
    // ── Rule 4: address must remain stable through the transfer ──
    a_paddr_stable:
    assert property (@(posedge clk) disable iff (!rst_n)
        (psel && !penable) ##1 (psel && penable) |->
            $stable(paddr) && $stable(pwrite))
        else $error("[%0t] paddr or pwrite changed mid-transfer", $time);
 
    // ── Cover: handshake scenarios exercised by the regression ───
    c_basic_write:
    cover property (@(posedge clk) disable iff (!rst_n)
        (psel && !penable && pwrite) ##1 (psel && penable && pwrite) ##[0:15] pready);
 
    c_basic_read:
    cover property (@(posedge clk) disable iff (!rst_n)
        (psel && !penable && !pwrite) ##1 (psel && penable && !pwrite) ##[0:15] pready);
endmodule
 
// ── Bind the assertion module to the DUT ────────────────────────
bind apb_slave_dut apb_slave_assertions u_apb_assertions (.*);

What this code does. Four assertions enforcing APB spec rules — penable held until pready, psel precedes penable by one cycle, pready within 16 cycles, address stability through the transfer — plus two cover properties confirming the regression exercised basic read and write handshakes. The bind directive at the bottom attaches the assertion module to the DUT without modifying the DUT's source.

How to simulate it. Compile DUT + assertion module + bind file together. Run an APB-protocol regression that exercises reads, writes, error responses, and back-pressure. Every protocol violation fires the appropriate assertion with $time and signal values; every successful handshake increments the matching cover property's count.

Expected output (assertion + cover summary).

# *E,ASRTST: [142] paddr or pwrite changed mid-transfer
#   a_paddr_stable failed at 142ns
#   paddr_prev=0x0000_0040 paddr_curr=0x0000_0044
# *E,ASRTST: [310] pready timeout — > 16 cycles since penable rose
#   a_pready_timeout failed at 310ns
#
# Coverage summary:
#   c_basic_write: 47 hits  (write handshake exercised 47 times)
#   c_basic_read:  31 hits  (read handshake exercised 31 times)
#
# Total assertion failures: 2
# Total covers fired: 78

What to read out of this. Two specific spec violations at specific times; both covers are firing (the regression exercised the handshake scenarios). The verification engineer reads the assertion log first — both failures localise immediately. The cover hits confirm the regression's reach; if c_basic_write were at 0, the regression wouldn't have been exercising write handshakes at all and the absence of write-handshake assertion failures would mean nothing.

The assert + cover Pairing Pattern

The example above demonstrates a discipline rule worth naming explicitly. Every spec-critical concurrent assertion is paired with a cover property using the same antecedent. The assertion catches bugs while the scenario runs; the cover proves the scenario was actually run.

The third row is the one that matters most. An assertion that "passes" without ever being exercised is meaningless evidence. The cover property is the diagnostic that distinguishes "clean run, scenario tested" from "clean run, scenario never reached." Sign-off audits read both numbers.

Common Pitfalls

Pitfall 1 — Forgetting disable iff and getting reset-window noise

Already covered in §"disable iff — The Reset-Window Necessity" above. The single most common reason new SVA users complain "my assertion fires constantly."

Pitfall 2 — Using |-> when |=> is meant (or vice versa)

// Intent: ack one cycle after req
assert property (@(posedge clk) req |-> ack);     // same-cycle — wrong
assert property (@(posedge clk) req |=> ack);     // next-cycle — right

Fix: |-> is overlapping (same cycle); |=> is non-overlapping (next cycle). One-cycle-off bugs are the most common assertion-debugging session for new users. Module 12.8 covers implication operators in depth.

Pitfall 3 — Putting concurrent assertions inside always blocks

always @(posedge clk) begin
    assert property (req |=> ack);     // SYNTAX ERROR in some sims, weird in others
end

Fix: concurrent assertions live at module scope, not inside always blocks. The clocking is part of the property, not part of an enclosing procedural block. If you find yourself writing always @(posedge clk) assert property, you almost certainly want an immediate assertion instead.

Pitfall 4 — Anonymous concurrent assertions

assert property (@(posedge clk) req |=> ack);
// Failure log: "Assertion at file.sv:42 failed"
// Refactor moves the line, the log entry becomes "Assertion at file.sv:47 failed"
// No grep-friendly name, no traceability to spec.

Fix: name every assertion. a_req_ack: assert property (...) gives the assertion a stable identifier that survives line-number drift and reads meaningfully in the regression log.

Debug Lab — "Assertion Fires Every Cycle During Reset"

The single most common SVA debugging session for new users. The mechanism is well-understood; the fix is mechanical; the discipline rule that prevents it is worth committing to memory.

module dut_with_handshake (
    input  bit clk, rst,
    input  bit req,
    output bit ack
);
    // DUT logic...
    always_ff @(posedge clk or posedge rst) begin
        if (rst)      ack <= 1'b0;
        else if (req) ack <= 1'b1;
        else          ack <= 1'b0;
    end
 
    // BUG: no disable iff (rst) — assertion fires during reset
    a_req_ack:
    assert property (@(posedge clk) req |=> ack);
endmodule

a_req_ack:
assert property (@(posedge clk) disable iff (rst)
    req |=> ack)
    else $error("[%0t] req=1 but ack=0 next cycle", $time);

Industry Context — Where Concurrent Assertions Earn Their Place

• AMBA protocol VIPs (AXI/AHB/APB). ARM publishes assertion bundles for every AMBA protocol — typically 30–80 assertions per protocol covering every spec rule. Integrators bind these to their DUT instances; the assertions ride along into every simulation that touches the bus.
• PCIe LTSSM and link-training. Spec mandates exact state transitions and timing windows — Detect.Quiet → Detect.Active within N cycles, Polling.Active → Polling.Configuration after K consecutive TS1 ordered sets. Concurrent assertions encode each rule; formal flows (Jasper, VC Formal) use the same SVA source for exhaustive proof.
• DDR / LPDDR command sequencing. Refresh-to-Activate timing (tRFC), Activate-to-Read latency (tRCD), Precharge-to-Activate (tRP) — every JEDEC timing parameter is a concurrent-assertion property in production controller VIPs.
• Cache coherence checking (MESI/MOESI). Two caches cannot simultaneously hold a line in M state; an invalidation must be acknowledged within N cycles. Concurrent assertions capture the temporal contracts; formal flows prove they hold for all reachable states.
• CDC and reset-domain checkers. Vendor tools (Synopsys SpyGlass CDC, Cadence Conformal-CDC) emit concurrent-assertion templates for every crossing they detect; integrators review and customise. The assertions stay in the design forever, running in every simulation.
• UVM-based testbenches with embedded SVA. UVM monitors invariably include concurrent assertions for protocol invariants — the same monitor that publishes transactions to the scoreboard also runs the assertions that enforce protocol rules. The assertion failures localise bugs at the protocol layer before the scoreboard sees the downstream symptom.

The pattern across these uses: concurrent assertions are the primary SVA form in production verification. Immediate forms (Modules 12.2, 12.3) handle the same-instant checks that complement concurrent; concurrent handles the temporal contracts that make up most spec rules.

Interview Q&A — Ten Questions You Will Be Asked

Coding Guidelines — Seven Rules for Concurrent-Assertion Discipline

1. Name every concurrent assertion with an a_ / c_ / m_ prefix. The names survive line-number drift, make logs grep-friendly, and provide stable identifiers for verification-plan traceability.
2. Every concurrent assertion in a clocked-RTL environment includes disable iff (...) covering reset. The exception is rare; when omitted, document why in a comment. This single rule eliminates the most common SVA debugging session.
3. Pair spec-critical assertions with cover property using the same antecedent. Zero assertion fails plus every cover fires is the green state; zero assertion fails with covers at zero is the failure-hiding state.
4. Use |-> for same-cycle implication, |=> for next-cycle. One-cycle-off bugs are the most common assertion-mechanic mistake. Module 12.8 covers the implication operators in depth.
5. Prefer bind for closed RTL; prefer inline for co-owned RTL. bind lets you add assertions without modifying signed-off source. Inline keeps assertions visible at PR review next to the RTL they protect.
6. Format fail messages with $time and the violating values. "Assertion failed" tells the engineer nothing; "[142ns] paddr changed mid-transfer: prev=0x40 curr=0x44" answers where, when, and with what values without needing a second look at the waveform.
7. Sort failure logs by $time before investigating. Failures clustered in the first few hundred nanoseconds are almost always reset-window noise (missing disable iff); failures scattered across the simulation are real bugs.

Summary

Concurrent assertions are the workhorse SVA form — clock-driven, running in parallel with the design across every cycle, the right tool for the temporal contracts that make up most spec rules. The four-part anatomy (construct, clocking, property, fail action) is invariant; the property expression vocabulary (booleans, sequences, implications, named properties) builds out across Modules 12.5–12.9. The Preponed-sampling / Observed-evaluation timing model is the conceptual key — concurrent assertions see the same values flip-flops with that clock would capture, immune to glitches and NBA races. Placement options (inline, separate file, bind) cover the spectrum from co-owned to closed RTL. disable iff is non-negotiable in clocked-RTL environments. Pair every spec-critical assertion with a cover property to distinguish "clean run, scenarios tested" from "clean run, scenarios never reached." Module 12.5 builds out the sequence vocabulary; Modules 12.6–12.9 build out properties, clocking, implication, and repetition operators.