Assertions

Assertions are run-time checks for errors which appear in many variations in different language environments. In one way assertions can be coded with existing tools but nowadays there is sometimes better support within the language environment.

As a rough classification, consider a software example where an index might put an array reference outside the array.

• An active test (i.e. with instructions which are part of the finished code) would be considered error handling.
• A run-time fault which is not trapped by the code but detected by (for example) memory management would typically be called an ‘exception’.
• An assertion is a check of the value for verification: part of the source code but not part of the finalised design.

Assertions should be able to raise the confidence that code works without needing to impact the final performance.

Verilog & SystemVerilog

In hardware terms we are primarily concerned with verification – finding faults before implementing and deploying the device. This is where assertions can provide a significant confidence boost.

• Basic Verilog did not directly support explicit assertions, although a similar functionality can be programmed in a testbench … with sufficient effort
• Various Verilog tool implementations have included a variety of more powerful (possibly non-standard) assertion extensions.
  These PSL (Property Specification Language) assertions can be added in what are otherwise comments; they are not described further here.
• SystemVerilog specifies an extensive range of standardised SVA (SystemVerilog Assertions).

This is an overview of the SystemVerilog facilities. It is here to give a starting point; refer ro something more definitive for fuller details.
(The description in the standard is 118 pp.)

Some associated keywords are:

• ‘assert’ — specifies a property that should hold for the design.
• ‘assume’ — specifies a property that should hold for the environment.
• ‘cover’   — specifies a property to be monitored for coverage.

There are two types of SystemVerilog assertions: Immediate Assertions and Concurrent Assertions.

Immediate assertions

Immediate assertions are fairly straightforward: they are ‘immediate’ in the sense that they are not dependent on time. They can be used for things like checking values or signal combinations.

Note that the assert can have an action before the else which is executed each time the assertion is satisfied. An example function would be counting the number of times this has happened.
It's also possible (and sensible!) to give the assertion a name so it can be identified in a wave trace.

Example

(Click to enlarge figure.)

    Log report

The system tasks $info, $warning, $error and $fatal are all ‘print’ outputs, intended for increasing severities of concern.

An assert is a statement, like any other, and needs to be told when to execute: the example above is sensitive to changes in aa and bb so it will be active throughout a simulation run. However a simulation may be halted on the occurence of a failed exception of sufficient ‘severity’ such as an $error but not a $warning.

assume is similar to assert in simulation but has added properties for formal verification.

Concurrent assertions

Immediate assertions happen when they are triggered by an event, such as a signal change. Concurrent assertions check behaviour repetitively, across time, using sampled values. As such they require some sort of timing reference – i.e. a clock. This will often be a/the system clock (but need not be) but should provide some sort of countable cycles.

As might be expected, there is considerable associated syntax which can provide an extensive range of facilities. Let's start with a simple, illustrative example, requiring only a few new functions.

• property indicates this is a concurrent assertion.
• disable suppresses the test iff it would not be meaningful.
• |-> is an implication operator; the left hand side (“antecedent”) being true asserts that the right hand side (“consequent”) should be true.
• ## specifies the difference in time – in this case 1 cycle later.

This therefore asserts that, as long as we are not being reset, if req is active at one clock edge ack is expected to active at the next. This is illustrated in the trace below.

Some more syntax

There is a plethora of accompanying ‘new’ syntax: here are some more salient items.

The |-> implication starts timing (counting) in the cycle(s) the implication is true. There is also a |=> implication which starts one cycle later.   “|=> ##n“ ≡ “|-> ##(n+1)“

The delay operator (“##n“) can also specify time ranges: “##[m:n]“.

You can have sequences on either side of implication operator, thus:
“req ##1 grant |-> ack ##1 !ack“

System tasks “$stable()“, “$rose()“ and “$fell()“ allow changes in signal states to be detected whilst a concurrent assertion is active. BEWARE! Such changes are detected by comparing samples at the chosen sample clock: they are not specified to spot a short glitch if it occurs entirely between two samples.
The system task “$past()“, allows expression from previous samples.

What else is worth including here?
(Work in progress!)

Back to general SystemVerilog

Up to Verilog index