		Search-engine friendly clone of the ACL2 documentation.

Propagating-errors

Vl-design-propagate-errors

Top-level function for propagating-errors. We identify any faulty design elements in a good design and move them into a bad design.

Signature
(vl-design-propagate-errors good bad) → (mv good-- bad++)
Arguments: good — The good design, which has presumably just been transformed in some way. This design may have some "zombies" — design elements with fatal warnings. We will remove these zombies and anything that depends on them.
Guard (vl-design-p good).; bad — The bad design which holds any faulty design elements. We will move the zombies into this design.
Guard (vl-design-p bad).
Returns: good-- — Cut down version of the good design, with any faulty elements and their dependents eliminated.
Type (vl-design-p good--).; bad++ — Extended version of the bad design, with any faulty elements from good moved over into it.
Type (vl-design-p bad++).

Definitions and Theorems

Function: vl-design-propagate-errors

(defun vl-design-propagate-errors (good bad)
  (declare (xargs :guard (and (vl-design-p good)
                              (vl-design-p bad))))
  (let ((__function__ 'vl-design-propagate-errors))
    (declare (ignorable __function__))
    (b* ((zombies (vl-design-zombies good))
         ((unless zombies)
          (mv (vl-design-fix good)
              (vl-design-fix bad)))
         (blame-alist (vl-blame-alist zombies good))
         (reportcard (vl-blame-alist-to-reportcard blame-alist nil))
         (good (vl-apply-reportcard good reportcard)))
      (vl-hierarchy-free)
      (vl-design-filter-zombies good bad))))

Theorem: vl-design-p-of-vl-design-propagate-errors.good--

(defthm vl-design-p-of-vl-design-propagate-errors.good--
  (b* (((mv ?good-- ?bad++)
        (vl-design-propagate-errors good bad)))
    (vl-design-p good--))
  :rule-classes :rewrite)

Theorem: vl-design-p-of-vl-design-propagate-errors.bad++

(defthm vl-design-p-of-vl-design-propagate-errors.bad++
  (b* (((mv ?good-- ?bad++)
        (vl-design-propagate-errors good bad)))
    (vl-design-p bad++))
  :rule-classes :rewrite)

Theorem: vl-design-propagate-errors-of-vl-design-fix-good

(defthm vl-design-propagate-errors-of-vl-design-fix-good
  (equal (vl-design-propagate-errors (vl-design-fix good)
                                     bad)
         (vl-design-propagate-errors good bad)))

Theorem: vl-design-propagate-errors-vl-design-equiv-congruence-on-good

(defthm
      vl-design-propagate-errors-vl-design-equiv-congruence-on-good
  (implies (vl-design-equiv good good-equiv)
           (equal (vl-design-propagate-errors good bad)
                  (vl-design-propagate-errors good-equiv bad)))
  :rule-classes :congruence)

Theorem: vl-design-propagate-errors-of-vl-design-fix-bad

(defthm vl-design-propagate-errors-of-vl-design-fix-bad
  (equal (vl-design-propagate-errors good (vl-design-fix bad))
         (vl-design-propagate-errors good bad)))

Theorem: vl-design-propagate-errors-vl-design-equiv-congruence-on-bad

(defthm vl-design-propagate-errors-vl-design-equiv-congruence-on-bad
  (implies (vl-design-equiv bad bad-equiv)
           (equal (vl-design-propagate-errors good bad)
                  (vl-design-propagate-errors good bad-equiv)))
  :rule-classes :congruence)

Subtopics

Vl-design-filter-zombies: Move modules and other design elements that have fatal warnings from the good design into the bad design.