The vast majority of real assertions follow the same shape: whenever something happens, then something else must follow. SystemVerilog expresses this with two implication operators, |-> and |=> — and choosing the wrong one is one of the most common mistakes in SVA, since it can produce an assertion that fails constantly even though the design is behaving exactly as intended.
12 min read | Intermediate Level
What You'll Learn
- What "vacuous success" means, and why the consequent is never even checked when the antecedent is false
- The difference between
|->(overlapping) and|=>(non-overlapping), and the automatic 1-cycle gap the latter inserts - Why the exact same signals can be reported as constantly failing under one operator and correctly passing under the other
- Why the "overlap" point for a multi-cycle antecedent is its last cycle, not its first
Vacuous Success: What Happens When the Antecedent Is False?
An implication has the form antecedent |-> consequent (or |=>). If the antecedent doesn't hold on a given cycle, the whole implication is considered true automatically — the consequent is never even evaluated. This is called vacuous success, and it's completely normal: req |-> gnt only has anything to check on cycles where req is actually high; every other cycle passes trivially, with nothing meaningful having been verified.
Overlapping Implication: |->
antecedent |-> consequent requires the consequent to hold starting on the same cycle the antecedent's own match completes — the two overlap at that shared cycle:
assert property (@(posedge clk) req |-> gnt);
This checks: whenever req is high, gnt must also be high on that exact same cycle, with no delay at all.
Non-Overlapping Implication: |=>
antecedent |=> consequent checks the exact same relationship, but with one difference: it automatically inserts a 1-cycle gap, requiring the consequent to hold starting the cycle after the antecedent completes:
assert property (@(posedge clk) req |=> gnt);
This checks: whenever req is high, gnt must be high on the following cycle instead.
Comparing Both on the Same Trace
Here's where the difference actually matters. Take a signal trace where gnt genuinely follows req by exactly one cycle — a completely correct, common design pattern:
| Cycle | 1 | 2 | 3 | 4 | 5 | 6 |
|---|---|---|---|---|---|---|
| req | 1 | 0 | 1 | 0 | 1 | 0 |
| gnt | 0 | 1 | 0 | 1 | 0 | 1 |
Checked with req |-> gnt (same cycle), every single assertion of req fails — gnt is never high on the same cycle as req in this trace:
- Cycle 1:
req=1,gnt=0→ FAIL - Cycle 3:
req=1,gnt=0→ FAIL - Cycle 5:
req=1,gnt=0→ FAIL
Checked with req |=> gnt (next cycle) on the exact same trace, every single one passes:
- Cycle 1:
req=1, checksgntat cycle 2 (=1) → PASS - Cycle 3:
req=1, checksgntat cycle 4 (=1) → PASS - Cycle 5:
req=1, checksgntat cycle 6 (=1) → PASS
The design here is perfectly correct — it's the choice of implication operator that determines whether the assertion recognizes that or not.
Quick Check
Q: If someone wrote req |-> gnt against this exact design and saw it fail on every single cycle where req was asserted, what would that suggest?
Show Answer
Most likely, the wrong implication operator was used — not necessarily a real design bug. A property that fails every single time its antecedent fires, with no exceptions, is a strong signal to double-check whether |=> (or an explicit cycle delay) is what was actually intended.
The Overlap Point for a Multi-Cycle Antecedent
When the antecedent itself spans multiple cycles, the "overlap" in |-> is with the antecedent's last cycle — not its first:
assert property (@(posedge clk) (req ##1 mid) |-> gnt);
Say req is high at cycle 1, and mid is high at cycle 2 — the antecedent req ##1 mid completes its own match at cycle 2, not cycle 1. So gnt needs to be high at cycle 2 (matching mid's cycle) for the overlapping implication to hold — cycle 1, where req happened, is irrelevant to where the overlap actually occurs.
Quick Check
Q: For the same (req ##1 mid) |-> gnt property, at which cycle would |=> instead require gnt to be checked?
Show Answer
Cycle 3 — one cycle after the antecedent's own completion point (cycle 2, where mid occurred), not one cycle after req. The non-overlapping gap is always measured from where the antecedent's match actually ends.
A Useful Equivalence
a |=> b is exactly equivalent to a |-> ##1 b — non-overlapping implication is just overlapping implication with an explicit one-cycle delay already built in. This is worth knowing, because it generalizes: a |-> ##2 b checks a two-cycle gap, a |-> ##[1:4] b checks a flexible window, and so on — |=> is really just the single most common special case of this same pattern.
Where Is This Used?
Essentially every protocol assertion follows this shape — "whenever a request happens, an acknowledge must follow within some number of cycles." Getting the implication operator (or the explicit delay) right is what separates an assertion that actually verifies the protocol from one that either fails constantly on a correct design, or passes vacuously without ever really checking anything meaningful.
Common Beginner Mistakes
Mistake #1: Using |-> when the design's timing actually needs |=>
As the comparison trace shows, this produces an assertion that fails on every single occurrence of the antecedent, even against a correctly-behaving design. Why? If a property fails constantly with no exceptions, check the implication operator (and any needed cycle delay) before assuming the design itself is broken.
Mistake #2: Treating vacuous success as suspicious
A cycle where the antecedent never fires, and the implication passes trivially, is completely normal — not a red flag. Why? That said, if the antecedent never fires across an entire test, the assertion has never actually been exercised at all — that's worth catching with coverage, separately from the assertion's own pass/fail result.
Mistake #3: Assuming |-> overlaps with the antecedent's first cycle
For a multi-cycle antecedent, the overlap point is the antecedent's last cycle — where its own match actually completes. Why? Assuming the overlap happens at the antecedent's starting point instead leads to checking the consequent at the wrong cycle entirely, especially once the antecedent itself takes more than one cycle to resolve.
Mistake #4: Forgetting a |=> b is just a |-> ##1 b
These aren't two unrelated constructs — |=> is a specific, common case of |-> plus an explicit one-cycle delay. Why? Recognizing this makes it much easier to generalize to other fixed or ranged delays (##2, ##[1:4]) using the same |-> foundation, instead of treating each delay amount as its own separate concept.
Practice Exercise
Challenge: Find the Right Delay
Given a trace where gnt follows req by exactly 2 cycles (req at cycles 1 and 4; gnt at cycles 3 and 6), determine whether req |-> gnt, req |=> gnt, or neither correctly captures this relationship — and if neither does, write the property that does.
Hint
Work out exactly which cycle each operator checks gnt on, for both occurrences of req, and compare against where gnt actually is.
Solution
Neither works. req |-> gnt checks the same cycle as req (cycles 1 and 4), where gnt is 0 both times — fails. req |=> gnt checks one cycle later (cycles 2 and 5), where gnt is also 0 both times — also fails. The correct property needs an explicit 2-cycle delay:
assert property (@(posedge clk) req |-> ##2 gnt);
This checks gnt exactly 2 cycles after each req — cycle 3 and cycle 6 — where gnt is genuinely 1 both times, correctly passing.
Summary
In this tutorial, you learned:
- An implication's consequent is only evaluated when its antecedent holds; otherwise the implication passes vacuously
|->(overlapping) checks the consequent on the same cycle the antecedent's match completes|=>(non-overlapping) checks the consequent one cycle later, automatically- The exact same signal trace can fail constantly under one operator and pass correctly under the other — a property failing on every occurrence is a strong signal to check which one was used
- For a multi-cycle antecedent, both operators measure from the antecedent's last cycle, not its first — and
a |=> bis just shorthand fora |-> ##1 b
