Hardware Reference
In-Depth Information
checker
check_latency(en, data_ready, max_latency,
1
event
clk = $inferred_clock,
2
untyped
rst = $inferred_disable);
3
default clocking
@clk;
endclocking
4
default disable iff
rst;
5
6
7
let
ub(x) = $clog2(x + 1) - 1;
let
nstages = $bits(en) + 1;
8
let
stage_ub = ub(nstages);
9
let
big_latency = max_latency + 1;
10
let
latency_ub = ub(big_latency);
11
12
13
rand bit
start;
bit
[stage_ub:0] stage = '0;
14
bit
[latency_ub:0] latency = '0;
15
16
17
bit
go;
assign
go = data_ready && start;
18
19
20
function type
(stage) next_stage;
if
(rst)
return
0;
21
if
(stage == 0 && go)
return
1;
22
if
(stage != 0 && stage != nstages && en[stage])
23
return
stage + 1;
24
return
stage;
25
endfunction
: next_stage
26
27
28
function type
(latency) next_latency;
if
(rst || latency == 0 && !go)
return
0;
29
if
(latency == big_latency)
return
big_latency;
30
return
latency + 1;
31
endfunction
: next_latency
32
33
34
always
@clk
begin
stage <= next_stage();
35
latency <= next_latency();
36
end
37
38
39
a1:
assert property
(
$rose(stage == nstages) -> latency != big_latency);
40
endchecker
: check_latency
41
Fig. 23.1
Checking pipeline latency
1.
start
is low at both clock ticks 10 and 20.
2.
start
is low at clock tick 10 and high at clock tick 20.
3.
start
is high at clock tick 10 and low at clock tick 20.
4.
start
is high at both clock ticks 10 and 20.
In the first, we never start counting and do not check anything; in the second,
we check only the transaction starting at clock tick 20; in the third, we check only
Search WWH ::
Custom Search