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

I2 edge_op expr1 [ iff expr2], where edge_op is one of posedge , negedge ,
or edge . 1
We say that an inferable event expression E is valid for an always or initial
procedure provided is satisfies the following:

V1 The procedure has one and only one event control, and E is an expression
appearing in that event control.
V2 There is no other blocking timing control in the procedure.
V3 If E is an event variable or a clocking block event, then E does not appear
in the body of the procedure, except in a clocking event or within an assertion
statement.
V4 If E has the form edge_op expr1 [ iff expr2], then no term in expr1 appears
in the body of the procedure, except in a clocking event or within an assertion
statement.
V5 If E has form edge_op expr1, then a larger event expression E iff expr2 does
not appear in the event control of the procedure.

Now we can state the Rule of Clock Inferencing :

Event expression E is the clock inferred for an always or initial procedure
provided E is the one and only valid inferable event expression for the procedure.
If the number of valid inferable event expressions for the procedure is zero or
greater than one, then no clock is inferred for the procedure.

If no clock is inferred, then clocks may be explicitly specified for the assertions.
Another alternative is to declare a default clock, which provides the clock for
assertions that would otherwise remain unclocked.
The following examples illustrate some details of clock inferencing.

Example 14.4. Clock inferencing with iff in the event control:

always @( posedge clk iff en) begin
d1 <= i1|i2;
a4: assert property (d1 |=> i3|i4);
dout <= f_ecap(d1);
end
The entire expression posedge clk iff en is inferred as the clock, not just
the subexpression posedge clk . According to V5 , the smaller event expression
posedge clk is not valid.

t

1 Note

that while edge v is semantically the same as posedge v or negedge v ,

these forms are not interchangeable for clock inferencing. edge v is inferable, while

posedge v or negedge v is not.