		Search-engine friendly clone of the ACL2 documentation.

Genblob

Vl-module->genblob

Convert most of a module into a vl-genblob.

Signature
(vl-module->genblob x) → genblob
Arguments: x — Guard (vl-module-p x).
Returns: genblob — Type (vl-genblob-p genblob).

Certain fields of a vl-module aren't also fields of a vl-genblob, for instance, a genblob doesn't have warnings, a name, location information, etc.

But aside from these fields, most of a module can be extracted and turned into a genblob for easy processing. After processing the blob, the updated fields can be reinstalled into the module using vl-genblob->module.

Definitions and Theorems

Function: vl-module->genblob

(defun vl-module->genblob (x)
  (declare (xargs :guard (vl-module-p x)))
  (let ((__function__ 'vl-module->genblob))
    (declare (ignorable __function__))
    (b* (((vl-module x)))
      (make-vl-genblob :id x.name
                       :scopetype :vl-module
                       :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
                       :finals x.finals
                       :typedefs x.typedefs
                       :imports x.imports
                       :genvars x.genvars
                       :assertions x.assertions
                       :cassertions x.cassertions
                       :properties x.properties
                       :sequences x.sequences
                       :clkdecls x.clkdecls
                       :gclkdecls x.gclkdecls
                       :defaultdisables x.defaultdisables
                       :dpiimports x.dpiimports
                       :dpiexports x.dpiexports
                       :binds x.binds
                       :classes x.classes
                       :covergroups x.covergroups
                       :elabtasks x.elabtasks))))

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

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

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

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

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

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