• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Fgl
    • Vwsim
    • Vl
      • Syntax
      • Loader
      • Warnings
      • Getting-started
      • Utilities
      • Printer
      • Kit
      • Mlib
      • Transforms
        • Unparameterization
          • Vl-unparameterize-flow
          • Vl-unparam-inst
          • Vl-unparam-add-to-ledger
          • Vl-scopeinfo-resolve-params
          • Vl-scope-finalize-params
          • Vl-create-unparameterized-interface
          • Vl-create-unparameterized-module
          • Vl-unparam-actualkeys
          • Vl-make-paramdecloverrides
          • Vl-unparam-class
          • Vl-unparam-instlist
          • Vl-create-unparameterized-class
          • Vl-add-lost-interface-warnings
          • Vl-add-lost-module-warnings
          • Vl-unparam-classlist
          • Vl-interfacelist->orignames
          • Vl-user-signature
          • Vl-interfaceport-default-signature
          • Vl-modulelist->orignames
          • Vl-plainarglist-update-ifports
          • Vl-portlist-interface-signatures
          • Vl-user-signatures
          • Vl-plainarg-update-ifports
          • Vl-unparam-inst->instkey
          • Vl-toplevel-signatures
          • Vl-unparam-basename
          • Vl-genblob-resolve-rejoin-scopeitems
          • Vl-gencase-some-match
          • Vl-gencase-match
          • Vl-package-elaborate
          • Vl-unparam-signature
          • Vl-unparam-ledger
          • Vl-packagelist-elaborate
          • Vl-design-elaborate
          • Vl-unparam-actualkey
          • Vl-make-paramdecloverrides-named
          • Vl-unparameterize-main
          • Vl-recover-modules-lost-from-elaboration
          • Vl-finish-unparameterized-interface
          • Vl-paramdecl-set-default
          • Vl-genblob-rejoin-scopeitems
          • Vl-finish-unparameterized-interfaces
          • Vl-unparam-instkey
          • Vl-finish-unparameterized-module
          • Vl-finish-unparameterized-class
          • Vl-finish-unparameterized-modules
          • Vl-finish-unparameterized-classes
          • Vl-genblob-split-scopeitems
          • Vl-user-paramsettings-for-top-names
          • Vl-string/int-alist-to-namedargs
          • Vl-add-lost-interface-warning
          • Vl-unparam-basename-exprstring
          • Vl-add-lost-module-warning
          • Vl-paramdecllist-remove-defaults
          • Vl-ifport-alist
          • Vl-paramdecl-remove-default
          • Vl-ifportexpr->name
          • Vl-paramdecllist-all-localp
          • Vl-unparam-instkeymap
          • Vl-unparam-donelist
          • Vl-unparam-instkeylist
        • Elaborate
        • Addnames
        • Annotate
        • Clean-warnings
        • Eliminitial
        • Custom-transform-hooks
        • Problem-modules
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Unparameterization

Vl-unparam-inst

Compute the final parameter values for a single module instance.

Signature

(vl-unparam-inst inst elabindex 
                 ledger warnings &key (config 'config)) 
 
  → 
(mv successp warnings inst instkey new-elabindex ledger)

Arguments

inst — Instance of some module. The module being instantiated may or may not have parameters.
    Guard (vl-modinst-p inst).

elabindex — at the instanting context.

ledger — Guard (vl-unparam-ledger-p ledger).

warnings — Warnings accumulator for the submodule.
    Guard (vl-warninglist-p warnings).

config — Guard (vl-simpconfig-p config).

Returns

successp — Type (booleanp successp).

warnings — Type (vl-warninglist-p warnings).

inst — Updated module instance, perhaps instantiating a new module like my_adder$width=5 instead of my_adder.
    Type (vl-modinst-p inst).

instkey — An instkey for the instantiated module, if needed. Note: Currently we produce an instkey even if there are no parameters. Not sure why we need to do this.
    Type (implies successp (vl-unparam-instkey-p instkey)).

ledger — Type (vl-unparam-ledger-p ledger).

Definitions and Theorems

Function: vl-unparam-inst-fn

(defun vl-unparam-inst-fn (inst elabindex ledger warnings config)
 (declare (xargs :stobjs (elabindex)))
 (declare (xargs :guard (and (vl-modinst-p inst)
                             (vl-unparam-ledger-p ledger)
                             (vl-warninglist-p warnings)
                             (vl-simpconfig-p config))))
 (let ((__function__ 'vl-unparam-inst))
  (declare (ignorable __function__))
  (b*
   ((ss (vl-elabindex->ss))
    ((vl-simpconfig config))
    ((mv warnings inst)
     (vl-modinst-maybe-argresolve config.defer-argresolve
                                  inst ss warnings))
    ((vl-modinst inst) inst)
    (ledger (vl-unparam-ledger-fix ledger))
    (elabindex (vl-elabindex-sync-scopes))
    (scopes (vl-elabindex->scopes))
    ((mv mod mod-ss)
     (vl-scopestack-find-definition/ss inst.modname ss))
    ((unless (and mod
                  (or (eq (tag mod) :vl-module)
                      (eq (tag mod) :vl-interface))))
     (vl-unparam-debug "~a0: can't find module ~a1.~%"
                       inst inst.modname)
     (mv nil
         (fatal :type :vl-unresolved-instance
                :msg "~a0 refers to undefined module ~m1."
                :args (list inst inst.modname))
         inst nil elabindex ledger))
    (mod.paramdecls (if (eq (tag mod) :vl-module)
                        (vl-module->paramdecls mod)
                      (vl-interface->paramdecls mod)))
    (mod.ports (if (eq (tag mod) :vl-module)
                   (vl-module->ports mod)
                 (vl-interface->ports mod)))
    ((unless (vl-arguments-case
                  inst.portargs
                  :vl-arguments-plain (eql (len inst.portargs.args)
                                           (len mod.ports))
                  :otherwise nil))
     (mv
      nil
      (fatal
       :type :vl-programming-error
       :msg
       "~a0: port args should be a plainarglist of the same ~
                         length as the module's ports"
       :args (list inst))
      inst nil elabindex ledger))
    (args (vl-arguments-plain->args inst.portargs))
    ((mv err new-ports inst-ifportalist)
     (vl-plainarglist-update-ifports args mod.ports ss scopes))
    ((when err)
     (mv nil
         (fatal :type :vl-instance-bad-interfaceports
                :msg "~a0: Interfaceport processing failed: ~@1"
                :args (list inst err))
         inst nil elabindex ledger))
    (elabindex
         (vl-elabindex-traverse mod-ss
                                (list (vl-elabinstruction-root))))
    (elabindex (if (and (vl-paramargs-empty-p inst.paramargs)
                        (atom inst-ifportalist))
                   elabindex
                 (b* ((scopes (vl-elabscopes-update-subscope
                                   (vl-elabkey-def inst.modname)
                                   (make-vl-elabscope)
                                   (vl-elabindex->scopes))))
                   (vl-elabindex-update-scopes scopes))))
    (elabindex (vl-elabindex-push mod))
    ((mv ok scope-warnings
         elabindex final-paramdecls)
     (vl-scope-finalize-params
          mod.paramdecls
          inst.paramargs nil elabindex ss
          (rev (vl-elabscopes->elabtraversal scopes))))
    (warnings
     (append
       (vl-warninglist-add-ctx scope-warnings (vl-modinst-fix inst))
       warnings))
    (inside-mod-ss (vl-elabindex->ss))
    (elabindex (vl-elabindex-undo))
    ((unless ok)
     (vl-unparam-debug "~a0: failed to finalize params~%" inst)
     (b* ((elabindex (vl-elabindex-undo)))
       (mv nil
           warnings inst nil elabindex ledger)))
    ((mv instkey ledger)
     (vl-unparam-add-to-ledger inst.modname final-paramdecls
                               new-ports inst-ifportalist
                               ledger ss inside-mod-ss))
    ((vl-unparam-signature sig)
     (cdr (hons-get instkey
                    (vl-unparam-ledger->instkeymap ledger))))
    (new-inst (change-vl-modinst inst
                                 :modname sig.newname
                                 :paramargs *vl-empty-paramargs*))
    (scopes (vl-elabindex->scopes))
    (mod-scope (vl-elabscopes-subscope (vl-elabkey-def inst.modname)
                                       (vl-elabindex->scopes)))
    (scopes
     (b*
      (((unless mod-scope) scopes)
       (scopes
        (vl-elabscopes-update-subscope (vl-elabkey-def inst.modname)
                                       (make-vl-elabscope)
                                       scopes)))
      (vl-elabscopes-update-subscope (vl-elabkey-def sig.newname)
                                     mod-scope scopes)))
    (elabindex (vl-elabindex-update-scopes scopes elabindex))
    (elabindex (vl-elabindex-undo))
    (elabindex
         (if inst.instname
             (vl-elabindex-update-item-info inst.instname new-inst)
           elabindex)))
   (vl-unparam-debug "~a0: success, new instance is ~a1.~%"
                     inst new-inst)
   (mv t warnings
       new-inst instkey elabindex ledger))))

Theorem: booleanp-of-vl-unparam-inst.successp

(defthm booleanp-of-vl-unparam-inst.successp
  (b* (((mv ?successp ?warnings
            ?inst ?instkey ?new-elabindex ?ledger)
        (vl-unparam-inst-fn inst elabindex ledger warnings config)))
    (booleanp successp))
  :rule-classes :type-prescription)

Theorem: vl-warninglist-p-of-vl-unparam-inst.warnings

(defthm vl-warninglist-p-of-vl-unparam-inst.warnings
  (b* (((mv ?successp ?warnings
            ?inst ?instkey ?new-elabindex ?ledger)
        (vl-unparam-inst-fn inst elabindex ledger warnings config)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-modinst-p-of-vl-unparam-inst.inst

(defthm vl-modinst-p-of-vl-unparam-inst.inst
  (b* (((mv ?successp ?warnings
            ?inst ?instkey ?new-elabindex ?ledger)
        (vl-unparam-inst-fn inst elabindex ledger warnings config)))
    (vl-modinst-p inst))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-unparam-inst.instkey

(defthm return-type-of-vl-unparam-inst.instkey
  (b* (((mv ?successp ?warnings
            ?inst ?instkey ?new-elabindex ?ledger)
        (vl-unparam-inst-fn inst elabindex ledger warnings config)))
    (implies successp
             (vl-unparam-instkey-p instkey)))
  :rule-classes :rewrite)

Theorem: vl-unparam-ledger-p-of-vl-unparam-inst.ledger

(defthm vl-unparam-ledger-p-of-vl-unparam-inst.ledger
  (b* (((mv ?successp ?warnings
            ?inst ?instkey ?new-elabindex ?ledger)
        (vl-unparam-inst-fn inst elabindex ledger warnings config)))
    (vl-unparam-ledger-p ledger))
  :rule-classes :rewrite)

Theorem: vl-unparam-inst-fn-of-vl-modinst-fix-inst

(defthm vl-unparam-inst-fn-of-vl-modinst-fix-inst
 (equal (vl-unparam-inst-fn (vl-modinst-fix inst)
                            elabindex ledger warnings config)
        (vl-unparam-inst-fn inst elabindex ledger warnings config)))

Theorem: vl-unparam-inst-fn-vl-modinst-equiv-congruence-on-inst

(defthm vl-unparam-inst-fn-vl-modinst-equiv-congruence-on-inst
 (implies
   (vl-modinst-equiv inst inst-equiv)
   (equal (vl-unparam-inst-fn inst elabindex ledger warnings config)
          (vl-unparam-inst-fn inst-equiv
                              elabindex ledger warnings config)))
 :rule-classes :congruence)

Theorem: vl-unparam-inst-fn-of-vl-unparam-ledger-fix-ledger

(defthm vl-unparam-inst-fn-of-vl-unparam-ledger-fix-ledger
 (equal (vl-unparam-inst-fn inst
                            elabindex (vl-unparam-ledger-fix ledger)
                            warnings config)
        (vl-unparam-inst-fn inst elabindex ledger warnings config)))

Theorem: vl-unparam-inst-fn-vl-unparam-ledger-equiv-congruence-on-ledger

(defthm
    vl-unparam-inst-fn-vl-unparam-ledger-equiv-congruence-on-ledger
 (implies
   (vl-unparam-ledger-equiv ledger ledger-equiv)
   (equal (vl-unparam-inst-fn inst elabindex ledger warnings config)
          (vl-unparam-inst-fn inst elabindex
                              ledger-equiv warnings config)))
 :rule-classes :congruence)

Theorem: vl-unparam-inst-fn-of-vl-warninglist-fix-warnings

(defthm vl-unparam-inst-fn-of-vl-warninglist-fix-warnings
 (equal (vl-unparam-inst-fn inst elabindex
                            ledger (vl-warninglist-fix warnings)
                            config)
        (vl-unparam-inst-fn inst elabindex ledger warnings config)))

Theorem: vl-unparam-inst-fn-vl-warninglist-equiv-congruence-on-warnings

(defthm
     vl-unparam-inst-fn-vl-warninglist-equiv-congruence-on-warnings
 (implies
   (vl-warninglist-equiv warnings warnings-equiv)
   (equal (vl-unparam-inst-fn inst elabindex ledger warnings config)
          (vl-unparam-inst-fn inst elabindex
                              ledger warnings-equiv config)))
 :rule-classes :congruence)

Theorem: vl-unparam-inst-fn-of-vl-simpconfig-fix-config

(defthm vl-unparam-inst-fn-of-vl-simpconfig-fix-config
 (equal (vl-unparam-inst-fn inst elabindex ledger
                            warnings (vl-simpconfig-fix config))
        (vl-unparam-inst-fn inst elabindex ledger warnings config)))

Theorem: vl-unparam-inst-fn-vl-simpconfig-equiv-congruence-on-config

(defthm vl-unparam-inst-fn-vl-simpconfig-equiv-congruence-on-config
 (implies
   (vl-simpconfig-equiv config config-equiv)
   (equal (vl-unparam-inst-fn inst elabindex ledger warnings config)
          (vl-unparam-inst-fn inst elabindex
                              ledger warnings config-equiv)))
 :rule-classes :congruence)