		Search-engine friendly clone of the ACL2 documentation.

Propagate

Vl-maybe-driven-by-modinst

Approxpimately the wires driven by a module instance (unsound).

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

Definitions and Theorems

Function: vl-maybe-driven-by-modinst

(defun vl-maybe-driven-by-modinst (x)
  (declare (xargs :guard (vl-modinst-p x)))
  (let ((__function__ 'vl-maybe-driven-by-modinst))
    (declare (ignorable __function__))
    (b* ((args (vl-modinst->portargs x))
         ((unless (eq (vl-arguments-kind args)
                      :vl-arguments-plain))
          (raise "args still named???")))
      (vl-maybe-driven-by-args (vl-arguments-plain->args args)))))

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

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