(vl-gate-make-svex-module type nargs) → (mv err portnames portdirs svmod)
Function:
(defun vl-gate-make-svex-module (type nargs) (declare (xargs :guard (and (vl-gatetype-p type) (natp nargs)))) (let ((__function__ 'vl-gate-make-svex-module)) (declare (ignorable __function__)) (b* (((mv err unimpl assigns portnames portdirs) (vl-gatetype-names/dirs/assigns type nargs)) ((when err) (mv err nil nil nil)) (wires (svex-gateinst-wirelist portnames)) ((when unimpl) (mv (vmsg "Unimplemented gate: ~x0" (vl-gatetype-fix type)) nil nil nil))) (mv nil portnames portdirs (sv::make-module :wires wires :assigns assigns)))))
Theorem:
(defthm return-type-of-vl-gate-make-svex-module.err (b* (((mv ?err ?portnames ?portdirs ?svmod) (vl-gate-make-svex-module type nargs))) (iff (vl-msg-p err) err)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-gate-make-svex-module.portnames (b* (((mv ?err ?portnames ?portdirs ?svmod) (vl-gate-make-svex-module type nargs))) (and (string-listp portnames) (implies (not err) (eql (len portnames) (nfix nargs))))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-gate-make-svex-module.portdirs (b* (((mv ?err ?portnames ?portdirs ?svmod) (vl-gate-make-svex-module type nargs))) (and (vl-directionlist-p portdirs) (implies (not err) (eql (len portdirs) (nfix nargs))))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-gate-make-svex-module.svmod (b* (((mv ?err ?portnames ?portdirs ?svmod) (vl-gate-make-svex-module type nargs))) (implies (not err) (sv::module-p svmod))) :rule-classes :rewrite)
Theorem:
(defthm svarlist-addr-p-of-vl-gate-make-svex-module (b* (((mv ?err ?portnames ?portdirs ?svmod) (vl-gate-make-svex-module type nargs))) (sv::svarlist-addr-p (sv::module-vars svmod))))
Theorem:
(defthm vl-gate-make-svex-module-of-vl-gatetype-fix-type (equal (vl-gate-make-svex-module (vl-gatetype-fix type) nargs) (vl-gate-make-svex-module type nargs)))
Theorem:
(defthm vl-gate-make-svex-module-vl-gatetype-equiv-congruence-on-type (implies (vl-gatetype-equiv type type-equiv) (equal (vl-gate-make-svex-module type nargs) (vl-gate-make-svex-module type-equiv nargs))) :rule-classes :congruence)
Theorem:
(defthm vl-gate-make-svex-module-of-nfix-nargs (equal (vl-gate-make-svex-module type (nfix nargs)) (vl-gate-make-svex-module type nargs)))
Theorem:
(defthm vl-gate-make-svex-module-nat-equiv-congruence-on-nargs (implies (acl2::nat-equiv nargs nargs-equiv) (equal (vl-gate-make-svex-module type nargs) (vl-gate-make-svex-module type nargs-equiv))) :rule-classes :congruence)