		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.