		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 suppress-fatals) → (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).; suppress-fatals — List of warning types that we should never treat as fatal.
Guard (symbol-listp suppress-fatals).
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 suppress-fatals)
  (declare (xargs :guard (and (vl-design-p good)
                              (vl-design-p bad)
                              (symbol-listp suppress-fatals))))
  (let ((__function__ 'vl-design-propagate-errors))
    (declare (ignorable __function__))
    (b* ((zombies (vl-design-zombies good suppress-fatals))
         ((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 suppress-fatals))))

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 suppress-fatals)))
    (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 suppress-fatals)))
    (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 suppress-fatals)
         (vl-design-propagate-errors good bad suppress-fatals)))

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 suppress-fatals)
       (vl-design-propagate-errors good-equiv bad suppress-fatals)))
 :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)
                                     suppress-fatals)
         (vl-design-propagate-errors good bad suppress-fatals)))

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 suppress-fatals)
       (vl-design-propagate-errors good bad-equiv suppress-fatals)))
 :rule-classes :congruence)

Theorem: vl-design-propagate-errors-of-symbol-list-fix-suppress-fatals

(defthm
      vl-design-propagate-errors-of-symbol-list-fix-suppress-fatals
  (equal (vl-design-propagate-errors
              good bad
              (acl2::symbol-list-fix suppress-fatals))
         (vl-design-propagate-errors good bad suppress-fatals)))

Theorem: vl-design-propagate-errors-symbol-list-equiv-congruence-on-suppress-fatals

(defthm
 vl-design-propagate-errors-symbol-list-equiv-congruence-on-suppress-fatals
 (implies
  (acl2::symbol-list-equiv suppress-fatals suppress-fatals-equiv)
  (equal
       (vl-design-propagate-errors good bad suppress-fatals)
       (vl-design-propagate-errors good bad suppress-fatals-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.