• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • 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
          • SSE Floating-Point Instructions
          • ARM AArch32 Floating-Point Instructions
          • X87 Instructions
          • IEEE-Compliant Square Root
        • Implementation of Elementary Operations
        • Register-Transfer Logic
        • Floating-Point Arithmetic
        • Modeling Algorithms in C++ and ACL2
        • Bibliography
    • Algebra
  • Testing-utilities

• Floating-Point Exceptions and Specification of Elementary Arithmetic Instructions

X87 Instructions

x87 Instructions

Definitions and Theorems

Function: fcw-rc

(defun fcw-rc (fcw)
  (declare (xargs :guard (natp fcw)))
  (case (bits fcw 11 10)
    (0 'rne)
    (1 'rdn)
    (2 'rup)
    (3 'rtz)))

Function: fcw-pc

(defun fcw-pc (fcw)
  (declare (xargs :guard (natp fcw)))
  (case (bits fcw 9 8)
    ((0 1) 24)
    (2 53)
    (3 64)))

Function: es

(defun es nil
  (declare (xargs :guard t))
  7)

Function: bb

(defun bb nil
  (declare (xargs :guard t))
  15)

Function: c1

(defun c1 nil
  (declare (xargs :guard t))
  9)

Function: set-es

(defun set-es (fsw)
  (declare (xargs :guard (natp fsw)))
  (set-flag (bb) (set-flag (es) fsw)))

Function: clear-c1

(defun clear-c1 (fsw)
  (declare (xargs :guard (natp fsw)))
  (logand fsw 65023))

Function: x87-binary-pre-comp-excp

(defun x87-binary-pre-comp-excp (op a af b bf)
  (declare (xargs :guard (and (member op '(add sub mul div))
                              (encodingp a af)
                              (encodingp b bf))))
  (if (or (snanp a af)
          (unsupp a af)
          (snanp b bf)
          (unsupp b bf))
      (set-flag (ibit) 0)
    (if (or (qnanp a af) (qnanp b bf))
        0
      (if (binary-undefined-p op a af b bf)
          (set-flag (ibit) 0)
        (if (and (eql op 'div)
                 (zerp b bf)
                 (not (infp a af)))
            (set-flag (zbit) 0)
          (if (or (denormp a af)
                  (pseudop a af)
                  (denormp b bf)
                  (pseudop b bf))
              (set-flag (dbit) 0)
            0))))))

Function: convert-nan-to-ep

(defun convert-nan-to-ep (x f)
  (declare (xargs :guard (and (encodingp x f) (<= (prec f) 64))))
  (cat (sgnf x f)
       1 (1- (expt 2 15))
       15 1 1 (manf x f)
       (1- (prec f))
       0 (- 64 (prec f))))

Function: x87-binary-pre-comp-val

(defun x87-binary-pre-comp-val (op a af b bf)
  (declare (xargs :guard (and (member op '(add sub mul div))
                              (encodingp a af)
                              (encodingp b bf)
                              (<= (prec af) 64)
                              (<= (prec bf) 64))))
  (let ((aep (convert-nan-to-ep a af))
        (bep (convert-nan-to-ep b bf)))
    (if (nanp a af)
        (if (nanp b bf)
            (if (> (sigf aep (ep)) (sigf bep (ep)))
                (qnanize aep (ep))
              (if (< (sigf aep (ep)) (sigf bep (ep)))
                  (qnanize bep (ep))
                (if (= (sgnf aep (ep)) 0)
                    (qnanize (convert-nan-to-ep a af) (ep))
                  (qnanize (convert-nan-to-ep b bf)
                           (ep)))))
          (qnanize aep (ep)))
      (if (nanp b bf)
          (qnanize bep (ep))
        (if (binary-undefined-p op a af b bf)
            (indef (ep))
          nil)))))

Function: x87-binary-pre-comp

(defun x87-binary-pre-comp (op a af b bf)
  (declare (xargs :guard (and (member op '(add sub mul div))
                              (encodingp a af)
                              (encodingp b bf)
                              (<= (prec af) 64)
                              (<= (prec bf) 64))))
  (mv (x87-binary-pre-comp-val op a af b bf)
      (x87-binary-pre-comp-excp op a af b bf)))

Function: x87-post-comp

(defun x87-post-comp (u fcw)
  (declare (xargs :guard (and (real/rationalp u)
                              (not (= u 0))
                              (natp fcw))))
  (let* ((rmode (fcw-rc fcw))
         (r (rnd u rmode (fcw-pc fcw)))
         (rsgn (if (< r 0) 1 0))
         (flags (if (= r u) 0 (set-flag (pbit) 0))))
    (if (> (abs r) (lpn (ep)))
        (let ((flags (set-flag (obit) flags)))
          (if (= (bitn fcw (obit)) 1)
              (let ((flags (set-flag (pbit) flags)))
                (if (or (and (eql rmode 'rdn) (> r 0))
                        (and (eql rmode 'rup) (< r 0))
                        (eql rmode 'rtz))
                    (mv (nencode (* (sgn r) (lpn (ep))) (ep))
                        flags)
                  (mv (iencode rsgn (ep))
                      (set-flag (c1) flags))))
            (let ((s (* r (expt 2 (- (* 3 (expt 2 13)))))))
              (if (> (abs s) (lpn (ep)))
                  (mv (iencode rsgn (ep))
                      (set-flag (c1) (set-flag (pbit) flags)))
                (mv (nencode s (ep))
                    (if (> (abs r) (abs u))
                        (set-flag (c1) flags)
                      flags))))))
      (if (< (abs r) (spn (ep)))
          (if (= (bitn fcw (ubit)) 1)
              (let ((d (drnd u rmode (ep))))
                (if (= d u)
                    (mv (dencode d (ep)) flags)
                  (let ((flags (set-flag (pbit)
                                         (set-flag (ubit) flags))))
                    (if (= d 0)
                        (mv (zencode rsgn (ep)) flags)
                      (if (= (abs d) (spn (ep)))
                          (mv (nencode d (ep))
                              (set-flag (c1) flags))
                        (mv (dencode d (ep))
                            (if (> (abs d) (abs u))
                                (set-flag (c1) flags)
                              flags)))))))
            (let ((flags (set-flag (ubit) flags))
                  (s (* r (expt 2 (* 3 (expt 2 13))))))
              (if (< (abs s) (spn (ep)))
                  (mv (zencode rsgn (ep))
                      (set-flag (pbit) flags))
                (mv (nencode s (ep))
                    (if (> (abs r) (abs u))
                        (set-flag (c1) flags)
                      flags)))))
        (mv (nencode r (ep))
            (if (> (abs r) (abs u))
                (set-flag (c1) flags)
              flags))))))

Function: x87-binary-comp

(defun x87-binary-comp (op a af b bf fcw)
  (declare (xargs :guard (and (member op '(add sub mul div))
                              (encodingp a af)
                              (encodingp b bf)
                              (natp fcw))))
  (if (or (infp a af)
          (if (eql op 'div)
              (zerp b bf)
            (infp b bf)))
      (mv (iencode (binary-inf-sgn op a af b bf)
                   (ep))
          0)
    (let* ((asgn (sgnf a af))
           (bsgn (sgnf b bf))
           (aval (decode a af))
           (bval (decode b bf))
           (u (binary-eval op aval bval)))
      (if (or (and (eql op 'div) (infp b bf))
              (= u 0))
          (mv (zencode (binary-zero-sgn op asgn bsgn (fcw-rc fcw))
                       (ep))
              0)
        (x87-post-comp u fcw)))))

Function: x87-binary-spec

(defun x87-binary-spec (op a af b bf fcw fsw)
  (declare (xargs :guard (and (member op '(add sub mul div))
                              (encodingp a af)
                              (encodingp b bf)
                              (<= (prec af) 64)
                              (<= (prec bf) 64)
                              (natp fcw)
                              (natp fsw))))
  (let ((fsw (clear-c1 fsw)))
    (mv-let (result pre-flags)
            (x87-binary-pre-comp op a af b bf)
      (if (unmasked-excp-p pre-flags fcw)
          (mv nil (set-es (logior fsw pre-flags)))
        (if result (mv result (logior fsw pre-flags))
          (mv-let (result post-flags)
                  (x87-binary-comp op a af b bf fcw)
            (mv result
                (if (unmasked-excp-p post-flags fcw)
                    (set-es (logior (logior fsw pre-flags)
                                    post-flags))
                  (logior (logior fsw pre-flags)
                          post-flags)))))))))

Function: x87-sqrt-pre-comp-excp

(defun x87-sqrt-pre-comp-excp (a f)
  (declare (xargs :guard (encodingp a f)))
  (if (or (unsupp a f) (snanp a f))
      (set-flag (ibit) 0)
    (if (qnanp a f)
        0
      (if (and (not (zerp a f)) (= (sgnf a f) 1))
          (set-flag (ibit) 0)
        (if (or (denormp a f) (pseudop a f))
            (set-flag (dbit) 0)
          0)))))

Function: x87-sqrt-pre-comp-val

(defun x87-sqrt-pre-comp-val (a f)
  (declare (xargs :guard (and (encodingp a f) (<= (prec f) 64))))
  (if (nanp a f)
      (qnanize (convert-nan-to-ep a f) (ep))
    (if (and (not (zerp a f)) (= (sgnf a f) 1))
        (indef (ep))
      nil)))

Function: x87-sqrt-pre-comp

(defun x87-sqrt-pre-comp (a f)
  (declare (xargs :guard (and (encodingp a f) (<= (prec f) 64))))
  (mv (x87-sqrt-pre-comp-val a f)
      (x87-sqrt-pre-comp-excp a f)))

Function: x87-sqrt-comp

(defun x87-sqrt-comp (a f fcw)
  (declare (xargs :guard (and (encodingp a f)
                              (or (zerp a f) (= (sgnf a f) 0))
                              (<= (prec f) 64)
                              (natp fcw))))
  (if (or (infp a f) (zerp a f))
      (mv a 0)
    (x87-post-comp (qsqrt (decode a f) 66)
                   fcw)))

Function: x87-sqrt-spec

(defun x87-sqrt-spec (a f fcw fsw)
  (declare (xargs :guard (and (encodingp a f)
                              (<= (prec f) 64)
                              (natp fcw)
                              (natp fsw))))
  (let ((fsw (clear-c1 fsw)))
    (mv-let (result pre-flags)
            (x87-sqrt-pre-comp a f)
      (if (unmasked-excp-p pre-flags fcw)
          (mv nil (set-es (logior fsw pre-flags)))
        (if result (mv result (logior fsw pre-flags))
          (mv-let (result post-flags)
                  (x87-sqrt-comp a f fcw)
            (mv result
                (if (unmasked-excp-p post-flags fcw)
                    (set-es (logior (logior fsw pre-flags)
                                    post-flags))
                  (logior (logior fsw pre-flags)
                          post-flags)))))))))