• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • 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-interface->flatten-modinsts
              • Vl-interfacelist-everinstanced-nrev
            • 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-interfacelist-everinstanced

Gather the names of every module and interface ever instanced in a interface list or used in an interface port.

Signature
(vl-interfacelist-everinstanced x) → names
Arguments
x — Guard (vl-interfacelist-p x).
Returns
names — Type (string-listp names).

The returned list typically will contain a lot of duplicates. This is fairly expensive, requiring a cons for every single interface instance. We optimize it to avoid the construction of intermediate lists and to use nrev.

Definitions and Theorems

Function: vl-interfacelist-everinstanced

(defun vl-interfacelist-everinstanced (x)
  (declare (xargs :guard (vl-interfacelist-p x)))
  (let ((__function__ 'vl-interfacelist-everinstanced))
    (declare (ignorable __function__))
    (mbe :logic
         (b* (((when (atom x)) nil)
              (modinsts1 (vl-interface->flatten-modinsts (car x)))
              (ifports1 (vl-interface->ifports (car x))))
           (append (vl-modinstlist->modnames modinsts1)
                   (vl-interfaceportlist->ifnames ifports1)
                   (vl-interfacelist-everinstanced (cdr x))))
         :exec
         (if (atom x)
             nil
           (with-local-nrev
                (vl-interfacelist-everinstanced-nrev x nrev))))))

Theorem: string-listp-of-vl-interfacelist-everinstanced

(defthm string-listp-of-vl-interfacelist-everinstanced
  (b* ((names (vl-interfacelist-everinstanced x)))
    (string-listp names))
  :rule-classes :rewrite)

Theorem: vl-interfacelist-everinstanced-nrev-removal

(defthm vl-interfacelist-everinstanced-nrev-removal
  (equal (vl-interfacelist-everinstanced-nrev x nrev)
         (append nrev
                 (vl-interfacelist-everinstanced x))))

Theorem: vl-interfacelist-everinstanced-of-vl-interfacelist-fix-x

(defthm vl-interfacelist-everinstanced-of-vl-interfacelist-fix-x
  (equal (vl-interfacelist-everinstanced (vl-interfacelist-fix x))
         (vl-interfacelist-everinstanced x)))

Theorem: vl-interfacelist-everinstanced-vl-interfacelist-equiv-congruence-on-x

(defthm
 vl-interfacelist-everinstanced-vl-interfacelist-equiv-congruence-on-x
 (implies (vl-interfacelist-equiv x x-equiv)
          (equal (vl-interfacelist-everinstanced x)
                 (vl-interfacelist-everinstanced x-equiv)))
 :rule-classes :congruence)

Subtopics

Vl-interface->flatten-modinsts
Gather modinsts from the module, including its generate blocks and bind constructs (which don't even belong to it) -- rarely sensible!
Vl-interfacelist-everinstanced-nrev