Recognizer for vl-portinfo structures.
(vl-portinfo-p x) → *
Function:
(defun vl-portinfo-p (x) (declare (xargs :guard t)) (let ((__function__ 'vl-portinfo-p)) (declare (ignorable __function__)) (and (consp x) (cond ((or (atom x) (eq (car x) :bad)) (and (eq (cdr x) nil) (b* nil t))) (t (and (eq (car x) :regular) (and (std::prod-consp (cdr x)) (std::prod-consp (std::prod-car (cdr x))) (std::prod-consp (std::prod-car (std::prod-car (cdr x)))) (std::prod-consp (std::prod-cdr (std::prod-car (cdr x)))) (std::prod-consp (std::prod-cdr (cdr x))) (std::prod-consp (std::prod-car (std::prod-cdr (cdr x)))) (std::prod-consp (std::prod-cdr (std::prod-cdr (cdr x))))) (b* ((portname (std::prod-car (std::prod-car (std::prod-car (cdr x))))) (port-dir (std::prod-cdr (std::prod-car (std::prod-car (cdr x))))) (conn-expr (std::prod-car (std::prod-cdr (std::prod-car (cdr x))))) (port-lhs (std::prod-cdr (std::prod-cdr (std::prod-car (cdr x))))) (conn-svex (std::prod-car (std::prod-car (std::prod-cdr (cdr x))))) (port-size (std::prod-cdr (std::prod-car (std::prod-cdr (cdr x))))) (?replicatedp (std::prod-car (std::prod-cdr (std::prod-cdr (cdr x))))) (interfacep (std::prod-cdr (std::prod-cdr (std::prod-cdr (cdr x)))))) (and (stringp portname) (vl-maybe-direction-p port-dir) (vl-maybe-expr-p conn-expr) (sv::lhs-p port-lhs) (sv::svex-p conn-svex) (posp port-size) (booleanp interfacep)))))))))
Theorem:
(defthm consp-when-vl-portinfo-p (implies (vl-portinfo-p x) (consp x)) :rule-classes :compound-recognizer)