Check an arbitrary vl-fundecl-p for uses of undeclared names.
(vl-fundecl-check-undeclared x st warnings) → new-warnings
Function declarations are tricky because they can have their own declarations and hence we need to treat them basically like a named block statement.
BOZO a problem with our approach is that paramterized function inputs won't exactly work, e.g., for
function foo ; parameter p = 4; input [p-1:0] in; ... endfunction
We will think that
Well, this is a pretty obscure, so I don't want to fix it until it becomes a problem.
Function:
(defun vl-fundecl-check-undeclared (x st warnings) (declare (xargs :guard (and (vl-fundecl-p x) (vl-implicitst-p st) (vl-warninglist-p warnings)))) (let ((__function__ 'vl-fundecl-check-undeclared)) (declare (ignorable __function__)) (b* ((x (vl-fundecl-fix x)) ((vl-fundecl x) x) (other-names (vl-exprlist-varnames (append (vl-portdecllist-allexprs x.portdecls) (vl-datatype-allexprs x.rettype)))) (warnings (vl-warn-about-undeclared-wires x other-names st warnings)) (local-decls (hons-shrink-alist (vl-implicitst->decls st) nil)) (local-imports (hons-shrink-alist (vl-implicitst->imports st) nil)) (local-st (change-vl-implicitst st :decls local-decls :imports local-imports)) ((mv warnings local-st) (vl-blockitemlist-check-undeclared x.blockitems local-st warnings)) (local-decls (vl-implicitst->decls local-st)) (local-decls (make-fal (pairlis$ (vl-portdecllist->names x.portdecls) nil) local-decls)) (local-decls (hons-acons x.name nil local-decls)) (local-st (change-vl-implicitst local-st :decls local-decls)) (warnings (vl-stmt-check-undeclared x x.body local-st warnings))) (fast-alist-free local-decls) warnings)))
Theorem:
(defthm vl-warninglist-p-of-vl-fundecl-check-undeclared (b* ((new-warnings (vl-fundecl-check-undeclared x st warnings))) (vl-warninglist-p new-warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-fundecl-check-undeclared-of-vl-fundecl-fix-x (equal (vl-fundecl-check-undeclared (vl-fundecl-fix x) st warnings) (vl-fundecl-check-undeclared x st warnings)))
Theorem:
(defthm vl-fundecl-check-undeclared-vl-fundecl-equiv-congruence-on-x (implies (vl-fundecl-equiv x x-equiv) (equal (vl-fundecl-check-undeclared x st warnings) (vl-fundecl-check-undeclared x-equiv st warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-fundecl-check-undeclared-of-vl-implicitst-fix-st (equal (vl-fundecl-check-undeclared x (vl-implicitst-fix st) warnings) (vl-fundecl-check-undeclared x st warnings)))
Theorem:
(defthm vl-fundecl-check-undeclared-vl-implicitst-equiv-congruence-on-st (implies (vl-implicitst-equiv st st-equiv) (equal (vl-fundecl-check-undeclared x st warnings) (vl-fundecl-check-undeclared x st-equiv warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-fundecl-check-undeclared-of-vl-warninglist-fix-warnings (equal (vl-fundecl-check-undeclared x st (vl-warninglist-fix warnings)) (vl-fundecl-check-undeclared x st warnings)))
Theorem:
(defthm vl-fundecl-check-undeclared-vl-warninglist-equiv-congruence-on-warnings (implies (vl-warninglist-equiv warnings warnings-equiv) (equal (vl-fundecl-check-undeclared x st warnings) (vl-fundecl-check-undeclared x st warnings-equiv))) :rule-classes :congruence)