Memoized core.
(vl-scope-portdecl-alist-aux scope) → alist
Function:
(defun vl-scope-portdecl-alist-aux (scope) (declare (xargs :guard (vl-scope-p scope))) (let ((__function__ 'vl-scope-portdecl-alist-aux)) (declare (ignorable __function__)) (b* ((scope (vl-scope-fix scope))) (case (tag scope) (:vl-interface (b* (((vl-interface scope :quietp t))) (make-fast-alist (vl-interface-scope-portdecl-alist scope nil)))) (:vl-module (b* (((vl-module scope :quietp t))) (make-fast-alist (vl-module-scope-portdecl-alist scope nil)))) (:vl-genblob (b* (((vl-genblob scope :quietp t))) (make-fast-alist (vl-genblob-scope-portdecl-alist scope nil)))) (otherwise nil)))))
Theorem:
(defthm vl-portdecl-alist-p-of-vl-scope-portdecl-alist-aux (b* ((alist (vl-scope-portdecl-alist-aux scope))) (vl-portdecl-alist-p alist)) :rule-classes :rewrite)
Theorem:
(defthm vl-scope-portdecl-alist-aux-correct (implies (stringp name) (equal (cdr (hons-assoc-equal name (vl-scope-portdecl-alist-aux scope))) (vl-scope-find-portdecl name scope))))
Theorem:
(defthm vl-scope-portdecl-alist-aux-of-vl-scope-fix-scope (equal (vl-scope-portdecl-alist-aux (vl-scope-fix scope)) (vl-scope-portdecl-alist-aux scope)))
Theorem:
(defthm vl-scope-portdecl-alist-aux-vl-scope-equiv-congruence-on-scope (implies (vl-scope-equiv scope scope-equiv) (equal (vl-scope-portdecl-alist-aux scope) (vl-scope-portdecl-alist-aux scope-equiv))) :rule-classes :congruence)