• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • Macro-libraries
    • ACL2
    • 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

    Vl-model-opts

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

    Syntax:

    (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 the lowest-level constructor for vl-model-opts-p structures. It simply conses together a structure with the specified fields.

    Note: It's generally better to use macros like make-vl-model-opts or change-vl-model-opts instead. These macros lead to more readable and robust code, because you don't have to remember the order of the fields.

    The vl-model-opts-p structures we create here are just constructed with ordinary cons. If you want to create honsed structures, see honsed-vl-model-opts instead.

    Definition

    This is an ordinary constructor function introduced by defaggregate.

    Function: vl-model-opts

    (defun 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))))
     (cons
      :vl-model-opts
      (cons
       (cons 'help help)
       (cons
        (cons 'readme readme)
        (cons
         (cons 'outdir outdir)
         (cons
          (cons 'model-file model-file)
          (cons
           (cons 'esims-file esims-file)
           (cons
            (cons 'verilog-file verilog-file)
            (cons
             (cons 'start-files start-files)
             (cons
              (cons 'search-path search-path)
              (cons
               (cons 'include-dirs include-dirs)
               (cons
                (cons 'search-exts search-exts)
                (cons
                 (cons 'defines defines)
                 (cons
                  (cons 'unroll-limit unroll-limit)
                  (cons
                   (cons 'dropmods dropmods)
                   (cons (cons 'edition edition)
                         (cons (cons 'strict strict)
                               (cons (cons 'mem mem)
                                     (cons (cons 'mustfail mustfail)
                                           (cons (cons 'mustget mustget)
                                                 nil))))))))))))))))))))