package FloatingPoint; import FloatingPoint.FloatCompareGreater; import FloatingPoint.FloatCompareQuietEqual; // ************************************************************************** // // // // 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)); module FloatCompareGreaterEqual(bv{Width} ?x, ?y, bool !r) { bool cqe, cg; if( isNaN(x) | isNaN(y) ) { r = false; } else { FloatCompareQuietEqual(x,y,cqe); FloatCompareGreater(x,y,cg); r = cqe | cg; } } // --------- all combinations of zero-zero --------- drivenby { // 0 x = (false@0b000@0b0000); y = (false@0b000@0b0000); assert(r==true); } drivenby { // 1 x = (true@0b000@0b0000); y = (false@0b000@0b0000); assert(r==true); } drivenby { // 2 x = (false@0b000@0b0000); y = (true@0b000@0b0000); assert(r==true); } drivenby { // 3 x = (true@0b000@0b0000); y = (true@0b000@0b0000); assert(r==true); } // --------- subnormal / denormal numbers --------- drivenby { // 4 x = (false@0b000@0b0000); y = (false@0b000@0b0000); assert(r==true); } drivenby { // 5 x = (false@0b000@0b0001); y = (false@0b000@0b0000); assert(r==true); } drivenby { // 6 x = (false@0b000@0b0000); y = (false@0b000@0b0001); assert(r==false); } drivenby { // 7 x = (false@0b000@0b1100); y = (false@0b000@0b0110); assert(r==true); } drivenby { // 8 x = (true@0b000@0b0000); y = (true@0b000@0b0000); assert(r==true); } drivenby { // 9 x = (true@0b000@0b0001); y = (true@0b000@0b0000); assert(r==false); } drivenby { // 10 x = (true@0b000@0b0000); y = (true@0b000@0b0001); assert(r==true); } drivenby { // 11 x = (true@0b000@0b1100); y = (true@0b000@0b0110); assert(r==false); } // --------- positive normal numbers - same exponent --------- drivenby { // 12 x = (false@0b010@0b1100); y = (false@0b010@0b1100); assert(r==true); } drivenby { // 13 x = (false@0b010@0b1100); y = (false@0b010@0b0100); assert(r==true); } drivenby { // 14 x = (false@0b010@0b0100); y = (false@0b010@0b1100); assert(r==false); } drivenby { // 15 x = (false@0b010@0b1100); y = (false@0b010@0b1100); assert(r==true); } // --------- negative normal numbers - varying exponent --------- drivenby { // 16 x = (false@0b001@0b0011); y = (false@0b010@0b1100); assert(r==false); } drivenby { // 17 x = (false@0b011@0b1100); y = (false@0b010@0b1100); assert(r==true); } drivenby { // 18 x = (false@0b010@0b1100); y = (false@0b011@0b1100); assert(r==false); } drivenby { // 19 x = (false@0b011@0b1100); y = (false@0b001@0b0011); assert(r==true); } // --------- normal numbers - varying sign --------- drivenby { // 20 x = (false@0b010@0b1100); y = (true@0b010@0b1100); assert(r==true); } drivenby { // 21 x = (false@0b001@0b0010); y = (true@0b010@0b1100); assert(r==true); } drivenby { // 22 x = (true@0b001@0b0010); y = (false@0b010@0b1100); assert(r==false); } drivenby { // 23 x = (false@0b110@0b1100); y = (true@0b011@0b1100); assert(r==true); } drivenby { // 24 x = (true@0b011@0b1000); y = (false@0b110@0b0011); assert(r==false); }