Float: Introduce nan propagation for same exp add (#778)

* Add nan propagation when ops has same exp.
* Refine the high level layout of add.
* Add assertion for sub function.
* Make sure the nan propagation covered by test.

Signed-off-by: Pan Li <[email protected]>

lib/float/arith_internal.sail

@@ -58,25 +58,59 @@ val      float_is_ge_internal : fp_bits_x2 -> bool
 function float_is_ge_internal ((op_0, op_1))
   = not (float_is_lt_internal ((op_0, op_1)))
 
+val      float_propagate_nan : forall 'n, 'n in {16, 32, 64, 128}.
+  (bits('n), bits('n)) -> (bits('n), fp_exception_flags)
+function float_propagate_nan (op_0, op_1) = {
+  let is_snan = float_is_snan (op_0) | float_is_snan (op_1);
+  let flags = if is_snan then fp_eflag_invalid else fp_eflag_none;
+
+  let one = sail_zero_extend ([bitone], length (op_0));
+  let fp_0 = float_decompose (op_0);
+  let mask = sail_shiftleft (one, length (fp_0.mantissa) - 1);
+  let op = if float_is_nan (op_0) then op_0 else op_1;
+
+  ((op | mask), flags)
+}
+
+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) = {
+  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.");
+
+  let is_exp_0_all_ones = is_all_ones (fp_0.exp);
+  let is_mantissa_all_zeros = is_all_zeros (fp_0.mantissa | fp_1.mantissa);
+
+  if is_all_zeros (fp_0.exp) then
+    (op_0 + sail_zero_extend (fp_1.mantissa, bitsize), fp_eflag_none)
+  else if is_exp_0_all_ones & is_mantissa_all_zeros then
+    (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);
+  };
+}
+
 val      float_add_internal : forall 'n, 'n in {16, 32, 64, 128}.
   (bits('n), bits('n)) -> (bits('n), fp_exception_flags)
 function float_add_internal (op_0, op_1) = {
   let fp_0 = float_decompose (op_0);
   let fp_1 = float_decompose (op_1);
-  let exp_diff = sub_bits (fp_0.exp, fp_1.exp);
-  let zero_exp_diff = is_all_zeros (exp_diff);
 
-  let bitsize = length (op_0);
-  let sum = if zero_exp_diff & is_all_zeros (fp_0.exp)
-            then op_0 + sail_zero_extend (fp_1.mantissa, bitsize)
-            else if is_all_ones (fp_0.exp)
-                 then op_0
-            else {
-              assert (false, "Not implemented yet.");
-              sail_zeros ('n);
-            };
-
-  (sum, fp_eflag_none);
+  assert (xor_vec (fp_0.sign, fp_1.sign) == [bitzero],
+    "The sign of float add operand 0 and operand 1 must be the same.");
+
+  if fp_0.exp == fp_1.exp then
+    float_add_same_exp (op_0, op_1)
+  else {
+    assert (false, "Not implemented yet.");
+    (sail_zeros ('n), fp_eflag_none);
+  }
 }
 
 val      float_sub_internal : forall 'n, 'n in {16, 32, 64, 128}.

test/float/add_test.sail

@@ -22,8 +22,36 @@ function test_float_add () -> unit = {
   assert(float_add (fp16_neg_denormal_add_1_op_0, fp16_neg_denormal_add_1_op_1) == (fp16_neg_denormal_add_1_sum, fp_eflag_none));
 
   assert(float_add (fp16_pos_inf, fp16_pos_inf) == (fp16_pos_inf, fp_eflag_none));
-  assert(float_add (fp16_pos_inf, fp16_pos_denormal_1) == (fp16_pos_inf, fp_eflag_none));
-  assert(float_add (fp16_pos_inf, fp16_pos_normal_0) == (fp16_pos_inf, fp_eflag_none));
+  assert(float_add (fp16_pos_inf, fp16_pos_qnan_default) == (fp16_pos_qnan_default, fp_eflag_none));
+  assert(float_add (fp16_pos_inf, fp16_pos_qnan_0) == (fp16_pos_qnan_0 | fp16_pos_qnan_default, fp_eflag_none));
+  assert(float_add (fp16_pos_inf, fp16_pos_snan_0) == (fp16_pos_snan_0 | fp16_pos_qnan_default, fp_eflag_invalid));
+
+  assert(float_add (fp16_neg_inf, fp16_neg_inf) == (fp16_neg_inf, fp_eflag_none));
+  assert(float_add (fp16_neg_inf, fp16_neg_qnan_default) == (fp16_neg_qnan_default, fp_eflag_none));
+  assert(float_add (fp16_neg_inf, fp16_neg_qnan_0) == (fp16_neg_qnan_0 | fp16_neg_qnan_default, fp_eflag_none));
+  assert(float_add (fp16_neg_inf, fp16_neg_snan_0) == (fp16_neg_snan_0 | fp16_neg_qnan_default, fp_eflag_invalid));
+
+  assert(float_add (fp16_pos_qnan_0, fp16_pos_qnan_1) == (fp16_pos_qnan_0 | fp16_pos_qnan_default, fp_eflag_none));
+  assert(float_add (fp16_pos_qnan_0, fp16_pos_qnan_default) == (fp16_pos_qnan_0 | fp16_pos_qnan_default, fp_eflag_none));
+  assert(float_add (fp16_pos_qnan_0, fp16_pos_inf) == (fp16_pos_qnan_0 | fp16_pos_qnan_default, fp_eflag_none));
+  assert(float_add (fp16_pos_qnan_0, fp16_pos_snan_0) == (fp16_pos_qnan_0 | fp16_pos_qnan_default, fp_eflag_invalid));
+
+  assert(float_add (fp16_neg_qnan_0, fp16_neg_qnan_1) == (fp16_neg_qnan_0 | fp16_neg_qnan_default, fp_eflag_none));
+  assert(float_add (fp16_neg_qnan_0, fp16_neg_qnan_default) == (fp16_neg_qnan_0 | fp16_neg_qnan_default, fp_eflag_none));
+  assert(float_add (fp16_neg_qnan_0, fp16_neg_inf) == (fp16_neg_qnan_0 | fp16_neg_qnan_default, fp_eflag_none));
+  assert(float_add (fp16_neg_qnan_0, fp16_neg_snan_0) == (fp16_neg_qnan_0 | fp16_neg_qnan_default, fp_eflag_invalid));
+
+  assert(float_add (fp16_pos_snan_0, fp16_pos_snan_1) == (fp16_pos_snan_0 | fp16_pos_qnan_default, fp_eflag_invalid));
+  assert(float_add (fp16_pos_snan_0, fp16_pos_qnan_0) == (fp16_pos_snan_0 | fp16_pos_qnan_default, fp_eflag_invalid));
+  assert(float_add (fp16_pos_snan_0, fp16_pos_qnan_default) == (fp16_pos_snan_0 | fp16_pos_qnan_default, fp_eflag_invalid));
+  assert(float_add (fp16_pos_snan_0, fp16_pos_inf) == (fp16_pos_snan_0 | fp16_pos_qnan_default, fp_eflag_invalid));
+  assert(float_add (fp16_pos_snan_0, fp16_pos_qnan_0) == (fp16_pos_snan_0 | fp16_pos_qnan_default, fp_eflag_invalid));
+
+  assert(float_add (fp16_neg_snan_0, fp16_neg_snan_1) == (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_neg_snan_0, fp16_neg_qnan_default) == (fp16_neg_snan_0 | fp16_neg_qnan_default, fp_eflag_invalid));
+  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));
 
   /* 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));
@@ -32,8 +60,36 @@ function test_float_add () -> unit = {
   assert(float_add (fp32_neg_denormal_add_1_op_0, fp32_neg_denormal_add_1_op_1) == (fp32_neg_denormal_add_1_sum, fp_eflag_none));
 
   assert(float_add (fp32_pos_inf, fp32_pos_inf) == (fp32_pos_inf, fp_eflag_none));
-  assert(float_add (fp32_pos_inf, fp32_pos_denormal_1) == (fp32_pos_inf, fp_eflag_none));
-  assert(float_add (fp32_pos_inf, fp32_pos_normal_0) == (fp32_pos_inf, fp_eflag_none));
+  assert(float_add (fp32_pos_inf, fp32_pos_qnan_default) == (fp32_pos_qnan_default, fp_eflag_none));
+  assert(float_add (fp32_pos_inf, fp32_pos_qnan_0) == (fp32_pos_qnan_0 | fp32_pos_qnan_default, fp_eflag_none));
+  assert(float_add (fp32_pos_inf, fp32_pos_snan_0) == (fp32_pos_snan_0 | fp32_pos_qnan_default, fp_eflag_invalid));
+
+  assert(float_add (fp32_neg_inf, fp32_neg_inf) == (fp32_neg_inf, fp_eflag_none));
+  assert(float_add (fp32_neg_inf, fp32_neg_qnan_default) == (fp32_neg_qnan_default, fp_eflag_none));
+  assert(float_add (fp32_neg_inf, fp32_neg_qnan_0) == (fp32_neg_qnan_0 | fp32_neg_qnan_default, fp_eflag_none));
+  assert(float_add (fp32_neg_inf, fp32_neg_snan_0) == (fp32_neg_snan_0 | fp32_neg_qnan_default, fp_eflag_invalid));
+
+  assert(float_add (fp32_pos_qnan_0, fp32_pos_qnan_1) == (fp32_pos_qnan_0 | fp32_pos_qnan_default, fp_eflag_none));
+  assert(float_add (fp32_pos_qnan_0, fp32_pos_qnan_default) == (fp32_pos_qnan_0 | fp32_pos_qnan_default, fp_eflag_none));
+  assert(float_add (fp32_pos_qnan_0, fp32_pos_inf) == (fp32_pos_qnan_0 | fp32_pos_qnan_default, fp_eflag_none));
+  assert(float_add (fp32_pos_qnan_0, fp32_pos_snan_0) == (fp32_pos_qnan_0 | fp32_pos_qnan_default, fp_eflag_invalid));
+
+  assert(float_add (fp32_neg_qnan_0, fp32_neg_qnan_1) == (fp32_neg_qnan_0 | fp32_neg_qnan_default, fp_eflag_none));
+  assert(float_add (fp32_neg_qnan_0, fp32_neg_qnan_default) == (fp32_neg_qnan_0 | fp32_neg_qnan_default, fp_eflag_none));
+  assert(float_add (fp32_neg_qnan_0, fp32_neg_inf) == (fp32_neg_qnan_0 | fp32_neg_qnan_default, fp_eflag_none));
+  assert(float_add (fp32_neg_qnan_0, fp32_neg_snan_0) == (fp32_neg_qnan_0 | fp32_neg_qnan_default, fp_eflag_invalid));
+
+  assert(float_add (fp32_pos_snan_0, fp32_pos_snan_1) == (fp32_pos_snan_0 | fp32_pos_qnan_default, fp_eflag_invalid));
+  assert(float_add (fp32_pos_snan_0, fp32_pos_qnan_0) == (fp32_pos_snan_0 | fp32_pos_qnan_default, fp_eflag_invalid));
+  assert(float_add (fp32_pos_snan_0, fp32_pos_qnan_default) == (fp32_pos_snan_0 | fp32_pos_qnan_default, fp_eflag_invalid));
+  assert(float_add (fp32_pos_snan_0, fp32_pos_inf) == (fp32_pos_snan_0 | fp32_pos_qnan_default, fp_eflag_invalid));
+  assert(float_add (fp32_pos_snan_0, fp32_pos_qnan_0) == (fp32_pos_snan_0 | fp32_pos_qnan_default, fp_eflag_invalid));
+
+  assert(float_add (fp32_neg_snan_0, fp32_neg_snan_1) == (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_neg_snan_0, fp32_neg_qnan_default) == (fp32_neg_snan_0 | fp32_neg_qnan_default, fp_eflag_invalid));
+  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));
 
   /* 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));
@@ -42,8 +98,36 @@ function test_float_add () -> unit = {
   assert(float_add (fp64_neg_denormal_add_1_op_0, fp64_neg_denormal_add_1_op_1) == (fp64_neg_denormal_add_1_sum, fp_eflag_none));
 
   assert(float_add (fp64_pos_inf, fp64_pos_inf) == (fp64_pos_inf, fp_eflag_none));
-  assert(float_add (fp64_pos_inf, fp64_pos_denormal_1) == (fp64_pos_inf, fp_eflag_none));
-  assert(float_add (fp64_pos_inf, fp64_pos_normal_0) == (fp64_pos_inf, fp_eflag_none));
+  assert(float_add (fp64_pos_inf, fp64_pos_qnan_default) == (fp64_pos_qnan_default, fp_eflag_none));
+  assert(float_add (fp64_pos_inf, fp64_pos_qnan_0) == (fp64_pos_qnan_0 | fp64_pos_qnan_default, fp_eflag_none));
+  assert(float_add (fp64_pos_inf, fp64_pos_snan_0) == (fp64_pos_snan_0 | fp64_pos_qnan_default, fp_eflag_invalid));
+
+  assert(float_add (fp64_neg_inf, fp64_neg_inf) == (fp64_neg_inf, fp_eflag_none));
+  assert(float_add (fp64_neg_inf, fp64_neg_qnan_default) == (fp64_neg_qnan_default, fp_eflag_none));
+  assert(float_add (fp64_neg_inf, fp64_neg_qnan_0) == (fp64_neg_qnan_0 | fp64_neg_qnan_default, fp_eflag_none));
+  assert(float_add (fp64_neg_inf, fp64_neg_snan_0) == (fp64_neg_snan_0 | fp64_neg_qnan_default, fp_eflag_invalid));
+
+  assert(float_add (fp64_pos_qnan_0, fp64_pos_qnan_1) == (fp64_pos_qnan_0 | fp64_pos_qnan_default, fp_eflag_none));
+  assert(float_add (fp64_pos_qnan_0, fp64_pos_qnan_default) == (fp64_pos_qnan_0 | fp64_pos_qnan_default, fp_eflag_none));
+  assert(float_add (fp64_pos_qnan_0, fp64_pos_inf) == (fp64_pos_qnan_0 | fp64_pos_qnan_default, fp_eflag_none));
+  assert(float_add (fp64_pos_qnan_0, fp64_pos_snan_0) == (fp64_pos_qnan_0 | fp64_pos_qnan_default, fp_eflag_invalid));
+
+  assert(float_add (fp64_neg_qnan_0, fp64_neg_qnan_1) == (fp64_neg_qnan_0 | fp64_neg_qnan_default, fp_eflag_none));
+  assert(float_add (fp64_neg_qnan_0, fp64_neg_qnan_default) == (fp64_neg_qnan_0 | fp64_neg_qnan_default, fp_eflag_none));
+  assert(float_add (fp64_neg_qnan_0, fp64_neg_inf) == (fp64_neg_qnan_0 | fp64_neg_qnan_default, fp_eflag_none));
+  assert(float_add (fp64_neg_qnan_0, fp64_neg_snan_0) == (fp64_neg_qnan_0 | fp64_neg_qnan_default, fp_eflag_invalid));
+
+  assert(float_add (fp64_pos_snan_0, fp64_pos_snan_1) == (fp64_pos_snan_0 | fp64_pos_qnan_default, fp_eflag_invalid));
+  assert(float_add (fp64_pos_snan_0, fp64_pos_qnan_0) == (fp64_pos_snan_0 | fp64_pos_qnan_default, fp_eflag_invalid));
+  assert(float_add (fp64_pos_snan_0, fp64_pos_qnan_default) == (fp64_pos_snan_0 | fp64_pos_qnan_default, fp_eflag_invalid));
+  assert(float_add (fp64_pos_snan_0, fp64_pos_inf) == (fp64_pos_snan_0 | fp64_pos_qnan_default, fp_eflag_invalid));
+  assert(float_add (fp64_pos_snan_0, fp64_pos_qnan_0) == (fp64_pos_snan_0 | fp64_pos_qnan_default, fp_eflag_invalid));
+
+  assert(float_add (fp64_neg_snan_0, fp64_neg_snan_1) == (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_neg_snan_0, fp64_neg_qnan_default) == (fp64_neg_snan_0 | fp64_neg_qnan_default, fp_eflag_invalid));
+  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));
 
   /* 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));
@@ -52,8 +136,36 @@ function test_float_add () -> unit = {
   assert(float_add (fp128_neg_denormal_add_1_op_0, fp128_neg_denormal_add_1_op_1) == (fp128_neg_denormal_add_1_sum, fp_eflag_none));
 
   assert(float_add (fp128_pos_inf, fp128_pos_inf) == (fp128_pos_inf, fp_eflag_none));
-  assert(float_add (fp128_pos_inf, fp128_pos_denormal_1) == (fp128_pos_inf, fp_eflag_none));
-  assert(float_add (fp128_pos_inf, fp128_pos_normal_0) == (fp128_pos_inf, fp_eflag_none));
+  assert(float_add (fp128_pos_inf, fp128_pos_qnan_default) == (fp128_pos_qnan_default, fp_eflag_none));
+  assert(float_add (fp128_pos_inf, fp128_pos_qnan_0) == (fp128_pos_qnan_0 | fp128_pos_qnan_default, fp_eflag_none));
+  assert(float_add (fp128_pos_inf, fp128_pos_snan_0) == (fp128_pos_snan_0 | fp128_pos_qnan_default, fp_eflag_invalid));
+
+  assert(float_add (fp128_neg_inf, fp128_neg_inf) == (fp128_neg_inf, fp_eflag_none));
+  assert(float_add (fp128_neg_inf, fp128_neg_qnan_default) == (fp128_neg_qnan_default, fp_eflag_none));
+  assert(float_add (fp128_neg_inf, fp128_neg_qnan_0) == (fp128_neg_qnan_0 | fp128_neg_qnan_default, fp_eflag_none));
+  assert(float_add (fp128_neg_inf, fp128_neg_snan_0) == (fp128_neg_snan_0 | fp128_neg_qnan_default, fp_eflag_invalid));
+
+  assert(float_add (fp128_pos_qnan_0, fp128_pos_qnan_1) == (fp128_pos_qnan_0 | fp128_pos_qnan_default, fp_eflag_none));
+  assert(float_add (fp128_pos_qnan_0, fp128_pos_qnan_default) == (fp128_pos_qnan_0 | fp128_pos_qnan_default, fp_eflag_none));
+  assert(float_add (fp128_pos_qnan_0, fp128_pos_inf) == (fp128_pos_qnan_0 | fp128_pos_qnan_default, fp_eflag_none));
+  assert(float_add (fp128_pos_qnan_0, fp128_pos_snan_0) == (fp128_pos_qnan_0 | fp128_pos_qnan_default, fp_eflag_invalid));
+
+  assert(float_add (fp128_neg_qnan_0, fp128_neg_qnan_1) == (fp128_neg_qnan_0 | fp128_neg_qnan_default, fp_eflag_none));
+  assert(float_add (fp128_neg_qnan_0, fp128_neg_qnan_default) == (fp128_neg_qnan_0 | fp128_neg_qnan_default, fp_eflag_none));
+  assert(float_add (fp128_neg_qnan_0, fp128_neg_inf) == (fp128_neg_qnan_0 | fp128_neg_qnan_default, fp_eflag_none));
+  assert(float_add (fp128_neg_qnan_0, fp128_neg_snan_0) == (fp128_neg_qnan_0 | fp128_neg_qnan_default, fp_eflag_invalid));
+
+  assert(float_add (fp128_pos_snan_0, fp128_pos_snan_1) == (fp128_pos_snan_0 | fp128_pos_qnan_default, fp_eflag_invalid));
+  assert(float_add (fp128_pos_snan_0, fp128_pos_qnan_0) == (fp128_pos_snan_0 | fp128_pos_qnan_default, fp_eflag_invalid));
+  assert(float_add (fp128_pos_snan_0, fp128_pos_qnan_default) == (fp128_pos_snan_0 | fp128_pos_qnan_default, fp_eflag_invalid));
+  assert(float_add (fp128_pos_snan_0, fp128_pos_inf) == (fp128_pos_snan_0 | fp128_pos_qnan_default, fp_eflag_invalid));
+  assert(float_add (fp128_pos_snan_0, fp128_pos_qnan_0) == (fp128_pos_snan_0 | fp128_pos_qnan_default, fp_eflag_invalid));
+
+  assert(float_add (fp128_neg_snan_0, fp128_neg_snan_1) == (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_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));
 }
 
 function main () -> unit = {

test/float/data.sail

@@ -16,10 +16,12 @@ let fp16_pos_snan_1      = 0x7d10
 let fp16_neg_snan_0      = 0xfc01
 let fp16_neg_snan_1      = 0xfd10
 
-let fp16_pos_qnan_0      = 0x7e00
-let fp16_pos_qnan_1      = 0x7e01
-let fp16_neg_qnan_0      = 0xfe00
-let fp16_neg_qnan_1      = 0xfe01
+let fp16_pos_qnan_0       = 0x7e00
+let fp16_pos_qnan_1       = 0x7e01
+let fp16_pos_qnan_default = 0x7e00
+let fp16_neg_qnan_0       = 0xfe00
+let fp16_neg_qnan_1       = 0xfe01
+let fp16_neg_qnan_default = 0xfe00
 
 let fp16_pos_inf         = 0x7c00
 let fp16_neg_inf         = 0xfc00
@@ -59,10 +61,12 @@ let fp32_pos_snan_1      = 0x7f8f0000
 let fp32_neg_snan_0      = 0xff800001
 let fp32_neg_snan_1      = 0xff8f0000
 
-let fp32_pos_qnan_0      = 0x7fc00000
-let fp32_pos_qnan_1      = 0x7fc00001
-let fp32_neg_qnan_0      = 0xffc00000
-let fp32_neg_qnan_1      = 0xffc00001
+let fp32_pos_qnan_0       = 0x7fc00000
+let fp32_pos_qnan_1       = 0x7fc00001
+let fp32_pos_qnan_default = 0x7fc00000
+let fp32_neg_qnan_0       = 0xffc00000
+let fp32_neg_qnan_1       = 0xffc00001
+let fp32_neg_qnan_default = 0xffc00000
 
 let fp32_pos_inf         = 0x7f800000
 let fp32_neg_inf         = 0xff800000
@@ -102,10 +106,12 @@ let fp64_pos_snan_1      = 0x7ff7000000000000
 let fp64_neg_snan_0      = 0xfff0000000000001
 let fp64_neg_snan_1      = 0xfff7000000000000
 
-let fp64_pos_qnan_0      = 0x7ff8000000000000
-let fp64_pos_qnan_1      = 0x7fff000000000000
-let fp64_neg_qnan_0      = 0xfff8000000000000
-let fp64_neg_qnan_1      = 0xffff000000000000
+let fp64_pos_qnan_0       = 0x7ff8000000000000
+let fp64_pos_qnan_1       = 0x7fff000000000000
+let fp64_pos_qnan_default = 0x7ff8000000000000
+let fp64_neg_qnan_0       = 0xfff8000000000000
+let fp64_neg_qnan_1       = 0xffff000000000000
+let fp64_neg_qnan_default = 0xfff8000000000000
 
 let fp64_pos_inf         = 0x7ff0000000000000
 let fp64_neg_inf         = 0xfff0000000000000
@@ -145,10 +151,12 @@ let fp128_pos_snan_1     = 0x7fff000000000000ff00000000000000
 let fp128_neg_snan_0     = 0xffff0000000000000000000000000001
 let fp128_neg_snan_1     = 0xffff000000000000ff00000000000000
 
-let fp128_pos_qnan_0     = 0x7fff8000000000000000000000000001
-let fp128_pos_qnan_1     = 0x7fff8d00000000000000000000000000
-let fp128_neg_qnan_0     = 0xffff8000000000000000000000000001
-let fp128_neg_qnan_1     = 0xffff8d00000000000000000000000000
+let fp128_pos_qnan_0       = 0x7fff8000000000000000000000000001
+let fp128_pos_qnan_1       = 0x7fff8d00000000000000000000000000
+let fp128_pos_qnan_default = 0x7fff8000000000000000000000000000
+let fp128_neg_qnan_0       = 0xffff8000000000000000000000000001
+let fp128_neg_qnan_1       = 0xffff8d00000000000000000000000000
+let fp128_neg_qnan_default = 0xffff8000000000000000000000000000
 
 let fp128_pos_inf        = 0x7fff0000000000000000000000000000
 let fp128_neg_inf        = 0xffff0000000000000000000000000000