Determines whether this datatype can be bitselected.
(vl-datatype-bitselect-ok x) → okp
The input datatype should not have packed or unpacked dimensions; if it does, then it's definitely OK to index into it (though it's only a bitselect if it's the last packed dimension). The input datatype should have usertypes resolved.
Function:
(defun vl-datatype-bitselect-ok (x) (declare (xargs :guard (vl-datatype-p x))) (declare (xargs :guard (and (not (consp (vl-datatype->pdims x))) (not (consp (vl-datatype->udims x)))))) (let ((__function__ 'vl-datatype-bitselect-ok)) (declare (ignorable __function__)) (vl-datatype-case x (:vl-coretype (b* (((vl-coredatatype-info xinfo) (vl-coretypename->info x.name))) (and xinfo.size (not (eql xinfo.size 1))))) (:vl-struct x.packedp) (:vl-union x.packedp) (:vl-enum nil) (:vl-usertype nil))))
Theorem:
(defthm vl-datatype-bitselect-ok-of-vl-datatype-fix-x (equal (vl-datatype-bitselect-ok (vl-datatype-fix x)) (vl-datatype-bitselect-ok x)))
Theorem:
(defthm vl-datatype-bitselect-ok-vl-datatype-equiv-congruence-on-x (implies (vl-datatype-equiv x x-equiv) (equal (vl-datatype-bitselect-ok x) (vl-datatype-bitselect-ok x-equiv))) :rule-classes :congruence)