Hardware Reference
In-Depth Information
end
:b3
else begin
:b4
// ...
a1:
assert property
(p);
end
:b4
// ...
end
:b2
// ...
end
:b1
Assertion
a1
is equivalent to the following stand-alone assertion:
assert property
(@(
posedge
clk) en && !cond |-> p);
This equivalent assertion has an additional suffix implication operator
|->
with
the antecedent
en && !cond
. The condition
en && !cond
is the entry condition
of the block
b4
to which the assertion
a4
belongs. This is quite natural since we
expect the assertion attempt to be triggered only when the block
b4
is activated.
t
As we know, assertions may also be placed in the scope of a looping statement.
To be tractable for FV, the looping statement must be statically unrollable, and the
assertion is replicated according to the iterations.
Example 21.32.
Consider the following code fragment:
property
p(
int
i, j);
a[i] |-> ##[1:2] b[j];
endproperty
:p
always
@(
posedge
clk)
begin
:b1
// ...
for
(
int
i = 0; i < 5; i++)
begin
:b2
// ...
for
(
int
j = 0; j < i; j++)
begin
:b3
// ...
a1:
assert property
(p(i, j));
end
:b3:
end
:b2
end
:b1
The assertion
a1
is equivalent to the following 10 stand-alone assertions:
assert property
(@(
posedge
clk) p(1, 0));
assert property
(@(
posedge
clk) p(2, 0));
...
assert property
(@(
posedge
clk) p(4, 3));
Note that the loops
b2
and
b3
are statically unrollable in spite of the fact that the
upper bound of the loop
b3
is not a constant.
t
Search WWH ::
Custom Search