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

dout <= f_ecap(d1);
end
By V4 , the references to terms e1 and e2 in the assertion a8_2 do not affect
validity, so posedge (e1|e2) is inferred as the leading clock for assertion a8_1 .
Such a reference can be in the body property or in an action block of the assertion
statement. t

Terms from an event expression may be used within assertion statements in
the procedural block without affecting validity.

When the event control of a procedure consists of a list of event expressions,
separated either by comma or by operator or , then the Rule of Clock Inferencing
requires that there be only one event expression from the list that is inferable and
valid for the procedure. Otherwise, no clock is inferred from the procedure.

Example 14.9. No clock inferred—two valid inferable event expressions:

always @( posedge e1 or posedge e2) begin
d1 <= i1|i2 ;
a9: assert property (d1 |=> i3|i4);
dout <= f_ecap(d1);
end
The Rule of Clock Inferencing is violated. t

A clock is inferred only if a single valid inferable event expression is specified
in the event control.

In the following example, asynchronous reset is specified as an event expression.
Even though the event control has two inferable event expressions, only one is valid.

Example 14.10. A common use of asynchronous reset event:

always @( posedge e1 or posedge reset) begin
if (reset)
d1 <= 0;
else begin
d1 <= i1|i2;
a10: assert property (d1 |=> i3|i4);
dout <= f_ecap(d1);
end
end