ARM AArch32 Floating-Point Instructions
Function:
(defun ioc nil (declare (xargs :guard t)) 0)
Function:
(defun dzc nil (declare (xargs :guard t)) 1)
Function:
(defun ofc nil (declare (xargs :guard t)) 2)
Function:
(defun ufc nil (declare (xargs :guard t)) 3)
Function:
(defun ixc nil (declare (xargs :guard t)) 4)
Function:
(defun idc nil (declare (xargs :guard t)) 7)
Function:
(defun fpscr-rc (fpscr) (declare (xargs :guard (natp fpscr))) (case (bits fpscr 23 22) (0 'rne) (1 'rup) (2 'rdn) (3 'rtz)))
Function:
(defun fz nil (declare (xargs :guard t)) 24)
Function:
(defun dn nil (declare (xargs :guard t)) 25)
Function:
(defun process-nan (x fpscr f) (declare (xargs :guard (and (encodingp x f) (natp fpscr)))) (if (= (bitn fpscr (dn)) 1) (indef f) (qnanize x f)))
Function:
(defun arm-binary-pre-comp-excp (op a b fpscr f) (declare (xargs :guard (and (member op '(add sub mul div)) (encodingp a f) (encodingp b f) (natp fpscr)))) (if (or (snanp a f) (snanp b f)) (set-flag (ioc) fpscr) (if (or (qnanp a f) (qnanp b f)) fpscr (if (binary-undefined-p op a f b f) (set-flag (ioc) fpscr) (if (and (eql op 'div) (zerp b f) (not (infp a f))) (set-flag (dzc) fpscr) fpscr)))))
Function:
(defun arm-binary-pre-comp-val (op a b fpscr f) (declare (xargs :guard (and (member op '(add sub mul div)) (encodingp a f) (encodingp b f) (natp fpscr)))) (if (snanp a f) (process-nan a fpscr f) (if (snanp b f) (process-nan b fpscr f) (if (qnanp a f) (process-nan a fpscr f) (if (qnanp b f) (process-nan b fpscr f) (if (binary-undefined-p op a f b f) (indef f) nil))))))
Function:
(defun arm-binary-pre-comp (op a b fpscr f) (declare (xargs :guard (and (member op '(add sub mul div)) (encodingp a f) (encodingp b f) (natp fpscr)))) (mv-let (a b fpscr) (if (= (bitn fpscr (fz)) 1) (mv (if (denormp a f) (zencode (sgnf a f) f) a) (if (denormp b f) (zencode (sgnf b f) f) b) (if (and (or (denormp a f) (denormp b f)) (not (equal f (hp)))) (set-flag (idc) fpscr) fpscr)) (mv a b fpscr)) (mv a b (arm-binary-pre-comp-val op a b fpscr f) (arm-binary-pre-comp-excp op a b fpscr f))))
Function:
(defun arm-post-comp (u fpscr f) (declare (xargs :guard (and (real/rationalp u) (not (= u 0)) (natp fpscr) (formatp f)))) (let* ((rmode (fpscr-rc fpscr)) (r (rnd u rmode (prec f))) (sgn (if (< u 0) 1 0))) (if (> (abs r) (lpn f)) (let ((fpscr (set-flag (ofc) (set-flag (ixc) fpscr)))) (if (or (and (eql rmode 'rdn) (> r 0)) (and (eql rmode 'rup) (< r 0)) (eql rmode 'rtz)) (mv (nencode (* (sgn r) (lpn f)) f) fpscr) (mv (iencode sgn f) fpscr))) (if (< (abs u) (spn f)) (if (= (bitn fpscr (fz)) 1) (mv (zencode sgn f) (set-flag (ufc) fpscr)) (let ((d (drnd u rmode f))) (if (= d u) (mv (dencode d f) fpscr) (let ((fpscr (set-flag (ixc) (set-flag (ufc) fpscr)))) (if (= d 0) (mv (zencode sgn f) fpscr) (if (= (abs d) (spn f)) (mv (nencode d f) fpscr) (mv (dencode d f) fpscr))))))) (mv (nencode r f) (if (= r u) fpscr (set-flag (ixc) fpscr)))))))
Function:
(defun arm-binary-comp (op a b fpscr f) (declare (xargs :guard (and (member op '(add sub mul div)) (encodingp a f) (encodingp b f) (natp fpscr)))) (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) fpscr) (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 (fpscr-rc fpscr)) f) fpscr) (arm-post-comp u fpscr f)))))
Function:
(defun arm-binary-spec (op a b fpscr f) (declare (xargs :guard (and (member op '(add sub mul div)) (encodingp a f) (encodingp b f) (natp fpscr)))) (mv-let (a b result fpscr) (arm-binary-pre-comp op a b fpscr f) (if result (mv result fpscr) (arm-binary-comp op a b fpscr f))))
Function:
(defun arm-sqrt-pre-comp-excp (a fpscr f) (declare (xargs :guard (and (encodingp a f) (natp fpscr)))) (if (snanp a f) (set-flag (ioc) fpscr) (if (qnanp a f) fpscr (if (and (not (zerp a f)) (= (sgnf a f) 1)) (set-flag (ioc) fpscr) fpscr))))
Function:
(defun arm-sqrt-pre-comp-val (a fpscr f) (declare (xargs :guard (and (encodingp a f) (natp fpscr)))) (if (nanp a f) (process-nan a fpscr f) (if (and (not (zerp a f)) (= (sgnf a f) 1)) (indef f) nil)))
Function:
(defun arm-sqrt-pre-comp (a fpscr f) (declare (xargs :guard (and (encodingp a f) (natp fpscr)))) (mv-let (a fpscr) (if (and (denormp a f) (= (bitn fpscr (fz)) 1)) (mv (zencode (sgnf a f) f) (if (not (equal f (hp))) (set-flag (idc) fpscr) fpscr)) (mv a fpscr)) (mv a (arm-sqrt-pre-comp-val a fpscr f) (arm-sqrt-pre-comp-excp a fpscr f))))
Function:
(defun arm-sqrt-comp (a fpscr f) (declare (xargs :guard (and (encodingp a f) (or (zerp a f) (= (sgnf a f) 0)) (natp fpscr)))) (if (or (infp a f) (zerp a f)) (mv a fpscr) (arm-post-comp (qsqrt (decode a f) (+ (prec f) 2)) fpscr f)))
Function:
(defun arm-sqrt-spec (a fpscr f) (declare (xargs :guard (and (encodingp a f) (natp fpscr)))) (mv-let (a result fpscr) (arm-sqrt-pre-comp a fpscr f) (if result (mv result fpscr) (arm-sqrt-comp a fpscr f))))
Function:
(defun arm-fma-pre-comp-excp (a b c fpscr f) (declare (xargs :guard (and (encodingp a f) (encodingp b f) (encodingp c f) (natp fpscr)))) (if (or (snanp a f) (snanp b f) (snanp c f) (fma-undefined-p b c a f)) (set-flag (ioc) fpscr) fpscr))
Function:
(defun arm-fma-pre-comp-val (a b c fpscr f) (declare (xargs :guard (and (encodingp a f) (encodingp b f) (encodingp c f) (natp fpscr)))) (if (snanp a f) (process-nan a fpscr f) (if (snanp b f) (process-nan b fpscr f) (if (snanp c f) (process-nan c fpscr f) (if (fma-undefined-p b c a f) (indef f) (if (qnanp a f) (process-nan a fpscr f) (if (qnanp b f) (process-nan b fpscr f) (if (qnanp c f) (process-nan c fpscr f) nil))))))))
Function:
(defun arm-fma-pre-comp (a b c fpscr f) (declare (xargs :guard (and (encodingp a f) (encodingp b f) (encodingp c f) (natp fpscr)))) (mv-let (a b c fpscr) (if (= (bitn fpscr (fz)) 1) (mv (if (denormp a f) (zencode (sgnf a f) f) a) (if (denormp b f) (zencode (sgnf b f) f) b) (if (denormp c f) (zencode (sgnf c f) f) c) (if (and (or (denormp a f) (denormp b f) (denormp c f)) (not (equal f (hp)))) (set-flag (idc) fpscr) fpscr)) (mv a b c fpscr)) (mv a b c (arm-fma-pre-comp-val a b c fpscr f) (arm-fma-pre-comp-excp a b c fpscr f))))
Function:
(defun arm-fma-comp (a b c fpscr f) (declare (xargs :guard (and (encodingp a f) (encodingp b f) (encodingp c f) (natp fpscr)))) (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 b f) (infp c f)) (mv (iencode (logxor bsgn csgn) f) fpscr) (if (infp a f) (mv a fpscr) (if (= u 0) (mv (zencode (if (= (logxor bsgn csgn) asgn) asgn (if (eql (fpscr-rc fpscr) 'rdn) 1 0)) f) fpscr) (arm-post-comp u fpscr f))))))
Function:
(defun arm-fma-spec (a b c fpscr f) (declare (xargs :guard (and (encodingp a f) (encodingp b f) (encodingp c f) (natp fpscr)))) (mv-let (a b c result fpscr) (arm-fma-pre-comp a b c fpscr f) (if result (mv result fpscr) (arm-fma-comp a b c fpscr f))))
Function:
(defun arm-fscale-pre-comp (a fpscr f) (declare (xargs :guard (and (encodingp a f) (natp fpscr)))) (mv-let (a fpscr) (if (and (= (bitn fpscr (fz)) 1) (denormp a f)) (mv (zencode (sgnf a f) f) (set-flag (idc) fpscr)) (mv a fpscr)) (mv a (if (nanp a f) (process-nan a fpscr f) nil) (if (snanp a f) (set-flag (ioc) fpscr) fpscr))))
Function:
(defun arm-fscale-comp (a b fpscr f) (declare (xargs :guard (and (encodingp a f) (natp b) (natp fpscr)))) (if (or (zerp a f) (infp a f)) (mv a fpscr) (let* ((fwidth (+ 1 (expw f) (sigw f))) (aval (decode a f)) (bval (si b fwidth)) (u (* aval (expt 2 bval)))) (arm-post-comp u fpscr f))))
Function:
(defun arm-fscale-spec (a b fpscr f) (declare (xargs :guard (and (encodingp a f) (natp b) (natp fpscr)))) (mv-let (a result fpscr) (arm-fscale-pre-comp a fpscr f) (if result (mv result fpscr) (arm-fscale-comp a b fpscr f))))
Function:
(defun bf-post-comp (u) (declare (xargs :guard (and (real/rationalp u) (not (= u 0))))) (let ((sgnf (if (< u 0) 1 0)) (r (rto u 24))) (if (> (abs r) (lpn (sp))) (iencode sgnf (sp)) (if (< (abs u) (spn (sp))) (zencode sgnf (sp)) (nencode r (sp))))))
Function:
(defun bfmul16-spec (a b) (declare (xargs :guard (and (encodingp a (bf)) (encodingp b (bf))))) (let ((sgnr (logxor (sgnf a (bf)) (sgnf b (bf))))) (if (or (nanp a (bf)) (nanp b (bf)) (and (infp a (bf)) (or (zerp b (bf)) (denormp b (bf)))) (and (infp b (bf)) (or (zerp a (bf)) (denormp a (bf))))) (indef (sp)) (if (or (infp a (bf)) (infp b (bf))) (iencode sgnr (sp)) (if (or (zerp a (bf)) (denormp a (bf)) (zerp b (bf)) (denormp b (bf))) (zencode sgnr (sp)) (bf-post-comp (* (ndecode a (bf)) (ndecode b (bf)))))))))
Function:
(defun bfadd32-spec (a b) (declare (xargs :guard (and (encodingp a (sp)) (encodingp b (sp))))) (let* ((sgna (sgnf a (sp))) (sgnb (sgnf b (sp))) (aval (if (or (zerp a (sp)) (denormp a (sp))) 0 (ndecode a (sp)))) (bval (if (or (zerp b (sp)) (denormp b (sp))) 0 (ndecode b (sp)))) (u (+ aval bval))) (if (or (nanp a (sp)) (nanp b (sp)) (and (infp a (sp)) (infp b (sp)) (not (= sgna sgnb)))) (indef (sp)) (if (infp a (sp)) a (if (infp b (sp)) b (if (= u 0) (if (= sgna sgnb) (zencode sgna (sp)) (zencode 0 (sp))) (bf-post-comp u)))))))