		Search-engine friendly clone of the ACL2 documentation.

Propagate

Vl-propagation-round

One single round of propagation.

Signature
(vl-propagation-round x limits) → new-x
Arguments: x — Guard (vl-module-p x).; limits — Guard (propagate-limits-p limits).
Returns: new-x — Type (vl-module-p new-x), given (force (vl-module-p x)).

Definitions and Theorems

Function: vl-propagation-round

(defun vl-propagation-round (x limits)
  (declare (xargs :guard (and (vl-module-p x)
                              (propagate-limits-p limits))))
  (let ((__function__ 'vl-propagation-round))
    (declare (ignorable __function__))
    (b* ((- (cw "Starting propagation round for ~s0~%"
                (vl-module->name x)))
         (sigma (propagation-sigma x limits))
         ((unless sigma) x)
         ((with-fast sigma))
         (propagate-names (alist-keys sigma))
         (temp-assigns (remove-simple-assigns-to
                            propagate-names (vl-module->assigns x)))
         (temp-mod (change-vl-module x
                                     :assigns temp-assigns)))
      (vl-module-subst temp-mod sigma))))

Theorem: vl-module-p-of-vl-propagation-round

(defthm vl-module-p-of-vl-propagation-round
  (implies (force (vl-module-p x))
           (b* ((new-x (vl-propagation-round x limits)))
             (vl-module-p new-x)))
  :rule-classes :rewrite)