package FloatingPoint;

import FloatingPoint.FloatCompareLess;



// ************************************************************************** //
//                                                                            //
//    eses                   eses                                             //
//   eses                     eses                                            //
//  eses    eseses  esesese    eses   Embedded Systems Group                  //
//  ese    ese  ese ese         ese                                           //
//  ese    eseseses eseseses    ese   Department of Computer Science          //
//  eses   eses          ese   eses                                           //
//   eses   eseses  eseseses  eses    University of Kaiserslautern            //
//    eses                   eses                                             //
//                                                                            //
// ************************************************************************** //
// This module implements multiplication of IEEE-like floating point numbers. //
// The algorithm below deals with the full IEEE standard including denormal   //
// and normal numbers, infinity and NaN values.                               //
// ************************************************************************** //

// parameters of the floating-point format
macro MantWidth = 4;
macro ExpWidth  = 3;
macro ExpMax    = exp(2,ExpWidth)-1;
macro ExpBias   = ExpMax / 2;
macro ExpMin    = +1 - ExpBias;
macro Width     = 1+ExpWidth+MantWidth;

macro MantMinNorm = exp(2,MantWidth-1);  // smallest normalized mantissa
macro MantMax     = exp(2,MantWidth)-1;  // largest mantissa value

// macros for extracting parts of the floating point number
macro Sign(x) = x{-1};
macro Exp(x)  = x{-2:MantWidth};
macro Mant(x) = x{MantWidth-1:0};
macro RmHBit(x) = Mant(x);            // remove hidden bit

// macros for interpretation of the floating point numbers
macro ValSign(s)    = (s?-1.0:1.0);
macro ValNMant(m)   = bv2nat(true@m)  * exp(2.0,-1*MantWidth);
macro ValDMant(m)   = bv2nat(false@m) * exp(2.0,-1*MantWidth);
macro ValMant(e,m)  = (e=={false::ExpWidth} ? ValDMant(m) : ValNMant(m));
macro ValNExp(e)    = +bv2nat(e)-ExpBias;
macro ValDExp(e)    = +1-ExpBias;
macro ValExp(e)     = (e=={false::ExpWidth} ? ValDExp(e) : ValNExp(e));
macro Float2Real(x) = ValSign(Sign(x)) * ValMant(Exp(x),Mant(x)) * exp(2.0,ValExp(Exp(x)));

// special values
macro posZero = false@{false::ExpWidth}@{false::MantWidth};
macro negZero =  true@{false::ExpWidth}@{false::MantWidth};
macro posInf  = false@{ true::ExpWidth}@{false::MantWidth};
macro negInf  =  true@{ true::ExpWidth}@{false::MantWidth};
macro posNaN  = false@{ true::ExpWidth}@{ true::MantWidth};
macro negNaN  =  true@{ true::ExpWidth}@{ true::MantWidth};


// Definition of some operations: declaration as macro
macro isZero(x)      = ( ( Exp(x) == {false::ExpWidth} ) & ( Mant(x) == {false::MantWidth} ) );
macro isNormal(x)    = ( 1 <= bv2nat(Exp(x)) ) & ( bv2nat(Exp(x)) <= (exp(2,ExpWidth)-2) );
macro isSubnormal(x) = ( Exp(x) == {false::ExpWidth} ) & ( Mant(x) != {false::MantWidth} );
macro isFinite(x)    = ( isZero(x) | isSubnormal(x) | isNormal(x) );
macro isInfinite(x)  = ( Exp(x) == {true::ExpWidth} ) & ( Mant(x) == {false::MantWidth} );
macro isNaN(x)       = ( Exp(x) == {true::ExpWidth} ) & ( Mant(x) != {false::MantWidth} );
macro isSignMinus(x) = ( Sign(x) != false );

// Macros that return a float
macro fAbs(x)         = (false@Exp(x)@Mant(x));
macro fCopySign(x,y)  = (Sign(y)@Exp(x)@Mant(x));
macro fNegate(x)      = ((Sign(x) ? false : true)@Exp(x)@Mant(x));


/**
 * FloatCompareNotLess
 * 
 * Return false if one or both inputs are NaN. Otherwise, the
 * function returns not compareLess
 */
module FloatCompareNotLess(bv{Width} ?x, ?y, bool !r) {
    bool notR;
    if( isNaN(x) | isNaN(y) ) {
        r = false;
    } else {
        FloatCompareLess(x,y,notR);
        r = !notR;
    }
}
// -------------- special case: NaNs --------------------
drivenby { // 0
    x = posNaN;
    y = posNaN;
    assert(r==false);
}
drivenby { // 1
    x = negNaN;
    y = posNaN;
    assert(r==false);
}
drivenby { // 2
    x = posNaN;
    y = negNaN;
    assert(r==false);
}
drivenby { // 3
    x = negNaN;
    y = negNaN;
    assert(r==false);
}
drivenby { // 4
    x = (false@0b010@0b0011);
    y = posNaN;
    assert(r==false);
}
drivenby { // 5
    x = posNaN;
    y = (false@0b010@0b0011);
    assert(r==false);
}
drivenby { // 6
    x = (false@0b010@0b0011);
    y = negNaN;
    assert(r==false);
}
drivenby { // 7
    x = negNaN;
    y = (false@0b010@0b0011);
    assert(r==false);
}
// -------------- special case: zeros --------------------
drivenby { // 8
    x = posZero;
    y = posZero;
    assert(r==true);
}
drivenby { // 9
    x = negZero;
    y = posZero;
    assert(r==true);
}
drivenby { // 10
    x = posZero;
    y = negZero;
    assert(r==true);
}
drivenby { // 11
    x = negZero;
    y = negZero;
    assert(r==true);
}
// -------------- special cases: +/-Inf --------------------
drivenby { // 12
    x = (false@0b010@0b0011);
    y = posInf;
    assert(r==false);
}
drivenby { // 13
    x = posInf;
    y = (false@0b010@0b0011);
    assert(r==true);
}
drivenby { // 14
    x = (false@0b010@0b0011);
    y = negInf;
    assert(r==true);
}
drivenby { // 15
    x = negInf;
    y = (false@0b010@0b0011);
    assert(r==false);
}
drivenby { // 16
    x = posInf;
    y = posInf;
    assert(r==true);
}
drivenby { // 17
    x = posInf;
    y = negInf;
    assert(r==true);
}
drivenby { // 18
    x = negInf;
    y = posInf;
    assert(r==false);
}
drivenby { // 19
    x = negInf;
    y = negInf;
    assert(r==true);
}
// -------------- regular cases--------------------
drivenby { // 20
    x = (false@0b010@0b0110);
    y = (false@0b010@0b0110);
    assert(r==true);
}
drivenby { // 21
    x = (true@0b010@0b0110);
    y = (false@0b010@0b0110);
    assert(r==false);
}
drivenby { // 22
    x = (false@0b010@0b0110);
    y = (true@0b010@0b0110);
    assert(r==true);
}
drivenby { // 23
    x = (true@0b100@0b0110);
    y = (true@0b100@0b0110);
    assert(r==true);
}