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

1 module m2( input logic c, d, clk);
2 logic a, b;
3 always_comb begin
4 a=c&d;b=c|d;
5 // Immediate assertion
6 a1: assert (a -> b);
7 // Deferred assertion
8 a2: assert final (a -> b);
9 // Concurrent assertion
10 a3: assert property (@clk a != b);
11 end
12 // Deferred assertion
13 a4: assert final (a -> b);
14 // Concurrent assertion
15 a5: assert property (@clk a != b);
16 endmodule :m2

Fig. 1.8 Kinds of assertions

The simplest assertions are immediate assertions . They act as procedural if
statements and are legal in any place where procedural if statements may appear.
Immediate assertions are nontemporal and are executed when the control flow
reaches them. The main advantage of immediate assertions is that they have unre-
stricted applicability in various kinds of designs, synchronous and asynchronous,
and in testbenches. Their ease of use makes them appealing, but the limited
expressiveness lends their efficacy to detecting only simple bugs. In some cases,
they are also prone to producing spurious failures due to simulation races. This is
explained in Sect. 4.2 .
Deferred assertions are an improvement over immediate assertions. They are
similar to immediate assertions in that they are nontemporal and unrestricted in
their use. Two important differences make them immensely useful over immediate
assertions: they do not produce spurious failures, and they can be placed both
inside and outside procedural code. Deferred assertions are further subdivided
into observed and final (sometimes called simply “final”). They are explained in
Sect. 4.3 .
The most interesting and complex assertions are concurrent assertions .Theyare
temporal and can describe design behaviors over time. For example, a concurrent
assertion can state that a request should be granted in two clock cycles. Concurrent
assertions are always clocked. Assertion a1 in Fig. 1.1 is a simple example of a
concurrent assertion. This assertion is Boolean and checked immediately before
the rising edge of clk . Concurrent assertions may appear both inside and outside
procedural code, but they cannot be placed in functions and tasks. The description
of concurrent assertions occupies the major part of this topic.
Figure 1.8 illustrates the use of all three kinds of assertions. Here, assertion a1 is
an immediate assertion, a2 and a4 are final deferred assertions, and a3 and a5 are
concurrent assertions. Operator -> used in assertions a1 , a2 , and a4 is an implication
operator. always_comb used in Line 3 is explained in Sect. 2.2 . Notice that deferred