• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Fgl
    • Vwsim
    • Vl
      • Syntax
      • Loader
      • Warnings
        • Lint-warning-suppression
        • Warning-basics
        • Vl-warning
        • Vl-warninglist-add-ctx
        • Vl-warninglist->types
        • Propagating-errors
          • Vl-design-propagate-errors
            • Vl-design-filter-zombies
          • Vl-blamealist
          • Vl-design-zombies
          • Vl-blame-alist-to-reportcard
          • Vl-blame-alist
          • Vl-blamealist-count
        • Vl-reportcard
        • Vl-some-warning-fatalp
        • Clean-warnings
        • Lint-whole-file-suppression
        • Warn
        • Vl-warninglist
        • Vl-remove-warnings
        • Vl-keep-warnings
        • Flat-warnings
        • Vl-some-warning-of-type-p
        • Vl-msg
        • Vl-warning-add-ctx
        • Vl-print-warning
        • Vmsg-binary-concat
        • Ok
        • Vl-trace-warnings
        • Fatal
        • Vmsg
      • Getting-started
      • Utilities
      • Printer
      • Kit
      • Mlib
      • Transforms
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Vl-design-propagate-errors

Vl-design-filter-zombies

Move modules and other design elements that have fatal warnings from the good design into the bad design.

Signature

(vl-design-filter-zombies good bad suppress-fatals) 
  → 
(mv good-- bad++)

Arguments

good — Guard (vl-design-p good).

bad — Guard (vl-design-p bad).

suppress-fatals — Guard (symbol-listp suppress-fatals).

Returns

good-- — Copy of good except that zombies are removed.
    Type (vl-design-p good--).

bad++ — Extension of bad with zombies from good.
    Type (vl-design-p bad++).

Definitions and Theorems

Function: vl-design-filter-zombies

(defun vl-design-filter-zombies (good bad suppress-fatals)
 (declare (xargs :guard (and (vl-design-p good)
                             (vl-design-p bad)
                             (symbol-listp suppress-fatals))))
 (let ((__function__ 'vl-design-filter-zombies))
  (declare (ignorable __function__))
  (b*
   (((vl-design good))
    ((vl-design bad))
    ((mv bad-mods good-mods)
     (vl-filter-modules
          (vl-modulelist-zombies good.mods suppress-fatals)
          good.mods))
    ((mv bad-interfaces good-interfaces)
     (vl-filter-interfaces
          (vl-interfacelist-zombies good.interfaces suppress-fatals)
          good.interfaces))
    ((mv bad-udps good-udps)
     (vl-filter-udps (vl-udplist-zombies good.udps suppress-fatals)
                     good.udps))
    ((mv bad-programs good-programs)
     (vl-filter-programs
          (vl-programlist-zombies good.programs suppress-fatals)
          good.programs))
    ((mv bad-classes good-classes)
     (vl-filter-classes
          (vl-classlist-zombies good.classes suppress-fatals)
          good.classes))
    ((mv bad-packages good-packages)
     (vl-filter-packages
          (vl-packagelist-zombies good.packages suppress-fatals)
          good.packages))
    ((mv bad-configs good-configs)
     (vl-filter-configs
          (vl-configlist-zombies good.configs suppress-fatals)
          good.configs))
    ((mv bad-typedefs good-typedefs)
     (vl-filter-typedefs
          (vl-typedeflist-zombies good.typedefs suppress-fatals)
          good.typedefs))
    (good (change-vl-design good
                            :mods good-mods
                            :interfaces good-interfaces
                            :udps good-udps
                            :programs good-programs
                            :classes good-classes
                            :packages good-packages
                            :configs good-configs
                            :typedefs good-typedefs))
    (bad (change-vl-design
              bad
              :mods (append bad-mods bad.mods)
              :interfaces (append bad-interfaces bad.interfaces)
              :udps (append bad-udps bad.udps)
              :programs (append bad-programs bad.programs)
              :classes (append bad-classes bad.classes)
              :packages (append bad-packages bad.packages)
              :configs (append bad-configs bad.configs)
              :typedefs (append bad-typedefs bad.typedefs))))
   (mv good bad))))

Theorem: vl-design-p-of-vl-design-filter-zombies.good--

(defthm vl-design-p-of-vl-design-filter-zombies.good--
  (b* (((mv ?good-- ?bad++)
        (vl-design-filter-zombies good bad suppress-fatals)))
    (vl-design-p good--))
  :rule-classes :rewrite)

Theorem: vl-design-p-of-vl-design-filter-zombies.bad++

(defthm vl-design-p-of-vl-design-filter-zombies.bad++
  (b* (((mv ?good-- ?bad++)
        (vl-design-filter-zombies good bad suppress-fatals)))
    (vl-design-p bad++))
  :rule-classes :rewrite)

Theorem: vl-design-filter-zombies-of-vl-design-fix-good

(defthm vl-design-filter-zombies-of-vl-design-fix-good
  (equal (vl-design-filter-zombies (vl-design-fix good)
                                   bad suppress-fatals)
         (vl-design-filter-zombies good bad suppress-fatals)))

Theorem: vl-design-filter-zombies-vl-design-equiv-congruence-on-good

(defthm vl-design-filter-zombies-vl-design-equiv-congruence-on-good
 (implies
  (vl-design-equiv good good-equiv)
  (equal (vl-design-filter-zombies good bad suppress-fatals)
         (vl-design-filter-zombies good-equiv bad suppress-fatals)))
 :rule-classes :congruence)

Theorem: vl-design-filter-zombies-of-vl-design-fix-bad

(defthm vl-design-filter-zombies-of-vl-design-fix-bad
  (equal (vl-design-filter-zombies good (vl-design-fix bad)
                                   suppress-fatals)
         (vl-design-filter-zombies good bad suppress-fatals)))

Theorem: vl-design-filter-zombies-vl-design-equiv-congruence-on-bad

(defthm vl-design-filter-zombies-vl-design-equiv-congruence-on-bad
 (implies
  (vl-design-equiv bad bad-equiv)
  (equal (vl-design-filter-zombies good bad suppress-fatals)
         (vl-design-filter-zombies good bad-equiv suppress-fatals)))
 :rule-classes :congruence)

Theorem: vl-design-filter-zombies-of-symbol-list-fix-suppress-fatals

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

Theorem: vl-design-filter-zombies-symbol-list-equiv-congruence-on-suppress-fatals

(defthm
 vl-design-filter-zombies-symbol-list-equiv-congruence-on-suppress-fatals
 (implies
  (acl2::symbol-list-equiv suppress-fatals suppress-fatals-equiv)
  (equal (vl-design-filter-zombies good bad suppress-fatals)
         (vl-design-filter-zombies good bad suppress-fatals-equiv)))
 :rule-classes :congruence)