		Search-engine friendly clone of the ACL2 documentation.

Vl-expr-selfsize

Vl-expr-opacity

Returns the "opacity" of the expression, a way of categorizing the expression for sizing.

Signature
(vl-expr-opacity x) → opacity
Arguments: x — Guard (vl-expr-p x).
Returns: opacity — Type (vl-opacity-p opacity).

We are sorting expressions into three categories here:

"Transparent" vector expressions, for which one or more immediate subexpressions must have the same size as the outer expression. These include vector-valued binary operations such as +, &, and <<, unary vector-valued operations such as + and ~, and ternary ? : expressions. When such an expression is sized, these subexpressions are extended to the required size, and usually the other immediate subexpressions (if any) are self-sized.
"Opaque" vector expressions, for which the outer expression's size doesn't affect the sizes of its subexpressions. These include constants, variables, indexing operations, function calls, concatenations, binary comparisons and logical operations (e.g. &&), and unary bit-reductions. There may be sizing constraints among the subexpressions, but they don't involve the size of the outer expression.
"Special" expressions, whose type is determined in some other way; e.g., a streaming concatenation or an assignment-pattern can take on a context-determined type.

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) + expression, we extend it by extending its operands. If it is an (opaque) expression, we just zero- or sign-extend it and don't change any of its operands.

Definitions and Theorems

Function: vl-expr-opacity

(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: vl-opacity-p-of-vl-expr-opacity

(defthm vl-opacity-p-of-vl-expr-opacity
  (b* ((opacity (vl-expr-opacity x)))
    (vl-opacity-p opacity))
  :rule-classes :rewrite)

Theorem: vl-expr-opacity-of-vl-expr-fix-x

(defthm vl-expr-opacity-of-vl-expr-fix-x
  (equal (vl-expr-opacity (vl-expr-fix x))
         (vl-expr-opacity x)))

Theorem: vl-expr-opacity-vl-expr-equiv-congruence-on-x

(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)