		Search-engine friendly clone of the ACL2 documentation.

Propagate

Vl-propagation-fixpoint

Signature
(vl-propagation-fixpoint x n limits) → new-x
Arguments: x — Guard (vl-module-p x).; n — Guard (natp n).; 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-fixpoint

(defun vl-propagation-fixpoint (x n limits)
 (declare (xargs :guard (and (vl-module-p x)
                             (natp n)
                             (propagate-limits-p limits))))
 (let ((__function__ 'vl-propagation-fixpoint))
  (declare (ignorable __function__))
  (b*
   (((when (zp n))
     (cw
      "Note: ran out of steps in vl-propagation-fixpoint for ~s0.~%"
      (vl-module->name x))
     x)
    (new-x (vl-propagation-round x limits))
    ((when (equal new-x x)) x))
   (vl-propagation-fixpoint new-x (- n 1)
                            limits))))

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

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