Hardware Reference
In-Depth Information
module m( input logic clock, logic [7:0] req, ack);
// ...
always @( posedge clock) begin
for ( int i=0;i<8;i++)
if (i != 3) begin
// ...
a1: assert property (req[i] |=> ack[i]);
end
end
endmodule :m
It is important that the loop variable i be automatic. If the loop in the module m were
written as:
always @( posedge clock) begin
int i; //Static lifetime
for (i=0;i<8;i++)
// ...
the resulting assertion would be multiply and redundantly evaluated as
assert property (req[$sampled(i)] |=> ack[$sampled(i)]);
This is unlikely to have been intended (see also the discussion about assertion
instantiation in loops in Sect. 14.4 ). If for some reason it is necessary to have the
loop variable with static lifetime, the const ' cast should be explicitly applied:
check mycheck(req[ const '(i)], ack[ const '(i)]);
t
Example 14.30.
Consider now a checker that contains procedural assertions:
checker check(a, b, c, event clk = $inferred_clock);
default clocking @clk; endclocking
always_ff @clk begin
a1: assert property (a);
a2: assert property (b |=> c);
end
endchecker : check
module m( input logic clock, ok, logic [7:0] req, ack);
// ...
always @( posedge clock) begin
for ( int i=0;i<8;i++)
if (i != 3) begin
// ...
check mycheck(ok, req[i], ack[i]);
end
end
endmodule :m
The checker instantiation is conceptually equivalent to the following code:
module m( input logic clock, ok, logic [7:0] req, ack);
// ...
always @( posedge clock) begin
for ( int i=0;i<8;i++)
if (i != 3) begin
Search WWH ::




Custom Search