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 the convertion of integer to IEEE 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; module FloatConvertFromInt(int ?x, bv{Width} !z, event !rdy) { int exponent; nat xAbs; if( x == 0 ) { z = posZero; } else { xAbs = abs(x); exponent = ExpBias + MantWidth; if( xAbs >= exp(2,MantWidth+1) ) { bool sticky, round; // Number is to large to fit into mantissa. Rounding might be // necessary. sticky = false; round = false; while( xAbs >= exp(2,MantWidth+1) ) { next(xAbs) = xAbs / 2; next(sticky) = sticky | round; next(round) = (xAbs % 1) == 1; next(exponent) = exponent + 1; pause; } if( (round & sticky) | (round & !sticky & (xAbs % 1)==1 ) ) { if( xAbs == exp(2,MantWidth+1)-1 ) { // rounding would cause overflow? next(xAbs) = exp(2,MantWidth+1); next(exponent) = exponent + 1; } else { next(xAbs) = xAbs + 1; } pause; } if(exponent > ExpMax) { // overflow ? z = ((x>=0) ? posInf : negInf); } else { z = (x<0)@nat2bv(abs(exponent),ExpWidth)@(nat2bv(xAbs,MantWidth+1){-2:0}); } } else { // Need left-shift to get a normalized number. Rounding is not // necessary because the integral completely fits into the mantissa. /* 16 e=7, xAbs=1 e=6, xAbs=2 e=5, xAbs=4 e=4, xAbs=8 e=3, xAbs=16 */ while( xAbs < exp(2,MantWidth) ) { next(xAbs) = xAbs*2; next(exponent) = exponent-1; pause; } z = (x<0)@nat2bv(abs(exponent),ExpWidth)@(nat2bv(xAbs,MantWidth+1){-2:0}); } } emit(rdy); } // x==y ==> z=x=y drivenby { // 000 x = 0; immediate abort { await(false); } when (rdy); assert(z==posZero); } drivenby { // 001 x = 1; immediate abort { await(false); } when (rdy); assert(z==false@false@{true::(ExpWidth-1)}@{false::MantWidth}); } drivenby { // 002 x = -1; immediate abort { await(false); } when (rdy); assert(z==true@false@{true::(ExpWidth-1)}@{false::MantWidth}); } drivenby { // 003 x = 3; immediate abort { await(false); } when (rdy); assert(z==false@false@{true::(ExpWidth-1)}@true@{false::(MantWidth-1)}); } drivenby { // 004 x = -3; immediate abort { await(false); } when (rdy); assert(z==true@false@{true::(ExpWidth-1)}@true@{false::(MantWidth-1)}); } drivenby { // 005 x = +bv2nat(0b1011); immediate abort { await(false); } when (rdy); assert(z==false@0b110@0b0110); } drivenby { // 006 x = +bv2nat(0b101110); immediate abort { await(false); } when (rdy); assert(z==posInf); } drivenby { // 007 x = -bv2nat(0b101110); immediate abort { await(false); } when (rdy); assert(z==negInf); }