• 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-operandinfo-to-svex-preproc

Preprocesses an operandinfo, changing an outer bitselect or partselect into a +: style partselect.

Signature

(vl-operandinfo-to-svex-preproc x indices) 
  → 
(mv err new-x new-indices)

Arguments

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

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

Returns

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

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

new-indices — Type (sv::svexlist-p new-indices).

This is just a code-simplifying step so that we don't have to deal with so many separate cases later.

Note: This function's correctness depends on the ordering in which indices are listed by vl-operandinfo->indices, so keep these two functions in sync.

The result is an operandinfo with the following characteristics:

• The select trace has no bitselect; it's just vector-level operations all the way.
• If we have a partselect, it's a plusminus select with resolved width.

Definitions and Theorems

Function: vl-operandinfo-to-svex-preproc

(defun vl-operandinfo-to-svex-preproc (x indices)
 (declare (xargs :guard (and (vl-operandinfo-p x)
                             (sv::svexlist-p indices))))
 (declare
      (xargs :guard (and (vl-operandinfo-usertypes-ok x)
                         (equal (len indices)
                                (vl-operandinfo-index-count x)))))
 (let ((__function__ 'vl-operandinfo-to-svex-preproc))
  (declare (ignorable __function__))
  (b* ((indices (sv::svexlist-fix indices))
       ((vl-operandinfo x)
        (vl-operandinfo-fix x)))
   (vl-partselect-case
    x.part :none
    (b* (((when (atom x.seltrace))
          (mv nil x indices))
         ((vl-selstep sel1) (car x.seltrace))
         ((unless (vl-select-case sel1.select :index))
          (mv nil x indices))
         (type (vl-seltrace-type (cdr x.seltrace)
                                 x.hidtype))
         ((unless (vl-datatype-index-is-bitselect type))
          (mv nil x indices))
         ((vl-select-index idx) sel1.select)
         ((cons bitselect-index rest-indices)
          indices))
     (mv nil
         (change-vl-operandinfo
              x
              :seltrace (cdr x.seltrace)
              :part (vl-plusminus->partselect
                         (make-vl-plusminus :width (vl-make-index 1)
                                            :base idx.val)))
         (list* (sv::svex-fix bitselect-index)
                (svex-int 1)
                rest-indices)))
    :range
    (b*
     (((list* ?msb-index ?lsb-index rest-indices)
       indices)
      ((unless (and (vl-expr-resolved-p x.part.msb)
                    (vl-expr-resolved-p x.part.lsb)))
       (mv (vmsg "Unresolved partselect range")
           x indices))
      (msb (vl-resolved->val x.part.msb))
      (lsb (vl-resolved->val x.part.lsb))
      (minusp (< msb lsb))
      (width (+ 1 (abs (- msb lsb))))
      (new-part (vl-plusminus->partselect
                     (make-vl-plusminus :base x.part.lsb
                                        :width (vl-make-index width)
                                        :minusp minusp))))
     (mv nil
         (change-vl-operandinfo x :part new-part)
         (list* (svex-int lsb)
                (svex-int width)
                rest-indices)))
    :plusminus
    (b*
     (((unless (b* ((width (cadr indices)))
                 (sv::svex-case
                      width
                      :quote (and (sv::2vec-p width.val)
                                  (natp (sv::2vec->val width.val)))
                      :otherwise nil)))
       (mv (vmsg "Unresolved plusminus select width")
           x indices)))
     (mv nil x indices))))))

Theorem: return-type-of-vl-operandinfo-to-svex-preproc.err

(defthm return-type-of-vl-operandinfo-to-svex-preproc.err
  (b* (((mv ?err ?new-x ?new-indices)
        (vl-operandinfo-to-svex-preproc x indices)))
    (iff (vl-msg-p err) err))
  :rule-classes :rewrite)

Theorem: vl-operandinfo-p-of-vl-operandinfo-to-svex-preproc.new-x

(defthm vl-operandinfo-p-of-vl-operandinfo-to-svex-preproc.new-x
  (b* (((mv ?err ?new-x ?new-indices)
        (vl-operandinfo-to-svex-preproc x indices)))
    (vl-operandinfo-p new-x))
  :rule-classes :rewrite)

Theorem: svexlist-p-of-vl-operandinfo-to-svex-preproc.new-indices

(defthm svexlist-p-of-vl-operandinfo-to-svex-preproc.new-indices
  (b* (((mv ?err ?new-x ?new-indices)
        (vl-operandinfo-to-svex-preproc x indices)))
    (sv::svexlist-p new-indices))
  :rule-classes :rewrite)

Theorem: vl-operandinfo-usertypes-ok-of-vl-operandinfo-to-svex-preproc

(defthm
      vl-operandinfo-usertypes-ok-of-vl-operandinfo-to-svex-preproc
  (b* (((mv ?err ?new-x ?new-indices)
        (vl-operandinfo-to-svex-preproc x indices)))
    (implies (vl-operandinfo-usertypes-ok x)
             (vl-operandinfo-usertypes-ok new-x))))

Theorem: len-indices-of-vl-operandinfo-to-svex-preproc

(defthm len-indices-of-vl-operandinfo-to-svex-preproc
  (b* (((mv ?err ?new-x ?new-indices)
        (vl-operandinfo-to-svex-preproc x indices)))
    (implies (equal (len indices)
                    (vl-operandinfo-index-count x))
             (equal (len new-indices)
                    (vl-operandinfo-index-count new-x)))))

Theorem: partselect-kind-of-vl-operandinfo-to-svex-preproc

(defthm partselect-kind-of-vl-operandinfo-to-svex-preproc
 (b* (((mv ?err ?new-x ?new-indices)
       (vl-operandinfo-to-svex-preproc x indices)))
   (implies
        (not err)
        (or (equal (vl-partselect-kind (vl-operandinfo->part new-x))
                   :none)
            (equal (vl-partselect-kind (vl-operandinfo->part new-x))
                   :plusminus))))
 :rule-classes
 ((:forward-chaining
   :trigger-terms
   ((vl-partselect-kind
      (vl-operandinfo->part
           (mv-nth 1
                   (vl-operandinfo-to-svex-preproc x indices))))))))

Theorem: vars-of-vl-operandinfo-to-svex-preproc

(defthm vars-of-vl-operandinfo-to-svex-preproc
  (b* (((mv ?err ?new-x ?new-indices)
        (vl-operandinfo-to-svex-preproc x indices)))
    (implies (not (member v (sv::svexlist-vars indices)))
             (not (member v (sv::svexlist-vars new-indices))))))

Theorem: constant-width-of-vl-operandinfo-to-svex-preproc-width

(defthm constant-width-of-vl-operandinfo-to-svex-preproc-width
 (b* (((mv ?err ?new-x ?new-indices)
       (vl-operandinfo-to-svex-preproc x indices)))
  (implies
   (and
       (not err)
       (not (equal (vl-partselect-kind (vl-operandinfo->part new-x))
                   :none)))
   (b* ((sv::width (cadr new-indices)))
    (and
       (equal (sv::svex-kind sv::width) :quote)
       (equal (sv::4vec->lower (sv::svex-quote->val sv::width))
              (sv::4vec->upper (sv::svex-quote->val sv::width)))
       (natp (sv::4vec->upper (sv::svex-quote->val sv::width))))))))

Theorem: vl-operandinfo-to-svex-preproc-of-vl-operandinfo-fix-x

(defthm vl-operandinfo-to-svex-preproc-of-vl-operandinfo-fix-x
  (equal (vl-operandinfo-to-svex-preproc (vl-operandinfo-fix x)
                                         indices)
         (vl-operandinfo-to-svex-preproc x indices)))

Theorem: vl-operandinfo-to-svex-preproc-vl-operandinfo-equiv-congruence-on-x

(defthm
 vl-operandinfo-to-svex-preproc-vl-operandinfo-equiv-congruence-on-x
 (implies (vl-operandinfo-equiv x x-equiv)
          (equal (vl-operandinfo-to-svex-preproc x indices)
                 (vl-operandinfo-to-svex-preproc x-equiv indices)))
 :rule-classes :congruence)

Theorem: vl-operandinfo-to-svex-preproc-of-svexlist-fix-indices

(defthm vl-operandinfo-to-svex-preproc-of-svexlist-fix-indices
  (equal
       (vl-operandinfo-to-svex-preproc x (sv::svexlist-fix indices))
       (vl-operandinfo-to-svex-preproc x indices)))

Theorem: vl-operandinfo-to-svex-preproc-svexlist-equiv-congruence-on-indices

(defthm
 vl-operandinfo-to-svex-preproc-svexlist-equiv-congruence-on-indices
 (implies (sv::svexlist-equiv indices indices-equiv)
          (equal (vl-operandinfo-to-svex-preproc x indices)
                 (vl-operandinfo-to-svex-preproc x indices-equiv)))
 :rule-classes :congruence)