Gather a flat list of warnings from a vl-design-p.
(vl-design-flat-warnings x) → warnings
Function:
(defun vl-design-flat-warnings (x) (declare (xargs :guard (vl-design-p x))) (let ((__function__ 'vl-design-flat-warnings)) (declare (ignorable __function__)) (mbe :logic (b* (((vl-design x) x)) (append (vl-modulelist-flat-warnings x.mods) (vl-udplist-flat-warnings x.udps) (vl-interfacelist-flat-warnings x.interfaces) (vl-programlist-flat-warnings x.programs) (vl-classlist-flat-warnings x.classes) (vl-packagelist-flat-warnings x.packages) (vl-configlist-flat-warnings x.configs))) :exec (b* (((vl-design x) x) (acc nil) (acc (vl-modulelist-flat-warnings-exec x.mods acc)) (acc (vl-udplist-flat-warnings-exec x.udps acc)) (acc (vl-interfacelist-flat-warnings-exec x.interfaces acc)) (acc (vl-programlist-flat-warnings-exec x.programs acc)) (acc (vl-classlist-flat-warnings-exec x.classes acc)) (acc (vl-packagelist-flat-warnings-exec x.packages acc)) (acc (vl-configlist-flat-warnings-exec x.configs acc))) (reverse acc)))))
Theorem:
(defthm vl-warninglist-p-of-vl-design-flat-warnings (b* ((warnings (vl-design-flat-warnings x))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-design-flat-warnings-of-vl-design-fix-x (equal (vl-design-flat-warnings (vl-design-fix x)) (vl-design-flat-warnings x)))
Theorem:
(defthm vl-design-flat-warnings-vl-design-equiv-congruence-on-x (implies (vl-design-equiv x x-equiv) (equal (vl-design-flat-warnings x) (vl-design-flat-warnings x-equiv))) :rule-classes :congruence)