• 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
      • Kit
        • Vl-lint
        • Vl-server
        • Vl-gather
        • Vl-zip
        • Vl-main
        • Split-plusargs
        • Vl-shell
        • Vl-json
          • Vl-json-opts-p
          • *vl-json-readme*
          • Vl-json-main
          • Vl-json-top
      • Mlib
      • Transforms
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Vl-json

Vl-json-main

Signature

(vl-json-main opts &key (state 'state)) → state

Arguments

opts — Guard (vl-json-opts-p opts).

Definitions and Theorems

Function: vl-json-main-fn

(defun vl-json-main-fn (opts state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (vl-json-opts-p opts)))
 (declare (xargs :guard (consp (vl-json-opts->start-files opts))))
 (let ((__function__ 'vl-json-main))
  (declare (ignorable __function__))
  (b*
   (((vl-json-opts opts) opts)
    ((mv cmdline-warnings defines)
     (vl-parse-cmdline-defines
          opts.defines
          (make-vl-location :filename "vl cmdline"
                            :line 1
                            :col 0)
          t))
    (- (or (not cmdline-warnings)
           (vl-cw-ps-seq (vl-print-warnings cmdline-warnings))))
    (loadconfig (make-vl-loadconfig :edition opts.edition
                                    :strictp opts.strict
                                    :start-files opts.start-files
                                    :plusargs opts.plusargs
                                    :search-path opts.search-path
                                    :search-exts opts.search-exts
                                    :include-dirs opts.include-dirs
                                    :defines defines
                                    :filemapp t))
    ((mv result state) (vl-load loadconfig))
    ((vl-loadresult result) result)
    (design
     (change-vl-design
        result.design
        :warnings
        (append-without-guard cmdline-warnings
                              (vl-design->warnings result.design))))
    ((mv outfile state)
     (if (equal opts.output "")
         (oslib::basename! (cat (car opts.start-files) ".json"))
       (mv opts.output state)))
    (- (cw "Writing output to file ~x0~%" outfile))
    (state
     (cwtime
         (with-ps-file outfile
                       (vl-ps-seq (vl-ps-update-autowrap-col 120)
                                  (vl-ps-update-autowrap-ind 10)
                                  (cwtime (vl-jp-design design))))))
    (- (cw "Done~%")))
   state)))