Float: Introduce floating point api lt (#617)

* The lt(less than) api(s) introduced. * Add test cases for half, single, double and quad floating point. * Add lt to interface. Signed-off-by: Pan Li <[email protected]>
rems-project · Jul 5, 2024 · ec47b19 · ec47b19
1 parent 19d83d6
commit ec47b19
Show file tree

Hide file tree

Showing 4 changed files with 234 additions and 0 deletions.
diff --git a/lib/float/interface.sail b/lib/float/interface.sail
@@ -38,5 +38,6 @@ $include <float/zero.sail>
 $include <float/normal.sail>
 $include <float/eq.sail>
 $include <float/ne.sail>
+$include <float/lt.sail>
 
 $endif
diff --git a/lib/float/lt.sail b/lib/float/lt.sail
@@ -0,0 +1,63 @@
+/*==========================================================================*/
+/*     Sail                                                                 */
+/*                                                                          */
+/* Copyright 2024 Intel Corporation                                         */
+/*   Pan Li - [email protected]                                             */
+/*                                                                          */
+/* Redistribution and use in source and binary forms, with or without       */
+/* modification, are permitted provided that the following conditions are   */
+/* met:                                                                     */
+/*                                                                          */
+/* 1. Redistributions of source code must retain the above copyright        */
+/*    notice, this list of conditions and the following disclaimer.         */
+/* 2. Redistributions in binary form must reproduce the above copyright     */
+/*    notice, this list of conditions and the following disclaimer in the   */
+/*    documentation and/or other materials provided with the distribution.  */
+/*                                                                          */
+/* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS      */
+/* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT        */
+/* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A  */
+/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT       */
+/* HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,   */
+/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED */
+/* TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR   */
+/* PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF   */
+/* LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING     */
+/* NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS       */
+/* SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.             */
+/*==========================================================================*/
+
+$ifndef _FLOAT_LT
+$define _FLOAT_LT
+
+$include <float/common.sail>
+$include <float/zero.sail>
+$include <float/nan.sail>
+
+val      float_is_lt : fp_bits_x2 -> fp_bool_and_flags
+function float_is_lt ((op_0, op_1)) = {
+  let is_nan  = float_is_nan (op_0) | float_is_nan (op_1);
+  let flags   = if   is_nan
+                then fp_eflag_invalid
+                else fp_eflag_none;
+
+  let fp_0 = float_decompose (op_0);
+  let fp_1 = float_decompose (op_1);
+
+  let is_zero      = float_is_zero (op_0) & float_is_zero (op_1);
+  let diff_sign_lt = (fp_0.sign[0] == bitone) & (is_zero == false);
+
+  let is_neg       = fp_0.sign[0] == bitone;
+  let unsigned_lt  = unsigned (op_0) < unsigned (op_1);
+  let is_xor       = (is_neg & unsigned_lt == false) | (is_neg == false & unsigned_lt);
+  let same_sign_lt = (op_0 != op_1) & is_xor;
+
+  let is_normal_lt = if   fp_0.sign != fp_1.sign
+                     then diff_sign_lt
+                     else same_sign_lt;
+  let is_lt        = is_nan == false & is_normal_lt;
+
+  (is_lt, flags);
+}
+
+$endif
diff --git a/src/bin/dune b/src/bin/dune
@@ -160,6 +160,7 @@
   (%{workspace_root}/lib/float/normal.sail as lib/float/normal.sail)
   (%{workspace_root}/lib/float/eq.sail as lib/float/eq.sail)
   (%{workspace_root}/lib/float/ne.sail as lib/float/ne.sail)
+  (%{workspace_root}/lib/float/lt.sail as lib/float/lt.sail)
   (%{workspace_root}/lib/float/interface.sail as lib/float/interface.sail)
   (%{workspace_root}/lib/reverse_endianness.sail
    as

diff --git a/test/float/lt_test.sail b/test/float/lt_test.sail
@@ -0,0 +1,169 @@
+/*==========================================================================*/
+/*     Sail                                                                 */
+/*                                                                          */
+/* Copyright 2024 Intel Corporation                                         */
+/*   Pan Li - [email protected]                                             */
+/*                                                                          */
+/* Redistribution and use in source and binary forms, with or without       */
+/* modification, are permitted provided that the following conditions are   */
+/* met:                                                                     */
+/*                                                                          */
+/* 1. Redistributions of source code must retain the above copyright        */
+/*    notice, this list of conditions and the following disclaimer.         */
+/* 2. Redistributions in binary form must reproduce the above copyright     */
+/*    notice, this list of conditions and the following disclaimer in the   */
+/*    documentation and/or other materials provided with the distribution.  */
+/*                                                                          */
+/* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS      */
+/* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT        */
+/* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A  */
+/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT       */
+/* HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,   */
+/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED */
+/* TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR   */
+/* PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF   */
+/* LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING     */
+/* NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS       */
+/* SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.             */
+/*==========================================================================*/
+
+default Order dec
+
+$include <prelude.sail>
+$include <float/lt.sail>
+$include "tuple_equality.sail"
+$include "data.sail"
+
+function test_float_is_lt () -> unit = {
+  /* Half floating point */
+  assert(float_is_lt((fp16_pos_snan_0, fp16_neg_snan_0)) == (false, fp_eflag_invalid));
+  assert(float_is_lt((fp16_pos_qnan_0, fp16_pos_normal_0)) == (false, fp_eflag_invalid));
+  assert(float_is_lt((fp16_neg_denormal_0, fp16_neg_snan_0)) == (false, fp_eflag_invalid));
+
+  assert(float_is_lt((fp16_neg_zero, fp16_neg_zero)) == (false, fp_eflag_none));
+  assert(float_is_lt((fp16_pos_zero, fp16_pos_zero)) == (false, fp_eflag_none));
+  assert(float_is_lt((fp16_neg_zero, fp16_pos_zero)) == (false, fp_eflag_none));
+  assert(float_is_lt((fp16_pos_zero, fp16_neg_zero)) == (false, fp_eflag_none));
+
+  assert(float_is_lt((fp16_pos_inf, fp16_pos_inf)) == (false, fp_eflag_none));
+  assert(float_is_lt((fp16_neg_inf, fp16_pos_inf)) == (true, fp_eflag_none));
+  assert(float_is_lt((fp16_neg_inf, fp16_neg_denormal_0)) == (true, fp_eflag_none));
+  assert(float_is_lt((fp16_neg_inf, fp16_neg_zero)) == (true, fp_eflag_none));
+  assert(float_is_lt((fp16_neg_inf, fp16_pos_denormal_0)) == (true, fp_eflag_none));
+  assert(float_is_lt((fp16_neg_inf, fp16_pos_normal_0)) == (true, fp_eflag_none));
+  assert(float_is_lt((fp16_pos_inf, fp16_pos_inf)) == (false, fp_eflag_none));
+  assert(float_is_lt((fp16_pos_inf, fp16_neg_denormal_0)) == (false, fp_eflag_none));
+  assert(float_is_lt((fp16_pos_inf, fp16_neg_zero)) == (false, fp_eflag_none));
+  assert(float_is_lt((fp16_pos_inf, fp16_pos_denormal_0)) == (false, fp_eflag_none));
+  assert(float_is_lt((fp16_pos_inf, fp16_pos_normal_0)) == (false, fp_eflag_none));
+
+  assert(float_is_lt((fp16_pos_normal_0, fp16_pos_normal_1)) == (false, fp_eflag_none));
+  assert(float_is_lt((fp16_pos_normal_1, fp16_pos_normal_0)) == (true, fp_eflag_none));
+  assert(float_is_lt((fp16_pos_normal_0, fp16_pos_normal_0)) == (false, fp_eflag_none));
+  assert(float_is_lt((fp16_neg_normal_0, fp16_neg_normal_1)) == (true, fp_eflag_none));
+  assert(float_is_lt((fp16_neg_normal_1, fp16_neg_normal_0)) == (false, fp_eflag_none));
+  assert(float_is_lt((fp16_neg_normal_0, fp16_neg_normal_0)) == (false, fp_eflag_none));
+
+  assert(float_is_lt((fp16_pos_denormal_0, fp16_pos_normal_0)) == (true, fp_eflag_none));
+  assert(float_is_lt((fp16_neg_denormal_0, fp16_neg_normal_0)) == (false, fp_eflag_none));
+
+  /* Single floating point */
+  assert(float_is_lt((fp32_pos_snan_0, fp32_neg_snan_0)) == (false, fp_eflag_invalid));
+  assert(float_is_lt((fp32_pos_qnan_0, fp32_pos_normal_0)) == (false, fp_eflag_invalid));
+  assert(float_is_lt((fp32_neg_denormal_0, fp32_neg_snan_0)) == (false, fp_eflag_invalid));
+
+  assert(float_is_lt((fp32_neg_zero, fp32_neg_zero)) == (false, fp_eflag_none));
+  assert(float_is_lt((fp32_pos_zero, fp32_pos_zero)) == (false, fp_eflag_none));
+  assert(float_is_lt((fp32_neg_zero, fp32_pos_zero)) == (false, fp_eflag_none));
+  assert(float_is_lt((fp32_pos_zero, fp32_neg_zero)) == (false, fp_eflag_none));
+
+  assert(float_is_lt((fp32_pos_inf, fp32_pos_inf)) == (false, fp_eflag_none));
+  assert(float_is_lt((fp32_neg_inf, fp32_pos_inf)) == (true, fp_eflag_none));
+  assert(float_is_lt((fp32_neg_inf, fp32_neg_denormal_0)) == (true, fp_eflag_none));
+  assert(float_is_lt((fp32_neg_inf, fp32_neg_zero)) == (true, fp_eflag_none));
+  assert(float_is_lt((fp32_neg_inf, fp32_pos_denormal_0)) == (true, fp_eflag_none));
+  assert(float_is_lt((fp32_neg_inf, fp32_pos_normal_0)) == (true, fp_eflag_none));
+  assert(float_is_lt((fp32_pos_inf, fp32_pos_inf)) == (false, fp_eflag_none));
+  assert(float_is_lt((fp32_pos_inf, fp32_neg_denormal_0)) == (false, fp_eflag_none));
+  assert(float_is_lt((fp32_pos_inf, fp32_neg_zero)) == (false, fp_eflag_none));
+  assert(float_is_lt((fp32_pos_inf, fp32_pos_denormal_0)) == (false, fp_eflag_none));
+  assert(float_is_lt((fp32_pos_inf, fp32_pos_normal_0)) == (false, fp_eflag_none));
+
+  assert(float_is_lt((fp32_pos_normal_0, fp32_pos_normal_1)) == (false, fp_eflag_none));
+  assert(float_is_lt((fp32_pos_normal_1, fp32_pos_normal_0)) == (true, fp_eflag_none));
+  assert(float_is_lt((fp32_pos_normal_0, fp32_pos_normal_0)) == (false, fp_eflag_none));
+  assert(float_is_lt((fp32_neg_normal_0, fp32_neg_normal_1)) == (true, fp_eflag_none));
+  assert(float_is_lt((fp32_neg_normal_1, fp32_neg_normal_0)) == (false, fp_eflag_none));
+  assert(float_is_lt((fp32_neg_normal_0, fp32_neg_normal_0)) == (false, fp_eflag_none));
+
+  assert(float_is_lt((fp32_pos_denormal_0, fp32_pos_normal_0)) == (true, fp_eflag_none));
+  assert(float_is_lt((fp32_neg_denormal_0, fp32_neg_normal_0)) == (false, fp_eflag_none));
+
+  /* Double floating point */
+  assert(float_is_lt((fp64_pos_snan_0, fp64_neg_snan_0)) == (false, fp_eflag_invalid));
+  assert(float_is_lt((fp64_pos_qnan_0, fp64_pos_normal_0)) == (false, fp_eflag_invalid));
+  assert(float_is_lt((fp64_neg_denormal_0, fp64_neg_snan_0)) == (false, fp_eflag_invalid));
+
+  assert(float_is_lt((fp64_neg_zero, fp64_neg_zero)) == (false, fp_eflag_none));
+  assert(float_is_lt((fp64_pos_zero, fp64_pos_zero)) == (false, fp_eflag_none));
+  assert(float_is_lt((fp64_neg_zero, fp64_pos_zero)) == (false, fp_eflag_none));
+  assert(float_is_lt((fp64_pos_zero, fp64_neg_zero)) == (false, fp_eflag_none));
+
+  assert(float_is_lt((fp64_pos_inf, fp64_pos_inf)) == (false, fp_eflag_none));
+  assert(float_is_lt((fp64_neg_inf, fp64_pos_inf)) == (true, fp_eflag_none));
+  assert(float_is_lt((fp64_neg_inf, fp64_neg_denormal_0)) == (true, fp_eflag_none));
+  assert(float_is_lt((fp64_neg_inf, fp64_neg_zero)) == (true, fp_eflag_none));
+  assert(float_is_lt((fp64_neg_inf, fp64_pos_denormal_0)) == (true, fp_eflag_none));
+  assert(float_is_lt((fp64_neg_inf, fp64_pos_normal_0)) == (true, fp_eflag_none));
+  assert(float_is_lt((fp64_pos_inf, fp64_pos_inf)) == (false, fp_eflag_none));
+  assert(float_is_lt((fp64_pos_inf, fp64_neg_denormal_0)) == (false, fp_eflag_none));
+  assert(float_is_lt((fp64_pos_inf, fp64_neg_zero)) == (false, fp_eflag_none));
+  assert(float_is_lt((fp64_pos_inf, fp64_pos_denormal_0)) == (false, fp_eflag_none));
+  assert(float_is_lt((fp64_pos_inf, fp64_pos_normal_0)) == (false, fp_eflag_none));
+
+  assert(float_is_lt((fp64_pos_normal_0, fp64_pos_normal_1)) == (false, fp_eflag_none));
+  assert(float_is_lt((fp64_pos_normal_1, fp64_pos_normal_0)) == (true, fp_eflag_none));
+  assert(float_is_lt((fp64_pos_normal_0, fp64_pos_normal_0)) == (false, fp_eflag_none));
+  assert(float_is_lt((fp64_neg_normal_0, fp64_neg_normal_1)) == (true, fp_eflag_none));
+  assert(float_is_lt((fp64_neg_normal_1, fp64_neg_normal_0)) == (false, fp_eflag_none));
+  assert(float_is_lt((fp64_neg_normal_0, fp64_neg_normal_0)) == (false, fp_eflag_none));
+
+  assert(float_is_lt((fp64_pos_denormal_0, fp64_pos_normal_0)) == (true, fp_eflag_none));
+  assert(float_is_lt((fp64_neg_denormal_0, fp64_neg_normal_0)) == (false, fp_eflag_none));
+
+  /* Quad floating point */
+  assert(float_is_lt((fp128_pos_snan_0, fp128_neg_snan_0)) == (false, fp_eflag_invalid));
+  assert(float_is_lt((fp128_pos_qnan_0, fp128_pos_normal_0)) == (false, fp_eflag_invalid));
+  assert(float_is_lt((fp128_neg_denormal_0, fp128_neg_snan_0)) == (false, fp_eflag_invalid));
+
+  assert(float_is_lt((fp128_neg_zero, fp128_neg_zero)) == (false, fp_eflag_none));
+  assert(float_is_lt((fp128_pos_zero, fp128_pos_zero)) == (false, fp_eflag_none));
+  assert(float_is_lt((fp128_neg_zero, fp128_pos_zero)) == (false, fp_eflag_none));
+  assert(float_is_lt((fp128_pos_zero, fp128_neg_zero)) == (false, fp_eflag_none));
+
+  assert(float_is_lt((fp128_pos_inf, fp128_pos_inf)) == (false, fp_eflag_none));
+  assert(float_is_lt((fp128_neg_inf, fp128_pos_inf)) == (true, fp_eflag_none));
+  assert(float_is_lt((fp128_neg_inf, fp128_neg_denormal_0)) == (true, fp_eflag_none));
+  assert(float_is_lt((fp128_neg_inf, fp128_neg_zero)) == (true, fp_eflag_none));
+  assert(float_is_lt((fp128_neg_inf, fp128_pos_denormal_0)) == (true, fp_eflag_none));
+  assert(float_is_lt((fp128_neg_inf, fp128_pos_normal_0)) == (true, fp_eflag_none));
+  assert(float_is_lt((fp128_pos_inf, fp128_pos_inf)) == (false, fp_eflag_none));
+  assert(float_is_lt((fp128_pos_inf, fp128_neg_denormal_0)) == (false, fp_eflag_none));
+  assert(float_is_lt((fp128_pos_inf, fp128_neg_zero)) == (false, fp_eflag_none));
+  assert(float_is_lt((fp128_pos_inf, fp128_pos_denormal_0)) == (false, fp_eflag_none));
+  assert(float_is_lt((fp128_pos_inf, fp128_pos_normal_0)) == (false, fp_eflag_none));
+
+  assert(float_is_lt((fp128_pos_normal_0, fp128_pos_normal_1)) == (false, fp_eflag_none));
+  assert(float_is_lt((fp128_pos_normal_1, fp128_pos_normal_0)) == (true, fp_eflag_none));
+  assert(float_is_lt((fp128_pos_normal_0, fp128_pos_normal_0)) == (false, fp_eflag_none));
+  assert(float_is_lt((fp128_neg_normal_0, fp128_neg_normal_1)) == (true, fp_eflag_none));
+  assert(float_is_lt((fp128_neg_normal_1, fp128_neg_normal_0)) == (false, fp_eflag_none));
+  assert(float_is_lt((fp128_neg_normal_0, fp128_neg_normal_0)) == (false, fp_eflag_none));
+
+  assert(float_is_lt((fp128_pos_denormal_0, fp128_pos_normal_0)) == (true, fp_eflag_none));
+  assert(float_is_lt((fp128_neg_denormal_0, fp128_neg_normal_0)) == (false, fp_eflag_none));
+}
+
+function main () -> unit = {
+  test_float_is_lt();
+}