Implication Operators

Module 12 · Page 12.8

Why This Module Gets Its Own Page

Modules 12.1, 12.4, and 12.6 all carried the same discipline rule: |-> is same-cycle implication; |=> is next-cycle implication; mismatching the operator to the spec's wording is the single most common SVA debugging session. Module 12.6's Debug Lab showed the failure mode (assertion vacuously passes against the buggy DUT because of an operator-off-by-one). This page is the deep dive on the two operators themselves — what they mean precisely, how to read the spec for the right operator, and the production-grade discipline that prevents the bug class entirely.

The two implication operators look almost identical and produce contracts whose simulation behaviour can differ by exactly one cycle. That one-cycle difference is the difference between "the assertion catches the bug" and "the assertion silently passes while the bug ships."

The Two Operators — Side by Side

The clearest way to internalise the operators is to see them side by side, running on the same stimulus.

property p_overlap;
    @(posedge clk) disable iff (rst)
        req |-> ack;    // SAME-cycle: ack must be high in the cycle req is high
endproperty
 
property p_non_overlap;
    @(posedge clk) disable iff (rst)
        req |=> ack;    // NEXT-cycle: ack must be high one cycle after req
endproperty
 
// ── Stimulus timeline ────────────────────────────────────────────
//   Cycle:    1   2   3   4   5   6   7   8
//   req:      0   1   0   1   0   0   0   0
//   ack:      0   1   0   0   1   0   0   0
//
// p_overlap evaluation:
//   Cycle 1: req=0 → vacuously true
//   Cycle 2: req=1, ack=1 (same cycle) → PASS ✓
//   Cycle 3: req=0 → vacuously true
//   Cycle 4: req=1, ack=0 (same cycle) → FAIL ✗
//   Cycles 5-8: req=0 → vacuously true
//   Result: 1 failure at cycle 4
//
// p_non_overlap evaluation:
//   Cycle 1: req=0 → vacuously true
//   Cycle 2: req=1 → must check ack at cycle 3
//                   Cycle 3: ack=0 → FAIL ✗
//   Cycle 3: req=0 → vacuously true
//   Cycle 4: req=1 → must check ack at cycle 5
//                   Cycle 5: ack=1 → PASS ✓
//   Cycles 5-8: req=0 → vacuously true
//   Result: 1 failure at cycle 2 (reported when checked at cycle 3)

The same stimulus produces different failure points under the two operators — and crucially, if the DUT is implementing the next-cycle handshake but the assertion uses |->, the assertion fires false failures on every cycle where req is high (because ack is correctly low same-cycle, only rising next cycle).

Vacuous Truth — The Conceptual Key

Both implication operators have the same vacuous-truth semantics: when the antecedent is false, the property holds (vacuously) — the consequent is not checked, no fail action runs.

property p_demo;
    @(posedge clk) disable iff (rst)
        valid |=> ready;
endproperty
 
// On cycles where valid is low, the property is vacuously true.
// The assertion does NOT fire. No log entry. No counter increment.
//
// On cycles where valid is high, the property checks: is ready high next cycle?
//   If yes → property passes (this evaluation is reported as "covered")
//   If no  → property fails → fail action runs

This behaviour is why implication is the right tool for conditional spec rules. The spec says "if A then B" — it doesn't say what happens when A doesn't happen. Implication encodes "if A doesn't happen, the rule doesn't apply." A boolean property A && B would fail on every cycle where A is low, flooding the log with irrelevant failures.

The cost of vacuous truth: an assertion that passes purely because the antecedent never fires is silent evidence of nothing. Module 12.6's discipline rule applies: pair every assert property (p_impl) with cover property (p_antecedent) so the dashboard can distinguish "passing because contract honored" from "passing because antecedent never fired."

Sequence Antecedents — Implications with Temporal Triggers

The antecedent of an implication doesn't have to be a single boolean — it can be a sequence. The contract becomes "if this temporal pattern matches, then the consequent must hold."

// The antecedent is a 3-cycle handshake; if that matches, ack must follow
property p_burst_complete;
    @(posedge clk) disable iff (rst)
        (start ##1 data ##1 last) |=> ack;
endproperty
 
// Interpretation:
//   The 3-cycle pattern (start in cycle N, data in cycle N+1, last in cycle N+2)
//   triggers the consequent: ack must be high in cycle N+3.
//
// When the sequence matches at any cycle, the implication fires at that cycle.
// When the sequence doesn't match, the implication is vacuously true.
 
// ── With local variable for cross-cycle comparison ─────────────
property p_addr_returned;
    bit [31:0] captured;
    @(posedge clk) disable iff (rst)
        (req_rose, captured = req_addr) |=> ##[1:16] (resp_addr == captured);
endproperty
 
// The antecedent fires when req rises; the address is captured.
// Within 1-16 cycles, the response must arrive with matching address.

Sequence antecedents are how SVA expresses complex temporal contracts — "given that this multi-cycle pattern happened, the consequence must hold." Most production protocol assertions use sequence antecedents to encode contracts like "if a burst-transfer pattern starts, the corresponding response must complete within K cycles."

The not (overlap) Complement Pattern

The "must never happen" form of a contract is naturally expressed with not:

// Direct form
property p_no_simultaneous_rw;
    @(posedge clk) disable iff (rst)
        not (read && write);
endproperty
 
// Equivalent implication form (more common in production)
property p_no_simultaneous_rw_impl;
    @(posedge clk) disable iff (rst)
        (read && write) |-> 1'b0;
endproperty
// The `|-> 1'b0` form is a tautological "this can never be true" —
// the implication's consequent is constant false, so the property fails
// whenever the antecedent fires.

Production discipline tends to prefer positive forms when possible — assert property (mutex_condition) is more readable than assert property (not (conflict_condition)). But for genuinely negative spec rules ("the design must never produce two grants in the same cycle"), not is the clearest expression.

Reading the Spec for the Right Operator

The single most useful skill for SVA verification is reading the spec carefully enough to pick the right implication operator. The discipline rule is mechanical: every implication operator choice is paired with a comment citing the spec section that justifies it.

Spec language → operator mapping

The ambiguous cases. "After" in a spec can mean any of |->, |=>, or |-> ##[1:K] depending on the protocol's exact handshake; the engineer must read the surrounding context. "Acknowledged" can mean "in the same cycle as the request" (same-cycle handshake, |->) or "in the cycle after the request" (sample-and-hold, |=>); the protocol's clocking determines which. Discipline rule: when the spec wording is ambiguous, add a comment to the property naming the disambiguation and the spec section that informed it.

Worked spec-to-operator translations

// Spec: "AWREADY may rise on the same cycle as AWVALID"
// Operator: |-> (same-cycle implication)
a_awready_same_cycle:
assert property (@(posedge aclk) disable iff (!aresetn)
    awvalid |-> (awready || $past(awready)));
// Reads: if awvalid is high, awready must be high in the same cycle
//        OR was high last cycle (sample-and-hold protocol)
 
// Spec: "ACK must be asserted the cycle after REQ"
// Operator: |=> (next-cycle implication)
a_req_ack:
assert property (@(posedge clk) disable iff (rst)
    req |=> ack);
 
// Spec: "Response must arrive within 16 cycles of the request"
// Operator: |-> with range delay
a_response_window:
assert property (@(posedge clk) disable iff (rst)
    $rose(req) |-> ##[1:16] resp);
 
// Spec: "Two grants must never coexist in the same cycle"
// Operator: |-> 1'b0 (tautological fail) or `not`
a_grant_mutex:
assert property (@(posedge clk) disable iff (rst)
    (grant_a && grant_b) |-> 1'b0);

The pattern is the same across the four examples: the spec wording dictates the operator, and the comment cites the spec section. Verification engineers reading the property file later can verify the operator choice against the cited section directly.

A Complete Working Example — APB Implication Library

The pattern below shows how implication operators are used across a production-shape APB property file. Each property's operator choice is documented; each spec rule maps to one operator.

package apb_implications;
    default clocking @(posedge pclk); endclocking
    default disable iff (!presetn);
 
    // ── Rule 1 (spec §4.2): "PSEL must be high one cycle before PENABLE rises"
    // Operator: $rose(penable) |-> $past(psel)
    // Same-cycle implication: the check happens AT the cycle penable rose
    property p_psel_before_penable(input bit psel, penable);
        $rose(penable) |-> $past(psel);
    endproperty
 
    // ── Rule 2 (spec §4.3): "ACCESS phase follows SETUP phase the next cycle"
    // Operator: |=> (non-overlapping, next-cycle)
    property p_setup_to_access(input bit psel, penable);
        (psel && !penable) |=> (psel && penable);
    endproperty
 
    // ── Rule 3 (spec §4.4): "PREADY must arrive within 16 cycles of ACCESS"
    // Operator: |-> with range delay (combines implication and ##)
    property p_pready_within_window(input bit psel, penable, pready);
        (psel && penable) |-> ##[0:15] pready;
    endproperty
 
    // ── Rule 4 (spec §4.7): "PADDR/PWRITE/PWDATA must remain stable during SETUP→ACCESS"
    // Operator: |=> (next-cycle), with $stable as the consequent
    property p_signals_stable(
        input bit psel, penable,
        input bit [31:0] paddr,
        input bit pwrite
    );
        (psel && !penable) |=>
            ((psel && penable) ##0
            ($stable(paddr) && $stable(pwrite)));
    endproperty
 
    // ── Rule 5 (spec §4.9): "Two transfers must never overlap"
    // Operator: |-> 1'b0 (tautological fail)
    property p_no_overlapping_transfers(
        input bit psel, penable,
        input bit psel_other, penable_other
    );
        ((psel && penable) && (psel_other && penable_other)) |-> 1'b0;
    endproperty
endpackage

What this code does. Five named properties, each encoding one APB spec rule. The operator choice for each property is documented inline with a spec-section citation. A reviewer reading the file with the APB spec open can verify each operator one row at a time. The default clocking and default disable iff from Module 12.7 keep the per-property boilerplate to a minimum.

Expected output (fragment from a regression).

# *E,ASRTST: [142] a_psel_before_penable failed
#   $rose(penable) at 142ns, but $past(psel) was low
#
# Coverage summary:
#   c_psel_before_penable_antecedent:  87 hits  (PSEL+PENABLE handshake triggered)
#   c_setup_to_access_antecedent:      87 hits  (SETUP phase entered)
#   c_pready_window_antecedent:        87 hits  (ACCESS phase entered)
#
# Total assertion failures: 1

The cover properties confirm each antecedent was exercised — the assertions are running, not silently disabled. The one failure has full context ($rose(penable) at a specific time, $past(psel) was low) — the engineer reading this log knows immediately which spec rule was violated and at which time.

Common Pitfalls

Pitfall 1 — The same-cycle / next-cycle confusion

The most common SVA bug class. Beginners read "after" or "follows" in a spec and reach for |-> (which is same-cycle). Discipline rule: every implication choice has a comment citing the spec section and the disambiguation reasoning.

Pitfall 2 — Forgetting that vacuous truth means the antecedent might never fire

// "0 failures" can mean any of:
//   - the contract was honored when the antecedent fired
//   - the antecedent never fired (vacuous truth across all cycles)
//
// Without a cover of the antecedent, the dashboard can't distinguish.
a_handshake:
assert property (req |=> ack);   // 0 fails reported
 
c_handshake_antecedent:
cover property (req);             // 0 hits? Then the assertion never ran.

Fix: pair every spec-critical implication with a cover of its antecedent. The cover hit count is the only diagnostic that confirms the assertion's antecedent fired in the regression.

Pitfall 3 — Boolean condition where implication was meant

// Wrong — fires on every cycle where ack is low or req is high
property p_wrong;
    req && ack;
endproperty
 
// Right — fires only when req is high and ack doesn't follow
property p_right;
    req |=> ack;
endproperty

Fix: when the spec says "if A then B," use implication, not boolean conjunction. The boolean form floods the log; the implication form is silent except when the contract is actually violated.

Pitfall 4 — Implication chain without intermediate naming

// Complex single property — hard to debug when it fails
property p_complex;
    @(posedge clk) disable iff (rst)
        $rose(start) |->
        (((data_valid throughout (1'b1 ##[1:5] burst_end)) and
            ($stable(addr) throughout (1'b1 ##[1:5] burst_end)))
        ##1 done) |=> idle;
endproperty
 
// Better — decompose into named sub-properties
property p_data_stable_through_burst;
    @(posedge clk) disable iff (rst)
        burst_start |-> (data_valid throughout (1'b1 ##[1:5] burst_end));
endproperty
 
property p_addr_stable_through_burst;
    @(posedge clk) disable iff (rst)
        burst_start |-> ($stable(addr) throughout (1'b1 ##[1:5] burst_end));
endproperty
 
property p_done_after_burst;
    @(posedge clk) disable iff (rst)
        burst_end |=> done;
endproperty
 
property p_idle_after_done;
    @(posedge clk) disable iff (rst)
        done |=> idle;
endproperty

Fix: when a single property uses multiple implications or chains complex temporal operators, decompose into named sub-properties. Each sub-property is independently assert-ed and cover-ed; a failure surfaces with the specific sub-property's name; the verification engineer reading the log knows which sub-contract was violated.

Debug Lab — "The Operator Looks Right But the Bug Still Slips Through"

A subtle failure mode that surfaces when an engineer translates a spec sentence to SVA without parsing the timing precisely.

// Spec: "After the request is acknowledged, the response must arrive
//        within 8 cycles."
//
// Engineer's translation:
property p_response_after_ack;
    @(posedge clk) disable iff (rst)
        req |-> ##[1:8] response;
endproperty

// Spec: "After the request is acknowledged, the response must arrive
//        within 8 cycles."
//
// Translation: trigger on $rose(ack), check response within 8 cycles
property p_response_after_ack;
    @(posedge clk) disable iff (rst)
        $rose(ack) |-> ##[1:8] response;
endproperty

Industry Context — Where Implication-Operator Discipline Lives

• AMBA protocol specifications. Every AMBA spec rule uses precise temporal language — "the next clock cycle," "in the same clock cycle," "within N clock cycles." VIPs translate each into the matching SVA operator; deviations are tracked as VIP bugs.
• Formal verification flows. JasperGold, VC Formal, and other formal tools require exact temporal semantics — an implication that's mistranslated produces a formal proof of the wrong property. Formal teams treat operator choice as a first-class review item, with senior engineers reviewing every property's spec mapping.
• PCIe and USB protocol verification. These spec rules are densely temporal — "the LTSSM must transition from Detect.Quiet to Detect.Active within 12 ms" maps to a complex implication with bounded delay; the operator choice is documented in the verification plan's traceability matrix.
• Cache coherence protocol verification. MESI/MOESI state-transition rules combine immediate consequences ("if M and Read, transition to O" — |->) with delayed consequences ("if Invalidate, M-line writeback within K cycles" — |=> with range delay). Production property files document each rule's spec mapping.
• Safety-critical / DO-254 / ISO 26262 flows. Auditors trace every implication operator choice to a spec section; the property file is part of the certification evidence. Mistranslation isn't just a verification bug — it's a certification finding that requires rework.
• UVM monitor checking. UVM monitors compose implication-based properties with the analysis-port pattern from Module 11.9. Each protocol violation surfaces with the named property's identifier; the operator choice is part of the contract documentation.

The pattern across these uses: implication operator choice is treated as semantically loaded engineering, not stylistic preference. The one-cycle distinction matters; production discipline ensures every choice traces to a spec section.

Interview Q&A — Ten Questions You Will Be Asked

Coding Guidelines — Seven Rules for Implication-Operator Discipline

1. Every implication operator choice carries a one-line comment citing the spec section. "Spec §4.2: 'PSEL must be high one cycle before PENABLE'" — the citation is the audit trail.
2. Parse spec sentences event-by-event, not word-by-word. Identify the trigger event, the consequent event, and the time relationship; map each to a part of the implication. Most "looks right but doesn't catch the bug" failures trace to word-for-word translation.
3. Pair every spec-critical implication with a cover of the antecedent. "0 failures" can mean "contract honored" or "antecedent never fired." Without the cover, the dashboard can't distinguish.
4. Use |-> for same-cycle; |=> for next-cycle; combine with ##[m:n] for bounded windows. Match the spec's exact temporal phrasing.
5. Decompose complex implications into named sub-properties. When a property uses multiple implications or chained temporal operators, splitting makes failures localisable and antecedents covered individually.
6. Treat operator choice as semantically loaded engineering. Two reviewers — at least — read every implication operator change against the spec. Polarity flips and operator mismatches are easy to introduce and silent.
7. Use not for naturally negative spec rules; use |-> 1'b0 only when the antecedent is itself complex. Both forms encode "must never happen"; production discipline prefers whichever reads more naturally for the spec rule.

Summary

|-> and |=> are SVA's conditional-contract operators — same-cycle and next-cycle implication respectively. Both have vacuous-truth semantics on cycles where the antecedent is false. Both can take sequence antecedents (and consequents) for complex temporal contracts. The single most common SVA debugging session is an operator-off-by-one mismatch between spec wording and operator choice; the discipline rule that prevents it is "every operator choice carries a comment citing the spec section, and the translation is event-by-event, not word-by-word." Pair every spec-critical implication with a cover of the antecedent so the regression dashboard distinguishes "passing because contract honored" from "passing because antecedent never fired." Module 12.9 builds on this with the repetition operators that compose with implication to encode multi-cycle waiting and bounded patterns.