• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Debugging
  • Projects
  • 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
            • Sv::vl-expr.lisp
              • Vl-scopecontext-to-addr
              • Vl-binaryop-to-svex
              • Vl-expr-to-svex-maybe-typed
              • Vl-datatype-syscall-to-svex
              • Vl-operandinfo-to-svex-preproc
              • Vl-structmemberlist->types
              • Vl-seltrace-to-svex-select
              • Vl-portdecllist->types
              • Vl-operandinfo-to-svex-select
              • Vl-plusminus-partselect->svex
              • Vl-arrayrange->rel-lsb-and-width
              • Vl-unaryop-to-svex
              • Vl-funcall-args-to-ordered
              • Vl-expr-to-svex-lhs
              • Vl-operandinfo-to-svex
              • Vl-array-assignpat-keyval-resolve
              • Vl-err->vfatal
              • Vl-datatypelist-usertype-resolve
              • Vl-upscope-to-svex-upscope
              • Vl-err->fatal
              • Vl-streaming-concat-trunc/extend
              • Vl-operandinfo-base-svar
              • Vl-index-shift-amount
              • Vttree->constraints
              • Vl-slicesize-resolve
              • Vl-function-map-find-matching-aux
              • Vl-funname-lookup
              • Vl-datatype-size-warn
              • Svex-repeat-aux
              • Vl-$test$plusargs-to-svex
              • Svex-extend
              • Vl-structmemberlist-shift-bits
              • Vl-datatype-slot-width/range
              • Vl-datatype-index-shift-amount
              • Vl-datatype-field-shift-amount
              • 4vec-extend
              • Vl-function-pair-inputs-with-actuals
              • Vl-expr-to-svex-untyped
              • Vl-function-map-check-matching
              • Vl-datatype-syscall-remove-dims
              • Svex-concat-list-aux
              • Vttree-add-constraints
              • Vttree-add-warnings
              • Vl-check-struct-assignpat-keys
              • Vl-check-array-assignpat-keys
              • Sv::constraintlist-subst-memo
              • Vl-svex-keyval-index-lookup
              • Vl-function-map-find-matching
              • Vl-convert-dollarsign-to-expr
              • Vttree->constraints-acc
              • Vl-seltrace-type
              • Vl-seltrace-to-path
              • Vl-keyval-member-lookup
              • Svex-repeat
              • Vttree->warnings-acc
              • Vl-trunc/extend-type-err
              • Constraintlist-add-ctx
              • Vl-hidtrace-add-to-path
              • Svex-multiconcat
              • Vttree-join
              • Vl-value-to-string-aux
              • Vl-seltrace-add-to-path
              • Vl-value-to-4vec
              • Vl-expr-to-svex-selfdet
              • Vl-svex-keyval-default-lookup
              • Vl-$test$plusargs-p
              • Vl-value-to-svex
              • Vl-value-in-range
              • Vl-keyval-default-lookup
              • Sv::svexlist-args-extract-constants
              • Vl-string->bits
              • Vl-size-to-unsigned-logic
              • Vl-hidtrace-to-path
              • Svex-concat-list
              • Vttree->warnings
              • Vl-seltrace-unres-count
              • Vl-datatype-index-is-bitselect
              • Vl-bitlist->4vec
              • Vl-svex-keyvallist-vars
              • Vl-hidstep->svex-index
              • Vl-selstep->svex-name
              • Vl-datatypelist-resolved-p
              • Vl-datatype-$unpacked_dimensions
              • Vl-datatype-$dimensions
              • Vl-bitlist->offset
              • Vl-bitlist->onset
              • Vl-streamexprlist-has-with
              • Vl-hidstep-resolved-p
              • Vl-expr-needs-type-context
              • Vl-streamexprlist->exprs
              • Vl-integer-to-string
              • Vl-hidtrace-resolved-p
              • Vl-selstep-resolved-p
              • Vl-select-resolved-p
              • Vl-svex-keyvallist
              • Vl-datatypelist
              • Svex-x
            • Vttree
          • Vl-design->svex-modalist
          • Vl-svstmt
        • 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

• Sv::vl-expr.lisp

Vl-expr-to-svex-maybe-typed

Convert an expression to svex, maybe given a datatype that it needs to match.

Signature

(vl-expr-to-svex-maybe-typed x type 
                             ss scopes &key (compattype ':equiv)) 
 
  → 
(mv vttree svex res-type res-size type-err)

Arguments

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

type — Guard (vl-maybe-datatype-p type).

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

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

compattype — Guard (vl-typecompat-p compattype).

Returns

vttree — Type (and (vttree-p vttree) (sv::svarlist-addr-p (sv::constraintlist-vars (vttree->constraints vttree)))) .

svex — Type (and (sv::svex-p svex) (sv::svarlist-addr-p (sv::svex-vars svex))).

res-type — Type (and (vl-maybe-datatype-p res-type) (and (implies res-type (vl-datatype-resolved-p res-type)))) .

res-size — Type (maybe-natp res-size).

type-err — Type (vl-maybe-type-error-p type-err).

Definitions and Theorems

Function: vl-expr-to-svex-maybe-typed-fn

(defun vl-expr-to-svex-maybe-typed-fn (x type ss scopes compattype)
 (declare (xargs :guard (and (vl-expr-p x)
                             (vl-maybe-datatype-p type)
                             (vl-scopestack-p ss)
                             (vl-elabscopes-p scopes)
                             (vl-typecompat-p compattype))))
 (declare (xargs :guard (or (not type)
                            (vl-datatype-resolved-p type))))
 (let ((__function__ 'vl-expr-to-svex-maybe-typed))
  (declare (ignorable __function__))
  (b* ((type (vl-maybe-datatype-fix type)))
   (if type
    (b*
     (((mv vttree type-err svex)
       (vl-expr-to-svex-datatyped x nil type ss scopes
                                  :compattype compattype))
      ((mv err size) (vl-datatype-size type))
      ((when (or err (not size)))
       (mv
        (vwarn
            :type :vl-expr-to-svex-fail
            :msg
            "Datatype ~a0 for expression ~a1 couldn't be sized: ~@0"
            :args (list type (vl-expr-fix x)
                        (or err "unsizable")))
        svex
        (and (mbt (vl-datatype-resolved-p type))
             type)
        nil type-err)))
     (mv vttree svex
         (and (mbt (vl-datatype-resolved-p type))
              type)
         size type-err))
    (b* (((mv vttree svex res-type res-size)
          (vl-expr-to-svex-untyped x ss scopes)))
      (mv vttree svex res-type res-size nil))))))

Theorem: return-type-of-vl-expr-to-svex-maybe-typed.vttree

(defthm return-type-of-vl-expr-to-svex-maybe-typed.vttree
 (b*
   (((mv ?vttree
         ?svex ?res-type ?res-size ?type-err)
     (vl-expr-to-svex-maybe-typed-fn x type ss scopes compattype)))
  (and
      (vttree-p vttree)
      (sv::svarlist-addr-p
           (sv::constraintlist-vars (vttree->constraints vttree)))))
 :rule-classes :rewrite)

Theorem: return-type-of-vl-expr-to-svex-maybe-typed.svex

(defthm return-type-of-vl-expr-to-svex-maybe-typed.svex
  (b*
    (((mv ?vttree
          ?svex ?res-type ?res-size ?type-err)
      (vl-expr-to-svex-maybe-typed-fn x type ss scopes compattype)))
    (and (sv::svex-p svex)
         (sv::svarlist-addr-p (sv::svex-vars svex))))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-expr-to-svex-maybe-typed.res-type

(defthm return-type-of-vl-expr-to-svex-maybe-typed.res-type
  (b*
    (((mv ?vttree
          ?svex ?res-type ?res-size ?type-err)
      (vl-expr-to-svex-maybe-typed-fn x type ss scopes compattype)))
    (and (vl-maybe-datatype-p res-type)
         (and (implies res-type
                       (vl-datatype-resolved-p res-type)))))
  :rule-classes :rewrite)

Theorem: maybe-natp-of-vl-expr-to-svex-maybe-typed.res-size

(defthm maybe-natp-of-vl-expr-to-svex-maybe-typed.res-size
  (b*
    (((mv ?vttree
          ?svex ?res-type ?res-size ?type-err)
      (vl-expr-to-svex-maybe-typed-fn x type ss scopes compattype)))
    (maybe-natp res-size))
  :rule-classes :type-prescription)

Theorem: vl-maybe-type-error-p-of-vl-expr-to-svex-maybe-typed.type-err

(defthm
      vl-maybe-type-error-p-of-vl-expr-to-svex-maybe-typed.type-err
  (b*
    (((mv ?vttree
          ?svex ?res-type ?res-size ?type-err)
      (vl-expr-to-svex-maybe-typed-fn x type ss scopes compattype)))
    (vl-maybe-type-error-p type-err))
  :rule-classes :rewrite)

Theorem: vl-expr-to-svex-maybe-typed-fn-of-vl-expr-fix-x

(defthm vl-expr-to-svex-maybe-typed-fn-of-vl-expr-fix-x
 (equal
      (vl-expr-to-svex-maybe-typed-fn (vl-expr-fix x)
                                      type ss scopes compattype)
      (vl-expr-to-svex-maybe-typed-fn x type ss scopes compattype)))

Theorem: vl-expr-to-svex-maybe-typed-fn-vl-expr-equiv-congruence-on-x

(defthm vl-expr-to-svex-maybe-typed-fn-vl-expr-equiv-congruence-on-x
 (implies
   (vl-expr-equiv x x-equiv)
   (equal
        (vl-expr-to-svex-maybe-typed-fn x type ss scopes compattype)
        (vl-expr-to-svex-maybe-typed-fn
             x-equiv type ss scopes compattype)))
 :rule-classes :congruence)

Theorem: vl-expr-to-svex-maybe-typed-fn-of-vl-maybe-datatype-fix-type

(defthm vl-expr-to-svex-maybe-typed-fn-of-vl-maybe-datatype-fix-type
 (equal
      (vl-expr-to-svex-maybe-typed-fn x (vl-maybe-datatype-fix type)
                                      ss scopes compattype)
      (vl-expr-to-svex-maybe-typed-fn x type ss scopes compattype)))

Theorem: vl-expr-to-svex-maybe-typed-fn-vl-maybe-datatype-equiv-congruence-on-type

(defthm
 vl-expr-to-svex-maybe-typed-fn-vl-maybe-datatype-equiv-congruence-on-type
 (implies
   (vl-maybe-datatype-equiv type type-equiv)
   (equal
        (vl-expr-to-svex-maybe-typed-fn x type ss scopes compattype)
        (vl-expr-to-svex-maybe-typed-fn
             x type-equiv ss scopes compattype)))
 :rule-classes :congruence)

Theorem: vl-expr-to-svex-maybe-typed-fn-of-vl-scopestack-fix-ss

(defthm vl-expr-to-svex-maybe-typed-fn-of-vl-scopestack-fix-ss
 (equal
      (vl-expr-to-svex-maybe-typed-fn x type (vl-scopestack-fix ss)
                                      scopes compattype)
      (vl-expr-to-svex-maybe-typed-fn x type ss scopes compattype)))

Theorem: vl-expr-to-svex-maybe-typed-fn-vl-scopestack-equiv-congruence-on-ss

(defthm
 vl-expr-to-svex-maybe-typed-fn-vl-scopestack-equiv-congruence-on-ss
 (implies
   (vl-scopestack-equiv ss ss-equiv)
   (equal
        (vl-expr-to-svex-maybe-typed-fn x type ss scopes compattype)
        (vl-expr-to-svex-maybe-typed-fn
             x type ss-equiv scopes compattype)))
 :rule-classes :congruence)

Theorem: vl-expr-to-svex-maybe-typed-fn-of-vl-elabscopes-fix-scopes

(defthm vl-expr-to-svex-maybe-typed-fn-of-vl-elabscopes-fix-scopes
 (equal
      (vl-expr-to-svex-maybe-typed-fn
           x type ss (vl-elabscopes-fix scopes)
           compattype)
      (vl-expr-to-svex-maybe-typed-fn x type ss scopes compattype)))

Theorem: vl-expr-to-svex-maybe-typed-fn-vl-elabscopes-equiv-congruence-on-scopes

(defthm
 vl-expr-to-svex-maybe-typed-fn-vl-elabscopes-equiv-congruence-on-scopes
 (implies
   (vl-elabscopes-equiv scopes scopes-equiv)
   (equal
        (vl-expr-to-svex-maybe-typed-fn x type ss scopes compattype)
        (vl-expr-to-svex-maybe-typed-fn
             x type ss scopes-equiv compattype)))
 :rule-classes :congruence)

Theorem: vl-expr-to-svex-maybe-typed-fn-of-vl-typecompat-fix-compattype

(defthm
     vl-expr-to-svex-maybe-typed-fn-of-vl-typecompat-fix-compattype
 (equal
      (vl-expr-to-svex-maybe-typed-fn
           x type ss
           scopes (vl-typecompat-fix compattype))
      (vl-expr-to-svex-maybe-typed-fn x type ss scopes compattype)))

Theorem: vl-expr-to-svex-maybe-typed-fn-vl-typecompat-equiv-congruence-on-compattype

(defthm
 vl-expr-to-svex-maybe-typed-fn-vl-typecompat-equiv-congruence-on-compattype
 (implies
   (vl-typecompat-equiv compattype compattype-equiv)
   (equal
        (vl-expr-to-svex-maybe-typed-fn x type ss scopes compattype)
        (vl-expr-to-svex-maybe-typed-fn
             x type ss scopes compattype-equiv)))
 :rule-classes :congruence)