Custom floating-point number.

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