Introduction - SVA: The Power of Assertions in SystemVerilog - page 4

1 module m( input logic c, clk);
2 logic a = 1'b0;
3 logic b = 1'b1;
4 always @( posedge clk) begin
5 a<=c;
6 b<=!c;
7 end
8 // assertion
9 a1: assert property (@( posedge clk)a!=b)
10 else $error("a != b does not hold");
11 endmodule :m

Fig. 1.1 A simple assertion

needs of designers to perform design verification with the assistance of assertions,
sometimes as the central groundwork in monitoring the progress of a design project.
By assertions, we mean statements that express properties to be true in a more
general sense, without implying any specific intention or application. Although the
most common application is for checking a design in order to detect bugs, other uses
include making assumptions about the environment and tracking test scenarios for
functional or behavioral coverage. Later in this chapter, we introduce various forms
of applications that are provided by SVA.
SystemVerilog provides assertion features that are declarative. That is, assertions
do not describe how to check, but only what to check. Figure 1.1 shows a simple
exampleofanassertioninSVA.
Consider module m . Its functionality is implemented in Lines 4 - 7 using an
always procedure 4 and nonblocking assignments.
Assertion a1 checks at each rising edge of clock clk that a!=b . If the assertion
does not hold, an error message a != b does not hold is issued. This assertion
may be checked in simulation or by formal verification tools.
The experience of using assertions has shown important benefits described below.

Implementing Checks in Verilog Is Difficult

One could ask how RTL correctness was checked in Verilog before the invention
of SystemVerilog. Checks can be obtained by implementing Verilog code that is
equivalent to writing assertions.
To appreciate why assertion implementation in RTL code is nontrivial and error
prone, consider checking that grant should be asserted four clock cycles after req .
For simplicity we ignore here the reset issue (see Exercise 1.2 ). A natural solution

4 The reader may be used to the term “ always block”, but according to the SystemVerilog 2012
standard, this construct is called “ always procedure”.