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

expression. Then always @clk becomes always @clock after substitution, and the
assertion clock cannot be inferred from the procedural context of the always .The
assertion might still get its clock otherwise, as from a default clock that applies in
the context of the checker declaration.

Example 14.32. In the following checker, the inferred clock for assertion a1 is

posedge clk .
checker check1(a, clk);
always_ff @( posedge clk)
a1: assert property (a);
endchecker : check1
This inference is due to the structure of the checker itself. The event control of the
checker procedure is an edge expression posedge clk . t

Example 14.33. Consider checker check2 and its instantiations c1 through c5 :
checker check2(a, event clk = $inferred_clock);
always_ff @clk
a2: assert property (a);
endchecker : check2
module m( input logic clock, b, ...);
// ...
check2 c1(b, posedge clock);
check2 c2(b, clock); // Illegal
always @( edge clock) begin :B1
check2 c3(b);
end
always @( edge clock or negedge b) begin :B2
check2 c4(b, edge clock);
check2 c5(b); // Illegal
end
endmodule :m
Assume that no default clock applies to the checker or within the module.
The clock of assertion a2 inferred in the instance c1 is posedge clock since
this is the actual argument passed to clk and it is inferable.
Instance c2 will not compile since the actual argument corresponding to clk is
clock , which is not inferable. In the absence of a default clock, c2.a2 remains
unclocked.
The clock edge clock is inferred for procedural block B1 , so this clock is
passed through $inferred_clock as default actual argument to clk in instance
c3 . edge clock is then inferred for the always_ff procedure in check2 and is the
clock for c3.a2 .
No clock is inferred for procedural block B2 because edge clock and
negedge b are both valid inferable event expressions, so uniqueness is violated
in the Rule of Clock Inferencing. The instance c5 is therefore illegal because there
is no actual argument for clk . t