• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
        • Preprocessor
        • Vl-loadconfig
        • Lexer
        • Vl-loadstate
        • Parser
          • Parse-expressions
            • Vl-parse-parameter-value-assignment-hack
            • Vl-erange-p
            • Vl-mixed-binop-list-p
            • Vl-parse-very-simple-type
            • Vl-mark-as-explicit-parens
            • Vl-parse-0+-scope-prefixes
            • Vl-parse-0+-attribute-instances
            • Vl-parse-op
            • Vl-parse-hierarchical-identifier
            • Vl-parse-pva-tail
            • Vl-parse-expression-top
            • Vl-parse-any-sort-of-concatenation
            • Vl-build-indexing-nest
            • Vl-erangetypelist-p
            • Vl-build-range-select-with
            • Vl-build-range-select
            • Vl-parse-simple-type
            • Vl-expr-has-any-atts-p
            • Vl-left-associate-mixed-binop-list
            • Vl-tack-scopes-onto-hid
            • Vl-parse-op-alist-p
            • Vl-make-guts-from-inttoken
            • Vl-parse-range-expression
            • Vl-parse-slice-size
            • Vl-parse-concatenation
            • Vl-parse-stream-expression
            • Vl-parse-1+-stream-expressions-separated-by-commas
            • Vl-parse-stream-concatenation
            • Vl-parse-primary
            • Vl-parse-0+-bracketed-expressions
            • Vl-parse-system-function-call
            • Vl-parse-shift-expression-aux
            • Vl-parse-power-expression-aux
            • Vl-parse-mult-expression-aux
            • Vl-parse-mintypmax-expression
            • Vl-parse-logor-expression-aux
            • Vl-parse-logand-expression-aux
            • Vl-parse-indexed-id-2012
            • Vl-parse-indexed-id-2005
            • Vl-parse-equality-expression-aux
            • Vl-parse-equality-expression
            • Vl-parse-compare-expression-aux
            • Vl-parse-bitxor-expression-aux
            • Vl-parse-bitor-expression-aux
            • Vl-parse-bitand-expression-aux
            • Vl-parse-1+-open-value-ranges
            • Vl-parse-1+-keyval-expression-pairs
            • Vl-parse-unary-expression
            • Vl-parse-shift-expression
            • Vl-parse-qmark-expression
            • Vl-parse-primary-main
            • Vl-parse-primary-cast
            • Vl-parse-power-expression
            • Vl-parse-open-value-range
            • Vl-parse-nonprimary-cast
            • Vl-parse-mult-expression
            • Vl-parse-logor-expression
            • Vl-parse-logand-expression
            • Vl-parse-indexed-id
            • Vl-parse-impl-expression
            • Vl-parse-function-call
            • Vl-parse-expression
            • Vl-parse-compare-expression
            • Vl-parse-bitxor-expression
            • Vl-parse-bitor-expression
            • Vl-parse-bitand-expression
            • Vl-parse-assignment-pattern
            • Vl-parse-add-expression-aux
            • Vl-parse-add-expression
            • Vl-parse-1+-expressions-separated-by-commas
          • Parse-udps
          • Vl-genelements
          • Parse-paramdecls
          • Parse-blockitems
          • Parse-utils
          • Parse-insts
          • Parse-datatype
          • Parse-functions
          • Parse-datatypes
          • Parse-strengths
          • Vl-parse-genvar-declaration
          • Vl-parse
          • Parse-ports
          • Seq
          • Parse-packages
        • Vl-load-merge-descriptions
        • Scope-of-defines
        • Vl-load-file
        • Vl-flush-out-descriptions
        • Vl-description
        • Vl-loadresult
        • Vl-read-file
        • Vl-find-basename/extension
        • Vl-find-file
        • Vl-read-files
        • Extended-characters
        • Vl-load
        • Vl-load-main
        • Vl-load-description
        • Vl-descriptions-left-to-load
        • Inject-warnings
        • Vl-load-descriptions
        • Vl-load-files
        • Vl-load-summary
        • Vl-collect-modules-from-descriptions
        • Vl-descriptionlist
      • Transforms
      • Lint
      • Mlib
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Parse-expressions

Vl-build-indexing-nest

Build the proper expression for successive indexing operations.

Signature

(vl-build-indexing-nest expr indices) → expr

Arguments

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

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

Returns

expr — Type (vl-expr-p expr), given the guard.

Another operation which we want to left-associate is bit/part selection, which might also be called array or memory indexing. The idea is that for foo[1][2][3], we want to build an expression of the form:

(vl-index (vl-index (vl-index foo 1)
                    2))
          3)

This is easy because we are only dealing with one operation and no attributes, so we can just read the list of selects and then left-associate them.

Definitions and Theorems

Function: vl-build-indexing-nest

(defun vl-build-indexing-nest (expr indices)
  (declare (xargs :guard (and (vl-expr-p expr)
                              (vl-exprlist-p indices))))
  (let ((__function__ 'vl-build-indexing-nest))
    (declare (ignorable __function__))
    (if (atom indices)
        expr
      (vl-build-indexing-nest
           (make-vl-nonatom :op :vl-index
                            :args (list expr (car indices)))
           (cdr indices)))))

Theorem: vl-expr-p-of-vl-build-indexing-nest

(defthm vl-expr-p-of-vl-build-indexing-nest
  (implies (and (force (vl-expr-p expr))
                (force (vl-exprlist-p indices)))
           (b* ((expr (vl-build-indexing-nest expr indices)))
             (vl-expr-p expr)))
  :rule-classes :rewrite)