• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • 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
          • Vl-expr-sliceable-p
          • Vl-msb-bitslice-expr
            • Vl-msb-bitslice-partselect
            • Vl-msb-bitslice-hidexpr
            • Vl-msb-bitslice-hidexpr-base
            • Vl-msb-bitslice-weirdint
            • Vl-msb-bitslice-constint
            • Vl-msb-bitslice-exprlist
        • 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
        • Namemangle
        • Caremask
        • Port-tools
        • Lvalues
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Expr-slicing

Vl-msb-bitslice-expr

Explode a well-typed, sliceable expression into a list of MSB-ordered, single-bit expressions.

Signature

(vl-msb-bitslice-expr x ss warnings) 
  → 
(mv successp warnings bit-exprs)

Arguments

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

ss — Guard (vl-scopestack-p ss).

warnings — Guard (vl-warninglist-p warnings).

Returns

successp — Type (booleanp successp).

warnings — Type (vl-warninglist-p warnings).

bit-exprs — Type (true-listp bit-exprs).

We require that X is a well-typed expression, i.e., our expression-sizing transform should have already been run. On success, we split the expression into its individual bits, and as basic correctness properties, we prove that on success the resulting bits is a list of well-typed expressions where:

• (len bits) is the finalwidth of x, and
• each bit_i is unsigned and has a finalwidth of 1.

The only reason this function will fail is if some identifier within x is not declared in the module or has a finalwidth that is smaller than its declared width. These situations should not arise in practice if the expressions have been sized correctly.

Theorem: return-type-of-vl-msb-bitslice-expr.successp

(defthm return-type-of-vl-msb-bitslice-expr.successp
  (b* (((mv ?successp ?warnings ?bit-exprs)
        (vl-msb-bitslice-expr x ss warnings)))
    (booleanp successp))
  :rule-classes :type-prescription)

Theorem: return-type-of-vl-msb-bitslice-expr.warnings

(defthm return-type-of-vl-msb-bitslice-expr.warnings
  (b* (((mv ?successp ?warnings ?bit-exprs)
        (vl-msb-bitslice-expr x ss warnings)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-msb-bitslice-expr.bit-exprs

(defthm return-type-of-vl-msb-bitslice-expr.bit-exprs
  (b* (((mv ?successp ?warnings ?bit-exprs)
        (vl-msb-bitslice-expr x ss warnings)))
    (true-listp bit-exprs))
  :rule-classes :type-prescription)

Theorem: return-type-of-vl-msb-bitslice-exprlist.successp

(defthm return-type-of-vl-msb-bitslice-exprlist.successp
  (b* (((mv ?successp ?warnings ?bit-exprs)
        (vl-msb-bitslice-exprlist x ss warnings)))
    (booleanp successp))
  :rule-classes :type-prescription)

Theorem: return-type-of-vl-msb-bitslice-exprlist.warnings

(defthm return-type-of-vl-msb-bitslice-exprlist.warnings
  (b* (((mv ?successp ?warnings ?bit-exprs)
        (vl-msb-bitslice-exprlist x ss warnings)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-msb-bitslice-exprlist.bit-exprs

(defthm return-type-of-vl-msb-bitslice-exprlist.bit-exprs
  (b* (((mv ?successp ?warnings ?bit-exprs)
        (vl-msb-bitslice-exprlist x ss warnings)))
    (true-listp bit-exprs))
  :rule-classes :type-prescription)

Theorem: vl-exprlist-p-of-vl-msb-bitslice-expr

(defthm vl-exprlist-p-of-vl-msb-bitslice-expr
  (let ((ret (vl-msb-bitslice-expr x ss warnings)))
    (vl-exprlist-p (mv-nth 2 ret))))

Theorem: vl-exprlist-p-of-vl-msb-bitslice-exprlist

(defthm vl-exprlist-p-of-vl-msb-bitslice-exprlist
  (let ((ret (vl-msb-bitslice-exprlist x ss warnings)))
    (vl-exprlist-p (mv-nth 2 ret))))

Theorem: len-of-vl-msb-bitslice-expr

(defthm len-of-vl-msb-bitslice-expr
  (let ((ret (vl-msb-bitslice-expr x ss warnings)))
    (implies (and (mv-nth 0 ret)
                  (force (vl-expr-sliceable-p x))
                  (force (vl-expr-welltyped-p x)))
             (equal (len (mv-nth 2 ret))
                    (vl-expr->finalwidth x)))))

Theorem: len-of-vl-msb-bitslice-exprlist

(defthm len-of-vl-msb-bitslice-exprlist
  (let ((ret (vl-msb-bitslice-exprlist x ss warnings)))
    (implies (and (mv-nth 0 ret)
                  (force (vl-exprlist-sliceable-p x))
                  (force (vl-exprlist-welltyped-p x)))
             (equal (len (mv-nth 2 ret))
                    (sum-nats (vl-exprlist->finalwidths x))))))

Theorem: vl-exprlist->finalwidths-of-vl-msb-bitslice-expr

(defthm vl-exprlist->finalwidths-of-vl-msb-bitslice-expr
  (let ((ret (vl-msb-bitslice-expr x ss warnings)))
    (implies (and (mv-nth 0 ret)
                  (force (vl-expr-sliceable-p x))
                  (force (vl-expr-welltyped-p x)))
             (equal (vl-exprlist->finalwidths (mv-nth 2 ret))
                    (replicate (vl-expr->finalwidth x)
                               1)))))

Theorem: vl-exprlist->finalwidths-of-vl-msb-bitslice-exprlist

(defthm vl-exprlist->finalwidths-of-vl-msb-bitslice-exprlist
 (let ((ret (vl-msb-bitslice-exprlist x ss warnings)))
  (implies (and (mv-nth 0 ret)
                (force (vl-exprlist-sliceable-p x))
                (force (vl-exprlist-welltyped-p x)))
           (equal (vl-exprlist->finalwidths (mv-nth 2 ret))
                  (replicate (sum-nats (vl-exprlist->finalwidths x))
                             1)))))

Theorem: vl-exprlist->finaltypes-of-vl-msb-bitslice-expr

(defthm vl-exprlist->finaltypes-of-vl-msb-bitslice-expr
  (let ((ret (vl-msb-bitslice-expr x ss warnings)))
    (implies (and (mv-nth 0 ret)
                  (force (vl-expr-sliceable-p x))
                  (force (vl-expr-welltyped-p x)))
             (equal (vl-exprlist->finaltypes (mv-nth 2 ret))
                    (replicate (vl-expr->finalwidth x)
                               :vl-unsigned)))))

Theorem: vl-exprlist->finaltypes-of-vl-msb-bitslice-exprlist

(defthm vl-exprlist->finaltypes-of-vl-msb-bitslice-exprlist
 (let ((ret (vl-msb-bitslice-exprlist x ss warnings)))
  (implies (and (mv-nth 0 ret)
                (force (vl-exprlist-sliceable-p x))
                (force (vl-exprlist-welltyped-p x)))
           (equal (vl-exprlist->finaltypes (mv-nth 2 ret))
                  (replicate (sum-nats (vl-exprlist->finalwidths x))
                             :vl-unsigned)))))

Theorem: vl-exprlist-welltyped-p-of-vl-msb-bitslice-expr

(defthm vl-exprlist-welltyped-p-of-vl-msb-bitslice-expr
  (let ((ret (vl-msb-bitslice-expr x ss warnings)))
    (implies (and (mv-nth 0 ret)
                  (force (vl-expr-sliceable-p x))
                  (force (vl-expr-welltyped-p x)))
             (vl-exprlist-welltyped-p (mv-nth 2 ret)))))

Theorem: vl-exprlist-welltyped-p-of-vl-msb-bitslice-exprlist

(defthm vl-exprlist-welltyped-p-of-vl-msb-bitslice-exprlist
  (let ((ret (vl-msb-bitslice-exprlist x ss warnings)))
    (implies (and (mv-nth 0 ret)
                  (force (vl-exprlist-sliceable-p x))
                  (force (vl-exprlist-welltyped-p x)))
             (vl-exprlist-welltyped-p (mv-nth 2 ret)))))

Subtopics

Vl-msb-bitslice-partselect

Explode a well-typed, part-select into into MSB-ordered, single-bit expressions.

Vl-msb-bitslice-hidexpr

Explode a well-typed, vl-id-p atom or hierarchical identifier into MSB-ordered, single-bit expressions.

Vl-msb-bitslice-hidexpr-base

Vl-msb-bitslice-weirdint

Explode a well-typed, vl-weirdint-p atom into MSB-ordered, single-bit expressions.

Vl-msb-bitslice-constint

Explode a well-typed vl-constint-p atom into MSB-ordered, single-bit expressions.

Vl-msb-bitslice-exprlist