		Search-engine friendly clone of the ACL2 documentation.

Delayredux

Vl-gateinst-delayredux

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

Definitions and Theorems

Function: vl-gateinst-delayredux-fn

(defun vl-gateinst-delayredux-fn (x delta vecp state-onlyp)
 (declare (xargs :guard (and (vl-gateinst-p x)
                             (vl-delta-p delta))))
 (let ((__function__ 'vl-gateinst-delayredux))
  (declare (ignorable __function__))
  (b*
   (((vl-gateinst 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 gate is too complex; we ~
                           only handle simple delays like #5."
       :args (list x)
       :fatalp t
       :fn 'vl-gateinst-delayredux)))
    (amount (vl-simpledelay->amount x.delay))
    ((when (zp amount))
     (mv (change-vl-gateinst x :delay nil)
         delta))
    ((when (and state-onlyp
                (not (hons-assoc-equal "VL_STATE_DELAY" x.atts))))
     (mv (change-vl-gateinst x :delay nil)
         delta))
    (badarg (vl-first-bad-gatearg-for-delayredux x.args))
    ((when badarg)
     (mv
      x
      (dwarn
       :type :vl-delay-toohard
       :msg
       "~a0: failing to eliminate the delay on this gate ~
                           because argument ~a1 ~s2."
       :args (list x badarg
                   (vl-why-is-gatearg-bad-for-delayredux badarg))
       :fatalp t
       :fn 'vl-gateinst-delayredux)))
    (addmods (vl-make-n-bit-delay-m 1 amount
                                    :vecp vecp))
    (delaymod (car addmods))
    ((mv new-args delta)
     (vl-gatearglist-delayredux delaymod x.args x.loc delta))
    (new-x (change-vl-gateinst x
                               :args new-args
                               :delay nil))
    (delta
         (change-vl-delta
              delta
              :addmods (append addmods (vl-delta->addmods delta)))))
   (mv new-x delta))))

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

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

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

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