• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
        • Warnings
        • Primitives
        • Use-set
        • Syntax
        • Getting-started
        • Utilities
        • Loader
        • Transforms
        • Lint
        • Mlib
        • Server
        • Kit
        • Printer
          • Ps
          • Basic-printing
          • Verilog-printing
            • Vl-fmt
            • Vl-ppc-module
            • Vl-pp-expr
            • Vl-maybe-escape-identifier
            • Vl-print-ext-wirename
            • Vl-pp-module
            • Vl-print-wirename
            • Vl-print-loc
            • Vl-print-modname
            • Vl-pp-origexpr
            • Vl-pps-module
            • Vl-pps-expr
            • Vl-ppc-modulelist
            • Vl-ppcs-module
            • Vl-ps-update-show-atts
            • Vl-pps-origexpr
            • Vl-pps-modulelist
            • Vl-ppcs-modulelist
            • Vl-cw-obj
            • Vl-ps->show-atts-p
            • Vl-cw
          • Printing-locally
          • Formatted-printing
          • Accessing-printed-output
          • Vl-printedlist
          • Json-printing
        • Esim-vl
        • Well-formedness
      • Sv
      • Fgl
      • Vwsim
      • Vl
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Printer

Verilog-printing

Printing routines for displaying Verilog constructs.

Using the VL printer, we implement pretty-printing routines to display our internal parse-tree representation (see syntax) as Verilog code. These functions produce either plain text or html output, depending upon the htmlp setting in the printer state, ps.

Subtopics

Vl-fmt
Print format strings with support for Verilog constructs.
Vl-ppc-module
Pretty print a module with comments to ps.
Vl-pp-expr
Pretty-printer for expressions.
Vl-maybe-escape-identifier
Add escape characters to an identifier name, if necessary.
Vl-print-ext-wirename
(vl-print-ext-wirename modname wirename &key (ps 'ps)) prints a wire's name.
Vl-pp-module
Pretty-print a module to ps.
Vl-print-wirename
(vl-print-wirename x &key (ps 'ps)) prints a wire's name.
Vl-print-loc
(vl-print-loc x &key (ps 'ps)) prints a vl-location-p.
Vl-print-modname
(vl-print-modname x &key (ps 'ps)) prints a module's name.
Vl-pp-origexpr
Pretty-print the "original," un-transformed version of an expression.
Vl-pps-module
Pretty-print a module to a plain-text string.
Vl-pps-expr
Pretty-print an expression into a string.
Vl-ppc-modulelist
Pretty print a list of modules with comments to ps.
Vl-ppcs-module
Pretty-print a module with comments to a plain-text string.
Vl-ps-update-show-atts
Set whether Verilog-2005 (* key = val *)-style attributes should be displayed.
Vl-pps-origexpr
Pretty-print the "original," un-transformed version of an expression into a string.
Vl-pps-modulelist
Pretty-print a list of modules to a plain-text string.
Vl-ppcs-modulelist
Pretty-print a list of modules with comments to a plain-text string.
Vl-cw-obj
Similar to vl-cw, but the arguments are given as a list instead of as macro arguments.
Vl-ps->show-atts-p
Should Verilog-2005 (* key = val *)-style attributes be shown?
Vl-cw
cw-like function for printing to ps, with support for pretty-printing Verilog constructs as in vl-fmt.