1 |
|
/* |
2 |
|
** Copyright (C) 2018 Martin Brain |
3 |
|
** |
4 |
|
** See the file LICENSE for licensing information. |
5 |
|
*/ |
6 |
|
|
7 |
|
/* |
8 |
|
** packing.h |
9 |
|
** |
10 |
|
** Martin Brain |
11 |
|
** martin.brain@cs.ox.ac.uk |
12 |
|
** 03/06/14 |
13 |
|
** |
14 |
|
** Algorithms for converting from a packed float (a bit vector) into |
15 |
|
** the working, unpacked float format. Should be instantiated with a |
16 |
|
** traits structure from one of the baseTypes/ implementations. |
17 |
|
** |
18 |
|
*/ |
19 |
|
|
20 |
|
#include "symfpu/core/unpackedFloat.h" |
21 |
|
|
22 |
|
#ifndef SYMFPU_PACKING |
23 |
|
#define SYMFPU_PACKING |
24 |
|
|
25 |
|
namespace symfpu { |
26 |
|
|
27 |
|
template<class t> |
28 |
339 |
unpackedFloat<t> unpack (const typename t::fpt format, const typename t::ubv &packedFloat) { |
29 |
|
typedef typename t::bwt bwt; |
30 |
|
typedef typename t::prop prop; |
31 |
|
typedef typename t::ubv ubv; |
32 |
|
typedef typename t::sbv sbv; |
33 |
|
|
34 |
339 |
bwt pWidth = format.packedWidth(); |
35 |
339 |
bwt exWidth = format.packedExponentWidth(); |
36 |
339 |
bwt sigWidth = format.packedSignificandWidth(); |
37 |
|
|
38 |
339 |
PRECONDITION(packedFloat.getWidth() == pWidth); |
39 |
|
|
40 |
|
// Extract |
41 |
678 |
ubv packedSignificand(packedFloat.extract(sigWidth - 1, 0)); |
42 |
678 |
ubv packedExponent(packedFloat.extract(sigWidth + exWidth - 1, sigWidth)); |
43 |
353 |
prop sign(packedFloat.extract(pWidth - 1, sigWidth + exWidth).isAllOnes()); |
44 |
|
|
45 |
|
// Prepare the normal and subnormal cases |
46 |
339 |
bwt unpackedExWidth = unpackedFloat<t>::exponentWidth(format); |
47 |
339 |
bwt unpackedSigWidth = unpackedFloat<t>::significandWidth(format); |
48 |
|
|
49 |
339 |
INVARIANT(unpackedExWidth > exWidth); // To avoid overflow |
50 |
678 |
sbv biasedExponent(packedExponent.extend(unpackedExWidth - exWidth).toSigned() - unpackedFloat<t>::bias(format)); |
51 |
|
// Optimisation : both the normal and subnormal paths subtract a constant |
52 |
|
// from the exponent as the last step (bias and minNormalExponent respectively) |
53 |
|
|
54 |
678 |
ubv significandWithLeadingZero(packedSignificand.extend(unpackedSigWidth - sigWidth)); |
55 |
678 |
ubv significandWithLeadingOne(unpackedFloat<t>::leadingOne(unpackedFloat<t>::significandWidth(format)) | significandWithLeadingZero); |
56 |
|
|
57 |
678 |
unpackedFloat<t> ufNormal(sign, biasedExponent, significandWithLeadingOne); |
58 |
678 |
unpackedFloat<t> ufSubnormalBase(sign, unpackedFloat<t>::minNormalExponent(format), significandWithLeadingZero); |
59 |
|
|
60 |
|
// Optimisation : right shift the significand by one if subnormal |
61 |
|
// and then set the carry in when you add to the exponent. |
62 |
|
// May be sufficient to just assert that it has a leading zero |
63 |
|
|
64 |
|
|
65 |
|
// Analyse |
66 |
353 |
prop zeroExponent(packedExponent.isAllZeros()); |
67 |
353 |
prop onesExponent(packedExponent.isAllOnes()); |
68 |
353 |
prop zeroSignificand(significandWithLeadingZero.isAllZeros()); // Shared with normaliseUp |
69 |
|
|
70 |
|
// Identify the cases |
71 |
353 |
prop isZero(zeroExponent && zeroSignificand); |
72 |
353 |
prop isSubnormal(zeroExponent && !zeroSignificand); |
73 |
353 |
prop isNormal(!zeroExponent && !onesExponent); |
74 |
353 |
prop isInf(onesExponent && zeroSignificand); |
75 |
353 |
prop isNaN(onesExponent && !zeroSignificand); |
76 |
|
|
77 |
339 |
INVARIANT(isZero || isSubnormal || isNormal || isInf || isNaN); |
78 |
|
|
79 |
339 |
probabilityAnnotation<t,prop>(isSubnormal, UNLIKELY); |
80 |
|
|
81 |
|
// Splice together |
82 |
989 |
unpackedFloat<t> uf(ITE(isNaN, |
83 |
|
unpackedFloat<t>::makeNaN(format), |
84 |
|
ITE(isInf, |
85 |
|
unpackedFloat<t>::makeInf(format, sign), |
86 |
|
ITE(isZero, |
87 |
|
unpackedFloat<t>::makeZero(format, sign), |
88 |
650 |
ITE(!isSubnormal, |
89 |
|
ufNormal, |
90 |
|
ufSubnormalBase.normaliseUp(format) ))))); |
91 |
|
|
92 |
339 |
POSTCONDITION(uf.valid(format)); |
93 |
|
|
94 |
678 |
return uf; |
95 |
|
} |
96 |
|
|
97 |
|
|
98 |
|
template<class t> |
99 |
6266 |
typename t::ubv pack (const typename t::fpt &format, const unpackedFloat<t> &uf) { |
100 |
|
typedef typename t::bwt bwt; |
101 |
|
typedef typename t::prop prop; |
102 |
|
typedef typename t::ubv ubv; |
103 |
|
typedef typename t::sbv sbv; |
104 |
|
|
105 |
6266 |
PRECONDITION(uf.valid(format)); |
106 |
|
|
107 |
|
// Sign |
108 |
12532 |
ubv packedSign(uf.getSign()); |
109 |
|
|
110 |
|
// Exponent |
111 |
6266 |
bwt packedExWidth(format.packedExponentWidth()); |
112 |
|
|
113 |
9409 |
prop inNormalRange(uf.inNormalRange(format, prop(true))); |
114 |
6266 |
INVARIANT(inNormalRange || uf.inSubnormalRange(format, prop(true))); // Default values ensure this. |
115 |
|
//prop inSubnormalRange(uf.inSubnormalRange(format)); // Allowing this optimisation |
116 |
9409 |
prop inSubnormalRange(!inNormalRange); |
117 |
|
|
118 |
6266 |
probabilityAnnotation<t,prop>(inNormalRange, LIKELY); |
119 |
6266 |
probabilityAnnotation<t,prop>(inSubnormalRange, UNLIKELY); |
120 |
|
|
121 |
12532 |
sbv biasedExp(uf.getExponent() + unpackedFloat<t>::bias(format)); |
122 |
|
// Will be correct for normal values only, subnormals may still be negative. |
123 |
12532 |
ubv packedBiasedExp(biasedExp.toUnsigned().extract(packedExWidth - 1,0)); |
124 |
|
|
125 |
12532 |
ubv maxExp(ubv::allOnes(packedExWidth)); |
126 |
12532 |
ubv minExp(ubv::zero(packedExWidth)); |
127 |
|
|
128 |
9409 |
prop hasMaxExp(uf.getNaN() || uf.getInf()); |
129 |
9409 |
prop hasMinExp(uf.getZero() || inSubnormalRange); |
130 |
9409 |
prop hasFixedExp(hasMaxExp || hasMinExp); |
131 |
|
|
132 |
12532 |
ubv packedExp(ITE(hasFixedExp, |
133 |
|
ITE(hasMaxExp, maxExp, minExp), |
134 |
|
packedBiasedExp)); |
135 |
|
|
136 |
|
|
137 |
|
// Significand |
138 |
6266 |
bwt packedSigWidth = format.packedSignificandWidth(); |
139 |
12532 |
ubv unpackedSignificand(uf.getSignificand()); |
140 |
6266 |
bwt unpackedSignificandWidth = unpackedSignificand.getWidth(); |
141 |
|
|
142 |
6266 |
INVARIANT(packedSigWidth == unpackedSignificandWidth - 1); |
143 |
12532 |
ubv dropLeadingOne(unpackedSignificand.extract(packedSigWidth - 1,0)); |
144 |
|
|
145 |
12532 |
ubv subnormalShiftAmount(uf.getSubnormalAmount(format).toUnsigned()); |
146 |
12532 |
ubv shiftAmount((subnormalShiftAmount.getWidth() <= unpackedSignificandWidth) ? |
147 |
|
subnormalShiftAmount.matchWidth(unpackedSignificand) : |
148 |
|
subnormalShiftAmount.extract(unpackedSignificandWidth - 1, 0)); |
149 |
|
// The extraction could loose data if exponent is much larger than the significand |
150 |
|
// However getSubnormalAmount is between 0 and packedSigWidth so it should be safe |
151 |
12532 |
ubv correctedSubnormal((unpackedSignificand >> shiftAmount).extract(packedSigWidth - 1,0)); |
152 |
|
|
153 |
9409 |
prop hasFixedSignificand(uf.getNaN() || uf.getInf() || uf.getZero()); |
154 |
|
|
155 |
18798 |
ubv packedSig(ITE(hasFixedSignificand, |
156 |
6266 |
ITE(uf.getNaN(), |
157 |
|
unpackedFloat<t>::nanPattern(packedSigWidth), |
158 |
|
ubv::zero(packedSigWidth)), |
159 |
|
ITE(inNormalRange, |
160 |
|
dropLeadingOne, |
161 |
|
correctedSubnormal))); |
162 |
|
|
163 |
|
|
164 |
|
// Finish up |
165 |
6266 |
ubv packed(packedSign.append(packedExp).append(packedSig)); |
166 |
|
|
167 |
6266 |
POSTCONDITION(packed.getWidth() == format.packedWidth()); |
168 |
|
|
169 |
12532 |
return packed; |
170 |
|
} |
171 |
|
|
172 |
|
} |
173 |
|
|
174 |
|
#endif |