• 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

SSE Floating-Point Instructions

SSE Floating-Point Instructions

Definitions and Theorems

Function: ibit

(defun ibit nil
  (declare (xargs :guard t))
  0)

Function: dbit

(defun dbit nil
  (declare (xargs :guard t))
  1)

Function: zbit

(defun zbit nil
  (declare (xargs :guard t))
  2)

Function: obit

(defun obit nil
  (declare (xargs :guard t))
  3)

Function: ubit

(defun ubit nil
  (declare (xargs :guard t))
  4)

Function: pbit

(defun pbit nil
  (declare (xargs :guard t))
  5)

Function: daz

(defun daz nil
  (declare (xargs :guard t))
  6)

Function: imsk

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

Function: dmsk

(defun dmsk nil
  (declare (xargs :guard t))
  8)

Function: zmsk

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

Function: omsk

(defun omsk nil
  (declare (xargs :guard t))
  10)

Function: umsk

(defun umsk nil
  (declare (xargs :guard t))
  11)

Function: pmsk

(defun pmsk nil
  (declare (xargs :guard t))
  12)

Function: ftz

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

Function: mxcsr-masks

(defun mxcsr-masks (mxcsr)
  (declare (xargs :guard (natp mxcsr)))
  (bits mxcsr 12 7))

Function: mxcsr-rc

(defun mxcsr-rc (mxcsr)
  (declare (xargs :guard (natp mxcsr)))
  (case (bits mxcsr 14 13)
    (0 'rne)
    (1 'rdn)
    (2 'rup)
    (3 'rtz)))

Function: set-flag

(defun set-flag (b flags)
  (declare (xargs :guard (and (natp b) (natp flags))))
  (logior flags (expt 2 b)))

Function: unmasked-excp-p

(defun unmasked-excp-p (flags masks)
  (declare (xargs :guard (and (natp flags) (natp masks))))
  (or (and (= (bitn flags (ibit)) 1)
           (= (bitn masks (ibit)) 0))
      (and (= (bitn flags (dbit)) 1)
           (= (bitn masks (dbit)) 0))
      (and (= (bitn flags (zbit)) 1)
           (= (bitn masks (zbit)) 0))
      (and (= (bitn flags (obit)) 1)
           (= (bitn masks (obit)) 0))
      (and (= (bitn flags (ubit)) 1)
           (= (bitn masks (ubit)) 0))
      (and (= (bitn flags (pbit)) 1)
           (= (bitn masks (pbit)) 0))))

Function: dazify

(defun dazify (x daz f)
  (declare (xargs :guard (and (encodingp x f) (natp daz))))
  (if (and (= daz 1) (denormp x f))
      (zencode (sgnf x f) f)
    x))

Function: binary-undefined-p

(defun binary-undefined-p (op a af b bf)
  (declare (xargs :guard (and (member op '(add sub mul div))
                              (encodingp a af)
                              (encodingp b bf))))
  (case op
    (add (and (infp a af)
              (infp b bf)
              (not (= (sgnf a af) (sgnf b bf)))))
    (sub (and (infp a af)
              (infp b bf)
              (= (sgnf a af) (sgnf b bf))))
    (mul (and (or (infp a af) (infp b bf))
              (or (zerp a af) (zerp b bf))))
    (div (or (and (infp a af) (infp b bf))
             (and (zerp a af) (zerp b bf))))))

Function: sse-binary-pre-comp-excp

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

Function: sse-binary-pre-comp-val

(defun sse-binary-pre-comp-val (op a b f)
  (declare (xargs :guard (and (member op '(add sub mul div))
                              (encodingp a f)
                              (encodingp b f))))
  (if (nanp a f)
      (qnanize a f)
    (if (nanp b f)
        (qnanize b f)
      (if (binary-undefined-p op a f b f)
          (indef f)
        nil))))

Function: sse-binary-pre-comp

(defun sse-binary-pre-comp (op a b mxcsr f)
  (declare (xargs :guard (and (member op '(add sub mul div))
                              (encodingp a f)
                              (encodingp b f)
                              (natp mxcsr))))
  (let* ((daz (bitn mxcsr (daz)))
         (a (dazify a daz f))
         (b (dazify b daz f)))
    (mv a b (sse-binary-pre-comp-val op a b f)
        (sse-binary-pre-comp-excp op a b f))))

Function: sse-post-comp

(defun sse-post-comp (u mxcsr f)
 (declare (xargs :guard (and (real/rationalp u)
                             (not (= u 0))
                             (natp mxcsr)
                             (formatp f))))
 (let* ((rmode (mxcsr-rc mxcsr))
        (r (rnd u rmode (prec f)))
        (rsgn (if (< r 0) 1 0))
        (flags (if (= r u) 0 (set-flag (pbit) 0))))
   (if (> (abs r) (lpn f))
       (let* ((flags (set-flag (obit) flags)))
         (if (= (bitn mxcsr (omsk)) 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 f)) f)
                       flags)
                 (mv (iencode rsgn f) flags)))
           (mv nil flags)))
     (if (< (abs r) (spn f))
         (if (= (bitn mxcsr (umsk)) 1)
             (if (= (bitn mxcsr (ftz)) 1)
                 (mv (zencode rsgn f)
                     (set-flag (pbit)
                               (set-flag (ubit) flags)))
               (let ((d (drnd u rmode f)))
                 (if (= d u)
                     (mv (dencode d f) flags)
                   (let ((flags (set-flag (pbit)
                                          (set-flag (ubit) flags))))
                     (if (= d 0)
                         (mv (zencode rsgn f) flags)
                       (if (= (abs d) (spn f))
                           (mv (nencode d f) flags)
                         (mv (dencode d f) flags)))))))
           (mv nil (set-flag (ubit) flags)))
       (mv (nencode r f) flags)))))

Function: binary-inf-sgn

(defun binary-inf-sgn (op a af b bf)
  (declare (xargs :guard (and (member op '(add sub mul div))
                              (encodingp a af)
                              (encodingp b bf))))
  (case op
    (add (if (infp a af)
             (sgnf a af)
           (sgnf b bf)))
    (sub (if (infp a af)
             (sgnf a af)
           (if (zerop (sgnf b bf)) 1 0)))
    ((mul div)
     (logxor (sgnf a af) (sgnf b bf)))))

Function: binary-zero-sgn

(defun binary-zero-sgn (op asgn bsgn rmode)
  (declare (xargs :guard (and (member op '(add sub mul div))
                              (bvecp asgn 1)
                              (bvecp bsgn 1)
                              (ieee-rounding-mode-p rmode))))
  (case op
    (add (if (= asgn bsgn)
             asgn
           (if (eql rmode 'rdn) 1 0)))
    (sub (if (not (= asgn bsgn))
             asgn
           (if (eql rmode 'rdn) 1 0)))
    ((mul div) (logxor asgn bsgn))))

Function: binary-eval

(defun binary-eval (op aval bval)
 (declare (xargs :guard (and (member op '(add sub mul div))
                             (real/rationalp aval)
                             (real/rationalp bval)
                             (not (and (eql op 'div) (= bval 0))))))
 (case op
   (add (+ aval bval))
   (sub (- aval bval))
   (mul (* aval bval))
   (div (/ aval bval))))

Function: sse-binary-comp

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

Function: sse-binary-spec

(defun sse-binary-spec (op a b mxcsr f)
 (declare (xargs :guard (and (member op '(add sub mul div))
                             (encodingp a f)
                             (encodingp b f)
                             (natp mxcsr))))
 (mv-let (adaz bdaz result pre-flags)
         (sse-binary-pre-comp op a b mxcsr f)
  (if (unmasked-excp-p pre-flags (mxcsr-masks mxcsr))
      (mv nil (logior mxcsr pre-flags))
   (if result (mv result (logior mxcsr pre-flags))
    (mv-let (result post-flags)
            (sse-binary-comp op adaz bdaz mxcsr f)
     (mv (and (not (unmasked-excp-p post-flags (mxcsr-masks mxcsr)))
              result)
         (logior (logior mxcsr pre-flags)
                 post-flags)))))))

Function: sse-sqrt-pre-comp-excp

(defun sse-sqrt-pre-comp-excp (a f)
  (declare (xargs :guard (encodingp a f)))
  (if (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 (denormp a f)
            (set-flag (dbit) 0)
          0)))))

Function: sse-sqrt-pre-comp-val

(defun sse-sqrt-pre-comp-val (a f)
  (declare (xargs :guard (encodingp a f)))
  (if (nanp a f)
      (qnanize a f)
    (if (and (not (zerp a f)) (= (sgnf a f) 1))
        (indef f)
      nil)))

Function: sse-sqrt-pre-comp

(defun sse-sqrt-pre-comp (a mxcsr f)
  (declare (xargs :guard (and (encodingp a f) (natp mxcsr))))
  (let ((a (dazify a (bitn mxcsr (daz)) f)))
    (mv a (sse-sqrt-pre-comp-val a f)
        (sse-sqrt-pre-comp-excp a f))))

Function: sse-sqrt-comp

(defun sse-sqrt-comp (a mxcsr f)
  (declare (xargs :guard (and (encodingp a f)
                              (or (zerp a f) (= (sgnf a f) 0))
                              (natp mxcsr))))
  (if (or (infp a f) (zerp a f))
      (mv a 0)
    (sse-post-comp (qsqrt (decode a f) (+ (prec f) 2))
                   mxcsr f)))

Function: sse-sqrt-spec

(defun sse-sqrt-spec (a mxcsr f)
 (declare (xargs :guard (and (encodingp a f) (natp mxcsr))))
 (mv-let (adaz result pre-flags)
         (sse-sqrt-pre-comp a mxcsr f)
  (if (unmasked-excp-p pre-flags (mxcsr-masks mxcsr))
      (mv nil (logior mxcsr pre-flags))
   (if result (mv result (logior mxcsr pre-flags))
    (mv-let (result post-flags)
            (sse-sqrt-comp adaz mxcsr f)
     (mv (and (not (unmasked-excp-p post-flags (mxcsr-masks mxcsr)))
              result)
         (logior (logior mxcsr pre-flags)
                 post-flags)))))))

Function: fma-undefined-p

(defun fma-undefined-p (a b c f)
  (declare (xargs :guard (and (encodingp a f)
                              (encodingp b f)
                              (encodingp c f))))
  (and (or (infp a f) (infp b f))
       (or (zerp a f)
           (zerp b f)
           (and (not (nanp a f))
                (not (nanp b f))
                (infp c f)
                (not (= (sgnf c f)
                        (logxor (sgnf a f) (sgnf b f))))))))

Function: sse-fma-pre-comp-excp

(defun sse-fma-pre-comp-excp (a b c f)
  (declare (xargs :guard (and (encodingp a f)
                              (encodingp b f)
                              (encodingp c f))))
  (if (or (snanp a f) (snanp b f) (snanp c f))
      (set-flag (ibit) 0)
    (if (or (qnanp a f) (qnanp b f) (qnanp c f))
        0
      (if (fma-undefined-p a b c f)
          (set-flag (ibit) 0)
        (if (or (denormp a f)
                (denormp b f)
                (denormp c f))
            (set-flag (dbit) 0)
          0)))))

Function: sse-fma-pre-comp-val

(defun sse-fma-pre-comp-val (a b c f)
  (declare (xargs :guard (and (encodingp a f)
                              (encodingp b f)
                              (encodingp c f))))
  (if (nanp a f)
      (qnanize a f)
    (if (nanp b f)
        (qnanize b f)
      (if (nanp c f)
          (qnanize c f)
        (if (fma-undefined-p a b c f)
            (indef f)
          nil)))))

Function: sse-fma-pre-comp

(defun sse-fma-pre-comp (a b c mxcsr f)
  (declare (xargs :guard (and (encodingp a f)
                              (encodingp b f)
                              (encodingp c f)
                              (natp mxcsr))))
  (let* ((daz (bitn mxcsr (daz)))
         (a (dazify a daz f))
         (b (dazify b daz f))
         (c (dazify c daz f)))
    (mv a b c (sse-fma-pre-comp-val a b c f)
        (sse-fma-pre-comp-excp a b c f))))

Function: sse-fma-comp

(defun sse-fma-comp (a b c mxcsr f)
  (declare (xargs :guard (and (encodingp a f)
                              (encodingp b f)
                              (encodingp c f)
                              (natp mxcsr))))
  (let* ((asgn (sgnf a f))
         (bsgn (sgnf b f))
         (csgn (sgnf c f))
         (aval (decode a f))
         (bval (decode b f))
         (cval (decode c f))
         (u (+ (* aval bval) cval)))
    (if (or (infp a f) (infp b f))
        (mv (iencode (logxor asgn bsgn) f) 0)
      (if (infp c f)
          (mv c 0)
        (if (= u 0)
            (mv (zencode (if (= (logxor asgn bsgn) csgn)
                             csgn
                           (if (eql (mxcsr-rc mxcsr) 'rdn) 1 0))
                         f)
                0)
          (sse-post-comp u mxcsr f))))))

Function: sse-fma-spec

(defun sse-fma-spec (a b c mxcsr f)
 (declare (xargs :guard (and (encodingp a f)
                             (encodingp b f)
                             (encodingp c f)
                             (natp mxcsr))))
 (mv-let (adaz bdaz cdaz result pre-flags)
         (sse-fma-pre-comp a b c mxcsr f)
  (if (unmasked-excp-p pre-flags (mxcsr-masks mxcsr))
      (mv nil (logior mxcsr pre-flags))
   (if result (mv result (logior mxcsr pre-flags))
    (mv-let (result post-flags)
            (sse-fma-comp adaz bdaz cdaz mxcsr f)
     (mv (and (not (unmasked-excp-p post-flags (mxcsr-masks mxcsr)))
              result)
         (logior (logior mxcsr pre-flags)
                 post-flags)))))))