Translate a VL module into an svex module, adding any auxiliary modules necessary.
(vl-module->svex-module name elabindex config modalist) → (mv warnings modalist1 new-elabindex)
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.
Function:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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)