Assertion Basic

Jan. 20, 2024 || Item:5.1.Assertion Basic

SystemVerilog assertions (SVA) are constructs in the SystemVerilog hardware description and verification language that allow designers and verification engineers to specify and check properties or conditions within a hardware design. Assertions are particularly useful for formal verification, dynamic simulation, and formal property checking.

In SystemVerilog there are two main kinds of assertions: immediate (assert) and concurrent (assert property)

- Immediate assertions: follow simulation event semantics for their execution and are executed like a statement in a procedural block. Immediate assertions are primarily intended to be used with simulation.

- Concurrent assertions: are based on clock semantics and use sampled values of variables. One of the goals of SystemVerilog assertions is to provide a common semantic meaning for assertions so that they can be used to drive various design and verification tools. Many tools, such as formal verification tools, evaluate circuit descriptions using cycle-based semantics, which typically relies on a clock signal or signals to drive the evaluation of the circuit. Any timing or event behavior between clock edges is abstracted away. Concurrent assertions incorporate these clock semantics. While this approach generally simplifies the evaluation of a circuit description, there are a number of scenarios under which this cycle-based evaluation provides different behavior from the standard event-based evaluation of SystemVerilog.

1. Immediate Assertion

Immediate assertions are procedural statements and are mainly used in simulation. An assertion is basically a statement that something must be true, similar to the if statement. The difference is that an if statement does not assert that an expression is true, it simply checks that it is true, e.g.:

if (A == B) ... // Simply checks if A equals B

assert (A == B); // Asserts that A equals B; if not, an error is generated

If the conditional expression of the immediate assert evaluates to X, Z or 0, then the assertion fails and the simulator writes an error message.

Syntax:

label: assert(expression) action_block;

Where:

label (identifier and colon): optional, creates a named block around the assertion statement

action_block: optional, specifies what actions are taken upon TRUE or FALSE of the assertion expression, with syntax:

pass_statement; else fail_statement;

The failure of an assertion has a severity associated with it. There are three severity system tasks that can be included in the fail statement to specify a severity level: $fatal, $error (the default severity) and $warning. In addition, the system task $info indicates that the assertion failure carries no specific severity.

Example:

always @(posedge tb_clk) 
    assert (tb_a && tb_b) $info("At time %3d ns - PASS", $time);
    else $info("At time %3d ns - FAIL", $time);

Output:
At time 2 ns - FAIL
At time 6 ns - PASS
At time 10 ns - FAIL
At time 14 ns - PASS
At time 18 ns - FAIL
At time 22 ns - PASS
...

2. Concurrent Assertion

Concurrent assertions check the sequence of events spread over multiple clock cycles. The Keyword differentiates the immediate assertion from the concurrent assertion is “property”.

The concurrent assertion is evaluated only at the occurrence of a clock tick.

It can be placed in a procedural block, a module, an interface or a program definition.

Example: re-write above example with property

property ex_property;
   @(posedge tb_clk) (tb_a && tb_b);
endproperty 
always assert property(ex_property)
   $info("At time %3d ns - PASS", $time);
   else $info("At time %3d ns - FAIL", $time);

---

Comments:

Leave a comment:

Submit