		Search-engine friendly clone of the ACL2 documentation.

Vl-loadconfig

Make-vl-loadconfig

Basic constructor macro for vl-loadconfig structures.

Syntax

(make-vl-loadconfig [:edition <edition>] 
                    [:strictp <strictp>] 
                    [:start-files <start-files>] 
                    [:start-names <start-names>] 
                    [:search-path <search-path>] 
                    [:search-exts <search-exts>] 
                    [:include-dirs <include-dirs>] 
                    [:defines <defines>] 
                    [:plusargs <plusargs>] 
                    [:filemapp <filemapp>] 
                    [:debugp <debugp>] 
                    [:flush-tries <flush-tries>] 
                    [:mintime <mintime>])

This is the usual way to construct vl-loadconfig structures. It simply conses together a structure with the specified fields.

This macro generates a new vl-loadconfig structure from scratch. See also change-vl-loadconfig, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-vl-loadconfig

(defmacro make-vl-loadconfig (&rest args)
  (std::make-aggregate 'vl-loadconfig
                       args
                       '((:edition . :system-verilog-2012)
                         (:strictp)
                         (:start-files)
                         (:start-names)
                         (:search-path)
                         (:search-exts quote ("v"))
                         (:include-dirs)
                         (:defines)
                         (:plusargs)
                         (:filemapp . t)
                         (:debugp)
                         (:flush-tries . 10000)
                         (:mintime . 1))
                       'make-vl-loadconfig
                       nil))

Function: vl-loadconfig

(defun vl-loadconfig (edition strictp start-files
                              start-names search-path search-exts
                              include-dirs defines plusargs
                              filemapp debugp flush-tries mintime)
  (declare (xargs :guard (and (vl-edition-p edition)
                              (booleanp strictp)
                              (string-listp start-files)
                              (string-listp start-names)
                              (string-listp search-path)
                              (string-listp search-exts)
                              (string-listp include-dirs)
                              (vl-defines-p defines)
                              (string-listp plusargs)
                              (booleanp filemapp)
                              (booleanp debugp)
                              (posp flush-tries)
                              (mintime-p mintime))))
  (declare (xargs :guard t))
  (let ((__function__ 'vl-loadconfig))
    (declare (ignorable __function__))
    (b* ((edition (mbe :logic (vl-edition-fix edition)
                       :exec edition))
         (strictp (mbe :logic (acl2::bool-fix strictp)
                       :exec strictp))
         (start-files (mbe :logic (string-list-fix start-files)
                           :exec start-files))
         (start-names (mbe :logic (string-list-fix start-names)
                           :exec start-names))
         (search-path (mbe :logic (string-list-fix search-path)
                           :exec search-path))
         (search-exts (mbe :logic (string-list-fix search-exts)
                           :exec search-exts))
         (include-dirs (mbe :logic (string-list-fix include-dirs)
                            :exec include-dirs))
         (defines (mbe :logic (vl-defines-fix defines)
                       :exec defines)
)
         (plusargs (mbe :logic (string-list-fix plusargs)
                        :exec plusargs))
         (filemapp (mbe :logic (acl2::bool-fix filemapp)
                        :exec filemapp))
         (debugp (mbe :logic (acl2::bool-fix debugp)
                      :exec debugp))
         (flush-tries (mbe :logic (pos-fix flush-tries)
                           :exec flush-tries))
         (mintime (mbe :logic (mintime-fix mintime)
                       :exec mintime)))
      (cons :vl-loadconfig (list (cons 'edition edition)
                                 (cons 'strictp strictp)
                                 (cons 'start-files start-files)
                                 (cons 'start-names start-names)
                                 (cons 'search-path search-path)
                                 (cons 'search-exts search-exts)
                                 (cons 'include-dirs include-dirs)
                                 (cons 'defines defines)
                                 (cons 'plusargs plusargs)
                                 (cons 'filemapp filemapp)
                                 (cons 'debugp debugp)
                                 (cons 'flush-tries flush-tries)
                                 (cons 'mintime mintime))))))