• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • Vl
      • Syntax
      • Loader
      • Warnings
      • Getting-started
      • Utilities
      • Printer
      • Kit
      • Mlib
        • Scopestack
        • Hid-tools
        • Filtering-by-name
          • Vl-keep-modinsts-by-modname
          • Vl-keep-modinsts-by-instname
          • Vl-delete-modinsts-by-instname
          • Vl-keep-imports-by-package
          • Vl-delete-modinsts-by-modname
          • Vl-delete-imports-by-package
          • Vl-keep-descriptions
          • Vl-delete-descriptions
          • Vl-keep-paramdecls
          • Vl-keep-interfaces
          • Vl-delete-paramdecls
          • Vl-delete-interfaces
          • Vl-keep-vardecls
          • Vl-keep-typedefs
          • Vl-keep-taskdecls
          • Vl-keep-programs
          • Vl-keep-portdecls
          • Vl-keep-packages
          • Vl-keep-fundecls
          • Vl-delete-taskdecls
          • Vl-delete-portdecls
          • Vl-keep-modules
          • Vl-keep-configs
            • Vl-fast-keep-configs
            • Vl-slow-keep-configs
          • Vl-keep-classes
          • Vl-delete-vardecls
          • Vl-delete-typedefs
          • Vl-delete-programs
          • Vl-delete-packages
          • Vl-delete-fundecls
          • Vl-delete-modules
          • Vl-delete-configs
          • Vl-delete-classes
          • Vl-keep-udps
          • Vl-delete-udps
          • Vl-filter-modinsts-by-modname+
          • Vl-filter-modinsts-by-modname
          • Vl-filter-modinsts-by-instname
          • Vl-filter-imports-by-package
          • Vl-filter-descriptions
          • Vl-filter-vardecls
          • Vl-filter-typedefs
          • Vl-filter-taskdecls
          • Vl-filter-programs
          • Vl-filter-portdecls
          • Vl-filter-paramdecls
          • Vl-filter-packages
          • Vl-filter-modules
          • Vl-filter-interfaces
          • Vl-filter-fundecls
          • Vl-filter-configs
          • Vl-filter-udps
          • Vl-filter-classes
        • Vl-interface-mocktype
        • Stripping-functions
        • Genblob
        • Expr-tools
        • Extract-vl-types
        • Hierarchy
        • 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

• Filtering-by-name

Vl-keep-configs

Keep vl-config-ps by name.

Signature

(vl-keep-configs names x) → filtered-x

Arguments

names — Names of vl-configs to keep.
    Guard (string-listp names).

x — List to filter.
    Guard (vl-configlist-p x).

Returns

filtered-x — Type (vl-configlist-p filtered-x).

Definitions and Theorems

Function: vl-keep-configs

(defun vl-keep-configs (names x)
 (declare (xargs :guard (and (string-listp names)
                             (vl-configlist-p x))))
 (let ((__function__ 'vl-keep-configs))
  (declare (ignorable __function__))
  (mbe
   :logic
   (cond ((atom x) nil)
         ((member-equal (vl-config->name (car x))
                        (string-list-fix names))
          (cons (vl-config-fix (car x))
                (vl-keep-configs names (cdr x))))
         (t (vl-keep-configs names (cdr x))))
   :exec
   (b*
    (((when (or (atom names) (atom x))) nil)
     ((unless (longer-than-p 10 names))
      (vl-slow-keep-configs names x))
     (fal (make-lookup-alist names))
     (ans (with-local-nrev (vl-fast-keep-configs names fal x nrev)))
     (- (fast-alist-free fal)))
    ans))))

Theorem: vl-configlist-p-of-vl-keep-configs

(defthm vl-configlist-p-of-vl-keep-configs
  (b* ((filtered-x (vl-keep-configs names x)))
    (vl-configlist-p filtered-x))
  :rule-classes :rewrite)

Theorem: vl-keep-configs-when-atom

(defthm vl-keep-configs-when-atom
  (implies (atom x)
           (equal (vl-keep-configs names x) nil)))

Theorem: vl-keep-configs-of-cons

(defthm vl-keep-configs-of-cons
  (equal (vl-keep-configs names (cons a x))
         (if (member-equal (vl-config->name a)
                           (string-list-fix names))
             (cons (vl-config-fix a)
                   (vl-keep-configs names x))
           (vl-keep-configs names x))))

Theorem: member-equal-of-vl-keep-configs

(defthm member-equal-of-vl-keep-configs
  (iff (member-equal a (vl-keep-configs names x))
       (and (member-equal a (vl-configlist-fix x))
            (member-equal (vl-config->name a)
                          (string-list-fix names)))))

Theorem: subsetp-equal-of-vl-keep-configs

(defthm subsetp-equal-of-vl-keep-configs
  (subsetp-equal (vl-keep-configs names x)
                 (vl-configlist-fix x)))

Theorem: vl-keep-configs-when-atom-of-names

(defthm vl-keep-configs-when-atom-of-names
  (implies (atom names)
           (equal (vl-keep-configs names x) nil)))

Theorem: vl-slow-keep-configs-removal

(defthm vl-slow-keep-configs-removal
  (equal (vl-slow-keep-configs names x)
         (vl-keep-configs names x)))

Theorem: vl-fast-keep-configs-removal

(defthm vl-fast-keep-configs-removal
  (equal (vl-fast-keep-configs names fal x nrev)
         (append nrev (vl-keep-configs names x))))

Theorem: vl-keep-configs-of-string-list-fix-names

(defthm vl-keep-configs-of-string-list-fix-names
  (equal (vl-keep-configs (string-list-fix names)
                          x)
         (vl-keep-configs names x)))

Theorem: vl-keep-configs-string-list-equiv-congruence-on-names

(defthm vl-keep-configs-string-list-equiv-congruence-on-names
  (implies (str::string-list-equiv names names-equiv)
           (equal (vl-keep-configs names x)
                  (vl-keep-configs names-equiv x)))
  :rule-classes :congruence)

Theorem: vl-keep-configs-of-vl-configlist-fix-x

(defthm vl-keep-configs-of-vl-configlist-fix-x
  (equal (vl-keep-configs names (vl-configlist-fix x))
         (vl-keep-configs names x)))

Theorem: vl-keep-configs-vl-configlist-equiv-congruence-on-x

(defthm vl-keep-configs-vl-configlist-equiv-congruence-on-x
  (implies (vl-configlist-equiv x x-equiv)
           (equal (vl-keep-configs names x)
                  (vl-keep-configs names x-equiv)))
  :rule-classes :congruence)

Subtopics

Vl-fast-keep-configs

Vl-slow-keep-configs