ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
utilFloat.h
Go to the documentation of this file.
1
20#ifndef ABC__sat__xSAT__xsatFloat_h
21#define ABC__sat__xSAT__xsatFloat_h
22
23#include "misc/util/abc_global.h"
24
25ABC_NAMESPACE_HEADER_START
26
30
31/*
32 The xFloat_t floating-point number is represented as a 32-bit unsigned int.
33 The number is (2^Exp)*Mnt, where Exp is a 16-bit exponent and Mnt is a
34 16-bit mantissa. The decimal point is located between the MSB of Mnt,
35 which is always 1, and the remaining 15 digits of Mnt.
36
37 Currently, only positive numbers are represented.
38
39 The range of possible values is [1.0; 2^(2^16-1)*1.111111111111111]
40 that is, the smallest possible number is 1.0 and the largest possible
41 number is 2^(---16 ones---).(1.---15 ones---)
42
43 Comparison of numbers can be done by comparing the underlying unsigned ints.
44
45 Only addition, multiplication, and division by 2^n are currently implemented.
46*/
47
48typedef struct xFloat_t_ xFloat_t;
49struct xFloat_t_
50{
51 unsigned Mnt : 16;
52 unsigned Exp : 16;
53};
54
55static inline unsigned xSat_Float2Uint( xFloat_t f ) { union { xFloat_t f; unsigned u; } temp; temp.f = f; return temp.u; }
56static inline xFloat_t xSat_Uint2Float( unsigned u ) { union { xFloat_t f; unsigned u; } temp; temp.u = u; return temp.f; }
57static inline int xSat_LessThan( xFloat_t a, xFloat_t b ) { return a.Exp < b.Exp || (a.Exp == b.Exp && a.Mnt < b.Mnt); }
58static inline int xSat_Equal( xFloat_t a, xFloat_t b ) { return a.Exp == b.Exp && a.Mnt == b.Mnt; }
59
60static inline xFloat_t xSat_FloatCreate( unsigned Exp, unsigned Mnt ) { xFloat_t res; res.Exp = Exp; res.Mnt = Mnt; return res; }
61
62static inline xFloat_t xSat_FloatCreateConst1() { return xSat_FloatCreate( 0, 1 << 15 ); }
63static inline xFloat_t xSat_FloatCreateConst2() { return xSat_FloatCreate( 1, 1 << 15 ); }
64static inline xFloat_t xSat_FloatCreateConst3() { return xSat_FloatCreate( 1, 3 << 14 ); }
65static inline xFloat_t xSat_FloatCreateConst12() { return xSat_FloatCreate( 3, 3 << 14 ); }
66static inline xFloat_t xSat_FloatCreateConst1point5() { return xSat_FloatCreate( 0, 3 << 14 ); }
67static inline xFloat_t xSat_FloatCreateConst2point5() { return xSat_FloatCreate( 1, 5 << 13 ); }
68static inline xFloat_t xSat_FloatCreateMaximum() { return xSat_Uint2Float( 0xFFFFFFFF ); }
69
70static inline float xSat_Float2Float( xFloat_t a ) { assert(a.Exp < 127); return Abc_Int2Float(((a.Exp + 127) << 23) | ((a.Mnt & 0x7FFF) << 8)); }
71static inline xFloat_t xSat_FloatFromFloat( float a ) { int A = Abc_Float2Int(a); assert(a >= 1.0); return xSat_FloatCreate((A >> 23)-127, 0x8000 | ((A >> 8) & 0x7FFF)); }
72
76
88static inline xFloat_t xSat_FloatAdd( xFloat_t a, xFloat_t b )
89{
90 unsigned Exp, Mnt;
91 if ( a.Exp < b.Exp )
92 return xSat_FloatAdd(b, a);
93 assert( a.Exp >= b.Exp );
94 // compute new mantissa
95 Mnt = a.Mnt + (b.Mnt >> (a.Exp - b.Exp));
96 // compute new exponent
97 Exp = a.Exp;
98 // update exponent and mantissa if new MSB is created
99 if ( Mnt & 0xFFFF0000 ) // new MSB bit is created
100 Exp++, Mnt >>= 1;
101 // check overflow
102 if ( Exp & 0xFFFF0000 ) // overflow
103 return xSat_Uint2Float( 0xFFFFFFFF );
104 assert( (Exp & 0xFFFF0000) == 0 );
105 assert( (Mnt & 0xFFFF0000) == 0 );
106 assert( Mnt & 0x00008000 );
107 return xSat_FloatCreate( Exp, Mnt );
108}
109
121static inline xFloat_t xSat_FloatMul( xFloat_t a, xFloat_t b )
122{
123 unsigned Exp, Mnt;
124 if ( a.Exp < b.Exp )
125 return xSat_FloatMul(b, a);
126 assert( a.Exp >= b.Exp );
127 // compute new mantissa
128 Mnt = (a.Mnt * b.Mnt) >> 15;
129 // compute new exponent
130 Exp = a.Exp + b.Exp;
131 // update exponent and mantissa if new MSB is created
132 if ( Mnt & 0xFFFF0000 ) // new MSB bit is created
133 Exp++, Mnt >>= 1;
134 // check overflow
135 if ( Exp & 0xFFFF0000 ) // overflow
136 return xSat_Uint2Float( 0xFFFFFFFF );
137 assert( (Exp & 0xFFFF0000) == 0 );
138 assert( (Mnt & 0xFFFF0000) == 0 );
139 assert( Mnt & 0x00008000 );
140 return xSat_FloatCreate( Exp, Mnt );
141}
142
154static inline xFloat_t xSat_FloatDiv( xFloat_t a, unsigned Deg2 )
155{
156 assert( Deg2 < 0xFFFF );
157 if ( a.Exp >= Deg2 )
158 return xSat_FloatCreate( a.Exp - Deg2, a.Mnt );
159 return xSat_FloatCreateConst1(); // underflow
160}
161
173static inline void xSat_FloatTest()
174{
175 xFloat_t c1 = xSat_FloatCreateConst1();
176 xFloat_t c2 = xSat_FloatCreateConst2();
177 xFloat_t c3 = xSat_FloatCreateConst3();
178 xFloat_t c12 = xSat_FloatCreateConst12();
179 xFloat_t c1p5 = xSat_FloatCreateConst1point5();
180 xFloat_t c2p5 = xSat_FloatCreateConst2point5();
181
182 xFloat_t c1_ = xSat_FloatFromFloat(1.0);
183 xFloat_t c2_ = xSat_FloatFromFloat(2.0);
184 xFloat_t c3_ = xSat_FloatFromFloat(3.0);
185 xFloat_t c12_ = xSat_FloatFromFloat(12.0);
186 xFloat_t c1p5_ = xSat_FloatFromFloat(1.5);
187 xFloat_t c2p5_ = xSat_FloatFromFloat(2.5);
188
189 xFloat_t sum1 = xSat_FloatAdd(c1, c1p5);
190 xFloat_t mul1 = xSat_FloatMul(c2, c1p5);
191
192 xFloat_t sum2 = xSat_FloatAdd(c1p5, c2p5);
193 xFloat_t mul2 = xSat_FloatMul(c1p5, c2p5);
194
195// float f1 = xSat_Float2Float(c1);
196// Extra_PrintBinary( stdout, (int *)&c1, 32 ); printf( "\n" );
197// Extra_PrintBinary( stdout, (int *)&f1, 32 ); printf( "\n" );
198
199 printf( "1 = %f\n", xSat_Float2Float(c1) );
200 printf( "2 = %f\n", xSat_Float2Float(c2) );
201 printf( "3 = %f\n", xSat_Float2Float(c3) );
202 printf( "12 = %f\n", xSat_Float2Float(c12) );
203 printf( "1.5 = %f\n", xSat_Float2Float(c1p5) );
204 printf( "2.5 = %f\n", xSat_Float2Float(c2p5) );
205
206 printf( "Converted 1 = %f\n", xSat_Float2Float(c1_) );
207 printf( "Converted 2 = %f\n", xSat_Float2Float(c2_) );
208 printf( "Converted 3 = %f\n", xSat_Float2Float(c3_) );
209 printf( "Converted 12 = %f\n", xSat_Float2Float(c12_) );
210 printf( "Converted 1.5 = %f\n", xSat_Float2Float(c1p5_) );
211 printf( "Converted 2.5 = %f\n", xSat_Float2Float(c2p5_) );
212
213 printf( "1.0 + 1.5 = %f\n", xSat_Float2Float(sum1) );
214 printf( "2.0 * 1.5 = %f\n", xSat_Float2Float(mul1) );
215
216 printf( "1.5 + 2.5 = %f\n", xSat_Float2Float(sum2) );
217 printf( "1.5 * 2.5 = %f\n", xSat_Float2Float(mul2) );
218 printf( "12 / 2^2 = %f\n", xSat_Float2Float(xSat_FloatDiv(c12, 2)) );
219
220 assert( xSat_Equal(sum1, c2p5) );
221 assert( xSat_Equal(mul1, c3) );
222}
223
224ABC_NAMESPACE_HEADER_END
225
226#endif
abc_global.h
ABC_NAMESPACE_HEADER_END
#define ABC_NAMESPACE_HEADER_END
Definition abc_namespaces.h:51
ABC_NAMESPACE_HEADER_START
#define ABC_NAMESPACE_HEADER_START
NAMESPACES ///.
Definition abc_namespaces.h:50
xFloat_t_
Definition utilFloat.h:50
xFloat_t_::Mnt
unsigned Mnt
Definition utilFloat.h:51
xFloat_t_::Exp
unsigned Exp
Definition utilFloat.h:52
xFloat_t
typedefABC_NAMESPACE_HEADER_START struct xFloat_t_ xFloat_t
STRUCTURE DEFINITIONS ///.
Definition utilFloat.h:48
assert
#define assert(ex)
Definition util_old.h:213