		Search-engine friendly clone of the ACL2 documentation.

Stmttemps

Vl-assignstmt-stmttemps

Introduce temp wires for right-hand sides.

Signature
(vl-assignstmt-stmttemps x delta elem) → (mv new-x delta)
Arguments: x — 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-assignstmt-stmttemps

(defun vl-assignstmt-stmttemps (x delta elem)
 (declare (xargs :guard (and (vl-stmt-p x)
                             (vl-delta-p delta)
                             (vl-modelement-p elem))))
 (declare (xargs :guard (eq (vl-stmt-kind x) :vl-assignstmt)))
 (let ((__function__ 'vl-assignstmt-stmttemps))
  (declare (ignorable __function__))
  (b*
   (((vl-assignstmt x) x)
    (lw (vl-expr->finalwidth x.lvalue))
    (ltype (vl-expr->finaltype x.lvalue))
    (rw (vl-expr->finalwidth x.expr))
    (rtype (vl-expr->finaltype x.expr))
    ((unless (and (posp lw) ltype))
     (mv
      x
      (dwarn
       :type :vl-stmttemps-fail
       :msg
       "~a0: failing to transform assignment ~a1. ~
                           Expected the lhs to have positive width and ~
                           decided type, but found width ~x2 and type ~x3."
       :args (list elem x lw ltype))))
    ((unless (and (posp rw) rtype))
     (mv
      x
      (dwarn
       :type :vl-stmttemps-fail
       :msg
       "~a0: failing to transform assignment ~a1. ~
                           Expected the rhs to have positive width and ~
                           decided type, but found width ~x2 and type ~x3."
       :args (list elem x rw rtype))))
    ((when (and (eql lw rw)
                (vl-expr-sliceable-p x.expr)))
     (mv x delta))
    (loc (vl-modelement->loc elem))
    ((vl-delta delta) delta)
    ((mv temp-name nf)
     (vl-namefactory-indexed-name "vl_rhs" delta.nf))
    ((mv temp-expr temp-decl)
     (vl-occform-mkwire temp-name lw
                        :loc loc))
    (temp-ass (make-vl-assign :lvalue temp-expr
                              :expr x.expr
                              :loc loc))
    (new-x (change-vl-assignstmt x
                                 :expr temp-expr)))
   (mv new-x
       (change-vl-delta delta
                        :nf nf
                        :vardecls (cons temp-decl delta.vardecls)
                        :assigns (cons temp-ass delta.assigns))))))

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

(defthm vl-stmt-p-of-vl-assignstmt-stmttemps.new-x
  (implies (and (force (vl-stmt-p x))
                (force (vl-delta-p delta))
                (force (vl-modelement-p elem))
                (force (eq (vl-stmt-kind$inline x)
                           ':vl-assignstmt)))
           (b* (((mv ?new-x ?delta)
                 (vl-assignstmt-stmttemps x delta elem)))
             (vl-stmt-p new-x)))
  :rule-classes :rewrite)

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

(defthm vl-delta-p-of-vl-assignstmt-stmttemps.delta
  (implies (and (force (vl-stmt-p x))
                (force (vl-delta-p delta))
                (force (vl-modelement-p elem))
                (force (eq (vl-stmt-kind$inline x)
                           ':vl-assignstmt)))
           (b* (((mv ?new-x ?delta)
                 (vl-assignstmt-stmttemps x delta elem)))
             (vl-delta-p delta)))
  :rule-classes :rewrite)