		Search-engine friendly clone of the ACL2 documentation.

Port-expressions

Vl-portexpr->internalnames

Collect the names of any internal wires that are connected to a well-formed port and return them as a list of strings.

Signature
(vl-portexpr->internalnames x) → names
Arguments: x — Guard (vl-expr-p x).
Returns: names — Type (string-listp names).

We just collect the names of the internal wires that are connected to the port. For instance, in the following module,

module mod (a, .b(foo), .c( {bar[2], baz[width-1:0] } )) ;
  ...
endmodule

the internalnames for the first port are ("a"), the second port to ("foo"), and for the third port to ("bar" "baz").

Note that this is a bit different than, e.g., just using vl-expr-names, because we omit any names that occur in index expressions, i.e., notice how we omit width in the third port.

Definitions and Theorems

Function: vl-portexpr->internalnames

(defun vl-portexpr->internalnames (x)
  (declare (xargs :guard (vl-expr-p x)))
  (declare (xargs :guard (vl-portexpr-p x)))
  (let ((__function__ 'vl-portexpr->internalnames))
    (declare (ignorable __function__))
    (if (vl-atomicportexpr-p x)
        (list (vl-atomicportexpr->internalname x))
      (vl-atomicportexprlist->internalnames (vl-nonatom->args x)))))

Theorem: string-listp-of-vl-portexpr->internalnames

(defthm string-listp-of-vl-portexpr->internalnames
  (b* ((names (vl-portexpr->internalnames x)))
    (string-listp names))
  :rule-classes :rewrite)

Theorem: vl-portexpr->internalnames-of-vl-expr-fix-x

(defthm vl-portexpr->internalnames-of-vl-expr-fix-x
  (equal (vl-portexpr->internalnames (vl-expr-fix x))
         (vl-portexpr->internalnames x)))

Theorem: vl-portexpr->internalnames-vl-expr-equiv-congruence-on-x

(defthm vl-portexpr->internalnames-vl-expr-equiv-congruence-on-x
  (implies (vl-expr-equiv x x-equiv)
           (equal (vl-portexpr->internalnames x)
                  (vl-portexpr->internalnames x-equiv)))
  :rule-classes :congruence)