Hardware Reference
In-Depth Information
To conclude this section, we wish to mention that unlike wires, let definitions
can be used to define expressions that are temporarily used and not meant to be
synthesized. For instance,
always_comb w=a&b;
assert #0 (w == 1);
If w is used only in the assert statement, the synthesis tool may or may not
synthesize this signal, even though it is not required in the physical implementation
of the design. Using let w=a&b ; instead avoids this problem. The conventional
solution is to use 'ifdef ... 'endif to enclose nonsynthesizable code but it is
less elegant.
It will be interesting to see what other uses will be devised for let , and what
kind of support various software tools will provide for debugging code that contains
let statements. Since let is part of the language unlike macros, it may be possible
to trace its evaluations and even collect coverage.
8.2
Sequence and Property Declarations
Sequence and property declarations allow users to compose temporal formulas into
units that can be instantiated in other such units as well as in assertions. This
mechanism thus provides means for abstracting temporal behavior to building more
complex temporal formulas. The declarations of a sequence and property are
named, and available with optional arguments. The formal argument list definition
in sequence declarations is similar to that in property declarations, except that the
latter also allows properties as arguments. The declaration interface and substitution
of an instance by the body of its definition are similar to let , but more complex due
to the presence of clocks and disabling conditions. Furthermore, formal argument
list and the association of the formal with actual arguments differs considerably
from the port list defined for modules, programs, interfaces, functions, and tasks.
We illustrate briefly some of these constructs in the following example. More
details are provided in the subsequent section.
Example 8.11.
sequence sf_after_a(
event clk = $inferred_clk, logic a, sequence sf, int n=1);
@( posedge clk) a ##n sf;
endsequence
property seq_impl_prop( logic rst = $inferred_disable,
event clk = $inferred_clk, sequence sf, property pf);
disable iff (rst) @clk sf |-> pf;
endproperty
The sequence sf_after_a has as its formal argument a clocking event named
clk . It has a default actual argument which is, in this case, the system function
$inferred_clock . In the absence of an actual argument, it infers the clocking event
Search WWH ::




Custom Search