• 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
        • Vl-model
        • Vl-json
          • Vl-json-opts-p
        • Vl-gather
        • Vl-server
        • Vl-pp
        • Vl-lint
        • Vl-main
        • Vl-toolkit-other-command
        • Vl-help
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Kit

Vl-json

The vl json command.

Signature

(vl-json cmdargs &optional (state 'state)) → state

Arguments

cmdargs — Guard (string-listp cmdargs).

Definitions and Theorems

Function: vl-json-fn

(defun vl-json-fn (cmdargs state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (string-listp cmdargs)))
 (let ((__function__ 'vl-json))
  (declare (ignorable __function__))
  (b*
   (((mv errmsg opts start-files)
     (parse-vl-json-opts cmdargs))
    ((when errmsg)
     (die "~@0~%" errmsg)
     state)
    ((vl-json-opts opts) opts)
    (- (acl2::set-max-mem (* (expt 2 30) opts.mem)))
    ((when opts.help)
     (vl-cw-ps-seq (vl-print *vl-json-help*))
     (exit-ok)
     state)
    ((when opts.readme)
     (vl-cw-ps-seq (vl-print *vl-json-readme*))
     (exit-ok)
     state)
    ((unless (consp start-files))
     (die "No files to process.")
     state)
    (outfile (if (equal opts.outfile "")
                 (cat (car start-files) ".json")
               opts.outfile))
    (- (or (not opts.debug)
           (cw "vl json options: ~x0~%" opts)))
    (state (must-be-regular-files! start-files))
    (state (must-be-directories! opts.search-path))
    (- (cw "Parsing Verilog sources...~%"))
    (loadconfig (make-vl-loadconfig :edition opts.edition
                                    :strictp opts.strict
                                    :start-files start-files
                                    :search-path opts.search-path
                                    :filemapp nil))
    (- (or (not opts.debug)
           (cw "vl load configuration: ~x0~%"
               loadconfig)))
    ((mv (vl-loadresult res) state)
     (cwtime (vl-load loadconfig)))
    (- (cw "JSON-Encoding Modules...~%"))
    (mods (vl-design->mods res.design))
    (state
     (cwtime
      (with-ps-file
           outfile (vl-ps-update-autowrap-col 120)
           (vl-ps-update-autowrap-ind 10)
           (cwtime (if opts.separate (vl-jp-individual-modules mods)
                     (vl-jp-modalist (vl-modalist mods)))
                   :name vl-json-encode))
      :name vl-json-export)))
   (exit-ok)
   state)))

Subtopics

Vl-json-opts-p

Options for running vl json.