		Search-engine friendly clone of the ACL2 documentation.

Basic-floating-point-utilities

Fp-decode

Signature
(fp-decode x exp-width frac-width) → (mv * * * * *)
Arguments: x — Guard (integerp x).; exp-width — Guard (posp exp-width).; frac-width — Guard (posp frac-width).

This function returns:

One of the symbols INDEF, QNAN, SNAN, INF, ZERO, DENORMAL, or NORMAL
sign bit
exponent bits
implicit bit value
fraction bits

Definitions and Theorems

Function: fp-decode

(defun fp-decode (x exp-width frac-width)
 (declare (xargs :guard (and (integerp x)
                             (posp exp-width)
                             (posp frac-width))))
 (let ((__function__ 'fp-decode))
  (declare (ignorable __function__))
  (b* ((sign-bit-index (+ frac-width exp-width))
       (frac (part-select x
                          :low 0
                          :width frac-width))
       (exp (part-select x
                         :low frac-width
                         :width exp-width))
       (sign (part-select x
                          :low sign-bit-index
                          :width 1)))
   (cond
      ((eql exp 0)
       (b* ((sym (if (not (eql frac 0))
                     'denormal
                   'zero)))
         (mv sym sign exp 0 frac)))
      ((eql exp (1- (ash 1 exp-width)))
       (if (eql frac 0)
           (mv 'inf sign exp 1 frac)
         (let ((sym (if (logbitp (1- frac-width) frac)
                        (if (and (eql sign 1)
                                 (eql frac (ash 1 (1- frac-width))))
                            'indef
                          'qnan)
                      'snan)))
           (mv sym sign exp 1 frac))))
      (t (mv 'normal sign exp 1 frac))))))

Theorem: n01p-fp-decode-sign-bit

(defthm n01p-fp-decode-sign-bit
 (unsigned-byte-p 1
                  (mv-nth 1 (fp-decode x exp-width frac-width)))
 :rule-classes
 (:rewrite
  (:type-prescription
     :corollary (bitp (mv-nth 1 (fp-decode x exp-width frac-width)))
     :hints
     (("Goal"
           :in-theory
           '(unsigned-byte-p integer-range-p natp bitp (:e expt)))))
  (:linear
   :corollary
   (and (<= 0
            (mv-nth 1 (fp-decode x exp-width frac-width)))
        (< (mv-nth 1 (fp-decode x exp-width frac-width))
           2))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))

Theorem: natp-exp-fp-decode

(defthm natp-exp-fp-decode
  (implies (posp exp-width)
           (natp (mv-nth 2 (fp-decode x exp-width frac-width))))
  :rule-classes :type-prescription)

Theorem: exp-width-wide-exp-from-fp-decode-lemma

(defthm exp-width-wide-exp-from-fp-decode-lemma
 (implies
    (posp exp-width)
    (unsigned-byte-p exp-width
                     (mv-nth 2 (fp-decode x exp-width frac-width))))
 :rule-classes
 (:rewrite
  (:linear
   :corollary
   (implies (posp exp-width)
            (and (<= 0
                     (mv-nth 2 (fp-decode x exp-width frac-width)))
                 (< (mv-nth 2 (fp-decode x exp-width frac-width))
                    (expt 2 exp-width))))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))

Theorem: n01p-implicit-bit-fp-decode

(defthm n01p-implicit-bit-fp-decode
 (unsigned-byte-p 1
                  (mv-nth 3 (fp-decode x exp-width frac-width)))
 :rule-classes
 (:rewrite
  (:type-prescription
     :corollary (bitp (mv-nth 3 (fp-decode x exp-width frac-width)))
     :hints
     (("Goal"
           :in-theory
           '(unsigned-byte-p integer-range-p natp bitp (:e expt)))))
  (:linear
   :corollary
   (and (<= 0
            (mv-nth 3 (fp-decode x exp-width frac-width)))
        (< (mv-nth 3 (fp-decode x exp-width frac-width))
           2))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))

Theorem: natp-frac-from-fp-decode

(defthm natp-frac-from-fp-decode
  (implies (posp frac-width)
           (natp (mv-nth 4 (fp-decode x exp-width frac-width))))
  :rule-classes :type-prescription)

Theorem: frac-width-wide-frac-from-fp-decode-lemma

(defthm frac-width-wide-frac-from-fp-decode-lemma
 (implies
    (posp frac-width)
    (unsigned-byte-p frac-width
                     (mv-nth 4 (fp-decode x exp-width frac-width))))
 :rule-classes
 (:rewrite
  (:type-prescription
      :corollary
      (implies (posp frac-width)
               (natp (mv-nth 4 (fp-decode x exp-width frac-width))))
      :hints
      (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp))))
  (:linear
   :corollary
   (implies (posp frac-width)
            (and (<= 0
                     (mv-nth 4 (fp-decode x exp-width frac-width)))
                 (< (mv-nth 4 (fp-decode x exp-width frac-width))
                    (expt 2 frac-width))))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))