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

// 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};
macro isPositive(x) = !Sign(x);
macro isNegative(x) =  Sign(x);


module FloatLes(bv{Width} ?x,?y,event !les) {
    case // define special cases according to IEEE standard
        (isNaN(x))  do les = false;
        (isNaN(y))  do les = false;
        (isInf(x))  do les = isNegative(x);
        (isInf(y))  do les = isPositive(y);
        (isZero(x)) do les = isPositive(y) & !isZero(y);
        (isZero(y)) do les = isNegative(x) & !isZero(x);
    default
        // x and y are (de)normal numbers different to zero
        les = (bv2int(x)<bv2int(y));
}