• 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
        • Printing-locally
        • Formatted-printing
        • Accessing-printed-output
          • Vl-print-to-file
          • Vl-ps->chars
          • Vl-ps->string
          • With-ps-file
        • Vl-printedlist
        • Json-printing
      • Esim-vl
      • Well-formedness
    • Sv
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Accessing-printed-output

With-ps-file

Convenient wrapper for vl-print-to-file.

The basic idea of this is that you can do, e.g.,

(with-ps-file "my-file.txt"
   (vl-print "Hello,")
   (vl-println "World!"))

And end up with a file called my-file.txt that says Hello, World!. The general form is:

(with-ps-file filename &rest forms)

Basically we just wrap the forms in a vl-ps-seq and then add a call of vl-print-to-file at the end. This is done in a with-local-stobj, so previously printed content isn't included.

This implicitly takes, modifies, and returns state.