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

The clock posedge e1 is inferred for assertion a11 since it is the only valid
inferable event expression. By V4 , event expression posedge reset is not valid
due to the use of term reset inside the procedure. t

In the example below, the additional event control @( posedge e2) violates V1
and prevents any clock inferencing for assertion a11 .
Example 14.11. No clock inferred—additional event control:

always @( posedge e1) begin
d1 <= i1|i2 ;
@( posedge e2) egL <= sL & sL1;
a11: assert property (d1 |=> i3|i4);
dout <= f_ecap(d1);
end

t

Only one event control may appear in the procedure for clock inferencing.

In the example below, the inclusion of a delay statement #6 violates V2 and bars
clock inferencing for assertion a12 .
Example 14.12.

No clock inferred—presence of a delay statement:

always @( posedge e1) begin
d1 <= i1|i2 ;
#6;
a12: assert property (d1 |=> i3|i4);
dout <= f_ecap(d1);
end

t

Whether a concurrent assertion is placed in an always procedure or an initial
procedure, the assertion is invoked, like any other statement, only if the simulation
execution reaches the assertion statement. From that moment onward, the temporal
assertion evaluation is driven by its leading clock as if the assertion were placed
outside its enclosing procedure. If the leading clock is the same as the contextually
inferred clock, then the evaluation for that clock tick happens in the same time
step as its invocation. Otherwise, the evaluation waits further until the leading
clock occurs. We discuss the precise semantics of scheduling procedural concurrent
assertions later in this chapter.

14.3 Using Automatic Variables

An important consideration in constructing a procedural concurrent assertion is
the presence of variables declared in the procedure that are part of the simulation
execution reaching the assertion statement. Static variables are treated differently