		Search-engine friendly clone of the ACL2 documentation.

Make-implicit-wires

Vl-modinst-exprs-for-implicit-wires

Get the expressions from a module instance, for making implicit wires.

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

Definitions and Theorems

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

(defun vl-modinst-exprs-for-implicit-wires (x)
  (declare (xargs :guard (vl-modinst-p x)))
  (let ((__function__ 'vl-modinst-exprs-for-implicit-wires))
    (declare (ignorable __function__))
    (b* (((vl-modinst x) x)
         ((mv main other)
          (vl-collect-exprs-for-implicit-wires-from-portargs
               x.portargs)))
      (mv main
          (append other (vl-maybe-range-allexprs x.range)
                  (vl-paramargs-allexprs x.paramargs)
                  (vl-maybe-gatedelay-allexprs x.delay))))))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Subtopics

Vl-collect-exprs-for-implicit-wires-from-namedargs
Vl-collect-exprs-for-implicit-wires-from-portargs
Vl-collect-exprs-for-implicit-wires-from-namedarg