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."

Vacuity — The Pass That Proves Nothing

Every implication has a way of succeeding without testing anything, and it has a name in the LRM.

An attempt of req |=> ack starts on each clock edge. The simulator samples req. If req is false, there is nothing to check — the implication is satisfied the way "if it rains, I bring an umbrella" is satisfied on a dry day. IEEE 1800 calls this a vacuous success: the antecedent did not match, so the consequent was never evaluated. The attempt is reported as a pass.

That last sentence is the whole problem. A vacuous pass and a real pass look identical in the tally.

Where vacuity comes from

Three sources account for nearly all of it:

• An antecedent the stimulus never produces. The regression does not reach the scenario. This is the common case, and it is a coverage problem wearing an assertion's clothes.
• An antecedent that is false because it is X or Z. SVA evaluates a boolean the way if does — 0, x, and z are all false. An undriven or reset-X signal in the antecedent silently converts every attempt to a vacuous pass. This is why "my assertion can't fire, the signal is X" is backwards: X on the antecedent suppresses evaluation; X on the consequent is a real failure.
• A disable iff that is true more often than you think. A disable iff (rst || !clk_en || pwr_state != ON) that is accidentally true for most of the run kills attempts wholesale. This is not vacuity in the LRM's sense — the attempts are disabled, not vacuously passed — but it produces the same green-and-meaningless outcome, and the diagnostic is the same.

The three antidotes

1. Pair the assertion with a cover property on the antecedent. This is the §"The assert + cover Pairing Pattern" rule below, and vacuity is the reason it exists. cover property on a property counts only non-vacuous matches, so a cover at zero is a direct measurement of "this assertion never actually ran." Zero failures and a firing cover is the only green state.
2. Turn on your tool's vacuity reporting. Every major simulator can separate vacuous from non-vacuous successes in the assertion report, and most can suppress vacuous-success counting entirely. The switch names differ by vendor, so read your tool's assertion-reporting section — but do turn it on, because the default report usually blends the two.
3. Read the ratio, not the failure count. A healthy assertion in a healthy regression has a non-vacuous success count in the same order of magnitude as the scenario's occurrence count. An assertion whose successes are 100% vacuous is a finding, even though nothing failed.

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 the DUT holds ack LOW no matter what. Any cycle in which the
// testbench (or a leftover from a previous phase) has req high is a genuine
// antecedent match with a consequent that reset guarantees is false — a real
// failure, once per clock, for the whole reset window. That noise hides the
// one or two real post-reset failures that actually matter.
 
// ── 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 clocking and disable iff in depth, and clocking blocks cover the sampling discipline on the testbench side.

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 while the access phase is stalled ──
    //  The antecedent must include !pready. Without it, the LAST cycle of every
    //  legal transfer (psel & penable & pready) becomes an antecedent match,
    //  and the following idle cycle — where penable has correctly dropped and
    //  pready is low — reads as a violation. Guarding on !pready restricts the
    //  rule to the case it is actually about: a STALLED access phase.
    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 ──
    //  NOTE the [0:16], not [1:16]: a zero-wait-state slave drives pready HIGH
    //  in the same cycle penable rises, and that is legal APB. A [1:16] window
    //  would demand a SECOND pready in the following 16 cycles and fail every
    //  zero-wait-state transfer.
    a_pready_timeout:
    assert property (@(posedge clk) disable iff (!rst_n)
        $rose(penable) |-> ##[0: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.

Runnable Proof — One Passing Property, One Failing, One Vacuous

The timing model and the vacuity rule are both checkable in about sixty lines. The design below has a deliberate bug; three assertions watch it; one passes for real, one fails for real, and one passes vacuously forever. Compile and run it and the simulator will tell you the same thing this page has.

// ─────────────────────────────────────────────────────────────────────────
//  DUT contract (the "spec"):
//     R1  ack must be high the cycle after req            → the DUT honours it
//     R2  busy must be high for TWO cycles after req      → the DUT does NOT
//     R3  err_req must also be acknowledged next cycle    → never exercised
//
//  vcs -sverilog -assert svaext sva_proof.sv && ./simv
//  xrun -sv -access +rwc sva_proof.sv
//  vlog -sv sva_proof.sv && vsim -c tb -do "run -all; quit"
// ─────────────────────────────────────────────────────────────────────────
module req_ack (
  input  logic clk,
  input  logic rst_n,
  input  logic req,
  output logic ack,
  output logic busy
);
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      ack  <= 1'b0;
      busy <= 1'b0;
    end else begin
      ack  <= req;    // R1 honoured: ack is registered req
      busy <= req;    // R2 VIOLATED: busy is one cycle wide, spec wants two
    end
  end
endmodule
 
module tb;
 
  timeunit      1ns;
  timeprecision 1ps;
 
  logic clk = 1'b0, rst_n = 1'b0;
  logic req = 1'b0, err_req = 1'b0;   // err_req is declared and never driven
  logic ack, busy;
 
  always #5 clk = ~clk;               // 100 MHz — posedges at 5, 15, 25 ns …
 
  req_ack dut (.*);
 
  // ── R1 — holds. A real (non-vacuous) pass every time req is high. ──────
  a_ack_follows_req:
  assert property (@(posedge clk) disable iff (!rst_n)
      req |=> ack)
    else $error("[%0t] a_ack_follows_req: req was high, ack did not follow", $time);
 
  // ── R2 — fails by construction, exactly once per req pulse. ───────────
  a_busy_two_cycles:
  assert property (@(posedge clk) disable iff (!rst_n)
      req |=> busy ##1 busy)
    else $error("[%0t] a_busy_two_cycles: busy not held for two cycles", $time);
 
  // ── R3 — passes VACUOUSLY on every clock edge, forever. ───────────────
  //  err_req is never driven, so the antecedent never matches, so the
  //  consequent is never evaluated. Zero failures. Zero evidence.
  a_err_ack:
  assert property (@(posedge clk) disable iff (!rst_n)
      err_req |=> ack)
    else $error("[%0t] a_err_ack: err_req was high, ack did not follow", $time);
 
  // ── The antidote: this cover measures whether a_err_ack ever ran. ─────
  c_err_req_seen:
  cover property (@(posedge clk) disable iff (!rst_n) err_req);
 
  // ── Stimulus. Drive with <= from the clock edge so the testbench never
  //    races the assertion's Preponed sample. ──────────────────────────
  initial begin
    repeat (2) @(posedge clk);
    rst_n <= 1'b1;                    // release reset
    repeat (2) @(posedge clk);
 
    req <= 1'b1;  @(posedge clk);     // one-cycle request pulse
    req <= 1'b0;
 
    repeat (6) @(posedge clk);
    $display("[%0t] stimulus complete", $time);
    $finish;
  end
 
endmodule

Expected result. Exactly one failure, at 65 ns:

# ** Error: [65] a_busy_two_cycles: busy not held for two cycles
#    Offending 'busy ##1 busy'
# [105] stimulus complete

Then read the assertion report — column names differ by vendor, but every tool gives you these three numbers per assertion:

  ASSERTION            FAILURES   REAL (non-vacuous) SUCCESSES
  a_ack_follows_req         0                 1
  a_busy_two_cycles         1                 0
  a_err_ack                 0                 0     ← every success was vacuous
 
  COVER                 HITS
  c_err_req_seen           0                       ← the scenario never ran

How to read it. a_ack_follows_req is the healthy state: no failures, and a real success proving the contract was actually exercised. a_busy_two_cycles did its job. And a_err_ack is the trap this page exists to make visible — it has a perfect record and has tested nothing, and the only artifact that tells you so is c_err_req_seen sitting at zero. A dashboard reporting only the failure column would show all three assertions green.

The failure on a timeline

The waveform below is the same run, drawn as the assertion sees it. Every value shown is the sampled value — what the Preponed region captured just before that clock edge, which is the only thing the property ever evaluates.

Three things this picture is meant to fix permanently. What is sampled — the pre-edge value, never the value the edge itself produces. When the consequent starts — cycle 5 for |=>, and it would have been cycle 4 for |->; that one-cycle choice is the whole difference between the two implication operators. Why the other seven cycles are silent — they sample req low, so they are vacuous passes, which is exactly why the cover property in the code above is not optional.

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);     // legal, but almost never what you meant
end

Fix: concurrent assertions live at module scope, not inside always blocks.

Be accurate about why, because this one is often taught as a syntax rule and it is not. IEEE 1800 explicitly defines concurrent assertions in procedural code (§16.14.6), so a conforming tool will compile the code above. What changes is the semantics: a procedural concurrent assertion is instantiated afresh every time the procedural flow reaches the statement, rather than running continuously at module scope, and it inherits its clock from the enclosing block rather than declaring its own. The result is an assertion whose set of evaluation attempts depends on the control flow of the always block that hosts it — which is essentially never the contract the author had in mind, and is very hard to reason about in a failure log.

So the rule stands, but as a design rule rather than a syntax rule: put the clocking in the property and the property at module scope. If you find yourself writing always @(posedge clk) assert property, you almost certainly want either a module-scope concurrent assertion or an immediate assertion.

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 — Eight 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.
8. Read the non-vacuous success count, not just the failure count. An assertion whose successes are entirely vacuous has never evaluated its consequent. Turn on your tool's vacuity reporting and treat a 100%-vacuous assertion as a finding, not as a pass.

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. And the concept that makes the assertion tally trustworthy is vacuity: an implication whose antecedent never matches passes on every attempt while evaluating its consequent zero times, so "no failures" is not evidence on its own. Pair every spec-critical assertion with a cover property, and read the non-vacuous success count, 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.

Where This Is Specified

Concurrent assertions are defined in IEEE Std 1800 (SystemVerilog), clause 16 — Assertions. The pieces this page uses live there: sequences and their delay/range operators, properties and the implication operators, disable iff, the assert / assume / cover / restrict statements, and the clause's treatment of vacuity and of concurrent assertions in procedural code (§16.14.6). The sampling and evaluation model — Preponed sampling, Observed-region evaluation — is defined in clause 4, Scheduling semantics, which is the clause to read if the "why does the assertion disagree with $display?" question ever comes back. The IEEE Standards Association listing is the primary source.

For the protocol rules encoded in the APB example, the normative source is the Arm AMBA APB Protocol Specification, published on Arm's AMBA specifications page — worth checking directly before writing any timeout window, since the zero-wait-state case is precisely where a hand-written ##[1:N] goes wrong.

Related lessons. Start from Introduction to SVA for the family overview; immediate assertions for the same-instant form this page complements. The vocabulary this page introduces is built out in sequences, properties, and implication operators; the four constructs are compared in assert, assume, cover, restrict; and the sampling controls are in clocking & disable iff and clocking blocks.