Skip to content

Commit

Permalink
Add quad floating point to float lib
Browse files Browse the repository at this point in the history
  • Loading branch information
jordancarlin authored and Alasdair committed Jun 21, 2024
1 parent ce27f52 commit d00c025
Show file tree
Hide file tree
Showing 8 changed files with 145 additions and 5 deletions.
19 changes: 14 additions & 5 deletions lib/float/common.sail
Original file line number Diff line number Diff line change
Expand Up @@ -32,8 +32,8 @@ $define _FLOAT_COMMON

/* Floating point types definition */
type fp_exception_flags = bits(5) /* Floating-point exception flags. */
type fp_bits = { 'n, 'n in {16, 32, 64}. bits('n) } /* Floating-point in bits. */
type fp_bits_x2 = { 'n, 'n in {16, 32, 64}. (bits('n), bits('n)) } /* Floating point x2 tuple */
type fp_bits = { 'n, 'n in {16, 32, 64, 128}. bits('n) } /* Floating-point in bits. */
type fp_bits_x2 = { 'n, 'n in {16, 32, 64, 128}. (bits('n), bits('n)) } /* Floating point x2 tuple */
type fp_bool_and_flags = (bool, fp_exception_flags) /* Floating point bool and exception flags tuple */

/* Floating point constants */
Expand All @@ -47,16 +47,20 @@ struct float_bits('n : Int) = {
then 5
else (if 'n == 32
then 8
else 11)),
else (if 'n == 64
then 11
else 15))),
mantissa : bits(if 'n == 16
then 10
else (if 'n == 32
then 23
else 52)),
else (if 'n == 64
then 52
else 112))),
}

/* The val func implementations */
val float_decompose : forall 'n, 'n in { 16, 32, 64 }. bits('n) -> float_bits('n)
val float_decompose : forall 'n, 'n in { 16, 32, 64, 128 }. bits('n) -> float_bits('n)
function float_decompose(op) = {
match 'n {
16 => struct {
Expand All @@ -73,6 +77,11 @@ function float_decompose(op) = {
sign = op[63..63],
exp = op[62..52],
mantissa = op[51..0],
},
128 => struct {
sign = op[127..127],
exp = op[126..112],
mantissa = op[111..0],
}
}
}
Expand Down
14 changes: 14 additions & 0 deletions test/float/eq_test.sail
Original file line number Diff line number Diff line change
Expand Up @@ -75,6 +75,20 @@ function test_float_is_eq () -> unit = {

assert(float_is_eq((0x7ff7000000000000, 0x0000234db0000000)) == (false, fp_eflag_invalid));
assert(float_is_eq((0x7ff0000000000001, 0xfff0000003000001)) == (false, fp_eflag_invalid));

/* Quad floating point */
assert(float_is_eq((0x00000000000000000000000000000001, 0x00000000000000000000000000000001)) == (true, fp_eflag_none));
assert(float_is_eq((0x0f00000000000000000000000000000f, 0x0f00000000000000000000000000000f)) == (true, fp_eflag_none));
assert(float_is_eq((0x80000000000000000000000000000000, 0x00000000000000000000000000000000)) == (true, fp_eflag_none));
assert(float_is_eq((0x7fff0000000000000000000000000000, 0x7fff0000000000000000000000000000)) == (true, fp_eflag_none));

assert(float_is_eq((0x00000000000000000000000000000001, 0x80000000000000000000000000000001)) == (false, fp_eflag_none));
assert(float_is_eq((0x0f00000000000000000000000000000f, 0x3f00000000000000000000000000000f)) == (false, fp_eflag_none));
assert(float_is_eq((0x7fff8000000000000000000000000000, 0x0000234db00000000000000000000000)) == (false, fp_eflag_none));
assert(float_is_eq((0x7fff8000000000000000000000000000, 0xffff8000000000000000000000000000)) == (false, fp_eflag_none));

assert(float_is_eq((0x7fff7000000000000000000000000000, 0x0000234db00000000000000000000000)) == (false, fp_eflag_invalid));
assert(float_is_eq((0x7fff0000000000000000000000000001, 0xfff00000030000000000000000000001)) == (false, fp_eflag_invalid));
}

function main () -> unit = {
Expand Down
11 changes: 11 additions & 0 deletions test/float/inf_test.sail
Original file line number Diff line number Diff line change
Expand Up @@ -65,6 +65,17 @@ function test_float_is_inf () -> unit = {
assert(float_is_inf(0xfff8000000000000) == false);
assert(float_is_inf(0xfff0000000000001) == false);
assert(float_is_inf(0xffc0000000000000) == false);

/* Quad floating point */
assert(float_is_inf(0x7fff0000000000000000000000000000));
assert(float_is_inf(0xffff0000000000000000000000000000));

assert(float_is_inf(0x7fff8000000000000000000000000000) == false);
assert(float_is_inf(0x7fff0000000000000000000000000001) == false);
assert(float_is_inf(0x7ffc0000000000000000000000000000) == false);
assert(float_is_inf(0xffff8000000000000000000000000000) == false);
assert(float_is_inf(0xffff0000000000000000000000000001) == false);
assert(float_is_inf(0xfffc0000000000000000000000000000) == false);
}

function main () -> unit = {
Expand Down
41 changes: 41 additions & 0 deletions test/float/nan_test.sail
Original file line number Diff line number Diff line change
Expand Up @@ -86,6 +86,24 @@ function test_float_is_nan () -> unit = {
assert(float_is_nan(0xfff0000000000000) == false);
assert(float_is_nan(0xffe0000000000000) == false);
assert(float_is_nan(0xffc0000000000000) == false);

/* Quad floating point */
assert(float_is_nan(0x7fff8000000000000000000000000000));
assert(float_is_nan(0x7fff0000000000000000000000000001));
assert(float_is_nan(0x7fff8000000000000000000000000100));
assert(float_is_nan(0x7fffc000000000001000000000000000));

assert(float_is_nan(0xffff8000000000000000000000000000));
assert(float_is_nan(0xffff0000000000000000000000000001));
assert(float_is_nan(0xffff8000000000000000000000000100));
assert(float_is_nan(0xffffc000000000001000000000000000));

assert(float_is_nan(0x7fff0000000000000000000000000000) == false);
assert(float_is_nan(0x7ffe0000000000000000000000000000) == false);
assert(float_is_nan(0x7ffc0000000000000000000000000000) == false);
assert(float_is_nan(0xffff0000000000000000000000000000) == false);
assert(float_is_nan(0xfffe0000000000000000000000000000) == false);
assert(float_is_nan(0xfffc0000000000000000000000000000) == false);
}

function test_float_is_snan () -> unit = {
Expand Down Expand Up @@ -121,6 +139,18 @@ function test_float_is_snan () -> unit = {
assert(float_is_snan(0x7ff8000000000000) == false);
assert(float_is_snan(0xfff8000000000000) == false);
assert(float_is_snan(0xfef8000000000001) == false);

/* Quad floating point */
assert(float_is_snan(0x7fff7000000000000000000000000000));
assert(float_is_snan(0x7fff7000000000000000000000000001));

assert(float_is_snan(0xffff7000000000000000000000000000));
assert(float_is_snan(0xffff7000000000000000000000000001));

assert(float_is_snan(0x7fff8000000000000000000000000000) == false);
assert(float_is_snan(0xffff8000000000000000000000000000) == false);
assert(float_is_snan(0xfeff8000000000000000000000000001) == false);

}

function test_float_is_qnan () -> unit = {
Expand Down Expand Up @@ -156,6 +186,17 @@ function test_float_is_qnan () -> unit = {
assert(float_is_qnan(0x7ff7000000000000) == false);
assert(float_is_qnan(0xfff7000000000000) == false);
assert(float_is_qnan(0xfef7000000000001) == false);

/* Quad floating point */
assert(float_is_qnan(0x7fff8000000000000000000000000000));
assert(float_is_qnan(0x7fff8000000000000000000000000001));

assert(float_is_qnan(0xffff8000000000000000000000000000));
assert(float_is_qnan(0xffff8000000000000000000000000001));

assert(float_is_qnan(0x7fff7000000000000000000000000000) == false);
assert(float_is_qnan(0xffff7000000000000000000000000000) == false);
assert(float_is_qnan(0xfeff7000000000000000000000000001) == false);
}

function main () -> unit = {
Expand Down
14 changes: 14 additions & 0 deletions test/float/ne_test.sail
Original file line number Diff line number Diff line change
Expand Up @@ -75,6 +75,20 @@ function test_float_is_ne () -> unit = {

assert(float_is_ne((0x7ff7000000000000, 0x0000234db0000000)) == (false, fp_eflag_invalid));
assert(float_is_ne((0x7ff0000000000001, 0xfff0000003000001)) == (false, fp_eflag_invalid));

/* Quad floating point */
assert(float_is_ne((0x80000000000000000000000000000001, 0x00000000000000000000000000000001)) == (true, fp_eflag_none));
assert(float_is_ne((0x8f00000000000000000000000000000f, 0x0f00000000000000000000000000000f)) == (true, fp_eflag_none));
assert(float_is_ne((0x80000000000000000000000000000000, 0x00000000000000000000000000000001)) == (true, fp_eflag_none));
assert(float_is_ne((0x7fff0000000000000000000000000000, 0xffff0000000000000000000000000000)) == (true, fp_eflag_none));

assert(float_is_ne((0x00000000000000000000000000000011, 0x00000000000000000000000000000011)) == (false, fp_eflag_none));
assert(float_is_ne((0x0ffff00000000000000000000000000f, 0x0ffff00000000000000000000000000f)) == (false, fp_eflag_none));
assert(float_is_ne((0x00000000000000000000000000000000, 0x80000000000000000000000000000000)) == (false, fp_eflag_none));
assert(float_is_ne((0x7fff8000000000000000000000000100, 0x7fff8000000000000000000000000100)) == (false, fp_eflag_none));

assert(float_is_ne((0x7fff7000000000000000000000000000, 0x0000000000000234db00000000000000)) == (false, fp_eflag_invalid));
assert(float_is_ne((0x7fff0000000000000000000000000001, 0xffff0000000000000000000003000001)) == (false, fp_eflag_invalid));
}

function main () -> unit = {
Expand Down
22 changes: 22 additions & 0 deletions test/float/normal_test.sail
Original file line number Diff line number Diff line change
Expand Up @@ -65,6 +65,17 @@ function test_float_is_normal () -> unit = {
assert(float_is_normal(0x7ff0000000000000) == false);
assert(float_is_normal(0x0008000000000000) == false);
assert(float_is_normal(0x8008000000000000) == false);

/* Quad floating point */
assert(float_is_normal(0x7ffe0000000000000000000000000000));
assert(float_is_normal(0x7ffe0000000000000000000000000001));
assert(float_is_normal(0xfffc000000000000000000000000000f));
assert(float_is_normal(0x80030000000000000001000000000000));

assert(float_is_normal(0x7fff8000000000000000000000000000) == false);
assert(float_is_normal(0x7fff0000000000000000000000000000) == false);
assert(float_is_normal(0x00008000000000000000000000000000) == false);
assert(float_is_normal(0x80008000000000000000000000000000) == false);
}

function test_float_is_denormal () -> unit = {
Expand Down Expand Up @@ -100,6 +111,17 @@ function test_float_is_denormal () -> unit = {
assert(float_is_denormal(0x7ff0000000000000) == false);
assert(float_is_denormal(0xffc000000000000f) == false);
assert(float_is_denormal(0x8030000000100000) == false);

/* Quad floating point */
assert(float_is_denormal(0x00008000000000000000000000000000));
assert(float_is_denormal(0x80008000000000000000000000000000));
assert(float_is_denormal(0x80000000000000000000000000000001));
assert(float_is_denormal(0x80008000000000000001000000000000));

assert(float_is_denormal(0x7fff8000000000000000000000000000) == false);
assert(float_is_denormal(0x7fff0000000000000000000000000000) == false);
assert(float_is_denormal(0xfffc000000000000000000000000000f) == false);
assert(float_is_denormal(0x80030000000000000001000000000000) == false);
}

function main () -> unit = {
Expand Down
20 changes: 20 additions & 0 deletions test/float/sign_test.sail
Original file line number Diff line number Diff line change
Expand Up @@ -62,6 +62,16 @@ function test_float_is_positive () -> unit = {
assert(float_is_positive(0xf8f0000000023000) == false);
assert(float_is_positive(0xfce0000000000000) == false);
assert(float_is_positive(0xe8c0000000000000) == false);

/* Quad floating point */
assert(float_is_positive(0x7ff080000f0f00000000000000000000));
assert(float_is_positive(0x0000000000000fedc000000000000001));
assert(float_is_positive(0x7fffffffffffffffffffffffffffffff));
assert(float_is_positive(0x00000000003000000000010000000000));

assert(float_is_positive(0xf8ff0000000000000023000000000000) == false);
assert(float_is_positive(0xffce0000000000000000000000000000) == false);
assert(float_is_positive(0xe88c0000000000000000000000000000) == false);
}

function test_float_is_negative () -> unit = {
Expand Down Expand Up @@ -94,6 +104,16 @@ function test_float_is_negative () -> unit = {
assert(float_is_negative(0x78f0000000023000) == false);
assert(float_is_negative(0x7ce0000000000000) == false);
assert(float_is_negative(0x68c0000000000000) == false);

/* Quad floating point */
assert(float_is_negative(0xfff0000000800000000f0f0000000000));
assert(float_is_negative(0x8000000000000fedc000000000000001));
assert(float_is_negative(0xffffffffffffffffffffffffffffffff));
assert(float_is_negative(0x80000000003000000000010000000000));

assert(float_is_negative(0x78ff0000000000000000023000000000) == false);
assert(float_is_negative(0x7fce0000000000000000000000000000) == false);
assert(float_is_negative(0x688c0000000000000000000000000000) == false);
}

function main () -> unit = {
Expand Down
9 changes: 9 additions & 0 deletions test/float/zero_test.sail
Original file line number Diff line number Diff line change
Expand Up @@ -59,6 +59,15 @@ function test_float_is_zero () -> unit = {
assert(float_is_zero(0x7ff0000000000001) == false);
assert(float_is_zero(0xfff8000000000000) == false);
assert(float_is_zero(0xfff0000000000001) == false);

/* Quad floating point */
assert(float_is_zero(0x80000000000000000000000000000000));
assert(float_is_zero(0x00000000000000000000000000000000));

assert(float_is_zero(0x7fff8000000000000000000000000000) == false);
assert(float_is_zero(0x7fff0000000000000000000000000001) == false);
assert(float_is_zero(0xffff8000000000000000000000000000) == false);
assert(float_is_zero(0xffff0000000000000000000000000001) == false);
}

function main () -> unit = {
Expand Down

0 comments on commit d00c025

Please sign in to comment.