Main function for checking whether a port declaration, which overlaps with some module item declaration, is a reasonable overlap.
For instance, we might have:
input x; wire x;
Which is fine, or we might have:
input [3:0] x; wire [4:0] x;
Which is definitely not okay. See also portdecl-sign. We expect that after parsing, the types will agree exactly.
Function:
(defun vl-portdecl-and-moduleitem-compatible-p (portdecl item) (declare (xargs :guard (and (vl-portdecl-p portdecl) (vl-moditem-p item)))) (b* (((vl-portdecl portdecl) portdecl) ((unless (eq (tag item) :vl-vardecl)) nil) ((vl-vardecl vardecl) item)) (if (equal portdecl.type vardecl.type) t nil)))
Function:
(defun vl-portdecl-and-moduleitem-compatible-p-warn (portdecl item warnings) (declare (xargs :guard (and (and (vl-portdecl-p portdecl) (vl-moditem-p item)) (vl-warninglist-p warnings))) (ignorable warnings)) (b* (((vl-portdecl portdecl) portdecl) ((unless (eq (tag item) :vl-vardecl)) (if nil (mv t warnings) (mv nil (cons (make-vl-warning :type :vl-weird-port :msg "~a0: port ~s1 is also declared to be a ~s2." :args (list portdecl portdecl.name (tag item))) warnings)))) ((vl-vardecl vardecl) item)) (if (equal portdecl.type vardecl.type) (mv t warnings) (mv nil (cons (make-vl-warning :type :vl-incompatible-port :msg "~a0: the variable declaration for port ~s1 has incompatible type: ~a1 vs. ~a2." :args (list portdecl portdecl.type vardecl.type)) warnings)))))
Theorem:
(defthm eliminate-vl-portdecl-and-moduleitem-compatible-p-warn (equal (mv-nth 0 (vl-portdecl-and-moduleitem-compatible-p-warn portdecl item warnings)) (vl-portdecl-and-moduleitem-compatible-p portdecl item)))
Theorem:
(defthm vl-warninglist-p-of-vl-portdecl-and-moduleitem-compatible-p-warn (implies (force (vl-warninglist-p warnings)) (vl-warninglist-p (mv-nth 1 (vl-portdecl-and-moduleitem-compatible-p-warn portdecl item warnings)))))