• 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

• Vl-msb-bitslice-expr

Vl-msb-bitslice-hidexpr

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

Signature

(vl-msb-bitslice-hidexpr 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 (vl-exprlist-p bit-exprs).

We require that X is a well-typed identifier or hierarchical identifier expression, i.e., our expression-sizing transform should have already been run. See also the discussion in vl-atom-welltyped-p and note that the finalwidth and finaltype of the identifier may differ from its declaration. We expect these widths to be at least as large as the identifier's width, and differences here are used to indicate zero/sign extensions.

The list of bits we want to return here depends on the order of the msb and lsb indices for the wire. For instance, if the wire is declared as:

wire [3:0] w;

Then we want to return {w[3], w[2], w[1], w[0]}. But if the wire is instead declared as:

wire [0:3] w;

Then we will want to return {w[0], w[1], w[2], w[3]} instead.

Definitions and Theorems

Function: vl-msb-bitslice-hidexpr

(defun vl-msb-bitslice-hidexpr (x ss warnings)
 (declare (xargs :guard (and (vl-expr-p x)
                             (vl-scopestack-p ss)
                             (vl-warninglist-p warnings))))
 (declare
      (xargs :guard (and (vl-hidexpr-p x)
                         (or (vl-atom-p x)
                             (eq (vl-nonatom->op x) :vl-hid-dot))
                         (vl-expr-welltyped-p x))))
 (let ((__function__ 'vl-msb-bitslice-hidexpr))
  (declare (ignorable __function__))
  (b*
   ((x (vl-expr-fix x))
    ((mv successp warnings main-bits)
     (vl-msb-bitslice-hidexpr-base x ss warnings))
    ((unless successp)
     (mv nil warnings nil))
    (x.finalwidth (vl-expr->finalwidth x))
    (x.finaltype (vl-expr->finaltype x))
    (nwires (len main-bits))
    ((when (< x.finalwidth nwires))
     (mv
      nil
      (fatal
       :type :vl-programming-error
       :msg
       "Found an identifier/HID expression for ~a0 ~
                         with width ~x1, which is smaller than ~x2, the size ~
                         of its range.  Expected all occurrences of plain ~
                         identifiers to have widths that are at least as ~
                         large as their declarations."
       :args (list x x.finalwidth nwires))
      nil))
    ((when (eql nwires x.finalwidth))
     (mv t warnings main-bits))
    (extension-bit (if (eq x.finaltype :vl-signed)
                       (car main-bits)
                     |*sized-1'b0*|))
    (bits (append (replicate (- x.finalwidth nwires)
                             extension-bit)
                  main-bits)))
   (mv t warnings bits))))

Theorem: booleanp-of-vl-msb-bitslice-hidexpr.successp

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

Theorem: vl-warninglist-p-of-vl-msb-bitslice-hidexpr.warnings

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

Theorem: vl-exprlist-p-of-vl-msb-bitslice-hidexpr.bit-exprs

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

Theorem: vl-msb-bitslice-hidexpr-mvtypes-0

(defthm vl-msb-bitslice-hidexpr-mvtypes-0
  (booleanp (mv-nth 0
                    (vl-msb-bitslice-hidexpr x ss warnings)))
  :rule-classes :type-prescription)

Theorem: vl-msb-bitslice-hidexpr-mvtypes-2

(defthm vl-msb-bitslice-hidexpr-mvtypes-2
  (true-listp (mv-nth 2
                      (vl-msb-bitslice-hidexpr x ss warnings)))
  :rule-classes :type-prescription)

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

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

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

(defthm vl-exprlist->finalwidths-of-vl-msb-bitslice-hidexpr
  (let ((ret (vl-msb-bitslice-hidexpr x ss warnings)))
    (implies (and (mv-nth 0 ret)
                  (force (vl-hidexpr-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->finaltypes-of-vl-msb-bitslice-hidexpr

(defthm vl-exprlist->finaltypes-of-vl-msb-bitslice-hidexpr
  (let ((ret (vl-msb-bitslice-hidexpr x ss warnings)))
    (implies (and (mv-nth 0 ret)
                  (force (vl-hidexpr-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-welltyped-p-of-vl-msb-bitslice-hidexpr

(defthm vl-exprlist-welltyped-p-of-vl-msb-bitslice-hidexpr
  (let ((ret (vl-msb-bitslice-hidexpr x ss warnings)))
    (implies (and (mv-nth 0 ret)
                  (force (vl-hidexpr-p x))
                  (or (vl-atom-p x)
                      (eq (vl-nonatom->op x) :vl-hid-dot))
                  (force (vl-expr-welltyped-p x)))
             (vl-exprlist-welltyped-p (mv-nth 2 ret)))))

Theorem: vl-msb-bitslice-hidexpr-of-vl-expr-fix-x

(defthm vl-msb-bitslice-hidexpr-of-vl-expr-fix-x
  (equal (vl-msb-bitslice-hidexpr (vl-expr-fix x)
                                  ss warnings)
         (vl-msb-bitslice-hidexpr x ss warnings)))

Theorem: vl-msb-bitslice-hidexpr-vl-expr-equiv-congruence-on-x

(defthm vl-msb-bitslice-hidexpr-vl-expr-equiv-congruence-on-x
  (implies (vl-expr-equiv x x-equiv)
           (equal (vl-msb-bitslice-hidexpr x ss warnings)
                  (vl-msb-bitslice-hidexpr x-equiv ss warnings)))
  :rule-classes :congruence)

Theorem: vl-msb-bitslice-hidexpr-of-vl-scopestack-fix-ss

(defthm vl-msb-bitslice-hidexpr-of-vl-scopestack-fix-ss
  (equal (vl-msb-bitslice-hidexpr x (vl-scopestack-fix ss)
                                  warnings)
         (vl-msb-bitslice-hidexpr x ss warnings)))

Theorem: vl-msb-bitslice-hidexpr-vl-scopestack-equiv-congruence-on-ss

(defthm vl-msb-bitslice-hidexpr-vl-scopestack-equiv-congruence-on-ss
  (implies (vl-scopestack-equiv ss ss-equiv)
           (equal (vl-msb-bitslice-hidexpr x ss warnings)
                  (vl-msb-bitslice-hidexpr x ss-equiv warnings)))
  :rule-classes :congruence)

Theorem: vl-msb-bitslice-hidexpr-of-vl-warninglist-fix-warnings

(defthm vl-msb-bitslice-hidexpr-of-vl-warninglist-fix-warnings
 (equal (vl-msb-bitslice-hidexpr x ss (vl-warninglist-fix warnings))
        (vl-msb-bitslice-hidexpr x ss warnings)))

Theorem: vl-msb-bitslice-hidexpr-vl-warninglist-equiv-congruence-on-warnings

(defthm
 vl-msb-bitslice-hidexpr-vl-warninglist-equiv-congruence-on-warnings
 (implies (vl-warninglist-equiv warnings warnings-equiv)
          (equal (vl-msb-bitslice-hidexpr x ss warnings)
                 (vl-msb-bitslice-hidexpr x ss warnings-equiv)))
 :rule-classes :congruence)