Check whether the operand is SNaN or QNaN and then return corresponding result. Also handle the infinities.
Function:
(defun sse-cvt-fp1-to-fp2-special (kind sign implicit frac frac-width1 exp-width2 frac-width2) (declare (type (unsigned-byte 1) sign) (type (unsigned-byte 1) implicit)) (declare (xargs :guard (and (natp frac) (posp frac-width1) (posp exp-width2) (posp frac-width2)))) (let ((__function__ 'sse-cvt-fp1-to-fp2-special)) (declare (ignorable __function__)) (let ((invalid (eq kind 'snan))) (cond ((eq kind 'snan) (let ((exp-width exp-width2) (frac-width frac-width2) (nan-frac-bits (ash (part-select frac :low 0 :high (nfix (- frac-width1 2))) (- frac-width2 frac-width1)))) (flag-make-special-bp 'qnan nan-frac-bits sign invalid))) ((or (eq kind 'qnan) (eq kind 'indef)) (let ((exp-width exp-width2) (frac (ash frac (- frac-width2 frac-width1)))) (mv t sign (fp-max-exp exp-width) implicit frac invalid))) ((eq kind 'inf) (let ((exp-width exp-width2) (frac-width frac-width2)) (flag-make-special-bp 'inf 0 sign invalid))) (t (mv nil 0 0 0 0 invalid))))))
Theorem:
(defthm integerp-sse-cvt-fp1-to-fp2-special-1 (implies (integerp sign) (integerp (mv-nth 1 (sse-cvt-fp1-to-fp2-special kind sign implicit frac frac-width1 exp-width2 frac-width2)))) :rule-classes :type-prescription)
Theorem:
(defthm integerp-sse-cvt-fp1-to-fp2-special-2 (integerp (mv-nth 2 (sse-cvt-fp1-to-fp2-special kind sign implicit frac frac-width1 exp-width2 frac-width2))) :rule-classes :type-prescription)
Theorem:
(defthm integerp-sse-cvt-fp1-to-fp2-special-3 (implies (integerp implicit) (integerp (mv-nth 3 (sse-cvt-fp1-to-fp2-special kind sign implicit frac frac-width1 exp-width2 frac-width2)))) :rule-classes :type-prescription)
Theorem:
(defthm integerp-sse-cvt-fp1-to-fp2-special-4 (integerp (mv-nth 4 (sse-cvt-fp1-to-fp2-special kind sign implicit frac frac-width1 exp-width2 frac-width2))) :rule-classes :type-prescription)