• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Debugging
  • Projects
  • 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
          • Multiplication
          • FMA-Based Division
          • Addition
          • SRT Division and Square Root
            • SRT Division and Quotient Digit Selection
            • SRT Square Root Extraction
        • Register-Transfer Logic
        • Floating-Point Arithmetic
        • Modeling Algorithms in C++ and ACL2
        • Bibliography
    • Algebra
  • Testing-utilities

• SRT Division and Square Root

SRT Division and Quotient Digit Selection

SRT Division and Quotient Digit Selection

Definitions and Theorems

Function: quot$

(defun quot$ (j)
  (if (zp j)
      0
    (+ (quot$ (1- j))
       (* (q$ j) (expt (r$) (- 1 j))))))

Function: rem$

(defun rem$ (j)
  (* (expt (r$) (1- j))
     (- (x$) (* (d$) (quot$ j)))))

Theorem: rem0-div-rewrite

(defthm rem0-div-rewrite
  (equal (rem$ 0) (/ (x$) (r$))))

Theorem: rem-div-recurrence

(defthm rem-div-recurrence
  (implies (natp j)
           (equal (rem$ (+ 1 j))
                  (- (* (r$) (rem$ j))
                     (* (q$ (1+ j)) (d$))))))

Theorem: rem0-div-bound

(defthm rem0-div-bound
  (< (abs (rem$ 0)) (* (rho$) (d$))))

Function: sel-upper-div

(defun sel-upper-div (k d)
  (* (+ k (rho$)) d))

Function: sel-lower-div

(defun sel-lower-div (k d)
  (* (- k (rho$)) d))

Theorem: rem-div-bnd-next

(defthm rem-div-bnd-next
  (implies (and (natp j)
                (<= (sel-lower-div (q$ (1+ j)) (d$))
                    (* (r$) (rem$ j)))
                (>= (sel-upper-div (q$ (1+ j)) (d$))
                    (* (r$) (rem$ j))))
           (<= (abs (rem$ (1+ j)))
               (* (rho$) (d$)))))

Theorem: select-overlap

(defthm select-overlap
  (implies (integerp k)
           (and (< (sel-lower-div k (d$))
                   (sel-lower-div (1+ k) (d$)))
                (< (sel-lower-div (1+ k) (d$))
                   (sel-upper-div k (d$)))
                (< (sel-upper-div k (d$))
                   (sel-upper-div (1+ k) (d$)))
                (<= (sel-upper-div k (d$))
                    (sel-lower-div (+ k 2) (d$))))))

Theorem: div-containment

(defthm div-containment
  (and (equal (sel-upper-div (a$) (d$))
              (* (r$) (rho$) (d$)))
       (equal (sel-lower-div (- (a$)) (d$))
              (- (* (r$) (rho$) (d$))))))

Function: md4

(defun md4 (k)
  (case k
    (2 13/8)
    (1 1/2)
    (0 -3/8)
    (-1 -3/2)))

Function: select-digit-d4

(defun select-digit-d4 (a)
  (cond ((<= (md4 2) a) 2)
        ((<= (md4 1) a) 1)
        ((<= (md4 0) a) 0)
        ((<= (md4 -1) a) -1)
        (t -2)))

Theorem: sel-limits-4

(defthm sel-limits-4
  (implies (and (<= 63/64 (d$))
                (<= (d$) 9/8)
                (= (r$) 4)
                (= (a$) 2)
                (member k '(-2 -1 0 1 2)))
           (and (<= (sel-lower-div k (d$))
                    (max (sel-lower-div k 63/64)
                         (sel-lower-div k 9/8)))
                (>= (sel-upper-div k (d$))
                    (min (sel-upper-div k 63/64)
                         (sel-upper-div k 9/8))))))

Theorem: sel-limits-check-4

(defthm sel-limits-check-4
  (implies (and (<= 63/64 (d$))
                (<= (d$) 9/8)
                (= (r$) 4)
                (= (a$) 2)
                (member k '(-1 0 1 2)))
           (and (<= (+ (max (sel-lower-div k 63/64)
                            (sel-lower-div k 9/8))
                       1/8)
                    (md4 k))
                (>= (min (sel-upper-div k 63/64)
                         (sel-upper-div k 9/8))
                    (md4 k)))))

Theorem: md4-k-bounds

(defthm md4-k-bounds
  (implies (and (<= 63/64 (d$))
                (<= (d$) 9/8)
                (= (r$) 4)
                (= (a$) 2))
           (and (implies (member k '(-1 0 1 2))
                         (<= (+ (sel-lower-div k (d$)) 1/8)
                             (md4 k)))
                (implies (member k '(-2 -1 0 1))
                         (>= (sel-upper-div k (d$))
                             (md4 (1+ k)))))))

Theorem: srt-div-rad-4

(defthm srt-div-rad-4
  (implies (and (= (r$) 4)
                (= (a$) 2)
                (<= 63/64 (d$))
                (<= (d$) 9/8)
                (natp j)
                (<= (abs (rem$ j)) (* 2/3 (d$)))
                (rationalp approx)
                (integerp (* 8 approx))
                (< (abs (- approx (* 4 (rem$ j)))) 1/8)
                (= (q$ (1+ j))
                   (select-digit-d4 approx)))
           (<= (abs (rem$ (1+ j))) (* 2/3 (d$)))))

Function: md8*64

(defun md8*64 (k i)
  (case (fl (/ i 2))
    (0 (case k
         (4 (if (= i 0) 113 115))
         (3 82)
         (2 50)
         (1 16)
         (0 -16)
         (-1 -48)
         (-2 -81)
         (-3 (if (= i 0) -112 -114))))
    (1 (case k
         (4 (if (= i 2) 117 118))
         (3 84)
         (2 50)
         (1 16)
         (0 -16)
         (-1 -50)
         (-2 -83)
         (-3 (if (= i 2) -116 -117))))
    (2 (case k
         (4 121)
         (3 86)
         (2 52)
         (1 16)
         (0 -16)
         (-1 -52)
         (-2 -86)
         (-3 -120)))
    (3 (case k
         (4 125)
         (3 90)
         (2 54)
         (1 18)
         (0 -18)
         (-1 -54)
         (-2 -88)
         (-3 -124)))
    (4 (case k
         (4 128)
         (3 92)
         (2 54)
         (1 18)
         (0 -18)
         (-1 -54)
         (-2 -90)
         (-3 -127)))
    (5 (case k
         (4 132)
         (3 94)
         (2 56)
         (1 18)
         (0 -18)
         (-1 -56)
         (-2 -94)
         (-3 -131)))
    (6 (case k
         (4 135)
         (3 96)
         (2 58)
         (1 18)
         (0 -18)
         (-1 -58)
         (-2 -96)
         (-3 -134)))
    (7 (case k
         (4 139)
         (3 100)
         (2 60)
         (1 20)
         (0 -20)
         (-1 -60)
         (-2 -98)
         (-3 -138)))
    (8 (case k
         (4 142)
         (3 102)
         (2 60)
         (1 20)
         (0 -20)
         (-1 -60)
         (-2 -100)
         (-3 -141)))
    (9 (case k
         (4 146)
         (3 104)
         (2 62)
         (1 20)
         (0 -20)
         (-1 -62)
         (-2 -104)
         (-3 -144)))
    (10 (case k
          (4 150)
          (3 106)
          (2 64)
          (1 20)
          (0 -20)
          (-1 -64)
          (-2 -106)
          (-3 -148)))
    (11 (case k
          (4 152)
          (3 108)
          (2 64)
          (1 20)
          (0 -20)
          (-1 -64)
          (-2 -108)
          (-3 -152)))
    (12 (case k
          (4 156)
          (3 112)
          (2 66)
          (1 22)
          (0 -22)
          (-1 -66)
          (-2 -112)
          (-3 -156)))
    (13 (case k
          (4 160)
          (3 114)
          (2 68)
          (1 22)
          (0 -22)
          (-1 -68)
          (-2 -114)
          (-3 -158)))
    (14 (case k
          (4 164)
          (3 116)
          (2 70)
          (1 24)
          (0 -24)
          (-1 -70)
          (-2 -116)
          (-3 -162)))
    (15 (case k
          (4 166)
          (3 118)
          (2 70)
          (1 24)
          (0 -24)
          (-1 -70)
          (-2 -118)
          (-3 -166)))
    (16 (case k
          (4 170)
          (3 120)
          (2 72)
          (1 24)
          (0 -24)
          (-1 -72)
          (-2 -120)
          (-3 -170)))
    (17 (case k
          (4 173)
          (3 124)
          (2 73)
          (1 24)
          (0 -24)
          (-1 -72)
          (-2 -124)
          (-3 -172)))
    (18 (case k
          (4 176)
          (3 126)
          (2 76)
          (1 24)
          (0 -24)
          (-1 -76)
          (-2 -124)
          (-3 -176)))
    (19 (case k
          (4 180)
          (3 128)
          (2 76)
          (1 24)
          (0 -24)
          (-1 -76)
          (-2 -128)
          (-3 -180)))
    (20 (case k
          (4 184)
          (3 132)
          (2 78)
          (1 24)
          (0 -24)
          (-1 -78)
          (-2 -132)
          (-3 -184)))
    (21 (case k
          (4 188)
          (3 134)
          (2 80)
          (1 28)
          (0 -28)
          (-1 -80)
          (-2 -134)
          (-3 -188)))
    (22 (case k
          (4 190)
          (3 136)
          (2 82)
          (1 28)
          (0 -28)
          (-1 -82)
          (-2 -136)
          (-3 -190)))
    (23 (case k
          (4 194)
          (3 138)
          (2 82)
          (1 28)
          (0 -28)
          (-1 -82)
          (-2 -138)
          (-3 -194)))
    (24 (case k
          (4 198)
          (3 140)
          (2 84)
          (1 28)
          (0 -28)
          (-1 -84)
          (-2 -140)
          (-3 -198)))
    (25 (case k
          (4 200)
          (3 142)
          (2 84)
          (1 28)
          (0 -28)
          (-1 -84)
          (-2 -142)
          (-3 -200)))
    (26 (case k
          (4 204)
          (3 146)
          (2 86)
          (1 28)
          (0 -28)
          (-1 -86)
          (-2 -146)
          (-3 -204)))
    (27 (case k
          (4 208)
          (3 148)
          (2 88)
          (1 28)
          (0 -28)
          (-1 -88)
          (-2 -148)
          (-3 -208)))
    (28 (case k
          (4 212)
          (3 152)
          (2 90)
          (1 28)
          (0 -28)
          (-1 -90)
          (-2 -152)
          (-3 -212)))
    (29 (case k
          (4 214)
          (3 152)
          (2 90)
          (1 28)
          (0 -28)
          (-1 -90)
          (-2 -152)
          (-3 -214)))
    (30 (case k
          (4 218)
          (3 154)
          (2 94)
          (1 28)
          (0 -28)
          (-1 -94)
          (-2 -154)
          (-3 -218)))
    (31 (case k
          (4 222)
          (3 158)
          (2 94)
          (1 32)
          (0 -32)
          (-1 -94)
          (-2 -158)
          (-3 -222)))))

Function: md8

(defun md8 (k i) (/ (md8*64 k i) 64))

Function: max-lower

(defun max-lower (i k)
  (max (sel-lower-div k (+ 1/2 (/ i 128)))
       (sel-lower-div k (+ 1/2 (/ (1+ i) 128)))))

Function: min-upper

(defun min-upper (i k)
  (min (sel-upper-div k (+ 1/2 (/ i 128)))
       (sel-upper-div k (+ 1/2 (/ (1+ i) 128)))))

Theorem: sel-limits-check-8

(defthm sel-limits-check-8
  (implies (and (= (r$) 8)
                (= (a$) 4)
                (bvecp i 6)
                (member k '(-3 -2 -1 0 1 2 3 4)))
           (and (<= (+ (max-lower i k) 1/64) (md8 k i))
                (>= (min-upper i (1- k)) (md8 k i)))))

Function: i64

(defun i64 (d) (fl (* 128 (- d 1/2))))

Theorem: sel-limits-8

(defthm sel-limits-8
  (implies (and (= (r$) 8)
                (= (a$) 4)
                (<= 1/2 (d$))
                (< (d$) 1)
                (member k '(-4 -3 -2 -1 0 1 2 3 4)))
           (and (<= (sel-lower-div k (d$))
                    (max-lower (i64 (d$)) k))
                (>= (sel-upper-div k (d$))
                    (min-upper (i64 (d$)) k)))))

Theorem: md8-k-bounds

(defthm md8-k-bounds
  (implies (and (= (r$) 8)
                (= (a$) 4)
                (<= 1/2 (d$))
                (< (d$) 1))
           (and (implies (member k '(-3 -2 -1 0 1 2 3 4))
                         (<= (+ (sel-lower-div k (d$)) 1/64)
                             (md8 k (i64 (d$)))))
                (implies (member k '(-4 -3 -2 -1 0 1 2 3))
                         (>= (sel-upper-div k (d$))
                             (md8 (1+ k) (i64 (d$))))))))

Function: select-digit-d8

(defun select-digit-d8 (a i)
  (cond ((<= (md8 4 i) a) 4)
        ((<= (md8 3 i) a) 3)
        ((<= (md8 2 i) a) 2)
        ((<= (md8 1 i) a) 1)
        ((<= (md8 0 i) a) 0)
        ((<= (md8 -1 i) a) -1)
        ((<= (md8 -2 i) a) -2)
        ((<= (md8 -3 i) a) -3)
        (t -4)))

Theorem: srt-div-rad-8

(defthm srt-div-rad-8
  (implies (and (= (r$) 8)
                (= (a$) 4)
                (<= 1/2 (d$))
                (< (d$) 1)
                (natp j)
                (<= (abs (rem$ j)) (* 4/7 (d$)))
                (rationalp approx)
                (integerp (* 64 approx))
                (< (abs (- approx (* 8 (rem$ j)))) 1/64)
                (= (q$ (1+ j))
                   (select-digit-d8 approx (i64 (d$)))))
           (<= (abs (rem$ (1+ j))) (* 4/7 (d$)))))