Immediate assertions

An immediate assertion checks a Boolean expression at the moment it is executed in procedural code. It has no notion of clocks or sequences — just "is this true right now?".

// fifo_ptr_checks.sv — simple immediate assertions inside a design
always_comb begin
  // The occupancy counter can never exceed the depth
  a_count_le_depth: assert (count <= DEPTH)
    else $error("FIFO count %0d exceeds depth %0d", count, DEPTH);

  // full and empty are never both true
  a_not_full_and_empty: assert (!(full && empty));
end

Formal tools treat an immediate assertion in always_comb as "must hold in every reachable state, every cycle". In simulation, however, procedural code can execute several times within one time step while signals settle, so a plain immediate assertion can fire on a transient glitch.

Deferred assertions

To avoid glitch failures in simulation, SystemVerilog provides deferred immediate assertions, which report only the final value in the time step:

always_comb begin
  a_onehot_sel: assert final ($onehot0(sel));   // evaluated once values have settled
end

assert #0 is an older, weaker form of the same idea. For formal there is no difference — the tool sees settled values anyway — but writing assert final keeps your properties reusable in simulation.

When to use immediate assertions

• Invariants on the current state: ranges, one-hot encodings, mutually exclusive flags.
• Checks inside functions or generate loops where a clock is not naturally available.
• Designer-written sanity checks embedded in RTL.

Anything that relates values in different cycles needs a concurrent assertion, covered next.