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); }