summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/sat/xsat/xsatFloat.h213
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
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-05 00:50:55 +0000