package FloatingPoint; import FloatingPoint.FloatCompareGreater; // ************************************************************************** // // // // 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)); /** * FloatCompareNotGreater * * Return false if one or both inputs are NaN. Otherwise, the * function returns not compareGreater */ module FloatCompareNotGreater(bv{Width} ?x, ?y, bool !r) { bool notR; if( isNaN(x) | isNaN(y) ) { r = false; } else { FloatCompareGreater(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==true); } drivenby { // 13 x = posInf; y = (false@0b010@0b0011); assert(r==false); } drivenby { // 14 x = (false@0b010@0b0011); y = negInf; assert(r==false); } drivenby { // 15 x = negInf; y = (false@0b010@0b0011); assert(r==true); } drivenby { // 16 x = posInf; y = posInf; assert(r==true); } drivenby { // 17 x = posInf; y = negInf; assert(r==false); } drivenby { // 18 x = negInf; y = posInf; assert(r==true); } 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==true); } drivenby { // 22 x = (false@0b010@0b0110); y = (true@0b010@0b0110); assert(r==false); } drivenby { // 23 x = (true@0b100@0b0110); y = (true@0b100@0b0110); assert(r==true); }