• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Community
  • 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-scopeinfo-resolve-params

Signature

(vl-scopeinfo-resolve-params x scopeinfo elabindex outer-ss 
                             outer-scope-path final-params-acc 
                             warnings &key (config 'config)) 
 
  → 
(mv successp warnings final-params elabindex)

Arguments

x — Guard (vl-paramdecloverridelist-p x).

scopeinfo — Represents the module scope.
    Guard (vl-scopeinfo-p scopeinfo).

elabindex — Scoped in the module whose parameters we're overriding. However, the SS in this elabindex is at the global level, and we always push the scopeinfo onto the top of it before using it. This is a bad breakage of the elabindex abstraction, but before changing this we'd need to think hard about how parameter values and types are resolved.

outer-ss — Scope of the overrides -- read-only.
    Guard (vl-scopestack-p outer-ss).

outer-scope-path — How to get to the scopes for the override context.
    Guard (vl-elabtraversal-p outer-scope-path).

final-params-acc — Guard (vl-paramdecllist-p final-params-acc).

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

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

Returns

successp — BOZO at the moment this never actually fails.

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

final-params — Type (vl-paramdecllist-p final-params).

elabindex — with parameters resolved.

Definitions and Theorems

Function: vl-scopeinfo-resolve-params-fn

(defun vl-scopeinfo-resolve-params-fn
       (x scopeinfo
          elabindex outer-ss outer-scope-path
          final-params-acc warnings config)
 (declare (xargs :stobjs (elabindex)))
 (declare (xargs :guard (and (vl-paramdecloverridelist-p x)
                             (vl-scopeinfo-p scopeinfo)
                             (vl-scopestack-p outer-ss)
                             (vl-elabtraversal-p outer-scope-path)
                             (vl-paramdecllist-p final-params-acc)
                             (vl-warninglist-p warnings)
                             (vl-simpconfig-p config))))
 (let ((__function__ 'vl-scopeinfo-resolve-params))
  (declare (ignorable __function__))
  (b*
   ((outside-module-ss (vl-elabindex->ss))
    (elabindex (vl-elabindex-update-ss
                    (vl-scopestack-push (vl-scopeinfo-fix scopeinfo)
                                        outside-module-ss)
                    elabindex))
    ((when (atom x))
     (mv t (ok)
         (revappend-without-guard
              (vl-paramdecllist-fix final-params-acc)
              nil)
         elabindex))
    ((vl-paramdecloverride x1) (car x))
    (warnings (ok))
    ((mv ok warnings final-paramdecl elabindex)
     (vl-override-parameter x1.decl elabindex x1.override
                            outer-ss outer-scope-path warnings))
    ((vl-scopeinfo scopeinfo))
    (new-scopeinfo
      (if ok
       (change-vl-scopeinfo
            scopeinfo
            :locals (hons-acons (vl-paramdecl->name final-paramdecl)
                                final-paramdecl scopeinfo.locals))
       scopeinfo))
    (elabindex
         (vl-elabindex-update-ss outside-module-ss elabindex)))
   (vl-scopeinfo-resolve-params
        (cdr x)
        new-scopeinfo
        elabindex outer-ss outer-scope-path
        (cons final-paramdecl final-params-acc)
        warnings))))

Theorem: vl-warninglist-p-of-vl-scopeinfo-resolve-params.warnings

(defthm vl-warninglist-p-of-vl-scopeinfo-resolve-params.warnings
  (b* (((mv ?successp
            ?warnings ?final-params ?elabindex)
        (vl-scopeinfo-resolve-params-fn
             x scopeinfo
             elabindex outer-ss outer-scope-path
             final-params-acc warnings config)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-paramdecllist-p-of-vl-scopeinfo-resolve-params.final-params

(defthm
     vl-paramdecllist-p-of-vl-scopeinfo-resolve-params.final-params
  (b* (((mv ?successp
            ?warnings ?final-params ?elabindex)
        (vl-scopeinfo-resolve-params-fn
             x scopeinfo
             elabindex outer-ss outer-scope-path
             final-params-acc warnings config)))
    (vl-paramdecllist-p final-params))
  :rule-classes :rewrite)

Theorem: vl-scopeinfo-resolve-params-fn-of-vl-paramdecloverridelist-fix-x

(defthm
   vl-scopeinfo-resolve-params-fn-of-vl-paramdecloverridelist-fix-x
  (equal (vl-scopeinfo-resolve-params-fn
              (vl-paramdecloverridelist-fix x)
              scopeinfo
              elabindex outer-ss outer-scope-path
              final-params-acc warnings config)
         (vl-scopeinfo-resolve-params-fn
              x scopeinfo
              elabindex outer-ss outer-scope-path
              final-params-acc warnings config)))

Theorem: vl-scopeinfo-resolve-params-fn-vl-paramdecloverridelist-equiv-congruence-on-x

(defthm
 vl-scopeinfo-resolve-params-fn-vl-paramdecloverridelist-equiv-congruence-on-x
 (implies (vl-paramdecloverridelist-equiv x x-equiv)
          (equal (vl-scopeinfo-resolve-params-fn
                      x scopeinfo
                      elabindex outer-ss outer-scope-path
                      final-params-acc warnings config)
                 (vl-scopeinfo-resolve-params-fn
                      x-equiv scopeinfo
                      elabindex outer-ss outer-scope-path
                      final-params-acc warnings config)))
 :rule-classes :congruence)

Theorem: vl-scopeinfo-resolve-params-fn-of-vl-scopeinfo-fix-scopeinfo

(defthm vl-scopeinfo-resolve-params-fn-of-vl-scopeinfo-fix-scopeinfo
  (equal (vl-scopeinfo-resolve-params-fn
              x (vl-scopeinfo-fix scopeinfo)
              elabindex outer-ss outer-scope-path
              final-params-acc warnings config)
         (vl-scopeinfo-resolve-params-fn
              x scopeinfo
              elabindex outer-ss outer-scope-path
              final-params-acc warnings config)))

Theorem: vl-scopeinfo-resolve-params-fn-vl-scopeinfo-equiv-congruence-on-scopeinfo

(defthm
 vl-scopeinfo-resolve-params-fn-vl-scopeinfo-equiv-congruence-on-scopeinfo
 (implies (vl-scopeinfo-equiv scopeinfo scopeinfo-equiv)
          (equal (vl-scopeinfo-resolve-params-fn
                      x scopeinfo
                      elabindex outer-ss outer-scope-path
                      final-params-acc warnings config)
                 (vl-scopeinfo-resolve-params-fn
                      x scopeinfo-equiv
                      elabindex outer-ss outer-scope-path
                      final-params-acc warnings config)))
 :rule-classes :congruence)

Theorem: vl-scopeinfo-resolve-params-fn-of-vl-scopestack-fix-outer-ss

(defthm vl-scopeinfo-resolve-params-fn-of-vl-scopestack-fix-outer-ss
  (equal (vl-scopeinfo-resolve-params-fn
              x scopeinfo
              elabindex (vl-scopestack-fix outer-ss)
              outer-scope-path
              final-params-acc warnings config)
         (vl-scopeinfo-resolve-params-fn
              x scopeinfo
              elabindex outer-ss outer-scope-path
              final-params-acc warnings config)))

Theorem: vl-scopeinfo-resolve-params-fn-vl-scopestack-equiv-congruence-on-outer-ss

(defthm
 vl-scopeinfo-resolve-params-fn-vl-scopestack-equiv-congruence-on-outer-ss
 (implies (vl-scopestack-equiv outer-ss outer-ss-equiv)
          (equal (vl-scopeinfo-resolve-params-fn
                      x scopeinfo
                      elabindex outer-ss outer-scope-path
                      final-params-acc warnings config)
                 (vl-scopeinfo-resolve-params-fn
                      x scopeinfo elabindex
                      outer-ss-equiv outer-scope-path
                      final-params-acc warnings config)))
 :rule-classes :congruence)

Theorem: vl-scopeinfo-resolve-params-fn-of-vl-elabtraversal-fix-outer-scope-path

(defthm
 vl-scopeinfo-resolve-params-fn-of-vl-elabtraversal-fix-outer-scope-path
 (equal (vl-scopeinfo-resolve-params-fn
             x scopeinfo elabindex outer-ss
             (vl-elabtraversal-fix outer-scope-path)
             final-params-acc warnings config)
        (vl-scopeinfo-resolve-params-fn
             x scopeinfo
             elabindex outer-ss outer-scope-path
             final-params-acc warnings config)))

Theorem: vl-scopeinfo-resolve-params-fn-vl-elabtraversal-equiv-congruence-on-outer-scope-path

(defthm
 vl-scopeinfo-resolve-params-fn-vl-elabtraversal-equiv-congruence-on-outer-scope-path
 (implies
    (vl-elabtraversal-equiv outer-scope-path outer-scope-path-equiv)
    (equal (vl-scopeinfo-resolve-params-fn
                x scopeinfo
                elabindex outer-ss outer-scope-path
                final-params-acc warnings config)
           (vl-scopeinfo-resolve-params-fn
                x scopeinfo elabindex
                outer-ss outer-scope-path-equiv
                final-params-acc warnings config)))
 :rule-classes :congruence)

Theorem: vl-scopeinfo-resolve-params-fn-of-vl-paramdecllist-fix-final-params-acc

(defthm
 vl-scopeinfo-resolve-params-fn-of-vl-paramdecllist-fix-final-params-acc
 (equal (vl-scopeinfo-resolve-params-fn
             x scopeinfo
             elabindex outer-ss outer-scope-path
             (vl-paramdecllist-fix final-params-acc)
             warnings config)
        (vl-scopeinfo-resolve-params-fn
             x scopeinfo
             elabindex outer-ss outer-scope-path
             final-params-acc warnings config)))

Theorem: vl-scopeinfo-resolve-params-fn-vl-paramdecllist-equiv-congruence-on-final-params-acc

(defthm
 vl-scopeinfo-resolve-params-fn-vl-paramdecllist-equiv-congruence-on-final-params-acc
 (implies
    (vl-paramdecllist-equiv final-params-acc final-params-acc-equiv)
    (equal (vl-scopeinfo-resolve-params-fn
                x scopeinfo
                elabindex outer-ss outer-scope-path
                final-params-acc warnings config)
           (vl-scopeinfo-resolve-params-fn
                x scopeinfo elabindex outer-ss
                outer-scope-path final-params-acc-equiv
                warnings config)))
 :rule-classes :congruence)

Theorem: vl-scopeinfo-resolve-params-fn-of-vl-warninglist-fix-warnings

(defthm
      vl-scopeinfo-resolve-params-fn-of-vl-warninglist-fix-warnings
 (equal
   (vl-scopeinfo-resolve-params-fn x scopeinfo elabindex outer-ss
                                   outer-scope-path final-params-acc
                                   (vl-warninglist-fix warnings)
                                   config)
   (vl-scopeinfo-resolve-params-fn
        x scopeinfo
        elabindex outer-ss outer-scope-path
        final-params-acc warnings config)))

Theorem: vl-scopeinfo-resolve-params-fn-vl-warninglist-equiv-congruence-on-warnings

(defthm
 vl-scopeinfo-resolve-params-fn-vl-warninglist-equiv-congruence-on-warnings
 (implies
  (vl-warninglist-equiv warnings warnings-equiv)
  (equal
   (vl-scopeinfo-resolve-params-fn
        x scopeinfo
        elabindex outer-ss outer-scope-path
        final-params-acc warnings config)
   (vl-scopeinfo-resolve-params-fn x scopeinfo elabindex outer-ss
                                   outer-scope-path final-params-acc
                                   warnings-equiv config)))
 :rule-classes :congruence)

Theorem: vl-scopeinfo-resolve-params-fn-of-vl-simpconfig-fix-config

(defthm vl-scopeinfo-resolve-params-fn-of-vl-simpconfig-fix-config
  (equal (vl-scopeinfo-resolve-params-fn
              x scopeinfo elabindex outer-ss
              outer-scope-path final-params-acc
              warnings (vl-simpconfig-fix config))
         (vl-scopeinfo-resolve-params-fn
              x scopeinfo
              elabindex outer-ss outer-scope-path
              final-params-acc warnings config)))

Theorem: vl-scopeinfo-resolve-params-fn-vl-simpconfig-equiv-congruence-on-config

(defthm
 vl-scopeinfo-resolve-params-fn-vl-simpconfig-equiv-congruence-on-config
 (implies
  (vl-simpconfig-equiv config config-equiv)
  (equal
   (vl-scopeinfo-resolve-params-fn
        x scopeinfo
        elabindex outer-ss outer-scope-path
        final-params-acc warnings config)
   (vl-scopeinfo-resolve-params-fn x scopeinfo elabindex outer-ss
                                   outer-scope-path final-params-acc
                                   warnings config-equiv)))
 :rule-classes :congruence)