• 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-zap-dontcares

Zero out the don't-care bits from the right-hand side of a ==? or !=? expression.

Signature

(vl-msb-bits-zap-dontcares msb-bits care-bits) → new-bitlist

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).

Returns

new-bitlist — Type (vl-bitlist-p new-bitlist).

Note: If there is ever a case where Z is one of the care bits, think about whether this does the right thing. Specifically: it is not the case that if Z is among the care bits, then this function produces the same bitlist value as msb-bits & caremask, because a Z among the msb-bits won't be fixed to an X.

Definitions and Theorems

Function: vl-msb-bits-zap-dontcares

(defun vl-msb-bits-zap-dontcares (msb-bits care-bits)
  (declare (xargs :guard (and (vl-bitlist-p msb-bits)
                              (vl-bitlist-p care-bits))))
  (declare (xargs :guard (true-listp care-bits)))
  (let ((__function__ 'vl-msb-bits-zap-dontcares))
    (declare (ignorable __function__))
    (b* (((when (atom msb-bits)) nil)
         (bit1 (vl-bit-fix (car msb-bits)))
         (value (if (member-eq bit1 (vl-bitlist-fix care-bits))
                    bit1
                  :vl-0val)))
      (cons value
            (vl-msb-bits-zap-dontcares (cdr msb-bits)
                                       care-bits)))))

Theorem: vl-bitlist-p-of-vl-msb-bits-zap-dontcares

(defthm vl-bitlist-p-of-vl-msb-bits-zap-dontcares
  (b* ((new-bitlist (vl-msb-bits-zap-dontcares msb-bits care-bits)))
    (vl-bitlist-p new-bitlist))
  :rule-classes :rewrite)

Theorem: len-of-vl-msb-bits-zap-dontcares

(defthm len-of-vl-msb-bits-zap-dontcares
  (equal (len (vl-msb-bits-zap-dontcares msb-bits cares))
         (len msb-bits)))

Theorem: vl-msb-bits-zap-dontcares-under-iff

(defthm vl-msb-bits-zap-dontcares-under-iff
  (iff (vl-msb-bits-zap-dontcares msb-bits cares)
       (consp msb-bits)))

Theorem: vl-msb-bits-zap-dontcares-of-vl-bitlist-fix-msb-bits

(defthm vl-msb-bits-zap-dontcares-of-vl-bitlist-fix-msb-bits
  (equal (vl-msb-bits-zap-dontcares (vl-bitlist-fix msb-bits)
                                    care-bits)
         (vl-msb-bits-zap-dontcares msb-bits care-bits)))

Theorem: vl-msb-bits-zap-dontcares-vl-bitlist-equiv-congruence-on-msb-bits

(defthm
  vl-msb-bits-zap-dontcares-vl-bitlist-equiv-congruence-on-msb-bits
  (implies
       (vl-bitlist-equiv msb-bits msb-bits-equiv)
       (equal (vl-msb-bits-zap-dontcares msb-bits care-bits)
              (vl-msb-bits-zap-dontcares msb-bits-equiv care-bits)))
  :rule-classes :congruence)

Theorem: vl-msb-bits-zap-dontcares-of-vl-bitlist-fix-care-bits

(defthm vl-msb-bits-zap-dontcares-of-vl-bitlist-fix-care-bits
 (equal
     (vl-msb-bits-zap-dontcares msb-bits (vl-bitlist-fix care-bits))
     (vl-msb-bits-zap-dontcares msb-bits care-bits)))

Theorem: vl-msb-bits-zap-dontcares-vl-bitlist-equiv-congruence-on-care-bits

(defthm
 vl-msb-bits-zap-dontcares-vl-bitlist-equiv-congruence-on-care-bits
 (implies
      (vl-bitlist-equiv care-bits care-bits-equiv)
      (equal (vl-msb-bits-zap-dontcares msb-bits care-bits)
             (vl-msb-bits-zap-dontcares msb-bits care-bits-equiv)))
 :rule-classes :congruence)