• Top

• Sv::vl-moddb.lisp

Vl-module->svex-module

Translate a VL module into an svex module, adding any auxiliary modules necessary.

Signature

(vl-module->svex-module name elabindex config modalist) 
  → 
(mv warnings modalist1 new-elabindex)

Arguments

name — Guard (stringp name).

elabindex — global scope.

config — Guard (vl-simpconfig-p config).

modalist — Guard (sv::modalist-p modalist).

Returns

warnings — Type (vl-warninglist-p warnings).

modalist1 — Type (and (sv::modalist-p modalist1) (implies (sv::svarlist-addr-p (sv::modalist-vars modalist)) (sv::svarlist-addr-p (sv::modalist-vars modalist1)))) .

Mostly this function just calls vl-genblob->svex-modules to do its work. However, it also needs to take care of the module's interface ports, by calling vl-interfaceports->svex.

Definitions and Theorems

Function: vl-module->svex-module

(defun vl-module->svex-module (name elabindex config modalist)
  (declare (xargs :stobjs (elabindex)))
  (declare (xargs :guard (and (stringp name)
                              (vl-simpconfig-p config)
                              (sv::modalist-p modalist))))
  (let ((__function__ 'vl-module->svex-module))
    (declare (ignorable __function__))
    (b* ((modalist (sv::modalist-fix modalist))
         (name (string-fix name))
         (x (vl-scopestack-find-definition name (vl-elabindex->ss)))
         (warnings nil)
         ((unless (and x (eq (tag x) :vl-module)))
          (mv (warn :type :vl-module->svex-fail
                    :msg "Module not found: ~s0"
                    :args (list name))
              (sv::modalist-fix modalist)
              elabindex))
         ((vl-module x) x)
         (genblob (vl-module->genblob x))
         ((wmv warnings mod modalist ?width elabindex)
          (vl-genblob->svex-modules
               genblob
               elabindex x.name config modalist nil)))
      (mv warnings
          (hons-acons x.name mod modalist)
          elabindex))))

Theorem: vl-warninglist-p-of-vl-module->svex-module.warnings

(defthm vl-warninglist-p-of-vl-module->svex-module.warnings
  (b* (((mv ?warnings ?modalist1 ?new-elabindex)
        (vl-module->svex-module name elabindex config modalist)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-module->svex-module.modalist1

(defthm return-type-of-vl-module->svex-module.modalist1
 (b* (((mv ?warnings ?modalist1 ?new-elabindex)
       (vl-module->svex-module name elabindex config modalist)))
  (and
     (sv::modalist-p modalist1)
     (implies (sv::svarlist-addr-p (sv::modalist-vars modalist))
              (sv::svarlist-addr-p (sv::modalist-vars modalist1)))))
 :rule-classes :rewrite)

Theorem: vl-module->svex-module-of-str-fix-name

(defthm vl-module->svex-module-of-str-fix-name
  (equal (vl-module->svex-module (str-fix name)
                                 elabindex config modalist)
         (vl-module->svex-module name elabindex config modalist)))

Theorem: vl-module->svex-module-streqv-congruence-on-name

(defthm vl-module->svex-module-streqv-congruence-on-name
 (implies
  (streqv name name-equiv)
  (equal
     (vl-module->svex-module name elabindex config modalist)
     (vl-module->svex-module name-equiv elabindex config modalist)))
 :rule-classes :congruence)

Theorem: vl-module->svex-module-of-vl-simpconfig-fix-config

(defthm vl-module->svex-module-of-vl-simpconfig-fix-config
 (equal (vl-module->svex-module name
                                elabindex (vl-simpconfig-fix config)
                                modalist)
        (vl-module->svex-module name elabindex config modalist)))

Theorem: vl-module->svex-module-vl-simpconfig-equiv-congruence-on-config

(defthm
    vl-module->svex-module-vl-simpconfig-equiv-congruence-on-config
 (implies
  (vl-simpconfig-equiv config config-equiv)
  (equal
     (vl-module->svex-module name elabindex config modalist)
     (vl-module->svex-module name elabindex config-equiv modalist)))
 :rule-classes :congruence)

Theorem: vl-module->svex-module-of-modalist-fix-modalist

(defthm vl-module->svex-module-of-modalist-fix-modalist
  (equal (vl-module->svex-module name elabindex
                                 config (sv::modalist-fix modalist))
         (vl-module->svex-module name elabindex config modalist)))

Theorem: vl-module->svex-module-modalist-equiv-congruence-on-modalist

(defthm vl-module->svex-module-modalist-equiv-congruence-on-modalist
 (implies
  (sv::modalist-equiv modalist modalist-equiv)
  (equal
     (vl-module->svex-module name elabindex config modalist)
     (vl-module->svex-module name elabindex config modalist-equiv)))
 :rule-classes :congruence)