• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Fgl
    • Vl
      • Syntax
      • Loader
      • Warnings
      • Getting-started
      • Utilities
      • Printer
      • Kit
        • Vl-lint
        • Vl-server
        • Vl-gather
          • Vl-gather-opts-p
          • Vl-modulelist-original-sources
          • Vl-module-original-source
          • Vl-gather-top
          • *vl-gather-help*
          • Vl-gather-main
          • Vl-design-original-source
        • Vl-zip
        • Vl-main
        • Split-plusargs
        • Vl-shell
        • Vl-json
      • Mlib
      • Transforms
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Testing-utilities
  • Math

• Vl-gather

Vl-gather-top

Top-level vl gather command.

Signature

(vl-gather-top argv &key (state 'state)) → state

Arguments

argv — Guard (string-listp argv).

Definitions and Theorems

Function: vl-gather-top-fn

(defun
   vl-gather-top-fn (argv state)
   (declare (xargs :stobjs (state)))
   (declare (xargs :guard (string-listp argv)))
   (let ((__function__ 'vl-gather-top))
        (declare (ignorable __function__))
        (b* (((mv errmsg opts start-files-and-plusargs)
              (parse-vl-gather-opts argv))
             ((when errmsg)
              (die "~@0~%" errmsg)
              state)
             ((mv start-files plusargs)
              (split-plusargs start-files-and-plusargs))
             (opts (change-vl-gather-opts opts
                                          :plusargs plusargs
                                          :start-files start-files))
             ((vl-gather-opts opts) opts)
             ((when opts.help)
              (vl-cw-ps-seq (vl-print *vl-gather-help*))
              (exit-ok)
              state)
             ((when opts.readme)
              (vl-cw-ps-seq (vl-print *vl-gather-readme*))
              (exit-ok)
              state)
             ((unless (consp opts.start-files))
              (die "No files to process.")
              state)
             (- (cw "VL Gather Configuration:~%"))
             (- (cw " - start files: ~x0~%"
                    opts.start-files))
             (state (must-be-regular-files! opts.start-files))
             (- (cw " - search path: ~x0~%"
                    opts.search-path))
             (state (must-be-directories! opts.search-path))
             (- (cw " - include directories: ~x0~%"
                    opts.include-dirs))
             (state (must-be-directories! opts.include-dirs))
             (- (and opts.defines
                     (cw "; defines: ~x0~%" opts.defines)))
             (- (cw " - output file: ~x0~%" opts.output))
             (- (cw "; Soft heap size ceiling: ~x0 GB~%"
                    opts.mem))
             (- (set-max-mem (* (expt 2 30) opts.mem)))
             (state (vl-gather-main opts)))
            (exit-ok)
            state)))