Verification
Assertion
A statement in verification code that checks whether a design property holds true during simulation or formal analysis.
Detailed Explanation
Assertions capture design intent and expected behavior in a formal, checkable manner. Immediate assertions check conditions at a specific point in time. Concurrent assertions describe temporal relationships using sequences and properties that span multiple clock cycles.
SystemVerilog Assertions (SVA) support complex temporal patterns like "if request goes high, grant must follow within 5 cycles." Assertions can run in simulation (dynamic verification) or be proven mathematically (formal verification).
Code Example
systemverilog
// Immediate assertion
always_ff @(posedge clk)
assert (!overflow) else $error("Counter overflow!");
// Concurrent assertion: req must be followed by ack within 5 cycles
property req_ack_protocol;
@(posedge clk) req |-> ##[1:5] ack;
endproperty
assert property (req_ack_protocol);