package FloatingPoint;





// ************************************************************************** //
//                                                                            //
//    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 logarithm of floating point numbers that conform    //
// with IEEE 754-2008 standard using a look-up table for the mantissa.        //
// 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));


// here comes the main module: it first deals with special cases like NaN, Zero and Infinities
// according to the IEEE standard and then (in the largest part of case construct) handles
// normal and denormal numbers

module FloatLog(bv{Width} ?x,!z,event !rdy) {
    // Actually, bv{Width-2} is sufficient for table entries:
    // Reason: we pre-compute the log(x) for 1 <= x < 2, which
    // is 0 <= log(x) < 1
    // <==> 0b0 00..00 00...00 <= log(x) < 0b0 011..11 00..00
    [MantMax+1]bv{Width} logtable;

    int e;
    bv{MantWidth}   m;
    bv{Width}       ml;
    bv{Width}       et;
    event rdy1, rdy2;

    // START OF auto-generated log table
    logtable[0] = false@0b000@0b0000;   // logtable_map[1.000000] = 0.000000
    logtable[1] = false@0b000@0b0011;   // logtable_map[1.062500] = 0.060625
    logtable[2] = false@0b000@0b0111;   // logtable_map[1.125000] = 0.117783
    logtable[3] = false@0b000@0b1011;   // logtable_map[1.187500] = 0.171850
    logtable[4] = false@0b000@0b1110;   // logtable_map[1.250000] = 0.223144
    logtable[5] = false@0b001@0b0001;   // logtable_map[1.312500] = 0.271934
    logtable[6] = false@0b001@0b0100;   // logtable_map[1.375000] = 0.318454
    logtable[7] = false@0b001@0b0111;   // logtable_map[1.437500] = 0.362906
    logtable[8] = false@0b001@0b1010;   // logtable_map[1.500000] = 0.405465
    logtable[9] = false@0b001@0b1101;   // logtable_map[1.562500] = 0.446287
    logtable[10] = false@0b001@0b1111;   // logtable_map[1.625000] = 0.485508
    logtable[11] = false@0b010@0b0001;   // logtable_map[1.687500] = 0.523248
    logtable[12] = false@0b010@0b0010;   // logtable_map[1.750000] = 0.559616
    logtable[13] = false@0b010@0b0011;   // logtable_map[1.812500] = 0.594707
    logtable[14] = false@0b010@0b0100;   // logtable_map[1.875000] = 0.628609
    logtable[15] = false@0b010@0b0101;   // logtable_map[1.937500] = 0.661398
    // END OF auto-generation    

    case // define special cases according to IEEE standard
        (isNaN(x)) do {
            z = x;
        }
        (isZero(x)) do {
            // How IEEE likes to have it:
            z = negInf;
        }
        (isSignMinus(x)) do {
            // How the intel does it:
            z = posNaN;
            // How IEEE likes to have it:
            //z = negNaN;
        }
    default {
        m = Mant(x);
        e = ValExp(Exp(x));
        if(isSubnormal(x)) {
            // Shift mantissa left to get a 1xxxx, where xxxx represent MantWidth bits.
            while(!m{-1}) {
                next(m) = m{-2:0}@false;
                next(e) = e - 1;
                pause;
            }
            // MSB is now '1'. We need to shift one more time to move out that bit
            // to get the same format as mantissa without the hidden bit.
            next(m) = m{-2:0}@false;
            next(e) = e - 1;
            pause;
        }
        ml = logtable[bv2nat(m)];

        FloatConvertFromInt(e,et,rdy1);
        FloatAdd(ml,et,z,rdy2);
    }
    emit(rdy);
}
// ---------------------------------------------
// Cover special cases
drivenby { // 0
    x = posNaN;
    immediate abort { await(false); } when (rdy);
    assert(z == posNaN);
}
drivenby { // 1
    x = negNaN;
    immediate abort { await(false); } when (rdy);
    assert(z == negNaN);
}
drivenby { // 2
    x = posZero;
    immediate abort { await(false); } when (rdy);
    assert(z == negInf);
}
drivenby { // 3
    x = negZero;
    immediate abort { await(false); } when (rdy);
    assert(z == negInf);
}
drivenby { // 4
    x = true@0b011@0b0110;
    immediate abort { await(false); } when (rdy);
    assert(z == posNaN);
}
drivenby { // 5
    x = true@0b101@0b0100;
    immediate abort { await(false); } when (rdy);
    assert(z == posNaN);
}
// ---------------------------------------------
// Cover default case: actual logarithm
// auto-generated test cases
drivenby { // case 6
  x = (true@0b100@0b1001);
  // log(x) = z
  // -3.1250000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 7
  x = (true@0b101@0b1111);
  // log(x) = z
  // -7.7500000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 8
  x = (false@0b000@0b0100);
  // log(x) = z
  // 0.0625000 = -2.7725887298583984375000
  // (-1)^(1) * 2^(4 - 3) * 10110 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b100@0b0110));
}
drivenby { // case 9
  x = (true@0b010@0b1011);
  // log(x) = z
  // -0.8437500 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 10
  x = (false@0b001@0b0011);
  // log(x) = z
  // 0.2968750 = -1.2144441604614257812500
  // (-1)^(1) * 2^(3 - 3) * 10011 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b011@0b0011));
}
drivenby { // case 11
  x = (false@0b000@0b0001);
  // log(x) = z
  // 0.0156250 = -4.1588830947875976562500
  // (-1)^(1) * 2^(5 - 3) * 10000 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b101@0b0001));
}
drivenby { // case 12
  x = (false@0b100@0b1011);
  // log(x) = z
  // 3.3750000 = 1.2163953781127929687500
  // (-1)^(0) * 2^(3 - 3) * 10011 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b0011));
}
drivenby { // case 13
  x = (false@0b011@0b1101);
  // log(x) = z
  // 1.8125000 = 0.5947071313858032226562
  // (-1)^(0) * 2^(2 - 3) * 10011 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b010@0b0011));
}
drivenby { // case 14
  x = (false@0b010@0b1110);
  // log(x) = z
  // 0.9375000 = -0.0645385235548019409180
  // (-1)^(1) * 2^(-1 - 3) * 10000 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b0100));
}
drivenby { // case 15
  x = (true@0b001@0b1111);
  // log(x) = z
  // -0.4843750 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 16
  x = (true@0b000@0b0011);
  // log(x) = z
  // -0.0468750 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 17
  x = (false@0b101@0b0111);
  // log(x) = z
  // 5.7500000 = 1.7491998672485351562500
  // (-1)^(0) * 2^(3 - 3) * 11011 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b1100));
}
drivenby { // case 18
  x = (true@0b100@0b0011);
  // log(x) = z
  // -2.3750000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 19
  x = (false@0b011@0b1101);
  // log(x) = z
  // 1.8125000 = 0.5947071313858032226562
  // (-1)^(0) * 2^(2 - 3) * 10011 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b010@0b0011));
}
drivenby { // case 20
  x = (true@0b101@0b1000);
  // log(x) = z
  // -6.0000000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 21
  x = (true@0b010@0b0100);
  // log(x) = z
  // -0.6250000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 22
  x = (true@0b000@0b0110);
  // log(x) = z
  // -0.0937500 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 23
  x = (false@0b001@0b0100);
  // log(x) = z
  // 0.3125000 = -1.1631507873535156250000
  // (-1)^(1) * 2^(3 - 3) * 10010 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b011@0b0011));
}
drivenby { // case 24
  x = (false@0b011@0b1110);
  // log(x) = z
  // 1.8750000 = 0.6286086440086364746094
  // (-1)^(0) * 2^(2 - 3) * 10100 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b010@0b0100));
}
drivenby { // case 25
  x = (false@0b100@0b0001);
  // log(x) = z
  // 2.1250000 = 0.7537717819213867187500
  // (-1)^(0) * 2^(2 - 3) * 11000 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b010@0b1000));
}
drivenby { // case 26
  x = (true@0b011@0b1100);
  // log(x) = z
  // -1.7500000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 27
  x = (true@0b010@0b1001);
  // log(x) = z
  // -0.7812500 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 28
  x = (false@0b011@0b0001);
  // log(x) = z
  // 1.0625000 = 0.0606246218085289001465
  // (-1)^(0) * 2^(-2 - 3) * 11111 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b0011));
}
drivenby { // case 29
  x = (true@0b000@0b0011);
  // log(x) = z
  // -0.0468750 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 30
  x = (false@0b011@0b1110);
  // log(x) = z
  // 1.8750000 = 0.6286086440086364746094
  // (-1)^(0) * 2^(2 - 3) * 10100 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b010@0b0100));
}
drivenby { // case 31
  x = (true@0b010@0b1100);
  // log(x) = z
  // -0.8750000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 32
  x = (true@0b010@0b1111);
  // log(x) = z
  // -0.9687500 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 33
  x = (false@0b000@0b0101);
  // log(x) = z
  // 0.0781250 = -2.5494451522827148437500
  // (-1)^(1) * 2^(4 - 3) * 10100 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b100@0b0100));
}
drivenby { // case 34
  x = (false@0b000@0b1101);
  // log(x) = z
  // 0.2031250 = -1.5939337015151977539062
  // (-1)^(1) * 2^(3 - 3) * 11001 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b011@0b1010));
}
drivenby { // case 35
  x = (true@0b010@0b1111);
  // log(x) = z
  // -0.9687500 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 36
  x = (false@0b000@0b0110);
  // log(x) = z
  // 0.0937500 = -2.3671236038208007812500
  // (-1)^(1) * 2^(4 - 3) * 10010 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b100@0b0011));
}
drivenby { // case 37
  x = (false@0b001@0b1100);
  // log(x) = z
  // 0.4375000 = -0.8266785740852355957031
  // (-1)^(1) * 2^(2 - 3) * 11010 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b010@0b1010));
}
drivenby { // case 38
  x = (false@0b000@0b1111);
  // log(x) = z
  // 0.2343750 = -1.4508328437805175781250
  // (-1)^(1) * 2^(3 - 3) * 10111 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b011@0b0111));
}
drivenby { // case 39
  x = (true@0b011@0b1010);
  // log(x) = z
  // -1.6250000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 40
  x = (false@0b100@0b1011);
  // log(x) = z
  // 3.3750000 = 1.2163953781127929687500
  // (-1)^(0) * 2^(3 - 3) * 10011 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b0011));
}
drivenby { // case 41
  x = (true@0b101@0b0110);
  // log(x) = z
  // -5.5000000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 42
  x = (true@0b000@0b1110);
  // log(x) = z
  // -0.2187500 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 43
  x = (false@0b001@0b1000);
  // log(x) = z
  // 0.3750000 = -0.9808292388916015625000
  // (-1)^(1) * 2^(2 - 3) * 11111 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b010@0b1111));
}
drivenby { // case 44
  x = (false@0b001@0b1001);
  // log(x) = z
  // 0.3906250 = -0.9400072693824768066406
  // (-1)^(1) * 2^(2 - 3) * 11110 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b010@0b1110));
}
drivenby { // case 45
  x = (true@0b100@0b1011);
  // log(x) = z
  // -3.3750000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 46
  x = (false@0b011@0b1111);
  // log(x) = z
  // 1.9375000 = 0.6613984704017639160156
  // (-1)^(0) * 2^(2 - 3) * 10101 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b010@0b0101));
}
drivenby { // case 47
  x = (true@0b011@0b1011);
  // log(x) = z
  // -1.6875000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 48
  x = (true@0b101@0b0101);
  // log(x) = z
  // -5.2500000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 49
  x = (true@0b011@0b0000);
  // log(x) = z
  // -1.0000000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 50
  x = (true@0b011@0b1010);
  // log(x) = z
  // -1.6250000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 51
  x = (true@0b100@0b1011);
  // log(x) = z
  // -3.3750000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 52
  x = (true@0b010@0b1000);
  // log(x) = z
  // -0.7500000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 53
  x = (true@0b010@0b1101);
  // log(x) = z
  // -0.9062500 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 54
  x = (true@0b101@0b1110);
  // log(x) = z
  // -7.5000000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 55
  x = (false@0b100@0b1011);
  // log(x) = z
  // 3.3750000 = 1.2163953781127929687500
  // (-1)^(0) * 2^(3 - 3) * 10011 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b0011));
}
drivenby { // case 56
  x = (false@0b011@0b0100);
  // log(x) = z
  // 1.2500000 = 0.2231435477733612060547
  // (-1)^(0) * 2^(0 - 3) * 11100 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b1110));
}
drivenby { // case 57
  x = (true@0b010@0b0101);
  // log(x) = z
  // -0.6562500 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 58
  x = (false@0b011@0b1001);
  // log(x) = z
  // 1.5625000 = 0.4462870955467224121094
  // (-1)^(0) * 2^(1 - 3) * 11100 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b001@0b1101));
}
drivenby { // case 59
  x = (true@0b101@0b0000);
  // log(x) = z
  // -4.0000000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 60
  x = (false@0b010@0b0001);
  // log(x) = z
  // 0.5312500 = -0.6325225830078125000000
  // (-1)^(1) * 2^(2 - 3) * 10100 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b010@0b0100));
}
drivenby { // case 61
  x = (false@0b001@0b1100);
  // log(x) = z
  // 0.4375000 = -0.8266785740852355957031
  // (-1)^(1) * 2^(2 - 3) * 11010 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b010@0b1010));
}
drivenby { // case 62
  x = (false@0b100@0b1100);
  // log(x) = z
  // 3.5000000 = 1.2527629137039184570312
  // (-1)^(0) * 2^(3 - 3) * 10100 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b0100));
}
drivenby { // case 63
  x = (false@0b101@0b0000);
  // log(x) = z
  // 4.0000000 = 1.3862943649291992187500
  // (-1)^(0) * 2^(3 - 3) * 10110 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b0110));
}
drivenby { // case 64
  x = (true@0b011@0b0011);
  // log(x) = z
  // -1.1875000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 65
  x = (true@0b011@0b0000);
  // log(x) = z
  // -1.0000000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 66
  x = (false@0b101@0b0101);
  // log(x) = z
  // 5.2500000 = 1.6582280397415161132812
  // (-1)^(0) * 2^(3 - 3) * 11010 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b1011));
}
drivenby { // case 67
  x = (false@0b101@0b1111);
  // log(x) = z
  // 7.7500000 = 2.0476927757263183593750
  // (-1)^(0) * 2^(4 - 3) * 10000 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b100@0b0000));
}
drivenby { // case 68
  x = (false@0b001@0b1010);
  // log(x) = z
  // 0.4062500 = -0.9007865190505981445312
  // (-1)^(1) * 2^(2 - 3) * 11100 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b010@0b1101));
}
drivenby { // case 69
  x = (true@0b101@0b0101);
  // log(x) = z
  // -5.2500000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 70
  x = (true@0b001@0b1010);
  // log(x) = z
  // -0.4062500 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 71
  x = (false@0b011@0b0011);
  // log(x) = z
  // 1.1875000 = 0.1718502640724182128906
  // (-1)^(0) * 2^(0 - 3) * 10101 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b1011));
}
drivenby { // case 72
  x = (false@0b011@0b1000);
  // log(x) = z
  // 1.5000000 = 0.4054650962352752685547
  // (-1)^(0) * 2^(1 - 3) * 11001 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b001@0b1010));
}
drivenby { // case 73
  x = (false@0b001@0b0011);
  // log(x) = z
  // 0.2968750 = -1.2144441604614257812500
  // (-1)^(1) * 2^(3 - 3) * 10011 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b011@0b0011));
}
drivenby { // case 74
  x = (true@0b010@0b1110);
  // log(x) = z
  // -0.9375000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 75
  x = (false@0b100@0b0010);
  // log(x) = z
  // 2.2500000 = 0.8109301924705505371094
  // (-1)^(0) * 2^(2 - 3) * 11001 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b010@0b1010));
}
drivenby { // case 76
  x = (false@0b000@0b1100);
  // log(x) = z
  // 0.1875000 = -1.6739764213562011718750
  // (-1)^(1) * 2^(3 - 3) * 11010 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b011@0b1011));
}
drivenby { // case 77
  x = (true@0b101@0b0100);
  // log(x) = z
  // -5.0000000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 78
  x = (false@0b011@0b1110);
  // log(x) = z
  // 1.8750000 = 0.6286086440086364746094
  // (-1)^(0) * 2^(2 - 3) * 10100 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b010@0b0100));
}
drivenby { // case 79
  x = (true@0b010@0b1011);
  // log(x) = z
  // -0.8437500 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 80
  x = (false@0b101@0b1100);
  // log(x) = z
  // 7.0000000 = 1.9459100961685180664062
  // (-1)^(0) * 2^(3 - 3) * 11111 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b1111));
}
drivenby { // case 81
  x = (false@0b101@0b1011);
  // log(x) = z
  // 6.7500000 = 1.9095425605773925781250
  // (-1)^(0) * 2^(3 - 3) * 11110 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b1111));
}
drivenby { // case 82
  x = (false@0b100@0b0101);
  // log(x) = z
  // 2.6250000 = 0.9650809168815612792969
  // (-1)^(0) * 2^(2 - 3) * 11110 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b010@0b1111));
}
drivenby { // case 83
  x = (false@0b000@0b1000);
  // log(x) = z
  // 0.1250000 = -2.0794415473937988281250
  // (-1)^(1) * 2^(4 - 3) * 10000 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b100@0b0001));
}
drivenby { // case 84
  x = (true@0b011@0b1011);
  // log(x) = z
  // -1.6875000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 85
  x = (false@0b010@0b0011);
  // log(x) = z
  // 0.5937500 = -0.5212969183921813964844
  // (-1)^(1) * 2^(2 - 3) * 10000 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b010@0b0001));
}
drivenby { // case 86
  x = (false@0b000@0b1001);
  // log(x) = z
  // 0.1406250 = -1.9616584777832031250000
  // (-1)^(1) * 2^(3 - 3) * 11111 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b011@0b1111));
}
drivenby { // case 87
  x = (true@0b100@0b0000);
  // log(x) = z
  // -2.0000000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 88
  x = (false@0b100@0b1111);
  // log(x) = z
  // 3.8750000 = 1.3545457124710083007812
  // (-1)^(0) * 2^(3 - 3) * 10101 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b0110));
}
drivenby { // case 89
  x = (false@0b011@0b1001);
  // log(x) = z
  // 1.5625000 = 0.4462870955467224121094
  // (-1)^(0) * 2^(1 - 3) * 11100 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b001@0b1101));
}
drivenby { // case 90
  x = (true@0b000@0b0111);
  // log(x) = z
  // -0.1093750 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 91
  x = (true@0b000@0b1000);
  // log(x) = z
  // -0.1250000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 92
  x = (false@0b000@0b0101);
  // log(x) = z
  // 0.0781250 = -2.5494451522827148437500
  // (-1)^(1) * 2^(4 - 3) * 10100 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b100@0b0100));
}
drivenby { // case 93
  x = (true@0b010@0b1000);
  // log(x) = z
  // -0.7500000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 94
  x = (false@0b010@0b1100);
  // log(x) = z
  // 0.8750000 = -0.1335313916206359863281
  // (-1)^(1) * 2^(0 - 3) * 10001 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b1000));
}
drivenby { // case 95
  x = (true@0b000@0b1100);
  // log(x) = z
  // -0.1875000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 96
  x = (false@0b000@0b0110);
  // log(x) = z
  // 0.0937500 = -2.3671236038208007812500
  // (-1)^(1) * 2^(4 - 3) * 10010 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b100@0b0011));
}
drivenby { // case 97
  x = (true@0b011@0b1110);
  // log(x) = z
  // -1.8750000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 98
  x = (false@0b101@0b1101);
  // log(x) = z
  // 7.2500000 = 1.9810014963150024414062
  // (-1)^(0) * 2^(3 - 3) * 11111 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b100@0b0000));
}
drivenby { // case 99
  x = (true@0b011@0b0010);
  // log(x) = z
  // -1.1250000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 100
  x = (true@0b010@0b0100);
  // log(x) = z
  // -0.6250000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 101
  x = (true@0b001@0b1101);
  // log(x) = z
  // -0.4531250 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 102
  x = (true@0b100@0b1111);
  // log(x) = z
  // -3.8750000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 103
  x = (true@0b001@0b0100);
  // log(x) = z
  // -0.3125000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 104
  x = (false@0b001@0b1110);
  // log(x) = z
  // 0.4687500 = -0.7576857209205627441406
  // (-1)^(1) * 2^(2 - 3) * 11000 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b010@0b1000));
}
drivenby { // case 105
  x = (false@0b010@0b1100);
  // log(x) = z
  // 0.8750000 = -0.1335313916206359863281
  // (-1)^(1) * 2^(0 - 3) * 10001 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b1000));
}
drivenby { // case 106
  x = (false@0b010@0b0000);
  // log(x) = z
  // 0.5000000 = -0.6931471824645996093750
  // (-1)^(1) * 2^(2 - 3) * 10110 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b010@0b0110));
}
drivenby { // case 107
  x = (false@0b000@0b0001);
  // log(x) = z
  // 0.0156250 = -4.1588830947875976562500
  // (-1)^(1) * 2^(5 - 3) * 10000 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b101@0b0001));
}
drivenby { // case 108
  x = (true@0b000@0b1101);
  // log(x) = z
  // -0.2031250 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 109
  x = (false@0b101@0b0100);
  // log(x) = z
  // 5.0000000 = 1.6094379425048828125000
  // (-1)^(0) * 2^(3 - 3) * 11001 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b1010));
}
drivenby { // case 110
  x = (false@0b100@0b1011);
  // log(x) = z
  // 3.3750000 = 1.2163953781127929687500
  // (-1)^(0) * 2^(3 - 3) * 10011 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b0011));
}
drivenby { // case 111
  x = (true@0b010@0b1010);
  // log(x) = z
  // -0.8125000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 112
  x = (false@0b101@0b1110);
  // log(x) = z
  // 7.5000000 = 2.0149030685424804687500
  // (-1)^(0) * 2^(4 - 3) * 10000 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b100@0b0000));
}
drivenby { // case 113
  x = (true@0b001@0b1100);
  // log(x) = z
  // -0.4375000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 114
  x = (true@0b001@0b0011);
  // log(x) = z
  // -0.2968750 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 115
  x = (true@0b011@0b0000);
  // log(x) = z
  // -1.0000000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 116
  x = (true@0b001@0b0100);
  // log(x) = z
  // -0.3125000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 117
  x = (true@0b101@0b0100);
  // log(x) = z
  // -5.0000000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 118
  x = (true@0b010@0b0000);
  // log(x) = z
  // -0.5000000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 119
  x = (false@0b000@0b0100);
  // log(x) = z
  // 0.0625000 = -2.7725887298583984375000
  // (-1)^(1) * 2^(4 - 3) * 10110 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b100@0b0110));
}
drivenby { // case 120
  x = (false@0b101@0b0100);
  // log(x) = z
  // 5.0000000 = 1.6094379425048828125000
  // (-1)^(0) * 2^(3 - 3) * 11001 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b1010));
}
drivenby { // case 121
  x = (true@0b000@0b1010);
  // log(x) = z
  // -0.1562500 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 122
  x = (false@0b000@0b1100);
  // log(x) = z
  // 0.1875000 = -1.6739764213562011718750
  // (-1)^(1) * 2^(3 - 3) * 11010 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b011@0b1011));
}
drivenby { // case 123
  x = (false@0b001@0b1001);
  // log(x) = z
  // 0.3906250 = -0.9400072693824768066406
  // (-1)^(1) * 2^(2 - 3) * 11110 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b010@0b1110));
}
drivenby { // case 124
  x = (false@0b001@0b0000);
  // log(x) = z
  // 0.2500000 = -1.3862943649291992187500
  // (-1)^(1) * 2^(3 - 3) * 10110 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b011@0b0110));
}
drivenby { // case 125
  x = (false@0b010@0b1001);
  // log(x) = z
  // 0.7812500 = -0.2468600720167160034180
  // (-1)^(1) * 2^(0 - 3) * 11111 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b001@0b0000));
}
drivenby { // case 126
  x = (false@0b010@0b1100);
  // log(x) = z
  // 0.8750000 = -0.1335313916206359863281
  // (-1)^(1) * 2^(0 - 3) * 10001 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b1000));
}
drivenby { // case 127
  x = (false@0b101@0b0101);
  // log(x) = z
  // 5.2500000 = 1.6582280397415161132812
  // (-1)^(0) * 2^(3 - 3) * 11010 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b1011));
}
drivenby { // case 128
  x = (true@0b100@0b0100);
  // log(x) = z
  // -2.5000000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 129
  x = (true@0b010@0b0100);
  // log(x) = z
  // -0.6250000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 130
  x = (true@0b101@0b1001);
  // log(x) = z
  // -6.2500000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 131
  x = (false@0b000@0b1011);
  // log(x) = z
  // 0.1718750 = -1.7609877586364746093750
  // (-1)^(1) * 2^(3 - 3) * 11100 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b011@0b1100));
}
drivenby { // case 132
  x = (false@0b100@0b1011);
  // log(x) = z
  // 3.3750000 = 1.2163953781127929687500
  // (-1)^(0) * 2^(3 - 3) * 10011 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b0011));
}
drivenby { // case 133
  x = (false@0b001@0b0101);
  // log(x) = z
  // 0.3281250 = -1.1143606901168823242188
  // (-1)^(1) * 2^(3 - 3) * 10001 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b011@0b0010));
}
drivenby { // case 134
  x = (true@0b001@0b1000);
  // log(x) = z
  // -0.3750000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 135
  x = (true@0b001@0b0010);
  // log(x) = z
  // -0.2812500 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 136
  x = (false@0b011@0b0000);
  // log(x) = z
  // 1.0000000 = 0.0000000000000000000000
  // (-1)^(0) * 2^(3 - 3) * 00000 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b0000));
}
drivenby { // case 137
  x = (false@0b100@0b0010);
  // log(x) = z
  // 2.2500000 = 0.8109301924705505371094
  // (-1)^(0) * 2^(2 - 3) * 11001 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b010@0b1010));
}
drivenby { // case 138
  x = (false@0b001@0b1010);
  // log(x) = z
  // 0.4062500 = -0.9007865190505981445312
  // (-1)^(1) * 2^(2 - 3) * 11100 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b010@0b1101));
}
drivenby { // case 139
  x = (false@0b000@0b1010);
  // log(x) = z
  // 0.1562500 = -1.8562979698181152343750
  // (-1)^(1) * 2^(3 - 3) * 11101 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b011@0b1110));
}
drivenby { // case 140
  x = (false@0b000@0b0011);
  // log(x) = z
  // 0.0468750 = -3.0602707862854003906250
  // (-1)^(1) * 2^(4 - 3) * 11000 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b100@0b1000));
}
drivenby { // case 141
  x = (false@0b000@0b1100);
  // log(x) = z
  // 0.1875000 = -1.6739764213562011718750
  // (-1)^(1) * 2^(3 - 3) * 11010 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b011@0b1011));
}
drivenby { // case 142
  x = (true@0b010@0b0111);
  // log(x) = z
  // -0.7187500 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 143
  x = (true@0b001@0b0000);
  // log(x) = z
  // -0.2500000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 144
  x = (false@0b000@0b1111);
  // log(x) = z
  // 0.2343750 = -1.4508328437805175781250
  // (-1)^(1) * 2^(3 - 3) * 10111 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b011@0b0111));
}
drivenby { // case 145
  x = (false@0b010@0b1001);
  // log(x) = z
  // 0.7812500 = -0.2468600720167160034180
  // (-1)^(1) * 2^(0 - 3) * 11111 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b001@0b0000));
}
drivenby { // case 146
  x = (false@0b000@0b1110);
  // log(x) = z
  // 0.2187500 = -1.5198256969451904296875
  // (-1)^(1) * 2^(3 - 3) * 11000 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b011@0b1000));
}
drivenby { // case 147
  x = (true@0b101@0b1110);
  // log(x) = z
  // -7.5000000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 148
  x = (true@0b001@0b0011);
  // log(x) = z
  // -0.2968750 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 149
  x = (true@0b101@0b1100);
  // log(x) = z
  // -7.0000000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 150
  x = (false@0b011@0b0000);
  // log(x) = z
  // 1.0000000 = 0.0000000000000000000000
  // (-1)^(0) * 2^(3 - 3) * 00000 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b0000));
}
drivenby { // case 151
  x = (false@0b001@0b0100);
  // log(x) = z
  // 0.3125000 = -1.1631507873535156250000
  // (-1)^(1) * 2^(3 - 3) * 10010 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b011@0b0011));
}
drivenby { // case 152
  x = (true@0b011@0b1100);
  // log(x) = z
  // -1.7500000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 153
  x = (false@0b010@0b0001);
  // log(x) = z
  // 0.5312500 = -0.6325225830078125000000
  // (-1)^(1) * 2^(2 - 3) * 10100 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b010@0b0100));
}
drivenby { // case 154
  x = (false@0b010@0b1100);
  // log(x) = z
  // 0.8750000 = -0.1335313916206359863281
  // (-1)^(1) * 2^(0 - 3) * 10001 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b1000));
}
drivenby { // case 155
  x = (true@0b010@0b1100);
  // log(x) = z
  // -0.8750000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 156
  x = (false@0b010@0b1010);
  // log(x) = z
  // 0.8125000 = -0.2076393663883209228516
  // (-1)^(1) * 2^(0 - 3) * 11010 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b1101));
}
drivenby { // case 157
  x = (true@0b001@0b0011);
  // log(x) = z
  // -0.2968750 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 158
  x = (true@0b010@0b1100);
  // log(x) = z
  // -0.8750000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 159
  x = (true@0b010@0b1001);
  // log(x) = z
  // -0.7812500 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 160
  x = (true@0b000@0b1111);
  // log(x) = z
  // -0.2343750 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 161
  x = (true@0b101@0b0110);
  // log(x) = z
  // -5.5000000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 162
  x = (true@0b010@0b0111);
  // log(x) = z
  // -0.7187500 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 163
  x = (true@0b000@0b0110);
  // log(x) = z
  // -0.0937500 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 164
  x = (true@0b000@0b0110);
  // log(x) = z
  // -0.0937500 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 165
  x = (true@0b101@0b1111);
  // log(x) = z
  // -7.7500000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 166
  x = (true@0b100@0b0110);
  // log(x) = z
  // -2.7500000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 167
  x = (true@0b101@0b0001);
  // log(x) = z
  // -4.2500000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 168
  x = (true@0b100@0b0100);
  // log(x) = z
  // -2.5000000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 169
  x = (true@0b101@0b1000);
  // log(x) = z
  // -6.0000000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 170
  x = (true@0b100@0b0010);
  // log(x) = z
  // -2.2500000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 171
  x = (false@0b011@0b1001);
  // log(x) = z
  // 1.5625000 = 0.4462870955467224121094
  // (-1)^(0) * 2^(1 - 3) * 11100 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b001@0b1101));
}
drivenby { // case 172
  x = (false@0b010@0b0101);
  // log(x) = z
  // 0.6562500 = -0.4212134778499603271484
  // (-1)^(1) * 2^(1 - 3) * 11010 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b001@0b1011));
}
drivenby { // case 173
  x = (false@0b000@0b1110);
  // log(x) = z
  // 0.2187500 = -1.5198256969451904296875
  // (-1)^(1) * 2^(3 - 3) * 11000 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b011@0b1000));
}
drivenby { // case 174
  x = (true@0b101@0b0001);
  // log(x) = z
  // -4.2500000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 175
  x = (true@0b000@0b0000);
  // log(x) = z
  // -0.0000000 = -inf
  // -inf
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b111@0b0000));
}
drivenby { // case 176
  x = (false@0b011@0b0101);
  // log(x) = z
  // 1.3125000 = 0.2719337046146392822266
  // (-1)^(0) * 2^(1 - 3) * 10001 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b001@0b0001));
}
drivenby { // case 177
  x = (false@0b000@0b0101);
  // log(x) = z
  // 0.0781250 = -2.5494451522827148437500
  // (-1)^(1) * 2^(4 - 3) * 10100 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b100@0b0100));
}
drivenby { // case 178
  x = (false@0b101@0b1110);
  // log(x) = z
  // 7.5000000 = 2.0149030685424804687500
  // (-1)^(0) * 2^(4 - 3) * 10000 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b100@0b0000));
}
drivenby { // case 179
  x = (false@0b011@0b0110);
  // log(x) = z
  // 1.3750000 = 0.3184537291526794433594
  // (-1)^(0) * 2^(1 - 3) * 10100 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b001@0b0100));
}
drivenby { // case 180
  x = (false@0b100@0b1100);
  // log(x) = z
  // 3.5000000 = 1.2527629137039184570312
  // (-1)^(0) * 2^(3 - 3) * 10100 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b0100));
}
drivenby { // case 181
  x = (false@0b000@0b1001);
  // log(x) = z
  // 0.1406250 = -1.9616584777832031250000
  // (-1)^(1) * 2^(3 - 3) * 11111 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b011@0b1111));
}
drivenby { // case 182
  x = (false@0b010@0b1010);
  // log(x) = z
  // 0.8125000 = -0.2076393663883209228516
  // (-1)^(1) * 2^(0 - 3) * 11010 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b1101));
}
drivenby { // case 183
  x = (true@0b000@0b0001);
  // log(x) = z
  // -0.0156250 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 184
  x = (true@0b100@0b1011);
  // log(x) = z
  // -3.3750000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 185
  x = (false@0b101@0b0001);
  // log(x) = z
  // 4.2500000 = 1.4469189643859863281250
  // (-1)^(0) * 2^(3 - 3) * 10111 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b0111));
}
drivenby { // case 186
  x = (true@0b001@0b0000);
  // log(x) = z
  // -0.2500000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 187
  x = (false@0b000@0b0001);
  // log(x) = z
  // 0.0156250 = -4.1588830947875976562500
  // (-1)^(1) * 2^(5 - 3) * 10000 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b101@0b0001));
}
drivenby { // case 188
  x = (false@0b010@0b1100);
  // log(x) = z
  // 0.8750000 = -0.1335313916206359863281
  // (-1)^(1) * 2^(0 - 3) * 10001 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b1000));
}
drivenby { // case 189
  x = (true@0b010@0b1001);
  // log(x) = z
  // -0.7812500 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 190
  x = (true@0b010@0b0011);
  // log(x) = z
  // -0.5937500 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 191
  x = (true@0b010@0b1001);
  // log(x) = z
  // -0.7812500 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 192
  x = (true@0b100@0b0010);
  // log(x) = z
  // -2.2500000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 193
  x = (false@0b100@0b0100);
  // log(x) = z
  // 2.5000000 = 0.9162907600402832031250
  // (-1)^(0) * 2^(2 - 3) * 11101 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b010@0b1101));
}
drivenby { // case 194
  x = (false@0b011@0b1110);
  // log(x) = z
  // 1.8750000 = 0.6286086440086364746094
  // (-1)^(0) * 2^(2 - 3) * 10100 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b010@0b0100));
}
drivenby { // case 195
  x = (false@0b001@0b1101);
  // log(x) = z
  // 0.4531250 = -0.7915872335433959960938
  // (-1)^(1) * 2^(2 - 3) * 11001 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b010@0b1001));
}
drivenby { // case 196
  x = (true@0b001@0b0001);
  // log(x) = z
  // -0.2656250 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 197
  x = (false@0b101@0b1111);
  // log(x) = z
  // 7.7500000 = 2.0476927757263183593750
  // (-1)^(0) * 2^(4 - 3) * 10000 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b100@0b0000));
}
drivenby { // case 198
  x = (true@0b010@0b1001);
  // log(x) = z
  // -0.7812500 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 199
  x = (true@0b011@0b0011);
  // log(x) = z
  // -1.1875000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 200
  x = (true@0b000@0b1010);
  // log(x) = z
  // -0.1562500 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}
drivenby { // case 201
  x = (false@0b011@0b0001);
  // log(x) = z
  // 1.0625000 = 0.0606246218085289001465
  // (-1)^(0) * 2^(-2 - 3) * 11111 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b0011));
}
drivenby { // case 202
  x = (false@0b001@0b0010);
  // log(x) = z
  // 0.2812500 = -1.2685112953186035156250
  // (-1)^(1) * 2^(3 - 3) * 10100 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b011@0b0100));
}
drivenby { // case 203
  x = (false@0b101@0b1100);
  // log(x) = z
  // 7.0000000 = 1.9459100961685180664062
  // (-1)^(0) * 2^(3 - 3) * 11111 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b1111));
}
drivenby { // case 204
  x = (false@0b101@0b1101);
  // log(x) = z
  // 7.2500000 = 1.9810014963150024414062
  // (-1)^(0) * 2^(3 - 3) * 11111 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b100@0b0000));
}
drivenby { // case 205
  x = (true@0b011@0b0110);
  // log(x) = z
  // -1.3750000 = nan
  // nan
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b111@0b1111));
}