Hardware Reference
In-Depth Information
For simplicity, we assume again that both
req
and
gnt
are Boolean.
checker
request_granted(
req,gnt,n=1,
event
clk = $inferred_clock,
untyped
rst = $inferred_disable
);
default clocking
@clk;
endclocking
default disable iff
rst;
bit
intrans = 1'b0;
always_ff
@clk
begin
if
(rst || gnt) intrans <= 1'b0;
else if
(req) intrans <= 1'b1;
end
a1:
assert property
(req |->
nexttime
[n] gnt);
final begin
a2:
assert
(!rst -> gnt || !(req || intrans))
else
$error("Outstanding request at the end of simulation");
end
endchecker
: request_granted
t
9.5
Checkers with Output Arguments
As we have already mentioned in Sect.
9.2.1
, checkers may have output arguments.
There are three main use cases where this checker capability is beneficial:
Returning assertion status from checkers
Writing modular checkers
Using checkers as a testbench
In this section we describe the first two use cases, postponing the discussion of
the third one to Sect.
23.5
. Before we proceed to the use cases we need to describe
the rules imposed on checker output arguments. To keep things clear, we illustrate
these rules on the example of a trivial checker containing a single assignment and
no assertions.
9.5.1
Checker Output Arguments
9.5.1.1
Checker Output Argument Typing
Checker output arguments must be typed, and their type cannot be
sequence
or
property
. The last two limitations are obvious, the first one is caused by the
Search WWH ::
Custom Search