		Search-engine friendly clone of the ACL2 documentation.

Vl-ifstmt

Vl-condition-fix

Construct a one-bit wide expression that is equivalent to condition in the context of if (condition) ....

Signature
(vl-condition-fix condition) → rhs
Arguments: condition — Guard (vl-expr-p condition).
Returns: rhs — Type (and (vl-expr-p rhs) (equal (vl-expr->finalwidth rhs) 1) (equal (vl-expr->finaltype rhs) :vl-unsigned)) , given the guard.

This function produces an aesthetically nice expression that is equivalent to condition in the context of an if statement.

When condition is wider than 1 bit, then if (condition) ... is the same as if (|condition) ....

We build |condition only if we have to. That is, if condition is only one bit wide to begin with, then we just return it unchanged.

Definitions and Theorems

Function: vl-condition-fix

(defun vl-condition-fix (condition)
  (declare (xargs :guard (vl-expr-p condition)))
  (declare
       (xargs :guard (and (vl-expr->finaltype condition)
                          (posp (vl-expr->finalwidth condition)))))
  (let ((__function__ 'vl-condition-fix))
    (declare (ignorable __function__))
    (b* ((condition (vl-expr-fix condition))
         ((when (and (eql (vl-expr->finalwidth condition) 1)
                     (eq (vl-expr->finaltype condition)
                         :vl-unsigned)))
          condition))
      (make-vl-nonatom :op :vl-unary-bitor
                       :args (list condition)
                       :finalwidth 1
                       :finaltype :vl-unsigned))))

Theorem: return-type-of-vl-condition-fix

(defthm return-type-of-vl-condition-fix
  (implies
       (and (force (vl-expr-p condition))
            (force (vl-expr->finaltype$inline condition))
            (force (posp (vl-expr->finalwidth$inline condition))))
       (b* ((rhs (vl-condition-fix condition)))
         (and (vl-expr-p rhs)
              (equal (vl-expr->finalwidth rhs) 1)
              (equal (vl-expr->finaltype rhs)
                     :vl-unsigned))))
  :rule-classes :rewrite)

Theorem: vl-expr-welltyped-p-of-vl-condition-fix

(defthm vl-expr-welltyped-p-of-vl-condition-fix
  (implies (and (vl-expr-welltyped-p condition)
                (force (vl-expr->finaltype condition))
                (force (posp (vl-expr->finalwidth condition))))
           (vl-expr-welltyped-p (vl-condition-fix condition))))