Two kinds of assertions — immediate (procedural, event-driven) and concurrent (clock-based, temporal) — their syntax, pass/fail action blocks, four severity levels, the sampled-value evaluation model, and the constraints on expressions used inside concurrent assertions.
SystemVerilog adds formal assertion support at two levels of abstraction. Choosing the right kind depends on whether the property being checked spans a single moment or multiple clock cycles.
if condition.always, initial, tasks, functions).An immediate assertion is a procedural statement. It evaluates a boolean expression immediately when executed and runs the pass or fail action depending on the result. It can appear anywhere a procedural statement is legal.
// Minimal form: expression only — no pass or fail action assert(a == b); // If a != b: tool calls $error by default (with file/line/time info) // With a fail action only assert(req1 || req2) else $fatal(1, "No request active!"); // With both pass and fail actions assert(myfunc(a,b)) count1 = count1 + 1; // pass: increment coverage counter else ->event1; // fail: trigger an event to alert monitor // In an always block — checked at every posedge clk when state==REQ always @(posedge clk) if (state == REQ) assert(req1 || req2); // Simple flag on failure assert(y == 0) else flag = 1;
if condition.The optional pass statement comes immediately after the closing parenthesis and executes if the assertion succeeds. The optional fail statement follows else and executes on failure. Either or both can be omitted.
// 1. Neither — default $error on fail assert(expr); // 2. Fail only assert(expr) else $error("failed"); // 3. Pass only (null else) assert(expr) count++; // 4. Both pass and fail assert(expr) pass_stmt; else fail_stmt;
// Multiple severity tasks in the else clause: // EACH one executes when the assertion fails assert(valid) else begin $error("Invalid state"); // logged as error ->error_event; // trigger alert fail_count++; // increment counter end
Both the pass statement and the fail statement can be any legal SystemVerilog procedural statement — assignments, task calls, event triggers, even forking threads. The action block executes immediately after the expression is evaluated.
Any assertion (or any other statement) can be given a label using the label_name: prefix. Labels create a named block around the assertion and are printed with %m in format strings — making it easy to identify which assertion fired in a large design.
// Labelled immediate assertion assert_foo: assert(foo) $display("%m passed"); // %m prints: "top.dut.assert_foo" else $display("%m failed"); // Labelled assertion in context req_check: assert(req1 || req2) else $error("%m: At least one request must be active at posedge clk"); // Tool-printed message includes: // — File name and line number // — Hierarchical name (label, if given; otherwise enclosing scope) // — Simulation time (for simulation tools)
bus_grant_valid, fifo_not_overflow, state_reachable.Every assertion failure has a severity level. If no else clause is given, the default severity is $error. Severity is specified explicitly using one of four system tasks in the fail clause.
// Fatal: simulation stops — use for unrecoverable design errors latch_check: assert(!latch_inferred) else $fatal(1, "Latch found in %m"); // Error: simulation continues — use for protocol violations resp_check: assert(resp != 2'bxx) else $error("%m: X propagated to response"); // Warning: suppressible — use for non-critical deviations timing_check: assert(delay < TMAX) else $warning("%m: Marginal timing"); // Info: tracing — use for coverage or milestone markers pkt_sent: assert(send_done) count_sent++; // pass: count else $info("%m: send incomplete");
All four severity tasks automatically print a tool-generated message containing:
Each severity task also accepts an optional format string (same syntax as $display) appended after the mandatory arguments. This user text is printed alongside the automatic message.
// Severity task signatures: $fatal(finish_number); // finish_number passed to $finish $fatal(finish_number, "format", args...); $error(); // no required args $error("format string", args...); $warning(); $warning("format", args...); $info(); $info("format", args...); // Example: rich error message bus_ack: assert(bus.ack) else $error("Bus ack missing: addr=0x%0h data=0x%0h", bus.addr, bus.data); // Tool prints: ERROR: file.sv:42: top.tb.bus_ack @100ns // Bus ack missing: addr=0x1234 data=0xABCD
The fail action can execute at a different simulation time than when the assertion fails. In this case, $time evaluated inside the action block captures the current time — not the time the assertion failed. To display the original failure time, capture $time when the assertion fails and use it in a delayed action.
time t; always @(posedge clk) if (state == REQ) assert (req1 || req2) else begin t = $time; // capture failure time = 10ns #5 $error("Fail at time %0t", t); // print at 15ns, but shows "10ns" end // If assertion fails at T=10: // — error message prints at T=15 // — user string says "Fail at time 10" (correctly captures the failure time)
Because action blocks are full procedural statements, they integrate assertions tightly with the testbench infrastructure.
// Coverage: count assertion passes data_valid: assert(data != 0) nonzero_count++; // pass action: functional coverage else $warning("Zero data on bus"); // Signalling: trigger an event to wake up a monitor process resp_ok: assert(resp == OK) else ->err_event; // unblocks any process waiting on err_event // State capture: record state on failure for later analysis assert(fifo.count <= FIFO_DEPTH) else begin fail_time = $time; fail_state = dut.state; fail_count++; $error("%m: FIFO overflow at t=%0t state=%s", fail_time, fail_state.name()); end // Randomisation check: assert randomize() succeeds assert(pkt.randomize()) else $fatal(1, "Constraint solve failed");
Concurrent assertions describe temporal behaviour — properties that span multiple clock cycles. The key difference from immediate assertions is the evaluation model: values are sampled at clock ticks rather than read at the moment of execution.
// Immediate: checks now, uses current signal values assert(req1 || req2); // Concurrent: checks at every posedge clk, uses SAMPLED values // The keyword 'property' distinguishes it from an immediate assertion base_rule1: assert property (@(posedge clk) req1 || req2) pass_stmt else fail_stmt;
property is the distinguishing marker. assert(expr) is an immediate assertion. assert property (...) is a concurrent assertion. Without property, the compiler treats the statement as immediate.A clock tick is an atomic instant in simulation time. At each clock tick, all variable values are sampled — these sampled values are the only values that concurrent assertions can see. The current (unsettled) value of a variable between clock ticks is never used.
The table below shows the difference between the simulation (continuous) value of req and its sampled value at each clock tick.
At clock tick 9: simulation value of req transitions to 1, but the sampled value at that tick is still 0 — because sampling happens in the Preponed region, before any Active transitions.
Every concurrent assertion is tied to an explicit clock definition. The clock controls when sampling and evaluation occur. Clocks can be simple or gated.
// Simple edge clock assert property (@(posedge clk) req |-> ack); // Gated clock using && assert property (@(clk && gating_signal) data_valid); // Gated clock using iff — cleaner for simulation assert property (@(clk iff gating_signal) data_valid); // Same variable in clock and assertion body — different values! // Clock expression uses current value; assertion body uses sampled value assert property (@(posedge clk) clk == 1); // 'clk' in the body is the SAMPLED value from Preponed (before posedge fires) // = 0 in the previous step. This assertion will always fail!
iff qualifier is preferred over && for gated clocks because it expresses clock-gating intent more explicitly.Expressions used in concurrent assertions are evaluated over sampled values. The result is interpreted as a boolean: X, Z, or 0 = false; any other value = true — same as an if condition. However, there are specific restrictions on what can appear in these expressions.
output or ref arguments — const ref is allowed.// Legal: automatic pure function function automatic int count_ones(bit[7:0] x); count_ones = 0; foreach(x[i]) count_ones += x[i]; endfunction assert property (@(posedge clk) count_ones(data) > 0); // Illegal: function with output argument // function int bad(output int x) ... endfunction // assert property (@(posedge clk) bad(y) == 1); // ERROR
shortreal, real, realtime (non-integer types)stringeventchandleclass (object handles)bit, logic, int, byte, longint, etc.)// Array comparisons legal in assertions (fixed-size) logic [7:0] arrayA[0:15], arrayB[0:15]; assert property (@(posedge clk) arrayA == arrayB); // whole array assert property (@(posedge clk) arrayA != arrayB); assert property (@(posedge clk) arrayA[i] >= arrayB[j]); // element assert property (@(posedge clk) arrayB[i][j+:2] == arrayA[k][m-:2]); // slice assert property (@(posedge clk) (arrayA[i] & (~arrayB[j])) == 0); // Struct and union member comparisons typedef struct { int a, b, c, d; } record; typedef int [4] array; union { record r; array a; } p, q; assert property (@(posedge clk) p.a == q.a); // union field assert property (@(posedge clk) p.r == q.r); // struct field
Variables that can appear in concurrent assertion expressions must be static design variables or function calls returning allowed types. Specifically:
// Static variable in a task — legal in assertions task driver; static int pkt_count = 0; // static — has a stable value between calls pkt_count++; endtask // pkt_count is sampled at each clock tick independently of driver() calls assert property (@(posedge clk) driver.pkt_count < MAX_PKTS);
All SystemVerilog operators valid for the allowed types may be used in assertion expressions, with two exceptions — both banned to prevent side effects:
=, +=, -=, *=, /=, %=, &=, |=, ^=, <<=, >>=++, -- (both prefix and postfix)+ - * / %&& || !& | ^ ~== != < > <= >= === !==<< >> <<< >>>?:& | ^ ~& ~| ~^// Legal: arithmetic and comparison in assertions assert property (@(posedge clk) count + 1 <= MAX); assert property (@(posedge clk) (a & b) == 0); // Illegal: assignment or ++ inside assertion expression // assert property (@(posedge clk) (count++ < MAX)); // ERROR: side effect // assert property (@(posedge clk) (x += 1)); // ERROR: side effect
| Feature | Immediate assert | Concurrent assert property |
|---|---|---|
| Evaluated when | Statement executes | At every clock tick |
| Values used | Current simulation values | Sampled values (Preponed region) |
| Temporal span | Single point in time | Multiple clock cycles |
| Where declared | Inside procedural blocks | Modules, interfaces, programs, clocking blocks |
| Clock required | No | Yes (explicit or inherited) |
| X/Z handling | X/Z = false | X/Z = false (sampled) |
| Formal verification | Not directly | Yes — designed for model checkers |
else clause: $error.else.else: all execute.%m in format strings and appear in tool error messages.output/ref args; must be automatic/stateless/no side effects.=, +=, etc.) and ++/--.## concatenation, repetition operators), properties (implication |-> and |=>, not, and, or, if-else), and declaring and using named sequences and properties.