• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • 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
          • Preprocessor
          • Vl-loadconfig
          • Lexer
          • Vl-loadstate
          • Parser
          • Vl-load-merge-descriptions
          • Scope-of-defines
          • Vl-load-file
          • Vl-flush-out-descriptions
          • Vl-description
          • Vl-loadresult
          • Vl-read-file
          • Vl-find-basename/extension
          • Vl-read-files
          • Vl-find-file
          • Extended-characters
          • Vl-load
          • Vl-load-main
            • Vl-load-description
            • Vl-descriptions-left-to-load
            • Inject-warnings
            • Vl-load-descriptions
            • Vl-load-files
            • Vl-load-summary
            • Vl-collect-modules-from-descriptions
            • Vl-descriptionlist
          • Transforms
          • Lint
          • Mlib
          • Server
          • Kit
          • Printer
          • Esim-vl
          • Well-formedness
        • Sv
        • Vwsim
        • Fgl
        • Vl
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Testing-utilities
      • Math
    • Loader

    Vl-load-main

    Top level interface for loading Verilog sources.

    Signature
    (vl-load-main config state) → (mv result state)
    Arguments
    config — Guard (vl-loadconfig-p config).
    Returns
    result — Type (vl-loadresult-p result).
    state — Type (state-p1 state), given (force (state-p1 state)).

    Definitions and Theorems

    Function: vl-load-main

    (defun
     vl-load-main (config state)
     (declare (xargs :stobjs (state)))
     (declare (xargs :guard (vl-loadconfig-p config)))
     (let
      ((__function__ 'vl-load-main))
      (declare (ignorable __function__))
      (b*
       ((config
         (change-vl-loadconfig
             config
             :include-dirs (cons "."
                                 (vl-loadconfig->include-dirs config))))
        ((vl-loadconfig config) config)
        (pstate (make-vl-parsestate :warnings nil
                                    :usertypes nil))
        (st (make-vl-loadstate :config config
                               :descs nil
                               :descalist nil
                               :defines config.defines
                               :reportcard nil
                               :pstate pstate
                               :filemap nil))
        ((mv st state)
         (time$ (vl-load-files config.start-files st state)
                :msg "; load start-files: ~st sec, ~sa bytes~%"
                :mintime config.mintime))
        ((mv st state)
         (time$ (vl-flush-out-descriptions st config.flush-tries state)
                :msg "; load missing modules: ~st sec, ~sa bytes~%"
                :mintime config.mintime))
        ((vl-loadstate st) st)
        (design (vl-design-from-descriptions st.descs))
        (design (vl-apply-reportcard design st.reportcard))
        (design
          (change-vl-design
               design
               :warnings
               (append-without-guard (vl-parsestate->warnings st.pstate)
                                     (vl-design->warnings design))))
        (result (make-vl-loadresult :design design
                                    :filemap st.filemap
                                    :defines st.defines)))
       (vl-parsestate-free st.pstate)
       (fast-alist-free st.descalist)
       (mv result state))))

    Theorem: vl-loadresult-p-of-vl-load-main.result

    (defthm vl-loadresult-p-of-vl-load-main.result
            (b* (((mv ?result acl2::?state)
                  (vl-load-main config state)))
                (vl-loadresult-p result))
            :rule-classes :rewrite)

    Theorem: state-p1-of-vl-load-main.state

    (defthm state-p1-of-vl-load-main.state
            (implies (force (state-p1 state))
                     (b* (((mv ?result acl2::?state)
                           (vl-load-main config state)))
                         (state-p1 state)))
            :rule-classes :rewrite)