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

dout two clock ticks later. This reflects the intent of the cascade of non-blocking
assignments to d1 and dout . The values of d1 and dout may be changing at
successive clock ticks. Each evaluation attempt of a1 provides its own results,
without interfering in the evaluation of other attempts.

t

Placing an assertion in procedural code can greatly improve the understanding
of the purpose of the procedural code. The surrounding code forms the context
for and motivates the placement of the assertion. This naturally leads to greater
readability and maintainability of the code and the assertion. When the assertion
fails, debugging is improved because the context of the assertion is readily available.
In the above example, it is clear that assertion a1 is placed to ensure the correctness
of propagation of i1|i2 through d1 to dout . If the temporal propagation of values is
violated, an error message is generated to indicate the precise point of failure. This
is immensely useful to the user as the debugging of the failure is made by inspecting
the values of the variables dout , i1 , i2 , and the intermediate quantity d1 .
The context of a procedural concurrent assertion affects the semantics of its
execution in two ways. First, the assertion is treated as a statement by the event
simulation semantics to start an evaluation at the point it is reached in procedural
execution. We shall say that a procedural concurrent assertion is invoked at the point
when it is reached in the flow of procedural execution. Second, the leading clock of
the assertion is inferred from the enclosing procedure and used to mark the passage
of time, just as in any concurrent assertion. These two effects are illustrated in the
following modification of Example 14.1 .

The clock of a procedural concurrent assertion is inferred from its context.

Example 14.2. A concurrent assertion under an enabling condition:

module e1Unit( input logic clk, ...);
logic i1, i2, d1, dout, out_en;
always @( posedge clk) begin
d1 <= i1|i2;
if (out_en) begin
dout <= d1;
a2_1: assert property ( nexttime dout == $past(i1|i2, 2));
end
else
a2_2: assert property ( nexttime $stable(dout));

end
...
endmodule
Assertion a2_1 gets invoked if the value of out_en is true. Otherwise a2_2 gets
invoked. Both assertions infer the clocking event posedge clk from context.

t