		Search-engine friendly clone of the ACL2 documentation.

Propagate

Vl-maybe-driven-by-args

Approximately collects the names of wires that are driven by the arguments to a gate/module instance. (unsound)

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

This hopefully returns an overapproximation of the wires that might possibly be driven by a gate/module instance with these arguments. Note that we only collect names here, so the entire wire is considered driven even if only a single bit of it is driven, etc.

It is not sound if there are incorrectly labeled ports (e.g., if a submodule drives its inputs, then we will not realize that the wires connected to that input are driven.

Definitions and Theorems

Function: vl-maybe-driven-by-args

(defun vl-maybe-driven-by-args (x)
  (declare (xargs :guard (vl-plainarglist-p x)))
  (let ((__function__ 'vl-maybe-driven-by-args))
    (declare (ignorable __function__))
    (b* (((mv ?in out inout unknown)
          (vl-partition-plainargs x nil nil nil nil))
         (out (remove nil (vl-plainarglist->exprs out)))
         (inout (remove nil (vl-plainarglist->exprs inout)))
         (unknown (remove nil (vl-plainarglist->exprs unknown))))
      (append (vl-exprlist-names out)
              (vl-exprlist-names inout)
              (vl-exprlist-names unknown)))))

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

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