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 <[email protected]>

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}.

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)
 

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 = {

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