• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
      • Transforms
      • Lint
      • Mlib
        • Scopestack
        • Filtering-by-name
        • Vl-namefactory
        • Substitution
        • Allexprs
        • Hid-tools
        • Vl-consteval
        • Range-tools
        • Lvalexprs
        • Hierarchy
        • Finding-by-name
        • Expr-tools
        • Expr-slicing
        • Stripping-functions
        • Stmt-tools
        • Modnamespace
        • Vl-parse-expr-from-str
        • Welltyped
        • Reordering-by-name
        • Flat-warnings
        • Genblob
          • Vl-genblob
          • Vl-genblob->module
          • Vl-genblob->elems
          • Vl-module->genblob
          • Vl-sort-genelements
        • Expr-building
        • Datatype-tools
        • Syscalls
        • Relocate
        • Expr-cleaning
        • Namemangle
        • Caremask
        • Port-tools
        • Lvalues
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Genblob

Vl-genblob->module

Install fields from a vl-genblob into a module.

Signature

(vl-genblob->module x orig) → new-mod

Arguments

x — Guard (vl-genblob-p x).

orig — Guard (vl-module-p orig).

Returns

new-mod — Type (vl-module-p new-mod).

See vl-module->genblob. This is the companion operation which takes the fields from the genblob and sticks them back into a module.

Certain fields of the module, like its warnings, name, and location information, aren't affected. But the real fields like modinsts, assigns, etc., are overwritten with whatever is in the genblob.

Definitions and Theorems

Function: vl-genblob->module

(defun vl-genblob->module (x orig)
  (declare (xargs :guard (and (vl-genblob-p x)
                              (vl-module-p orig))))
  (let ((__function__ 'vl-genblob->module))
    (declare (ignorable __function__))
    (b* (((vl-genblob x)))
      (change-vl-module orig
                        :generates x.generates
                        :ports x.ports
                        :portdecls x.portdecls
                        :assigns x.assigns
                        :aliases x.aliases
                        :vardecls x.vardecls
                        :paramdecls x.paramdecls
                        :fundecls x.fundecls
                        :taskdecls x.taskdecls
                        :modinsts x.modinsts
                        :gateinsts x.gateinsts
                        :alwayses x.alwayses
                        :initials x.initials
                        :imports x.imports
                        :genvars x.genvars))))

Theorem: vl-module-p-of-vl-genblob->module

(defthm vl-module-p-of-vl-genblob->module
  (b* ((new-mod (vl-genblob->module x orig)))
    (vl-module-p new-mod))
  :rule-classes :rewrite)

Theorem: vl-genblob->module-of-vl-genblob-fix-x

(defthm vl-genblob->module-of-vl-genblob-fix-x
  (equal (vl-genblob->module (vl-genblob-fix x)
                             orig)
         (vl-genblob->module x orig)))

Theorem: vl-genblob->module-vl-genblob-equiv-congruence-on-x

(defthm vl-genblob->module-vl-genblob-equiv-congruence-on-x
  (implies (vl-genblob-equiv x x-equiv)
           (equal (vl-genblob->module x orig)
                  (vl-genblob->module x-equiv orig)))
  :rule-classes :congruence)

Theorem: vl-genblob->module-of-vl-module-fix-orig

(defthm vl-genblob->module-of-vl-module-fix-orig
  (equal (vl-genblob->module x (vl-module-fix orig))
         (vl-genblob->module x orig)))

Theorem: vl-genblob->module-vl-module-equiv-congruence-on-orig

(defthm vl-genblob->module-vl-module-equiv-congruence-on-orig
  (implies (vl-module-equiv orig orig-equiv)
           (equal (vl-genblob->module x orig)
                  (vl-genblob->module x orig-equiv)))
  :rule-classes :congruence)