Get the attributes from any statement.
Function:
(defun vl-stmt->atts (x) (declare (xargs :guard (vl-stmt-p x))) (let ((__function__ 'vl-stmt->atts)) (declare (ignorable __function__)) (vl-stmt-case x :vl-nullstmt x.atts :vl-assignstmt x.atts :vl-deassignstmt x.atts :vl-callstmt x.atts :vl-disablestmt x.atts :vl-eventtriggerstmt x.atts :vl-casestmt x.atts :vl-ifstmt x.atts :vl-foreverstmt x.atts :vl-waitstmt x.atts :vl-whilestmt x.atts :vl-dostmt x.atts :vl-forstmt x.atts :vl-foreachstmt x.atts :vl-blockstmt x.atts :vl-repeatstmt x.atts :vl-timingstmt x.atts :vl-breakstmt x.atts :vl-continuestmt x.atts :vl-returnstmt x.atts :vl-assertstmt x.atts :vl-cassertstmt x.atts)))
Theorem:
(defthm vl-atts-p-of-vl-stmt->atts (b* ((atts (vl-stmt->atts x))) (vl-atts-p atts)) :rule-classes :rewrite)
Theorem:
(defthm vl-stmt->atts-of-vl-stmt-fix-x (equal (vl-stmt->atts (vl-stmt-fix x)) (vl-stmt->atts x)))
Theorem:
(defthm vl-stmt->atts-vl-stmt-equiv-congruence-on-x (implies (vl-stmt-equiv x x-equiv) (equal (vl-stmt->atts x) (vl-stmt->atts x-equiv))) :rule-classes :congruence)