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

In an initial procedure, the flow of execution is initiated at the beginning of
simulation, and is carried on until the end of the procedure, without ever returning
to the initial point again. During this flow of execution, an assertion is invoked
whenever it is reached. Embedding a concurrent assertion in an initial procedure
is shown in Example 14.3 .

Example 14.3. A concurrent assertion in an initial procedure:

module b1Unit( input bit clk, rst, ...);
bit running;
initial begin :B1
if (!rst) begin
a3: assert property (@( posedge clk) running until rst);
...
end
end
...
endmodule
Procedural block B1 is executed at time 0. Suppose that rst is initially low. At that
point, assertion a3 is initiated. It waits until the clock tick posedge clk occurs, and
then starts an evaluation attempt. No more new assertion attempts are started, but
the initial attempt will continue its evaluation until completed in accordance with
the normal assertion semantics.

t

14.2 Clock Inferencing

When an assertion leading clock is not explicitly specified, this clock is inferred
from the assertion context. For concurrent assertions outside procedural code, the
clock inference rules have been discussed in Chap. 12 . For procedural concurrent
assertions, the inferred clock is derived from the preceding event control statement
in the procedure. In the examples seen so far, the inferred clock has been the entire
event expression of the event control. The rules for clock inference follow synthesis
guidelines to provide for more general extraction of an inferred clock. There is some
subtlety to the rules, and in some cases the form of the procedure will not admit any
inferred clock.

Clock inferencing closely follows common design synthesis guidelines.

We say that an event expression is inferable if the entire expression has one of
the following forms:

I1 An event variable or a clocking block event.