package FloatingPoint;





// ************************************************************************** //
//                                                                            //
//    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));

// Macros to shift a bitvector by the given (constant!) width
macro shiftRightNStep(x,n) = {false::n}@(x{-1:n});
macro shiftLeftNStep(x,n)  = (x{-(1+n):0})@{false::n};

// Macros to shift a bitvector by the given (constant!) width
// in dependence of the given condition bit. If the condition
// bit is set, the bitvector is shifted, if the condition bit
// is not set, the vector is not modified and returned.
macro shiftRightNCStep(x,n,c) = (c ? shiftRightNStep(x,n) : x);
macro shiftLeftNCStep(x,n,c) = (c ? shiftLeftNStep(x,n) : x);

// Macros to shift a bitvector by up to 1, 2, 4 bits (depending on the
// width of the shift amount). Note: N represents the width of the shift
// amount in shiftRightN and shiftLeftN
macro shiftRight1(x,s) = shiftRightNCStep(x,1,s{0});
macro shiftLeft1(x,s)  = shiftLeftNCStep(x,1,s{0});

macro shiftRight2(x,s) = shiftRightNCStep(shiftRight1(x,s),2,s{1});
macro shiftLeft2(x,s)  = shiftLeftNCStep(shiftLeft1(x,s),2,s{1});

macro shiftRight3(x,s) = shiftRightNCStep(shiftRight2(x,s),4,s{2});
macro shiftLeft3(x,s)  = shiftLeftNCStep(shiftLeft2(x,s),4,s{2});

// This macro defines the maximal left-bit-shift by an exponent. It
// is required to determine the bitwidth of an integer.
macro AddExpWidth = ExpMax - ExpBias;
// Bitwidth to represent a float as integer PLUS the precision bits)
macro MaxIntFullPrecBitWidth = AddExpWidth + 1 + MantWidth + 1;

// fCopySign will be used as a macro. FloatCopySign is a simple wrapper to test the macro.
module FloatConvertToInteger(bv{Width} ?x,int !z, bool !exception) {
  bv{MaxIntFullPrecBitWidth} x_exp_correct;
  bool r_bit, s_bit;
  bool is_even;

  // Check special cases
  if( isNaN( x ) ) {
    emit( exception );
  } else if( isZero( x ) ) {
    z = 0;
  } else if( isInfinite( x ) ) {
    emit( exception );
  } 

  // Compute Mant(x) << Exp(x) including precision bits.
  else if( isSubnormal ( x ) ) {
    // assumption: ExpWidth >= 2
    // (-1) ^sign(x) * exp(x+1) * (0.x) = (-1) ^sign(x) * exp(x) * (x{-1}.x{-2:0})
    if( ValNExp(Exp(x)) >= 0 ) {
      // With condition isSubnormal(x), we conclude Exp(x)==0
      // With assumption ExpWidth >= 2 ==> (Exp(x) - ExpBias) < 0
      // Hence, this case must not occur
      assert(false);
    } else if( ValNExp(Exp(x)) <= -2 ) {
      // In this case, x results in a number <= 0.25, i.e. all bits of mantissa will
      // only influence the result of the sticky bit while the round bit always results
      // in 0.
      x_exp_correct = shiftRight3({false::AddExpWidth}@Mant(x)@{false::2}, nat2bv( ExpBias - bv2nat(Exp(x)), ExpWidth ) );
      r_bit = false;
      s_bit = Mant(x)!={false::MantWidth};
    } else {
      // Exp(x) - ExpBias == -1 only if ExpWidth==2
      assert( ExpWidth==2 );
      // shift right 1 bit
      x_exp_correct = shiftRight3({false::AddExpWidth}@Mant(x)@{false::2}, nat2bv( ExpBias - bv2nat(Exp(x)), ExpWidth ) );
      r_bit = x_exp_correct{MantWidth};
      s_bit = x_exp_correct{(MantWidth-1):0}!={false::MantWidth};
    }
  } else {
    // (-1) ^sign(x) * exp(x) * (1.x)
    if( ValNExp(Exp(x)) >= 0 ) {
      x_exp_correct = shiftLeft3({false::AddExpWidth}@true@Mant(x)@false, nat2bv( bv2nat(Exp(x)) - ExpBias, ExpWidth ) );
      r_bit = x_exp_correct{MantWidth};
      s_bit = x_exp_correct{(MantWidth-1):0}!={false::MantWidth};
    } else if( ValNExp(Exp(x)) <= -2 ) { // x results in a number <= 0.25
      // In this case, x results in a number <= 0.25, i.e. all bits of mantissa will
      // only influence the result of the sticky bit
      x_exp_correct = shiftRight3({false::AddExpWidth}@true@Mant(x)@false, nat2bv( ExpBias - bv2nat(Exp(x)), ExpWidth ) );
      r_bit = false;
      s_bit = true; // always true because actual mantissa=1.xxxx => the one will always occur in the sticky bit computation
    } else { // ValNExp(Exp(x)) == -1
      x_exp_correct = shiftRight3({false::AddExpWidth}@true@Mant(x)@false, nat2bv( ExpBias - bv2nat(Exp(x)), ExpWidth ) );
      r_bit = x_exp_correct{MantWidth};
      s_bit = x_exp_correct{(MantWidth-1):0}!={false::MantWidth};
    }
  }
  is_even = x_exp_correct{(MantWidth+1)}==false;

  // Including precision bits, _BUT_ only to keep track of sticky bits as long as the
  // number can be 0.5xxxx. This is only for normal numbers with exp=-1.
  // Smaller exponents result in numbers <=0.25 that are eventually rounded

  // round to nearest even
  if( !r_bit | ( r_bit & !s_bit & is_even ) ) {  // < 0.5 || ==0.5 && (x_exp_correct is even)
    if( Sign(x) ) {
      z = -bv2nat( x_exp_correct{-1:(AddExpWidth + 1)} );
    } else {
      z = bv2nat( x_exp_correct{-1:(AddExpWidth + 1)} );
    }
  } else if ( ( r_bit & s_bit )    | ( r_bit & !s_bit & !is_even ) ) {
    //        (x_exp_correct>=0.5) | (x_exp_correct==0.5) & (x_exp_correct is odd)
    if( Sign(x) ) {
      z = -( bv2nat( x_exp_correct{-1:(AddExpWidth + 1)} ) + 1 );
    } else {
      z = bv2nat( x_exp_correct{-1:(AddExpWidth + 1)} ) + 1;
    }
  } else {
    assert( false );
  }
}
// x==y ==> z=x=y
drivenby { // 000
    x = posZero;
    assert(z==0);
}
drivenby { // 001
    x = negZero;
    assert(z==0);
}
drivenby { // 002
    x = posInf;
    assert(exception);
}
drivenby { // 003
    x = negInf;
    assert(exception);
}
drivenby { // 004
    x = posNaN;
    assert(exception);
}
drivenby { // 005
    x = negNaN;
    assert(exception);
}
// following test cases only cover round-to-nearest-even
// some floats that already have an integer value
drivenby { // 006
    x = (false@0b011@0b0000); // (-1)^0 * 2^(0b011-0b011) * 1.0000
    assert(z==1);
}
drivenby { // 007
    x = (true@0b011@0b0000); // (-1)^1 * 2^(0b011-0b011) * 1.0000
    assert(z==-1);
}
drivenby { // 008
    x = (false@0b100@0b0000); // (-1)^0 * 2^(0b100-0b011) * 1.0000
    assert(z==2);
}
drivenby { // 009
    x = (false@0b101@0b1100); // (-1)^0 * 2^(0b101-0b011) * 1.1100
    assert(z==7);
}
drivenby { // 010
    x = (true@0b110@0b0110); // (-1)^1 * 2^(0b110-0b011) * 1.0110
    assert(z==-11);
}
// some denormalized floats that will result in 0
drivenby { // 011
    x = (true@0b000@0b1000); // (-1)^1 * 2^(0b000-0b011) * 1.000
    assert(z==0);
}
drivenby { // 012
    x = (true@0b001@0b1000); // (-1)^1 * 2^(0b001-0b011) * 1.1000
    assert(z==0);
}
drivenby { // 013
    x = (false@0b001@0b0000); // (-1)^0 * 2^(0b001-0b011) * 1.0000
    assert(z==0);
}
drivenby { // 014
    x = (false@0b010@0b1000); // (-1)^0 * 2^(0b010-0b011) * 1.1000
    assert(z==1);
}
// some floats that need to be rounded towards 0 (<x.5)
drivenby { // 015
    x = (false@0b011@0b0111); // (-1)^0 * 2^(0b011-0b011) * 1.0111
    assert(z==1);
}
drivenby { // 016
    x = (true@0b101@0b1101); // (-1)^1 * 2^(0b101-0b011) * 1.1101
    assert(z==-7);
}
drivenby { // 017
    x = (false@0b101@0b0111); // (-1)^0 * 2^(0b101-0b011) * 1.0001
    assert(z==6);
}
drivenby { // 018
    x = (true@0b100@0b1010); // (-1)^1 * 2^(0b100-0b011) * 1.1010
    assert(z==-3);
}
// some floats that need to be rounded towards +/- inf (>x.5)
drivenby { // 019
    x = (false@0b011@0b1011); // (-1)^0 * 2^(0b011-0b011) * 1.1011
    assert(z==2);
}
drivenby { // 020
    x = (true@0b100@0b1101); // (-1)^1 * 2^(0b100-0b011) * 1.1101
    assert(z==-4);
}
drivenby { // 021
    x = (true@0b010@0b0001); // (-1)^1 * 2^(0b010-0b011) * 1.0001
    assert(z==-1);
}
// some floats that need to be rounded to nearest even (=x.5)
drivenby { // 022
    x = (false@0b011@0b1000); // (-1)^0 * 2^(0b011-0b011) * 1.1000
    assert(z==2);
}
drivenby { // 023
    x = (false@0b010@0b0000); // (-1)^0 * 2^(0b010-0b011) * 1.0000
    assert(z==0);
}
drivenby { // 024
    x = (true@0b110@0b0001); // (-1)^1 * 2^(0b110-0b011) * 1.0001
    assert(z==-8);
}
drivenby { // 025
    x = (true@0b110@0b0011); // (-1)^1 * 2^(0b110-0b011) * 1.0011
    assert(z==-10);
}