// ************************************************************************** //
//                                                                            //
//    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;
}