• 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
            • 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
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Sv::vl-expr.lisp

Vl-seltrace-to-svex-select

Signature

(vl-seltrace-to-svex-select x indices base-type base-svar outer-ss) 
  → 
(mv err select)

Arguments

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

indices — Guard (sv::svexlist-p indices).

base-type — The type of the variable that the selects are indexing into.
    Guard (vl-datatype-p base-type).

base-svar — Guard (sv::svar-p base-svar).

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

Returns

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

select — Type (implies (not err) (sv::svex-select-p select)).

Definitions and Theorems

Function: vl-seltrace-to-svex-select

(defun vl-seltrace-to-svex-select
       (x indices base-type base-svar outer-ss)
 (declare (xargs :guard (and (vl-seltrace-p x)
                             (sv::svexlist-p indices)
                             (vl-datatype-p base-type)
                             (sv::svar-p base-svar)
                             (vl-scopestack-p outer-ss))))
 (declare (xargs :guard (and (vl-seltrace-usertypes-ok x)
                             (vl-datatype-resolved-p base-type)
                             (>= (len indices)
                                 (vl-seltrace-index-count x)))))
 (let ((__function__ 'vl-seltrace-to-svex-select))
  (declare (ignorable __function__))
  (b*
   ((type (vl-seltrace-type x base-type))
    ((mv err size) (vl-datatype-size type))
    ((when err) (mv err nil))
    ((unless size)
     (mv (vmsg "Could not size datatype ~s0" type)
         nil))
    ((when (atom x))
     (mv nil
         (sv::make-svex-select-var :name base-svar
                                   :width size)))
    ((vl-selstep step) (car x))
    (rest-type (vl-seltrace-type (cdr x) base-type))
    (rest-type (vl-maybe-usertype-resolve rest-type))
    ((mv err shift-amt)
     (vl-select-case
          step.select :field
          (b* (((mv err idx)
                (vl-datatype-field-shift-amount
                     rest-type step.select.name))
               ((when err) (mv err idx)))
            (mv nil (svex-int idx)))
          :index
          (vl-datatype-index-shift-amount rest-type (car indices))))
    ((when err) (mv err nil))
    ((mv err rest)
     (vl-seltrace-to-svex-select
          (cdr x)
          (vl-select-case step.select
                          :field indices
                          :index (cdr indices))
          base-type base-svar outer-ss))
    ((when err) (mv err nil)))
   (mv err
       (sv::make-svex-select-part :lsb shift-amt
                                  :width size
                                  :subexp rest)))))

Theorem: return-type-of-vl-seltrace-to-svex-select.err

(defthm return-type-of-vl-seltrace-to-svex-select.err
  (b* (((mv ?err ?select)
        (vl-seltrace-to-svex-select
             x
             indices base-type base-svar outer-ss)))
    (iff (vl-msg-p err) err))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-seltrace-to-svex-select.select

(defthm return-type-of-vl-seltrace-to-svex-select.select
  (b* (((mv ?err ?select)
        (vl-seltrace-to-svex-select
             x
             indices base-type base-svar outer-ss)))
    (implies (not err)
             (sv::svex-select-p select)))
  :rule-classes :rewrite)

Theorem: vars-of-vl-seltrace-to-svex-select

(defthm vars-of-vl-seltrace-to-svex-select
 (b* (((mv ?err ?select)
       (vl-seltrace-to-svex-select
            x
            indices base-type base-svar outer-ss)))
  (implies
    (and (not (member v
                      (double-rewrite (sv::svexlist-vars indices))))
         (not (equal v (sv::svar-fix base-svar)))
         (not err))
    (not (member v (sv::svex-select-vars select))))))

Theorem: vl-seltrace-to-svex-select-of-vl-seltrace-fix-x

(defthm vl-seltrace-to-svex-select-of-vl-seltrace-fix-x
 (equal
   (vl-seltrace-to-svex-select (vl-seltrace-fix x)
                               indices base-type base-svar outer-ss)
   (vl-seltrace-to-svex-select
        x
        indices base-type base-svar outer-ss)))

Theorem: vl-seltrace-to-svex-select-vl-seltrace-equiv-congruence-on-x

(defthm vl-seltrace-to-svex-select-vl-seltrace-equiv-congruence-on-x
  (implies (vl-seltrace-equiv x x-equiv)
           (equal (vl-seltrace-to-svex-select
                       x indices base-type base-svar outer-ss)
                  (vl-seltrace-to-svex-select
                       x-equiv
                       indices base-type base-svar outer-ss)))
  :rule-classes :congruence)

Theorem: vl-seltrace-to-svex-select-of-svexlist-fix-indices

(defthm vl-seltrace-to-svex-select-of-svexlist-fix-indices
  (equal (vl-seltrace-to-svex-select x (sv::svexlist-fix indices)
                                     base-type base-svar outer-ss)
         (vl-seltrace-to-svex-select
              x
              indices base-type base-svar outer-ss)))

Theorem: vl-seltrace-to-svex-select-svexlist-equiv-congruence-on-indices

(defthm
    vl-seltrace-to-svex-select-svexlist-equiv-congruence-on-indices
 (implies
  (sv::svexlist-equiv indices indices-equiv)
  (equal (vl-seltrace-to-svex-select
              x indices base-type base-svar outer-ss)
         (vl-seltrace-to-svex-select x indices-equiv
                                     base-type base-svar outer-ss)))
 :rule-classes :congruence)

Theorem: vl-seltrace-to-svex-select-of-vl-datatype-fix-base-type

(defthm vl-seltrace-to-svex-select-of-vl-datatype-fix-base-type
 (equal
   (vl-seltrace-to-svex-select x indices (vl-datatype-fix base-type)
                               base-svar outer-ss)
   (vl-seltrace-to-svex-select
        x
        indices base-type base-svar outer-ss)))

Theorem: vl-seltrace-to-svex-select-vl-datatype-equiv-congruence-on-base-type

(defthm
 vl-seltrace-to-svex-select-vl-datatype-equiv-congruence-on-base-type
 (implies
  (vl-datatype-equiv base-type base-type-equiv)
  (equal
   (vl-seltrace-to-svex-select
        x indices base-type base-svar outer-ss)
   (vl-seltrace-to-svex-select x indices
                               base-type-equiv base-svar outer-ss)))
 :rule-classes :congruence)

Theorem: vl-seltrace-to-svex-select-of-svar-fix-base-svar

(defthm vl-seltrace-to-svex-select-of-svar-fix-base-svar
 (equal
      (vl-seltrace-to-svex-select x indices
                                  base-type (sv::svar-fix base-svar)
                                  outer-ss)
      (vl-seltrace-to-svex-select
           x
           indices base-type base-svar outer-ss)))

Theorem: vl-seltrace-to-svex-select-svar-equiv-congruence-on-base-svar

(defthm
      vl-seltrace-to-svex-select-svar-equiv-congruence-on-base-svar
 (implies
  (sv::svar-equiv base-svar base-svar-equiv)
  (equal
   (vl-seltrace-to-svex-select
        x indices base-type base-svar outer-ss)
   (vl-seltrace-to-svex-select x indices
                               base-type base-svar-equiv outer-ss)))
 :rule-classes :congruence)

Theorem: vl-seltrace-to-svex-select-of-vl-scopestack-fix-outer-ss

(defthm vl-seltrace-to-svex-select-of-vl-scopestack-fix-outer-ss
  (equal (vl-seltrace-to-svex-select
              x indices base-type
              base-svar (vl-scopestack-fix outer-ss))
         (vl-seltrace-to-svex-select
              x
              indices base-type base-svar outer-ss)))

Theorem: vl-seltrace-to-svex-select-vl-scopestack-equiv-congruence-on-outer-ss

(defthm
 vl-seltrace-to-svex-select-vl-scopestack-equiv-congruence-on-outer-ss
 (implies
  (vl-scopestack-equiv outer-ss outer-ss-equiv)
  (equal
   (vl-seltrace-to-svex-select
        x indices base-type base-svar outer-ss)
   (vl-seltrace-to-svex-select x indices
                               base-type base-svar outer-ss-equiv)))
 :rule-classes :congruence)