ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
utilDouble.h
Go to the documentation of this file.
1
20
21#ifndef ABC__sat__Xdbl__Xdbl_h
22#define ABC__sat__Xdbl__Xdbl_h
23
25
27
31
32/*
33 The xdbl floating-point number is represented as a 64-bit unsigned int.
34 The number is (2^Exp)*Mnt, where Exp is a 16-bit exponent and Mnt is a
35 48-bit mantissa. The decimal point is located between the MSB of Mnt,
36 which is always 1, and the remaining 15 digits of Mnt.
37
38 Currently, only positive numbers are represented.
39
40 The range of possible values is [1.0; 2^(2^16-1)*1.111111111111111]
41 that is, the smallest possible number is 1.0 and the largest possible
42 number is 2^(---16 ones---).(1.---47 ones---)
43
44 Comparison of numbers can be done by comparing the underlying unsigned ints.
45
46 Only addition, multiplication, and division by 2^n are currently implemented.
47*/
48
49typedef word xdbl;
50
51static inline word Xdbl_Exp( xdbl a ) { return a >> 48; }
52static inline word Xdbl_Mnt( xdbl a ) { return (a << 16) >> 16; }
53
54static inline xdbl Xdbl_Create( word Exp, word Mnt ) { assert(!(Exp>>16) && (Mnt>>47)==(word)1); return (Exp<<48) | Mnt; }
55
56static inline xdbl Xdbl_Const1() { return Xdbl_Create( (word)0, (word)1 << 47 ); }
57static inline xdbl Xdbl_Const2() { return Xdbl_Create( (word)1, (word)1 << 47 ); }
58static inline xdbl Xdbl_Const3() { return Xdbl_Create( (word)1, (word)3 << 46 ); }
59static inline xdbl Xdbl_Const12() { return Xdbl_Create( (word)3, (word)3 << 46 ); }
60static inline xdbl Xdbl_Const1point5() { return Xdbl_Create( (word)0, (word)3 << 46 ); }
61static inline xdbl Xdbl_Const2point5() { return Xdbl_Create( (word)1, (word)5 << 45 ); }
62static inline xdbl Xdbl_Maximum() { return ~(word)0; }
63
64static inline double Xdbl_ToDouble( xdbl a ) { assert(Xdbl_Exp(a) < 1023); return Abc_Word2Dbl(((Xdbl_Exp(a) + 1023) << 52) | (((a<<17)>>17) << 5)); }
65static inline xdbl Xdbl_FromDouble( double a ) { word A = Abc_Dbl2Word(a); assert(a >= 1.0); return Xdbl_Create((A >> 52)-1023, (((word)1) << 47) | ((A << 12) >> 17)); }
66
70
82static inline xdbl Xdbl_Add( xdbl a, xdbl b )
83{
84 word Exp, Mnt;
85 if ( a < b ) a ^= b, b ^= a, a ^= b;
86 assert( a >= b );
87 Mnt = Xdbl_Mnt(a) + (Xdbl_Mnt(b) >> (Xdbl_Exp(a) - Xdbl_Exp(b)));
88 Exp = Xdbl_Exp(a);
89 if ( Mnt >> 48 ) // new MSB is created
90 Exp++, Mnt >>= 1;
91 if ( Exp >> 16 ) // overflow
92 return Xdbl_Maximum();
93 return Xdbl_Create( Exp, Mnt );
94}
95
107static inline xdbl Xdbl_Mul( xdbl a, xdbl b )
108{
109 word Exp, Mnt, MntA, MntB, MntAh, MntBh, MntAl, MntBl;
110 if ( a < b ) a ^= b, b ^= a, a ^= b;
111 assert( a >= b );
112 MntA = Xdbl_Mnt(a);
113 MntB = Xdbl_Mnt(b);
114 MntAh = MntA>>32;
115 MntBh = MntB>>32;
116 MntAl = (MntA<<32)>>32;
117 MntBl = (MntB<<32)>>32;
118 Mnt = ((MntAh * MntBh) << 17) + ((MntAl * MntBl) >> 47) + ((MntAl * MntBh) >> 15) + ((MntAh * MntBl) >> 15);
119 Exp = Xdbl_Exp(a) + Xdbl_Exp(b);
120 if ( Mnt >> 48 ) // new MSB is created
121 Exp++, Mnt >>= 1;
122 if ( Exp >> 16 ) // overflow
123 return Xdbl_Maximum();
124 return Xdbl_Create( Exp, Mnt );
125}
126
138static inline xdbl Xdbl_Div( xdbl a, unsigned Deg2 )
139{
140 if ( Xdbl_Exp(a) >= (word)Deg2 )
141 return Xdbl_Create( Xdbl_Exp(a) - Deg2, Xdbl_Mnt(a) );
142 return Xdbl_Const1(); // underflow
143}
144
156static inline void Xdbl_Test()
157{
158 xdbl c1 = Xdbl_Const1();
159 xdbl c2 = Xdbl_Const2();
160 xdbl c3 = Xdbl_Const3();
161 xdbl c12 = Xdbl_Const12();
162 xdbl c1p5 = Xdbl_Const1point5();
163 xdbl c2p5 = Xdbl_Const2point5();
164
165 xdbl c1_ = Xdbl_FromDouble(1.0);
166 xdbl c2_ = Xdbl_FromDouble(2.0);
167 xdbl c3_ = Xdbl_FromDouble(3.0);
168 xdbl c12_ = Xdbl_FromDouble(12.0);
169 xdbl c1p5_ = Xdbl_FromDouble(1.5);
170 xdbl c2p5_ = Xdbl_FromDouble(2.5);
171
172 xdbl sum1 = Xdbl_Add(c1, c1p5);
173 xdbl mul1 = Xdbl_Mul(c2, c1p5);
174
175 xdbl sum2 = Xdbl_Add(c1p5, c2p5);
176 xdbl mul2 = Xdbl_Mul(c1p5, c2p5);
177
178 xdbl a = Xdbl_FromDouble(1.2929725);
179 xdbl b = Xdbl_FromDouble(10.28828287);
180 xdbl ab = Xdbl_Mul(a, b);
181
182 xdbl ten100 = Xdbl_FromDouble( 1e100 );
183 xdbl ten100_ = ABC_CONST(0x014c924d692ca61b);
184
185 assert( ten100 == ten100_ );
186
187// float f1 = Xdbl_ToDouble(c1);
188// Extra_PrintBinary( stdout, (int *)&c1, 32 ); printf( "\n" );
189// Extra_PrintBinary( stdout, (int *)&f1, 32 ); printf( "\n" );
190
191 printf( "1 = %lf\n", Xdbl_ToDouble(c1) );
192 printf( "2 = %lf\n", Xdbl_ToDouble(c2) );
193 printf( "3 = %lf\n", Xdbl_ToDouble(c3) );
194 printf( "12 = %lf\n", Xdbl_ToDouble(c12) );
195 printf( "1.5 = %lf\n", Xdbl_ToDouble(c1p5) );
196 printf( "2.5 = %lf\n", Xdbl_ToDouble(c2p5) );
197
198 printf( "Converted 1 = %lf\n", Xdbl_ToDouble(c1_) );
199 printf( "Converted 2 = %lf\n", Xdbl_ToDouble(c2_) );
200 printf( "Converted 3 = %lf\n", Xdbl_ToDouble(c3_) );
201 printf( "Converted 12 = %lf\n", Xdbl_ToDouble(c12_) );
202 printf( "Converted 1.5 = %lf\n", Xdbl_ToDouble(c1p5_) );
203 printf( "Converted 2.5 = %lf\n", Xdbl_ToDouble(c2p5_) );
204
205 printf( "1.0 + 1.5 = %lf\n", Xdbl_ToDouble(sum1) );
206 printf( "2.0 * 1.5 = %lf\n", Xdbl_ToDouble(mul1) );
207
208 printf( "1.5 + 2.5 = %lf\n", Xdbl_ToDouble(sum2) );
209 printf( "1.5 * 2.5 = %lf\n", Xdbl_ToDouble(mul2) );
210 printf( "12 / 2^2 = %lf\n", Xdbl_ToDouble(Xdbl_Div(c12, 2)) );
211
212 printf( "12 / 2^2 = %lf\n", Xdbl_ToDouble(Xdbl_Div(c12, 2)) );
213
214 printf( "%.16lf * %.16lf = %.16lf (%.16lf)\n", Xdbl_ToDouble(a), Xdbl_ToDouble(b), Xdbl_ToDouble(ab), 1.2929725 * 10.28828287 );
215
216 assert( sum1 == c2p5 );
217 assert( mul1 == c3 );
218}
219
221
222#endif
#define ABC_CONST(number)
PARAMETERS ///.
Definition abc_global.h:240
#define ABC_NAMESPACE_HEADER_END
#define ABC_NAMESPACE_HEADER_START
NAMESPACES ///.
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
ABC_NAMESPACE_HEADER_START typedef word xdbl
STRUCTURE DEFINITIONS ///.
Definition utilDouble.h:49
#define assert(ex)
Definition util_old.h:213