✅ Two Kinds of Assertion

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.

⚠ Immediate Assertions

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;

▶ Pass and Fail Action Blocks

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.

🏷 Statement Labels

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)

⚠ Severity Levels

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");

📋 Severity Message Content

All four severity tasks automatically print a tool-generated message containing:

• The file name and line number of the assertion statement.
• The hierarchical name of the assertion — the label name if labelled, or the enclosing scope name if not.
• For simulation tools: the simulation time at which the severity task executes.

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

🕐 Deferred Failure Display

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)

📌 Creative Uses of Action Blocks

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 Overview

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;

⏱ Clock Ticks and Sampled Values

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.

• Variable values are sampled in the Preponed region of the clock-tick time step — before any Active events fire in that time step.
• Concurrent assertions are evaluated in the Observed region of the clock-tick time step — after all RTL activity has settled.
• A clock ticks at most once per simulation time — even if the clock signal glitches, sampling occurs at the defined edge only.
• The sampled value of a variable at clock tick N is its value from the end of the previous simulation step — not any intermediate glitching value from the current step.

🔄 Sampling Visualised

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.

⏱ Clock Expressions

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!

📌 Boolean Expressions in Assertions

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.

General rules

• All expressions are evaluated using the sampled values of variables, not their current simulation values.
• The result is always boolean (true/false) — X and Z propagate as false.
• Function calls are allowed, subject to restrictions.

Function call restrictions in assertion expressions

• Functions may not have output or ref arguments — const ref is allowed.
• Functions should be automatic (or stateless) with no side effects — calling them repeatedly with the same inputs must always return the same result.

// 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

📌 Allowed and Forbidden Operand Types

// 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 in Assertion Expressions

Variables that can appear in concurrent assertion expressions must be static design variables or function calls returning allowed types. Specifically:

• Static variables declared in modules — the primary target (RTL signals).
• Static variables declared in programs, interfaces, or clocking blocks.
• Static variables declared in tasks — sampled like any other static variable, independently of task calls.
• Automatic variables are not allowed — they only exist during a task/function call and have no stable value to sample.

// 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);

📌 Operators in Assertion Expressions

All SystemVerilog operators valid for the allowed types may be used in assertion expressions, with two exceptions — both banned to prevent side effects:

// 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

📋 Quick Reference

Immediate vs concurrent assertions

Immediate assertion rules

• Default severity when no else clause: $error.
• Pass action: first statement after closing parenthesis.
• Fail action: statement(s) after else.
• Multiple severity tasks in else: all execute.
• Action blocks are any legal procedural statement — assignments, task calls, event triggers.
• Labels enable %m in format strings and appear in tool error messages.

Concurrent assertion expression restrictions

• Forbidden types: real, string, event, chandle, class, associative/dynamic arrays.
• Allowed types: integer types, fixed-size arrays (whole or slice), structs, enums, function return values.
• Functions: no output/ref args; must be automatic/stateless/no side effects.
• Forbidden operators: all assignment operators (=, +=, etc.) and ++/--.
• Variables: static design variables; static task variables; program/interface/clocking block statics.