SVA sequences and properties

In short: SVA sequences describe what happens cycle-by-cycle and properties say when it must hold; |-> checks the consequent on the same clock tick the antecedent completes, while |=> checks it on the next tick, and repetition operators let you compress multi-cycle behavior into one readable check.

SystemVerilog Assertions (SVA) are the backbone of modern assertion-based verification. If you have written a few assert property statements but still hesitate when a reviewer asks "why |=> and not |-> here?", this article walks through the mental model that every verification engineer needs before a real DV interview or a production testbench.

Sequences: the alphabet of temporal checks

A sequence is an ordered description of boolean events spread across clock cycles. The cycle-delay operator ##N advances the clock N times. So req ##1 gnt reads: "req is high this cycle, and exactly one cycle later gnt is high." A range such as ##[1:3] means "between one and three cycles later", and ##[1:$] means "eventually, any number of cycles later". Everything in SVA is sampled in the preponed region, meaning the assertion sees the value of each signal just before the active clock edge, which is why SVA never races with the RTL that drives those same signals.

A bare sequence is not a check. req ##1 gnt; on its own is just a description. It only becomes a pass/fail obligation when wrapped in a property and an assert, assume, or cover directive.

Properties and the implication operators

A property adds the logic of obligation. The most common form is implication: an antecedent sequence that acts as a trigger, and a consequent that must then hold. There are two implication operators, and confusing them is the single most common SVA bug.

• Overlapping — |->: the consequent is evaluated on the same cycle the antecedent's final element matches. Use it when cause and effect are combinationally or same-cycle related.
• Non-overlapping — |=>: the consequent is evaluated starting the next cycle. It is exactly equivalent to |-> ##1. Use it when the effect is registered and appears one cycle after the trigger.

Consider a simple handshake. If your design asserts ack combinationally the same cycle it sees valid && ready, write valid && ready |-> ack. But if ack is a registered output, the correct check is valid && ready |=> ack. Pick the wrong one and you either get a false failure every transaction or, worse, a silently passing assertion that never actually constrains the registered path.

Vacuity: the quiet danger

Implication has a subtle property called vacuous success. When the antecedent never matches, the property passes trivially. A testbench can run ten million cycles, report "assertion PASSED", and have checked nothing because req was never driven. Tools like Synopsys VCS, Cadence Xcelium, and Siemens Questa all report vacuity counts; treat a high vacuous-pass ratio as a red flag, and pair every meaningful assertion with a matching cover property so you can prove the antecedent actually fired.

Rule of thumb: for every assert property with an implication, add a cover property on the antecedent. If the cover never hits, your assertion is decorative.

Repetition operators: compressing time

Writing a ##1 a ##1 a ##1 a is tedious and error-prone. SVA gives three repetition operators that make multi-cycle behavior concise and intent-revealing.

A classic packet check combines them: sop |-> ##1 (!sop)[*0:$] ##1 eop says "after start-of-packet, no second sop appears until end-of-packet arrives." The goto form shines for "wait for the Nth occurrence" patterns — trigger |-> strobe[->3] ##1 done verifies that exactly on the third strobe after a trigger, done follows.

Building a complex, real check

Let us assemble a bus-protocol property that uses everything above. A read request must get its data within 1 to 8 cycles, and the data-valid pulse must last exactly one cycle:

property rd_latency;
  @(posedge clk) disable iff (!rst_n)
  rd_req |=> ##[1:8] rd_dvalid ##1 !rd_dvalid;
endproperty
assert property (rd_latency);

Three things make this production-grade. First, disable iff (!rst_n) aborts the check during reset so you do not log spurious failures while the DUT is held in reset. Second, the ##[1:8] window encodes the real latency spec as a number, not a guess. Third, rd_dvalid ##1 !rd_dvalid enforces the single-cycle pulse shape. This is the kind of layered reasoning interviewers probe for: can you turn an English spec into a temporal check that is neither too loose nor too strict?

Sequences can be reused and parameterized, which keeps large verification environments maintainable — a lesson every team learns the hard way. For a structured grounding in how assertions fit into a complete UVM flow, see our deep dive on assertion-based verification, and for the formal-tool angle, our guide to formal property verification. Teams building silicon in India often pair these skills with hands-on RTL training from ChipXpert's VLSI programs.

Want to write assertions that survive a real tape-out review? Our CourseTron Functional Verification track takes you from your first |-> to signed-off UVM checkers with SVA.

FAQ

When should I use |-> versus |=>?

Use |-> when the consequent is true on the same cycle the antecedent completes (combinational or already-registered effects), and |=> when the effect appears one cycle later (a registered output). |=> is literally shorthand for |-> ##1.

What is a vacuous pass and why should I care?

An implication passes vacuously when its antecedent never matches, so nothing is actually checked. If your coverage shows the antecedent never fired, the assertion gave you false confidence. Always cover the antecedent separately.

What is the difference between [*n] and [->n]?

[*n] requires n consecutive matches with no gaps. [->n] (goto) allows gaps and ends the sequence exactly on the n-th match, which is ideal for "wait until the Nth event" patterns.

Why do I need disable iff?

It aborts an in-flight assertion attempt when the condition (usually reset) is true, preventing noisy failures while the DUT is being reset or held in an undefined state.