diff options
Diffstat (limited to 'src/sat/xsat')
-rw-r--r-- | src/sat/xsat/xsatFloat.h | 213 |
1 files changed, 213 insertions, 0 deletions
diff --git a/src/sat/xsat/xsatFloat.h b/src/sat/xsat/xsatFloat.h new file mode 100644 index 00000000..73b74ff7 --- /dev/null +++ b/src/sat/xsat/xsatFloat.h @@ -0,0 +1,213 @@ +/**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" +#include "misc/vec/vecInt.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)); } + +//////////////////////////////////////////////////////////////////////// +/// 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 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( "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 |