		Search-engine friendly clone of the ACL2 documentation.

Propagate

Vl-maybe-driven-by-gateinst

Approximately the wires driven by a gate instance.

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

This should be sound if argresolve treats gate instances correctly.

Definitions and Theorems

Function: vl-maybe-driven-by-gateinst

(defun vl-maybe-driven-by-gateinst (x)
  (declare (xargs :guard (vl-gateinst-p x)))
  (let ((__function__ 'vl-maybe-driven-by-gateinst))
    (declare (ignorable __function__))
    (vl-maybe-driven-by-args (vl-gateinst->args x))))

Theorem: string-listp-of-vl-maybe-driven-by-gateinst

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