• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • Vl
      • Syntax
      • Loader
      • Warnings
      • Getting-started
      • Utilities
      • Printer
      • Kit
      • Mlib
      • Transforms
        • Unparameterization
        • Elaborate
          • Elabindex
          • Vl-override-parameter
            • Vl-convert-parameter-value-to-explicit-type
          • Vl-genblob-elaborate
          • Vl-modelement-elaborate
          • Vl-design-elaborate-aux
          • Vl-package-elaborate-aux
          • Vl-taskdecl-elaborate
          • Vl-clkdecl-elaborate
          • Vl-defaultdisablelist-elaborate
          • Vl-modport-portlist-elaborate
          • Vl-modinst-elaborate-aux
          • Vl-maybe-parse-temps-elaborate
          • Vl-ansi-portdecllist-elaborate
          • Vl-ansi-portdecl-elaborate
          • Vl-parse-temps-elaborate
          • Vl-dpiimportlist-elaborate
          • Vl-clkassignlist-elaborate
          • Vl-cassertionlist-elaborate
          • Vl-assertionlist-elaborate
          • Vl-taskdecllist-elaborate
          • Vl-sequencelist-elaborate
          • Vl-propportlist-elaborate
          • Vl-propertylist-elaborate
          • Vl-plainarglist-elaborate
          • Vl-namedarglist-elaborate
          • Vl-maybe-clkskew-elaborate
          • Vl-gclkdecllist-elaborate
          • Vl-gateinstlist-elaborate
          • Vl-elabtasklist-elaborate
          • Vl-defaultdisable-elaborate
          • Vl-sequence-elaborate
          • Vl-property-elaborate
          • Vl-modportlist-elaborate
          • Vl-modport-port-elaborate
          • Vl-modinstlist-elaborate
          • Vl-letdecllist-elaborate
          • Vl-interfaceport-elaborate
          • Vl-initiallist-elaborate
          • Vl-gateinst-elaborate
          • Vl-fundecllist-elaborate
          • Vl-clkdecllist-elaborate
          • Vl-assignlist-elaborate
          • Vl-assign-elaborate-aux
          • Vl-arguments-elaborate
          • Vl-alwayslist-elaborate
          • Vl-regularport-elaborate
          • Vl-portlist-elaborate
          • Vl-finallist-elaborate
          • Vl-dpiimport-elaborate
          • Vl-clkassign-elaborate
          • Vl-bindlist-elaborate
          • Vl-aliaslist-elaborate
          • Vl-warn-about-negative-indices
          • Vl-udplist-elaborate
          • Vl-propport-elaborate
          • Vl-modinst-elaborate
          • Vl-udp-elaborate
          • Vl-port-elaborate
          • Vl-plainarg-elaborate
          • Vl-namedarg-elaborate
          • Vl-modport-elaborate
          • Vl-gclkdecl-elaborate
          • Vl-elabtask-elaborate
          • Vl-clkskew-elaborate
          • Vl-assign-elaborate
          • Vl-always-elaborate-aux
          • Vl-always-elaborate
          • Vl-alias-elaborate
          • Vl-initial-elaborate
          • Vl-bind-elaborate
          • Vl-final-elaborate
          • Vl-fundecl-paramdecls-for-const-args
          • Vl-fundecl-body-with-const-args
          • Vl-exprlist-args-to-4vec-consts
          • Sv::svex-constval
        • Addnames
        • Annotate
        • Clean-warnings
        • Eliminitial
        • Custom-transform-hooks
        • Problem-modules
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Elaborate

Vl-override-parameter

Try to override a parameter with a new expression.

Signature

(vl-override-parameter decl 
                       elabindex override ov-ss ov-scope-path 
                       warnings &key (config 'config)) 
 
  → 
(mv okp warnings new-param new-elabindex)

Arguments

decl — Some parameter from the submodule.
    Guard (vl-paramdecl-p decl).

elabindex — In the declaration scope.

override — The value to override this parameter with, if any -- should be elaborated already.
    Guard (vl-maybe-paramvalue-p override).

ov-ss — Scopestack for the override context.
    Guard (vl-scopestack-p ov-ss).

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

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

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

Returns

okp — Type (booleanp okp).

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

new-param — On success, final (coerced) value to use for this parameter.
    Type (vl-paramdecl-p new-param).

new-elabindex — updated svexconf for paramdecl context.

Definitions and Theorems

Function: vl-override-parameter-fn

(defun vl-override-parameter-fn
       (decl elabindex override
             ov-ss ov-scope-path warnings config)
 (declare (xargs :stobjs (elabindex)))
 (declare (xargs :guard (and (vl-paramdecl-p decl)
                             (vl-maybe-paramvalue-p override)
                             (vl-scopestack-p ov-ss)
                             (vl-elabtraversal-p ov-scope-path)
                             (vl-warninglist-p warnings)
                             (vl-simpconfig-p config))))
 (let ((__function__ 'vl-override-parameter))
  (declare (ignorable __function__))
  (b* (((vl-paramdecl decl)
        (vl-paramdecl-fix decl))
       (warnings (ok))
       ((vl-simpconfig config))
       ((wmv ok warnings decl.type elabindex)
        (vl-paramtype-elaborate decl.type elabindex
                                :reclimit config.elab-limit))
       (elabindex (vl-elabindex-sync-scopes))
       (scopes1 (vl-elabindex->scopes))
       (ov-scopes (vl-elabscopes-traverse ov-scope-path scopes1))
       ((unless ok)
        (mv nil warnings decl elabindex)))
   (vl-paramtype-case
    decl.type
    (:vl-typeparam
     (b*
      (((unless override)
        (b*
         (((unless decl.type.default)
           (mv
            nil
            (fatal
             :type :vl-bad-parameter-override
             :msg
             "Can't instantiate without assignment ~
                                    for type parameter ~a1."
             :args (list nil decl))
            decl elabindex))
          ((unless (vl-datatype-resolved-p decl.type.default))
           (mv
            nil
            (fatal
                 :type :vl-bad-parameter-override
                 :msg "Default type for parameter ~a1 not resolved."
                 :args (list nil decl))
            decl elabindex)))
         (mv t (ok)
             (change-vl-paramdecl decl
                                  :type decl.type)
             elabindex)))
       ((when (vl-paramvalue-case override :expr))
        (mv
         nil
         (fatal
           :type :vl-bad-parameter-override
           :msg "Overriding type parameter ~a1 with expression ~a2."
           :args (list nil decl
                       (vl-paramvalue-expr->expr override)))
         decl elabindex))
       (type (vl-paramvalue-type->type override))
       ((unless (vl-datatype-resolved-p type))
        (mv
         nil
         (fatal
            :type :vl-bad-parameter-override
            :msg "Override type ~a1 for parameter ~a2 not resolved."
            :args (list nil type decl))
         decl elabindex)))
      (mv t warnings
          (change-vl-paramdecl
               decl
               :type (change-vl-typeparam decl.type
                                          :default type)
               :overriddenp t)
          elabindex)))
    (:vl-explicitvalueparam
     (b*
      (((when (and override
                   (vl-paramvalue-case override :type)))
        (mv
         nil
         (fatal :type :vl-bad-parameter-override
                :msg "Overriding value parameter ~a1 with type ~a2."
                :args (list nil decl
                            (vl-paramvalue-type->type override)))
         decl elabindex))
       ((mv expr expr-ss expr-scopes)
        (if override (mv (vl-paramvalue-expr->expr override)
                         ov-ss ov-scopes)
          (mv decl.type.default (vl-elabindex->ss)
              (vl-elabindex->scopes))))
       ((unless expr)
        (mv
         nil
         (fatal
          :type :vl-bad-parameter-override
          :msg
          "Can't instantiate without assignment for ~
                              value parameter ~a1."
          :args (list nil decl))
         decl elabindex))
       ((unless (vl-datatype-resolved-p decl.type.type))
        (mv
         nil
         (fatal
             :type :vl-bad-parameter-override
             :msg "Failed to resolve datatype ~a1 for parameter ~a2"
             :args (list nil decl.type.type decl))
         decl elabindex))
       ((mv okp warnings coerced-expr)
        (vl-convert-parameter-value-to-explicit-type
             decl.type.type expr
             expr-ss expr-scopes warnings decl.name))
       ((unless okp)
        (mv nil warnings decl elabindex))
       (new-decl
        (change-vl-paramdecl
          decl
          :type (change-vl-explicitvalueparam decl.type
                                              :default coerced-expr)
          :overriddenp (and override t))))
      (vl-unparam-debug
           "successfully overriding value parameter ~a1 with ~a2.~%"
           nil decl coerced-expr)
      (mv t (ok) new-decl elabindex)))
    (:vl-implicitvalueparam
     (b*
      (((when (and override
                   (vl-paramvalue-case override :type)))
        (mv
         nil
         (fatal :type :vl-bad-parameter-override
                :msg "Overriding value parameter ~a1 with type ~a2."
                :args (list nil decl
                            (vl-paramvalue-type->type override)))
         decl elabindex))
       ((mv expr expr-ss expr-scopes)
        (if override (mv (vl-paramvalue-expr->expr override)
                         ov-ss ov-scopes)
          (mv decl.type.default (vl-elabindex->ss)
              (vl-elabindex->scopes))))
       ((unless expr)
        (mv
         nil
         (fatal
          :type :vl-bad-parameter-override
          :msg
          "Can't instantiate without assignment for ~
                              value parameter ~a1."
          :args (list nil decl))
         decl elabindex))
       ((wmv warnings err datatype)
        (vl-implicitvalueparam-final-type
             decl.type expr expr-ss expr-scopes))
       ((when err)
        (mv
         nil
         (fatal
          :type :vl-bad-parameter-override
          :msg
          "Failed to determine datatype for parameter ~
                              ~a1 overridden with ~a2: ~@3"
          :args (list nil decl expr err))
         decl elabindex))
       ((mv okp warnings coerced-expr)
        (vl-convert-parameter-value-to-explicit-type
             datatype expr
             expr-ss expr-scopes warnings decl.name))
       ((unless okp)
        (mv nil warnings decl elabindex))
       (new-decl
        (change-vl-paramdecl
            decl
            :type (make-vl-explicitvalueparam :type datatype
                                              :default coerced-expr)
            :overriddenp (and override t))))
      (vl-unparam-debug "successfully overriding ~a1 with ~a2.~%"
                        nil decl coerced-expr)
      (mv t (ok) new-decl elabindex)))))))

Theorem: booleanp-of-vl-override-parameter.okp

(defthm booleanp-of-vl-override-parameter.okp
 (b*
  (((mv ?okp
        ?warnings ?new-param ?new-elabindex)
    (vl-override-parameter-fn decl elabindex override
                              ov-ss ov-scope-path warnings config)))
  (booleanp okp))
 :rule-classes :type-prescription)

Theorem: vl-warninglist-p-of-vl-override-parameter.warnings

(defthm vl-warninglist-p-of-vl-override-parameter.warnings
 (b*
  (((mv ?okp
        ?warnings ?new-param ?new-elabindex)
    (vl-override-parameter-fn decl elabindex override
                              ov-ss ov-scope-path warnings config)))
  (vl-warninglist-p warnings))
 :rule-classes :rewrite)

Theorem: vl-paramdecl-p-of-vl-override-parameter.new-param

(defthm vl-paramdecl-p-of-vl-override-parameter.new-param
 (b*
  (((mv ?okp
        ?warnings ?new-param ?new-elabindex)
    (vl-override-parameter-fn decl elabindex override
                              ov-ss ov-scope-path warnings config)))
  (vl-paramdecl-p new-param))
 :rule-classes :rewrite)

Theorem: vl-override-parameter-fn-of-vl-paramdecl-fix-decl

(defthm vl-override-parameter-fn-of-vl-paramdecl-fix-decl
 (equal
    (vl-override-parameter-fn (vl-paramdecl-fix decl)
                              elabindex override
                              ov-ss ov-scope-path warnings config)
    (vl-override-parameter-fn decl elabindex override
                              ov-ss ov-scope-path warnings config)))

Theorem: vl-override-parameter-fn-vl-paramdecl-equiv-congruence-on-decl

(defthm
     vl-override-parameter-fn-vl-paramdecl-equiv-congruence-on-decl
 (implies
  (vl-paramdecl-equiv decl decl-equiv)
  (equal
    (vl-override-parameter-fn decl elabindex override
                              ov-ss ov-scope-path warnings config)
    (vl-override-parameter-fn decl-equiv elabindex override
                              ov-ss ov-scope-path warnings config)))
 :rule-classes :congruence)

Theorem: vl-override-parameter-fn-of-vl-maybe-paramvalue-fix-override

(defthm vl-override-parameter-fn-of-vl-maybe-paramvalue-fix-override
 (equal
    (vl-override-parameter-fn decl elabindex
                              (vl-maybe-paramvalue-fix override)
                              ov-ss ov-scope-path warnings config)
    (vl-override-parameter-fn decl elabindex override
                              ov-ss ov-scope-path warnings config)))

Theorem: vl-override-parameter-fn-vl-maybe-paramvalue-equiv-congruence-on-override

(defthm
 vl-override-parameter-fn-vl-maybe-paramvalue-equiv-congruence-on-override
 (implies
  (vl-maybe-paramvalue-equiv override override-equiv)
  (equal
    (vl-override-parameter-fn decl elabindex override
                              ov-ss ov-scope-path warnings config)
    (vl-override-parameter-fn decl elabindex override-equiv
                              ov-ss ov-scope-path warnings config)))
 :rule-classes :congruence)

Theorem: vl-override-parameter-fn-of-vl-scopestack-fix-ov-ss

(defthm vl-override-parameter-fn-of-vl-scopestack-fix-ov-ss
 (equal
    (vl-override-parameter-fn decl elabindex
                              override (vl-scopestack-fix ov-ss)
                              ov-scope-path warnings config)
    (vl-override-parameter-fn decl elabindex override
                              ov-ss ov-scope-path warnings config)))

Theorem: vl-override-parameter-fn-vl-scopestack-equiv-congruence-on-ov-ss

(defthm
   vl-override-parameter-fn-vl-scopestack-equiv-congruence-on-ov-ss
 (implies
  (vl-scopestack-equiv ov-ss ov-ss-equiv)
  (equal
      (vl-override-parameter-fn decl elabindex override
                                ov-ss ov-scope-path warnings config)
      (vl-override-parameter-fn decl elabindex override ov-ss-equiv
                                ov-scope-path warnings config)))
 :rule-classes :congruence)

Theorem: vl-override-parameter-fn-of-vl-elabtraversal-fix-ov-scope-path

(defthm
     vl-override-parameter-fn-of-vl-elabtraversal-fix-ov-scope-path
 (equal
    (vl-override-parameter-fn decl elabindex override ov-ss
                              (vl-elabtraversal-fix ov-scope-path)
                              warnings config)
    (vl-override-parameter-fn decl elabindex override
                              ov-ss ov-scope-path warnings config)))

Theorem: vl-override-parameter-fn-vl-elabtraversal-equiv-congruence-on-ov-scope-path

(defthm
 vl-override-parameter-fn-vl-elabtraversal-equiv-congruence-on-ov-scope-path
 (implies
  (vl-elabtraversal-equiv ov-scope-path ov-scope-path-equiv)
  (equal
    (vl-override-parameter-fn decl elabindex override
                              ov-ss ov-scope-path warnings config)
    (vl-override-parameter-fn decl elabindex override ov-ss
                              ov-scope-path-equiv warnings config)))
 :rule-classes :congruence)

Theorem: vl-override-parameter-fn-of-vl-warninglist-fix-warnings

(defthm vl-override-parameter-fn-of-vl-warninglist-fix-warnings
 (equal
    (vl-override-parameter-fn decl
                              elabindex override ov-ss ov-scope-path
                              (vl-warninglist-fix warnings)
                              config)
    (vl-override-parameter-fn decl elabindex override
                              ov-ss ov-scope-path warnings config)))

Theorem: vl-override-parameter-fn-vl-warninglist-equiv-congruence-on-warnings

(defthm
 vl-override-parameter-fn-vl-warninglist-equiv-congruence-on-warnings
 (implies
  (vl-warninglist-equiv warnings warnings-equiv)
  (equal
    (vl-override-parameter-fn decl elabindex override
                              ov-ss ov-scope-path warnings config)
    (vl-override-parameter-fn decl elabindex override ov-ss
                              ov-scope-path warnings-equiv config)))
 :rule-classes :congruence)

Theorem: vl-override-parameter-fn-of-vl-simpconfig-fix-config

(defthm vl-override-parameter-fn-of-vl-simpconfig-fix-config
 (equal
    (vl-override-parameter-fn decl
                              elabindex override ov-ss ov-scope-path
                              warnings (vl-simpconfig-fix config))
    (vl-override-parameter-fn decl elabindex override
                              ov-ss ov-scope-path warnings config)))

Theorem: vl-override-parameter-fn-vl-simpconfig-equiv-congruence-on-config

(defthm
  vl-override-parameter-fn-vl-simpconfig-equiv-congruence-on-config
 (implies
  (vl-simpconfig-equiv config config-equiv)
  (equal
    (vl-override-parameter-fn decl elabindex override
                              ov-ss ov-scope-path warnings config)
    (vl-override-parameter-fn decl elabindex override ov-ss
                              ov-scope-path warnings config-equiv)))
 :rule-classes :congruence)

Subtopics

Vl-convert-parameter-value-to-explicit-type

Alter the expression given to an explicitly typed parameter so that it has the correct type.