• 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
            • 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-arrayrange->rel-lsb-and-width

Signature

(vl-arrayrange->rel-lsb-and-width x dim-lsb dim-msb) 
  → 
(mv err rel-lsb width)

Arguments

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

dim-lsb — Guard (natp dim-lsb).

dim-msb — Guard (natp dim-msb).

Returns

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

rel-lsb — Type (implies (not err) (natp rel-lsb)).

width — Type (implies (not err) (posp width)).

Definitions and Theorems

Function: vl-arrayrange->rel-lsb-and-width

(defun vl-arrayrange->rel-lsb-and-width (x dim-lsb dim-msb)
  (declare (xargs :guard (and (vl-arrayrange-p x)
                              (natp dim-lsb)
                              (natp dim-msb))))
  (declare (xargs :guard (not (vl-arrayrange-case x :none))))
  (let ((__function__ 'vl-arrayrange->rel-lsb-and-width))
    (declare (ignorable __function__))
    (b* ((dim-lsb (lnfix dim-lsb))
         (dim-msb (lnfix dim-msb)))
      (vl-arrayrange-case
           x :range
           (b* (((unless (and (vl-expr-resolved-p x.lsb)
                              (vl-expr-resolved-p x.msb)))
                 (mv "Array range not resolved" nil nil))
                (sel-lsb (vl-resolved->val x.lsb))
                (sel-msb (vl-resolved->val x.msb))
                ((when (or (and (< sel-lsb sel-msb)
                                (< dim-msb dim-lsb))
                           (and (> sel-lsb sel-msb)
                                (> dim-msb dim-lsb))))
                 (mv "Reversed array range" nil nil))
                ((unless (or (and (<= dim-lsb sel-lsb)
                                  (<= sel-msb dim-msb))
                             (and (>= dim-lsb sel-lsb)
                                  (>= sel-msb dim-msb))))
                 (mv "Range indices out of bounds" nil nil))
                (rel-lsb (abs (- sel-lsb dim-lsb)))
                (width (+ 1 (abs (- sel-msb sel-lsb)))))
             (mv nil rel-lsb width))
           :index
           (b* (((unless (vl-expr-resolved-p x.expr))
                 (mv "Array index not resolved" nil nil))
                (sel (vl-resolved->val x.expr))
                ((unless (or (and (<= dim-lsb sel) (<= sel dim-msb))
                             (and (>= dim-lsb sel)
                                  (>= sel dim-msb))))
                 (mv "Range index out of bounds" nil nil))
                (rel-lsb (abs (- sel dim-lsb)))
                (width 1))
             (mv nil rel-lsb width))
           :plusminus
           (b* (((unless (and (vl-expr-resolved-p x.width)
                              (vl-expr-resolved-p x.base)))
                 (mv "Array range not resolved" nil nil))
                (sel-base (vl-resolved->val x.base))
                (sel-width (vl-resolved->val x.width))
                ((unless (> sel-width 0))
                 (mv "Range width zero" nil nil))
                (sel-end (if x.minusp (- sel-base (- sel-width 1))
                           (+ sel-base (- sel-width 1))))
                ((unless (if (< dim-lsb dim-msb)
                             (and (<= dim-lsb sel-base)
                                  (<= dim-lsb sel-end)
                                  (<= sel-base dim-msb)
                                  (<= sel-end dim-msb))
                           (and (<= dim-msb sel-base)
                                (<= dim-msb sel-end)
                                (<= sel-base dim-lsb)
                                (<= sel-end dim-lsb))))
                 (mv "Range indices out of bounds" nil nil))
                (rel-lsb (min (abs (- sel-base dim-lsb))
                              (abs (- sel-end dim-lsb)))))
             (mv nil rel-lsb sel-width))
           :otherwise (prog2$ (impossible)
                              (mv "impossible" nil nil))))))

Theorem: return-type-of-vl-arrayrange->rel-lsb-and-width.err

(defthm return-type-of-vl-arrayrange->rel-lsb-and-width.err
  (b* (((mv ?err ?rel-lsb ?width)
        (vl-arrayrange->rel-lsb-and-width x dim-lsb dim-msb)))
    (iff (vl-msg-p err) err))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-arrayrange->rel-lsb-and-width.rel-lsb

(defthm return-type-of-vl-arrayrange->rel-lsb-and-width.rel-lsb
  (b* (((mv ?err ?rel-lsb ?width)
        (vl-arrayrange->rel-lsb-and-width x dim-lsb dim-msb)))
    (implies (not err) (natp rel-lsb)))
  :rule-classes :type-prescription)

Theorem: return-type-of-vl-arrayrange->rel-lsb-and-width.width

(defthm return-type-of-vl-arrayrange->rel-lsb-and-width.width
  (b* (((mv ?err ?rel-lsb ?width)
        (vl-arrayrange->rel-lsb-and-width x dim-lsb dim-msb)))
    (implies (not err) (posp width)))
  :rule-classes :type-prescription)

Theorem: vl-arrayrange->rel-lsb-and-width-of-vl-arrayrange-fix-x

(defthm vl-arrayrange->rel-lsb-and-width-of-vl-arrayrange-fix-x
  (equal (vl-arrayrange->rel-lsb-and-width (vl-arrayrange-fix x)
                                           dim-lsb dim-msb)
         (vl-arrayrange->rel-lsb-and-width x dim-lsb dim-msb)))

Theorem: vl-arrayrange->rel-lsb-and-width-vl-arrayrange-equiv-congruence-on-x

(defthm
 vl-arrayrange->rel-lsb-and-width-vl-arrayrange-equiv-congruence-on-x
 (implies
   (vl-arrayrange-equiv x x-equiv)
   (equal
        (vl-arrayrange->rel-lsb-and-width x dim-lsb dim-msb)
        (vl-arrayrange->rel-lsb-and-width x-equiv dim-lsb dim-msb)))
 :rule-classes :congruence)

Theorem: vl-arrayrange->rel-lsb-and-width-of-nfix-dim-lsb

(defthm vl-arrayrange->rel-lsb-and-width-of-nfix-dim-lsb
  (equal (vl-arrayrange->rel-lsb-and-width x (nfix dim-lsb)
                                           dim-msb)
         (vl-arrayrange->rel-lsb-and-width x dim-lsb dim-msb)))

Theorem: vl-arrayrange->rel-lsb-and-width-nat-equiv-congruence-on-dim-lsb

(defthm
   vl-arrayrange->rel-lsb-and-width-nat-equiv-congruence-on-dim-lsb
 (implies
   (acl2::nat-equiv dim-lsb dim-lsb-equiv)
   (equal
        (vl-arrayrange->rel-lsb-and-width x dim-lsb dim-msb)
        (vl-arrayrange->rel-lsb-and-width x dim-lsb-equiv dim-msb)))
 :rule-classes :congruence)

Theorem: vl-arrayrange->rel-lsb-and-width-of-nfix-dim-msb

(defthm vl-arrayrange->rel-lsb-and-width-of-nfix-dim-msb
  (equal (vl-arrayrange->rel-lsb-and-width x dim-lsb (nfix dim-msb))
         (vl-arrayrange->rel-lsb-and-width x dim-lsb dim-msb)))

Theorem: vl-arrayrange->rel-lsb-and-width-nat-equiv-congruence-on-dim-msb

(defthm
   vl-arrayrange->rel-lsb-and-width-nat-equiv-congruence-on-dim-msb
 (implies
   (acl2::nat-equiv dim-msb dim-msb-equiv)
   (equal
        (vl-arrayrange->rel-lsb-and-width x dim-lsb dim-msb)
        (vl-arrayrange->rel-lsb-and-width x dim-lsb dim-msb-equiv)))
 :rule-classes :congruence)