		Search-engine friendly clone of the ACL2 documentation.

Qmarksize-check

Vl-qmark-test-size

Determine the "original size" of the test expression for a ?: operator.

Signature
(vl-qmark-test-size x) → *
Arguments: x — Guard (vl-expr-p x).

This is an ugly hack. (vl-qmark-test-size x) is given an exprsesion x which should be the test expression from a conditional expression like:

test ? then : else

Also, x should have already been sized.

Since oprewrite is applied before sizing, x has been transformed and either looks like |A or ~(|A), where A is the original version of x.

We want to return the width of A, rather than the width of x (which is always just 1), so that we can detect cases where the test expression that was given was wider than 1 bit.

To support this, oprewrite is set up so that it annotates the | and ~ expressions it introduces with the VL_CONDITIONAL_FIX attribute. We check for this attribute in order to know where to find A.

Definitions and Theorems

Function: vl-qmark-test-size

(defun vl-qmark-test-size (x)
  (declare (xargs :guard (vl-expr-p x)))
  (let ((__function__ 'vl-qmark-test-size))
    (declare (ignorable __function__))
    (b* (((when (vl-fast-atom-p x))
          (vl-expr->finalwidth x))
         (op (vl-nonatom->op x))
         (args (vl-nonatom->args x))
         ((unless (and (or (eq op :vl-unary-bitnot)
                           (eq op :vl-unary-bitor))
                       (assoc-equal "VL_CONDITIONAL_FIX"
                                    (vl-nonatom->atts x))))
          (vl-expr->finalwidth x))
         (arg1 (first args))
         ((when (eq op :vl-unary-bitor))
          (vl-expr->finalwidth arg1))
         ((unless (and (not (vl-fast-atom-p arg1))
                       (eq (vl-nonatom->op arg1)
                           :vl-unary-bitor)
                       (assoc-equal "VL_CONDITIONAL_FIX"
                                    (vl-nonatom->atts arg1))))
          (raise "Malformed oprewrite conditional fix?  ~x0.~%"
                 x)))
      (vl-expr->finalwidth (first (vl-nonatom->args arg1))))))