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