Using SystemVerilog Assertions in RTL Code

By Michael Smith,
Doulos Ltd.

Introduction
SystemVerilog is a set of extensions to the Verilog hardware description language and is expected to become IEEE standard 1800 later in 2005. SystemVerilog Assertions (SVA) form an important subset of SystemVerilog, and as such may be introduced into existing Verilog and VHDL design flows.

Assertions are primarily used to validate the behavior 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?"). You can add assertions to your RTL code as you write it " these form "active comments" that document what you have written and what assumptions you have made. Assertions may also be used as a formal specification language, making the requirements clear and unambiguous, and making it possible to automate validation of the design against the specification.

SystemVerilog Assertions are not difficult to learn; in this tutorial, you will learn the basic syntax, so that you can start using them in your RTL code and testbenches.

Properties and Assertions
An assertion is an instruction to a verification tool to check a property. Properties can be checked dynamically by simulators such as VCS, or statically by a separate property checker tool " such as Magellan. They are understood by Design Compiler, which knows to ignore them with a warning. Alternatively, you can use the translate_off/translate_on pragmas.

In SystemVerilog there are two kinds of assertion: 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, which are primarily used by formal tools. Finally, expect is a procedural statement that checks that some specified activity (property) occurs. The three types of concurrent assertion statement and the expect statement make use of sequences that describe the design"s temporal behavior " i.e. behavior 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 should be 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");

You may omit the pass statement yet still include 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 the 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++; $error("A should equal B"); end

Concurrent Assertions
The behavior 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 behavior 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 often 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.

Implication
The implication construct (|->) allows a user to monitor sequences based on satisfying some criteria, e.g. attach a precondition to a sequence and evaluate the sequence only if the condition is successful. The left-hand side operand of the implication is called the antecedent sequence expression, while the right-hand side is called the consequent sequence expression.

If there is no match of the antecedent sequence expression, implication succeeds vacuously by returning true. If there is a match, for each successful match of the antecedent sequence expression, the consequent sequence expression is separately evaluated, beginning at the end point of the match.

There are two forms of implication: overlapped using operator |->, and non-overlapped using operator |=>.

For overlapped implication, if there is a match for the antecedent sequence expression, then the first element of the consequent sequence expression is evaluated on the same clock tick.

s1 |-> s2;

In the example above, if the sequence s1 matches, then sequence s2 must also match. If sequence s1 does not match, then the result is true.

For non-overlapped implication, the first element of the consequent sequence expression is evaluated on the next clock tick.

s1 |=> s2;

The expression above is basically equivalent to:

"define true 1
s1 ##1 "true |-> s2;

where `true is a boolean expression, used for visual clarity, that always evaluates to true.

Properties and Sequences
In the examples we have been using, the properties being asserted are specified in the assert property statements themselves. Properties may also be declared separately, for example:

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

Complex properties are often built using sequences. Sequences, too, may be declared separately:

sequence request
  Req;
endsequence
sequence acknowledge
  ##[1:2] Ack;
endsequence

property handshake;
  @(posedge Clock) request |-> acknowledge;
endproperty

assert property (handshake);

Assertion Clocking
Concurrent assertions (assert property and cover property statements) use a generalized model of a clock and are only evaluated when a clock tick occurs. In fact, the values of the variables in the property are sampled right at the end of the previous time step. Everything in between clock ticks is ignored. This model of execution corresponds to the way a RTL description of a design is interpreted after synthesis.

A clock tick is an atomic moment in time and a clock ticks only once at any simulation time. The clock can actually be a single signal, a gated clock (e.g. (clk && GatingSig)) or other more complex expression. When monitoring asynchronous signals, a simulation time step corresponds to a clock tick.

The clock for a property can be specified in several ways, of which the most common are:

• The clock is explicitly specified in the property:
  property p;
    @(posedge clk) a ##1 b;
  endproperty
  assert property (p);
• The clock is explicitly specified in the concurrent assertion:
  assert property (@(posedge clk) a ##1 b);
• The clock is inferred from a procedural block:
  property p;
    a ##1 b;
  endproperty
  always @(posedge clk) assert property (p);

Handling Asynchronous Resets
In the following example, the disable iff clause allows an asynchronous reset to be specified.

property p1;
  @(posedge clk) disable iff (Reset) not b ##1 c;
endproperty

assert property (p1);

The not negates the result of the sequence following it. So, this assertion means that if Reset becomes true at any time during the evaluation of the sequence, then the attempt for p1 is a success. Otherwise, the sequence (b ##1 c) must never evaluate to true.

Sequences
A sequence is a list of boolean expressions in a linear order of increasing time. The sequence is true over time if the boolean expressions are true at the specific clock ticks. The expressions used in sequences are interpreted in the same way as the condition of a procedural if statement.

Here are some simple examples of sequences. The ## operator delays execution by the specified number of clocking events, or clock cycles.

a ##1 b	// a must be true on the current clock tick // and b on the next clock tick
a ##N b	// Check b on the Nth clock tick after a
a ##[1:4] b	// a must be true on the current clock tick and b // on some clock tick between the first and fourth // after the current clock tick

The * operator is used to specify a consecutive repetition of the left-hand side operand.

a ##1 b [*3] ##1 c	// Equiv. to a ##1 b ##1 b ##1 b ##1 c
(a ##2 b) [*2]	// Equiv. to (a ##2 b ##1 a ##2 b)
(a ##2 b)[*1:3]	// Equiv. to (a ##2 b) // or (a ##2 b ##1 a ##2 b) // or (a ##2 b ##1 a ##2 b ##1 a ##2 b)

The $ operator can be used to extend a time window to a finite, but unbounded range.

a ##1 b [*1:$] ##1 c      // E.g. a b b b b c

The [-> or goto repetition operator specifies a non-consecutive sequence.

a ##1 b[->1:3] ##1 c      // E.g. a !b b b !b !b b c

This means a is followed by any number of clocks where c is false, and b is true between one and three times, the last time being the clock before c is true.

The [= or non-consecutive repetition operator is similar to goto repetition, but the expression (b in this example) need not be true in the clock cycle before c is true.

a ##1 b [=1:3] ##1 c      // E.g. a !b b b !b !b b !b !b c

Putting It All Together
Now that we have seen the basic syntax, let"s look at a couple of practical examples.

"A request (req high for one or more cycles then returning to zero) is followed after a period of one or more cycles by an acknowledge (ack high for one or more cycles before returning to zero). ack must be zero in the cycle in which req returns to zero."

assert property ( @(posedge clk) disable iff reset
                  !req ##1 req[*1:$] ##1 !req
                  |->
                  !ack[*1:$] ##1 ack[*1:$] ##1 !ack );

"After a request, ack must remain high until the cycle before grant is high. If grant goes high one cycle after req goes high then ack need not be asserted."

assert property ( @(posedge clk) disable iff reset
                  $rose(req) |=> ack[*0:$] ##1 grant );

where $rose(req) is true if req has changed from 0 to 1.

Summary and Conclusions
In this tutorial, you have learnt the basic syntax of the SystemVerilog Assertions language. This includes immediate and concurrent assertions, properties and sequences. Using these, you can incrementally add assertions to your RTL code, which makes bugs easier and quicker to detect, thus improving the quality of your designs.

Further Information
Doulos's Modular SystemVerilog training program provides full-scope training in SystemVerilog and includes a training module specifically on the use of SystemVerilog assertions. The courses include full support for Synopsys tools, including Design Compiler and VCS.

Public Modular SystemVerilog classes are scheduled in the USA and Europe, and team-based training is available worldwide. Dates and locations currently scheduled are these:

July 26 San Jose, CA, USA
Aug 1 Cambridge, UK
Sept 26 Austin, TX, USA
Oct 17 Munich, Germany
Nov 14 Cambridge, UK
Nov 28 San Jose, CA, USA

Doulos also publishes the SystemVerilog Golden Reference Guide, a comprehensive quick reference for the entire SystemVerilog language. A new SystemVerilog Assertions Golden Reference Guide will be available later in the year.

About Michael Smith
Michael Smith is a co-founder of Doulos Ltd. and has over 20 years experience in training and supporting ASIC and FPGA designers in the use and application of simulation and synthesis languages and technologies.

About Doulos Ltd.
Doulos is the global leader for the development and delivery of training solutions for engineers creating the world"s electronic products.