Returns the "opacity" of the expression, a way of categorizing the expression for sizing.
(vl-expr-opacity x) → opacity
We are sorting expressions into three categories here:
This distinction is a useful one because this second group are the
expressions that may need to be sign- or zero-extended. E.g., if I have an
expression whose self-size is 4 and I use it in a context where it needs to be
extended to 8 bits, this happens differently depending which group it is in.
For example, if it is a (transparent)
Function:
(defun vl-expr-opacity (x) (declare (xargs :guard (vl-expr-p x))) (let ((__function__ 'vl-expr-opacity)) (declare (ignorable __function__)) (vl-expr-case x :vl-literal :opaque :vl-index :opaque :vl-unary (if (member x.op '(:vl-unary-bitand :vl-unary-nand :vl-unary-bitor :vl-unary-nor :vl-unary-xor :vl-unary-xnor :vl-unary-lognot)) :opaque :transparent) :vl-binary (if (member x.op '(:vl-binary-logand :vl-binary-logor :vl-implies :vl-equiv :vl-binary-eq :vl-binary-neq :vl-binary-ceq :vl-binary-cne :vl-binary-lt :vl-binary-lte :vl-binary-gt :vl-binary-gte :vl-binary-wildeq :vl-binary-wildneq)) :opaque :transparent) :vl-qmark :transparent :vl-concat :opaque :vl-multiconcat :opaque :vl-bitselect-expr :opaque :vl-partselect-expr :opaque :vl-inside :opaque :vl-call :opaque :vl-cast :opaque :vl-pattern :opaque :vl-mintypmax :transparent :vl-special :special :vl-stream :special :vl-tagged :special :vl-eventexpr :special)))
Theorem:
(defthm vl-opacity-p-of-vl-expr-opacity (b* ((opacity (vl-expr-opacity x))) (vl-opacity-p opacity)) :rule-classes :rewrite)
Theorem:
(defthm vl-expr-opacity-of-vl-expr-fix-x (equal (vl-expr-opacity (vl-expr-fix x)) (vl-expr-opacity x)))
Theorem:
(defthm vl-expr-opacity-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-expr-opacity x) (vl-expr-opacity x-equiv))) :rule-classes :congruence)