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)); // isInfinite will be used as a macro. FloatIsInfinite is a simple wrapper to test the macro. module FloatIsInfinite(bv{Width} ?x,bool !r) { r = isInfinite(x); } drivenby { x = posZero; assert(r==false); } drivenby { x = negZero; assert(r==false); } drivenby { x = (false@0b000@0b1000); assert(r==false); } drivenby { x = (true@0b000@0b1000); assert(r==false); } drivenby { x = (false@0b010@0b1000); assert(r==false); } drivenby { x = (true@0b010@0b1000); assert(r==false); } drivenby { x = (false@0b100@0b0000); assert(r==false); } drivenby { x = (true@0b100@0b0000); assert(r==false); } drivenby { x = posInf; assert(r==true); } drivenby { x = negInf; assert(r==true); } drivenby { x = posNaN; assert(r==false); } drivenby { x = negNaN; assert(r==false); }