• 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
      • Rtl
        • Floating-Point Exceptions and Specification of Elementary Arithmetic Instructions
        • Implementation of Elementary Operations
        • Register-Transfer Logic
        • Floating-Point Arithmetic
          • Rounding
          • Floating-Point Formats
            • Normal Encodings
            • Denormals and Zeroes
            • Classification of Formats
            • Rebiasing Exponents
            • Infinities and NaNs
          • Floating-Point Numbers
        • Modeling Algorithms in C++ and ACL2
        • Bibliography
    • Algebra
  • Testing-utilities

• Floating-Point Formats

Denormals and Zeroes

Denormals and Zeroes

Definitions and Theorems

Function: zerp

(defun zerp (x f)
  (declare (xargs :guard (encodingp x f)))
  (and (mbt (encodingp x f))
       (= (expf x f) 0)
       (= (sigf x f) 0)))

Function: zencode

(defun zencode (sgn f)
  (declare (xargs :guard (and (bvecp sgn 1) (formatp f))))
  (cat sgn 1 0 (+ (sigw f) (expw f))))

Function: denormp

(defun denormp (x f)
  (declare (xargs :guard (encodingp x f)))
  (and (mbt (encodingp x f))
       (= (expf x f) 0)
       (not (= (sigf x f) 0))
       (implies (explicitp f)
                (= (bitn x (1- (prec f))) 0))))

Function: pseudop

(defun pseudop (x f)
  (declare (xargs :guard (encodingp x f)))
  (and (mbt (encodingp x f))
       (explicitp f)
       (= (expf x f) 0)
       (= (bitn x (1- (prec f))) 1)))

Function: ddecode

(defun ddecode (x f)
  (declare (xargs :guard (encodingp x f)))
  (* (if (= (sgnf x f) 0) 1 -1)
     (sigf x f)
     (expt 2 (+ 2 (- (bias f)) (- (prec f))))))

Function: decode

(defun decode (x f)
  (declare (xargs :guard (encodingp x f)))
  (if (= (expf x f) 0)
      (ddecode x f)
    (ndecode x f)))

Theorem: sgn-ddecode

(defthm sgn-ddecode
  (implies (or (denormp x f) (pseudop x f))
           (equal (sgn (ddecode x f))
                  (if (= (sgnf x f) 0) 1 -1))))

Theorem: expo-ddecode

(defthm expo-ddecode
  (implies (or (denormp x f) (pseudop x f))
           (equal (expo (ddecode x f))
                  (+ 2 (- (prec f))
                     (- (bias f))
                     (expo (sigf x f))))))

Theorem: sig-ddecode

(defthm sig-ddecode
  (implies (or (denormp x f) (pseudop x f))
           (equal (sig (ddecode x f))
                  (sig (sigf x f)))))

Function: drepp

(defun drepp (x f)
  (declare (xargs :guard t))
  (and (rationalp x)
       (formatp f)
       (not (= x 0))
       (<= (- 2 (prec f))
           (+ (expo x) (bias f)))
       (<= (+ (expo x) (bias f)) 0)
       (exactp x (+ (1- (prec f)) (bias f) (expo x)))))

Theorem: drepp-exactp

(defthm drepp-exactp
  (implies (drepp x f)
           (exactp x (prec f))))

Function: dencode

(defun dencode (x f)
  (declare (xargs :guard (drepp x f)))
  (cat (if (= (sgn x) 1) 0 1)
       1 0 (expw f)
       (* (sig x)
          (expt 2 (+ -2 (prec f) (expo x) (bias f))))
       (sigw f)))

Theorem: drepp-ddecode

(defthm drepp-ddecode
  (implies (denormp x f)
           (drepp (ddecode x f) f)))

Theorem: dencode-ddecode

(defthm dencode-ddecode
  (implies (denormp x f)
           (equal (dencode (ddecode x f) f) x)))

Theorem: denormp-dencode

(defthm denormp-dencode
  (implies (drepp x f)
           (denormp (dencode x f) f)))

Theorem: ddecode-dencode

(defthm ddecode-dencode
  (implies (drepp x f)
           (equal (ddecode (dencode x f) f) x)))

Theorem: drepp<spn

(defthm drepp<spn
  (implies (drepp x f)
           (< (abs x) (spn f))))

Function: spd

(defun spd (f)
  (declare (xargs :guard (formatp f)))
  (expt 2 (+ 2 (- (bias f)) (- (prec f)))))

Theorem: positive-spd

(defthm positive-spd
  (implies (formatp f) (> (spd f) 0))
  :rule-classes :linear)

Theorem: drepp-spd

(defthm drepp-spd
  (implies (formatp f) (drepp (spd f) f)))

Theorem: smallest-spd

(defthm smallest-spd
  (implies (drepp r f)
           (>= (abs r) (spd f))))

Theorem: spd-mult

(defthm spd-mult
  (implies (and (formatp f)
                (> r 0)
                (= m (/ r (spd f))))
           (iff (drepp r f)
                (and (natp m)
                     (<= 1 m)
                     (< m (expt 2 (1- (prec f))))))))