Hardware Reference
In-Depth Information
they are written is immaterial. If
actual_expression
is missing, then again the
default actual expression is used.
If a mix of positional and named binding is used, then the positional form must
precede any named form.
8.1.2
Uses of Let
let
is useful for abstracting expressions and for configuring them as templates in
a checker library. A strong case for this abstraction form is when such a template
is picked up from a checker library, and instantiated in immediate and deferred
assertions. The following example illustrates this point, but for detailed discussion
of this topic, see Chap.
24
.
Example 8.10.
let
onehot0(exp,
bit
reset = 1'b0) = reset || $onehot0(exp);
let
noUnknown(exp,
bit
reset = 1'b0) = reset || $isunknown(exp);
module
check(
input
logic
rst,
logic
[15:0] decoded,
logic
[3:0] sel
);
a1:
assert
#0 (noUnknown({decoded, sel}));
a2:
assert
#0 (onehot0(sel, rst));
endmodule
: check
Module
check
is a combinational checker that verifies in assertion
a1
that the
ports
decoded
and
sel
never have an
x
or
z
value in any bit position, and in assertion
a2
that the port
sel
has at most one bit asserted 1 . Assertion
a1
is checking the
expression regardless of whether
rst
is asserted or not because the default value of
0 is used as the actual argument for
reset
. Assertion
a2
is disabled when
rst
is
asserted 1.
t
Notice that we could have used functions
$onehot
and
$isunknown
directly in
the assertions, but then the reset argument would have to be always added in the
expression of the assertion, which can be error prone. The
let
template in a library
allows to hide this detail and makes the use of the functions more user friendly.
Similarly, we could define a template for
$past
that provides different default values
for its arguments than those provided by the function definition. The let declaration
can be placed in a package and then imported wherever needed.
let
declarations are suitable for libraries of property-like templates in
packages to be used in deferred and immediate assertions.
Search WWH ::
Custom Search