add float_sub_internal implement

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);
 }
 

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

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

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);
 

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