SystemVerilog Assertions Basics

Introduction

An assertion is a statement about your design that you expect to be true always.

- Formal Verification, Erik Seligman et al.

SystemVerilog Assertions (SVA) is essentially a language construct which provides a powerful alternate way to write constraints, checkers and cover points for your design. It lets you express rules (i.e., english sentences) in the design specification in a SystemVerilog format which tools can understand.

For example, let's assume your design specification has the following 2 rules:

1. Every time the request req goes high, ack arrives exactly 3 clocks later
2. Every time the valid signal vld is high, the cnt is incremented

This is how you would express the above statements using SVA.

// Check if ack arrives 3 clocks after a request
assert property (@(posedge clk) req |-> ##3 ack);

// Check if cnt increments everytime vld is set
assert property ((@posedge clk) vld |-> (cnt == ($past(cnt) + 1)); 

Now, when you run a functional simulation, these assertions are monitored by the simulator and if the RTL violates an assertion the simulator reports an error. This is how easy and concise it is to write checkers using SVA.

This article takes you through the basics of

    1. What an assertion looks like
    2. What tools you have at your disposal to write assertions
    3. Code examples
    4. Where do you place assertions in your code

---

Subscribe

Get Notified when a new article is published!

---

Types of Assertions

Let's begin with the types of assertions - there are two of them.

Figure 1: Types of assertions

Immediate Assertions

I like to think of immediate assertions as a simple if statement. These assertions do not depend upon a clock edge or reset.

immediate_assertion_name:              // assertion name
    assert (current_state != 0)        // expression to be checked
    else                               // (optional) custom error message
        $error("%m checker failed");

General structure of an immediate assertion

The above code structure is equivalent to an if condition within an always_comb block. The assertion checks to make sure current_state is never 0.

// This is just dummy code. It's an alternate way to think of immediate assertion.
always_comb begin
    if (assertion statement)
        // do nothing;
    else
        $error("fail");
end

As the simulation test runs, the simulator continuously checks the expression within assert(). If it returns false, the error message is printed. I usually skip the error message because the simulator prints a default message with the assertion name in the absence of a custom error message.

Concurrent Assertions

Concurrent assertions let you describe more complex expressions that span time and are triggered relative to a clock edge.

The keyword property distinguishes an immediate from a concurrent assertion. There are two formats

// Format 1 - Inline expression
concurrent_assertion_name:                          // assertion label
    assert 
        property (                                  
            @(posedge clk) disable iff (rst)        // sampling event
            req |-> ##3 gnt                         // expression to check
        )
        else                                        // (optional) error message
            $error("%m no grant after request");

// Format 2 - Separate property block 
property ConcurrentPropName;
   @(posedge clk) disable iff (rst)
   req |-> ##3 gnt;
endproperty
AssertionName: assert property (ConcurrentPropName);

General structure of a concurrent assertion

The above example shows the general structure of a concurrent expression.

• The assertion is disabled during reset
• The variables in the expression are sampled at the edge of the clock specified
• The expression checks if a grant gnt arrives 3 clocks after request req is made.
• If the expression returns false, an error is reported

I like to think of concurrent assertions as if statements within an always_ff block. Like this

// This is just dummy code. It's an alternate way to think of concurrent assertion.
always_ff @(posedge clk) begin
    if (rst) begin
        // in rst
    end else begin
        if (assertion expression)
            // do nothing;
        else
            $error("fail");
        end
    end
end

As you write assertions for your design, you'll find yourself using concurrent assertions a lot more frequently than immediate assertions.

Implication Operator

When you look at examples of concurrent assertions, you'll see |-> and |=> operators frequently used. These are called implication operators and the LHS of the operator is called the antecedent and the RHS is called the consequent.

|-> : Overlapping implication - The RHS is evaluated from the same cycle LHS is true
|=> : Non-overlapping implication - The RHS is evaluated one clock cycle after LHS is true

Consider the following example waveform. The code below shows how to express this waveform with |-> and |=>.

Figure 2: Implication operator example

// If inputs vld=1 and dat=8'h55, then ack is high 3 cycles later.

// The RHS is evaluated from the same cycle LHS is true
valid_gnt_chk: assert property(@posdege (clk) disable iff (rst)
            (vld && dat == 8'h55) |-> ##3 ack);

// The RHS is evaluated one clock cycle after LHS is true
valid_gnt_chk: assert property(@posdege (clk) disable iff (rst)
            (vld && dat == 8'h55) |=> ##2 ack);

To keep code readable and consistent, you could just stick to using the |-> operator.

System Functions & Operators

Examples from the previous sections briefly introduce the implication operator and $past() system function. The tables below list some more useful tools that let you write assertion expressions.

Function	Use
$rose	returns true if the LSB of the expression changed to 1. Otherwise, it returns false.
$fell	returns true if the LSB of the expression changed to 0. Otherwise, it returns false.
$stable	returns true if the value of the expression did not change. Otherwise, it returns false.
$past(expression, num_cycles)	Returns value of expression from num_cycles ago
$countones	Returns the number of 1s in an expression
$onehot	Returns true if exactly one bit is 1. if no bits or more than one bit is 1, it returns false.
$onehot0	Returns true is no bits or just 1 bit in the expression is 1
$isunknown	Returns true if any bit in the expression is 'X' or 'Z'

... Table 1: SVA system functions

Operator	Use
##n ##[m:n]	Delay operators - Fixed time interval and Time inteval range
!, ||, &&	Boolean operators
|->	Overlapping implication
|=>	Nonoverlapping implication
not, or, and	Property operators

... Table 2: SVA operators

Operator	Use
[*n] [*m:n]	Continuous repetition operator. The expression repeats continuously for the specified range of cycles.
[->n] [->m:n]	Go to repetition operator. Indicates there's one or more delay cycles between each repetition of the expression. a[->3] is equivalent to (!a[*0:$] ##1 a) [*3]
[=n] [=m:n]	Non-consecutive implication. a[=3] is equivalent to (!a[*0:$] ##1 a ##1 !a[*0:$]) [*3]

... Table 3: Repetition operators

Check out the examples in the next section ... read on!

Note

The table above lists operators most frequently used in SVAs. There are several more - intersect, throughout, within, etc. In my opinion, while these operators are powerful, they lead to confusion. Most assertions can be written using the above table.

Assertion Examples

Here is a set of commonly used code patterns which represent how assertions can be used.

// FIFO level cannot go down without a pop.
property FifoLevelCheck;
   @(posedge clk) disable iff (rst)
   (!rd_vld) |->
   ##1 (fifo_level >= $past(fifo_level));
endproperty
FifoLevelCheck_C: assume property (FifoLevelCheck);

// when there's a no_space_err, the no_space_ctr_incr signal is flagged
// for exactly once clock
property NoSpaceErrCtr;
   @(posedge clk) disable iff (rst)
   (no_space_err) |-> (no_space_ctr_incr ^ $past(no_space_ctr_incr));
endproperty
NoSpaceErrCtr_A: assert property (NoSpaceErrCtr);

// if there's an uncorrectable err during an ADD request,
// err_cnt should be incremented in the same cycle and an interrupt
// should be flagged in the next cycle
property AddUncorErrCheck;
   @(posedge clk) disable iff (rst)
   (uncor_err && (req_type == ADD)) |->
   (err_cnt_incr ##1 intr);
endproperty
AddUncorErrCheck_A: assert property (AddUncorErrCheck);

// INIT and FLUSH transactions should complete within MAX_LATENCY.
property LatencyCheck;
   @(posedge clk) disable iff (rst)
   ((req_type == INIT) ||
    (req_type == FLUSH)) |->
   (block_latency < MAX_LATENCY);
endproperty
LatencyCheck_A: assert property(LatencyCheck);

// interrupt should never get set
property InterruptCheck;
   @(posedge clk) disable iff (rst)
   (!intr);
endproperty
InterruptCheck_A: assert property (InterruptCheck);

// wr_data should be stable until wr_ack arrives
property WriteData;
   @(posedge clk) disable iff (rst)
   (wr && !wr_ack) |->
   ##1 (wr_data == $past(wr_data));
endproperty
WriteData_A: assert property (WriteData);

// wr_ack should be asserted only when there's a wr request
property WriteAck;
   @(posedge clk) disable iff (rst)
   (!wr) |-> (!wr_ack);
endproperty
WriteAck1_C: assume property (WriteAck1);

// if wr is asserted, it should remain high until wr_ack is received
property WriteAck2;
   @(posedge clk) disable iff (rst)
   (wr && (!wr_ack)) |-> ##1 wr;
endproperty
WriteAck2_A: assert property (WriteAck2);

// output is not x or z when valid is high
DoutCheck: assert property (@(posedge clk) valid |-> (!$isunknown(dout)));

// Check if ack arrives 3 to 5 clocks after a request
assert property (@(posedge clk) req |-> ##[3:5] ack);

// check if interrupt propagates when intr is enabled
generate
    for (i=0; i < 16; i++) begin: INTR0
        Intr0 : assert property (@(posedge clk) disable iff (rst) 
            ((intr_enable[i] & intr_status[i] ) |-> ##1 intr))
        else `uvm_error ("INTR_ERR", $sformatf ( "[%m] : Interrupt not propagating"))
    end
endgenerate

// When vld rises high -
// .. a is repeated twice then 
// .. after 2 clocks b is repeated 3 to 4 times with gaps in between, 
// .. after last occurence of b, exactly 1 clock later c occurs
// .. one clock after c, d occurs 3 times non-consecutively,
// .. after last occurence of d, there are a variable number of empty
// .. clocks, then e happens
property Repeat1;
    @(posedge clk) disable iff (rst)
    $rose(vld) |-> (a[*2] ##2 b[->3:4] ##1 c ##1 d[=3] ##1 e);
endproperty
Repeat1_A: assert property (Repeat1);

// Going crazy with repetition operators
property Repeat2;
    @(posedge clk) disable iff (rst)
    $fell(reset) |-> ##[3:5] ((st1 ##6 st2) [*2]) ##2 (ready [*1:5]);
endproperty
Repeat2_A: assert property (Repeat2);

Cover Property

In SVA, cover points are written exactly the same way as assertion expressions. By replacing the assert keyword with cover, you ask the simulator tool to update the coverage database if that expression is true.

Apart from the implication operators, |-> & |=>, all other system functions and Boolean operators from Tables 1 & 2 can be used in cover property expressions.

Cover Examples

// Use generate statement to cover all combinations of vld inputs
generate
    for (i=0; i < 16; i++) begin: CVR
        CovVld: cover property (@(posedge clk) {vld3, vld2, vld1, vld0} == i);
    end
endgenerate

property CovRepeat1;
    @(posedge clk) disable iff (rst)
    (a[*2] ##2 b[->3:4] ##1 c ##1 d[=3] ##1 e);
endproperty
CovRepeat1_C: cover property (CovRepeat1);

property CovSimpleKey;
    @(posedge clk) disable iff (rst)
    (key == 512'd0 & key_valid == 1'd0) ##16 (key == fixed_key1 & key_valid == 1'd1) ##1 
    (key == 512'd0 & key_valid == 1'd0) ##64 (key == fixed_key2 & key_valid == 1'd0);
endproperty
CovSimpleKey_W: cover property (CovSimpleKey);

Connecting Assertions to Design

There are two methods to connect assertions to your design.

Using `include

Place assertions in a separate file and `include that file at the end of your design module.

/* File name : bus_arbiter.sv */
// Design module
module bus_arbiter (
input logic clk,
input logic rst,
input logic [7:0] a,
input logic a_vld,
input logic [7:0] b,
input logic b_vld,
output logic [7:0] c);

logic [1:0] arb_sig;
logic [31:0] a_cnt;
logic [31:0] b_cnt;
logic [3:0] current_state;

// ... design code goes here

// place this at the end, right before endmodule
`include "bus_arb_assertions.svh"

endmodule: bus_arbiter

/* File name : bus_arb_assertions.svh */
prop_a_cnt: assert property (
    @(posedge clk) disable iff (rst)
    a_vld |-> (a_cnt == $past(a_cnt) + 1));

property valid_state;
    @(posedge clk) disable iff (rst)
    $onehot0(current_state);
endproperty
prop_valid_state: assert property (valid_state);

// ... other assertions and cover props

Using bind

But, there's a more powerful way to insert assertions into your design -- using the SystemVerilog bind directive.

Place assertions and cover properties in a separate module, then bind this assertions module to one instance or all instances of a design module. This is my favorite method and I use it a lot.

The bind syntax works as follows:

bind {design_module_name/design_instance_name} {sva_module_name} {bind_instance_name} (port_list); 

bind is a way of instantiating a module within another module. In plain english, bind says

please insert the following line

{sva_module_name} {bind_instance_name} (port_list);

within

module design_module;
endmodule

The added advantage with bind is that, you can link your assertions to a specific instance of the module using XMR (cross-module reference). If you `include the assertions as in #2 above, the assertions will be run against all instances of that module. Which may not be your intention.

The bind statement can be placed in your tb_top.

bind tb_top.mod_a.bus_arb_inst sva_bus_arb sva_bus_arb_inst (
    sva_module_port_list
); 

Here's the example from #1 written once again, but using bind

/* File name : bus_arbiter.sv */
// Design module
module bus_arbiter (
input logic clk,
input logic rst,
input logic [7:0] a,
input logic a_vld,
input logic [7:0] b,
input logic b_vld,
output logic [7:0] c);

logic [1:0] arb_sig;
logic [31:0] a_cnt;
logic [31:0] b_cnt;
logic [3:0] current_state;

// ... design code goes here
endmodule: bus_arbiter

/* File name : bus_arb_assertions.sv */
module bus_arb_assertions (
input logic clk,
input logic rst,
input logic [7:0] a,
input logic a_vld,
input logic [7:0] b,
input logic b_vld,
// all signals are inputs to this checker module
input logic [7:0] c,
// also include any internal signals that you
// use in your assertion expression
input logic [3:0] current_state,
input logic [31:0] a_cnt
);

prop_a_cnt: assert property (
    @(posedge clk) disable iff (rst)
    a_vld |-> (a_cnt == $past(a_cnt) + 1));

property valid_state;
    @(posedge clk) disable iff (rst)
    $onehot0(current_state);
endproperty
prop_valid_state: assert property (valid_state);

// ... other assertions and cover props

endmodule: bus_arb_assertions

/* File name : tb_top.sv */
module tb_top;

    ...
    bus_arbiter bus_arb_inst();
    ... 

endmodule: tb_top

bind tb_top.bus_arb_inst bus_arb_assertions bus_arb_sva_inst (
    clk, rst, a, a_vld, b, b_vld, c, current_state, a_cnt );

In a Nutshell

With this article you now know

1. What an immediate and concurrent assertions looks like
2. Operators and system function at your disposal to construct assertions
3. How to write cover properties using assertions
4. How to hook up assertions to your design

References

1. SystemVerilog LRM IEEE 1800-2012
2. Applied Formal Verification - Douglas Perry & Harry Foster
3. Formal Verification - Erik Seligman, et. al
4. A Practical Guide for SystemVerilog Assertions - Srikanth Vijayaraghavan, et. al
5. Wavedrom waveform generator

Questions & Comments

For questions or comments on this article, please use the following link.

---

Sign-up for the Newsletter

Every month or so I send out a newsletter with notable technical papers, notifications about new articles and lessons from my experience.

If you found this content useful then please consider supporting this site! 🫶