Assertion Statements - SVA: The Power of Assertions in SystemVerilog - page 68

4.4 Concurrent Assertions

Concurrent assertions have the same format as the immediate simple and deferred
ones, however, their action blocks are not limited to subroutine calls as in the case
of deferred assertions. The action blocks may contain any statements and their body
may have a more complex structure:

concurrent_assertion_body ::=
[clocking_event] [ disable iff ( reset ) ] property

Here, the square brackets are not part of the syntax, they show that the corresponding
constructs are optional.

Example 4.4. The following concurrent assertion

a1: assert property (@( posedge clk)
disable iff (rst) a |-> nexttime [2] b);
is controlled by clocking event posedge clk and has a disabling condition rst .
The assertion property is a |-> nexttime [2] b .

t

Like immediate assertions of any kind, concurrent assertions can be used inside
modules, interfaces, programs and checkers. They can be placed:

￿in always procedures
￿in initial procedures
￿ standalone (also called static)—outside any procedure

For an assertion placed in either of the two procedures, it gets evaluated only
when the control point reaches the assertion statement. Commonly, an assertion is
placed in an initial procedure with the intention of evaluating the assertion only
once. For example, assertion a1 checks that ready is low at the first tick of the
clock:

initial a2: assert property (@( posedge clk) !ready);
In other cases, the assertion is monitored continuously: at each tick of its clock.
For example, assertion a3 checks that ok is high at every tick of the clock:
a3: assert property (@( posedge clk) ok);
Or, an assertion monitored continuously can be placed in an always proce-
dure as:

always @( posedge clk) begin
d1 <= i1 | i2 ;
a4: assert property (d1 |=> i3 | i4);
dout <= f_ecap(d1);
end
Procedural assertions embedded in always procedures are discussed in detail in
Chap. 14 . Their use in checkers is discussed in detail in Chap. 9 and in Chap. 24 .