Hardware Reference
In-Depth Information
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
Search WWH ::
Custom Search