• 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)