		Search-engine friendly clone of the ACL2 documentation.

Vl-ifstmt

Vl-condition-merge

Join conditions from nested if expressions.

Signature
(vl-condition-merge outer-cond inner-cond) → ans
Arguments: outer-cond — may be nil to say there is no outer condition.
Guard (or (not outer-cond) (and (vl-expr-p outer-cond) (vl-expr->finaltype outer-cond) (posp (vl-expr->finalwidth outer-cond)))) .; inner-cond — Guard (and (vl-expr-p inner-cond) (vl-expr->finaltype inner-cond) (posp (vl-expr->finalwidth inner-cond))) .
Returns: ans — a one-bit wide expression equivalent to outer-cond && inner-cond.
Type (and (vl-expr-p ans) (equal (vl-expr->finalwidth ans) 1) (equal (vl-expr->finaltype ans) :vl-unsigned)) , given the guard.

For compatibility with oprewrite, we actually build something like (|outer-cond & |inner-cond), except we omit the reduction operators where possible.

Definitions and Theorems

Function: vl-condition-merge

(defun vl-condition-merge (outer-cond inner-cond)
 (declare
  (xargs
      :guard (and (or (not outer-cond)
                      (and (vl-expr-p outer-cond)
                           (vl-expr->finaltype outer-cond)
                           (posp (vl-expr->finalwidth outer-cond))))
                  (and (vl-expr-p inner-cond)
                       (vl-expr->finaltype inner-cond)
                       (posp (vl-expr->finalwidth inner-cond))))))
 (let ((__function__ 'vl-condition-merge))
   (declare (ignorable __function__))
   (if (not outer-cond)
       (vl-condition-fix inner-cond)
     (make-vl-nonatom :op :vl-binary-bitand
                      :args (list (vl-condition-fix outer-cond)
                                  (vl-condition-fix inner-cond))
                      :finalwidth 1
                      :finaltype :vl-unsigned))))

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

(defthm return-type-of-vl-condition-merge
 (implies
  (and
     (force (if (not outer-cond)
                (not outer-cond)
              (if (vl-expr-p outer-cond)
                  (if (vl-expr->finaltype$inline outer-cond)
                      (posp (vl-expr->finalwidth$inline outer-cond))
                    'nil)
                'nil)))
     (force (vl-expr-p inner-cond))
     (force (vl-expr->finaltype$inline inner-cond))
     (force (posp (vl-expr->finalwidth$inline inner-cond))))
  (b* ((ans (vl-condition-merge outer-cond inner-cond)))
    (and (vl-expr-p ans)
         (equal (vl-expr->finalwidth ans) 1)
         (equal (vl-expr->finaltype ans)
                :vl-unsigned))))
 :rule-classes :rewrite)

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

(defthm vl-expr-welltyped-p-of-vl-condition-merge
 (implies
  (and (or (not outer-cond)
           (vl-expr-welltyped-p outer-cond))
       (vl-expr-welltyped-p inner-cond)
       (or (not outer-cond)
           (and (vl-expr-p outer-cond)
                (vl-expr->finaltype outer-cond)
                (posp (vl-expr->finalwidth outer-cond))))
       (and (vl-expr-p inner-cond)
            (vl-expr->finaltype inner-cond)
            (posp (vl-expr->finalwidth inner-cond))))
  (vl-expr-welltyped-p (vl-condition-merge outer-cond inner-cond))))