1 |
|
/* |
2 |
|
** Copyright (C) 2018 Martin Brain |
3 |
|
** |
4 |
|
** See the file LICENSE for licensing information. |
5 |
|
*/ |
6 |
|
|
7 |
|
/* |
8 |
|
** convert.h |
9 |
|
** |
10 |
|
** Martin Brain |
11 |
|
** martin.brain@cs.ox.ac.uk |
12 |
|
** 03/02/14 |
13 |
|
** |
14 |
|
** Conversion from unpacked floats in one format to another. |
15 |
|
** |
16 |
|
*/ |
17 |
|
|
18 |
|
#include "symfpu/core/unpackedFloat.h" |
19 |
|
#include "symfpu/core/rounder.h" |
20 |
|
|
21 |
|
#ifndef SYMFPU_CONVERT |
22 |
|
#define SYMFPU_CONVERT |
23 |
|
|
24 |
|
namespace symfpu { |
25 |
|
|
26 |
|
template <class t> |
27 |
125 |
unpackedFloat<t> convertFloatToFloat (const typename t::fpt &sourceFormat, |
28 |
|
const typename t::fpt &targetFormat, |
29 |
|
const typename t::rm &roundingMode, |
30 |
|
const unpackedFloat<t> &input) { |
31 |
|
|
32 |
125 |
PRECONDITION(input.valid(sourceFormat)); |
33 |
|
|
34 |
|
typedef typename t::bwt bwt; |
35 |
|
//typedef typename t::prop prop; |
36 |
|
//typedef typename t::ubv ubv; |
37 |
|
//typedef typename t::sbv sbv; |
38 |
|
|
39 |
|
// increased includes equality |
40 |
125 |
bool exponentIncreased = unpackedFloat<t>::exponentWidth(sourceFormat) <= unpackedFloat<t>::exponentWidth(targetFormat); |
41 |
125 |
bool significandIncreased = unpackedFloat<t>::significandWidth(sourceFormat) <= unpackedFloat<t>::significandWidth(targetFormat); |
42 |
|
|
43 |
125 |
bwt expExtension = (exponentIncreased) ? unpackedFloat<t>::exponentWidth(targetFormat) - unpackedFloat<t>::exponentWidth(sourceFormat) : 0; |
44 |
125 |
bwt sigExtension = (significandIncreased) ? unpackedFloat<t>::significandWidth(targetFormat) - unpackedFloat<t>::significandWidth(sourceFormat) : 0; |
45 |
|
|
46 |
250 |
unpackedFloat<t> extended(input.extend(expExtension, sigExtension)); |
47 |
|
|
48 |
|
// Format sizes are literal so it is safe to branch on them |
49 |
125 |
if (exponentIncreased && significandIncreased) { |
50 |
|
// Fast path strict promotions |
51 |
|
|
52 |
89 |
POSTCONDITION(extended.valid(targetFormat)); |
53 |
|
|
54 |
89 |
return extended; |
55 |
|
|
56 |
|
} else { |
57 |
|
|
58 |
72 |
unpackedFloat<t> rounded(rounder(targetFormat, roundingMode, extended)); |
59 |
|
|
60 |
144 |
unpackedFloat<t> result(ITE(input.getNaN(), |
61 |
|
unpackedFloat<t>::makeNaN(targetFormat), |
62 |
36 |
ITE(input.getInf(), |
63 |
|
unpackedFloat<t>::makeInf(targetFormat, input.getSign()), |
64 |
36 |
ITE(input.getZero(), |
65 |
|
unpackedFloat<t>::makeZero(targetFormat, input.getSign()), |
66 |
|
rounded)))); |
67 |
|
|
68 |
36 |
POSTCONDITION(result.valid(targetFormat)); |
69 |
|
|
70 |
36 |
return result; |
71 |
|
} |
72 |
|
} |
73 |
|
|
74 |
|
|
75 |
|
template <class t> |
76 |
160 |
unpackedFloat<t> roundToIntegral (const typename t::fpt &format, |
77 |
|
const typename t::rm &roundingMode, |
78 |
|
const unpackedFloat<t> &input) { |
79 |
|
|
80 |
160 |
PRECONDITION(input.valid(format)); |
81 |
|
|
82 |
|
typedef typename t::bwt bwt; |
83 |
|
typedef typename t::prop prop; |
84 |
|
typedef typename t::ubv ubv; |
85 |
|
typedef typename t::sbv sbv; |
86 |
|
|
87 |
320 |
sbv exponent(input.getExponent()); |
88 |
160 |
bwt exponentWidth(exponent.getWidth()); |
89 |
|
|
90 |
320 |
sbv packedSigWidth(exponentWidth, format.packedSignificandWidth()); |
91 |
320 |
sbv unpackedSigWidth(exponentWidth, format.significandWidth()); |
92 |
|
|
93 |
|
// Fast path for things that must be integral |
94 |
180 |
prop isIntegral(exponent >= packedSigWidth); |
95 |
180 |
prop isSpecial(input.getNaN() || input.getInf() || input.getZero()); |
96 |
180 |
prop isID(isIntegral || isSpecial); |
97 |
160 |
probabilityAnnotation<t>(isID, LIKELY); |
98 |
|
// TODO : fast path the cases that don't round up |
99 |
|
|
100 |
|
|
101 |
|
// Otherwise, compute rounding location |
102 |
320 |
sbv initialRoundingPoint(expandingSubtract<t>(packedSigWidth,exponent)); // Expansion only needed in obscure formats |
103 |
640 |
sbv collaredRoundingPoint(collar<t>(initialRoundingPoint, |
104 |
320 |
sbv::zero(exponentWidth + 1), |
105 |
|
unpackedSigWidth.extend(1).increment())); |
106 |
|
|
107 |
|
// Round |
108 |
320 |
ubv significand(input.getSignificand()); |
109 |
160 |
bwt significandWidth(significand.getWidth()); |
110 |
320 |
ubv roundingPoint((significandWidth >= exponentWidth) ? |
111 |
|
collaredRoundingPoint.toUnsigned().matchWidth(significand) : |
112 |
|
collaredRoundingPoint.toUnsigned().extract(significandWidth - 1, 0)); |
113 |
|
// Extract is safe because of the collar |
114 |
|
|
115 |
320 |
significandRounderResult<t> roundedResult(variablePositionRound<t>(roundingMode, input.getSign(), significand, |
116 |
|
roundingPoint, |
117 |
|
prop(false), // TODO : Could actually be exponent >= 0 |
118 |
|
isID)); // The fast-path case so just deactives some code |
119 |
|
|
120 |
|
// Reconstruct |
121 |
|
// Note this is not in a valid form if significand is all zeros |
122 |
|
// The max is necessary to catch cases when we round up to one from very small numbers |
123 |
|
// The rounder ensures these are zero if they don't round up |
124 |
320 |
unpackedFloat<t> reconstructed(input.getSign(), |
125 |
|
max<t>(conditionalIncrement<t>(roundedResult.incrementExponent, exponent), |
126 |
|
sbv::zero(exponentWidth)), |
127 |
|
roundedResult.significand); |
128 |
|
|
129 |
|
|
130 |
440 |
unpackedFloat<t> result(ITE(isID, |
131 |
|
input, |
132 |
280 |
ITE(roundedResult.significand.isAllZeros(), |
133 |
|
unpackedFloat<t>::makeZero(format, input.getSign()), |
134 |
|
reconstructed))); |
135 |
|
|
136 |
160 |
POSTCONDITION(result.valid(format)); |
137 |
|
|
138 |
320 |
return result; |
139 |
|
|
140 |
|
|
141 |
|
#if 0 |
142 |
|
// increased includes equality |
143 |
|
bool exponentIncreased = unpackedFloat<t>::exponentWidth(sourceFormat) <= unpackedFloat<t>::exponentWidth(targetFormat); |
144 |
|
bool significandIncreased = unpackedFloat<t>::significandWidth(sourceFormat) <= unpackedFloat<t>::significandWidth(targetFormat); |
145 |
|
|
146 |
|
bwt expExtension = (exponentIncreased) ? unpackedFloat<t>::exponentWidth(targetFormat) - unpackedFloat<t>::exponentWidth(sourceFormat) : 0; |
147 |
|
bwt sigExtension = (significandIncreased) ? unpackedFloat<t>::significandWidth(targetFormat) - unpackedFloat<t>::significandWidth(sourceFormat) : 0; |
148 |
|
|
149 |
|
unpackedFloat<t> extended(input.extend(expExtension, sigExtension)); |
150 |
|
|
151 |
|
// Format sizes are literal so it is safe to branch on them |
152 |
|
if (exponentIncreased && significandIncreased) { |
153 |
|
// Fast path strict promotions |
154 |
|
|
155 |
|
POSTCONDITION(extended.valid(targetFormat)); |
156 |
|
|
157 |
|
return extended; |
158 |
|
|
159 |
|
} else { |
160 |
|
|
161 |
|
unpackedFloat<t> rounded(rounder(targetFormat, roundingMode, extended)); |
162 |
|
|
163 |
|
unpackedFloat<t> result(ITE(input.getNaN(), |
164 |
|
unpackedFloat<t>::makeNaN(targetFormat), |
165 |
|
ITE(input.getInf(), |
166 |
|
unpackedFloat<t>::makeInf(targetFormat, input.getSign()), |
167 |
|
ITE(input.getZero(), |
168 |
|
unpackedFloat<t>::makeZero(targetFormat, input.getSign()), |
169 |
|
rounded)))); |
170 |
|
|
171 |
|
POSTCONDITION(result.valid(targetFormat)); |
172 |
|
|
173 |
|
return result; |
174 |
|
} |
175 |
|
#endif |
176 |
|
|
177 |
|
} |
178 |
|
|
179 |
|
|
180 |
|
template <class t> |
181 |
68 |
unpackedFloat<t> convertUBVToFloat (const typename t::fpt &targetFormat, |
182 |
|
const typename t::rm &roundingMode, |
183 |
|
const typename t::ubv &preInput, |
184 |
|
const typename t::bwt &decimalPointPosition = 0) { |
185 |
|
|
186 |
|
typedef typename t::bwt bwt; |
187 |
|
typedef typename t::prop prop; |
188 |
|
typedef typename t::ubv ubv; |
189 |
|
typedef typename t::sbv sbv; |
190 |
|
typedef typename t::fpt fpt; |
191 |
|
|
192 |
|
// In the case of a 1 bit input(?) extend to 2 bits so that the intermediate float is a sensible format |
193 |
136 |
ubv input((preInput.getWidth() == 1) ? preInput.extend(1) : preInput); |
194 |
|
|
195 |
68 |
bwt inputWidth(input.getWidth()); |
196 |
|
|
197 |
68 |
PRECONDITION(decimalPointPosition <= inputWidth); |
198 |
|
|
199 |
|
// Devise an appropriate format |
200 |
68 |
bwt initialExponentWidth(bitsToRepresent<bwt>(inputWidth) + 1); // +1 as unsigned -> signed |
201 |
68 |
fpt initialFormat(initialExponentWidth, inputWidth); |
202 |
68 |
bwt actualExponentWidth(unpackedFloat<t>::exponentWidth(initialFormat)); |
203 |
|
|
204 |
|
// Build |
205 |
136 |
unpackedFloat<t> initial(prop(false), sbv(actualExponentWidth, (inputWidth - 1) - decimalPointPosition), input); // inputWidth - 1 as we want one bit above the decimal point |
206 |
|
|
207 |
|
// Normalise |
208 |
136 |
unpackedFloat<t> normalised(initial.normaliseUpDetectZero(initialFormat)); |
209 |
|
|
210 |
|
// Round (the conversion will catch the cases where no rounding is needed) |
211 |
136 |
return convertFloatToFloat(initialFormat, targetFormat, roundingMode, normalised); |
212 |
|
} |
213 |
|
|
214 |
|
|
215 |
|
template <class t> |
216 |
8 |
unpackedFloat<t> convertSBVToFloat (const typename t::fpt &targetFormat, |
217 |
|
const typename t::rm &roundingMode, |
218 |
|
const typename t::sbv &input, |
219 |
|
const typename t::bwt &decimalPointPosition = 0) { |
220 |
|
typedef typename t::bwt bwt; |
221 |
|
typedef typename t::prop prop; |
222 |
|
typedef typename t::sbv sbv; |
223 |
|
typedef typename t::fpt fpt; |
224 |
|
|
225 |
8 |
bwt inputWidth(input.getWidth()); |
226 |
|
|
227 |
8 |
PRECONDITION(inputWidth > 1); // A 1 bit signed-number is ??? |
228 |
8 |
PRECONDITION(decimalPointPosition <= inputWidth); |
229 |
|
|
230 |
|
// Devise an appropriate format |
231 |
8 |
bwt initialExponentWidth(bitsToRepresent<bwt>(inputWidth) + 1); // +1 as unsigned -> signed |
232 |
8 |
fpt initialFormat(initialExponentWidth, inputWidth + 1); // +1 as signed -> unsigned |
233 |
8 |
bwt actualExponentWidth(unpackedFloat<t>::exponentWidth(initialFormat)); |
234 |
|
|
235 |
|
// Work out the sign |
236 |
8 |
prop negative(input < sbv::zero(inputWidth)); |
237 |
|
|
238 |
|
// Build |
239 |
16 |
unpackedFloat<t> initial(negative, sbv(actualExponentWidth, inputWidth - decimalPointPosition), (abs<t,sbv>(input.extend(1))).toUnsigned()); |
240 |
|
|
241 |
|
// Normalise |
242 |
16 |
unpackedFloat<t> normalised(initial.normaliseUpDetectZero(initialFormat)); |
243 |
|
|
244 |
|
// Round (the conversion will catch the cases where no rounding is needed) |
245 |
16 |
return convertFloatToFloat(initialFormat, targetFormat, roundingMode, normalised); |
246 |
|
} |
247 |
|
|
248 |
|
|
249 |
|
// Common conversion code for both convert to sgined and to unsigned. |
250 |
|
// Note that the results will be junk if it is not in bounds, etc. |
251 |
|
// convertFloatToUBV and convertFloatToSBV handle all of that logic. |
252 |
|
template <class t> |
253 |
|
significandRounderResult<t> convertFloatToBV (const typename t::fpt &format, |
254 |
|
const typename t::rm &roundingMode, |
255 |
|
const unpackedFloat<t> &input, |
256 |
|
const typename t::bwt &targetWidth, |
257 |
|
const typename t::bwt &decimalPointPosition) { |
258 |
|
|
259 |
|
typedef typename t::bwt bwt; |
260 |
|
typedef typename t::prop prop; |
261 |
|
typedef typename t::ubv ubv; |
262 |
|
typedef typename t::sbv sbv; |
263 |
|
|
264 |
|
|
265 |
|
PRECONDITION(decimalPointPosition < targetWidth); |
266 |
|
|
267 |
|
|
268 |
|
// TODO : fast path the RTZ / don't need to round case |
269 |
|
|
270 |
|
bwt maxShift(targetWidth + 1); // + 1 as we have to shift over the guard bit |
271 |
|
bwt maxShiftBits(bitsToRepresent(maxShift) + 1); // +1 as we want it to be signed |
272 |
|
|
273 |
|
bwt exponentWidth(input.getExponent().getWidth()); |
274 |
|
bwt workingExponentWidth((exponentWidth >= maxShiftBits) ? |
275 |
|
exponentWidth : maxShiftBits); |
276 |
|
|
277 |
|
sbv maxShiftAmount(workingExponentWidth, maxShift); |
278 |
|
sbv exponent(input.getExponent().matchWidth(maxShiftAmount)); |
279 |
|
|
280 |
|
|
281 |
|
// Optimisation : compact the significand in the case targetWidth < significantWidth |
282 |
|
ubv inputSignificand(input.getSignificand()); |
283 |
|
bwt inputSignificandWidth(inputSignificand.getWidth()); |
284 |
|
ubv *working = NULL; |
285 |
|
if (targetWidth + 2 < inputSignificandWidth) { |
286 |
|
|
287 |
|
ubv dataAndGuard(inputSignificand.extract(inputSignificandWidth - 1, (inputSignificandWidth - targetWidth) - 1)); |
288 |
|
prop sticky(!inputSignificand.extract((inputSignificandWidth - targetWidth) - 2, 0).isAllZeros()); |
289 |
|
|
290 |
|
working = new ubv(dataAndGuard.append(ubv(sticky))); |
291 |
|
} else { |
292 |
|
working = new ubv(inputSignificand); |
293 |
|
} |
294 |
|
ubv significand(*working); |
295 |
|
delete working; |
296 |
|
bwt significandWidth(significand.getWidth()); |
297 |
|
|
298 |
|
// Handle zero |
299 |
|
ubv zerodSignificand(significand & |
300 |
|
ITE(input.getZero(), ubv::zero(significandWidth), ubv::allOnes(significandWidth))); |
301 |
|
ubv expandedSignificand(zerodSignificand.extend(maxShift)); // Start with the significand in the sticky position. |
302 |
|
// targetWidth +1 is for the guard bit |
303 |
|
|
304 |
|
// Align |
305 |
|
sbv shiftAmount(collar<t>(expandingAdd<t>(exponent, |
306 |
|
sbv(workingExponentWidth, decimalPointPosition + 2)), // +1 to guard, +1 to LSB |
307 |
|
sbv::zero(workingExponentWidth + 1), |
308 |
|
maxShiftAmount.extend(1))); |
309 |
|
ubv convertedShiftAmount(shiftAmount.resize(bitsToRepresent(maxShift) + 1 /* +1 for sign bit, safe due to collar */ |
310 |
|
).toUnsigned().matchWidth(expandedSignificand)); |
311 |
|
ubv aligned(expandedSignificand << convertedShiftAmount); // Safe by collar |
312 |
|
|
313 |
|
|
314 |
|
// Fixed position round |
315 |
|
significandRounderResult<t> rounded(fixedPositionRound<t>(roundingMode, input.getSign(), |
316 |
|
aligned, targetWidth, |
317 |
|
prop(false), prop(false))); |
318 |
|
|
319 |
|
return rounded; |
320 |
|
} |
321 |
|
|
322 |
|
// A more compact version for round to zero |
323 |
|
// Only handles normal, subnormal and zero cases, overflow of targetWidth will give junk. |
324 |
|
// Inf, NaN, and overflow must be handled by the caller. |
325 |
|
template <class t> |
326 |
|
significandRounderResult<t> convertFloatToBVRTZ (const typename t::fpt &format, |
327 |
|
const unpackedFloat<t> &input, |
328 |
|
const typename t::bwt &targetWidth, |
329 |
|
const typename t::bwt &decimalPointPosition) { |
330 |
|
typedef typename t::bwt bwt; |
331 |
|
typedef typename t::prop prop; |
332 |
|
typedef typename t::ubv ubv; |
333 |
|
typedef typename t::sbv sbv; |
334 |
|
|
335 |
|
PRECONDITION(targetWidth > 0); |
336 |
|
PRECONDITION(decimalPointPosition < targetWidth); |
337 |
|
|
338 |
|
// A working significand of the right length |
339 |
|
ubv significand(input.getSignificand()); |
340 |
|
bwt significandWidth(significand.getWidth()); |
341 |
|
|
342 |
|
ubv significantSignificand(significand.extract(significandWidth - 1, |
343 |
|
((targetWidth < significandWidth) ? significandWidth - targetWidth : 0))); |
344 |
|
bwt ssWidth(significantSignificand.getWidth()); |
345 |
|
|
346 |
|
|
347 |
|
// Handle zero and fractional cases |
348 |
|
sbv exponent(input.getExponent()); |
349 |
|
bwt exponentWidth(exponent.getWidth()); |
350 |
|
|
351 |
|
prop fraction(input.getExponent() < sbv::zero(exponentWidth)); |
352 |
|
ubv zerodSignificand(significantSignificand & |
353 |
|
ITE(input.getZero() || fraction, ubv::zero(ssWidth), ubv::allOnes(ssWidth))); |
354 |
|
|
355 |
|
ubv expandedSignificand(zerodSignificand.extend(targetWidth - 1)); // Start with the significand in the LSB of output |
356 |
|
|
357 |
|
|
358 |
|
// Prepare exponent |
359 |
|
bwt maxShift(targetWidth - 1); // - 1 as we are already at LSB |
360 |
|
bwt maxShiftBits(bitsToRepresent(maxShift)); // Don't care about it being signed |
361 |
|
|
362 |
|
ubv convertedExponent(exponent.toUnsigned()); |
363 |
|
bwt topExtractedBit(((maxShiftBits > (exponentWidth - 1)) ? exponentWidth : maxShiftBits) - 1); |
364 |
|
|
365 |
|
ubv shiftBits(convertedExponent.extract(topExtractedBit, 0)); |
366 |
|
ubv shiftOperand(shiftBits.matchWidth(expandedSignificand)); |
367 |
|
|
368 |
|
// Align |
369 |
|
ubv shifted(expandedSignificand.modularLeftShift(shiftOperand)); |
370 |
|
bwt shiftedWidth(shifted.getWidth()); |
371 |
|
|
372 |
|
// Extract |
373 |
|
ubv result(shifted.extract(shiftedWidth - 1, shiftedWidth - targetWidth)); |
374 |
|
|
375 |
|
return significandRounderResult<t>(result, prop(false)); |
376 |
|
} |
377 |
|
|
378 |
|
|
379 |
|
|
380 |
|
// Decimal point position in the bit in the output on the left hand side of the decimal point |
381 |
|
// I.E. if it is positive then it is converting to a fix-point number |
382 |
|
template <class t> |
383 |
|
typename t::ubv convertFloatToUBV (const typename t::fpt &format, |
384 |
|
const typename t::rm &roundingMode, |
385 |
|
const unpackedFloat<t> &input, |
386 |
|
const typename t::bwt &targetWidth, |
387 |
|
const typename t::ubv &undefValue, |
388 |
|
const typename t::bwt &decimalPointPosition = 0) { |
389 |
|
|
390 |
|
typedef typename t::bwt bwt; |
391 |
|
typedef typename t::prop prop; |
392 |
|
typedef typename t::ubv ubv; |
393 |
|
typedef typename t::sbv sbv; |
394 |
|
|
395 |
|
|
396 |
|
PRECONDITION(decimalPointPosition < targetWidth); |
397 |
|
|
398 |
|
|
399 |
|
// Invalid cases |
400 |
|
prop specialValue(input.getInf() || input.getNaN()); |
401 |
|
|
402 |
|
bwt maxExponentValue(targetWidth); |
403 |
|
bwt maxExponentBits(bitsToRepresent(maxExponentValue) + 1); |
404 |
|
|
405 |
|
bwt exponentWidth(input.getExponent().getWidth()); |
406 |
|
bwt workingExponentWidth((exponentWidth >= maxExponentBits) ? |
407 |
|
exponentWidth : maxExponentBits); |
408 |
|
|
409 |
|
sbv maxExponent(workingExponentWidth, maxExponentValue); |
410 |
|
sbv exponent(input.getExponent().matchWidth(maxExponent)); |
411 |
|
|
412 |
|
prop tooLarge(exponent >= maxExponent); |
413 |
|
|
414 |
|
prop tooNegative(input.getSign() && |
415 |
|
!input.getZero() && // Zero is handled elsewhere |
416 |
|
sbv::zero(workingExponentWidth) <= exponent); // Can't round to 0 |
417 |
|
|
418 |
|
prop earlyUndefinedResult(specialValue || tooLarge || tooNegative); |
419 |
|
probabilityAnnotation<t>(earlyUndefinedResult, LIKELY); // Convertable values are rare |
420 |
|
|
421 |
|
|
422 |
|
// Fixed position round |
423 |
|
significandRounderResult<t> rounded(convertFloatToBV(format, roundingMode, input, |
424 |
|
targetWidth, decimalPointPosition)); |
425 |
|
|
426 |
|
// TODO : fast path negative by converting exp==0 into guard and exp < 0 into sticky |
427 |
|
|
428 |
|
// Put the result together |
429 |
|
prop undefinedResult(earlyUndefinedResult || |
430 |
|
rounded.incrementExponent || // Overflow |
431 |
|
(input.getSign() && !rounded.significand.isAllZeros())); // Negative case |
432 |
|
|
433 |
|
ubv result(ITE(undefinedResult, |
434 |
|
undefValue, |
435 |
|
rounded.significand)); |
436 |
|
|
437 |
|
return result; |
438 |
|
} |
439 |
|
|
440 |
|
// Decimal point position in the bit in the output on the left hand side of the decimal point |
441 |
|
// I.E. if it is positive then it is converting to a fix-point number |
442 |
|
template <class t> |
443 |
|
typename t::sbv convertFloatToSBV (const typename t::fpt &format, |
444 |
|
const typename t::rm &roundingMode, |
445 |
|
const unpackedFloat<t> &input, |
446 |
|
const typename t::bwt &targetWidth, |
447 |
|
const typename t::sbv &undefValue, |
448 |
|
const typename t::bwt &decimalPointPosition = 0) { |
449 |
|
|
450 |
|
typedef typename t::bwt bwt; |
451 |
|
typedef typename t::prop prop; |
452 |
|
//typedef typename t::ubv ubv; |
453 |
|
typedef typename t::sbv sbv; |
454 |
|
|
455 |
|
|
456 |
|
PRECONDITION(decimalPointPosition < targetWidth); |
457 |
|
|
458 |
|
|
459 |
|
// Invalid cases |
460 |
|
prop specialValue(input.getInf() || input.getNaN()); |
461 |
|
|
462 |
|
bwt maxExponentValue(targetWidth); |
463 |
|
bwt maxExponentBits(bitsToRepresent(maxExponentValue) + 1); |
464 |
|
|
465 |
|
bwt exponentWidth(input.getExponent().getWidth()); |
466 |
|
bwt workingExponentWidth((exponentWidth >= maxExponentBits) ? |
467 |
|
exponentWidth : maxExponentBits); |
468 |
|
|
469 |
|
sbv maxExponent(workingExponentWidth, maxExponentValue); |
470 |
|
sbv exponent(input.getExponent().matchWidth(maxExponent)); |
471 |
|
|
472 |
|
prop tooLarge(exponent >= maxExponent); |
473 |
|
|
474 |
|
prop earlyUndefinedResult(specialValue || tooLarge); |
475 |
|
probabilityAnnotation<t>(earlyUndefinedResult, LIKELY); // Convertable values are rare |
476 |
|
|
477 |
|
|
478 |
|
// Fixed position round |
479 |
|
// (It is tempting to think that this could be done with targetWidth - 1 bits but that |
480 |
|
// missed the case of things like -128.05 -> int8_t) |
481 |
|
significandRounderResult<t> rounded(convertFloatToBV(format, roundingMode, input, |
482 |
|
targetWidth, decimalPointPosition)); |
483 |
|
|
484 |
|
// Put the result together |
485 |
|
bwt roundSigWidth(rounded.significand.getWidth()); |
486 |
|
prop undefinedResult(earlyUndefinedResult || |
487 |
|
rounded.incrementExponent || // Definite Overflow |
488 |
|
(rounded.significand.extract(roundSigWidth - 1, |
489 |
|
roundSigWidth - 1).isAllOnes() && |
490 |
|
!(input.getSign() && rounded.significand.extract(roundSigWidth - 2, 0).isAllZeros()))); // -2^{n-1} is the only safe "overflow" case |
491 |
|
|
492 |
|
|
493 |
|
sbv result(ITE(undefinedResult, |
494 |
|
undefValue, |
495 |
|
conditionalNegate<t,sbv,prop>(input.getSign(), rounded.significand.toSigned()))); |
496 |
|
|
497 |
|
return result; |
498 |
|
} |
499 |
|
|
500 |
|
} |
501 |
|
|
502 |
|
#endif |