Clocking & disable iff

Module 12 · Page 12.7

The Two Decisions Every Concurrent Assertion Makes

Every concurrent assertion answers two structural questions before it can run: when does it evaluate (the clocking spec), and when does it stay dormant (the disable expression). Modules 12.4–12.6 have been carrying both clauses in their examples — @(posedge clk) disable iff (rst) is the canonical opening of any concurrent property. This page is the deep dive: how each clause works, the precedence rules, the multi-clock case, and the discipline that prevents the most common SVA debugging session every team encounters.

The clocking and disable clauses are inseparable from the property they gate. Get them wrong and the assertion either fires when it shouldn't (reset-window noise), misses violations that happen between clock edges (wrong clock granularity), or never fires at all (the clocking expression never matches the property's intent). This page builds the discipline that gets them right.

The Clocking Clause — Forms and Scopes

The clocking specification tells the simulator when to sample property-referenced signals (in the Preponed region) and when to evaluate the property (in the Observed region). Three forms cover almost every production case.

Form 1 — Explicit per-property clocking

property p_req_ack;
    @(posedge clk)               // explicit — applies to this property only
        req |=> ack;
endproperty
 
a_req_ack:
assert property (p_req_ack)
    else $error("req-ack violation");

When to use. When the assertion is the only one on its clock, when properties in the same file use different clocks, or when explicit clarity is preferred over default-clocking machinery. The most common form in small assertion files; less common in protocol VIPs that share a clock across many assertions.

Form 2 — default clocking block

default clocking cb_main @(posedge clk);
endclocking
 
// All properties in this scope inherit the default clocking
property p_req_ack;
    req |=> ack;     // no @(...) — uses default cb_main
endproperty
 
property p_grant_legal;
    grant |-> req;
endproperty
 
a_req_ack:  assert property (p_req_ack)  else $error("req-ack");
a_grant:    assert property (p_grant_legal) else $error("grant-req");

When to use. When many properties in the same module share a single clock. The default clocking directive declares the clock once at module scope; every property without its own explicit clocking inherits the default. The pattern keeps the property file uncluttered with repeated @(posedge clk) boilerplate.

Form 3 — Multi-clock properties

property p_cross_clock_handshake;
    @(posedge clk_a) req_a ##1 @(posedge clk_b) ack_b;
    // The property crosses clock domains — req_a sampled on clk_a,
    // ack_b sampled on the next posedge of clk_b after req_a's cycle.
endproperty

When to use. When the property spans clock domains — typically CDC verification, or protocols where request and response are on different clocks. The clocking expression changes mid-property; the ##1 operator means "one cycle of the next-mentioned clock," not "one cycle of the previous clock." Multi-clock properties are powerful but easy to misuse — most engineers use them for one specific contract per page rather than as a default pattern.

Form 4 — Inline clocking inside a sequence

A sequence can carry its own clocking that overrides the enclosing property's. This is rare and almost always confusing; production discipline avoids it.

sequence s_with_own_clock;
    @(posedge fast_clk) a ##1 b;       // sequence-level clocking
endsequence
 
property p_using_sequence;
    @(posedge slow_clk)               // property's clocking
        c |-> s_with_own_clock;        // sequence brings its own clock!
endproperty

When to avoid. Almost always. The clocking switches mid-property in non-obvious ways; the property file becomes hard to review. If the property genuinely needs two clocks, use the explicit multi-clock form (Form 3); if not, keep clocking at the property level.

The disable iff Clause — Reset and Don't-Care Windows

Modules 12.1–12.6 have repeated the discipline rule: every concurrent assertion in a clocked-RTL environment includes disable iff (reset_expression). This page makes the rule precise.

Syntax and placement

property p_req_ack;
    @(posedge clk) disable iff (rst)     // clocking first, disable iff second
        req |=> ack;
endproperty
 
// The disable iff clause is BEFORE the property expression.
// Order: clocking → disable iff → property expression.

The clause is positioned between the clocking specification and the property expression. Order matters syntactically; production files keep the convention consistent so reviewers can scan for the disable clause at the same line position in every property.

Restart-on-deassert semantics

The key semantic property: when the disable expression goes from true to false (deasserts), every in-flight evaluation of the property is restarted. Multi-step properties that were mid-evaluation when reset asserted don't continue; new evaluations start fresh when reset deasserts.

// Consider this 4-cycle property
property p_full_xfer;
    @(posedge clk) disable iff (rst)
        start ##1 stage1 ##1 stage2 ##1 done;
endproperty
 
// Timeline:
//   T=0:   start=0, rst=0  — nothing pending
//   T=10:  start=1, rst=0  — property starts evaluating
//   T=20:  stage1=1         — property at cycle 2 of 4
//   T=30:  RST ASSERTS      — in-flight evaluation is DROPPED
//   T=40:  RST DEASSERTS    — clean slate; new evaluations can start
//   T=50:  start=1          — fresh evaluation begins
//
// The mid-reset partial evaluation is NOT resumed when reset clears.
// This is the LRM-required behaviour: disable iff means "this evaluation
// did not happen," not "this evaluation is paused."

The restart-on-deassert rule is what makes disable iff the right tool for reset and other don't-care windows. The assertion isn't "pending forever waiting for the next clock"; it's "completely cleared," ready for a fresh evaluation on the next sampling event after the disable expression goes false.

Default disable

Just as properties can share a default clocking block, they can share a default disable iff clause that applies to every property without its own explicit disable.

default disable iff (!rst_n);
 
// All properties without their own disable iff inherit this default
property p_req_ack;
    @(posedge clk) req |=> ack;
endproperty
 
property p_grant_legal;
    @(posedge clk) grant |-> req;
endproperty
 
// Both p_req_ack and p_grant_legal are disabled when !rst_n is high
// (i.e., when rst_n is low — typical active-low reset)

When to use. When most properties in the file share the same disable condition. The default disable iff declaration at module scope keeps individual properties uncluttered. Production protocol VIPs invariably use this pattern; the explicit per-property disable is reserved for properties that need a different disable (e.g., also disable during scan mode, low-power state, etc.).

Per-property disable that overrides the default

default disable iff (!rst_n);
 
property p_normal;
    @(posedge clk) req |=> ack;       // uses default disable
endproperty
 
property p_scan_aware;
    @(posedge clk) disable iff (!rst_n || scan_mode)
        critical |-> response;         // also disabled during scan mode
endproperty

When to use. When some properties need to be disabled under broader conditions than the default — scan mode, debug mode, low-power state, configurable test modes. The explicit disable iff overrides the default for that specific property; other properties still inherit the default.

Putting It Together — A Real APB Property File

The pattern below shows production discipline: default clocking, default disable iff, named properties with consistent structure, and per-property overrides only where they're justified.

package apb_property_file;
    import apb_sequences::*;     // sequence library from Module 12.5
 
    // ── Defaults — apply to every property in this scope ─────────
    default clocking cb_main @(posedge clk); endclocking
    default disable iff (!rst_n);
 
    // ── Property 1 — uses defaults ───────────────────────────────
    property p_psel_before_penable(input bit psel, penable);
        $rose(penable) |-> $past(psel);
    endproperty
 
    // ── Property 2 — uses defaults ───────────────────────────────
    property p_pready_window(input bit psel, penable, pready);
        s_apb_access_phase(psel, penable) |-> ##[0:15] pready;
    endproperty
 
    // ── Property 3 — override: also disabled during scan_mode ────
    property p_normal_op_only(
        input bit psel, penable, pwrite,
        input bit scan_mode
    );
        @(posedge clk) disable iff (!rst_n || scan_mode)
            $rose(penable) |-> !pwrite || pready_within_64;
    endproperty
endpackage

The convention production files maintain: defaults at the top of every property package, explicit overrides documented inline with a comment explaining why. A code reviewer can scan the file and immediately spot which properties depart from the standard discipline; the departures are the ones that need closer review.

Common Pitfalls

Pitfall 1 — Forgetting disable iff entirely

The single most common SVA debugging session. Module 12.4's Debug Lab covered the "247 fails in first 50ns" pattern. The structural fix is disable iff (rst); the discipline rule is "every concurrent assertion in a clocked-RTL environment includes the clause."

Pitfall 2 — Wrong reset polarity

// Active-low reset (rst_n), but disable iff treats it as active-high
property p_wrong_polarity;
    @(posedge clk) disable iff (rst_n)    // BUG: disables when rst_n is HIGH (i.e., NOT in reset)
        req |=> ack;
endproperty
 
// Right: disable when reset is asserted (rst_n is LOW)
property p_correct;
    @(posedge clk) disable iff (!rst_n)
        req |=> ack;
endproperty

Fix: the disable expression should be true when the assertion should be skipped — i.e., during reset. For active-low reset, that's !rst_n (true during reset); for active-high reset, that's rst (true during reset). Production environments adopt a convention (typically default disable iff (!rst_n) for active-low or default disable iff (rst) for active-high) and stick to it across the project.

Pitfall 3 — Using wrong clock in multi-clock environments

// Signal is in the clk_b domain, but assertion clocks on clk_a
property p_wrong_clock;
    @(posedge clk_a)              // BUG: req_b is updated on clk_b
        req_b |=> ack_a;
endproperty
 
// Right: sample req_b on its own clock; ack_a follows on clk_a
property p_correct;
    @(posedge clk_b) req_b ##1 @(posedge clk_a) ack_a;
endproperty

Fix: every signal in a property must be sampled on its own clock. For cross-domain checks, use the multi-clock property form. Mistakenly using one clock for signals from another domain produces metastability-induced false positives or, worse, real-bug-masking false negatives.

Pitfall 4 — Default clocking + bind file scoping confusion

// In assertions_for_apb.sv:
default clocking @(posedge clk); endclocking
default disable iff (!rst_n);
 
property p_handshake;
    req |=> ack;     // uses defaults
endproperty
 
// When this module is BIND-ed into another DUT:
bind some_dut assertions_for_apb a (...);
// The defaults travel with the bound module. They apply inside
// assertions_for_apb but DON'T apply to any properties declared
// in some_dut itself.

Fix: default clocking and default disable iff are scoped to the file/module they're declared in, not globally. When using bind, the bound module's defaults apply only within that module; the parent's properties don't inherit them. Each module (or assertion file) carries its own defaults explicitly.

Debug Lab — "The Assertion Stops Working After Adding default disable iff"

A subtle failure mode that surfaces when the team adopts default disable iff partway through a project.

// Before — every property had explicit disable iff
property p_handshake_v1;
    @(posedge clk) disable iff (!rst_n)
        req |=> ack;
endproperty
 
// After "cleanup" — engineer added default disable iff but flipped polarity
default disable iff (rst_n);     // BUG: rst_n is high during NORMAL operation
 
property p_handshake_v2;
    @(posedge clk) req |=> ack;      // inherits the wrong default
endproperty

default disable iff (!rst_n);   // disable when rst_n is LOW (during reset)
 
property p_handshake;
    @(posedge clk) req |=> ack;
endproperty

Industry Context — Where Clocking and Disable Discipline Lives

• AMBA protocol VIPs. Every published AXI/AHB/APB property package declares default clocking @(posedge ACLK) (or per-protocol equivalent) and default disable iff (!ARESETn) at the package top. Integrators import the package and inherit the discipline automatically.
• CDC verification. Vendor tools (Synopsys SpyGlass CDC, Cadence Conformal-CDC) emit multi-clock property templates with explicit per-property clocking — the cross-domain nature of the assertions means default clocking doesn't apply. Each crossing has its own clock pair.
• DDR/LPDDR controllers. Controller verification environments declare separate default clocking blocks per clock domain (@(posedge ck_t) for the JEDEC interface, @(posedge axi_clk) for the host-side AXI). Properties on each domain inherit the correct default; cross-domain handshakes use explicit multi-clock form.
• UVM RAL property files. Register access properties typically declare default clocking @(posedge bus_clk) and default disable iff (!bus_rst_n || scan_mode || low_power_mode). The triple-disable expression matches the integrator-environment's real don't-care window — RAL properties don't fire during scan or low-power phases.
• Safety-critical / DO-254 / ISO 26262 flows. Every property file's default disable iff clause is part of the certification artifact. Auditors verify the clause covers all the spec-defined don't-care windows and that no property silently re-enables itself by overriding the default with a weaker disable expression.
• Formal verification. Formal tools (JasperGold, VC Formal) require precise clocking and disable specifications to define the legal input space. A wrong disable iff polarity in formal mode produces proofs that exclude the operating regime where bugs actually live — same failure mode as today's debug lab, but with the silent gap appearing in a "passed" formal proof.

The pattern across these uses: clocking and disable are not implementation details. They are part of the spec's verification translation — the spec defines when the contract applies, and the SVA clauses must encode that exactly. Production discipline treats every modification of these clauses with the same scrutiny as a property expression change.

Interview Q&A — Ten Questions You Will Be Asked

Coding Guidelines — Seven Rules for Clocking and Disable Discipline

1. Declare default clocking and default disable iff at the top of every property package. Centralised defaults, single point of edit, consistent enforcement.
2. Use explicit per-property clocking only when the property's clock differs from the default. Multi-clock properties, properties on a non-default clock domain, properties in test files where clarity matters more than brevity.
3. Match the disable polarity to the reset polarity convention. Active-low reset → disable iff (!rst_n). Active-high reset → disable iff (rst). Production environments adopt one convention and apply it everywhere.
4. Override the default disable only with documented justification. Per-property disable iff (!rst_n || scan_mode) is fine when the spec requires it; the override should carry a comment citing the spec section.
5. For multi-clock properties, every signal samples on its own clock. Mixing signals from different domains under one clock produces metastability-induced false positives or real-bug-masking false negatives.
6. Pair every spec-critical assertion with a cover of its antecedent. The cover hit count is the diagnostic that distinguishes "clean run, scenario exercised, contract honored" from "clean run, scenario never reached" or "clean run, assertion silently disabled."
7. Refactors of disable iff get an extra polarity review. Most "I cleaned up the disable clauses and assertions stopped working" bugs are polarity flips during manual translation. The second-reviewer rule catches them before the regression masks them.

Summary

The clocking and disable clauses are the two structural decisions every concurrent assertion makes. The clocking specifies when sampling and evaluation happen — explicit per-property, inherited from default clocking, or multi-clock for cross-domain properties. The disable iff clause specifies when evaluation is skipped entirely; the restart-on-deassert semantics ensure mid-evaluation partial patterns are cleared cleanly when reset deasserts. Production verification environments declare default clocking and default disable iff at the top of every property package and override per-property only with documented justification. The most common SVA debugging session — assertion fires during reset, or assertion silently doesn't fire at all — traces directly to a clocking or disable clause that's either missing, wrong-polarity, or scoped incorrectly. Pair every spec-critical assertion with a cover of its antecedent so the regression dashboard can distinguish "0 fails because clean" from "0 fails because nothing ran." Module 12.8 builds on this with the implication operators (|-> and |=>) in depth — the most common form for property expressions inside the clocking and disable framework this page established.