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