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