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

• Vl-zip

Vl-zip-main

Signature

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

Arguments

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

Definitions and Theorems

Function: vl-zip-main-fn

(defun
 vl-zip-main-fn (opts state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (vl-zip-opts-p opts)))
 (let
  ((__function__ 'vl-zip-main))
  (declare (ignorable __function__))
  (b*
   (((vl-zip-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)
    ((mv date state) (oslib::date))
    ((mv ltime state)
     (oslib::universal-time))
    (design
     (change-vl-design
        result.design
        :warnings
        (append-without-guard cmdline-warnings
                              (vl-design->warnings result.design))))
    (zip (make-vl-zipfile :name opts.name
                          :syntax *vl-current-syntax-version*
                          :date date
                          :ltime ltime
                          :design design
                          :filemap result.filemap
                          :defines result.defines))
    (- (cw "Writing output file ~x0~%"
           opts.output))
    (state (cwtime (vl-write-zip opts.output zip)))
    (- (cw "All done.")))
   state)))