• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • Vl
      • Syntax
      • Loader
      • Warnings
      • Getting-started
      • Utilities
      • Printer
      • Kit
      • Mlib
        • Scopestack
        • Hid-tools
          • Vl-follow-hidexpr
          • Vl-index-expr-typetrace
          • Vl-follow-scopeexpr
          • Vl-follow-hidexpr-dimscheck
          • Vl-datatype-resolve-selects
          • Vl-datatype-remove-dim
          • Vl-operandinfo
          • Vl-follow-hidexpr-dimcheck
          • Vl-follow-data-selects
          • Vl-follow-hidexpr-error
          • Vl-hidstep
          • Vl-scopestack-find-item/ss/path
          • Vl-follow-array-indices
          • Vl-scopecontext
          • Vl-datatype-set-unsigned
          • Vl-selstep
          • Vl-scopestack-find-elabpath
          • Vl-hid-prefix-for-subhid
          • Vl-find-structmember
          • Vl-select
          • Vl-scopeexpr-replace-hid
          • Vl-genblocklist-find-block
          • Vl-partselect-width
          • Vl-seltrace->indices
          • Vl-datatype->structmembers
          • Vl-hidexpr-resolved-p
          • Vl-operandinfo->indices
          • Vl-flatten-hidindex
          • Vl-subhid-p
          • Vl-seltrace-usertypes-ok
          • Vl-flatten-hidexpr
          • Vl-scopeexpr->hid
          • Vl-seltrace-index-count
          • Vl-operandinfo-usertypes-ok
          • Vl-operandinfo-index-count
          • Vl-datatype-dims-count
          • Vl-scopeexpr-index-count
          • Vl-hidexpr-index-count
          • Vl-usertype-lookup
          • Vl-hidindex-resolved-p
          • Vl-scopeexpr-resolved-p
          • Vl-selstep-usertypes-ok
          • Vl-hidtrace
          • Vl-seltrace
          • Vl-scopedef-interface-p
        • Filtering-by-name
        • Vl-interface-mocktype
        • Stripping-functions
        • Genblob
        • Expr-tools
        • Extract-vl-types
        • Hierarchy
        • Range-tools
        • Finding-by-name
        • Stmt-tools
        • Modnamespace
        • Flat-warnings
        • Reordering-by-name
        • Datatype-tools
        • Syscalls
        • Allexprs
        • Lvalues
        • Port-tools
      • Transforms
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Hid-tools

Vl-datatype-resolve-selects

Signature

(vl-datatype-resolve-selects type tail indices part) 
  → 
(mv err seltrace finaltype)

Arguments

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

tail — Guard (vl-hidexpr-p tail).

indices — Guard (vl-exprlist-p indices).

part — Guard (vl-partselect-p part).

Returns

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

seltrace — Type (implies (not err) (vl-seltrace-p seltrace)).

finaltype — Type (implies (not err) (vl-datatype-p finaltype)).

Definitions and Theorems

Function: vl-datatype-resolve-selects

(defun vl-datatype-resolve-selects (type tail indices part)
 (declare (xargs :guard (and (vl-datatype-p type)
                             (vl-hidexpr-p tail)
                             (vl-exprlist-p indices)
                             (vl-partselect-p part))))
 (declare (xargs :guard (vl-datatype-resolved-p type)))
 (let ((__function__ 'vl-datatype-resolve-selects))
  (declare (ignorable __function__))
  (b* (((mv err seltrace)
        (vl-follow-data-selects tail type nil))
       ((when err) (mv err nil nil))
       (type (vl-datatype-fix type))
       (seltype (if (consp seltrace)
                    (b* (((vl-selstep selstep) (car seltrace)))
                      selstep.type)
                  type))
       ((mv err rev-idxtrace)
        (vl-follow-array-indices indices seltype))
       ((when err) (mv err nil nil))
       (seltrace (revappend rev-idxtrace seltrace))
       (seltype (if (consp seltrace)
                    (b* (((vl-selstep selstep) (car seltrace)))
                      selstep.type)
                  type))
       ((when (vl-partselect-case part :none))
        (mv nil seltrace seltype))
       ((mv err ?caveat single-type &)
        (vl-datatype-remove-dim seltype))
       ((when err) (mv err nil nil))
       ((mv err width)
        (vl-partselect-width part))
       ((when err) (mv err nil nil))
       (new-dim (vl-range->dimension
                     (make-vl-range :msb (vl-make-index (1- width))
                                    :lsb (vl-make-index 0))))
       (packedp (vl-datatype-packedp seltype))
       (psel-type
            (if packedp (vl-datatype-update-pdims
                             (cons new-dim
                                   (vl-datatype->pdims single-type))
                             single-type)
              (vl-datatype-update-udims
                   (cons new-dim
                         (vl-datatype->udims single-type))
                   single-type))))
    (mv nil seltrace psel-type))))

Theorem: return-type-of-vl-datatype-resolve-selects.err

(defthm return-type-of-vl-datatype-resolve-selects.err
  (b* (((mv ?err ?seltrace ?finaltype)
        (vl-datatype-resolve-selects type tail indices part)))
    (iff (vl-msg-p err) err))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-datatype-resolve-selects.seltrace

(defthm return-type-of-vl-datatype-resolve-selects.seltrace
  (b* (((mv ?err ?seltrace ?finaltype)
        (vl-datatype-resolve-selects type tail indices part)))
    (implies (not err)
             (vl-seltrace-p seltrace)))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-datatype-resolve-selects.finaltype

(defthm return-type-of-vl-datatype-resolve-selects.finaltype
  (b* (((mv ?err ?seltrace ?finaltype)
        (vl-datatype-resolve-selects type tail indices part)))
    (implies (not err)
             (vl-datatype-p finaltype)))
  :rule-classes :rewrite)

Theorem: vl-seltrace-usertypes-ok-of-vl-datatype-resolve-selects

(defthm vl-seltrace-usertypes-ok-of-vl-datatype-resolve-selects
  (b* (((mv ?err ?seltrace ?finaltype)
        (vl-datatype-resolve-selects type tail indices part)))
    (implies (and (not err)
                  (vl-datatype-resolved-p type))
             (vl-seltrace-usertypes-ok seltrace))))

Theorem: vl-datatype-resolved-p-of-vl-datatype-resolve-selects

(defthm vl-datatype-resolved-p-of-vl-datatype-resolve-selects
  (b* (((mv ?err ?seltrace ?finaltype)
        (vl-datatype-resolve-selects type tail indices part)))
    (implies (and (not err)
                  (vl-datatype-resolved-p type))
             (vl-datatype-resolved-p finaltype))))

Theorem: vl-seltrace-count-of-vl-datatype-resolve-selects

(defthm vl-seltrace-count-of-vl-datatype-resolve-selects
  (b* (((mv ?err ?seltrace ?finaltype)
        (vl-datatype-resolve-selects type tail indices part)))
    (implies (not err)
             (< (vl-exprlist-count (vl-seltrace->indices seltrace))
                (+ (vl-exprlist-count indices)
                   (vl-hidexpr-count tail)))))
  :rule-classes :linear)

Theorem: vl-datatype-resolve-selects-of-vl-datatype-fix-type

(defthm vl-datatype-resolve-selects-of-vl-datatype-fix-type
  (equal (vl-datatype-resolve-selects (vl-datatype-fix type)
                                      tail indices part)
         (vl-datatype-resolve-selects type tail indices part)))

Theorem: vl-datatype-resolve-selects-vl-datatype-equiv-congruence-on-type

(defthm
   vl-datatype-resolve-selects-vl-datatype-equiv-congruence-on-type
 (implies
   (vl-datatype-equiv type type-equiv)
   (equal
        (vl-datatype-resolve-selects type tail indices part)
        (vl-datatype-resolve-selects type-equiv tail indices part)))
 :rule-classes :congruence)

Theorem: vl-datatype-resolve-selects-of-vl-hidexpr-fix-tail

(defthm vl-datatype-resolve-selects-of-vl-hidexpr-fix-tail
  (equal (vl-datatype-resolve-selects type (vl-hidexpr-fix tail)
                                      indices part)
         (vl-datatype-resolve-selects type tail indices part)))

Theorem: vl-datatype-resolve-selects-vl-hidexpr-equiv-congruence-on-tail

(defthm
    vl-datatype-resolve-selects-vl-hidexpr-equiv-congruence-on-tail
 (implies
   (vl-hidexpr-equiv tail tail-equiv)
   (equal
        (vl-datatype-resolve-selects type tail indices part)
        (vl-datatype-resolve-selects type tail-equiv indices part)))
 :rule-classes :congruence)

Theorem: vl-datatype-resolve-selects-of-vl-exprlist-fix-indices

(defthm vl-datatype-resolve-selects-of-vl-exprlist-fix-indices
 (equal
    (vl-datatype-resolve-selects type tail (vl-exprlist-fix indices)
                                 part)
    (vl-datatype-resolve-selects type tail indices part)))

Theorem: vl-datatype-resolve-selects-vl-exprlist-equiv-congruence-on-indices

(defthm
 vl-datatype-resolve-selects-vl-exprlist-equiv-congruence-on-indices
 (implies
   (vl-exprlist-equiv indices indices-equiv)
   (equal
        (vl-datatype-resolve-selects type tail indices part)
        (vl-datatype-resolve-selects type tail indices-equiv part)))
 :rule-classes :congruence)

Theorem: vl-datatype-resolve-selects-of-vl-partselect-fix-part

(defthm vl-datatype-resolve-selects-of-vl-partselect-fix-part
  (equal (vl-datatype-resolve-selects
              type
              tail indices (vl-partselect-fix part))
         (vl-datatype-resolve-selects type tail indices part)))

Theorem: vl-datatype-resolve-selects-vl-partselect-equiv-congruence-on-part

(defthm
 vl-datatype-resolve-selects-vl-partselect-equiv-congruence-on-part
 (implies
   (vl-partselect-equiv part part-equiv)
   (equal
        (vl-datatype-resolve-selects type tail indices part)
        (vl-datatype-resolve-selects type tail indices part-equiv)))
 :rule-classes :congruence)