• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
      • 100-theorems
      • Arithmetic
      • Bit-vectors
        • Sparseint
        • Bitops
        • Bv
        • Ihs
          • Logops-definitions
            • Logops-byte-functions
              • Wrb
              • Rdb
              • Bsp
                • Bspp
                • Wrb-field
                • Bsp-size
                • Bsp-position
                • Rdb-test
                • Rdb-field
                • Wrb-guard
                • Rdb-guard
              • Defword
              • Defbytetype
              • Logext
              • Logrev
              • Loghead
              • Logops-bit-functions
              • Logtail
              • Logapp
              • Logsat
              • Binary--
              • Logcdr
              • Logcar
              • Logbit
              • Logextu
              • Logcons
              • Lshu
              • Logrpl
              • Ashu
              • Logmaskp
              • Lognotu
              • Logmask
              • Imod
              • Ifloor
              • Bfix
              • Bitmaskp
              • Logite
              • Expt2
              • Zbp
              • *logops-functions*
              • Word/bit-macros
              • Logops-definitions-theory
              • Logops-functions
              • Lbfix
              • Logextu-guard
              • Lshu-guard
              • Logtail-guard
              • Logrpl-guard
              • Logrev-guard
              • Lognotu-guard
              • Logmask-guard
              • Loghead-guard
              • Logext-guard
              • Logbit-guard
              • Logapp-guard
              • Ashu-guard
            • Math-lemmas
            • Ihs-theories
            • Ihs-init
            • Logops
          • Rtl
        • Algebra
      • Testing-utilities
    • Logops-byte-functions

    Bsp

    (bsp size pos) returns a byte-specifier.

    This specifier designates a byte whose width is size and whose bits have weights 2^(pos) through 2^(pos+size-1). Both size and pos must be nonnegative integers.

    BSP is mnemonic for Byte SPecifier or Byte Size and Position, and is analogous to Common Lisp's (byte size position).

    BSP is implemented as a macro for simplicity and convenience. One should always use BSP in preference to CONS, however, to ensure compatibility with future releases.

    Macro: bsp

    (defmacro bsp (size pos)
      (cons 'cons
            (cons size (cons pos 'nil))))