Translate a VL interface definition into an svex module.
(vl-interface->svex-module name elabindex config modalist) → (mv warnings modalist1 elabindex)
We expect an interface to basically only contain variable declarations. We ignore modports. The module generated for an interface is much like that generated for a struct; it has a :self wire that is aliased to the concatenation of all its other declared wires.
Function:
(defun vl-interface->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-interface->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-interface))) (mv (warn :type :vl-interface->svex-fail :msg "Interface not found: ~s0" :args (list name)) (sv::modalist-fix modalist) elabindex)) ((vl-interface x) x) (genblob (vl-interface->genblob x)) ((wmv warnings mod modalist ?width elabindex) (vl-genblob->svex-modules genblob elabindex x.name config modalist t))) (mv warnings (hons-acons (sv::modname-fix name) mod modalist) elabindex))))
Theorem:
(defthm vl-warninglist-p-of-vl-interface->svex-module.warnings (b* (((mv ?warnings ?modalist1 ?elabindex) (vl-interface->svex-module name elabindex config modalist))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-interface->svex-module.modalist1 (b* (((mv ?warnings ?modalist1 ?elabindex) (vl-interface->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-interface->svex-module-of-str-fix-name (equal (vl-interface->svex-module (str-fix name) elabindex config modalist) (vl-interface->svex-module name elabindex config modalist)))
Theorem:
(defthm vl-interface->svex-module-streqv-congruence-on-name (implies (streqv name name-equiv) (equal (vl-interface->svex-module name elabindex config modalist) (vl-interface->svex-module name-equiv elabindex config modalist))) :rule-classes :congruence)
Theorem:
(defthm vl-interface->svex-module-of-vl-simpconfig-fix-config (equal (vl-interface->svex-module name elabindex (vl-simpconfig-fix config) modalist) (vl-interface->svex-module name elabindex config modalist)))
Theorem:
(defthm vl-interface->svex-module-vl-simpconfig-equiv-congruence-on-config (implies (vl-simpconfig-equiv config config-equiv) (equal (vl-interface->svex-module name elabindex config modalist) (vl-interface->svex-module name elabindex config-equiv modalist))) :rule-classes :congruence)
Theorem:
(defthm vl-interface->svex-module-of-modalist-fix-modalist (equal (vl-interface->svex-module name elabindex config (sv::modalist-fix modalist)) (vl-interface->svex-module name elabindex config modalist)))
Theorem:
(defthm vl-interface->svex-module-modalist-equiv-congruence-on-modalist (implies (sv::modalist-equiv modalist modalist-equiv) (equal (vl-interface->svex-module name elabindex config modalist) (vl-interface->svex-module name elabindex config modalist-equiv))) :rule-classes :congruence)