• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
      • Fgl
      • Vwsim
      • Vl
        • Syntax
        • Loader
        • Warnings
        • Getting-started
        • Utilities
        • Printer
          • Ps
          • Verilog-printing
            • Vl-pp-expr
            • Vl-fmt
              • Vl-progindent
              • Vl-ppc-module
              • Vl-mimic-linestart
              • Vl-maybe-escape-identifier
              • Vl-print-ext-wirename
              • Vl-print-wirename
              • Vl-print-loc
              • Vl-pp-module
              • Vl-pp-describe
              • Vl-print-modname
              • Vl-pp-genblob-guts
              • Vl-pp-origexpr
              • Vl-pp-modinst
              • Vl-pps-module
              • Vl-ppc-modulelist
              • Vl-pp-interface
              • Vl-maybe-strip-outer-linestart
              • Vl-pps-expr
              • Vl-pp-modulename-link
              • Vl-binaryop-precedence
              • Vl-pp-genblob
              • Vl-ppcs-module
              • Vl-pp-paramdecl
              • Vl-pp-package
              • Vl-pp-modulename-link-aux
              • Vl-pp-modelement
              • Vl-pp-interfacelist
              • Vl-pp-bind
              • Vl-pp-arguments
              • Vl-ps-update-mimic-linebreaks
              • Vl-pp-vardecl-aux
              • Vl-pp-repetition
              • Vl-pp-packagelist
              • Vl-pp-modulelist
              • Vl-pp-modinstlist
              • Vl-pp-definition-scope-summary
              • Vl-pp-bindlist
              • Vl-maybe-escape-string
              • Vl-ps-update-show-atts
              • Vl-pps-modulelist
              • Vl-ppcs-modulelist
              • Vl-pp-portdecl
              • Vl-pp-ansi-portdecl
              • Vl-cw-obj
              • Vl-ps-update-copious-parens
              • Vl-pps-origexpr
              • Vl-pp-vardecl-atts-begin
              • Vl-pp-propport
              • Vl-pp-gateinst-atts-begin
              • Vl-pp-gatedelay
              • Vl-pp-foreachstmt-loopvars
              • Vl-pp-dpiimport
              • Vl-pp-clkdecl
              • Vl-gatetype-string
              • Vl-coretypename-string
              • Vl-atts-find-paramname
              • Vl-randomqualifier-string
              • Vl-ps-update-use-origexprs
              • Vl-pp-vardecl-atts-end
              • Vl-pp-taskdecl
              • Vl-pp-scope-summary
              • Vl-pp-namedparamvaluelist
              • Vl-pp-modinst-atts-begin
              • Vl-pp-gatestrength
              • Vl-pp-gateinst
              • Vl-pp-fundecl
              • Vl-nettypename-string
              • Vl-fwdtypedefkind-string
              • Vl-expr-precedence
              • Vl-distweighttype-string
              • Vl-assertdeferral-string
              • Vl-pp-vardecllist-comma-separated
              • Vl-pp-repeateventcontrol
              • Vl-pp-regularport
              • Vl-pp-plainarglist
              • Vl-pp-plainarg
              • Vl-pp-paramvaluelist
              • Vl-pp-namedarglist
              • Vl-pp-modport-port
              • Vl-pp-interfaceport
              • Vl-pp-forloop-assigns
              • Vl-pp-exprdistlist-with-commas
              • Vl-pp-dpiexport
              • Vl-pp-distitem
              • Vl-pp-design
              • Vl-pp-delayoreventcontrol
              • Vl-pp-assign
              • Vl-blocktype-startstring
              • Vl-blocktype-endstring
              • Vl-asserttype-string
              • Vl-alwaystype-string
              • Vl-pp-vardecllist-indented
              • Vl-pp-typedeflist-indented
              • Vl-pp-typedef
              • Vl-pp-set-portnames
              • Vl-pp-sequence
              • Vl-pp-scopetype
              • Vl-pp-regularportlist
              • Vl-pp-propspec
              • Vl-pp-property
              • Vl-pp-paramdecllist-indented
              • Vl-pp-namedparamvalue
              • Vl-pp-namedarg
              • Vl-pp-modport-portlist
              • Vl-pp-interfaceportlist
              • Vl-pp-delaycontrol
              • Vl-pp-defaultdisablelist
              • Vl-pp-defaultdisable
              • Vl-pp-covergroup
              • Vl-pp-constint
              • Vl-pp-clkskew
              • Vl-pp-clkassign
              • Vl-leftright-string
              • Vl-direction-string
              • Vl-cstrength-string
              • Vl-casetype-string
              • Vl-casecheck-string
              • Vl-pp-taskdecllist
              • Vl-pp-specialkey
              • Vl-pp-scopename
              • Vl-pp-rhs
              • Vl-pp-propportlist
              • Vl-pp-program
              • Vl-pp-paramdecllist
              • Vl-pp-paramargs
              • Vl-pp-modelementlist
              • Vl-pp-importlist-indented
              • Vl-pp-import
              • Vl-pp-gclkdecl
              • Vl-pp-fwdtypedeflist
              • Vl-pp-fwdtypedef
              • Vl-pp-exprdist
              • Vl-pp-eventcontrol
              • Vl-pp-dpiimportlist
              • Vl-pp-dpiexportlist
              • Vl-pp-covergrouplist
              • Vl-pp-clkassignlist
              • Vl-pp-class
              • Vl-pp-cassertionlist
              • Vl-pp-assertionlist
              • Vl-pp-alias
              • Vl-vardecl-hiddenp
              • Vl-pps-range
              • Vl-pp-weirdint
              • Vl-pp-vardecllist
              • Vl-pp-value
              • Vl-pp-udp
              • Vl-pp-typedeflist
              • Vl-pp-string
              • Vl-pp-sequencelist
              • Vl-pp-rangelist
              • Vl-pp-propertylist
              • Vl-pp-programlist
              • Vl-pp-portlist
              • Vl-pp-portdecllist
              • Vl-pp-paramvalue
              • Vl-pp-modport
              • Vl-pp-lifetime
              • Vl-pp-initiallist
              • Vl-pp-initial
              • Vl-pp-importlist
              • Vl-pp-genvar
              • Vl-pp-gclkdecllist
              • Vl-pp-gateinstlist
              • Vl-pp-fundecllist
              • Vl-pp-finallist
              • Vl-pp-extint
              • Vl-pp-elabtasklist
              • Vl-pp-distlist
              • Vl-pp-configlist
              • Vl-pp-config
              • Vl-pp-clkdecllist
              • Vl-pp-classlist
              • Vl-pp-assignlist
              • Vl-pp-alwayslist
              • Vl-pp-always
              • Vl-pp-vardecl
              • Vl-pp-udplist
              • Vl-pp-time
              • Vl-pp-real
              • Vl-pp-port
              • Vl-pp-final
              • Vl-pp-elabtask
              • Vl-lifetime-string
              • Vl-expr-dollarsign-p
              • Vl-dpispec->string
              • Vl-dpiprop->string
              • Vl-dpifntask->string
              • Vl-ps->copious-parens-p
              • Vl-ps->show-atts-p
              • Vl-ps->mimic-linebreaks-p
              • Vl-ps->use-origexprs-p
              • Vl-progindent-block-start
              • Vl-progindent-block-end
              • Vl-cw
            • Basic-printing
            • Printing-locally
            • Formatted-printing
            • Accessing-printed-output
            • Json-printing
            • Vl-printedlist
          • Kit
          • Mlib
          • Transforms
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • Verilog-printing

    Vl-fmt

    Print format strings with support for Verilog constructs.

    Signature
    (vl-fmt x alist &key (ps 'ps)) → ps
    Arguments
    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 "centaur/vl/util/fmt-base".

    ~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:
    • locations,
    • expressions (and automatically prefers to print "original expressions" rather than "simplified expressions"),
    • ranges,
    • statements,
    • plain or named arguments,
    • contexts,
    • any module element,
    • or even a whole module (for which it only prints the name of the module, perhaps with links).
    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 printed.
    ~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.