diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-02-11 13:55:41 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-02-11 13:55:41 -0800 |
commit | 45f4d6c7e8678e140b363f3114b5393ed1f29681 (patch) | |
tree | 4c59d7ba61a8612cde9e056153b9e609ec1104fb /src/misc/util | |
parent | ab2d3acac99620aef7d5b1c48eb59ee33bb2b584 (diff) | |
download | abc-45f4d6c7e8678e140b363f3114b5393ed1f29681.tar.gz abc-45f4d6c7e8678e140b363f3114b5393ed1f29681.tar.bz2 abc-45f4d6c7e8678e140b363f3114b5393ed1f29681.zip |
Movinng custom floating-point implementations, etc.
Diffstat (limited to 'src/misc/util')
-rw-r--r-- | src/misc/util/abc_global.h | 2 | ||||
-rw-r--r-- | src/misc/util/utilDouble.h | 222 | ||||
-rw-r--r-- | src/misc/util/utilFloat.h | 226 |
3 files changed, 450 insertions, 0 deletions
diff --git a/src/misc/util/abc_global.h b/src/misc/util/abc_global.h index 00d5d514..9e906816 100644 --- a/src/misc/util/abc_global.h +++ b/src/misc/util/abc_global.h @@ -225,6 +225,8 @@ static inline double Abc_MinDouble( double a, double b ) { return a < b ? static inline int Abc_Float2Int( float Val ) { union { int x; float y; } v; v.y = Val; return v.x; } static inline float Abc_Int2Float( int Num ) { union { int x; float y; } v; v.x = Num; return v.y; } +static inline word Abc_Dbl2Word( double Dbl ) { union { word x; double y; } v; v.y = Dbl; return v.x; } +static inline double Abc_Word2Dbl( word Num ) { union { word x; double y; } v; v.x = Num; return v.y; } static inline int Abc_Base2Log( unsigned n ) { int r; if ( n < 2 ) return n; for ( r = 0, n--; n; n >>= 1, r++ ) {}; return r; } static inline int Abc_Base10Log( unsigned n ) { int r; if ( n < 2 ) return n; for ( r = 0, n--; n; n /= 10, r++ ) {}; return r; } static inline int Abc_Base16Log( unsigned n ) { int r; if ( n < 2 ) return n; for ( r = 0, n--; n; n /= 16, r++ ) {}; return r; } diff --git a/src/misc/util/utilDouble.h b/src/misc/util/utilDouble.h new file mode 100644 index 00000000..0d023781 --- /dev/null +++ b/src/misc/util/utilDouble.h @@ -0,0 +1,222 @@ +/**CFile**************************************************************** + + FileName [utilDouble.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [] + + Synopsis [Double floating point number implementation.] + + Author [Alan Mishchenko, Bruno Schmitt] + + Affiliation [UC Berkeley / UFRGS] + + Date [Ver. 1.0. Started - February 11, 2017.] + + Revision [] + +***********************************************************************/ + +#ifndef ABC__sat__Xdbl__Xdbl_h +#define ABC__sat__Xdbl__Xdbl_h + +#include "misc/util/abc_global.h" + +ABC_NAMESPACE_HEADER_START + +//////////////////////////////////////////////////////////////////////// +/// STRUCTURE DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/* + The xdbl floating-point number is represented as a 64-bit unsigned int. + The number is (2^Exp)*Mnt, where Exp is a 16-bit exponent and Mnt is a + 48-bit mantissa. The decimal point is located between the MSB of Mnt, + which is always 1, and the remaining 15 digits of Mnt. + + Currently, only positive numbers are represented. + + The range of possible values is [1.0; 2^(2^16-1)*1.111111111111111] + that is, the smallest possible number is 1.0 and the largest possible + number is 2^(---16 ones---).(1.---47 ones---) + + Comparison of numbers can be done by comparing the underlying unsigned ints. + + Only addition, multiplication, and division by 2^n are currently implemented. +*/ + +typedef word xdbl; + +static inline word Xdbl_Exp( xdbl a ) { return a >> 48; } +static inline word Xdbl_Mnt( xdbl a ) { return (a << 16) >> 16; } + +static inline xdbl Xdbl_Create( word Exp, word Mnt ) { assert(!(Exp>>16) && (Mnt>>47)==(word)1); return (Exp<<48) | Mnt; } + +static inline xdbl Xdbl_Const1() { return Xdbl_Create( (word)0, (word)1 << 47 ); } +static inline xdbl Xdbl_Const2() { return Xdbl_Create( (word)1, (word)1 << 47 ); } +static inline xdbl Xdbl_Const3() { return Xdbl_Create( (word)1, (word)3 << 46 ); } +static inline xdbl Xdbl_Const12() { return Xdbl_Create( (word)3, (word)3 << 46 ); } +static inline xdbl Xdbl_Const1point5() { return Xdbl_Create( (word)0, (word)3 << 46 ); } +static inline xdbl Xdbl_Const2point5() { return Xdbl_Create( (word)1, (word)5 << 45 ); } +static inline xdbl Xdbl_Maximum() { return ~(word)0; } + +static inline double Xdbl_ToDouble( xdbl a ) { assert(Xdbl_Exp(a) < 1023); return Abc_Word2Dbl(((Xdbl_Exp(a) + 1023) << 52) | (((a<<17)>>17) << 5)); } +static 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)); } + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Adding two floating-point numbers.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline xdbl Xdbl_Add( xdbl a, xdbl b ) +{ + word Exp, Mnt; + if ( a < b ) a ^= b, b ^= a, a ^= b; + assert( a >= b ); + Mnt = Xdbl_Mnt(a) + (Xdbl_Mnt(b) >> (Xdbl_Exp(a) - Xdbl_Exp(b))); + Exp = Xdbl_Exp(a); + if ( Mnt >> 48 ) // new MSB is created + Exp++, Mnt >>= 1; + if ( Exp >> 16 ) // overflow + return Xdbl_Maximum(); + return Xdbl_Create( Exp, Mnt ); +} + +/**Function************************************************************* + + Synopsis [Multiplying two floating-point numbers.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline xdbl Xdbl_Mul( xdbl a, xdbl b ) +{ + word Exp, Mnt, MntA, MntB, MntAh, MntBh, MntAl, MntBl; + if ( a < b ) a ^= b, b ^= a, a ^= b; + assert( a >= b ); + MntA = Xdbl_Mnt(a); + MntB = Xdbl_Mnt(b); + MntAh = MntA>>32; + MntBh = MntB>>32; + MntAl = (MntA<<32)>>32; + MntBl = (MntB<<32)>>32; + Mnt = ((MntAh * MntBh) << 17) + ((MntAl * MntBl) >> 47) + ((MntAl * MntBh) >> 15) + ((MntAh * MntBl) >> 15); + Exp = Xdbl_Exp(a) + Xdbl_Exp(b); + if ( Mnt >> 48 ) // new MSB is created + Exp++, Mnt >>= 1; + if ( Exp >> 16 ) // overflow + return Xdbl_Maximum(); + return Xdbl_Create( Exp, Mnt ); +} + +/**Function************************************************************* + + Synopsis [Dividing floating point number by a degree of 2.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline xdbl Xdbl_Div( xdbl a, unsigned Deg2 ) +{ + if ( Xdbl_Exp(a) >= (word)Deg2 ) + return Xdbl_Create( Xdbl_Exp(a) - Deg2, Xdbl_Mnt(a) ); + return Xdbl_Const1(); // underflow +} + +/**Function************************************************************* + + Synopsis [Testing procedure.] + + Description [Helpful link https://www.h-schmidt.net/FloatConverter/IEEE754.html] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Xdbl_Test() +{ + xdbl c1 = Xdbl_Const1(); + xdbl c2 = Xdbl_Const2(); + xdbl c3 = Xdbl_Const3(); + xdbl c12 = Xdbl_Const12(); + xdbl c1p5 = Xdbl_Const1point5(); + xdbl c2p5 = Xdbl_Const2point5(); + + xdbl c1_ = Xdbl_FromDouble(1.0); + xdbl c2_ = Xdbl_FromDouble(2.0); + xdbl c3_ = Xdbl_FromDouble(3.0); + xdbl c12_ = Xdbl_FromDouble(12.0); + xdbl c1p5_ = Xdbl_FromDouble(1.5); + xdbl c2p5_ = Xdbl_FromDouble(2.5); + + xdbl sum1 = Xdbl_Add(c1, c1p5); + xdbl mul1 = Xdbl_Mul(c2, c1p5); + + xdbl sum2 = Xdbl_Add(c1p5, c2p5); + xdbl mul2 = Xdbl_Mul(c1p5, c2p5); + + xdbl a = Xdbl_FromDouble(1.2929725); + xdbl b = Xdbl_FromDouble(10.28828287); + xdbl ab = Xdbl_Mul(a, b); + + xdbl ten100 = Xdbl_FromDouble( 1e100 ); + xdbl ten100_ = ABC_CONST(0x014c924d692ca61b); + + assert( ten100 == ten100_ ); + +// float f1 = Xdbl_ToDouble(c1); +// Extra_PrintBinary( stdout, (int *)&c1, 32 ); printf( "\n" ); +// Extra_PrintBinary( stdout, (int *)&f1, 32 ); printf( "\n" ); + + printf( "1 = %lf\n", Xdbl_ToDouble(c1) ); + printf( "2 = %lf\n", Xdbl_ToDouble(c2) ); + printf( "3 = %lf\n", Xdbl_ToDouble(c3) ); + printf( "12 = %lf\n", Xdbl_ToDouble(c12) ); + printf( "1.5 = %lf\n", Xdbl_ToDouble(c1p5) ); + printf( "2.5 = %lf\n", Xdbl_ToDouble(c2p5) ); + + printf( "Converted 1 = %lf\n", Xdbl_ToDouble(c1_) ); + printf( "Converted 2 = %lf\n", Xdbl_ToDouble(c2_) ); + printf( "Converted 3 = %lf\n", Xdbl_ToDouble(c3_) ); + printf( "Converted 12 = %lf\n", Xdbl_ToDouble(c12_) ); + printf( "Converted 1.5 = %lf\n", Xdbl_ToDouble(c1p5_) ); + printf( "Converted 2.5 = %lf\n", Xdbl_ToDouble(c2p5_) ); + + printf( "1.0 + 1.5 = %lf\n", Xdbl_ToDouble(sum1) ); + printf( "2.0 * 1.5 = %lf\n", Xdbl_ToDouble(mul1) ); + + printf( "1.5 + 2.5 = %lf\n", Xdbl_ToDouble(sum2) ); + printf( "1.5 * 2.5 = %lf\n", Xdbl_ToDouble(mul2) ); + printf( "12 / 2^2 = %lf\n", Xdbl_ToDouble(Xdbl_Div(c12, 2)) ); + + printf( "12 / 2^2 = %lf\n", Xdbl_ToDouble(Xdbl_Div(c12, 2)) ); + + printf( "%.16lf * %.16lf = %.16lf (%.16lf)\n", Xdbl_ToDouble(a), Xdbl_ToDouble(b), Xdbl_ToDouble(ab), 1.2929725 * 10.28828287 ); + + assert( sum1 == c2p5 ); + assert( mul1 == c3 ); +} + +ABC_NAMESPACE_HEADER_END + +#endif diff --git a/src/misc/util/utilFloat.h b/src/misc/util/utilFloat.h new file mode 100644 index 00000000..f0739a92 --- /dev/null +++ b/src/misc/util/utilFloat.h @@ -0,0 +1,226 @@ +/**CFile**************************************************************** + + FileName [utilFloat.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [] + + Synopsis [Floating point number implementation.] + + Author [Alan Mishchenko, Bruno Schmitt] + + Affiliation [UC Berkeley / UFRGS] + + Date [Ver. 1.0. Started - January 28, 2017.] + + Revision [] + +***********************************************************************/ +#ifndef ABC__sat__xSAT__xsatFloat_h +#define ABC__sat__xSAT__xsatFloat_h + +#include "misc/util/abc_global.h" + +ABC_NAMESPACE_HEADER_START + +//////////////////////////////////////////////////////////////////////// +/// STRUCTURE DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/* + The xFloat_t floating-point number is represented as a 32-bit unsigned int. + The number is (2^Exp)*Mnt, where Exp is a 16-bit exponent and Mnt is a + 16-bit mantissa. The decimal point is located between the MSB of Mnt, + which is always 1, and the remaining 15 digits of Mnt. + + Currently, only positive numbers are represented. + + The range of possible values is [1.0; 2^(2^16-1)*1.111111111111111] + that is, the smallest possible number is 1.0 and the largest possible + number is 2^(---16 ones---).(1.---15 ones---) + + Comparison of numbers can be done by comparing the underlying unsigned ints. + + Only addition, multiplication, and division by 2^n are currently implemented. +*/ + +typedef struct xFloat_t_ xFloat_t; +struct xFloat_t_ +{ + unsigned Mnt : 16; + unsigned Exp : 16; +}; + +static inline unsigned xSat_Float2Uint( xFloat_t f ) { union { xFloat_t f; unsigned u; } temp; temp.f = f; return temp.u; } +static inline xFloat_t xSat_Uint2Float( unsigned u ) { union { xFloat_t f; unsigned u; } temp; temp.u = u; return temp.f; } +static inline int xSat_LessThan( xFloat_t a, xFloat_t b ) { return a.Exp < b.Exp || (a.Exp == b.Exp && a.Mnt < b.Mnt); } +static inline int xSat_Equal( xFloat_t a, xFloat_t b ) { return a.Exp == b.Exp && a.Mnt == b.Mnt; } + +static inline xFloat_t xSat_FloatCreate( unsigned Exp, unsigned Mnt ) { xFloat_t res; res.Exp = Exp; res.Mnt = Mnt; return res; } + +static inline xFloat_t xSat_FloatCreateConst1() { return xSat_FloatCreate( 0, 1 << 15 ); } +static inline xFloat_t xSat_FloatCreateConst2() { return xSat_FloatCreate( 1, 1 << 15 ); } +static inline xFloat_t xSat_FloatCreateConst3() { return xSat_FloatCreate( 1, 3 << 14 ); } +static inline xFloat_t xSat_FloatCreateConst12() { return xSat_FloatCreate( 3, 3 << 14 ); } +static inline xFloat_t xSat_FloatCreateConst1point5() { return xSat_FloatCreate( 0, 3 << 14 ); } +static inline xFloat_t xSat_FloatCreateConst2point5() { return xSat_FloatCreate( 1, 5 << 13 ); } +static inline xFloat_t xSat_FloatCreateMaximum() { return xSat_Uint2Float( 0xFFFFFFFF ); } + +static inline float xSat_Float2Float( xFloat_t a ) { assert(a.Exp < 127); return Abc_Int2Float(((a.Exp + 127) << 23) | ((a.Mnt & 0x7FFF) << 8)); } +static 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)); } + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Adding two floating-point numbers.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline xFloat_t xSat_FloatAdd( xFloat_t a, xFloat_t b ) +{ + unsigned Exp, Mnt; + if ( a.Exp < b.Exp ) + return xSat_FloatAdd(b, a); + assert( a.Exp >= b.Exp ); + // compute new mantissa + Mnt = a.Mnt + (b.Mnt >> (a.Exp - b.Exp)); + // compute new exponent + Exp = a.Exp; + // update exponent and mantissa if new MSB is created + if ( Mnt & 0xFFFF0000 ) // new MSB bit is created + Exp++, Mnt >>= 1; + // check overflow + if ( Exp & 0xFFFF0000 ) // overflow + return xSat_Uint2Float( 0xFFFFFFFF ); + assert( (Exp & 0xFFFF0000) == 0 ); + assert( (Mnt & 0xFFFF0000) == 0 ); + assert( Mnt & 0x00008000 ); + return xSat_FloatCreate( Exp, Mnt ); +} + +/**Function************************************************************* + + Synopsis [Multiplying two floating-point numbers.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline xFloat_t xSat_FloatMul( xFloat_t a, xFloat_t b ) +{ + unsigned Exp, Mnt; + if ( a.Exp < b.Exp ) + return xSat_FloatMul(b, a); + assert( a.Exp >= b.Exp ); + // compute new mantissa + Mnt = (a.Mnt * b.Mnt) >> 15; + // compute new exponent + Exp = a.Exp + b.Exp; + // update exponent and mantissa if new MSB is created + if ( Mnt & 0xFFFF0000 ) // new MSB bit is created + Exp++, Mnt >>= 1; + // check overflow + if ( Exp & 0xFFFF0000 ) // overflow + return xSat_Uint2Float( 0xFFFFFFFF ); + assert( (Exp & 0xFFFF0000) == 0 ); + assert( (Mnt & 0xFFFF0000) == 0 ); + assert( Mnt & 0x00008000 ); + return xSat_FloatCreate( Exp, Mnt ); +} + +/**Function************************************************************* + + Synopsis [Dividing floating point number by a degree of 2.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline xFloat_t xSat_FloatDiv( xFloat_t a, unsigned Deg2 ) +{ + assert( Deg2 < 0xFFFF ); + if ( a.Exp >= Deg2 ) + return xSat_FloatCreate( a.Exp - Deg2, a.Mnt ); + return xSat_FloatCreateConst1(); // underflow +} + +/**Function************************************************************* + + Synopsis [Testing procedure.] + + Description [Helpful link https://www.h-schmidt.net/FloatConverter/IEEE754.html] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void xSat_FloatTest() +{ + xFloat_t c1 = xSat_FloatCreateConst1(); + xFloat_t c2 = xSat_FloatCreateConst2(); + xFloat_t c3 = xSat_FloatCreateConst3(); + xFloat_t c12 = xSat_FloatCreateConst12(); + xFloat_t c1p5 = xSat_FloatCreateConst1point5(); + xFloat_t c2p5 = xSat_FloatCreateConst2point5(); + + xFloat_t c1_ = xSat_FloatFromFloat(1.0); + xFloat_t c2_ = xSat_FloatFromFloat(2.0); + xFloat_t c3_ = xSat_FloatFromFloat(3.0); + xFloat_t c12_ = xSat_FloatFromFloat(12.0); + xFloat_t c1p5_ = xSat_FloatFromFloat(1.5); + xFloat_t c2p5_ = xSat_FloatFromFloat(2.5); + + xFloat_t sum1 = xSat_FloatAdd(c1, c1p5); + xFloat_t mul1 = xSat_FloatMul(c2, c1p5); + + xFloat_t sum2 = xSat_FloatAdd(c1p5, c2p5); + xFloat_t mul2 = xSat_FloatMul(c1p5, c2p5); + +// float f1 = xSat_Float2Float(c1); +// Extra_PrintBinary( stdout, (int *)&c1, 32 ); printf( "\n" ); +// Extra_PrintBinary( stdout, (int *)&f1, 32 ); printf( "\n" ); + + printf( "1 = %f\n", xSat_Float2Float(c1) ); + printf( "2 = %f\n", xSat_Float2Float(c2) ); + printf( "3 = %f\n", xSat_Float2Float(c3) ); + printf( "12 = %f\n", xSat_Float2Float(c12) ); + printf( "1.5 = %f\n", xSat_Float2Float(c1p5) ); + printf( "2.5 = %f\n", xSat_Float2Float(c2p5) ); + + printf( "Converted 1 = %f\n", xSat_Float2Float(c1_) ); + printf( "Converted 2 = %f\n", xSat_Float2Float(c2_) ); + printf( "Converted 3 = %f\n", xSat_Float2Float(c3_) ); + printf( "Converted 12 = %f\n", xSat_Float2Float(c12_) ); + printf( "Converted 1.5 = %f\n", xSat_Float2Float(c1p5_) ); + printf( "Converted 2.5 = %f\n", xSat_Float2Float(c2p5_) ); + + printf( "1.0 + 1.5 = %f\n", xSat_Float2Float(sum1) ); + printf( "2.0 * 1.5 = %f\n", xSat_Float2Float(mul1) ); + + printf( "1.5 + 2.5 = %f\n", xSat_Float2Float(sum2) ); + printf( "1.5 * 2.5 = %f\n", xSat_Float2Float(mul2) ); + printf( "12 / 2^2 = %f\n", xSat_Float2Float(xSat_FloatDiv(c12, 2)) ); + + assert( xSat_Equal(sum1, c2p5) ); + assert( xSat_Equal(mul1, c3) ); +} + +ABC_NAMESPACE_HEADER_END + +#endif |