• Top
  • Documentation
  • Books
  • 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
          • Vl-loadstate-fix
          • Vl-loadstate-p
          • Make-vl-loadstate
          • Vl-loadstate-equiv
          • Change-vl-loadstate
          • Vl-loadstate->reportcard
          • Vl-loadstate->descalist
          • Vl-loadstate->pstate
          • Vl-loadstate->filemap
          • Vl-loadstate->descs
          • Vl-loadstate->defines
          • Vl-loadstate->config
        • 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-find-file
        • Vl-read-files
        • 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
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Vl-loadstate

Make-vl-loadstate

Basic constructor macro for vl-loadstate structures.

Syntax

(make-vl-loadstate [:config <config>] 
                   [:descs <descs>] 
                   [:descalist <descalist>] 
                   [:defines <defines>] 
                   [:reportcard <reportcard>] 
                   [:pstate <pstate>] 
                   [:filemap <filemap>]) 

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-vl-loadstate

(defmacro make-vl-loadstate (&rest args)
  (std::make-aggregate 'vl-loadstate
                       args
                       '((:config)
                         (:descs)
                         (:descalist)
                         (:defines)
                         (:reportcard)
                         (:pstate)
                         (:filemap))
                       'make-vl-loadstate
                       nil))

Function: vl-loadstate

(defun vl-loadstate (config descs descalist
                            defines reportcard pstate filemap)
 (declare (xargs :guard (and (vl-loadconfig-p config)
                             (vl-descriptionlist-p descs)
                             (vl-defines-p defines)
                             (vl-reportcard-p reportcard)
                             (vl-parsestate-p pstate)
                             (vl-filemap-p filemap))))
 (declare
      (xargs :guard (equal descalist (vl-make-descalist descs))))
 (let ((__function__ 'vl-loadstate))
  (declare (ignorable __function__))
  (b* ((config (mbe :logic (vl-loadconfig-fix config)
                    :exec config))
       (descs (mbe :logic (vl-descriptionlist-fix descs)
                   :exec descs))
       (defines (mbe :logic (vl-defines-fix defines)
                     :exec defines)
)
       (reportcard (mbe :logic (vl-reportcard-fix reportcard)
                        :exec reportcard))
       (pstate (mbe :logic (vl-parsestate-fix pstate)
                    :exec pstate))
       (filemap (mbe :logic (vl-filemap-fix filemap)
                     :exec filemap)))
   (let ((descalist (mbe :logic (vl-make-descalist descs)
                         :exec descalist)))
    (cons
       :vl-loadstate
       (std::prod-cons
            (std::prod-cons config (std::prod-cons descs descalist))
            (std::prod-cons (std::prod-cons defines reportcard)
                            (std::prod-cons pstate filemap))))))))