(vl-vardecl-reasonable-p x) determines if a vl-vardecl-p is reasonable.
We restrict wire declarations in the following ways:
Function:
(defun vl-vardecl-reasonable-p (x) (declare (xargs :guard (vl-vardecl-p x))) (b* (((vl-vardecl x) x)) (and (if (and (equal (vl-datatype-kind x.type) :vl-coretype) (member (vl-coretype->name x.type) '(:vl-logic :vl-reg)) (member x.nettype '(nil :vl-supply0 :vl-supply1 :vl-wire))) t nil) (if (let ((x.udims (vl-datatype->udims x.type)) (x.pdims (vl-datatype->pdims x.type))) (and (not x.udims) (or (atom x.pdims) (atom (cdr x.pdims))))) t nil) (if (vl-simplevar-p x) t nil))))
Function:
(defun vl-vardecl-reasonable-p-warn (x warnings) (declare (xargs :guard (and (vl-vardecl-p x) (vl-warninglist-p warnings))) (ignorable warnings)) (b* (((vl-vardecl x) x)) (b* (((mv __ok1__ warnings) (if (and (equal (vl-datatype-kind x.type) :vl-coretype) (member (vl-coretype->name x.type) '(:vl-logic :vl-reg)) (member x.nettype '(nil :vl-supply0 :vl-supply1 :vl-wire))) (mv t warnings) (mv nil (cons (make-vl-warning :type :vl-bad-variable :msg "~a0: wire has unsupported type ~a1/nettype ~a2." :args (list x x.type x.nettype)) warnings)))) ((mv __ok2__ warnings) (b* (((mv __ok1__ warnings) (if (let ((x.udims (vl-datatype->udims x.type)) (x.pdims (vl-datatype->pdims x.type))) (and (not x.udims) (or (atom x.pdims) (atom (cdr x.pdims))))) (mv t warnings) (mv nil (cons (make-vl-warning :type :vl-bad-variable :msg "~a0: arrays are not yet supported." :args (list x)) warnings)))) ((mv __ok2__ warnings) (b* (((mv __ok1__ warnings) (if (vl-simplevar-p x) (mv t warnings) (mv nil (cons (make-vl-warning :type :vl-bad-variable :msg "~a0: variable is too complicated." :args (list x)) warnings)))) ((mv __ok2__ warnings) (mv t warnings))) (mv (and __ok1__ __ok2__) warnings)))) (mv (and __ok1__ __ok2__) warnings)))) (mv (and __ok1__ __ok2__) warnings))))
Theorem:
(defthm eliminate-vl-vardecl-reasonable-p-warn (equal (mv-nth 0 (vl-vardecl-reasonable-p-warn x warnings)) (vl-vardecl-reasonable-p x)))
Theorem:
(defthm vl-warninglist-p-of-vl-vardecl-reasonable-p-warn (implies (force (vl-warninglist-p warnings)) (vl-warninglist-p (mv-nth 1 (vl-vardecl-reasonable-p-warn x warnings)))))