• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Debugging
    • Projects
    • 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
            • Vl-println?
            • Vl-printable-p
            • Vl-print
            • Vl-col-after-printing-chars
            • Vl-print-strings-with-commas
            • Vl-col-after-printing-string
            • Vl-string-needs-html-encoding-p
            • Vl-println-markup
            • Vl-print-strings-as-lines
            • Vl-print-url
            • Vl-print-nat
              • Vl-print-natchars-aux
              • Vl-print-nat-main
            • Vl-indent
            • Vl-println
            • Vl-print-markup
            • Vl-ps-seq
            • Vl-cw-ps-seq
            • Vl-when-html
            • Vl-ps-span
          • Verilog-printing
          • Printing-locally
          • Formatted-printing
          • Accessing-printed-output
          • Vl-printedlist
          • Json-printing
        • Esim-vl
        • Well-formedness
      • Sv
      • Fgl
      • Vl
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Testing-utilities
    • Math
  • Basic-printing

Vl-print-nat

(vl-print-nat x) is an optimized version of vl-print for natural numbers.

We make a few optimizations.

  • We identify numeric literals (like 5) at compile time and turn them into strings, so they can be printed at runtime without any coercion.
  • Numbers don't have to be encoded, so there's no need to consider whether we're in HTML mode.
  • We essentially use str::revappend-nat-to-dec-chars instead of calling natstr or similar. This does the minimum amount of consing and doesn't build a string.
  • We manually inline the executable definition of str::revappend-nat-to-dec-chars to avoid doing the loop.

Subtopics

Vl-print-natchars-aux
Optimized base-10 natural number printing into ps.
Vl-print-nat-main