From 5aa4989f89bb2ff90c621129f0394a4c265c28b3 Mon Sep 17 00:00:00 2001 From: KotorinMinami Date: Fri, 4 Jul 2025 15:31:31 +0800 Subject: [PATCH] add float_sub_internal implement --- lib/float/add.sail | 5 +++- lib/float/arith_internal.sail | 52 +++++++++++++++++++++++++++++++++-- lib/float/common.sail | 8 ++++++ test/float/add_test.sail | 4 +++ test/float/data.sail | 16 +++++++++++ 5 files changed, 82 insertions(+), 3 deletions(-) diff --git a/lib/float/add.sail b/lib/float/add.sail index 353ab3b8e..f04f7727a 100644 --- a/lib/float/add.sail +++ b/lib/float/add.sail @@ -21,7 +21,10 @@ function float_add (op_0, op_1) = { let (sum, flags) = if same_sign then float_add_internal (op_0, op_1) - else float_sub_internal (op_0, op_1); + else { + let fp_1 = float_decompose (op_1); + float_sub_internal (op_0, not_vec(fp_1.sign) @ fp_1.exp @ fp_1.mantissa); + }; (sum, flags); } diff --git a/lib/float/arith_internal.sail b/lib/float/arith_internal.sail index 7c038077e..4ca3bea0b 100644 --- a/lib/float/arith_internal.sail +++ b/lib/float/arith_internal.sail @@ -226,11 +226,59 @@ function float_add_internal (op_0, op_1) = { } } +val float_sub_same_exp_internal : forall 'n, 'n in {16, 32, 64, 128}. (bits('n), bits('n)) + -> (bits('n), fp_exception_flags) +function float_sub_same_exp_internal (op_0, op_1) = { + let fp_0 = float_decompose (op_0); + let fp_1 = float_decompose (op_1); + + let mantissa = sub_bits (fp_0.mantissa, fp_1.mantissa); + let shift_bitsize = count_leading_zeros (mantissa) + 1; + let mantissa_shift = sail_shiftleft (mantissa, shift_bitsize); + let exp = sub_bits_int (fp_0.exp, shift_bitsize); + + (fp_0.sign @ exp @ mantissa_shift, fp_eflag_none) +} + +val float_sub_same_exp: forall 'n, 'n in {16, 32, 64, 128}. + (bits('n), bits('n)) -> (bits('n), fp_exception_flags) +function float_sub_same_exp (op_0, op_1) = { + let bitsize = length (op_0); + let fp_0 = float_decompose (op_0); + let fp_1 = float_decompose (op_1); + + assert (fp_0.exp == fp_1.exp, "The exp of floating point must be same."); + if is_all_ones(fp_0.exp) then { + assert(false, "Not implemented yet."); + (sail_zeros ('n), fp_eflag_none); + } + else { + if unsigned (fp_0.mantissa) > unsigned (fp_1.mantissa) then + float_sub_same_exp_internal (op_0, op_1) + else if unsigned (fp_0.mantissa) < unsigned (fp_1.mantissa) then + float_sub_same_exp_internal (not_vec(fp_1.sign) @ fp_1.exp @ fp_1.mantissa, op_0) + else { + assert (false, "Not implemented yet."); + (sail_zeros ('n), fp_eflag_none); + } + } +} + val float_sub_internal : forall 'n, 'n in {16, 32, 64, 128}. (bits('n), bits('n)) -> (bits('n), fp_exception_flags) function float_sub_internal (op_0, op_1) = { - assert (false, "Not implemented yet."); - (sail_zeros ('n), fp_eflag_none); + let fp_0 = float_decompose (op_0); + let fp_1 = float_decompose (op_1); + + assert (xor_vec (fp_0.sign, fp_1.sign) == [bitzero], + "The sign of float sub operand 0 and operand 1 must be the same."); + + if fp_0.exp == fp_1.exp then + float_sub_same_exp (op_0, op_1) + else { + assert (false, "Not implemented yet."); + (sail_zeros ('n), fp_eflag_none); + } } $endif diff --git a/lib/float/common.sail b/lib/float/common.sail index 2320fc832..2f506b0ef 100644 --- a/lib/float/common.sail +++ b/lib/float/common.sail @@ -119,4 +119,12 @@ function is_highest_zero (op) = op['n - 1] == bitzero val is_all_zeros : forall 'n, 0 < 'n. bits('n) -> bool function is_all_zeros (op) = op == sail_zeros ('n) +val sub_bits_int = { + ocaml: "sub_vec_int", + interpreter: "sub_vec_int", + lem: "sub_vec_int", + c: "sub_bits_int", + coq: "sub_vec_int" +} : forall 'n. (bits('n), int) -> bits('n) + $endif diff --git a/test/float/add_test.sail b/test/float/add_test.sail index fe8f3d98b..bef23816f 100644 --- a/test/float/add_test.sail +++ b/test/float/add_test.sail @@ -58,6 +58,7 @@ function test_float_add () -> unit = { 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)); + assert(float_add (fp16_pos_normal_add_14_op_0, fp16_neg_normal_add_14_op_1) == (fp16_pos_normal_add_14_sum, fp_eflag_none)); float_set_rounding (fp_rounding_rne); @@ -156,6 +157,7 @@ function test_float_add () -> unit = { 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)); + assert(float_add (fp32_pos_normal_add_14_op_0, fp32_neg_normal_add_14_op_1) == (fp32_pos_normal_add_14_sum, fp_eflag_none)); float_set_rounding (fp_rounding_rne); @@ -254,6 +256,7 @@ function test_float_add () -> unit = { 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)); + assert(float_add (fp64_pos_normal_add_14_op_0, fp64_neg_normal_add_14_op_1) == (fp64_pos_normal_add_14_sum, fp_eflag_none)); float_set_rounding (fp_rounding_rne); @@ -352,6 +355,7 @@ function test_float_add () -> unit = { 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)); + assert(float_add (fp128_pos_normal_add_14_op_0, fp128_neg_normal_add_14_op_1) == (fp128_pos_normal_add_14_sum, fp_eflag_none)); float_set_rounding (fp_rounding_rne); diff --git a/test/float/data.sail b/test/float/data.sail index 6fedc038b..73491c811 100644 --- a/test/float/data.sail +++ b/test/float/data.sail @@ -119,6 +119,10 @@ let fp16_neg_normal_add_13_sum_rdn = 0xfb81 let fp16_neg_normal_add_13_sum_rup = 0xfb80 let fp16_neg_normal_add_13_sum_rtz = 0xfb80 +let fp16_pos_normal_add_14_op_0 = 0x4980 +let fp16_neg_normal_add_14_op_1 = 0xCA00 +let fp16_pos_normal_add_14_sum = 0xBC00 + 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 @@ -244,6 +248,10 @@ let fp32_neg_normal_add_13_sum_rdn = 0xff7ff878 let fp32_neg_normal_add_13_sum_rup = 0xff7ff877 let fp32_neg_normal_add_13_sum_rtz = 0xff7ff877 +let fp32_pos_normal_add_14_op_0 = 0x42600000 +let fp32_neg_normal_add_14_op_1 = 0xC2400000 +let fp32_pos_normal_add_14_sum = 0x41000000 + 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 @@ -369,6 +377,10 @@ let fp64_neg_normal_add_13_sum_rdn = 0xffe00107fffffffe let fp64_neg_normal_add_13_sum_rup = 0xffe00107fffffffd let fp64_neg_normal_add_13_sum_rtz = 0xffe00107fffffffd +let fp64_pos_normal_add_14_op_0 = 0x41D8000000000000 +let fp64_neg_normal_add_14_op_1 = 0xC1D4000000000000 +let fp64_pos_normal_add_14_sum = 0x41B0000000000000 + 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 @@ -494,6 +506,10 @@ let fp128_neg_normal_add_13_sum_rdn = 0xfffe000000068ff892110a7feeef1d3e let fp128_neg_normal_add_13_sum_rup = 0xfffe000000068ff892110a7feeef1d3d let fp128_neg_normal_add_13_sum_rtz = 0xfffe000000068ff892110a7feeef1d3d +let fp128_pos_normal_add_14_op_0 = 0x43E79000000000000000000000000000 +let fp128_neg_normal_add_14_op_1 = 0xC3E78800000000000000000000000000 +let fp128_pos_normal_add_14_sum = 0x43E20000000000000000000000000000 + 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