		Search-engine friendly clone of the ACL2 documentation.

Make-implicit-wires

Vl-gateinst-exprs-for-implicit-wires

Gets the expressions from a gate instance, for making implicit wires.

Signature
(vl-gateinst-exprs-for-implicit-wires x) → (mv main other)
Arguments: x — Guard (vl-gateinst-p x).
Returns: main — The expressions from the gateinst's port list, where implicit wires are allowed.
Type (vl-exprlist-p main).; other — The other expressions in the gate instance (its range, delay) where implicit wires aren't allowed.
Type (vl-exprlist-p other).

Definitions and Theorems

Function: vl-gateinst-exprs-for-implicit-wires

(defun vl-gateinst-exprs-for-implicit-wires (x)
  (declare (xargs :guard (vl-gateinst-p x)))
  (let ((__function__ 'vl-gateinst-exprs-for-implicit-wires))
    (declare (ignorable __function__))
    (b* (((vl-gateinst x) x))
      (mv (vl-plainarglist-allexprs x.args)
          (append (vl-maybe-range-allexprs x.range)
                  (vl-maybe-gatedelay-allexprs x.delay))))))

Theorem: vl-exprlist-p-of-vl-gateinst-exprs-for-implicit-wires.main

(defthm vl-exprlist-p-of-vl-gateinst-exprs-for-implicit-wires.main
  (b* (((mv ?main ?other)
        (vl-gateinst-exprs-for-implicit-wires x)))
    (vl-exprlist-p main))
  :rule-classes :rewrite)

Theorem: vl-exprlist-p-of-vl-gateinst-exprs-for-implicit-wires.other

(defthm vl-exprlist-p-of-vl-gateinst-exprs-for-implicit-wires.other
  (b* (((mv ?main ?other)
        (vl-gateinst-exprs-for-implicit-wires x)))
    (vl-exprlist-p other))
  :rule-classes :rewrite)

Theorem: vl-gateinst-exprs-for-implicit-wires-mvtypes-0

(defthm vl-gateinst-exprs-for-implicit-wires-mvtypes-0
  (true-listp (mv-nth 0
                      (vl-gateinst-exprs-for-implicit-wires x)))
  :rule-classes :type-prescription)

Theorem: vl-gateinst-exprs-for-implicit-wires-mvtypes-1

(defthm vl-gateinst-exprs-for-implicit-wires-mvtypes-1
  (true-listp (mv-nth 1
                      (vl-gateinst-exprs-for-implicit-wires x)))
  :rule-classes :type-prescription)

Theorem: vl-gateinst-exprs-for-implicit-wires-complete

(defthm vl-gateinst-exprs-for-implicit-wires-complete
  (let ((ret (vl-gateinst-exprs-for-implicit-wires x)))
    (set-equiv (append (mv-nth 0 ret) (mv-nth 1 ret))
               (vl-gateinst-allexprs x))))

Theorem: vl-gateinst-exprs-for-implicit-wires-of-vl-gateinst-fix-x

(defthm vl-gateinst-exprs-for-implicit-wires-of-vl-gateinst-fix-x
  (equal (vl-gateinst-exprs-for-implicit-wires (vl-gateinst-fix x))
         (vl-gateinst-exprs-for-implicit-wires x)))

Theorem: vl-gateinst-exprs-for-implicit-wires-vl-gateinst-equiv-congruence-on-x

(defthm
 vl-gateinst-exprs-for-implicit-wires-vl-gateinst-equiv-congruence-on-x
 (implies (vl-gateinst-equiv x x-equiv)
          (equal (vl-gateinst-exprs-for-implicit-wires x)
                 (vl-gateinst-exprs-for-implicit-wires x-equiv)))
 :rule-classes :congruence)