• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • ACL2
    • Macro-libraries
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
        • Warnings
        • Primitives
        • Use-set
        • Syntax
        • Getting-started
        • Utilities
        • Loader
        • Transforms
        • Lint
        • Mlib
        • Server
        • Kit
          • Vl-model
            • Vl-model-opts-p
              • Parse-vl-model-opts
              • Vl-model-opts
              • Make-vl-model-opts
              • Honsed-vl-model-opts
                • Change-vl-model-opts
                • *vl-model-opts-usage*
                • Make-honsed-vl-model-opts
                • Vl-model-opts->verilog-file
                • Vl-model-opts->unroll-limit
                • Vl-model-opts->strict
                • Vl-model-opts->start-files
                • Vl-model-opts->search-path
                • Vl-model-opts->search-exts
                • Vl-model-opts->readme
                • Vl-model-opts->outdir
                • Vl-model-opts->mustget
                • Vl-model-opts->mustfail
                • Vl-model-opts->model-file
                • Vl-model-opts->mem
                • Vl-model-opts->include-dirs
                • Vl-model-opts->help
                • Vl-model-opts->esims-file
                • Vl-model-opts->edition
                • Vl-model-opts->dropmods
                • Vl-model-opts->defines
            • Vl-json
            • Vl-gather
            • Vl-server
            • Vl-pp
            • Vl-lint
            • Vl-main
            • Vl-toolkit-other-command
            • Vl-help
          • Printer
          • Esim-vl
          • Well-formedness
        • Sv
        • Fgl
        • Vwsim
        • Vl
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • Vl-model-opts-p

    Honsed-vl-model-opts

    Raw constructor for honsed vl-model-opts-p structures.

    Syntax:

    (honsed-vl-model-opts help readme outdir model-file 
                          esims-file verilog-file start-files 
                          search-path include-dirs search-exts 
                          defines unroll-limit dropmods 
                          edition strict mem mustfail mustget)

    This is identical to vl-model-opts, except that we hons the structure we are creating.

    Definition

    This is an ordinary honsing constructor introduced by defaggregate.

    Function: honsed-vl-model-opts

    (defun honsed-vl-model-opts
           (help readme outdir model-file
                 esims-file verilog-file start-files
                 search-path include-dirs search-exts
                 defines unroll-limit dropmods
                 edition strict mem mustfail mustget)
     (declare (xargs :guard (and (booleanp help)
                                 (booleanp readme)
                                 (stringp outdir)
                                 (stringp model-file)
                                 (stringp esims-file)
                                 (stringp verilog-file)
                                 (string-listp start-files)
                                 (string-listp search-path)
                                 (string-listp include-dirs)
                                 (string-listp search-exts)
                                 (string-listp defines)
                                 (natp unroll-limit)
                                 (string-listp dropmods)
                                 (vl-edition-p edition)
                                 (booleanp strict)
                                 (posp mem)
                                 (string-listp mustfail)
                                 (string-listp mustget))))
     (mbe
      :logic (vl-model-opts help readme outdir model-file
                            esims-file verilog-file start-files
                            search-path include-dirs search-exts
                            defines unroll-limit dropmods
                            edition strict mem mustfail mustget)
      :exec
      (hons
       :vl-model-opts
       (hons
        (hons 'help help)
        (hons
         (hons 'readme readme)
         (hons
          (hons 'outdir outdir)
          (hons
           (hons 'model-file model-file)
           (hons
            (hons 'esims-file esims-file)
            (hons
             (hons 'verilog-file verilog-file)
             (hons
              (hons 'start-files start-files)
              (hons
               (hons 'search-path search-path)
               (hons
                (hons 'include-dirs include-dirs)
                (hons
                 (hons 'search-exts search-exts)
                 (hons
                  (hons 'defines defines)
                  (hons
                   (hons 'unroll-limit unroll-limit)
                   (hons
                    (hons 'dropmods dropmods)
                    (hons
                        (hons 'edition edition)
                        (hons (hons 'strict strict)
                              (hons (hons 'mem mem)
                                    (hons (hons 'mustfail mustfail)
                                          (hons (hons 'mustget mustget)
                                                nil)))))))))))))))))))))