// ************************************************************************** // // // // 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 decoding of IEEE-like floating point numbers. // // Thus, it essentially provides macros for that purpose, while the Quartz // // module will only enumerate all possible values and decodes them. // // ************************************************************************** // // parameters of the floating-point format macro MantWidth = 23; macro ExpWidth = 8; macro ExpMax = exp(2,ExpWidth)-1; macro ExpBias = ExpMax/2; macro Width = 1+ExpWidth+MantWidth; // 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}; // 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}; // special values (independent of their sign) macro isZero(x) = Exp(x)=={false::ExpWidth} & Mant(x)=={false::MantWidth}; macro isDenormal(x) = Exp(x)=={false::ExpWidth} & Mant(x)!={false::MantWidth}; macro isNormal(x) = Exp(x)!={ true::ExpWidth} & Exp(x)!={false::ExpWidth}; macro isInf(x) = Exp(x)=={ true::ExpWidth} & Mant(x)=={false::MantWidth}; macro isNaN(x) = Exp(x)=={ true::ExpWidth} & Mant(x)!={false::MantWidth}; macro isNumber(x) = Exp(x)!={ true::ExpWidth}; module FloatConstants() { bv{Width} MinDenormal, MaxDenormal, MinNormal, MaxNormal, Infinity; real rMinDenormal, rMaxDenormal, rMinNormal, rMaxNormal, rInfinity; MinDenormal = false@{false::ExpWidth}@{false::MantWidth-1}@true; MaxDenormal = false@{false::ExpWidth}@{true::MantWidth}; MinNormal = false@{false::ExpWidth-1}@true@{false::MantWidth}; MaxNormal = false@{true::ExpWidth-1}@false@{true::MantWidth}; Infinity = false@{true::ExpWidth}@{false::MantWidth}; rMinDenormal = Float2Real(MinDenormal); rMaxDenormal = Float2Real(MaxDenormal); rMinNormal = Float2Real(MinNormal); rMaxNormal = Float2Real(MaxNormal); rInfinity = Float2Real(Infinity); } drivenby { nothing; }