• 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
      • Transforms
      • Lint
      • Mlib
        • Scopestack
        • Filtering-by-name
        • Vl-namefactory
        • Substitution
        • Allexprs
        • Hid-tools
        • Vl-consteval
        • Range-tools
        • Lvalexprs
        • Hierarchy
        • Finding-by-name
        • Expr-tools
        • Expr-slicing
        • Stripping-functions
        • Stmt-tools
        • Modnamespace
        • Vl-parse-expr-from-str
        • Welltyped
        • Reordering-by-name
        • Flat-warnings
        • Genblob
        • Expr-building
        • Datatype-tools
        • Syscalls
        • Relocate
        • Expr-cleaning
          • Vl-exprlist-clean-selects
          • Vl-expr-clean-selects1
          • Vl-maybe-merge-selects-aux
          • Vl-merge-consts
            • Vl-merge-consts-aux
          • Vl-maybe-merge-selects
          • Vl-expr-clean-selects
          • Vl-elim-nested-concats
          • Vl-expr-clean-concats
        • Namemangle
        • Caremask
        • Port-tools
        • Lvalues
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Expr-cleaning

Vl-merge-consts

Consolidate concatenations of constants.

Signature

(vl-merge-consts x) → new-x

Arguments

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

Returns

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

(vl-merge-consts-aux x) returns (mv startwidth startval weirdval rest).

Startwidth is the width of the initial sequence of constants. If this initial sequence involves any bits which are Z or X, then weirdval is a vl-bitlist-p whose value is the same as the bits of this initial sequence, and startval is nil. Otherwise, weirdval is nil and startval is the value of the initial sequence. Rest is the remaining expressions, with constants consolidated.

Example: Suppose we have { 2'h3, 4'ha, foo[4:3], 6'h3a, 8'h10 }. Running vl-merge-consts-aux on this yields

STARTWIDTH = 6      ;; sum of widths of initial constants
STARTVAL = 53       ;; hex 3a, value of concatenated initial constants
WEIRDVAL = nil
REST = { foo[4:3], 14'ha10 }
                    ;; remaining exprs, constants consolidated

If we have { 2'b1x, 4'ha, foo[4:3], 6'h3a, 8'h10 }. Running vl-merge-consts-aux on this yields

STARTWIDTH = 6      ;; sum of widths of initial constants
STARTVAL = nil
WEIRDVAL = bits 1x1010
REST = { foo[4:3], 14'ha10 }
                    ;; remaining exprs, constants consolidated

Theorem: return-type-of-vl-merge-consts.new-x

(defthm return-type-of-vl-merge-consts.new-x
  (b* ((?new-x (vl-merge-consts x)))
    (vl-exprlist-p new-x))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-merge-consts-aux.startwidth

(defthm return-type-of-vl-merge-consts-aux.startwidth
  (b* (((mv ?startwidth
            ?startval ?weirdval common-lisp::?rest)
        (vl-merge-consts-aux x)))
    (natp startwidth))
  :rule-classes :type-prescription)

Theorem: return-type-of-vl-merge-consts-aux.startval

(defthm return-type-of-vl-merge-consts-aux.startval
  (b* (((mv ?startwidth
            ?startval ?weirdval common-lisp::?rest)
        (vl-merge-consts-aux x)))
    (maybe-natp startval))
  :rule-classes :type-prescription)

Theorem: return-type-of-vl-merge-consts-aux.weirdval

(defthm return-type-of-vl-merge-consts-aux.weirdval
  (b* (((mv ?startwidth
            ?startval ?weirdval common-lisp::?rest)
        (vl-merge-consts-aux x)))
    (vl-bitlist-p weirdval))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-merge-consts-aux.rest

(defthm return-type-of-vl-merge-consts-aux.rest
  (b* (((mv ?startwidth
            ?startval ?weirdval common-lisp::?rest)
        (vl-merge-consts-aux x)))
    (vl-exprlist-p rest))
  :rule-classes :rewrite)

Theorem: true-listp-of-vl-merge-consts-aux->exprs

(defthm true-listp-of-vl-merge-consts-aux->exprs
  (true-listp (mv-nth 3 (vl-merge-consts-aux x)))
  :rule-classes :type-prescription)

Theorem: true-listp-of-vl-merge-consts->exprs

(defthm true-listp-of-vl-merge-consts->exprs
  (true-listp (vl-merge-consts x))
  :rule-classes :type-prescription)

Theorem: vl-merge-consts-aux-invar

(defthm vl-merge-consts-aux-invar
  (b* (((mv width val bits ?exprs)
        (vl-merge-consts-aux x)))
    (and (implies val (not bits))
         (implies (not val)
                  (equal (len bits) width))
         (implies val (< val (expt 2 width))))))

Theorem: vl-merge-consts-of-vl-exprlist-fix-x

(defthm vl-merge-consts-of-vl-exprlist-fix-x
  (equal (vl-merge-consts (vl-exprlist-fix x))
         (vl-merge-consts x)))

Theorem: vl-merge-consts-aux-of-vl-exprlist-fix-x

(defthm vl-merge-consts-aux-of-vl-exprlist-fix-x
  (equal (vl-merge-consts-aux (vl-exprlist-fix x))
         (vl-merge-consts-aux x)))

Theorem: vl-merge-consts-vl-exprlist-equiv-congruence-on-x

(defthm vl-merge-consts-vl-exprlist-equiv-congruence-on-x
  (implies (vl-exprlist-equiv x x-equiv)
           (equal (vl-merge-consts x)
                  (vl-merge-consts x-equiv)))
  :rule-classes :congruence)

Theorem: vl-merge-consts-aux-vl-exprlist-equiv-congruence-on-x

(defthm vl-merge-consts-aux-vl-exprlist-equiv-congruence-on-x
  (implies (vl-exprlist-equiv x x-equiv)
           (equal (vl-merge-consts-aux x)
                  (vl-merge-consts-aux x-equiv)))
  :rule-classes :congruence)

Subtopics

Vl-merge-consts-aux