Check to see whether a datatype is packed.
(vl-datatype->packedp x) → *
Doesn't do deep consistency checking to say whether the datatype really can be considered packed -- just that it doesn't have unpacked dims, and it's of a bit-stream coretype or a packed struct/union type. Ignoring enums for the moment.
Function:
(defun vl-datatype->packedp (x) (declare (xargs :guard (vl-datatype-p x))) (let ((__function__ 'vl-datatype->packedp)) (declare (ignorable __function__)) (b* (((when (consp (vl-datatype->udims x))) nil)) (vl-datatype-case x :vl-coretype (and (member x.name '(:vl-logic :vl-reg :vl-bit :vl-byte :vl-shortint :vl-int :vl-longint :vl-integer :vl-time)) t) :vl-struct x.packedp :vl-union x.packedp :vl-enum t :otherwise nil))))
Theorem:
(defthm vl-datatype->packedp-of-vl-datatype-fix-x (equal (vl-datatype->packedp (vl-datatype-fix x)) (vl-datatype->packedp x)))
Theorem:
(defthm vl-datatype->packedp-vl-datatype-equiv-congruence-on-x (implies (vl-datatype-equiv x x-equiv) (equal (vl-datatype->packedp x) (vl-datatype->packedp x-equiv))) :rule-classes :congruence)