		Search-engine friendly clone of the ACL2 documentation.

Vl-ifstmt

Vl-condition-neg

Construct a one-bit wide expression that is equivalent to !condition.

Signature
(vl-condition-neg condition) → rhs
Arguments: condition — Guard (and (vl-expr-p condition) (posp (vl-expr->finalwidth condition)) (vl-expr->finaltype 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.

We produce an expression that is equivalent to !condition.

For compatibility with oprewrite, the expression we actually generate is:

~(|condition), if condition is more than 1 bit wide, or
~condition when condition is exactly 1 bit wide.

Definitions and Theorems

Function: vl-condition-neg

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

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

(defthm return-type-of-vl-condition-neg
 (implies (and (force (vl-expr-p condition))
               (force (posp (vl-expr->finalwidth$inline condition)))
               (force (vl-expr->finaltype$inline condition)))
          (b* ((rhs (vl-condition-neg 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-neg

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