SSE Floating-Point Instructions
Function:
(defun ibit nil (declare (xargs :guard t)) 0)
Function:
(defun dbit nil (declare (xargs :guard t)) 1)
Function:
(defun zbit nil (declare (xargs :guard t)) 2)
Function:
(defun obit nil (declare (xargs :guard t)) 3)
Function:
(defun ubit nil (declare (xargs :guard t)) 4)
Function:
(defun pbit nil (declare (xargs :guard t)) 5)
Function:
(defun daz nil (declare (xargs :guard t)) 6)
Function:
(defun imsk nil (declare (xargs :guard t)) 7)
Function:
(defun dmsk nil (declare (xargs :guard t)) 8)
Function:
(defun zmsk nil (declare (xargs :guard t)) 9)
Function:
(defun omsk nil (declare (xargs :guard t)) 10)
Function:
(defun umsk nil (declare (xargs :guard t)) 11)
Function:
(defun pmsk nil (declare (xargs :guard t)) 12)
Function:
(defun ftz nil (declare (xargs :guard t)) 15)
Function:
(defun mxcsr-masks (mxcsr) (declare (xargs :guard (natp mxcsr))) (bits mxcsr 12 7))
Function:
(defun mxcsr-rc (mxcsr) (declare (xargs :guard (natp mxcsr))) (case (bits mxcsr 14 13) (0 'rne) (1 'rdn) (2 'rup) (3 'rtz)))
Function:
(defun set-flag (b flags) (declare (xargs :guard (and (natp b) (natp flags)))) (logior flags (expt 2 b)))
Function:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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)))))))