		Search-engine friendly clone of the ACL2 documentation.

Propagate

Vl-driven-by-assign

Approximate the wires driven by an assignment.

Signature
(vl-driven-by-assign x) → drive-names
Arguments: x — Guard (vl-assign-p x).
Returns: drive-names — Type (string-listp drive-names), given the guard.

Definitions and Theorems

Function: vl-driven-by-assign

(defun vl-driven-by-assign (x)
  (declare (xargs :guard (vl-assign-p x)))
  (let ((__function__ 'vl-driven-by-assign))
    (declare (ignorable __function__))
    (vl-expr-names (vl-assign->lvalue x))))

Theorem: string-listp-of-vl-driven-by-assign

(defthm string-listp-of-vl-driven-by-assign
  (implies (and (force (vl-assign-p x)))
           (b* ((drive-names (vl-driven-by-assign x)))
             (string-listp drive-names)))
  :rule-classes :rewrite)