• 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-set-unsigned

Removes any explicit signed indicator from a datatype.

Signature

(vl-datatype-set-unsigned x) → new-x

Arguments

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

Returns

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

This is rather specific in purpose and generally shouldn't be used. The case where it is useful is when we are indexing into an (explicitly signed) packed array; this means that the whole array is signed, but not the selected parts. So we strip the signed qualifier off of the type when we index into packed dimensions. (This doesn't apply to usertypes that are defined as signed types! If we index down to such a type, it IS signed, but any packed array of such a type is not. So we don't need to descend into usertypes or somehow mark them as unsigned. We just have to know that a usertype with one or more packed dimensions counts as unsigned.)

Definitions and Theorems

Function: vl-datatype-set-unsigned

(defun vl-datatype-set-unsigned (x)
 (declare (xargs :guard (vl-datatype-p x)))
 (let ((__function__ 'vl-datatype-set-unsigned))
  (declare (ignorable __function__))
  (vl-datatype-case
     x
     :vl-coretype
     (mbe :logic
          (change-vl-coretype x :signedp nil)
          :exec
          (if x.signedp (change-vl-coretype x :signedp nil)
            x))
     :vl-struct (mbe :logic (change-vl-struct x :signedp nil)
                     :exec
                     (if x.signedp (change-vl-struct x :signedp nil)
                       x))
     :vl-union (mbe :logic (change-vl-union x :signedp nil)
                    :exec
                    (if x.signedp (change-vl-union x :signedp nil)
                      x))
     :otherwise (vl-datatype-fix x))))

Theorem: vl-datatype-p-of-vl-datatype-set-unsigned

(defthm vl-datatype-p-of-vl-datatype-set-unsigned
  (b* ((new-x (vl-datatype-set-unsigned x)))
    (vl-datatype-p new-x))
  :rule-classes :rewrite)

Theorem: vl-datatype-resolved-p-of-set-unsigned

(defthm vl-datatype-resolved-p-of-set-unsigned
  (b* ((?new-x (vl-datatype-set-unsigned x)))
    (implies (vl-datatype-resolved-p x)
             (vl-datatype-resolved-p new-x))))

Theorem: vl-datatype-set-unsigned-of-vl-datatype-fix-x

(defthm vl-datatype-set-unsigned-of-vl-datatype-fix-x
  (equal (vl-datatype-set-unsigned (vl-datatype-fix x))
         (vl-datatype-set-unsigned x)))

Theorem: vl-datatype-set-unsigned-vl-datatype-equiv-congruence-on-x

(defthm vl-datatype-set-unsigned-vl-datatype-equiv-congruence-on-x
  (implies (vl-datatype-equiv x x-equiv)
           (equal (vl-datatype-set-unsigned x)
                  (vl-datatype-set-unsigned x-equiv)))
  :rule-classes :congruence)