• 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
      • Getting-started
      • Utilities
      • Printer
      • Kit
      • Mlib
        • Scopestack
        • Hid-tools
        • Filtering-by-name
        • Vl-interface-mocktype
        • Stripping-functions
        • Genblob
        • Expr-tools
        • Extract-vl-types
        • Hierarchy
          • Vl-design-toplevel
          • Vl-remove-unnecessary-elements
          • Vl-necessary-elements-transitive
          • Vl-interfacelist-everinstanced
          • Vl-dependent-elements-transitive
          • Vl-necessary-elements-direct
          • Vl-modulelist-everinstanced
          • Vl-dependent-elements-direct
          • Vl-design-deporder-modules
          • Vl-design-check-complete
          • Vl-design-upgraph
          • Immdeps
          • Vl-design-downgraph
          • Vl-collect-dependencies
          • Vl-hierarchy-free
        • Range-tools
        • Finding-by-name
        • Stmt-tools
        • Modnamespace
        • Flat-warnings
        • Reordering-by-name
        • Datatype-tools
        • Syscalls
        • Allexprs
        • Lvalues
        • Port-tools
      • Transforms
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Hierarchy

Vl-remove-unnecessary-elements

Throws away whatever part of the design is not necessary for particular design elements.

Signature

(vl-remove-unnecessary-elements keep design) → trimmed-design

Arguments

keep — Names of top level design elements (modules, interfaces, etc.) that you want to keep.
    Guard (string-listp keep).

design — The design to filter.
    Guard (vl-design-p design).

Returns

trimmed-design — Type (vl-design-p trimmed-design).

Definitions and Theorems

Function: vl-remove-unnecessary-elements

(defun vl-remove-unnecessary-elements (keep design)
 (declare (xargs :guard (and (string-listp keep)
                             (vl-design-p design))))
 (let ((__function__ 'vl-remove-unnecessary-elements))
  (declare (ignorable __function__))
  (b*
   ((necessary (vl-necessary-elements-transitive keep design))
    (fal (make-lookup-alist necessary))
    ((vl-design design))
    (mods
        (with-local-nrev
             (vl-fast-keep-modules necessary fal design.mods nrev)))
    (udps (with-local-nrev
               (vl-fast-keep-udps necessary fal design.udps nrev)))
    (interfaces
       (with-local-nrev (vl-fast-keep-interfaces
                             necessary fal design.interfaces nrev)))
    (programs
     (with-local-nrev
        (vl-fast-keep-programs necessary fal design.programs nrev)))
    (packages
     (with-local-nrev
        (vl-fast-keep-packages necessary fal design.packages nrev)))
    (configs
     (with-local-nrev
          (vl-fast-keep-configs necessary fal design.configs nrev)))
    (vardecls
     (with-local-nrev
        (vl-fast-keep-vardecls necessary fal design.vardecls nrev)))
    (taskdecls
     (with-local-nrev
      (vl-fast-keep-taskdecls necessary fal design.taskdecls nrev)))
    (fundecls
     (with-local-nrev
        (vl-fast-keep-fundecls necessary fal design.fundecls nrev)))
    (paramdecls
       (with-local-nrev (vl-fast-keep-paramdecls
                             necessary fal design.paramdecls nrev)))
    (typedefs
     (with-local-nrev
        (vl-fast-keep-typedefs necessary fal design.typedefs nrev)))
    (imports
         (with-local-nrev (vl-fast-keep-imports-by-package
                               necessary fal design.imports nrev)))
    (- (fast-alist-free fal)))
   (change-vl-design design
                     :mods mods
                     :udps udps
                     :interfaces interfaces
                     :programs programs
                     :packages packages
                     :configs configs
                     :vardecls vardecls
                     :taskdecls taskdecls
                     :fundecls fundecls
                     :paramdecls paramdecls
                     :typedefs typedefs
                     :imports imports
                     :fwdtypes nil))))

Theorem: vl-design-p-of-vl-remove-unnecessary-elements

(defthm vl-design-p-of-vl-remove-unnecessary-elements
 (b* ((trimmed-design (vl-remove-unnecessary-elements keep design)))
   (vl-design-p trimmed-design))
 :rule-classes :rewrite)

Theorem: vl-remove-unnecessary-elements-of-string-list-fix-keep

(defthm vl-remove-unnecessary-elements-of-string-list-fix-keep
  (equal (vl-remove-unnecessary-elements (string-list-fix keep)
                                         design)
         (vl-remove-unnecessary-elements keep design)))

Theorem: vl-remove-unnecessary-elements-string-list-equiv-congruence-on-keep

(defthm
 vl-remove-unnecessary-elements-string-list-equiv-congruence-on-keep
 (implies
      (str::string-list-equiv keep keep-equiv)
      (equal (vl-remove-unnecessary-elements keep design)
             (vl-remove-unnecessary-elements keep-equiv design)))
 :rule-classes :congruence)

Theorem: vl-remove-unnecessary-elements-of-vl-design-fix-design

(defthm vl-remove-unnecessary-elements-of-vl-design-fix-design
 (equal (vl-remove-unnecessary-elements keep (vl-design-fix design))
        (vl-remove-unnecessary-elements keep design)))

Theorem: vl-remove-unnecessary-elements-vl-design-equiv-congruence-on-design

(defthm
 vl-remove-unnecessary-elements-vl-design-equiv-congruence-on-design
 (implies
      (vl-design-equiv design design-equiv)
      (equal (vl-remove-unnecessary-elements keep design)
             (vl-remove-unnecessary-elements keep design-equiv)))
 :rule-classes :congruence)