• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • 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-consteval

    Signature
    (vl-consteval x ss scopes &key (ctxsize 'nil) 
                  (type 'nil) 
                  (lhs 'nil)) 
     
      → 
    (mv warnings new-x)
    Arguments
    x — Guard (vl-expr-p x).
    ss — Guard (vl-scopestack-p ss).
    scopes — Guard (vl-elabscopes-p scopes).
    ctxsize — Guard (maybe-natp ctxsize).
    type — Guard (vl-maybe-datatype-p type).
    lhs — Guard (vl-maybe-expr-p lhs).
    Returns
    warnings — Type (vl-warninglist-p warnings).
    new-x — Type (vl-expr-p new-x).

    Definitions and Theorems

    Function: vl-consteval-fn

    (defun vl-consteval-fn (x ss scopes ctxsize type lhs)
      (declare (xargs :guard (and (vl-expr-p x)
                                  (vl-scopestack-p ss)
                                  (vl-elabscopes-p scopes)
                                  (maybe-natp ctxsize)
                                  (vl-maybe-datatype-p type)
                                  (vl-maybe-expr-p lhs))))
      (let ((__function__ 'vl-consteval))
        (declare (ignorable __function__))
        (b* (((mv ?ok ?constant warnings new-x ?svex)
              (vl-elaborated-expr-consteval x ss scopes
                                            :ctxsize ctxsize
                                            :type type
                                            :lhs lhs)))
          (mv warnings new-x))))

    Theorem: vl-warninglist-p-of-vl-consteval.warnings

    (defthm vl-warninglist-p-of-vl-consteval.warnings
      (b* (((mv ?warnings ?new-x)
            (vl-consteval-fn x ss scopes ctxsize type lhs)))
        (vl-warninglist-p warnings))
      :rule-classes :rewrite)

    Theorem: vl-expr-p-of-vl-consteval.new-x

    (defthm vl-expr-p-of-vl-consteval.new-x
      (b* (((mv ?warnings ?new-x)
            (vl-consteval-fn x ss scopes ctxsize type lhs)))
        (vl-expr-p new-x))
      :rule-classes :rewrite)

    Theorem: vl-consteval-fn-of-vl-expr-fix-x

    (defthm vl-consteval-fn-of-vl-expr-fix-x
      (equal (vl-consteval-fn (vl-expr-fix x)
                              ss scopes ctxsize type lhs)
             (vl-consteval-fn x ss scopes ctxsize type lhs)))

    Theorem: vl-consteval-fn-vl-expr-equiv-congruence-on-x

    (defthm vl-consteval-fn-vl-expr-equiv-congruence-on-x
      (implies
           (vl-expr-equiv x x-equiv)
           (equal (vl-consteval-fn x ss scopes ctxsize type lhs)
                  (vl-consteval-fn x-equiv ss scopes ctxsize type lhs)))
      :rule-classes :congruence)

    Theorem: vl-consteval-fn-of-vl-scopestack-fix-ss

    (defthm vl-consteval-fn-of-vl-scopestack-fix-ss
      (equal (vl-consteval-fn x (vl-scopestack-fix ss)
                              scopes ctxsize type lhs)
             (vl-consteval-fn x ss scopes ctxsize type lhs)))

    Theorem: vl-consteval-fn-vl-scopestack-equiv-congruence-on-ss

    (defthm vl-consteval-fn-vl-scopestack-equiv-congruence-on-ss
      (implies
           (vl-scopestack-equiv ss ss-equiv)
           (equal (vl-consteval-fn x ss scopes ctxsize type lhs)
                  (vl-consteval-fn x ss-equiv scopes ctxsize type lhs)))
      :rule-classes :congruence)

    Theorem: vl-consteval-fn-of-vl-elabscopes-fix-scopes

    (defthm vl-consteval-fn-of-vl-elabscopes-fix-scopes
      (equal (vl-consteval-fn x ss (vl-elabscopes-fix scopes)
                              ctxsize type lhs)
             (vl-consteval-fn x ss scopes ctxsize type lhs)))

    Theorem: vl-consteval-fn-vl-elabscopes-equiv-congruence-on-scopes

    (defthm vl-consteval-fn-vl-elabscopes-equiv-congruence-on-scopes
      (implies
           (vl-elabscopes-equiv scopes scopes-equiv)
           (equal (vl-consteval-fn x ss scopes ctxsize type lhs)
                  (vl-consteval-fn x ss scopes-equiv ctxsize type lhs)))
      :rule-classes :congruence)

    Theorem: vl-consteval-fn-of-maybe-natp-fix-ctxsize

    (defthm vl-consteval-fn-of-maybe-natp-fix-ctxsize
      (equal (vl-consteval-fn x ss scopes (maybe-natp-fix ctxsize)
                              type lhs)
             (vl-consteval-fn x ss scopes ctxsize type lhs)))

    Theorem: vl-consteval-fn-maybe-nat-equiv-congruence-on-ctxsize

    (defthm vl-consteval-fn-maybe-nat-equiv-congruence-on-ctxsize
      (implies
           (acl2::maybe-nat-equiv ctxsize ctxsize-equiv)
           (equal (vl-consteval-fn x ss scopes ctxsize type lhs)
                  (vl-consteval-fn x ss scopes ctxsize-equiv type lhs)))
      :rule-classes :congruence)

    Theorem: vl-consteval-fn-of-vl-maybe-datatype-fix-type

    (defthm vl-consteval-fn-of-vl-maybe-datatype-fix-type
      (equal (vl-consteval-fn x ss scopes
                              ctxsize (vl-maybe-datatype-fix type)
                              lhs)
             (vl-consteval-fn x ss scopes ctxsize type lhs)))

    Theorem: vl-consteval-fn-vl-maybe-datatype-equiv-congruence-on-type

    (defthm vl-consteval-fn-vl-maybe-datatype-equiv-congruence-on-type
      (implies
           (vl-maybe-datatype-equiv type type-equiv)
           (equal (vl-consteval-fn x ss scopes ctxsize type lhs)
                  (vl-consteval-fn x ss scopes ctxsize type-equiv lhs)))
      :rule-classes :congruence)

    Theorem: vl-consteval-fn-of-vl-maybe-expr-fix-lhs

    (defthm vl-consteval-fn-of-vl-maybe-expr-fix-lhs
      (equal (vl-consteval-fn x ss scopes
                              ctxsize type (vl-maybe-expr-fix lhs))
             (vl-consteval-fn x ss scopes ctxsize type lhs)))

    Theorem: vl-consteval-fn-vl-maybe-expr-equiv-congruence-on-lhs

    (defthm vl-consteval-fn-vl-maybe-expr-equiv-congruence-on-lhs
      (implies
           (vl-maybe-expr-equiv lhs lhs-equiv)
           (equal (vl-consteval-fn x ss scopes ctxsize type lhs)
                  (vl-consteval-fn x ss scopes ctxsize type lhs-equiv)))
      :rule-classes :congruence)