Assertions - Variables

Variables can be used in sequences and properties. A common use for this occurs in pipelines:

`define true 1

property p_pipe;
logic v;
@(posedge clk) (`true,v=DataIn) ##5 (DataOut === v);
endproperty

In this example, the variable v is assigned the value of DataIn unconditionally on each clock. Five clocks later, DataOut is expected to equal the assigned value. Each invocation of the property (here there is one invocation on every clock) has its own copy of v. Notice the syntax: the assignment to v is separated from a sequence expression by a comma, and the sequence expression and variable assignment are enclosed in parentheses.

Coverage Statements

In order to monitor sequences and other behavioural aspects of a design for functional coverage, cover property statements can be used. The syntax of these is the same as that of assert property. The simulator keeps a count of the number of times the property in the cover property statement holds or fails. This can be used to determine whether or not certain aspects of the designs functionality have been exercised.

module Amod2(input bit clk);bit X, Y;
sequence s1;@(posedge clk) X ##1 Y;endsequence
CovLavel: cover property (s1); ...endmodule

SystemVerilog also includes covergroup statements for specifying functional coverage. These are introduced in the Constrained-Random Verification Tutorial.

Assertion System Functions

SystemVerilog provides a number of system functions, which can be used in assertions.

$rose, $fell and $stable indicate whether or not the value of an expression has changed between two adjacent clock ticks. For example,

assert property
(@(posedge clk) $rose(in) |=> detect);

asserts that if in changes from 0 to 1 between one rising clock and the next, detect must be 1 on the following clock.

assert property
(@(posedge clk) enable == 0 |=> $stable(data));

states that data shouldn’t change whilst enable is 0.

The system function $past returns the value of an expression in a previous clock cycle. For example,

assert property (@(posedge clk) disable iff (reset) enable |=> q == $past(q+1));

states that q increments, provided reset is low and enable is high.

The system functions $onehot and $onehot0 are used for checking one-hot encoded signals. $onehot(expr) returns true if exactly one bit of expr is high; $onehot0(expr) returns true if at most one bit of expr is high.

assert property (@(posedge clk) $onehot(state));

Binding

We have seen that assertions can be included directly in the source code of the modules in which they apply. They can even be embedded in procedural code. Alternatively, verification code can be written in a separate program, for example, and that program can then be bound to a specific module or module instance.

For example, suppose there is a module for which assertions are to be written:

module M (...);
// The design is modelled here
endmodule

The properties, sequences and assertions for the module can be written in a separate program:

program M_assertions(...);
// sequences, properties, assertions for M go here
endprogram

This program can be bound to the module M like this:

bind M M_assertions M_assertions_inst (...);

The syntax and meaning of M_assertions is the same as if the program were instanced in the module itself:

module M (...);
// The design is modelled here
M_assertions M_assertions_inst (...);endmodule