• 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
        • 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
          • Vl-msb-bits-to-care-mask
          • Vl-msb-bits-zap-dontcares
          • Vl-msb-bits-to-intliteral
          • Vl-intliteral-msb-bits
        • Port-tools
        • Lvalues
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Caremask

Vl-msb-bits-to-care-mask

Construct a bit-mask that captures the non-wild bits from a casex pattern or the right-hand side of a ==? or !=? expression.

Signature

(vl-msb-bits-to-care-mask msb-bits care-bits value) 
  → 
care-mask

Arguments

msb-bits — MSB-ordered bits from the RHS.
    Guard (vl-bitlist-p msb-bits).

care-bits — Set of bit values that are cares; usually {1,0} or {1,0,X}.
    Guard (vl-bitlist-p care-bits).

value — Value we're constructing, zero to begin with.
    Guard (natp value).

Returns

care-mask — Type (natp care-mask).

Definitions and Theorems

Function: vl-msb-bits-to-care-mask

(defun vl-msb-bits-to-care-mask (msb-bits care-bits value)
  (declare (xargs :guard (and (vl-bitlist-p msb-bits)
                              (vl-bitlist-p care-bits)
                              (natp value))))
  (declare (xargs :guard (true-listp care-bits)))
  (let ((__function__ 'vl-msb-bits-to-care-mask))
    (declare (ignorable __function__))
    (b* ((value (lnfix value))
         ((when (atom msb-bits)) value)
         (bit1 (vl-bit-fix (car msb-bits)))
         (value (if (member-eq bit1 (vl-bitlist-fix care-bits))
                    (logior 1 (ash value 1))
                  (ash value 1))))
      (vl-msb-bits-to-care-mask (cdr msb-bits)
                                care-bits value))))

Theorem: natp-of-vl-msb-bits-to-care-mask

(defthm natp-of-vl-msb-bits-to-care-mask
  (b*
   ((care-mask (vl-msb-bits-to-care-mask msb-bits care-bits value)))
   (natp care-mask))
  :rule-classes :type-prescription)

Theorem: unsigned-byte-p-of-vl-msb-bits-to-care-mask-general

(defthm unsigned-byte-p-of-vl-msb-bits-to-care-mask-general
  (implies (unsigned-byte-p n value)
           (unsigned-byte-p
                (+ n (len msb-bits))
                (vl-msb-bits-to-care-mask msb-bits cares value))))

Theorem: unsigned-byte-p-of-vl-msb-bits-to-care-mask-zero

(defthm unsigned-byte-p-of-vl-msb-bits-to-care-mask-zero
  (unsigned-byte-p (len msb-bits)
                   (vl-msb-bits-to-care-mask msb-bits cares 0)))

Theorem: upper-bound-of-vl-msb-bits-to-care-mask-zero

(defthm upper-bound-of-vl-msb-bits-to-care-mask-zero
  (< (vl-msb-bits-to-care-mask msb-bits cares 0)
     (expt 2 (len msb-bits)))
  :rule-classes ((:rewrite) (:linear)))

Theorem: vl-msb-bits-to-care-mask-of-vl-bitlist-fix-msb-bits

(defthm vl-msb-bits-to-care-mask-of-vl-bitlist-fix-msb-bits
  (equal (vl-msb-bits-to-care-mask (vl-bitlist-fix msb-bits)
                                   care-bits value)
         (vl-msb-bits-to-care-mask msb-bits care-bits value)))

Theorem: vl-msb-bits-to-care-mask-vl-bitlist-equiv-congruence-on-msb-bits

(defthm
   vl-msb-bits-to-care-mask-vl-bitlist-equiv-congruence-on-msb-bits
 (implies
  (vl-bitlist-equiv msb-bits msb-bits-equiv)
  (equal (vl-msb-bits-to-care-mask msb-bits care-bits value)
         (vl-msb-bits-to-care-mask msb-bits-equiv care-bits value)))
 :rule-classes :congruence)

Theorem: vl-msb-bits-to-care-mask-of-vl-bitlist-fix-care-bits

(defthm vl-msb-bits-to-care-mask-of-vl-bitlist-fix-care-bits
  (equal
       (vl-msb-bits-to-care-mask msb-bits (vl-bitlist-fix care-bits)
                                 value)
       (vl-msb-bits-to-care-mask msb-bits care-bits value)))

Theorem: vl-msb-bits-to-care-mask-vl-bitlist-equiv-congruence-on-care-bits

(defthm
  vl-msb-bits-to-care-mask-vl-bitlist-equiv-congruence-on-care-bits
 (implies
  (vl-bitlist-equiv care-bits care-bits-equiv)
  (equal (vl-msb-bits-to-care-mask msb-bits care-bits value)
         (vl-msb-bits-to-care-mask msb-bits care-bits-equiv value)))
 :rule-classes :congruence)

Theorem: vl-msb-bits-to-care-mask-of-nfix-value

(defthm vl-msb-bits-to-care-mask-of-nfix-value
  (equal (vl-msb-bits-to-care-mask msb-bits care-bits (nfix value))
         (vl-msb-bits-to-care-mask msb-bits care-bits value)))

Theorem: vl-msb-bits-to-care-mask-nat-equiv-congruence-on-value

(defthm vl-msb-bits-to-care-mask-nat-equiv-congruence-on-value
 (implies
  (acl2::nat-equiv value value-equiv)
  (equal (vl-msb-bits-to-care-mask msb-bits care-bits value)
         (vl-msb-bits-to-care-mask msb-bits care-bits value-equiv)))
 :rule-classes :congruence)