Hardware Reference
In-Depth Information
checker
check(
logic
a, b, c, clk, rst);
1
logic
x, y, z, v, t;
2
assign
x=a;
//CVofa
3
always_ff
@(
posedge
clk
or negedge
rst) // CV of clk and rst
4
begin
5
a1:
assert final
(b);
// SV of b
6
if
(rst)
// CV of rst
7
z<=b;
//SVofb
8
else
z <= !c;
// SV of c
9
end
10
always_comb begin
11
a2:
assert final
(b);
// CV of b
12
if
(a)
//CVofa
13
v=b;
//CVofb
14
else
v = !b;
// CV of b
15
end
16
always_latch begin
17
a3:
assert final
(b);
// CV of b
18
if
(clk)
// CV of clk
19
t<=b;
//CVofb
20
21
end
22
...
23
endchecker
: check
In the values used in the continuous assignment on Line
3
, in the statements
belonging to the
always_comb
procedure (Lines
12
-
15
) and in the statements
belonging to the
always_latch
procedure (Lines
18
-
20
) are not sampled, accord-
ing to the sampling definition in checkers. This behavior is the same as in modules.
The behavior in the statements of
always_ff
procedure (Lines
6
-
9
) is different.
The values of
clk
and
rst
on Line
7
are not sampled because these variables
belong to the event control of the
always_ff
procedure. The value of
b
on Line
6
is sampled, even though it is used in a final assertion because this assertion belongs
to
always_ff
procedure. The value of
rst
on Line
7
is not sampled because it is
used in the event control (Line
4
). The values of
b
and
c
in Lines
8
and
9
are again
sampled, because these statements belong to
always_ff
procedure.
t
9.4.3
Checker Variables in Final Procedures
In this section we provide an example showing usage of checker variables in a final
procedure.
Example 9.25.
In Example
9.12
to check for pending requests at the end of
simulation, we assumed that
req
remains asserted until the reception of
gnt
.The
checker may be modified to work properly even without this assumption. For this
purpose, we introduce a checker variable
intrans
which is set to 1 between the
assertions of
req
and its
gnt
, or more precisely, from the clock tick after
req
until
the clock tick after
gnt
.
Search WWH ::
Custom Search