• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • 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
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Vl-svstmt.lisp

Vl-elaborated-expr-consteval

Assumes expression is already elaborated.

Signature

(vl-elaborated-expr-consteval x ss scopes &key (ctxsize 'nil) 
                              (type 'nil) 
                              (lhs 'nil)) 
 
  → 
(mv ok constp warnings1 new-x svex)

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

ok — no errors.

constp — successfully reduced to constant.

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

new-x — Type (vl-expr-p new-x).

svex — Type (sv::svex-p svex).

Definitions and Theorems

Function: vl-elaborated-expr-consteval-fn

(defun vl-elaborated-expr-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-elaborated-expr-consteval))
  (declare (ignorable __function__))
  (b*
   ((x (vl-expr-fix x))
    (type (vl-maybe-datatype-fix type))
    ((when (and type
                (not (vl-datatype-resolved-p type))))
     (mv
      nil nil
      (list
       (make-vl-warning
            :type :vl-expression-type-unresolved
            :msg
            "Datatype ~a0 unresolved when evaluating expression ~a1"
            :args (list type x)))
      x (svex-x)))
    (warnings nil)
    ((mv warnings svex size)
     (if type
      (b* (((mv ?err size) (vl-datatype-size type))
           ((vwmv vttree type-err svex)
            (vl-expr-to-svex-datatyped x nil type ss scopes
                                       :compattype :assign))
           ((wmv warnings)
            (vl-type-error-basic-warn x nil type-err lhs type ss)))
        (mv warnings svex size))
      (if ctxsize
          (b* (((vwmv vttree svex size)
                (vl-expr-to-svex-selfdet x ctxsize ss scopes)))
            (mv warnings svex size))
        (b* (((vwmv vttree svex ?type size)
              (vl-expr-to-svex-untyped x ss scopes)))
          (mv warnings svex size)))))
    ((unless (posp size))
     (mv nil nil warnings x (svex-x)))
    (svex (sv::svex-reduce-consts svex))
    (val (sv::svex-case svex
                        :quote svex.val
                        :otherwise nil))
    ((unless val)
     (mv t nil warnings x svex))
    ((when type)
     (b*
      (((wmv warnings new-expr &)
        (vl-literal-expr-from-4vec type val))
       (new-expr (vl-expr-update-atts new-expr
                                      (cons (cons "VL_ORIG_EXPR" x)
                                            (vl-expr->atts x)))))
      (mv t t warnings new-expr svex)))
    ((wmv warnings class)
     (if type (b* (((mv ?caveat class)
                    (vl-datatype-arithclass type)))
                (mv nil class))
       (vl-expr-typedecide x ss scopes)))
    (signedness (if (vl-integer-arithclass-p class)
                    (vl-integer-arithclass->exprsign class)
                  :vl-unsigned))
    (new-x
     (make-vl-literal :val (vl-4vec-to-value val size
                                             :signedness signedness)
                      :atts (cons (cons "VL_ORIG_EXPR" x)
                                  (vl-expr->atts x)))))
   (mv t t warnings new-x svex))))

Theorem: vl-warninglist-p-of-vl-elaborated-expr-consteval.warnings1

(defthm vl-warninglist-p-of-vl-elaborated-expr-consteval.warnings1
 (b*
  (((mv ?ok ?constp ?warnings1 ?new-x ?svex)
    (vl-elaborated-expr-consteval-fn x ss scopes ctxsize type lhs)))
  (vl-warninglist-p warnings1))
 :rule-classes :rewrite)

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

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

Theorem: svex-p-of-vl-elaborated-expr-consteval.svex

(defthm svex-p-of-vl-elaborated-expr-consteval.svex
 (b*
  (((mv ?ok ?constp ?warnings1 ?new-x ?svex)
    (vl-elaborated-expr-consteval-fn x ss scopes ctxsize type lhs)))
  (sv::svex-p svex))
 :rule-classes :rewrite)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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