• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Community
  • Proof-automation
  • ACL2
  • Macro-libraries
  • 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-convert-parameter-value-to-explicit-type
            • Vl-override-parameter-with-expr
            • Vl-override-parameter-with-type
            • Vl-paramdecl-final-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

• Vl-override-parameter-value

Vl-override-parameter-with-expr

Try to override a parameter with a new expression.

Signature

(vl-override-parameter-with-expr decl expr ss warnings ctx) 
  → 
(mv okp warnings new-value)

Arguments

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

expr — The value expression to override this parameter with.
    Guard (vl-expr-p expr).

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

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

ctx — Context for error messages.
    Guard (vl-context-p ctx).

Returns

okp — Type (booleanp okp).

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

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

Definitions and Theorems

Function: vl-override-parameter-with-expr

(defun vl-override-parameter-with-expr (decl expr ss warnings ctx)
 (declare (xargs :guard (and (vl-paramdecl-p decl)
                             (vl-expr-p expr)
                             (vl-scopestack-p ss)
                             (vl-warninglist-p warnings)
                             (vl-context-p ctx))))
 (let ((__function__ 'vl-override-parameter-with-expr))
  (declare (ignorable __function__))
  (b* (((vl-paramdecl decl)
        (vl-paramdecl-fix decl))
       (expr (vl-expr-fix expr))
       (ctx (vl-context-fix ctx)))
   (vl-paramtype-case
    decl.type
    (:vl-typeparam
     (vl-unparam-debug
      "~a0: can't override type parameter ~a1 width expression ~a2.~%"
      ctx decl expr)
     (mv
      nil
      (fatal
       :type :vl-bad-instance
       :msg
       "~a0: can't override parameter ~s1 with expression, ~
                        ~a2: ~s1 is a type parameter, not a value parameter."
       :args (list ctx decl.name expr))
      expr))
    (:vl-explicitvalueparam
     (b* (((mv okp warnings coerced-expr)
           (vl-convert-parameter-value-to-explicit-type
                decl.type.type
                expr ss warnings ctx decl.name))
          ((unless okp) (mv nil warnings expr)))
      (vl-unparam-debug
       "~a0: successfully overriding value parameter ~a1 with ~a2.~%"
       ctx decl coerced-expr)
      (mv t (ok) coerced-expr)))
    (:vl-implicitvalueparam
     (b*
      (((mv ok reduced-expr)
        (vl-consteval expr ss))
       ((unless ok)
        (vl-unparam-debug
         "~a0: can't override ~a1, only reduced expr ~a2 to ~a3 (not a constant)."
         ctx decl expr reduced-expr)
        (mv
         nil
         (fatal
          :type :vl-bad-instance
          :msg
          "~a0: can't override parameter ~s1: failed to ~
                              reduce expression ~a2 to a constant integer."
          :args (list ctx decl.name expr))
         expr))
       (new-dims
         (cond (decl.type.range (list decl.type.range))
               ((eql 1 (vl-expr->finalwidth reduced-expr))
                nil)
               (t (list (vl-make-n-bit-range
                             (vl-expr->finalwidth reduced-expr))))))
       (new-signedp
            (cond ((and (not decl.type.range)
                        (not decl.type.sign))
                   (eq (vl-expr->finaltype reduced-expr)
                       :vl-signed))
                  (decl.type.sign (eq decl.type.sign :vl-signed))
                  (t nil)))
       (explicit-type (make-vl-coretype :name :vl-logic
                                        :signedp new-signedp
                                        :pdims new-dims))
       ((mv okp warnings coerced-expr)
        (vl-convert-parameter-value-to-explicit-type
             explicit-type
             reduced-expr ss warnings ctx decl.name))
       ((unless okp) (mv nil warnings expr)))
      (vl-unparam-debug
           "~a0: successfully overriding ~a1 with ~a2.~%"
           ctx decl coerced-expr)
      (mv t (ok) coerced-expr)))))))

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

(defthm booleanp-of-vl-override-parameter-with-expr.okp
 (b* (((mv ?okp ?warnings ?new-value)
       (vl-override-parameter-with-expr decl expr ss warnings ctx)))
   (booleanp okp))
 :rule-classes :type-prescription)

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

(defthm vl-warninglist-p-of-vl-override-parameter-with-expr.warnings
 (b* (((mv ?okp ?warnings ?new-value)
       (vl-override-parameter-with-expr decl expr ss warnings ctx)))
   (vl-warninglist-p warnings))
 :rule-classes :rewrite)

Theorem: vl-expr-p-of-vl-override-parameter-with-expr.new-value

(defthm vl-expr-p-of-vl-override-parameter-with-expr.new-value
 (b* (((mv ?okp ?warnings ?new-value)
       (vl-override-parameter-with-expr decl expr ss warnings ctx)))
   (vl-expr-p new-value))
 :rule-classes :rewrite)

Theorem: vl-override-parameter-with-expr-of-vl-paramdecl-fix-decl

(defthm vl-override-parameter-with-expr-of-vl-paramdecl-fix-decl
  (equal
       (vl-override-parameter-with-expr (vl-paramdecl-fix decl)
                                        expr ss warnings ctx)
       (vl-override-parameter-with-expr decl expr ss warnings ctx)))

Theorem: vl-override-parameter-with-expr-vl-paramdecl-equiv-congruence-on-decl

(defthm
 vl-override-parameter-with-expr-vl-paramdecl-equiv-congruence-on-decl
 (implies
  (vl-paramdecl-equiv decl decl-equiv)
  (equal (vl-override-parameter-with-expr decl expr ss warnings ctx)
         (vl-override-parameter-with-expr
              decl-equiv expr ss warnings ctx)))
 :rule-classes :congruence)

Theorem: vl-override-parameter-with-expr-of-vl-expr-fix-expr

(defthm vl-override-parameter-with-expr-of-vl-expr-fix-expr
  (equal
       (vl-override-parameter-with-expr decl (vl-expr-fix expr)
                                        ss warnings ctx)
       (vl-override-parameter-with-expr decl expr ss warnings ctx)))

Theorem: vl-override-parameter-with-expr-vl-expr-equiv-congruence-on-expr

(defthm
   vl-override-parameter-with-expr-vl-expr-equiv-congruence-on-expr
 (implies
  (vl-expr-equiv expr expr-equiv)
  (equal (vl-override-parameter-with-expr decl expr ss warnings ctx)
         (vl-override-parameter-with-expr
              decl expr-equiv ss warnings ctx)))
 :rule-classes :congruence)

Theorem: vl-override-parameter-with-expr-of-vl-scopestack-fix-ss

(defthm vl-override-parameter-with-expr-of-vl-scopestack-fix-ss
 (equal
   (vl-override-parameter-with-expr decl expr (vl-scopestack-fix ss)
                                    warnings ctx)
   (vl-override-parameter-with-expr decl expr ss warnings ctx)))

Theorem: vl-override-parameter-with-expr-vl-scopestack-equiv-congruence-on-ss

(defthm
 vl-override-parameter-with-expr-vl-scopestack-equiv-congruence-on-ss
 (implies
  (vl-scopestack-equiv ss ss-equiv)
  (equal (vl-override-parameter-with-expr decl expr ss warnings ctx)
         (vl-override-parameter-with-expr
              decl expr ss-equiv warnings ctx)))
 :rule-classes :congruence)

Theorem: vl-override-parameter-with-expr-of-vl-warninglist-fix-warnings

(defthm
     vl-override-parameter-with-expr-of-vl-warninglist-fix-warnings
  (equal
       (vl-override-parameter-with-expr
            decl
            expr ss (vl-warninglist-fix warnings)
            ctx)
       (vl-override-parameter-with-expr decl expr ss warnings ctx)))

Theorem: vl-override-parameter-with-expr-vl-warninglist-equiv-congruence-on-warnings

(defthm
 vl-override-parameter-with-expr-vl-warninglist-equiv-congruence-on-warnings
 (implies
  (vl-warninglist-equiv warnings warnings-equiv)
  (equal (vl-override-parameter-with-expr decl expr ss warnings ctx)
         (vl-override-parameter-with-expr
              decl expr ss warnings-equiv ctx)))
 :rule-classes :congruence)

Theorem: vl-override-parameter-with-expr-of-vl-context-fix-ctx

(defthm vl-override-parameter-with-expr-of-vl-context-fix-ctx
  (equal
       (vl-override-parameter-with-expr
            decl
            expr ss warnings (vl-context-fix ctx))
       (vl-override-parameter-with-expr decl expr ss warnings ctx)))

Theorem: vl-override-parameter-with-expr-vl-context-equiv-congruence-on-ctx

(defthm
 vl-override-parameter-with-expr-vl-context-equiv-congruence-on-ctx
 (implies
  (vl-context-equiv ctx ctx-equiv)
  (equal (vl-override-parameter-with-expr decl expr ss warnings ctx)
         (vl-override-parameter-with-expr
              decl expr ss warnings ctx-equiv)))
 :rule-classes :congruence)