Skip to content
VLSIMentor

SystemVerilog · Module 12

SVA Properties

The named-contract layer above sequences. `property ... endproperty`, the parts a property gates around a sequence (clocking, disable iff, implication, negation), local variables for cross-cycle value capture, parameterised properties, and the discipline that turns sequences into reviewable spec rules with grep-friendly names.

Module 12 · Page 12.6

What a Property Is

Module 12.5 introduced sequences — the named temporal patterns that describe what happened. A property is the named contract layer above sequences — it adds when the contract applies (clocking, reset disable), how it's gated (implication, negation), and what binding the sequence has to local state (local variables). A property is what gets assert-ed, cover-ed, or assume-ed.

The conceptual division of labour:

  • A sequence says "req followed two cycles later by ack."
  • A property says "on every clock edge, when reset is deasserted, if req happens then 2 cycles later ack must happen."
  • An assertion construct says "enforce this property — fire $error if it fails."

You can write everything inline as one expression inside assert property (...) — and tutorials and small examples often do. Production codebases name the property, name the sequences inside it, and assemble the assertion from named pieces. The naming is what makes a 500-assertion property file reviewable.

Declaring a Property

A property is declared with property ... endproperty. It has a name, optional arguments, an optional clocking specification (typically the assertion's clocking), an optional disable iff clause, and a property expression — which can be a boolean, a sequence reference, an implication, or a more complex composition.

SystemVerilog — property declaration grammar
Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
property p_handshake_completes;
    @(posedge clk) disable iff (rst)        // clocking + reset disable
        req |=> ack;                          // property expression
endproperty
 
a_handshake:
assert property (p_handshake_completes)
    else $error("[%0t] req-ack handshake violation", $time);
 
// Same property reused for cover — proves the scenario was exercised
c_handshake_hit:
cover property (p_handshake_completes);

The reading rule: a property is the noun a verification engineer reviews against a spec section. The p_handshake_completes name maps one-to-one to the spec row "every request must be acknowledged the following cycle." Reviewers can read the property file alongside the spec and check each property's correspondence — naming and clear structure are what make this review possible.

The Property Expression Grammar

A property expression can take any of the following shapes. The full grammar is in the LRM (IEEE 1800-2017); the shapes below cover ~95% of production assertions.

Expression formExampleMeaning
Booleanreq && ackBoth high in same cycle
Sequence references_handshakeThe named sequence holds
Overlapping implicationreq |-> ackSame cycle: if req, then ack
Non-overlapping implicationreq |=> ackNext cycle: if req, then ack next cycle
Property negationnot p_violationThe property must NOT hold
and / orp1 and p2, p1 or p2Both / either property holds
nexttimenexttime ackack holds at next clock edge
if/elseif (cond) p1 else p2Conditional property selection

The two implications (|->, |=>) are by far the most common — most spec rules are conditional, and implication is how SVA expresses conditional temporal contracts.

SystemVerilog — the four most common property shapes
Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
// ── 1. Sequence reference — wraps a sequence in property semantics
property p_handshake;
    @(posedge clk) disable iff (rst)
        s_apb_full_transfer;     // sequence from Module 12.5
endproperty
 
// ── 2. Overlapping implication — same-cycle dependency
property p_grant_implies_request;
    @(posedge clk) disable iff (rst)
        grant |-> req;
endproperty
 
// ── 3. Non-overlapping implication — next-cycle dependency
property p_req_followed_by_ack;
    @(posedge clk) disable iff (rst)
        req |=> ack;
endproperty
 
// ── 4. Property negation — "this must NOT happen"
property p_no_overflow;
    @(posedge clk) disable iff (rst)
        not (push && full);
endproperty

Implication vs boolean — the conceptual key. A boolean property req && ack is true on every cycle where both are high. An implication property req |-> ack is true on every cycle except when req is high and ack is low — it's "vacuously true" when req is low (the consequent doesn't matter), and fails only when req is high and the consequent fails. This vacuous-truth behaviour is what makes implication the right tool for conditional spec rules.

Local Variables — (local int v) and the , Operator

Properties can declare local variables that capture values from the antecedent and reuse them in the consequent. This is the SVA mechanism for "the data sampled when the request arrived must match the data on the response."

SystemVerilog — properties with local variables
Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
// ── Capture the address at the request; check it matches at the response
property p_address_matches;
    bit [31:0] captured_addr;
    @(posedge clk) disable iff (rst)
        ($rose(req), captured_addr = addr_bus) |=>
        (ack ##1 (addr_bus == captured_addr));
endproperty
 
// The (boolean, assignment) shape captures the antecedent's data;
// the consequent references the captured value.
// Reads: "When req rises, capture addr. Next cycle, ack must rise,
//          and the cycle after that, addr must equal the captured value."
 
// ── Captured value used to enforce a CRC-style contract
property p_data_integrity;
    bit [31:0] expected_data;
    @(posedge clk) disable iff (rst)
        (start_xfer, expected_data = compute_crc(payload)) |=>
        ##[1:16] (rcv_crc == expected_data);
endproperty

The (boolean, assignment) syntax inside a sequence position is how local variables are introduced. The comma separates the boolean trigger from the variable assignment; the assignment happens at the cycle the trigger fires. After that, the local variable is in scope for the rest of the property — typically referenced in the consequent of an implication.

When local variables matter. Anywhere the spec ties two non-adjacent cycles' values together — "the address driven on the AW channel must match the address on the B response," "the transaction ID must round-trip unchanged," "the data computed at start matches the data observed at end." Without local variables, these properties cannot be expressed as a single SVA contract.

Parameterised Properties

Properties accept arguments — typed parameters that customise behaviour for the call site. The argument list goes in parentheses after the property name.

SystemVerilog — parameterised property
Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
property p_response_within(
    int unsigned       max_delay,
    string             signal_name
);
    @(posedge clk) disable iff (rst)
        $rose(req) |-> ##[1:max_delay] ack;
endproperty
 
// ── Reuse the same property with different deadlines
a_response_16:
assert property (p_response_within(16, "AXI"))
    else $error("AXI response > 16 cycles");
 
a_response_4:
assert property (p_response_within(4, "AHB"))
    else $error("AHB response > 4 cycles");

The benefit is the same as parameterised functions in any language: one property definition, many call sites with customised behaviour. For protocol VIPs that need to support multiple speed grades or configurable timing parameters, parameterised properties are the canonical pattern.

Limit on parameters. Property parameters must be compile-time constants in the LRM — runtime values cannot be passed because the property's structure (especially ##[1:max_delay]) needs to be elaborated at compile time. For runtime-varying contracts, you typically write a property that reads the runtime value from a signal rather than passing it as an argument.

A Complete Working Example — APB Property File

The pattern below is the canonical production shape: a property file that imports a sequence library (from Module 12.5), composes named properties with clocking and disable conditions, and uses them in assertions and cover properties — all with grep-friendly naming.

SystemVerilog — APB property file
Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
package apb_properties;
    import apb_sequences::*;     // sequence library from Module 12.5
 
    // ── Property 1: PSEL must rise one cycle before PENABLE ──────
    property p_psel_before_penable(input bit psel, penable);
        @(posedge clk) disable iff (!rst_n)
            $rose(penable) |-> $past(psel);
    endproperty
 
    // ── Property 2: PREADY must arrive within 16 cycles of ACCESS ─
    property p_pready_within_window(
        input bit psel, penable, pready, rst_n
    );
        @(posedge clk) disable iff (!rst_n)
            s_apb_access_phase(psel, penable) |->
                ##[0:15] pready;
    endproperty
 
    // ── Property 3: PADDR/PWRITE stable through the transfer ─────
    property p_addr_stable_through_transfer(
        input bit psel, penable, rst_n,
        input bit [31:0] paddr
    );
        bit [31:0] captured_addr;
        @(posedge clk) disable iff (!rst_n)
            (s_apb_setup_phase(psel, penable), captured_addr = paddr) |=>
                s_apb_access_phase(psel, penable) ##0
                    (paddr == captured_addr);
    endproperty
 
    // ── Property 4: No SETUP without IDLE first (no back-to-back) ─
    property p_idle_before_setup(input bit psel, penable);
        @(posedge clk) disable iff (!rst_n)
            s_apb_setup_phase(psel, penable) |-> $past(!psel);
    endproperty
endpackage
 
// ── Assertion module composes the properties ─────────────────────
module apb_slave_assertions (
    input  bit clk, rst_n,
    input  bit psel, penable, pwrite, pready,
    input  bit [31:0] paddr, pwdata, prdata
);
    import apb_properties::*;
    import apb_sequences::*;
 
    a_psel_before_penable:
    assert property (p_psel_before_penable(psel, penable))
        else $error("[%0t] PENABLE rose without PSEL high last cycle",
                     $time);
 
    a_pready_within_window:
    assert property (p_pready_within_window(psel, penable, pready, rst_n))
        else $error("[%0t] PREADY > 16 cycles after ACCESS started", $time);
 
    a_addr_stable:
    assert property (
        p_addr_stable_through_transfer(psel, penable, rst_n, paddr))
        else $error("[%0t] PADDR changed between SETUP and ACCESS", $time);
 
    a_idle_before_setup:
    assert property (p_idle_before_setup(psel, penable))
        else $error("[%0t] Back-to-back SETUP without IDLE", $time);
 
    // ── Cover companions for each assertion ──────────────────────
    c_pready_window_hit:
    cover property (p_pready_within_window(psel, penable, pready, rst_n));
 
    c_addr_stability_check:
    cover property (
        p_addr_stable_through_transfer(psel, penable, rst_n, paddr));
endmodule

What this code does. Declares four named properties in a package — each corresponds to one APB spec rule. The property p_addr_stable_through_transfer uses a local variable (captured_addr) to compare the address at SETUP to the address at ACCESS — the canonical use case for local variables. The assertion module imports the property package, instantiates each property with the relevant signal connections, and pairs each assert with a cover to confirm the regression exercised the scenario.

How to simulate it. Compile the property + sequence packages alongside the assertion module and DUT. Run an APB regression. Each assertion failure surfaces with the named property identifier (a_addr_stable); cover properties report hit counts.

Expected output (fragment).

Simulation log fragment
Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
# *E,ASRTST: [142] PADDR changed between SETUP and ACCESS
#   a_addr_stable failed at 142ns
#   captured_addr=0x40, current paddr=0x44
#
# Coverage summary:
#   c_pready_window_hit:      87 hits
#   c_addr_stability_check:  130 hits
#
# Total assertion failures: 1

What to read out of this. One real spec violation, two cover patterns exercised. The local-variable property's failure log includes both the captured value and the current value — the verification engineer reading the log knows immediately what changed. Without the named property + local variable structure, this same bug would surface as "PADDR is wrong" with no context about what it should have been.

Common Pitfalls

Pitfall 1 — Confusing |-> and |=>

Already covered in Module 12.4. The implication operators differ by one cycle: |-> requires the consequent in the same cycle as the antecedent; |=> requires it in the next cycle. This is the single most common SVA debugging session — and at the property layer, the mistake is often subtle because the property's name doesn't reveal which form was used.

Pitfall 2 — Property without disable iff reset clause

Already covered in Module 12.4. Every concurrent property in a clocked-RTL environment includes disable iff (rst) (or the equivalent). At the property layer, the discipline rule is "every named property is reviewed for disable iff presence" — code review verifies the clause is present and the reset expression matches the design.

Pitfall 3 — Boolean property where implication was meant

SystemVerilog — boolean vs implication
Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
// ── Boolean — true only on cycles where BOTH are high
property p_wrong;
    @(posedge clk) disable iff (rst)
        req && ack;     // BUG: fails on every cycle where req || !ack
endproperty
 
// ── Implication — true on cycles where req implies ack
property p_right;
    @(posedge clk) disable iff (rst)
        req |=> ack;     // passes when req is low (vacuously); fails when req is high but ack not next cycle
endproperty

Fix: when the spec says "if A then B," use implication, not boolean conjunction. The boolean form fires on every cycle where A is low and floods the log; the implication form fires only when A is high and B doesn't follow — matching the spec's intent.

Pitfall 4 — Local variable scoping confusion

SystemVerilog — local variable lifetime
Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
property p_unclear;
    bit [31:0] captured;
    @(posedge clk) disable iff (rst)
        ($rose(req), captured = data) |=> ##5 (rcv == captured);
endproperty
 
// captured is scoped to ONE INSTANCE of the property's evaluation.
// If two `req` rises happen 3 cycles apart (overlapping evaluations),
// each evaluation has its OWN captured value — they don't interfere.
// This is the SVA local variable's per-thread semantics; rely on it.

Fix: local variables are per-evaluation-thread. Each match of the antecedent creates a new evaluation thread with its own copy of the local variable. Don't try to share state across evaluations via local variables — that's not what they're for, and the SVA semantics specifically prevent it. For cross-evaluation state, use module-level signals or a different verification mechanism.

Debug Lab — "The Assertion Passes But Doesn't Catch the Bug"

A failure mode that surfaces when an engineer uses the wrong implication operator and the assertion happens to be vacuously true.

Buggy code
SystemVerilog — wrong implication, false-pass
Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
// Spec: when start_xfer is asserted, data must be valid the NEXT cycle
// Intent: start_xfer |=> data_valid
 
property p_data_valid_next;
    @(posedge clk) disable iff (!rst_n)
        start_xfer |-> data_valid;       // BUG: |-> instead of |=>
endproperty
 
a_data_valid:
assert property (p_data_valid_next)
    else $error("[%0t] data not valid after start", $time);
Symptom

The regression runs. The DUT clearly has the bug — data_valid asserts 2 cycles after start_xfer in the buggy design, not the spec-required 1 cycle. The verification engineer expects a_data_valid to fire. It doesn't. The assertion log shows 0 fails for a_data_valid; the test passes; sign-off proceeds. Three months later, integration testing surfaces the timing bug.

Root cause

The property uses |-> (overlapping implication) instead of |=> (non-overlapping). The contract start_xfer |-> data_valid reads "in the cycle start_xfer is high, data_valid must ALSO be high." In the buggy design, start_xfer is high in cycle N and data_valid is low; the implication should fail. But the engineer mis-encoded the spec rule — the spec says "data_valid in cycle N+1," not "in cycle N." The buggy design also has data_valid low in cycle N (matching the same-cycle reading of the wrong property), so the assertion incorrectly passes.

The deeper failure: the assertion encodes the wrong contract. Even if the DUT were spec-correct, the assertion would not enforce the spec — it enforces a different (stricter, wrong) rule. The assertion's pass-or-fail status doesn't tell you anything about the spec; it tells you about the wrong rule the assertion happened to encode.

Fix

Fix the implication operator to match the spec.

SystemVerilog — corrected non-overlapping implication
Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
property p_data_valid_next;
    @(posedge clk) disable iff (!rst_n)
        start_xfer |=> data_valid;       // FIX: |=> means next cycle
endproperty

The discipline rule that prevents recurrence: every property's |-> or |=> operator choice is reviewed against the spec's exact wording. "Same cycle" → |->; "next cycle" → |=>. Code review must check the operator matches the spec rule's intent — there is no way to infer the right choice from the signal names alone.

The complementary discipline: pair every assert with a cover of the antecedent. If c_start_xfer_seen is firing hundreds of times in the regression while a_data_valid reports 0 fails, the assertion is either vacuously passing (wrong operator, as above) or the contract is being honored (the genuine green state). Without the cover, the assertion's "pass" is ambiguous; with it, you can distinguish the two cases.

Industry Context — Where Property Discipline Lives

  • AMBA protocol VIPs. Every AXI/AHB/APB VIP includes a property file that imports the corresponding sequence library; the properties encode each spec section as a named contract. ARM publishes the property file as a verification IP deliverable — integrators import it, instantiate the properties with their DUT's signal connections, and inherit the entire spec contract.
  • PCIe LTSSM specification. Each link-training state transition is a property. The property file mirrors the LTSSM state-graph spec; the assertion module composes them into the full link-training contract. Formal flows use the properties for compositional model-checking.
  • DDR / LPDDR controller verification. JEDEC timing parameters become properties — p_tRCD_satisfied, p_tRP_after_precharge, p_tRC_min_cycle. Each property uses local variables to track the relevant command's start cycle and verify the timing constraint.
  • UVM register model verification. RAL (Register Abstraction Layer) properties enforce register-access semantics — RO writes are no-ops, W1C writes clear-on-write, locked fields don't change. The properties live in the RAL package and apply to every register-block instance.
  • CDC / RDC verification. Synopsys SpyGlass CDC, Cadence Conformal-CDC, and similar tools emit property templates for every crossing they detect — the integrator reviews and customises. The templates use local variables to capture handshake-protocol state across the crossing.
  • Safety-critical / DO-254 / ISO 26262 flows. Each safety property is named, documented with a spec citation, and reviewed independently. The traceability matrix maps spec rows to property names; auditors verify the mapping during certification.

The pattern across these uses: properties are the spec-to-assertion translation layer. Sequences encode protocol vocabulary; properties encode protocol rules; assertions enforce the properties. The three-layer structure is what scales to industrial verification — a 5000-line property file is reviewable; the equivalent inline-everything assertion file is not.

Interview Q&A — Ten Questions You Will Be Asked

A named contract declared with property ... endproperty. The property has a name, optional arguments, an optional clocking specification, an optional disable iff clause, and a property expression that can be a boolean, a sequence reference, an implication, or a more complex composition. Properties are what assert property (...), cover property (...), and assume property (...) reference; the property is the noun that encodes a spec rule, the assertion is the verb that enforces it.

Coding Guidelines — Seven Rules for Property Discipline

  1. Name every property with a p_ prefix that encodes the spec rule. p_psel_before_penable reads as "PSEL precedes PENABLE" — meaningful to anyone reviewing the property file against the spec.
  2. Group properties in a package; import the package into the assertion module. Centralised contract vocabulary, single point of edit, consistent enforcement across the verification environment.
  3. Every property includes disable iff (reset) covering reset and other don't-care windows. Module 12.4's discipline rule carries forward — no concurrent property runs during reset without explicit justification.
  4. Match |-> and |=> to the spec's wording. "Same cycle" / "in the same cycle" → |->; "next cycle" / "after" / "the following cycle" → |=>. Every implication choice is paired with a comment citing the spec section.
  5. Use local variables for cross-cycle value comparisons; nothing else needs them. Capture-and-compare patterns are the canonical use; sharing state across evaluation threads is not what local variables are for.
  6. Pair every spec-critical property with assert + cover constructs. The assertion catches violations; the cover proves the scenario was exercised. The combination distinguishes "clean run, contract honored" from "clean run, never tested."
  7. Treat the property file as the spec's verification translation. Code review reads the property names alongside the spec sections; if a property's name doesn't trace to a spec row, it shouldn't be in the production file. Sandbox-quality properties for ad-hoc debug live separately.

Summary

Properties are SVA's named-contract layer. The property ... endproperty construct wraps a sequence (or boolean, or implication, or composed sub-property) with clocking, disable iff, implication, negation, and optional local variables. The property is what assert, cover, and assume constructs reference; the same property can drive all three. Local variables enable cross-cycle value capture for "address must match," "data must round-trip," "CRC must verify" contracts. Parameterised properties enable one definition to serve many call sites with different deadlines or signal connections. Production verification environments use sequences-in-properties-in-assertions as a three-layer naming structure that scales to thousands of contracts in reviewable form. Module 12.7 builds on this with explicit clocking and disable iff semantics; Module 12.8 covers the implication operators in depth.