Assertions - Introduction

Introduction

Assertions are primarily used to validate the behaviour of a design. ("Is it working correctly?") They may also be used to provide functional coverage information for a design ("How good is the test?"). Assertions can be checked dynamically by simulation, or statically by a separate property checker tool – i.e. a formal verification tool that proves whether or not a design meets its specification. Such tools may require certain assumptions about the design’s behaviour to be specified.

In SystemVerilog there are two kinds of assertions: immediate (assert) and concurrent (assert property). Coverage statements (cover property) are concurrent and have the same syntax as concurrent assertions, as do assume property statements. Another similar statement – expect – is used in testbenches; it is a procedural statement that checks that some specified activity occurs. The three types of concurrent assertion statement and the expect statement make use of sequences and properties that describe the design’s temporal behaviour – i.e. behaviour over time, as defined by one or more clocks.

Immediate Assertions:

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.

An immediate assertion may include a pass statement and/or a fail statement. In our example the pass statement is omitted, so no action is taken when the assert expression is true. If the pass statement exists:

assert (A == B)
$display ("OK. A equals B");

it is executed immediately after the evaluation of the assert expression. The statement associated with an else is called a fail statement and is executed if the assertion fails:

assert (A == B)
$display ("OK. A equals B");
else
$error("It's gone wrong");

Note that you can omit the pass statement and still have a fail statement:

assert (A == B)
else
$error("It's gone wrong");

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.

Here are some examples:
ReadCheck: assert (data == correct_data)
else
$error("memory read error");
Igt10: assert (I > 10)
else
$warning("I has exceeded 10");

The pass and fail statements can be any legal SystemVerilog procedural statement. They can be used, for example, to write out a message, set an error flag, increment a count of errors, or signal a failure to another part of the testbench.

AeqB: assert (a == b)
else begin error_count++; $err or("A should equal B"); end

Concurrent Assertions

The behaviour of a design may be specified using statements similar to these:

"The Read and Write signals should never be asserted together."

"A Request should be followed by an Acknowledge occurring no more than two clocks after the Request is asserted."

Concurrent assertions are used to check behaviour such as this. These are statements that assert that specified properties must be true. For example,

assert property (!(Read && Write));

asserts that the expression Read && Write is never true at any point during simulation.

Properties are built using sequences. For example,

assert property (@(posedge Clock) Req |-> ##[1:2] Ack);

where Req is a simple sequence (it’s just a boolean expression) and ##[1:2] Ack is a more complex sequence expression, meaning that Ack is true on the next clock, or on the one following (or both). |-> is the implication operator, so this assertion checks that whenever Req is asserted, Ack must be asserted on the next clock, or the following clock.

Concurrent assertions like these are checked throughout simulation. They usually appear outside any initial or always blocks in modules, interfaces and programs. (Concurrent assertions may also be used as statements in initial or always blocks. A concurrent assertion in an initial block is only tested on the first clock tick.)

The first assertion example above does not contain a clock. Therefore it is checked at every point in the simulation. The second assertion is only checked when a rising clock edge has occurred; the values of Req and Ack are sampled on the rising edge of Clock.