Immediate vs concurrent SVA

In short: Use an immediate SystemVerilog assertion as a procedural, sampling-free check inside always/initial or task code when you want to test a value the instant you reach that line, and a concurrent assertion when you need to verify temporal behaviour across one or more clock edges using a sampled, clocked sequence.

SystemVerilog Assertions (SVA) come in two fundamentally different flavours, and confusing them is one of the most common mistakes engineers make when they first move from writing testbench code to writing real checkers. Both are called "assertions", both can fire a pass or fail action, and both appear in interview questions constantly — yet they evaluate at completely different moments in simulation time and obey different semantics. Understanding exactly when each one triggers is the difference between a checker that catches a bug and one that silently passes garbage.

What an immediate assertion actually does

An immediate assertion is a procedural statement. It behaves like an if inside your RTL or testbench code: when the simulator's program counter reaches the assertion, it evaluates the expression right then, using the current (not sampled) values of the variables, and executes the pass or fail block immediately.

always @(posedge clk) begin
  // immediate assertion inside procedural code
  assert (fifo_count <= DEPTH)
    else $error("FIFO overflow: count=%0d", fifo_count);
end

Because it runs in the Active region of the event scheduler, an immediate assertion sees whatever value the variable holds at that instant — including mid-delta-cycle glitches. That makes it perfect for checks that have nothing to do with time: a legal one-hot state, a non-null pointer in a class-based testbench, a function argument range, or a computed result inside a task. SystemVerilog also offers assert final (evaluates in the Reactive region, avoiding glitches) and deferred immediate assertions written assert #0, which postpone evaluation to the Observed/Reactive region to dodge false firings from combinational settling.

Key fact: An immediate assertion has no implicit clock and no sampling. It fires the moment control flow reaches it. If you put a raw combinational signal in one, you may get spurious failures as the signal settles within the same time step — which is exactly why deferred (#0) immediates exist.

What a concurrent assertion actually does

A concurrent assertion is declarative and clocked. It describes behaviour over time using a sequence or property and is evaluated on a sampling clock edge. Crucially, it reads the sampled value of each signal — the value from the Preponed region, i.e. the value just before the clock edge. This single rule eliminates the race conditions that plague naive clock-edge checks.

// concurrent assertion: req must be granted within 1-3 cycles
property p_req_ack;
  @(posedge clk) disable iff (!rst_n)
  req |-> ##[1:3] ack;
endproperty
assert property (p_req_ack)
  else $error("ack did not arrive 1-3 cycles after req");

Here |-> is the overlapping implication operator and ##[1:3] is a cycle-delay range. The property only starts checking when req is sampled high, then watches up to three clock edges for ack. Concurrent assertions live outside procedural blocks (module scope, interfaces, or inside always only when attached to a clock) and are the backbone of protocol checking for AMBA AXI, APB, and memory controllers.

Side-by-side comparison

A worked example: req/ack handshake

Suppose a bus master asserts req and the slave must raise ack on the very next cycle. An immediate assertion cannot express "next cycle" — it has no notion of cycles. You would have to hand-build a state flag and sample it yourself, which is error-prone. A concurrent assertion says it in one line:

assert property (@(posedge clk) req |=> ack);

The non-overlapping implication |=> means "if req is sampled true, then on the next clock ack must be true." This is why verification teams at companies building with Synopsys VCS, Cadence Xcelium, or Siemens Questa write the overwhelming majority of their RTL checkers as concurrent assertions — formal tools like Synopsys VC Formal and Cadence JasperGold can only prove temporal properties expressed concurrently.

When to reach for each

Reach for an immediate assertion when the thing you are checking is true or false at a single point with no reference to a clock: verifying a coverage-model index stays in range, asserting a queue is non-empty before a pop_front(), or guarding a divide-by-zero in a reference model. These live naturally inside the procedural code that already computes the value.

Reach for a concurrent assertion whenever the property involves sequence, timing, or stability across cycles: "grant is one-hot every cycle", "write data is stable while wvalid is high until wready", or "FIFO never overflows between pushes". These are the properties formal engines prove and that protocol monitors reuse across every testbench.

Key fact: A subtle trap — an immediate assert (a == b) placed in a clocked always block still reads live values, so if a and b update in the same block you can read a half-updated state. The equivalent concurrent assertion reads both from the stable Preponed region and avoids the race entirely.

For the deeper theory of building reusable checkers, see our companion piece on assertion-based verification, and for the sequence-operator mechanics that make concurrent properties expressive, read SVA sequences and properties. Teams that want hands-on, tool-driven coaching often pair self-study with the design-services expertise at Avecas VLSI design services.

Want to write production-grade SVA that formal tools can actually prove? The CourseTron Functional Verification track walks you through immediate, concurrent, and formal assertions with real AXI and FIFO checkers built on industry simulators.

Frequently asked questions

Can an immediate assertion check behaviour over multiple clock cycles?

No. An immediate assertion evaluates at a single instant and has no clock. To check anything spanning cycles you must use a concurrent assertion, or manually store state in variables and re-check them — which is far more error-prone.

Why does my concurrent assertion seem to use "old" values?

That is by design. Concurrent assertions read signals sampled in the Preponed region, just before the clock edge, so the value is the one that was stable going into the edge. This removes read/write races between your RTL and the checker.

What is a deferred immediate assertion?

Written as assert #0 (...) or assert final (...), it postpones evaluation to the Observed or Reactive region so combinational signals have settled. It is still "immediate" (no clock, no temporal span) but avoids spurious failures from glitches.

Do formal tools support immediate assertions?

Formal property checkers such as Cadence JasperGold and Synopsys VC Formal primarily reason about concurrent (temporal) properties. Immediate assertions inside procedural code are generally treated as simulation-only checks, so write proof targets as concurrent assertions.