		Search-engine friendly clone of the ACL2 documentation.

Occform

Vl-simple-instantiate

Convenient way to generating module instances.

Signature
(vl-simple-instantiate x instname actuals &key (loc '*vl-fakeloc*)) → inst
Arguments: x — submodule to create an instance of.
Guard (vl-module-p x).; instname — name for the new instance.
Guard (stringp instname).; actuals — expressions to bind to the module's ports in port order.
Guard (vl-exprlist-p actuals).; loc — Guard (vl-location-p loc).
Returns: inst — Type (vl-modinst-p inst).

If you are writing code to generate modules (as we often are in occform), it can be particularly onerous to generate module instances because you have to build vl-plainarg-p structures for all of the arguments and wrap these up in a vl-arguments-p.

vl-simple-instantiate automates this, at least for instantiating simple modules. You tell it the module you want to instantiate, x, and the expressions you want to use as the actuals. It pairs up these actuals with the submodule's ports, figuring out the directions/names of the plainargs, etc., and gives you back the new instance. As an added bonus, you get basic arity checking.

Definitions and Theorems

Function: vl-simple-instantiate-fn

(defun vl-simple-instantiate-fn (x instname actuals loc)
 (declare (xargs :guard (and (vl-module-p x)
                             (stringp instname)
                             (vl-exprlist-p actuals)
                             (vl-location-p loc))))
 (let ((__function__ 'vl-simple-instantiate))
  (declare (ignorable __function__))
  (b*
   (((vl-module x) x)
    (plainargs
      (if
       (and (not x.ifports)
            (same-lengthp actuals x.ports))
       (vl-simple-instantiate-args-main actuals x.ports x.portdecls)
       (raise "Wrong number of arguments for ~x0.~%"
              x.name))))
   (make-vl-modinst
        :modname x.name
        :instname (string-fix instname)
        :paramargs (make-vl-paramargs-plain :args nil)
        :portargs (make-vl-arguments-plain :args plainargs)
        :loc loc))))

Theorem: vl-modinst-p-of-vl-simple-instantiate

(defthm vl-modinst-p-of-vl-simple-instantiate
  (b* ((inst (vl-simple-instantiate-fn x instname actuals loc)))
    (vl-modinst-p inst))
  :rule-classes :rewrite)

Theorem: vl-simple-instantiate-fn-of-vl-module-fix-x

(defthm vl-simple-instantiate-fn-of-vl-module-fix-x
  (equal (vl-simple-instantiate-fn (vl-module-fix x)
                                   instname actuals loc)
         (vl-simple-instantiate-fn x instname actuals loc)))

Theorem: vl-simple-instantiate-fn-vl-module-equiv-congruence-on-x

(defthm vl-simple-instantiate-fn-vl-module-equiv-congruence-on-x
 (implies
    (vl-module-equiv x x-equiv)
    (equal (vl-simple-instantiate-fn x instname actuals loc)
           (vl-simple-instantiate-fn x-equiv instname actuals loc)))
 :rule-classes :congruence)

Theorem: vl-simple-instantiate-fn-of-str-fix-instname

(defthm vl-simple-instantiate-fn-of-str-fix-instname
  (equal (vl-simple-instantiate-fn x (str-fix instname)
                                   actuals loc)
         (vl-simple-instantiate-fn x instname actuals loc)))

Theorem: vl-simple-instantiate-fn-streqv-congruence-on-instname

(defthm vl-simple-instantiate-fn-streqv-congruence-on-instname
 (implies
    (streqv instname instname-equiv)
    (equal (vl-simple-instantiate-fn x instname actuals loc)
           (vl-simple-instantiate-fn x instname-equiv actuals loc)))
 :rule-classes :congruence)

Theorem: vl-simple-instantiate-fn-of-vl-exprlist-fix-actuals

(defthm vl-simple-instantiate-fn-of-vl-exprlist-fix-actuals
 (equal
      (vl-simple-instantiate-fn x instname (vl-exprlist-fix actuals)
                                loc)
      (vl-simple-instantiate-fn x instname actuals loc)))

Theorem: vl-simple-instantiate-fn-vl-exprlist-equiv-congruence-on-actuals

(defthm
   vl-simple-instantiate-fn-vl-exprlist-equiv-congruence-on-actuals
 (implies
    (vl-exprlist-equiv actuals actuals-equiv)
    (equal (vl-simple-instantiate-fn x instname actuals loc)
           (vl-simple-instantiate-fn x instname actuals-equiv loc)))
 :rule-classes :congruence)

Theorem: vl-simple-instantiate-fn-of-vl-location-fix-loc

(defthm vl-simple-instantiate-fn-of-vl-location-fix-loc
 (equal
   (vl-simple-instantiate-fn x
                             instname actuals (vl-location-fix loc))
   (vl-simple-instantiate-fn x instname actuals loc)))

Theorem: vl-simple-instantiate-fn-vl-location-equiv-congruence-on-loc

(defthm vl-simple-instantiate-fn-vl-location-equiv-congruence-on-loc
 (implies
    (vl-location-equiv loc loc-equiv)
    (equal (vl-simple-instantiate-fn x instname actuals loc)
           (vl-simple-instantiate-fn x instname actuals loc-equiv)))
 :rule-classes :congruence)

Subtopics

Vl-simple-instantiate-list: Generate a bunch of module instances.
Vl-simple-instantiate-args-main: Create plainargs binding some actuals to their ports, filling in the portnames and directions.
Vl-simple-inst: Like vl-simple-instantiate except it's a nice macro so that you don't have to put the actuals in a list.