GCC Code Coverage Report
Directory: . Exec Total Coverage
File: deps/install/include/symfpu/core/rounder.h Lines: 133 147 90.5 %
Date: 2021-03-23 Branches: 377 711 53.0 %

Line Exec Source
1
/*
2
** Copyright (C) 2018 Martin Brain
3
**
4
** See the file LICENSE for licensing information.
5
*/
6
7
/*
8
** rounder.h
9
**
10
** Martin Brain
11
** martin.brain@cs.ox.ac.uk
12
** 26/08/14
13
**
14
** Rounding arbitrary length unpacked floats back to their correct length.
15
**
16
*/
17
18
/*
19
 * Rounder Ideas
20
 *
21
 *  - get the rounder to handle things with 1 or 2 possible leading
22
 *    0's rather than normalise before and after rounding.
23
 *    Subnormal rounding should ideally be temporarily denormalised to
24
 *    avoid the expensive variable position rounding.
25
 *
26
 *  1. Take exponent and add a 0 at the start to deal with overflow.
27
 *     (may not be needed if the exponent has already been extended due
28
 *      to subnormals, addition, etc.)
29
 *  2. For each of the possible positions of the binary point, produce
30
 *     an incremented version and round and sticky bits.
31
 *     (given the alignment is known, may be able to just pick how much
32
 *      to increment by and then increment once.)
33
 *  3. The leading zeros of the original exponent pick which set of
34
 *     round and sticky to use.  Thus pick which of the incremented /
35
 *     normal to use and align apart from 1.
36
 *  4. Finally align, most of the information needed for this will be
37
 *     already known.
38
 *  (Catch -- this can introduce diamonds)
39
 *
40
 * - can fold the increment from the rounder into the circuitry /
41
 *   last round of accumulation.
42
 *   In fact, can take this further.  a + b + 1 takes the same
43
 *   circuitry as a + b.  a * b + 1 shares most of the circuit with
44
 *   a * b and neither of them require a sign extension.  Extending
45
 *   this to a + b + k and a * b + k for positional rounding is an
46
 *   open question.
47
 *
48
 * - add a 'non-deterministic rounding' mode for underapproximation.
49
 *
50
 * - add 'round-to-odd' and 'round-away-from-zero' mode
51
 *
52
 * - add 'flush subnormals to zero' option
53
 *
54
 * - Rather than increment and re-align, take all but the top bit of the
55
 *   significand, concatinate on to the exponent and then increment.
56
 *   This is effectively using the ordering trick for packed rounding.
57
 *
58
 * - The sticky bit should be a flag rather than concatinated on to the
59
 *   number to make arithmetic reasoning easier.
60
 *   (Conversely ... having it as bits is better for semi-normalised things)
61
 *
62
 * - Specialised rounders
63
 *    Additive
64
 *     Only one overflow increment is possible, even for a + b + 1
65
 *     When a subnormal number if generated, it is exact and thus you
66
 *      don't need to think about positional rounding for the
67
 *      subnormals.
68
 *     No need to check for underflow to zero for similar reasons.
69
 *     The rounder for the near path can be even more specialised as
70
 *      the sticky bit is always 0 and it can't overflow.
71
 *     Can only overflow if it is an effective add.
72
 *
73
 *    Multiplicative
74
 *     May be able to increment without overflow.
75
 *      It only seems to be possible for subnormals.
76
 *     Don't need to extend the exponent to increment when normalising.
77
 *     Can use injection bits during the multiplication reduction tree,
78
 *      the problem with the carry up can be fixed afterwards with an
79
 *      increment (add for subnormal) or by spotting the carry up during
80
 *      the reduction.
81
 *
82
 *    FMA
83
 *     More like multiply.
84
 */
85
86
87
#include "symfpu/core/operations.h"
88
#include "symfpu/core/unpackedFloat.h"
89
90
#ifndef SYMFPU_ROUNDER
91
#define SYMFPU_ROUNDER
92
93
namespace symfpu {
94
95
  // The final reconstruction of the rounded result
96
  // Handles the overflow and underflow conditions
97
  template <class t>
98
1139
  unpackedFloat<t> rounderSpecialCases (const typename t::fpt &format,
99
					const typename t::rm &roundingMode,
100
					const unpackedFloat<t> &roundedResult,
101
					const typename t::prop &overflow,
102
					const typename t::prop &underflow,
103
					const typename t::prop &isZero)
104
  {
105
    typedef typename t::prop prop;
106
    typedef typename t::ubv ubv;
107
108
    /*** Underflow and overflow ***/
109
110
    // On overflow either return inf or max
111
2691
    prop returnInf(roundingMode == t::RNE() ||
112
680
		   roundingMode == t::RNA() ||
113
2669
		   (roundingMode == t::RTP() && !roundedResult.getSign()) ||
114
439
		   (roundingMode == t::RTN() &&  roundedResult.getSign()));
115
1139
    probabilityAnnotation<t>(returnInf, LIKELY);  // Inf is more likely than max in most application scenarios
116
117
    // On underflow either return 0 or minimum subnormal
118
2691
    prop returnZero(roundingMode == t::RNE() ||
119
680
		    roundingMode == t::RNA() ||
120
495
		    roundingMode == t::RTZ() ||
121
2547
		    (roundingMode == t::RTP() &&  roundedResult.getSign()) ||
122
332
		    (roundingMode == t::RTN() && !roundedResult.getSign()));
123
1139
    probabilityAnnotation<t>(returnZero, LIKELY);   // 0 is more likely than min in most application scenarios
124
125
126
127
    /*** Reconstruct ***/
128
2278
    unpackedFloat<t> inf(unpackedFloat<t>::makeInf(format, roundedResult.getSign()));
129
2278
    unpackedFloat<t> max(roundedResult.getSign(), unpackedFloat<t>::maxNormalExponent(format), ubv::allOnes(unpackedFloat<t>::significandWidth(format)));
130
2278
    unpackedFloat<t> min(roundedResult.getSign(), unpackedFloat<t>::minSubnormalExponent(format), unpackedFloat<t>::leadingOne(unpackedFloat<t>::significandWidth(format)));
131
2278
    unpackedFloat<t> zero(unpackedFloat<t>::makeZero(format, roundedResult.getSign()));
132
133
1139
    unpackedFloat<t> result(ITE(isZero,
134
				zero,
135
				ITE(underflow,
136
				    ITE(returnZero, zero, min),
137
				    ITE(overflow,
138
					ITE(returnInf, inf, max),
139
					roundedResult))));
140
2278
    return result;
141
  }
142
143
144
  // Decide whether to round up or not
145
  template <class t>
146
1404
    typename t::prop roundingDecision (const typename t::rm &roundingMode,
147
				     const typename t::prop &sign,
148
				     const typename t::prop &significandEven,
149
				     const typename t::prop &guardBit,
150
				     const typename t::prop &stickyBit,
151
				     const typename t::prop &knownRoundDown) {
152
    typedef typename t::prop prop;
153
154
1475
    prop roundUpRNE(roundingMode == t::RNE() && guardBit && (stickyBit || !significandEven));
155
1475
    prop roundUpRNA(roundingMode == t::RNA() && guardBit);
156
1475
    prop roundUpRTP(roundingMode == t::RTP() && !sign && (guardBit || stickyBit));
157
1475
    prop roundUpRTN(roundingMode == t::RTN() &&  sign && (guardBit || stickyBit));
158
1475
    prop roundUpRTZ(roundingMode == t::RTZ() && prop(false));
159
1541
    prop roundUp(!knownRoundDown &&
160
866
		 (roundUpRNE || roundUpRNA || roundUpRTP || roundUpRTN || roundUpRTZ));
161
162
1475
    return roundUp;
163
  }
164
165
166
167
  template <class t>
168
160
  struct significandRounderResult{
169
    typename t::ubv significand;
170
    typename t::prop incrementExponent;
171
172
160
    significandRounderResult(const typename t::ubv &sig, const typename t::prop &inc) :
173
160
      significand(sig), incrementExponent(inc) {}
174
175
    significandRounderResult(const significandRounderResult &old) :
176
      significand(old.significand), incrementExponent(old.incrementExponent) {}
177
  };
178
179
  // Handles rounding the significand to a fixed width
180
  // If knownRoundDown is true should simplify to just extract
181
  // Not quite the same as either rounder so can't quite be refactored
182
  template <class t>
183
  significandRounderResult<t> fixedPositionRound(const typename t::rm &roundingMode,
184
						 const typename t::prop &sign,
185
						 const typename t::ubv &significand,
186
						 const typename t::bwt &targetWidth,
187
						 const typename t::prop &knownLeadingOne,
188
						 const typename t::prop &knownRoundDown) {
189
    typedef typename t::bwt bwt;
190
    typedef typename t::prop prop;
191
    typedef typename t::ubv ubv;
192
193
    bwt sigWidth(significand.getWidth());
194
    PRECONDITION(sigWidth >= targetWidth + 2);
195
    // Extract
196
    ubv extractedSignificand(significand.extract(sigWidth - 1, sigWidth - targetWidth).extend(1)); // extended to catch the overflow
197
198
    prop significandEven(extractedSignificand.extract(0,0).isAllZeros());
199
200
201
    // Normal guard and sticky bits
202
    bwt guardBitPosition(sigWidth - (targetWidth + 1));
203
    prop guardBit(significand.extract(guardBitPosition, guardBitPosition).isAllOnes());
204
205
    prop stickyBit(!significand.extract(guardBitPosition - 1,0).isAllZeros());
206
207
    // Rounding decision
208
    prop roundUp(roundingDecision<t>(roundingMode, sign, significandEven,
209
				     guardBit, stickyBit, knownRoundDown));
210
211
    // Conditional increment
212
    ubv roundedSignificand(conditionalIncrement<t>(roundUp, extractedSignificand));
213
214
    ubv overflowBit(roundedSignificand.extract(targetWidth, targetWidth) & ubv(roundUp));
215
    ubv carryUpMask((overflowBit | ubv(knownLeadingOne)).append(ubv::zero(targetWidth - 1)));   // Cheaper than conditional shift
216
217
    // Build result
218
    significandRounderResult<t> result(roundedSignificand.extract(targetWidth-1,0) | carryUpMask,
219
				    overflowBit.isAllOnes());
220
221
    return result;
222
  }
223
224
225
  // Handles rounding the significand to a fixed width
226
  // If knownRoundDown is true should simplify to just mask
227
  // Not quite the same as either rounder so can't quite be refactored
228
  template <class t>
229
160
  significandRounderResult<t> variablePositionRound(const typename t::rm &roundingMode,
230
						    const typename t::prop &sign,
231
						    const typename t::ubv &significand,
232
						    const typename t::ubv &roundPosition,
233
						    const typename t::prop &knownLeadingOne,
234
						    const typename t::prop &knownRoundDown) {
235
    typedef typename t::bwt bwt;
236
    typedef typename t::prop prop;
237
    typedef typename t::ubv ubv;
238
239
160
    bwt sigWidth(significand.getWidth());
240
241
    // Set up significand
242
    // Round-up-from-sticky bit and overflow bit at MSB, (fall-back) guard and sticky bits at LSB
243
320
    ubv expandedSignificand(significand.extend(2).append(ubv::zero(2)));
244
160
    bwt exsigWidth(expandedSignificand.getWidth());
245
246
247
    // Identify the increment, guard and sticky bits
248
320
    ubv incrementLocation(ubv(exsigWidth, (0x1U << 2U)) << roundPosition.matchWidth(expandedSignificand));
249
320
    ubv guardLocation(incrementLocation >> ubv::one(exsigWidth));
250
320
    ubv stickyLocations(guardLocation.decrement());
251
252
180
    prop significandEven((incrementLocation & expandedSignificand).isAllZeros());
253
180
    prop guardBit(!(guardLocation & expandedSignificand).isAllZeros());
254
180
    prop stickyBit(!(stickyLocations & expandedSignificand).isAllZeros());
255
256
    // Rounding decision
257
180
    prop roundUp(roundingDecision<t>(roundingMode, sign, significandEven,
258
				     guardBit, stickyBit, knownRoundDown));
259
260
    // Conditional increment
261
320
    ubv roundedSignificand(expandedSignificand + ITE(roundUp,
262
						     incrementLocation,
263
						     ubv::zero(exsigWidth)));
264
265
    // Mask out rounded bits and extract
266
320
    ubv maskedRoundedSignificand(roundedSignificand & (~(stickyLocations << ubv::one(exsigWidth)))); // LSB is wrong but gets cut
267
268
320
    ubv roundUpFromSticky(roundedSignificand.extract(exsigWidth - 1, exsigWidth - 1));  // Only true when rounding up and whole significand is sticky
269
320
    ubv overflowBit(roundedSignificand.extract(exsigWidth - 2, exsigWidth - 2));
270
320
    ubv maskTrigger((roundUpFromSticky | overflowBit) & ubv(roundUp));
271
320
    ubv carryUpMask((maskTrigger | ubv(knownLeadingOne)).append(ubv::zero(sigWidth - 1)));   // Cheaper than conditional shift
272
273
    // Build result
274
160
    significandRounderResult<t> result(maskedRoundedSignificand.extract(sigWidth + 1, 2) | carryUpMask,
275
				       maskTrigger.isAllOnes());
276
277
320
    return result;
278
  }
279
280
281
282
  // Allows various of the key branches in the rounder to be fixed / removed
283
  // using information that is known from the operation in which the rounder
284
  // is used. Setting these to false gives the usual rounder.
285
  template <class t>
286
93
  struct customRounderInfo {
287
    typedef typename t::prop prop;
288
289
    prop noOverflow;
290
    prop noUnderflow;
291
    prop exact;                 // Significand does not need to be changed
292
    prop subnormalExact;        // If the value is subnormal then it is exact
293
    prop noSignificandOverflow; // Incrementing the significand will not cause overflow
294
    //prop stickyIsZero;        // Can be fixed in the number directly
295
296
1139
    customRounderInfo (const prop &noO, const prop &noU,
297
		       const prop &e, const prop &sE,
298
		       const prop &nSO) :
299
      noOverflow(noO), noUnderflow(noU), exact(e),
300
1139
      subnormalExact(sE), noSignificandOverflow(nSO) {}
301
  };
302
303
template <class t>
304
1139
  unpackedFloat<t> customRounder (const typename t::fpt &format,
305
				  const typename t::rm &roundingMode,
306
				  const unpackedFloat<t> &uf,
307
				  const customRounderInfo<t> &known) {
308
309
  typedef typename t::bwt bwt;
310
  typedef typename t::prop prop;
311
  typedef typename t::ubv ubv;
312
  typedef typename t::sbv sbv;
313
314
  //PRECONDITION(uf.valid(format));
315
  // Not a precondition because
316
  //  1. Exponent and significand may be extended.
317
  //  2. Their values may also be outside of the correct range.
318
  //
319
  // However some thing do hold:
320
  //  1. Leading bit of the significant is 1   (if you want to get a meaningful answer)
321
  //     (if not, a cancellation on the near path of add can cause
322
  //      this, but the result will not be used, so it can be incorrect)
323
2278
  ubv psig(uf.getSignificand());
324
1139
  bwt sigWidth(psig.getWidth());
325
  //PRECONDITION(psig.extract(sigWidth-1, sigWidth-1).isAllOnes());
326
2278
  ubv sig(psig | unpackedFloat<t>::leadingOne(sigWidth));
327
328
  //  2. Must have round and sticky bits
329
1139
  bwt targetSignificandWidth(unpackedFloat<t>::significandWidth(format));
330
1139
  PRECONDITION(sigWidth >= targetSignificandWidth + 2);
331
332
  //  3. Must have at least enough exponent bits
333
2278
  sbv exp(uf.getExponent());
334
1139
  bwt expWidth(exp.getWidth());
335
1139
  bwt targetExponentWidth(unpackedFloat<t>::exponentWidth(format));
336
1139
  PRECONDITION(expWidth >= targetExponentWidth);
337
338
  // Also, do not round special values.
339
  // Note that this relies on these having default values and
340
  // the code that calls the rounder constructing uf from parts.
341
  //PRECONDITION(!uf.getNaN());
342
  //PRECONDITION(!uf.getInf());
343
  //PRECONDITION(!uf.getZero());
344
  // The safe choice of default values means this should work OK
345
346
347
348
  /*** Early underflow and overflow detection ***/
349
1139
  bwt exponentExtension(expWidth - targetExponentWidth);
350
1180
  prop earlyOverflow(exp > unpackedFloat<t>::maxNormalExponent(format).extend(exponentExtension));
351
1180
  prop earlyUnderflow(exp < unpackedFloat<t>::minSubnormalExponent(format).extend(exponentExtension).decrement());
352
  // Optimisation : if the precondition on sigWidth and targetSignificandWidth is removed
353
  //                then can change to:
354
  //                   exponent >= minSubnormalExponent - 1
355
  //                && sigWidth > targetSignificandBits
356
1139
  probabilityAnnotation<t>(earlyOverflow, UNLIKELY);  // (over,under)flows are generally rare events
357
1139
  probabilityAnnotation<t>(earlyUnderflow, UNLIKELY);
358
359
1180
  prop potentialLateOverflow(exp == unpackedFloat<t>::maxNormalExponent(format).extend(exponentExtension));
360
1180
  prop potentialLateUnderflow(exp == unpackedFloat<t>::minSubnormalExponent(format).extend(exponentExtension).decrement());
361
1139
  probabilityAnnotation<t>(potentialLateOverflow, VERYUNLIKELY);
362
1139
  probabilityAnnotation<t>(potentialLateUnderflow, VERYUNLIKELY);
363
364
365
366
  /*** Normal or subnormal rounding? ***/
367
1180
  prop normalRoundingRange(exp >= unpackedFloat<t>::minNormalExponent(format).extend(exponentExtension));
368
1139
  probabilityAnnotation<t>(normalRoundingRange, LIKELY);
369
1180
  prop normalRounding(normalRoundingRange || known.subnormalExact);
370
371
372
373
  /*** Round to correct significand. ***/
374
2278
  ubv extractedSignificand(sig.extract(sigWidth - 1, sigWidth - targetSignificandWidth).extend(1)); // extended to catch the overflow
375
376
  // Normal guard and sticky bits
377
1139
  bwt guardBitPosition(sigWidth - (targetSignificandWidth + 1));
378
1180
  prop guardBit(sig.extract(guardBitPosition, guardBitPosition).isAllOnes());
379
380
1180
  prop stickyBit(!sig.extract(guardBitPosition - 1,0).isAllZeros());
381
382
383
  // For subnormals, locating the guard and stick bits is a bit more involved
384
  //sbv subnormalAmount(uf.getSubnormalAmount(format)); // Catch is, uf isn't in the given format, so this doesn't work
385
2278
  sbv subnormalAmount(expandingSubtract<t>(unpackedFloat<t>::minNormalExponent(format).matchWidth(exp),exp));
386
1139
  INVARIANT((subnormalAmount < sbv(expWidth + 1, sigWidth - 1)) || earlyUnderflow);
387
  // Note that this is negative if normal, giving a full subnormal mask
388
  // but the result will be ignored (see the next invariant)
389
390
2278
  ubv subnormalShiftPrepared(subnormalAmount.toUnsigned().matchWidth(extractedSignificand));
391
392
  // Compute masks
393
2278
  ubv subnormalMask(orderEncode<t>(subnormalShiftPrepared)); // Invariant implies this if all ones, it will not be used
394
2278
  ubv subnormalStickyMask(subnormalMask >> ubv::one(targetSignificandWidth + 1)); // +1 as the exponent is extended
395
396
  // Apply
397
2278
  ubv subnormalMaskedSignificand(extractedSignificand & (~subnormalMask));
398
2278
  ubv subnormalMaskRemoved(extractedSignificand & subnormalMask);
399
  // Optimisation : remove the masking with a single orderEncodeBitwise style construct
400
401
1180
  prop subnormalGuardBit(!(subnormalMaskRemoved & (~subnormalStickyMask)).isAllZeros());
402
3058
  prop subnormalStickyBit(guardBit || stickyBit ||
403
2976
			  !((subnormalMaskRemoved & subnormalStickyMask).isAllZeros()));
404
405
406
2278
  ubv subnormalIncrementAmount((subnormalMask.modularLeftShift(ubv::one(targetSignificandWidth + 1))) & ~subnormalMask); // The only case when this looses info is earlyUnderflow
407
1139
  INVARIANT(IMPLIES(subnormalIncrementAmount.isAllZeros(), earlyUnderflow || normalRounding));
408
409
410
  // Have to choose the right one dependent on rounding mode
411
1180
  prop choosenGuardBit(ITE(normalRounding, guardBit, subnormalGuardBit));
412
1180
  prop choosenStickyBit(ITE(normalRounding, stickyBit, subnormalStickyBit));
413
414
1180
  prop significandEven(ITE(normalRounding,
415
			   extractedSignificand.extract(0,0).isAllZeros(),
416
			   ((extractedSignificand & subnormalIncrementAmount).isAllZeros())));
417
1180
  prop roundUp(roundingDecision<t>(roundingMode, uf.getSign(), significandEven,
418
				   choosenGuardBit, choosenStickyBit,
419
2196
				   known.exact || (known.subnormalExact && !normalRoundingRange)));
420
421
422
  // Perform the increment as needed
423
2278
  ubv leadingOne(unpackedFloat<t>::leadingOne(targetSignificandWidth));
424
  // Not actually true, consider minSubnormalExponent - 1 : not an early underfow and empty significand
425
  //INVARIANT(!(subnormalMaskedSignificand & leadingOne).isAllZeros() ||
426
  //          earlyUnderflow); // This one really matters, it means only the early underflow path is wrong
427
428
429
  // Convert the round up flag to a mask
430
2278
  ubv normalRoundUpAmount(ubv(roundUp).matchWidth(extractedSignificand));
431
2278
  ubv subnormalRoundUpMask(ubv(roundUp).append(ubv::zero(targetSignificandWidth)).signExtendRightShift(ubv(targetSignificandWidth + 1, targetSignificandWidth)));
432
2278
  ubv subnormalRoundUpAmount(subnormalRoundUpMask & subnormalIncrementAmount);
433
434
2278
  ubv rawRoundedSignificand((ITE(normalRounding,
435
				 extractedSignificand,
436
				 subnormalMaskedSignificand)
437
			     +
438
			     ITE(normalRounding,
439
				 normalRoundUpAmount,
440
				 subnormalRoundUpAmount)));
441
442
  // We might have lost the leading one, if so, re-add and note that we need to increment the significand
443
1180
  prop significandOverflow(rawRoundedSignificand.extract(targetSignificandWidth, targetSignificandWidth).isAllOnes());
444
1139
  INVARIANT(IMPLIES(significandOverflow, roundUp));
445
446
2278
  ubv extractedRoundedSignificand(rawRoundedSignificand.extract(targetSignificandWidth - 1, 0));
447
2278
  ubv roundedSignificand(extractedRoundedSignificand | leadingOne);
448
1139
  INVARIANT(IMPLIES(significandOverflow, extractedRoundedSignificand.isAllZeros()));
449
450
451
452
453
  /*** Round to correct exponent. ***/
454
455
  // The extend is almost certainly unnecessary (see specialised rounders)
456
2278
  sbv extendedExponent(exp.extend(1));
457
458
1180
  prop incrementExponentNeeded(roundUp && significandOverflow);  // The roundUp is implied but kept for signal forwarding
459
1139
  probabilityAnnotation<t>(incrementExponentNeeded, VERYUNLIKELY);
460
1180
  prop incrementExponent(!known.noSignificandOverflow && incrementExponentNeeded);
461
1139
  INVARIANT(IMPLIES(known.noSignificandOverflow, !incrementExponentNeeded));
462
463
2278
  sbv correctedExponent(conditionalIncrement<t>(incrementExponent, extendedExponent));
464
465
  // Track overflows and underflows
466
2278
  sbv maxNormal(unpackedFloat<t>::maxNormalExponent(format).matchWidth(correctedExponent));
467
2278
  sbv minSubnormal(unpackedFloat<t>::minSubnormalExponent(format).matchWidth(correctedExponent));
468
469
2278
  sbv correctedExponentInRange(collar<t>(correctedExponent, minSubnormal, maxNormal));
470
471
472
  // This can over and underflow but these values will not be used
473
1139
  bwt currentExponentWidth(correctedExponentInRange.getWidth());
474
2278
  sbv roundedExponent(correctedExponentInRange.contract(currentExponentWidth - targetExponentWidth));
475
476
477
478
  /*** Finish ***/
479
480
1180
  prop computedOverflow(potentialLateOverflow && incrementExponentNeeded);
481
1180
  prop computedUnderflow(potentialLateUnderflow && !incrementExponentNeeded);
482
1139
  probabilityAnnotation<t>(computedOverflow, UNLIKELY);
483
1139
  probabilityAnnotation<t>(computedUnderflow, UNLIKELY);
484
485
1180
  prop lateOverflow(!earlyOverflow && computedOverflow);
486
1180
  prop lateUnderflow(!earlyUnderflow && computedUnderflow);
487
1139
  probabilityAnnotation<t>(lateOverflow, VERYUNLIKELY);
488
1139
  probabilityAnnotation<t>(lateUnderflow, VERYUNLIKELY);
489
490
491
  // So that ITE abstraction works...
492
1180
  prop overflow(!known.noOverflow && ITE(lateOverflow, prop(true), earlyOverflow));
493
1180
  prop underflow(!known.noUnderflow && ITE(lateUnderflow, prop(true), earlyUnderflow));
494
495
2278
  unpackedFloat<t> roundedResult(uf.getSign(), roundedExponent, roundedSignificand);
496
1139
  unpackedFloat<t> result(rounderSpecialCases<t>(format, roundingMode, roundedResult,
497
						 overflow, underflow, uf.getZero()));
498
499
1139
  POSTCONDITION(result.valid(format));
500
501
2278
  return result;
502
 }
503
504
template <class t>
505
unpackedFloat<t> originalRounder (const typename t::fpt &format,
506
				  const typename t::rm &roundingMode,
507
				  const unpackedFloat<t> &uf) {
508
509
  typedef typename t::bwt bwt;
510
  typedef typename t::prop prop;
511
  typedef typename t::ubv ubv;
512
  typedef typename t::sbv sbv;
513
514
  //PRECONDITION(uf.valid(format));
515
  // Not a precondition because
516
  //  1. Exponent and significand may be extended.
517
  //  2. Their values may also be outside of the correct range.
518
  //
519
  // However some thing do hold:
520
  //  1. Leading bit of the significant is 1   (if you want to get a meaningful answer)
521
  //     (if not, a cancellation on the near path of add can cause
522
  //      this, but the result will not be used, so it can be incorrect)
523
  ubv psig(uf.getSignificand());
524
  bwt sigWidth(psig.getWidth());
525
  //PRECONDITION(psig.extract(sigWidth-1, sigWidth-1).isAllOnes());
526
  ubv sig(psig | unpackedFloat<t>::leadingOne(sigWidth));
527
528
  //  2. Must have round and sticky bits
529
  bwt targetSignificandWidth(unpackedFloat<t>::significandWidth(format));
530
  PRECONDITION(sigWidth >= targetSignificandWidth + 2);
531
532
  //  3. Must have at least enough exponent bits
533
  sbv exp(uf.getExponent());
534
  bwt expWidth(exp.getWidth());
535
  bwt targetExponentWidth(unpackedFloat<t>::exponentWidth(format));
536
  PRECONDITION(expWidth >= targetExponentWidth);
537
538
  // Also, do not round special values.
539
  // Note that this relies on these having default values and
540
  // the code that calls the rounder constructing uf from parts.
541
  PRECONDITION(!uf.getNaN());
542
  PRECONDITION(!uf.getInf());
543
  //PRECONDITION(!uf.getZero());   // The safe choice of default values means this should work OK
544
545
546
547
  /*** Early underflow and overflow detection ***/
548
  bwt exponentExtension(expWidth - targetExponentWidth);
549
  prop earlyOverflow(exp > unpackedFloat<t>::maxNormalExponent(format).extend(exponentExtension));
550
  prop earlyUnderflow(exp < unpackedFloat<t>::minSubnormalExponent(format).extend(exponentExtension).decrement());
551
  // Optimisation : if the precondition on sigWidth and targetSignificandWidth is removed
552
  //                then can change to:
553
  //                   exponent >= minSubnormalExponent - 1
554
  //                && sigWidth > targetSignificandBits
555
556
557
558
  /*** Normal or subnormal rounding? ***/
559
  prop normalRounding(exp >= unpackedFloat<t>::minNormalExponent(format).extend(exponentExtension));
560
  probabilityAnnotation<t>(normalRounding, LIKELY);
561
562
563
  /*** Round to correct significand. ***/
564
  ubv extractedSignificand(sig.extract(sigWidth - 1, sigWidth - targetSignificandWidth));
565
566
  bwt guardBitPosition(sigWidth - (targetSignificandWidth + 1));
567
  prop guardBit(sig.extract(guardBitPosition, guardBitPosition).isAllOnes());
568
569
  prop stickyBit(!sig.extract(guardBitPosition - 1,0).isAllZeros());
570
571
572
  // For subnormals, locating the guard and stick bits is a bit more involved
573
  sbv subnormalAmount(unpackedFloat<t>::maxSubnormalExponent(format).extend(exponentExtension) - exp);
574
  prop belowLimit(subnormalAmount <= sbv::zero(expWidth));    // Not subnormal
575
  prop aboveLimit(subnormalAmount >= sbv(expWidth, targetSignificandWidth));  // Will underflow
576
  sbv subnormalShift(ITE((belowLimit || aboveLimit), sbv::zero(expWidth), subnormalAmount));
577
  // Optimisation : collar
578
579
  ubv subnormalShiftPrepared(subnormalShift.toUnsigned().extend(targetSignificandWidth - expWidth));
580
  ubv guardLocation(ubv::one(targetSignificandWidth) << subnormalShiftPrepared);
581
  ubv stickyMask(guardLocation.decrement());
582
583
584
  prop subnormalGuardBit(!(extractedSignificand & guardLocation).isAllZeros());
585
  prop subnormalStickyBit(guardBit || stickyBit ||
586
			  !((extractedSignificand & stickyMask).isAllZeros()));
587
588
589
590
591
  // Can overflow but is handled
592
  ubv incrementedSignificand(extractedSignificand.modularIncrement());
593
  prop incrementedSignificandOverflow(incrementedSignificand.isAllZeros());
594
  // Optimisation : conditional increment
595
  // Optimisation : use top bit of significand to increment the exponent
596
597
  ubv correctedIncrementedSignificand(ITE(!incrementedSignificandOverflow,
598
					  incrementedSignificand,
599
					  unpackedFloat<t>::leadingOne(unpackedFloat<t>::significandWidth(format))));
600
601
602
  ubv incrementAmount(guardLocation.modularLeftShift(ubv::one(guardLocation.getWidth()))); // Overflows (safely) in the case of rounding up to the least subnormal.
603
  ubv mask(guardLocation | stickyMask);
604
  ubv maskedSignificand(extractedSignificand & ~mask);
605
606
  ubv subnormalIncrementedSignificand(maskedSignificand.modularAdd(incrementAmount));
607
  prop subnormalIncrementedSignificandOverflow(subnormalIncrementedSignificand.isAllZeros());
608
  ubv subnomalCorrectedIncrementedSignificand(ITE(!subnormalIncrementedSignificandOverflow,
609
						  subnormalIncrementedSignificand,
610
						  unpackedFloat<t>::leadingOne(unpackedFloat<t>::significandWidth(format))));
611
612
613
614
  // Have to choose the right one dependent on rounding mode
615
  prop choosenGuardBit(ITE(normalRounding, guardBit, subnormalGuardBit));
616
  prop choosenStickyBit(ITE(normalRounding, stickyBit, subnormalStickyBit));
617
618
  prop significandEven(ITE(normalRounding,
619
			   extractedSignificand.extract(0,0).isAllZeros(),
620
			   ((extractedSignificand & incrementAmount).isAllZeros())));
621
  prop roundUp(roundingDecision<t>(roundingMode, uf.getSign(), significandEven,
622
				   choosenGuardBit, choosenStickyBit, prop(false)));
623
624
  ubv roundedSignificand(ITE(normalRounding,
625
			     ITE((!roundUp), extractedSignificand, correctedIncrementedSignificand),
626
			     ITE((!roundUp), maskedSignificand, subnomalCorrectedIncrementedSignificand)));
627
628
629
630
  /*** Round to correct exponent. ***/
631
632
  // The extend is almost certainly unnecessary (see specialised rounders)
633
  sbv extendedExponent(exp.extend(1));
634
635
  prop incrementExponent(ITE(normalRounding,
636
			     incrementedSignificandOverflow,
637
			     subnormalIncrementedSignificandOverflow)
638
			 && roundUp);
639
  probabilityAnnotation<t>(incrementExponent, VERYUNLIKELY);
640
641
  sbv correctedExponent(conditionalIncrement<t>(incrementExponent, extendedExponent));
642
643
  // This can over and underflow but these values will not be used
644
  bwt currentExponentWidth(correctedExponent.getWidth());
645
  sbv roundedExponent(correctedExponent.contract(currentExponentWidth - targetExponentWidth));
646
647
648
  /*** Finish ***/
649
  prop computedOverflow(correctedExponent > unpackedFloat<t>::maxNormalExponent(format).extend(currentExponentWidth - targetExponentWidth));
650
  prop computedUnderflow(correctedExponent < unpackedFloat<t>::minSubnormalExponent(format).extend(currentExponentWidth - targetExponentWidth));
651
652
  // So that ITE abstraction works...
653
  prop overflow(ITE(earlyOverflow, prop(true), computedOverflow));
654
  prop underflow(ITE(earlyUnderflow, prop(true), computedUnderflow));
655
656
  unpackedFloat<t> roundedResult(uf.getSign(), roundedExponent, roundedSignificand);
657
  unpackedFloat<t> result(rounderSpecialCases<t>(format, roundingMode, roundedResult,
658
						 overflow, underflow, uf.getZero()));
659
660
  POSTCONDITION(result.valid(format));
661
662
  return result;
663
 }
664
665
666
template <class t>
667
351
  unpackedFloat<t> rounder (const typename t::fpt &format,
668
			    const typename t::rm &roundingMode,
669
			    const unpackedFloat<t> &uf) {
670
  typedef typename t::prop prop;
671
366
  customRounderInfo<t> cri(prop(false), prop(false), prop(false), prop(false), prop(false));  // Default is to know nothing
672
673
  #ifdef USE_ORIGINAL_ROUNDER
674
  return originalRounder(format, roundingMode, uf);  // Allow old versions to be compared
675
  #else
676
366
  return customRounder(format, roundingMode, uf, cri);
677
  #endif
678
 }
679
680
681
}
682
683
#endif