// ************************************************************************** // // // // 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. To // // this end, 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 = 4; macro ExpWidth = 3; 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 Float2RealTable(bv{Width} z,real rz,event rdy) { for(j=0..exp(2,Width-1)-1) { z = false@nat2bv(j,Width-1); rz = Float2Real(z); pause; } emit(rdy); } drivenby { await(rdy); }