• 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

ARM AArch32 Floating-Point Instructions

ARM AArch32 Floating-Point Instructions

Definitions and Theorems

Function: ioc

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

Function: dzc

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

Function: ofc

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

Function: ufc

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

Function: ixc

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

Function: idc

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

Function: fpscr-rc

(defun fpscr-rc (fpscr)
  (declare (xargs :guard (natp fpscr)))
  (case (bits fpscr 23 22)
    (0 'rne)
    (1 'rup)
    (2 'rdn)
    (3 'rtz)))

Function: fz

(defun fz nil
  (declare (xargs :guard t))
  24)

Function: dn

(defun dn nil
  (declare (xargs :guard t))
  25)

Function: process-nan

(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: arm-binary-pre-comp-excp

(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: arm-binary-pre-comp-val

(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: arm-binary-pre-comp

(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: arm-post-comp

(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: arm-binary-comp

(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: arm-binary-spec

(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: arm-sqrt-pre-comp-excp

(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: arm-sqrt-pre-comp-val

(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: arm-sqrt-pre-comp

(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: arm-sqrt-comp

(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: arm-sqrt-spec

(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: arm-fma-pre-comp-excp

(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: arm-fma-pre-comp-val

(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: arm-fma-pre-comp

(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: arm-fma-comp

(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: arm-fma-spec

(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: arm-fscale-pre-comp

(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: arm-fscale-comp

(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: arm-fscale-spec

(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: bf-post-comp

(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: bfmul16-spec

(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: bfadd32-spec

(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)))))))