		Search-engine friendly clone of the ACL2 documentation.

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