		Search-engine friendly clone of the ACL2 documentation.

Delayredux

Vl-assign-delayredux

Remove the delay from an assignment by introducing an explicit delay module.

Signature
(vl-assign-delayredux x delta &key vecp state-onlyp) → (mv new-x delta)
Arguments: x — Guard (vl-assign-p x).; delta — Guard (vl-delta-p delta).
Returns: new-x — Type (vl-assign-p new-x), given the guard.; delta — Type (vl-delta-p delta), given the guard.

Definitions and Theorems

Function: vl-assign-delayredux-fn

(defun vl-assign-delayredux-fn (x delta vecp state-onlyp)
 (declare (xargs :guard (and (vl-assign-p x)
                             (vl-delta-p delta))))
 (let ((__function__ 'vl-assign-delayredux))
  (declare (ignorable __function__))
  (b*
   (((vl-assign x) x)
    ((unless x.delay) (mv x delta))
    ((unless (vl-simpledelay-p x.delay))
     (mv
      x
      (dwarn
       :type :vl-delay-toohard
       :msg
       "~a0: the delay on this assignment is too complex; ~
                           we only handle plain delays for now."
       :args (list x)
       :fatalp t)))
    (width (vl-expr->finalwidth x.expr))
    ((unless (posp width))
     (mv
      x
      (dwarn
       :type :vl-bad-assign
       :msg
       "~a0: expected widths to be computed and positive, ~
                           but rhs width is ~x1."
       :args (list x width)
       :fatalp t)))
    (delay (vl-simpledelay->amount x.delay))
    ((when (zp delay))
     (mv (change-vl-assign x :delay nil)
         delta))
    ((when (and state-onlyp
                (not (hons-assoc-equal "VL_STATE_DELAY" x.atts))))
     (mv (change-vl-assign x :delay nil)
         delta))
    ((vl-delta delta) delta)
    (addmods (vl-make-n-bit-delay-m width delay
                                    :vecp vecp))
    ((mv temp-name nf)
     (vl-namefactory-indexed-name "vl_del" delta.nf))
    ((mv instname nf)
     (vl-namefactory-indexed-name "vl_mkdel" nf))
    ((mv temp-expr temp-vardecl)
     (vl-occform-mkwire temp-name width
                        :loc x.loc))
    (modinst (vl-simple-instantiate (car addmods)
                                    instname (list temp-expr x.expr)
                                    :loc x.loc))
    (new-x (change-vl-assign x
                             :expr temp-expr
                             :delay nil))
    (delta
     (change-vl-delta
         delta
         :nf nf
         :vardecls (cons temp-vardecl delta.vardecls)
         :modinsts (cons modinst delta.modinsts)
         :addmods (revappend-without-guard addmods delta.addmods))))
   (mv new-x delta))))

Theorem: vl-assign-p-of-vl-assign-delayredux.new-x

(defthm vl-assign-p-of-vl-assign-delayredux.new-x
 (implies (and (force (vl-assign-p x))
               (force (vl-delta-p delta)))
          (b* (((mv ?new-x ?delta)
                (vl-assign-delayredux-fn x delta vecp state-onlyp)))
            (vl-assign-p new-x)))
 :rule-classes :rewrite)

Theorem: vl-delta-p-of-vl-assign-delayredux.delta

(defthm vl-delta-p-of-vl-assign-delayredux.delta
 (implies (and (force (vl-assign-p x))
               (force (vl-delta-p delta)))
          (b* (((mv ?new-x ?delta)
                (vl-assign-delayredux-fn x delta vecp state-onlyp)))
            (vl-delta-p delta)))
 :rule-classes :rewrite)