Checking whether a port declaration, which overlaps with some module item declaration, is a reasonable overlap.
(vl-check-portdecl-and-moduleitem-compatible portdecl item) → warning
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-check-portdecl-and-moduleitem-compatible (portdecl item) (declare (xargs :guard (and (vl-portdecl-p portdecl) (vl-scopeitem-p item)))) (let ((__function__ 'vl-check-portdecl-and-moduleitem-compatible)) (declare (ignorable __function__)) (b* ((portdecl (vl-portdecl-fix portdecl)) (item (vl-scopeitem-fix item)) ((vl-portdecl portdecl) portdecl) ((unless (eq (tag item) :vl-vardecl)) (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)) :fatalp t :fn __function__)) ((vl-vardecl item)) ((unless (equal portdecl.type item.type)) (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 item.type) :fatalp t :fn __function__)) ((unless (equal portdecl.nettype item.nettype)) (make-vl-warning :type :vl-incompatible-port :msg "~a0: the variable declaration for port ~s1 has ~ incompatible nettype: ~a1 vs. ~a2." :args (list portdecl portdecl.nettype item.nettype) :fatalp t :fn __function__))) nil)))
Theorem:
(defthm return-type-of-vl-check-portdecl-and-moduleitem-compatible (b* ((warning (vl-check-portdecl-and-moduleitem-compatible portdecl item))) (iff (vl-warning-p warning) warning)) :rule-classes :rewrite)
Theorem:
(defthm vl-check-portdecl-and-moduleitem-compatible-of-vl-portdecl-fix-portdecl (equal (vl-check-portdecl-and-moduleitem-compatible (vl-portdecl-fix portdecl) item) (vl-check-portdecl-and-moduleitem-compatible portdecl item)))
Theorem:
(defthm vl-check-portdecl-and-moduleitem-compatible-vl-portdecl-equiv-congruence-on-portdecl (implies (vl-portdecl-equiv portdecl portdecl-equiv) (equal (vl-check-portdecl-and-moduleitem-compatible portdecl item) (vl-check-portdecl-and-moduleitem-compatible portdecl-equiv item))) :rule-classes :congruence)
Theorem:
(defthm vl-check-portdecl-and-moduleitem-compatible-of-vl-scopeitem-fix-item (equal (vl-check-portdecl-and-moduleitem-compatible portdecl (vl-scopeitem-fix item)) (vl-check-portdecl-and-moduleitem-compatible portdecl item)))
Theorem:
(defthm vl-check-portdecl-and-moduleitem-compatible-vl-scopeitem-equiv-congruence-on-item (implies (vl-scopeitem-equiv item item-equiv) (equal (vl-check-portdecl-and-moduleitem-compatible portdecl item) (vl-check-portdecl-and-moduleitem-compatible portdecl item-equiv))) :rule-classes :congruence)