• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
      • Svex-stvs
      • Svex-decomposition-methodology
      • Sv-versus-esim
      • Svex-decomp
      • Svex-compose-dfs
      • Svex-compilation
      • Moddb
      • Svmods
      • Svstmt
      • Sv-tutorial
      • Expressions
      • Symbolic-test-vector
      • Vl-to-svex
        • Vl-to-sv
        • Vl-design->sv-design
          • Vl-simpconfig
          • Vl-hierarchy-sv-translation
          • Vl-expr-svex-translation
          • Vl-design->svex-modalist
          • Vl-svstmt
            • Vl-svstmt.lisp
              • Vl-casestmt-violation-conds
              • Vl-caselist-none/multiple
              • Vl-elaborated-expr-consteval
              • Vl-always->svex
              • Vl-caseexprs->svex-test
              • Vl-always->svex-checks
              • Vl-implicitvalueparam-final-type
              • Vl-assignstmt->svstmts
              • Vl-fundecl-to-svex
              • Vl-evatomlist-delay-substitution
              • Vl-consteval
              • Vl-alwayslist->svex
              • Vl-index-expr-svex/size/type
              • Vl-vardecllist->svstmts
              • Sv::svex-alist->assigns
              • Vl-case-conservative-test-expr
              • Vl-evatomlist->svex
              • Vl-case-xcond-wrapper
              • Sv::constraintlist-maybe-rewrite-fixpoint
              • Vl-always-apply-trigger-to-updates
              • Vl-initiallist-size-warnings
              • Vl-initial-size-warnings
              • Vl-finallist-size-warnings
              • Vl-always->svex-latch-warnings
              • Vl-final-size-warnings
              • Sv::svarlist-masked-x-subst
              • Sv::svar->lhs-by-mask
              • Svstmt-config
              • Sv::svex-alist-unset-nonblocking
              • Sv::svar->lhs-by-size
              • Combine-mask-alists
              • Sv::svarlist-delay-subst
              • Vttree-constraints-to-svstmts
              • Sv::4vmask-alist-unset-nonblocking
              • Sv::svarlist-remove-delays
              • Vl-caselist->caseexprs
              • Vl-evatomlist-has-edge
        • Vl-to-sv-main
        • Vl-simplify-sv
        • Vl-user-paramsettings->unparam-names
        • Vl-user-paramsettings->modnames
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Vl-svstmt.lisp

Vl-implicitvalueparam-final-type

Signature

(vl-implicitvalueparam-final-type x override ss scopes) 
  → 
(mv warnings err type)

Arguments

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

override — Guard (vl-expr-p override).

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

scopes — for override.
    Guard (vl-elabscopes-p scopes).

Returns

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

err — Type (iff (vl-msg-p err) err).

type — Type (implies (not err) (vl-datatype-p type)).

Definitions and Theorems

Function: vl-implicitvalueparam-final-type

(defun vl-implicitvalueparam-final-type (x override ss scopes)
 (declare (xargs :guard (and (vl-paramtype-p x)
                             (vl-expr-p override)
                             (vl-scopestack-p ss)
                             (vl-elabscopes-p scopes))))
 (declare
      (xargs :guard (vl-paramtype-case x :vl-implicitvalueparam)))
 (let ((__function__ 'vl-implicitvalueparam-final-type))
  (declare (ignorable __function__))
  (b*
   ((override (vl-expr-fix override))
    ((vl-implicitvalueparam x)
     (vl-paramtype-fix x))
    (warnings nil)
    ((when x.range)
     (if
      (vl-range-resolved-p x.range)
      (mv
       warnings nil
       (make-vl-coretype :name :vl-logic
                         :pdims (list (vl-range->dimension x.range))
                         :signedp (eq x.sign :vl-signed)))
      (mv warnings (vmsg "Unresolved range")
          nil)))
    ((wmv warnings size)
     (vl-expr-selfsize override ss scopes))
    ((unless (posp size))
     (mv warnings
         (vmsg "Unsized or zero-size parameter override: ~a0"
               override)
         nil))
    (dims (list (vl-range->dimension
                     (make-vl-range :msb (vl-make-index (1- size))
                                    :lsb (vl-make-index 0)))))
    ((when x.sign)
     (mv warnings nil
         (make-vl-coretype :name :vl-logic
                           :pdims dims
                           :signedp (eq x.sign :vl-signed))))
    ((wmv warnings class)
     (vl-expr-typedecide override ss scopes))
    ((unless (vl-integer-arithclass-p class))
     (mv
        warnings
        (vmsg "Couldn't decide signedness of parameter override ~a0"
              override)
        nil)))
   (mv warnings nil
       (if (and (eql size 32)
                (vl-arithclass-equiv class :vl-signed-int-class))
           (make-vl-coretype :name :vl-integer
                             :signedp t)
         (make-vl-coretype
              :name :vl-logic
              :pdims dims
              :signedp
              (vl-arithclass-equiv class :vl-signed-int-class)))))))

Theorem: vl-warninglist-p-of-vl-implicitvalueparam-final-type.warnings

(defthm
      vl-warninglist-p-of-vl-implicitvalueparam-final-type.warnings
  (b* (((mv ?warnings ?err common-lisp::?type)
        (vl-implicitvalueparam-final-type x override ss scopes)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-implicitvalueparam-final-type.err

(defthm return-type-of-vl-implicitvalueparam-final-type.err
  (b* (((mv ?warnings ?err common-lisp::?type)
        (vl-implicitvalueparam-final-type x override ss scopes)))
    (iff (vl-msg-p err) err))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-implicitvalueparam-final-type.type

(defthm return-type-of-vl-implicitvalueparam-final-type.type
  (b* (((mv ?warnings ?err common-lisp::?type)
        (vl-implicitvalueparam-final-type x override ss scopes)))
    (implies (not err)
             (vl-datatype-p type)))
  :rule-classes :rewrite)

Theorem: vl-datatype-resolved-p-of-vl-implicitvalueparam-final-type

(defthm vl-datatype-resolved-p-of-vl-implicitvalueparam-final-type
  (b* (((mv ?warnings ?err common-lisp::?type)
        (vl-implicitvalueparam-final-type x override ss scopes)))
    (implies (not err)
             (vl-datatype-resolved-p type))))

Theorem: vl-implicitvalueparam-final-type-of-vl-paramtype-fix-x

(defthm vl-implicitvalueparam-final-type-of-vl-paramtype-fix-x
  (equal (vl-implicitvalueparam-final-type (vl-paramtype-fix x)
                                           override ss scopes)
         (vl-implicitvalueparam-final-type x override ss scopes)))

Theorem: vl-implicitvalueparam-final-type-vl-paramtype-equiv-congruence-on-x

(defthm
 vl-implicitvalueparam-final-type-vl-paramtype-equiv-congruence-on-x
 (implies
  (vl-paramtype-equiv x x-equiv)
  (equal
     (vl-implicitvalueparam-final-type x override ss scopes)
     (vl-implicitvalueparam-final-type x-equiv override ss scopes)))
 :rule-classes :congruence)

Theorem: vl-implicitvalueparam-final-type-of-vl-expr-fix-override

(defthm vl-implicitvalueparam-final-type-of-vl-expr-fix-override
  (equal (vl-implicitvalueparam-final-type x (vl-expr-fix override)
                                           ss scopes)
         (vl-implicitvalueparam-final-type x override ss scopes)))

Theorem: vl-implicitvalueparam-final-type-vl-expr-equiv-congruence-on-override

(defthm
 vl-implicitvalueparam-final-type-vl-expr-equiv-congruence-on-override
 (implies
  (vl-expr-equiv override override-equiv)
  (equal
     (vl-implicitvalueparam-final-type x override ss scopes)
     (vl-implicitvalueparam-final-type x override-equiv ss scopes)))
 :rule-classes :congruence)

Theorem: vl-implicitvalueparam-final-type-of-vl-scopestack-fix-ss

(defthm vl-implicitvalueparam-final-type-of-vl-scopestack-fix-ss
  (equal (vl-implicitvalueparam-final-type
              x override (vl-scopestack-fix ss)
              scopes)
         (vl-implicitvalueparam-final-type x override ss scopes)))

Theorem: vl-implicitvalueparam-final-type-vl-scopestack-equiv-congruence-on-ss

(defthm
 vl-implicitvalueparam-final-type-vl-scopestack-equiv-congruence-on-ss
 (implies
  (vl-scopestack-equiv ss ss-equiv)
  (equal
     (vl-implicitvalueparam-final-type x override ss scopes)
     (vl-implicitvalueparam-final-type x override ss-equiv scopes)))
 :rule-classes :congruence)

Theorem: vl-implicitvalueparam-final-type-of-vl-elabscopes-fix-scopes

(defthm vl-implicitvalueparam-final-type-of-vl-elabscopes-fix-scopes
  (equal (vl-implicitvalueparam-final-type
              x
              override ss (vl-elabscopes-fix scopes))
         (vl-implicitvalueparam-final-type x override ss scopes)))

Theorem: vl-implicitvalueparam-final-type-vl-elabscopes-equiv-congruence-on-scopes

(defthm
 vl-implicitvalueparam-final-type-vl-elabscopes-equiv-congruence-on-scopes
 (implies
  (vl-elabscopes-equiv scopes scopes-equiv)
  (equal
     (vl-implicitvalueparam-final-type x override ss scopes)
     (vl-implicitvalueparam-final-type x override ss scopes-equiv)))
 :rule-classes :congruence)