• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
      • Floating-Point Exceptions and Specification of Elementary Arithmetic Instructions
      • Implementation of Elementary Operations
      • Register-Transfer Logic
      • Floating-Point Arithmetic
        • Rounding
          • Unbiased Rounding
          • IEEE Rounding
          • Denormal Rounding
          • Rounding Away from Zero
          • Truncation
          • Odd Rounding
        • Floating-Point Formats
        • Floating-Point Numbers
      • Modeling Algorithms in C++ and ACL2
      • Bibliography
  • Software-verification
  • Math
  • Testing-utilities

• Rounding

Denormal Rounding

Denormal Rounding

Definitions and Theorems

Function: drnd

(defun drnd (x mode f)
  (declare (xargs :guard (and (real/rationalp x)
                              (common-mode-p mode)
                              (formatp f))))
  (rnd x mode
       (+ (prec f)
          (expo x)
          (- (expo (spn f))))))

Theorem: drnd-minus

(defthm drnd-minus
  (equal (drnd (- x) mode f)
         (- (drnd x (flip-mode mode) f))))

Theorem: drnd-pos

(defthm drnd-pos
  (implies (and (formatp f)
                (rationalp x)
                (>= x 0)
                (<= x (spn f))
                (common-mode-p mode))
           (>= (drnd x mode f) 0)))

Theorem: drnd-rewrite

(defthm drnd-rewrite
  (implies (and (formatp f)
                (rationalp x)
                (<= (abs x) (spn f))
                (common-mode-p mode))
           (equal (drnd x mode f)
                  (- (rnd (+ x (* (sgn x) (spn f)))
                          mode (prec f))
                     (* (sgn x) (spn f))))))

Theorem: drnd-exactp-a

(defthm drnd-exactp-a
  (implies (and (formatp f)
                (rationalp x)
                (<= (abs x) (spn f))
                (common-mode-p mode))
           (or (drepp (drnd x mode f) f)
               (= (drnd x mode f) 0)
               (= (drnd x mode f)
                  (* (sgn x) (spn f)))))
  :rule-classes nil)

Theorem: drnd-exactp-b

(defthm drnd-exactp-b
  (implies (and (formatp f)
                (rationalp x)
                (drepp x f)
                (common-mode-p mode))
           (equal (drnd x mode f) x)))

Theorem: drnd-exactp-c

(defthm drnd-exactp-c
  (implies (and (formatp f)
                (rationalp x)
                (<= (expo x) (- (bias f)))
                (>= (expo x)
                    (+ 2 (- (bias f)) (- (prec f))))
                (common-mode-p mode))
           (iff (equal x (drnd x mode f))
                (exactp x
                        (+ (1- (prec f)) (bias f) (expo x))))))

Theorem: drnd-exactp-d

(defthm drnd-exactp-d
  (implies (and (formatp f)
                (rationalp x)
                (<= (abs x) (spn f))
                (rationalp a)
                (drepp a f)
                (>= a x)
                (common-mode-p mode))
           (>= a (drnd x mode f)))
  :rule-classes nil)

Theorem: drnd-exactp-e

(defthm drnd-exactp-e
  (implies (and (formatp f)
                (rationalp x)
                (<= (abs x) (spn f))
                (rationalp a)
                (drepp a f)
                (<= a x)
                (common-mode-p mode))
           (<= a (drnd x mode f)))
  :rule-classes nil)

Theorem: drnd-rtz

(defthm drnd-rtz
  (implies (and (formatp f)
                (rationalp x)
                (<= (abs x) (spn f)))
           (<= (abs (drnd x 'rtz f)) (abs x)))
  :rule-classes nil)

Theorem: drnd-raz

(defthm drnd-raz
  (implies (and (formatp f)
                (rationalp x)
                (<= (abs x) (spn f)))
           (>= (abs (drnd x 'raz f)) (abs x)))
  :rule-classes nil)

Theorem: drnd-rdn

(defthm drnd-rdn
  (implies (and (formatp f)
                (rationalp x)
                (<= (abs x) (spn f)))
           (<= (drnd x 'rdn f) x))
  :rule-classes nil)

Theorem: drnd-rup

(defthm drnd-rup
  (implies (and (formatp f)
                (rationalp x)
                (<= (abs x) (spn f)))
           (>= (drnd x 'rup f) x))
  :rule-classes nil)

Theorem: drnd-diff

(defthm drnd-diff
  (implies (and (formatp f)
                (rationalp x)
                (<= (abs x) (spn f))
                (common-mode-p mode))
           (< (abs (- x (drnd x mode f))) (spd f)))
  :rule-classes nil)

Theorem: drnd-rne-diff

(defthm drnd-rne-diff
  (implies (and (formatp f)
                (rationalp x)
                (<= (abs x) (spn f))
                (drepp a f))
           (>= (abs (- x a))
               (abs (- x (drnd x 'rne f)))))
  :rule-classes nil)

Theorem: drnd-rna-diff

(defthm drnd-rna-diff
  (implies (and (formatp f)
                (rationalp x)
                (<= (abs x) (spn f))
                (drepp a f))
           (>= (abs (- x a))
               (abs (- x (drnd x 'rna f)))))
  :rule-classes nil)

Theorem: drnd-rto

(defthm drnd-rto
  (implies (and (formatp f)
                (common-mode-p mode)
                (rationalp x)
                (<= (abs x) (spn f))
                (natp n)
                (>= n
                    (+ (prec f)
                       (expo x)
                       (- (expo (spn f)))
                       2)))
           (equal (drnd (rto x n) mode f)
                  (drnd x mode f))))

Theorem: rnd-drnd-exactp

(defthm rnd-drnd-exactp
  (implies (and (formatp f)
                (rationalp x)
                (< (abs x) (spn f))
                (common-mode-p mode)
                (= (drnd x mode f) x))
           (equal (rnd x mode (prec f)) x)))

Theorem: drnd-tiny-a

(defthm drnd-tiny-a
  (implies (and (formatp f)
                (common-mode-p mode)
                (rationalp x)
                (< 0 x)
                (< x (/ (spd f) 2)))
           (equal (drnd x mode f)
                  (if (member mode '(raz rup))
                      (spd f)
                    0))))

Theorem: drnd-tiny-b

(defthm drnd-tiny-b
  (implies (and (formatp f) (common-mode-p mode))
           (equal (drnd (/ (spd f) 2) mode f)
                  (if (member mode '(raz rup rna))
                      (spd f)
                    0))))

Theorem: drnd-tiny-c

(defthm drnd-tiny-c
  (implies (and (formatp f)
                (common-mode-p mode)
                (rationalp x)
                (< (/ (spd f) 2) x)
                (< x (spd f)))
           (equal (drnd x mode f)
                  (if (member mode '(rtz rdn))
                      0
                    (spd f)))))

Theorem: drnd-tiny-equal

(defthm drnd-tiny-equal
  (implies (and (formatp f)
                (common-mode-p mode)
                (rationalp x)
                (< 0 x)
                (< (abs x) (/ (spd f) 2))
                (rationalp y)
                (< 0 y)
                (< (abs y) (/ (spd f) 2)))
           (equal (drnd x mode f) (drnd y mode f)))
  :rule-classes nil)

Theorem: rnd-drnd

(defthm rnd-drnd
  (implies (and (formatp f)
                (> (prec f) 2)
                (rationalp m)
                (< 0 m)
                (< m 1)
                (common-mode-p mode))
           (let* ((x (* (spn f) m))
                  (p (prec f))
                  (r (rnd x mode p))
                  (d (drnd x mode f)))
             (case mode
               ((rdn rtz)
                (and (< r (spn f)) (< d (spn f))))
               ((rup raz)
                (and (iff (< r (spn f))
                          (<= m (- 1 (expt 2 (- p)))))
                     (iff (< d (spn f))
                          (<= m (- 1 (expt 2 (- 1 p)))))))
               ((rne rna)
                (and (iff (< r (spn f))
                          (< m (- 1 (expt 2 (- (1+ p))))))
                     (iff (< d (spn f))
                          (< m (- 1 (expt 2 (- p)))))))))))

Theorem: rnd-drnd-up

(defthm rnd-drnd-up
  (implies (and (formatp f)
                (rationalp x)
                (< (abs x) (spn f))
                (common-mode-p mode)
                (= (abs (rnd x mode (prec f))) (spn f)))
           (equal (abs (drnd x mode f)) (spn f))))

Theorem: rnd-drnd-inject-a

(defthm rnd-drnd-inject-a
  (let* ((p (prec f))
         (s (spn f))
         (x (* s z))
         (m (* (expt 2 (1- k)) z))
         (sum (+ m (rnd-const (1- k) mode p)))
         (sl (bits sum (1- (- k p)) 0))
         (sh (bits sum k (- k p))))
    (implies (and (formatp f)
                  (rationalp z)
                  (< 0 z)
                  (< z 2)
                  (common-mode-p mode)
                  (natp k)
                  (>= k (+ p 2))
                  (natp m)
                  (< (expo m) (- k p)))
             (equal (drnd x mode f)
                    (if (and (= mode 'rne) (= sl 0))
                        (* (expt 2 (- 2 p)) s (bits sh p 1))
                      (* (expt 2 (- 1 p)) s sh))))))

Theorem: rnd-drnd-inject-b

(defthm rnd-drnd-inject-b
  (let* ((p (prec f))
         (s (spn f))
         (x (* s z))
         (m (* (expt 2 (1- k)) z))
         (c (rnd-const (1- k) mode p))
         (sum (+ m c))
         (sl (bits sum (1- (- k p)) 0)))
    (implies (and (formatp f)
                  (rationalp z)
                  (< 0 z)
                  (< z 2)
                  (common-mode-p mode)
                  (natp k)
                  (>= k (+ p 2))
                  (natp m))
             (iff (= x (drnd x mode f)) (= sl c)))))

Theorem: rnd-drnd-inject-c

(defthm rnd-drnd-inject-c
  (let* ((p (prec f))
         (s (spn f))
         (x (* s z))
         (m (* (expt 2 (1- k)) z))
         (c (rnd-const (1- k) mode p))
         (sum (+ m c))
         (sh (bits sum k (- k p))))
    (implies (and (formatp f)
                  (rationalp z)
                  (< 0 z)
                  (< z 2)
                  (common-mode-p mode)
                  (natp k)
                  (>= k (+ p 2))
                  (natp m)
                  (> sh (expt 2 (1- p))))
             (and (>= x s) (>= (rnd x mode p) s)))))

Theorem: rnd-drnd-inject-d

(defthm rnd-drnd-inject-d
  (let* ((p (prec f))
         (s (spn f))
         (x (* s z))
         (m (* (expt 2 (1- k)) z))
         (c (rnd-const (1- k) mode p))
         (sum (+ m c))
         (sh (bits sum k (- k p))))
    (implies (and (formatp f)
                  (rationalp z)
                  (< 0 z)
                  (< z 2)
                  (common-mode-p mode)
                  (natp k)
                  (>= k (+ p 2))
                  (natp m)
                  (< sh (expt 2 (1- p))))
             (and (< x s) (< (rnd x mode p) s)))))

Theorem: rnd-drnd-inject-e

(defthm rnd-drnd-inject-e
  (let* ((p (prec f))
         (s (spn f))
         (x (* s z))
         (m (* (expt 2 (1- k)) z))
         (c (rnd-const (1- k) mode p))
         (sum (+ m c))
         (sh (bits sum k (- k p))))
    (implies (and (formatp f)
                  (rationalp z)
                  (< 0 z)
                  (< z 2)
                  (common-mode-p mode)
                  (natp k)
                  (>= k (+ p 2))
                  (natp m)
                  (= sh (expt 2 (1- p)))
                  (or (= mode 'rtz) (= mode 'rdn)))
             (and (>= x s) (>= (rnd x mode p) s)))))

Theorem: rnd-drnd-inject-f-i

(defthm rnd-drnd-inject-f-i
  (let* ((p (prec f))
         (s (spn f))
         (x (* s z))
         (m (* (expt 2 (1- k)) z))
         (c (rnd-const (1- k) mode p))
         (sum (+ m c))
         (sh (bits sum k (- k p)))
         (sl (bits sum (1- (- k p)) 0)))
    (implies (and (formatp f)
                  (rationalp z)
                  (< 0 z)
                  (< z 2)
                  (common-mode-p mode)
                  (natp k)
                  (>= k (+ p 2))
                  (natp m)
                  (= sh (expt 2 (1- p)))
                  (or (= mode 'raz) (= mode 'rup)))
             (iff (< x s) (not (= sl c))))))

Theorem: rnd-drnd-inject-f-ii

(defthm rnd-drnd-inject-f-ii
  (let* ((p (prec f))
         (s (spn f))
         (x (* s z))
         (m (* (expt 2 (1- k)) z))
         (c (rnd-const (1- k) mode p))
         (sum (+ m c))
         (sh (bits sum k (- k p)))
         (g (bitn sum (1- (- k p)))))
    (implies (and (formatp f)
                  (rationalp z)
                  (< 0 z)
                  (< z 2)
                  (common-mode-p mode)
                  (natp k)
                  (>= k (+ p 2))
                  (natp m)
                  (= sh (expt 2 (1- p)))
                  (or (= mode 'raz) (= mode 'rup)))
             (iff (< (rnd x mode p) s) (= g 0)))))

Theorem: rnd-drnd-inject-g-i

(defthm rnd-drnd-inject-g-i
  (let* ((p (prec f))
         (s (spn f))
         (x (* s z))
         (m (* (expt 2 (1- k)) z))
         (c (rnd-const (1- k) mode p))
         (sum (+ m c))
         (sh (bits sum k (- k p)))
         (g (bitn sum (1- (- k p)))))
    (implies (and (formatp f)
                  (rationalp z)
                  (< 0 z)
                  (< z 2)
                  (common-mode-p mode)
                  (natp k)
                  (>= k (+ p 2))
                  (natp m)
                  (= sh (expt 2 (1- p)))
                  (or (= mode 'rne) (= mode 'rna)))
             (iff (< x s) (= g 0)))))

Theorem: rnd-drnd-inject-g-ii

(defthm rnd-drnd-inject-g-ii
  (let* ((p (prec f))
         (s (spn f))
         (x (* s z))
         (m (* (expt 2 (1- k)) z))
         (c (rnd-const (1- k) mode p))
         (sum (+ m c))
         (sh (bits sum k (- k p)))
         (g (bitn sum (1- (- k p))))
         (r (bitn sum (- (- k p) 2))))
    (implies (and (formatp f)
                  (rationalp z)
                  (< 0 z)
                  (< z 2)
                  (common-mode-p mode)
                  (natp k)
                  (>= k (+ p 2))
                  (natp m)
                  (= sh (expt 2 (1- p)))
                  (or (= mode 'rne) (= mode 'rna)))
             (iff (< (rnd x mode p) s)
                  (and (= g 0) (= r 0))))))