Print format strings with support for Verilog constructs.
(vl-fmt x alist &key (ps 'ps)) → ps
- x — Guard (stringp x).
- alist — Guard (alistp alist).
(vl-fmt x alist &key (ps 'ps)) extends the basic formatted-printing routine,
vl-basic-fmt, with new directives for more conveniently printing Verilog
modules. In particular, while vl-basic-fmt only supports a small set of
directives like ~|, ~%, ~x0, and ~s0, vl-fmt
additionally supports ~a and ~m, which are convenient when we want to
tell the user about some parse-tree construct.
Although vl-basic-fmt does not yet implement many ACL2 directives, we
might imagine wanting to support its other directives. So we have kept our
directives separate from those mentioned in :doc fmt.
The more complicated directives, namely ~a, ~m, and ~w, are
handled by attachments. The following description pertains to the default
implementation of those directives, provided by the book
"centaur/vl/mlib/fmt". A simpler version is provided in
- ~a, the "(almost) anything directive"
- This directive can handle most Verilog constructs and is our preferred way
to print things in warning messages. It understands how to pretty-print:
Because this directive is intended for warning messages, it only prints short
summaries of any contexts and module elements. On the other hand, it prints
expressions, ranges, statements, and arguments "in full".
- ~m, the "module name directive"
- The corresponding argument should be a string that is the name of a module,
but can also be an entire module. In html mode, a link to this module will be
- ~w, the "wire name directive"
- The corresponding argument should be a string that is the name of something
in the module's namespace, for instance wire names. But this can also be used
for names of module instances, gate instances, parameters, etc. In html mode,
a link to this module element will be printed.
The ~l directive is deprecated and is now a synonym for ~a. It was
formerly the "location directive" and printed a location.