Procedural Concurrent Assertions - SVA: The Power of Assertions in SystemVerilog - page 302

In this chapter, we describe how concurrent assertions can be placed in
procedural code and how one can make use of the code context in which they
are placed. There are many nuances that need to be understood for proper usage of
procedural concurrent assertions. We discuss a commonly used form for replicating
assertions by placing them in a for-loop. We describe in detail the simulation
semantics, that is, how procedural assertions are evaluated in simulation. We
describe the use of the disable statement to abort evaluations of procedural
concurrent assertions that have been invoked but not yet committed. Finally, we
explain how the instantiation of a checker in procedural code creates procedural
concurrent assertions, from both static and procedural concurrent assertions in the
checker declaration.

14.1 Using Procedural Context

Due to the temporal behavior of concurrent assertions, they are restricted to
be placed either in an always procedure or an initial procedure. Contrary
to functions and other constructs which must not incur any time delays, these
procedures allow evaluations to continue past a single time unit. The always
procedure may be of any kind, including always_comb , which has an implicit event
expression for controlling the execution of the procedure. Concurrent assertions
cannot be placed in a function, task, or a class.

Concurrent assertions may only be placed in an always or initial

procedure.

Let us start with a simple example of placing a concurrent assertion in an always
procedure.

Example 14.1. A concurrent assertion in an always procedure:

module e1Unit( input logic clk, ...);
logic i1, i2, d1, dout;
always @( posedge clk) begin
d1 <= i1|i2;
dout <= d1;
a1: assert property ( nexttime [2] dout == $past(i1|i2, 2));
end
...
endmodule
A new evaluation attempt of assertion a1 is started each time a clock tick
posedge clk occurs, and this clocking event is used to reckon time within a1 .
a1 evaluates to make sure that the current value of i1|i2 becomes the value of