RTL Bench PRO
Open RTL Bench →

SystemVerilog Assertions (SVA)

Assertions are checks you write inside your design or testbench to verify that the hardware behaves exactly as intended. If an assertion fails, the simulation stops or warns you immediately.

Immediate vs. Concurrent

RTL Bench supports basic immediate assertions in both simulation and synthesis.

always_comb begin
  // Immediate assertion: checks instantly
  assert (a != b) else $error("a and b cannot be equal!");
end

Concurrent Assertions (SVA)

Concurrent assertions are evaluated on a clock edge. They are the most powerful tool for verification engineers.

// If req goes high, ack must go high 1 to 3 cycles later
assert property (@(posedge clk) req |-> ##[1:3] ack);
⚠️ Synthesis tools (like Yosys) completely ignore assert property. If you want to simulate assertions, ensure you run the Testbench simulation in RTL Bench, which uses Icarus Verilog.

Frequently asked questions

What is the difference between immediate assertions and concurrent assertions in SVA?

Immediate assertions (assert (condition)) evaluate instantaneously like procedural if statements when executed. Concurrent assertions (assert property (@(posedge clk) ...)) evaluate across clock cycles based on clock edges and sampled signal values, making them ideal for protocol and handshake verification.

Can SystemVerilog Assertions (SVA) be synthesized into hardware?

Most formal and simulation SVA properties are non-synthesizable verification constructs ignored by synthesis tools (using // synthesis translate_off or tool pragmas). Some specialized tools can synthesize assertion checkers into debug logic.

How do assertions help pinpoint bugs faster than waveform inspection alone?

Assertions fire at the exact cycle and simulation time an invariant or protocol assumption is violated, printing descriptive error messages instead of forcing you to manually trace signal discrepancies thousands of cycles later.

Next

Try it in the workbench →