		Search-engine friendly clone of the ACL2 documentation.

Stmttemps

Vl-ifstmt-stmttemps

Introduce temp wires for if-statement conditions.

Signature
(vl-ifstmt-stmttemps x delta elem) → (mv new-x delta)
Arguments: x — any statement, but we only rewrite it when it's an if statement; this makes writing vl-stmt-stmttemps very simple.
Guard (vl-stmt-p x).; delta — Guard (vl-delta-p delta).; elem — Guard (vl-modelement-p elem).
Returns: new-x — Type (vl-stmt-p new-x), given the guard.; delta — Type (vl-delta-p delta), given the guard.

Definitions and Theorems

Function: vl-ifstmt-stmttemps

(defun vl-ifstmt-stmttemps (x delta elem)
 (declare (xargs :guard (and (vl-stmt-p x)
                             (vl-delta-p delta)
                             (vl-modelement-p elem))))
 (let ((__function__ 'vl-ifstmt-stmttemps))
  (declare (ignorable __function__))
  (b*
   (((unless (eq (vl-stmt-kind x) :vl-ifstmt))
     (mv x delta))
    ((vl-ifstmt x) x)
    (width (vl-expr->finalwidth x.condition))
    (type (vl-expr->finaltype x.condition))
    ((when (and (eql width 1)
                (vl-fast-atom-p x.condition)
                (vl-expr-sliceable-p x.condition)))
     (mv x delta))
    ((unless (and type (posp width)))
     (mv
      x
      (dwarn
       :type :vl-stmttemps-fail
       :msg
       "~a0: failing to transform if-statement condition ~
                           for ~a1. Expected the condition to have positive ~
                           width and decided type, but found width ~x2 and ~
                           type ~x3."
       :args (list elem x width type))))
    ((unless (vl-expr-welltyped-p x.condition))
     (mv
      x
      (dwarn
       :type :vl-stmttemps-fail
       :msg
       "~a0: failing to transform if-statement condition ~
                           for ~a1.  The condition expression is not well ~
                           typed! Raw expression: ~x2."
       :args (list elem x x.condition)
       :fatalp t)))
    (loc (vl-modelement->loc elem))
    ((vl-delta delta) delta)
    ((mv temp-name nf)
     (vl-namefactory-indexed-name "vl_test" delta.nf))
    ((mv temp-expr temp-decl)
     (vl-occform-mkwire temp-name 1
                        :loc loc))
    (temp-rhs (vl-condition-fix x.condition))
    (temp-assign (make-vl-assign :lvalue temp-expr
                                 :expr temp-rhs
                                 :loc loc)))
   (mv
     (change-vl-ifstmt x
                       :condition temp-expr)
     (change-vl-delta delta
                      :nf nf
                      :assigns (cons temp-assign delta.assigns)
                      :vardecls (cons temp-decl delta.vardecls))))))

Theorem: vl-stmt-p-of-vl-ifstmt-stmttemps.new-x

(defthm vl-stmt-p-of-vl-ifstmt-stmttemps.new-x
  (implies (and (force (vl-stmt-p x))
                (force (vl-delta-p delta))
                (force (vl-modelement-p elem)))
           (b* (((mv ?new-x ?delta)
                 (vl-ifstmt-stmttemps x delta elem)))
             (vl-stmt-p new-x)))
  :rule-classes :rewrite)

Theorem: vl-delta-p-of-vl-ifstmt-stmttemps.delta

(defthm vl-delta-p-of-vl-ifstmt-stmttemps.delta
  (implies (and (force (vl-stmt-p x))
                (force (vl-delta-p delta))
                (force (vl-modelement-p elem)))
           (b* (((mv ?new-x ?delta)
                 (vl-ifstmt-stmttemps x delta elem)))
             (vl-delta-p delta)))
  :rule-classes :rewrite)