• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Community
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
      • Transforms
        • Expression-sizing
        • Occform
        • Oprewrite
        • Expand-functions
        • Delayredux
        • Unparameterization
          • Scopesubst
          • Vl-scopeinfo-resolve-params
          • Vl-make-paramdecloverrides
          • Vl-unparam-inst
          • Vl-scope-finalize-params
          • Vl-override-parameter-value
          • Vl-unparam-instlist
          • Vl-create-unparameterized-module
          • Vl-module-default-signature
          • Vl-modulelist-default-signatures
          • Vl-gencase-some-match
          • Vl-gencase-match
          • Vl-make-paramdecloverrides-named
          • Vl-unparam-newname
          • Vl-paramdecl-set-default
          • Vl-unparam-signature
          • Vl-genblob-collect-modinst-paramsigs
          • Vl-design-unparameterize
          • Vl-paramdecllist-remove-defaults
          • Vl-unparam-newname-exprstring
          • Vl-paramdecl-remove-default
          • Vl-unparam-sigalist
          • Vl-unparam-signaturelist
        • Caseelim
        • Split
        • Selresolve
        • Weirdint-elim
        • Vl-delta
        • Replicate-insts
        • Rangeresolve
        • Propagate
        • Clean-selects
        • Clean-params
        • Blankargs
        • Inline-mods
        • Expr-simp
        • Trunc
        • Always-top
        • Gatesplit
        • Gate-elim
        • Expression-optimization
        • Elim-supplies
        • Wildelim
        • Drop-blankports
        • Clean-warnings
        • Addinstnames
        • Custom-transform-hooks
        • Annotate
        • Latchcode
        • Elim-unused-vars
        • Problem-modules
      • Lint
      • Mlib
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Unparameterization

Vl-scopeinfo-resolve-params

Signature

(vl-scopeinfo-resolve-params x scopeinfo 
                             ss final-params-acc warnings ctx) 
 
  → 
(mv successp warnings new-scopeinfo final-params)

Arguments

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

scopeinfo — Guard (vl-scopeinfo-p scopeinfo).

ss — Guard (vl-scopestack-p ss).

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

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

ctx — Guard (vl-context-p ctx).

Returns

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

new-scopeinfo — input scopeinfo modified with final parameter values.
    Type (vl-scopeinfo-p new-scopeinfo).

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

Definitions and Theorems

Function: vl-scopeinfo-resolve-params

(defun vl-scopeinfo-resolve-params
       (x scopeinfo
          ss final-params-acc warnings ctx)
 (declare (xargs :guard (and (vl-paramdecloverridelist-p x)
                             (vl-scopeinfo-p scopeinfo)
                             (vl-scopestack-p ss)
                             (vl-paramdecllist-p final-params-acc)
                             (vl-warninglist-p warnings)
                             (vl-context-p ctx))))
 (let ((__function__ 'vl-scopeinfo-resolve-params))
  (declare (ignorable __function__))
  (b*
   (((when (atom x))
     (mv t (ok)
         (vl-scopeinfo-fix scopeinfo)
         (revappend-without-guard
              (vl-paramdecllist-fix final-params-acc)
              nil)))
    ((vl-paramdecloverride x1) (car x))
    (current-ss (vl-scopestack-push (vl-scopeinfo-fix scopeinfo)
                                    ss))
    (subst-decl (vl-paramdecl-scopesubst x1.decl current-ss))
    (ov-value
       (or x1.override
           (vl-paramtype->default (vl-paramdecl->type subst-decl))))
    ((unless ov-value)
     (mv nil
         (fatal :type :vl-bad-inst
                :msg "~a0: no value for parameter ~s1."
                :args (list (vl-context-fix ctx)
                            (vl-paramdecl->name x1.decl)))
         (vl-scopeinfo-fix scopeinfo)
         nil))
    ((mv ok warnings final-value)
     (vl-override-parameter-value subst-decl
                                  ov-value current-ss warnings ctx))
    ((unless ok)
     (mv nil
         warnings (vl-scopeinfo-fix scopeinfo)
         nil))
    ((mv ok final-paramdecl)
     (vl-paramdecl-set-default subst-decl final-value))
    ((unless ok)
     (mv
      nil
      (warn
       :type :vl-programming-error
       :msg
       "~a0: Tried to set the value of an type/value ~
                        parameter ~a1 as value/type ~a2"
       :args (list (vl-context-fix ctx)
                   x1.decl final-value))
      (vl-scopeinfo-fix scopeinfo)
      nil))
    ((vl-scopeinfo scopeinfo))
    (new-scopeinfo
       (change-vl-scopeinfo
            scopeinfo
            :locals (hons-acons (vl-paramdecl->name final-paramdecl)
                                final-paramdecl scopeinfo.locals))))
   (vl-scopeinfo-resolve-params
        (cdr x)
        new-scopeinfo ss
        (cons final-paramdecl final-params-acc)
        warnings ctx))))

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

(defthm vl-warninglist-p-of-vl-scopeinfo-resolve-params.warnings
 (b*
  (((mv ?successp
        ?warnings ?new-scopeinfo ?final-params)
    (vl-scopeinfo-resolve-params x scopeinfo
                                 ss final-params-acc warnings ctx)))
  (vl-warninglist-p warnings))
 :rule-classes :rewrite)

Theorem: vl-scopeinfo-p-of-vl-scopeinfo-resolve-params.new-scopeinfo

(defthm vl-scopeinfo-p-of-vl-scopeinfo-resolve-params.new-scopeinfo
 (b*
  (((mv ?successp
        ?warnings ?new-scopeinfo ?final-params)
    (vl-scopeinfo-resolve-params x scopeinfo
                                 ss final-params-acc warnings ctx)))
  (vl-scopeinfo-p new-scopeinfo))
 :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 ?new-scopeinfo ?final-params)
    (vl-scopeinfo-resolve-params x scopeinfo
                                 ss final-params-acc warnings ctx)))
  (vl-paramdecllist-p final-params))
 :rule-classes :rewrite)

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

(defthm
      vl-scopeinfo-resolve-params-of-vl-paramdecloverridelist-fix-x
 (equal
    (vl-scopeinfo-resolve-params (vl-paramdecloverridelist-fix x)
                                 scopeinfo
                                 ss final-params-acc warnings ctx)
    (vl-scopeinfo-resolve-params x scopeinfo
                                 ss final-params-acc warnings ctx)))

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

(defthm
 vl-scopeinfo-resolve-params-vl-paramdecloverridelist-equiv-congruence-on-x
 (implies
  (vl-paramdecloverridelist-equiv x x-equiv)
  (equal
    (vl-scopeinfo-resolve-params x scopeinfo
                                 ss final-params-acc warnings ctx)
    (vl-scopeinfo-resolve-params x-equiv scopeinfo
                                 ss final-params-acc warnings ctx)))
 :rule-classes :congruence)

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

(defthm vl-scopeinfo-resolve-params-of-vl-scopeinfo-fix-scopeinfo
 (equal
    (vl-scopeinfo-resolve-params x (vl-scopeinfo-fix scopeinfo)
                                 ss final-params-acc warnings ctx)
    (vl-scopeinfo-resolve-params x scopeinfo
                                 ss final-params-acc warnings ctx)))

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

(defthm
 vl-scopeinfo-resolve-params-vl-scopeinfo-equiv-congruence-on-scopeinfo
 (implies
  (vl-scopeinfo-equiv scopeinfo scopeinfo-equiv)
  (equal
    (vl-scopeinfo-resolve-params x scopeinfo
                                 ss final-params-acc warnings ctx)
    (vl-scopeinfo-resolve-params x scopeinfo-equiv
                                 ss final-params-acc warnings ctx)))
 :rule-classes :congruence)

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

(defthm vl-scopeinfo-resolve-params-of-vl-scopestack-fix-ss
 (equal
    (vl-scopeinfo-resolve-params x scopeinfo (vl-scopestack-fix ss)
                                 final-params-acc warnings ctx)
    (vl-scopeinfo-resolve-params x scopeinfo
                                 ss final-params-acc warnings ctx)))

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

(defthm
   vl-scopeinfo-resolve-params-vl-scopestack-equiv-congruence-on-ss
 (implies
  (vl-scopestack-equiv ss ss-equiv)
  (equal
      (vl-scopeinfo-resolve-params x scopeinfo
                                   ss final-params-acc warnings ctx)
      (vl-scopeinfo-resolve-params x scopeinfo ss-equiv
                                   final-params-acc warnings ctx)))
 :rule-classes :congruence)

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

(defthm
 vl-scopeinfo-resolve-params-of-vl-paramdecllist-fix-final-params-acc
 (equal
    (vl-scopeinfo-resolve-params
         x scopeinfo ss
         (vl-paramdecllist-fix final-params-acc)
         warnings ctx)
    (vl-scopeinfo-resolve-params x scopeinfo
                                 ss final-params-acc warnings ctx)))

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

(defthm
 vl-scopeinfo-resolve-params-vl-paramdecllist-equiv-congruence-on-final-params-acc
 (implies
  (vl-paramdecllist-equiv final-params-acc final-params-acc-equiv)
  (equal
      (vl-scopeinfo-resolve-params x scopeinfo
                                   ss final-params-acc warnings ctx)
      (vl-scopeinfo-resolve-params
           x scopeinfo ss
           final-params-acc-equiv warnings ctx)))
 :rule-classes :congruence)

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

(defthm vl-scopeinfo-resolve-params-of-vl-warninglist-fix-warnings
 (equal
    (vl-scopeinfo-resolve-params x scopeinfo ss final-params-acc
                                 (vl-warninglist-fix warnings)
                                 ctx)
    (vl-scopeinfo-resolve-params x scopeinfo
                                 ss final-params-acc warnings ctx)))

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

(defthm
 vl-scopeinfo-resolve-params-vl-warninglist-equiv-congruence-on-warnings
 (implies
  (vl-warninglist-equiv warnings warnings-equiv)
  (equal
      (vl-scopeinfo-resolve-params x scopeinfo
                                   ss final-params-acc warnings ctx)
      (vl-scopeinfo-resolve-params
           x scopeinfo ss
           final-params-acc warnings-equiv ctx)))
 :rule-classes :congruence)

Theorem: vl-scopeinfo-resolve-params-of-vl-context-fix-ctx

(defthm vl-scopeinfo-resolve-params-of-vl-context-fix-ctx
 (equal
    (vl-scopeinfo-resolve-params x scopeinfo ss final-params-acc
                                 warnings (vl-context-fix ctx))
    (vl-scopeinfo-resolve-params x scopeinfo
                                 ss final-params-acc warnings ctx)))

Theorem: vl-scopeinfo-resolve-params-vl-context-equiv-congruence-on-ctx

(defthm
     vl-scopeinfo-resolve-params-vl-context-equiv-congruence-on-ctx
 (implies
  (vl-context-equiv ctx ctx-equiv)
  (equal
      (vl-scopeinfo-resolve-params x scopeinfo
                                   ss final-params-acc warnings ctx)
      (vl-scopeinfo-resolve-params
           x scopeinfo ss
           final-params-acc warnings ctx-equiv)))
 :rule-classes :congruence)