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

Example 14.5. No clock inferred - logic variable without an edge operator:

logic clk;
...
always @(clk) begin
d1 <= i1|i2 ;
a5: assert property (d1 |=> i3|i4);
dout <= f_ecap(d1);
end
clk is just a logic variable, without any edge operator, so it is not an inferable event
expression. Therefore, clk is not inferred as the leading clock for assertion a5 . t
Example 14.6. Event variable inferred as clock:

event ev;
...
always @(ev) begin
d1 <= i1|i2;
a6: assert property (d1 |=> i3|i4);
dout <= f_ecap(d1);
end
ev is an event variable and is inferred as the clock for a6 . ev would also be inferred
if it were a reference to a clocking block event. t

Example 14.7. No clock inferred—a variable in the event expression is used in the

procedure:

always @( posedge (e1|e2) iff !reset) begin
d1 <= i1|i2;
e1N = ~e1;
a7: assert property (d1 |=> i3|i4);
dout <= f_ecap(d1);
end
Because term e1 is used in the blocking assignment, Rule V4 specifies that
posedge (e1|e2) iff !reset is not valid. This restriction, however, does not
apply to terms in the right-hand operand expression of operator iff .Term reset
could be used in the always procedure without affecting validity. t

Terms in the right-hand operand expression of iff maybeusedfreelyinthe
procedural block without affecting validity.

Example 14.8. Terms referenced in an assertion statement do not affect validity:

always @( posedge (e1|e2)) begin
d1 <= i1|i2;
a8_1: assert property (d1 |=> i3|i4);