From 21cc706f5a179682a360d01d39d0fb7995f1dec8 Mon Sep 17 00:00:00 2001 From: Pan Li Date: Sun, 22 Dec 2024 16:33:36 +0800 Subject: [PATCH] Float: Introduce no rounding for same exp add * Add no rounding handing for same exp * Add new sub func add_internal * Make sure the code change covered by test. Signed-off-by: Pan Li --- lib/float/arith_internal.sail | 34 ++++++++++++++++--- lib/float/common.sail | 12 +++++++ test/float/add_test.sail | 20 +++++++++++ test/float/data.sail | 64 +++++++++++++++++++++++++++++++++++ 4 files changed, 126 insertions(+), 4 deletions(-) diff --git a/lib/float/arith_internal.sail b/lib/float/arith_internal.sail index 127f18290..9a3cc1c0d 100644 --- a/lib/float/arith_internal.sail +++ b/lib/float/arith_internal.sail @@ -72,6 +72,34 @@ function float_propagate_nan (op_0, op_1) = { ((op | mask), flags) } +val float_add_same_exp_internal : forall 'n, 'n in {16, 32, 64, 128}. + (bits('n), bits('n)) -> (bits('n), fp_exception_flags) +function float_add_same_exp_internal (op_0, op_1) = { + let fp_0 = float_decompose (op_0); + let fp_1 = float_decompose (op_1); + + let bitsize = length (op_0); + let mantissa_0 = sail_zero_extend (fp_0.mantissa, bitsize); + let mantissa_1 = sail_zero_extend (fp_1.mantissa, bitsize); + let mantissa_sum = mantissa_0 + mantissa_1; + + let no_round = is_lowest_zero (mantissa_sum) & not (float_has_max_exp (op_0)); + + if no_round then { + let mantissa_shift = sail_shiftright (mantissa_sum, 1); + let mantissa_bitsize = length (fp_0.mantissa); + + let sign = fp_0.sign; + let exp = fp_0.exp + sail_zero_extend ([bitone], length (fp_0.exp)); + let mantissa = truncate (mantissa_shift, mantissa_bitsize); + + (sign @ exp @ mantissa, fp_eflag_none); + } else { + assert (false, "Not implemented yet."); + (sail_zeros ('n), fp_eflag_none); + } +} + val float_add_same_exp: forall 'n, 'n in {16, 32, 64, 128}. (bits('n), bits('n)) -> (bits('n), fp_exception_flags) function float_add_same_exp (op_0, op_1) = { @@ -90,10 +118,8 @@ function float_add_same_exp (op_0, op_1) = { (op_0, fp_eflag_none) else if is_exp_0_all_ones & not (is_mantissa_all_zeros) then float_propagate_nan (op_0, op_1) - else { - assert (false, "Not implemented yet."); - (sail_zeros ('n), fp_eflag_none); - }; + else + float_add_same_exp_internal (op_0, op_1); } val float_add_internal : forall 'n, 'n in {16, 32, 64, 128}. diff --git a/lib/float/common.sail b/lib/float/common.sail index 47311231c..d1584d9f7 100644 --- a/lib/float/common.sail +++ b/lib/float/common.sail @@ -66,6 +66,18 @@ function float_decompose(op) = { } } +val float_has_max_exp : forall 'n, 'n in { 16, 32, 64, 128 }. bits('n) -> bool +function float_has_max_exp (op) = { + let fp = float_decompose (op); + let bitsize = length (op); + let one = sail_zero_extend ([bitone], bitsize); + let two = sail_shiftleft (one, 1); + let max_exp = sub_bits (sail_shiftleft (one, length (fp.exp)), two); + let has_max = max_exp == sail_zero_extend (fp.exp, bitsize); + + has_max; +} + val not : forall ('p : Bool). bool('p) -> bool(not('p)) function not(b) = not_bool(b) diff --git a/test/float/add_test.sail b/test/float/add_test.sail index 03386b7ce..2448c9988 100644 --- a/test/float/add_test.sail +++ b/test/float/add_test.sail @@ -53,6 +53,11 @@ function test_float_add () -> unit = { assert(float_add (fp16_neg_snan_0, fp16_neg_inf) == (fp16_neg_snan_0 | fp16_neg_qnan_default, fp_eflag_invalid)); assert(float_add (fp16_neg_snan_0, fp16_neg_qnan_0) == (fp16_neg_snan_0 | fp16_neg_qnan_default, fp_eflag_invalid)); + assert(float_add (fp16_pos_normal_add_2_op_0, fp16_pos_normal_add_2_op_1) == (fp16_pos_normal_add_2_sum, fp_eflag_none)); + assert(float_add (fp16_pos_normal_add_3_op_0, fp16_pos_normal_add_3_op_1) == (fp16_pos_normal_add_3_sum, fp_eflag_none)); + assert(float_add (fp16_neg_normal_add_4_op_0, fp16_neg_normal_add_4_op_1) == (fp16_neg_normal_add_4_sum, fp_eflag_none)); + assert(float_add (fp16_neg_normal_add_5_op_0, fp16_neg_normal_add_5_op_1) == (fp16_neg_normal_add_5_sum, fp_eflag_none)); + /* Single floating point */ assert(float_add (fp32_pos_denormal_add_0_op_0, fp32_pos_denormal_add_0_op_1) == (fp32_pos_denormal_add_0_sum, fp_eflag_none)); assert(float_add (fp32_pos_denormal_add_1_op_0, fp32_pos_denormal_add_1_op_1) == (fp32_pos_denormal_add_1_sum, fp_eflag_none)); @@ -91,6 +96,11 @@ function test_float_add () -> unit = { assert(float_add (fp32_neg_snan_0, fp32_neg_inf) == (fp32_neg_snan_0 | fp32_neg_qnan_default, fp_eflag_invalid)); assert(float_add (fp32_neg_snan_0, fp32_neg_qnan_0) == (fp32_neg_snan_0 | fp32_neg_qnan_default, fp_eflag_invalid)); + assert(float_add (fp32_pos_normal_add_2_op_0, fp32_pos_normal_add_2_op_1) == (fp32_pos_normal_add_2_sum, fp_eflag_none)); + assert(float_add (fp32_pos_normal_add_3_op_0, fp32_pos_normal_add_3_op_1) == (fp32_pos_normal_add_3_sum, fp_eflag_none)); + assert(float_add (fp32_neg_normal_add_4_op_0, fp32_neg_normal_add_4_op_1) == (fp32_neg_normal_add_4_sum, fp_eflag_none)); + assert(float_add (fp32_neg_normal_add_5_op_0, fp32_neg_normal_add_5_op_1) == (fp32_neg_normal_add_5_sum, fp_eflag_none)); + /* Double floating point */ assert(float_add (fp64_pos_denormal_add_0_op_0, fp64_pos_denormal_add_0_op_1) == (fp64_pos_denormal_add_0_sum, fp_eflag_none)); assert(float_add (fp64_pos_denormal_add_1_op_0, fp64_pos_denormal_add_1_op_1) == (fp64_pos_denormal_add_1_sum, fp_eflag_none)); @@ -129,6 +139,11 @@ function test_float_add () -> unit = { assert(float_add (fp64_neg_snan_0, fp64_neg_inf) == (fp64_neg_snan_0 | fp64_neg_qnan_default, fp_eflag_invalid)); assert(float_add (fp64_neg_snan_0, fp64_neg_qnan_0) == (fp64_neg_snan_0 | fp64_neg_qnan_default, fp_eflag_invalid)); + assert(float_add (fp64_pos_normal_add_2_op_0, fp64_pos_normal_add_2_op_1) == (fp64_pos_normal_add_2_sum, fp_eflag_none)); + assert(float_add (fp64_pos_normal_add_3_op_0, fp64_pos_normal_add_3_op_1) == (fp64_pos_normal_add_3_sum, fp_eflag_none)); + assert(float_add (fp64_neg_normal_add_4_op_0, fp64_neg_normal_add_4_op_1) == (fp64_neg_normal_add_4_sum, fp_eflag_none)); + assert(float_add (fp64_neg_normal_add_5_op_0, fp64_neg_normal_add_5_op_1) == (fp64_neg_normal_add_5_sum, fp_eflag_none)); + /* Quad floating point */ assert(float_add (fp128_pos_denormal_add_0_op_0, fp128_pos_denormal_add_0_op_1) == (fp128_pos_denormal_add_0_sum, fp_eflag_none)); assert(float_add (fp128_pos_denormal_add_1_op_0, fp128_pos_denormal_add_1_op_1) == (fp128_pos_denormal_add_1_sum, fp_eflag_none)); @@ -166,6 +181,11 @@ function test_float_add () -> unit = { assert(float_add (fp128_neg_snan_0, fp128_neg_qnan_default) == (fp128_neg_snan_0 | fp128_neg_qnan_default, fp_eflag_invalid)); assert(float_add (fp128_neg_snan_0, fp128_neg_inf) == (fp128_neg_snan_0 | fp128_neg_qnan_default, fp_eflag_invalid)); assert(float_add (fp128_neg_snan_0, fp128_neg_qnan_0) == (fp128_neg_snan_0 | fp128_neg_qnan_default, fp_eflag_invalid)); + + assert(float_add (fp128_pos_normal_add_2_op_0, fp128_pos_normal_add_2_op_1) == (fp128_pos_normal_add_2_sum, fp_eflag_none)); + assert(float_add (fp128_pos_normal_add_3_op_0, fp128_pos_normal_add_3_op_1) == (fp128_pos_normal_add_3_sum, fp_eflag_none)); + assert(float_add (fp128_neg_normal_add_4_op_0, fp128_neg_normal_add_4_op_1) == (fp128_neg_normal_add_4_sum, fp_eflag_none)); + assert(float_add (fp128_neg_normal_add_5_op_0, fp128_neg_normal_add_5_op_1) == (fp128_neg_normal_add_5_sum, fp_eflag_none)); } function main () -> unit = { diff --git a/test/float/data.sail b/test/float/data.sail index be3f32e08..4f9aeca30 100644 --- a/test/float/data.sail +++ b/test/float/data.sail @@ -39,6 +39,22 @@ let fp16_pos_normal_1 = 0x71ff let fp16_neg_normal_0 = 0xfa00 let fp16_neg_normal_1 = 0xf1ff +let fp16_pos_normal_add_2_op_0 = 0x04f0 +let fp16_pos_normal_add_2_op_1 = 0x04fe +let fp16_pos_normal_add_2_sum = 0x08f7 + +let fp16_pos_normal_add_3_op_0 = 0x74f1 +let fp16_pos_normal_add_3_op_1 = 0x740f +let fp16_pos_normal_add_3_sum = 0x7880 + +let fp16_neg_normal_add_4_op_0 = 0xf701 +let fp16_neg_normal_add_4_op_1 = 0xf70f +let fp16_neg_normal_add_4_sum = 0xfb08 + +let fp16_neg_normal_add_5_op_0 = 0xc901 +let fp16_neg_normal_add_5_op_1 = 0xc9f1 +let fp16_neg_normal_add_5_sum = 0xcd79 + let fp16_pos_denormal_add_0_op_0 = 0x00ff let fp16_pos_denormal_add_0_op_1 = 0x0021 let fp16_pos_denormal_add_0_sum = 0x0120 @@ -84,6 +100,22 @@ let fp32_pos_normal_1 = 0x0100002f let fp32_neg_normal_0 = 0x9a000000 let fp32_neg_normal_1 = 0x8100002f +let fp32_pos_normal_add_2_op_0 = 0x3ebd70a4 +let fp32_pos_normal_add_2_op_1 = 0x3ebdfff8 +let fp32_pos_normal_add_2_sum = 0x3f3db84e + +let fp32_pos_normal_add_3_op_0 = 0x7efd70a4 +let fp32_pos_normal_add_3_op_1 = 0x7ef00002 +let fp32_pos_normal_add_3_sum = 0x7f76b853 + +let fp32_neg_normal_add_4_op_0 = 0x8901000f +let fp32_neg_normal_add_4_op_1 = 0x89311a2f +let fp32_neg_normal_add_4_sum = 0x89990d1f + +let fp32_neg_normal_add_5_op_0 = 0xf7a70102 +let fp32_neg_normal_add_5_op_1 = 0xf7affff0 +let fp32_neg_normal_add_5_sum = 0xf82b8079 + let fp32_pos_denormal_add_0_op_0 = 0x000fffff let fp32_pos_denormal_add_0_op_1 = 0x00000021 let fp32_pos_denormal_add_0_sum = 0x00100020 @@ -129,6 +161,22 @@ let fp64_pos_normal_1 = 0x0100001111000000 let fp64_neg_normal_0 = 0x9000000000000000 let fp64_neg_normal_1 = 0x8100001111000000 +let fp64_pos_normal_add_2_op_0 = 0x011101238430d021 +let fp64_pos_normal_add_2_op_1 = 0x01110fffffff2321 +let fp64_pos_normal_add_2_sum = 0x01210891c217f9a1 + +let fp64_pos_normal_add_3_op_0 = 0x7efd70a4abcdabcd +let fp64_pos_normal_add_3_op_1 = 0x7efd70000000000b +let fp64_pos_normal_add_3_sum = 0x7f0d705255e6d5eC + +let fp64_neg_normal_add_4_op_0 = 0xf020102030405060 +let fp64_neg_normal_add_4_op_1 = 0xf0201ffffffffff2 +let fp64_neg_normal_add_4_sum = 0xf030181018202829 + +let fp64_neg_normal_add_5_op_0 = 0x8f00abcddeadbeaf +let fp64_neg_normal_add_5_op_1 = 0x8f00000000000001 +let fp64_neg_normal_add_5_sum = 0x8f1055e6ef56df58 + let fp64_pos_denormal_add_0_op_0 = 0x0000ffffffffffff let fp64_pos_denormal_add_0_op_1 = 0x0000000000000041 let fp64_pos_denormal_add_0_sum = 0x0001000000000040 @@ -174,6 +222,22 @@ let fp128_pos_normal_1 = 0x01000011110000000000000000000000 let fp128_neg_normal_0 = 0x90000000000000000000000000000000 let fp128_neg_normal_1 = 0x81000011110000000000000000000000 +let fp128_pos_normal_add_2_op_0 = 0x011101238430d0210000adecd12de823 +let fp128_pos_normal_add_2_op_1 = 0x01110123ffffffffffffffffffffffff +let fp128_pos_normal_add_2_sum = 0x01120123c2186810800056f66896f411 + +let fp128_pos_normal_add_3_op_0 = 0x7efd70a4abcdabcd92042deaedbecde2 +let fp128_pos_normal_add_3_op_1 = 0x7efd70f1111111111112222222222334 +let fp128_pos_normal_add_3_sum = 0x7efe70cade6f5e6f518b280687f0788b + +let fp128_neg_normal_add_4_op_0 = 0xf0201f203040506002003020499290e0 +let fp128_neg_normal_add_4_op_1 = 0xf0201f2ffffffff20000000000122212 +let fp128_neg_normal_add_4_sum = 0xf0211f28182028290100181024d25979 + +let fp128_neg_normal_add_5_op_0 = 0x8f00abfffffffffffffffffffffffffe +let fp128_neg_normal_add_5_op_1 = 0x8f00abc0000000000000000000000000 +let fp128_neg_normal_add_5_sum = 0x8f01abdfffffffffffffffffffffffff + let fp128_pos_denormal_add_0_op_0 = 0x00000fffffffffffffffffffffffffff let fp128_pos_denormal_add_0_op_1 = 0x00000000000000000000000000000091 let fp128_pos_denormal_add_0_sum = 0x00001000000000000000000000000090