Recognizer for svtv-data-obj structures.
(svtv-data-obj-p x) → *
Function:
(defun svtv-data-obj-p (x) (declare (xargs :guard t)) (let ((__function__ 'svtv-data-obj-p)) (declare (ignorable __function__)) (and (true-listp x) (eql (len x) 18) (b* ((design (std::da-nth 0 x)) (user-names (std::da-nth 1 x)) (namemap (std::da-nth 2 x)) (namemap-validp (std::da-nth 3 x)) (flatten (std::da-nth 4 x)) (flatten-validp (std::da-nth 5 x)) (flatnorm-setup (std::da-nth 6 x)) (flatnorm (std::da-nth 7 x)) (flatnorm-validp (std::da-nth 8 x)) (phase-fsm-setup (std::da-nth 9 x)) (phase-fsm (std::da-nth 10 x)) (phase-fsm-validp (std::da-nth 11 x)) (cycle-phases (std::da-nth 12 x)) (cycle-fsm (std::da-nth 13 x)) (cycle-fsm-validp (std::da-nth 14 x)) (pipeline-setup (std::da-nth 15 x)) (pipeline (std::da-nth 16 x)) (pipeline-validp (std::da-nth 17 x))) (and (design-p design) (svtv-namemap-p user-names) (svtv-name-lhs-map-p namemap) (booleanp namemap-validp) (flatten-res-p flatten) (booleanp flatten-validp) (flatnorm-setup-p flatnorm-setup) (flatnorm-res-p flatnorm) (booleanp flatnorm-validp) (phase-fsm-config-p phase-fsm-setup) (fsm-p phase-fsm) (booleanp phase-fsm-validp) (svtv-cyclephaselist-p cycle-phases) (fsm-p cycle-fsm) (booleanp cycle-fsm-validp) (pipeline-setup-p pipeline-setup) (svex-alist-p pipeline) (booleanp pipeline-validp))))))
Theorem:
(defthm consp-when-svtv-data-obj-p (implies (svtv-data-obj-p x) (consp x)) :rule-classes :compound-recognizer)