		Search-engine friendly clone of the ACL2 documentation.

Expr-tools

Vl-expr-names

Gather the names of all vl-id-p atoms throughout an expression.

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

We compute the names of all simple identifiers used throughout an expression.

These identifiers might refer to wires, registers, ports, parameters, or anything else in the module. This function can often be used in conjunction with the allexprs family of functions, e.g., to see all the wires that are ever mentioned in some module item.

Note that we look for vl-id-p atoms only. A consequence is that we do not return any hierarchical identifiers, function names, or system function names, since these are not treated as vl-id-p atoms, but are instead vl-hidpiece-p, vl-sysfunname-p, or vl-funname-p atoms.

Note that as we gather names, we do NOT descend into any embedded (* foo = bar *)-style attributes.

vl-expr-names is necessarily mutually-recursive with vl-exprlist-names. For efficiency we use a tail-recursive, accumulator-style functions to do the collection. Under the hood, we also use nreverse optimization.

Theorem: return-type-of-vl-expr-names.names

(defthm return-type-of-vl-expr-names.names
  (b* ((?names (vl-expr-names x)))
    (string-listp names))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-exprlist-names.names

(defthm return-type-of-vl-exprlist-names.names
  (b* ((?names (vl-exprlist-names x)))
    (string-listp names))
  :rule-classes :rewrite)

Theorem: true-listp-of-vl-expr-names

(defthm true-listp-of-vl-expr-names
  (true-listp (vl-expr-names x))
  :rule-classes :type-prescription)

Theorem: true-listp-of-vl-exprlist-names

(defthm true-listp-of-vl-exprlist-names
  (true-listp (vl-exprlist-names x))
  :rule-classes :type-prescription)

Theorem: vl-expr-names-nrev-removal

(defthm vl-expr-names-nrev-removal
  (equal (vl-expr-names-nrev x nrev)
         (append nrev (vl-expr-names x))))

Theorem: vl-exprlist-names-nrev-removal

(defthm vl-exprlist-names-nrev-removal
  (equal (vl-exprlist-names-nrev x nrev)
         (append nrev (vl-exprlist-names x))))

Theorem: vl-exprlist-names-when-atom

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

Theorem: vl-exprlist-names-of-cons

(defthm vl-exprlist-names-of-cons
  (equal (vl-exprlist-names (cons a x))
         (append (vl-expr-names a)
                 (vl-exprlist-names x))))

Theorem: vl-exprlist-names-of-append

(defthm vl-exprlist-names-of-append
  (equal (vl-exprlist-names (append x y))
         (append (vl-exprlist-names x)
                 (vl-exprlist-names y))))

Theorem: vl-exprlist-names-preserves-set-equiv

(defthm vl-exprlist-names-preserves-set-equiv
  (implies (set-equiv x x-equiv)
           (set-equiv (vl-exprlist-names x)
                      (vl-exprlist-names x-equiv)))
  :rule-classes (:congruence))

Theorem: vl-expr-names-of-vl-expr-fix-x

(defthm vl-expr-names-of-vl-expr-fix-x
  (equal (vl-expr-names (vl-expr-fix x))
         (vl-expr-names x)))

Theorem: vl-exprlist-names-of-vl-exprlist-fix-x

(defthm vl-exprlist-names-of-vl-exprlist-fix-x
  (equal (vl-exprlist-names (vl-exprlist-fix x))
         (vl-exprlist-names x)))

Theorem: vl-expr-names-vl-expr-equiv-congruence-on-x

(defthm vl-expr-names-vl-expr-equiv-congruence-on-x
  (implies (vl-expr-equiv x x-equiv)
           (equal (vl-expr-names x)
                  (vl-expr-names x-equiv)))
  :rule-classes :congruence)

Theorem: vl-exprlist-names-vl-exprlist-equiv-congruence-on-x

(defthm vl-exprlist-names-vl-exprlist-equiv-congruence-on-x
  (implies (vl-exprlist-equiv x x-equiv)
           (equal (vl-exprlist-names x)
                  (vl-exprlist-names x-equiv)))
  :rule-classes :congruence)

Subtopics

Vl-expr-names-nrev
Vl-exprlist-names