diff options
Diffstat (limited to 'src/sat/xsat/xsatFloat.h')
-rw-r--r-- | src/sat/xsat/xsatFloat.h | 227 |
1 files changed, 0 insertions, 227 deletions
diff --git a/src/sat/xsat/xsatFloat.h b/src/sat/xsat/xsatFloat.h deleted file mode 100644 index fb451a94..00000000 --- a/src/sat/xsat/xsatFloat.h +++ /dev/null @@ -1,227 +0,0 @@ -/**CFile**************************************************************** - - FileName [xsatFloat.h] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [xSAT - A SAT solver written in C. - Read the license file for more info.] - - 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 |