1 |
|
/* |
2 |
|
** Copyright (C) 2018 Martin Brain |
3 |
|
** |
4 |
|
** See the file LICENSE for licensing information. |
5 |
|
*/ |
6 |
|
|
7 |
|
/* |
8 |
|
** divide.h |
9 |
|
** |
10 |
|
** Martin Brain |
11 |
|
** martin.brain@cs.ox.ac.uk |
12 |
|
** 04/02/16 |
13 |
|
** |
14 |
|
** Division of arbitrary precision floats |
15 |
|
** |
16 |
|
*/ |
17 |
|
|
18 |
|
#include "symfpu/core/unpackedFloat.h" |
19 |
|
#include "symfpu/core/ite.h" |
20 |
|
#include "symfpu/core/rounder.h" |
21 |
|
#include "symfpu/core/operations.h" |
22 |
|
|
23 |
|
#ifndef SYMFPU_DIVIDE |
24 |
|
#define SYMFPU_DIVIDE |
25 |
|
|
26 |
|
namespace symfpu { |
27 |
|
|
28 |
|
template <class t> |
29 |
202 |
unpackedFloat<t> addDivideSpecialCases (const typename t::fpt &format, |
30 |
|
const unpackedFloat<t> &left, |
31 |
|
const unpackedFloat<t> &right, |
32 |
|
const typename t::prop &sign, |
33 |
|
const unpackedFloat<t> ÷Result) { |
34 |
|
typedef typename t::prop prop; |
35 |
|
|
36 |
208 |
prop eitherArgumentNaN(left.getNaN() || right.getNaN()); |
37 |
429 |
prop generateNaN((left.getInf() && right.getInf()) || |
38 |
250 |
(left.getZero() && right.getZero())); |
39 |
|
|
40 |
208 |
prop isNaN(eitherArgumentNaN || generateNaN); |
41 |
|
|
42 |
425 |
prop isInf((!left.getZero() && right.getZero()) || |
43 |
198 |
(left.getInf() && !right.getInf())); |
44 |
|
|
45 |
431 |
prop isZero((!left.getInf() && right.getInf()) || |
46 |
208 |
(left.getZero() && !right.getZero())); |
47 |
|
|
48 |
|
return ITE(isNaN, |
49 |
|
unpackedFloat<t>::makeNaN(format), |
50 |
|
ITE(isInf, |
51 |
|
unpackedFloat<t>::makeInf(format, sign), |
52 |
|
ITE(isZero, |
53 |
|
unpackedFloat<t>::makeZero(format, sign), |
54 |
208 |
divideResult))); |
55 |
|
} |
56 |
|
|
57 |
|
|
58 |
|
template <class t> |
59 |
202 |
unpackedFloat<t> arithmeticDivide (const typename t::fpt &format, |
60 |
|
const unpackedFloat<t> &left, |
61 |
|
const unpackedFloat<t> &right) { |
62 |
|
typedef typename t::bwt bwt; |
63 |
|
typedef typename t::prop prop; |
64 |
|
typedef typename t::ubv ubv; |
65 |
|
typedef typename t::sbv sbv; |
66 |
|
typedef typename t::fpt fpt; |
67 |
|
|
68 |
202 |
PRECONDITION(left.valid(format)); |
69 |
202 |
PRECONDITION(right.valid(format)); |
70 |
|
|
71 |
|
// Compute sign |
72 |
208 |
prop divideSign(left.getSign() ^ right.getSign()); |
73 |
|
|
74 |
|
// Subtract up exponents |
75 |
404 |
sbv exponentDiff(expandingSubtract<t>(left.getExponent(),right.getExponent())); |
76 |
|
// Optimisation : do this late and use the increment as a carry in |
77 |
|
|
78 |
404 |
sbv min(unpackedFloat<t>::minSubnormalExponent(format)); |
79 |
404 |
sbv max(unpackedFloat<t>::maxNormalExponent(format)); |
80 |
202 |
INVARIANT(expandingSubtract<t>(min,max) <= exponentDiff); |
81 |
202 |
INVARIANT(exponentDiff <= expandingSubtract<t>(max, min)); |
82 |
|
// Optimisation : use the if-then-lazy-else to avoid dividing for underflow and overflow |
83 |
|
// subnormal / greater-than-2^sigwidth does not need to be evaluated |
84 |
|
|
85 |
|
|
86 |
|
// Divide the significands |
87 |
|
// We need significandWidth() + 1 bits in the result but the top one may cancel, so add two bits |
88 |
404 |
ubv extendedNumerator(left.getSignificand().append(ubv::zero(2))); |
89 |
404 |
ubv extendedDenominator(right.getSignificand().append(ubv::zero(2))); |
90 |
|
|
91 |
404 |
resultWithRemainderBit<t> divided(fixedPointDivide<t>(extendedNumerator, extendedDenominator)); |
92 |
|
|
93 |
|
|
94 |
202 |
bwt resWidth(divided.result.getWidth()); |
95 |
404 |
ubv topBit(divided.result.extract(resWidth - 1, resWidth - 1)); |
96 |
404 |
ubv nextBit(divided.result.extract(resWidth - 2, resWidth - 2)); |
97 |
|
|
98 |
|
// Alignment of inputs means at least one of the two MSB is 1 |
99 |
|
// i.e. [1,2) / [1,2) = [0.5,2) |
100 |
|
// Top bit is set by the first round of the divide and thus is 50/50 1 or 0 |
101 |
208 |
prop topBitSet(topBit.isAllOnes()); |
102 |
202 |
INVARIANT(topBitSet || nextBit.isAllOnes()); |
103 |
202 |
INVARIANT(topBitSet == (left.getSignificand() >= right.getSignificand())); |
104 |
|
|
105 |
|
|
106 |
|
// Re-align |
107 |
404 |
sbv alignedExponent(conditionalDecrement<t>(!topBitSet, exponentDiff)); // Will not overflow as previously expanded |
108 |
404 |
ubv alignedSignificand(conditionalLeftShiftOne<t>(!topBitSet, divided.result)); // Will not loose information |
109 |
|
|
110 |
|
// Create the sticky bit, it is important that this is after alignment |
111 |
404 |
ubv finishedSignificand(alignedSignificand | ubv(divided.remainderBit).extend(resWidth - 1)); |
112 |
|
|
113 |
|
// Put back together |
114 |
202 |
fpt extendedFormat(format.exponentWidth() + 1, format.significandWidth() + 2); |
115 |
202 |
unpackedFloat<t> divideResult(extendedFormat, divideSign, alignedExponent, finishedSignificand); |
116 |
|
|
117 |
|
// A brief word about formats. |
118 |
|
// You might think that the extend above is unnecessary : it is from a overflow point of view. |
119 |
|
// It's needed so that it is a valid number with exponentWidth() + 2. |
120 |
|
// +1 is sufficient in almost all cases. However: |
121 |
|
// very large normal / very small subnormal |
122 |
|
// can have an exponent greater than very large normal * 2 ( + 1) |
123 |
|
// because the exponent range is asymmetric with more subnormal than normal. |
124 |
|
|
125 |
202 |
POSTCONDITION(divideResult.valid(extendedFormat)); |
126 |
|
|
127 |
404 |
return divideResult; |
128 |
|
} |
129 |
|
|
130 |
|
|
131 |
|
// Put it all together... |
132 |
|
template <class t> |
133 |
202 |
unpackedFloat<t> divide (const typename t::fpt &format, |
134 |
|
const typename t::rm &roundingMode, |
135 |
|
const unpackedFloat<t> &left, |
136 |
|
const unpackedFloat<t> &right) { |
137 |
|
//typedef typename t::bwt bwt; |
138 |
|
//typedef typename t::prop prop; |
139 |
|
//typedef typename t::ubv ubv; |
140 |
|
//typedef typename t::sbv sbv; |
141 |
|
|
142 |
202 |
PRECONDITION(left.valid(format)); |
143 |
202 |
PRECONDITION(right.valid(format)); |
144 |
|
|
145 |
404 |
unpackedFloat<t> divideResult(arithmeticDivide(format, left, right)); |
146 |
|
|
147 |
404 |
unpackedFloat<t> roundedDivideResult(rounder(format, roundingMode, divideResult)); |
148 |
|
|
149 |
202 |
unpackedFloat<t> result(addDivideSpecialCases(format, left, right, roundedDivideResult.getSign(), roundedDivideResult)); |
150 |
|
|
151 |
202 |
POSTCONDITION(result.valid(format)); |
152 |
|
|
153 |
404 |
return result; |
154 |
|
} |
155 |
|
|
156 |
|
|
157 |
|
} |
158 |
|
|
159 |
|
#endif |