Float: Introduce floating point api gt_quiet

* The gt(greater than) quiet api(s) introduced.
* Add test cases for half, single, double and quad floating point.
* Add gt_quiet to interface.

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

lib/float/gt_quiet.sail

@@ -0,0 +1,49 @@
+/*==========================================================================*/
+/* 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_GT_QUIET
+$define _FLOAT_GT_QUIET
+
+$include <float/common.sail>
+$include <float/nan.sail>
+$include <float/arith_internal.sail>
+
+val float_is_gt_quiet : fp_bits_x2 -> fp_bool_and_flags
+function float_is_gt_quiet ((op_0, op_1)) = {
+ let is_nan = float_is_nan (op_0) | float_is_nan (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 is_gt = not (is_nan) & float_is_gt_internal ((op_0, op_1));
+
+ (is_gt, flags);
+}
+
+$endif

lib/float/interface.sail

@@ -43,5 +43,6 @@ $include <float/lt_quiet.sail>
 $include <float/le.sail>
 $include <float/le_quiet.sail>
 $include <float/gt.sail>
+$include <float/gt_quiet.sail>
 
 $endif

src/bin/dune

@@ -169,6 +169,7 @@
  (%{workspace_root}/lib/float/le.sail as lib/float/le.sail)
  (%{workspace_root}/lib/float/le_quiet.sail as lib/float/le_quiet.sail)
  (%{workspace_root}/lib/float/gt.sail as lib/float/gt.sail)
+ (%{workspace_root}/lib/float/gt_quiet.sail as lib/float/gt_quiet.sail)
  (%{workspace_root}/lib/float/interface.sail as lib/float/interface.sail)
  (%{workspace_root}/lib/reverse_endianness.sail
  as

test/float/gt_quiet_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/gt_quiet.sail>
+$include "tuple_equality.sail"
+$include "data.sail"
+
+function test_float_is_gt_quiet () -> unit = {
+ /* Half floating point */
+ assert(float_is_gt_quiet((fp16_pos_snan_0, fp16_neg_snan_0)) == (false, fp_eflag_invalid));
+ assert(float_is_gt_quiet((fp16_pos_qnan_0, fp16_pos_normal_0)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp16_neg_denormal_0, fp16_neg_snan_0)) == (false, fp_eflag_invalid));
+
+ assert(float_is_gt_quiet((fp16_neg_zero, fp16_neg_zero)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp16_pos_zero, fp16_pos_zero)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp16_neg_zero, fp16_pos_zero)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp16_pos_zero, fp16_neg_zero)) == (false, fp_eflag_none));
+
+ assert(float_is_gt_quiet((fp16_pos_inf, fp16_pos_inf)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp16_neg_inf, fp16_pos_inf)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp16_neg_inf, fp16_neg_denormal_0)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp16_neg_inf, fp16_neg_zero)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp16_neg_inf, fp16_pos_denormal_0)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp16_neg_inf, fp16_pos_normal_0)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp16_pos_inf, fp16_pos_inf)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp16_pos_inf, fp16_neg_denormal_0)) == (true, fp_eflag_none));
+ assert(float_is_gt_quiet((fp16_pos_inf, fp16_neg_zero)) == (true, fp_eflag_none));
+ assert(float_is_gt_quiet((fp16_pos_inf, fp16_pos_denormal_0)) == (true, fp_eflag_none));
+ assert(float_is_gt_quiet((fp16_pos_inf, fp16_pos_normal_0)) == (true, fp_eflag_none));
+
+ assert(float_is_gt_quiet((fp16_pos_normal_0, fp16_pos_normal_1)) == (true, fp_eflag_none));
+ assert(float_is_gt_quiet((fp16_pos_normal_1, fp16_pos_normal_0)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp16_pos_normal_0, fp16_pos_normal_0)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp16_neg_normal_0, fp16_neg_normal_1)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp16_neg_normal_1, fp16_neg_normal_0)) == (true, fp_eflag_none));
+ assert(float_is_gt_quiet((fp16_neg_normal_0, fp16_neg_normal_0)) == (false, fp_eflag_none));
+
+ assert(float_is_gt_quiet((fp16_pos_denormal_0, fp16_pos_normal_0)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp16_neg_denormal_0, fp16_neg_normal_0)) == (true, fp_eflag_none));
+
+ /* Single floating point */
+ assert(float_is_gt_quiet((fp32_pos_snan_0, fp32_neg_snan_0)) == (false, fp_eflag_invalid));
+ assert(float_is_gt_quiet((fp32_pos_qnan_0, fp32_pos_normal_0)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp32_neg_denormal_0, fp32_neg_snan_0)) == (false, fp_eflag_invalid));
+
+ assert(float_is_gt_quiet((fp32_neg_zero, fp32_neg_zero)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp32_pos_zero, fp32_pos_zero)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp32_neg_zero, fp32_pos_zero)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp32_pos_zero, fp32_neg_zero)) == (false, fp_eflag_none));
+
+ assert(float_is_gt_quiet((fp32_pos_inf, fp32_pos_inf)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp32_neg_inf, fp32_pos_inf)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp32_neg_inf, fp32_neg_denormal_0)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp32_neg_inf, fp32_neg_zero)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp32_neg_inf, fp32_pos_denormal_0)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp32_neg_inf, fp32_pos_normal_0)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp32_pos_inf, fp32_pos_inf)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp32_pos_inf, fp32_neg_denormal_0)) == (true, fp_eflag_none));
+ assert(float_is_gt_quiet((fp32_pos_inf, fp32_neg_zero)) == (true, fp_eflag_none));
+ assert(float_is_gt_quiet((fp32_pos_inf, fp32_pos_denormal_0)) == (true, fp_eflag_none));
+ assert(float_is_gt_quiet((fp32_pos_inf, fp32_pos_normal_0)) == (true, fp_eflag_none));
+
+ assert(float_is_gt_quiet((fp32_pos_normal_0, fp32_pos_normal_1)) == (true, fp_eflag_none));
+ assert(float_is_gt_quiet((fp32_pos_normal_1, fp32_pos_normal_0)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp32_pos_normal_0, fp32_pos_normal_0)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp32_neg_normal_0, fp32_neg_normal_1)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp32_neg_normal_1, fp32_neg_normal_0)) == (true, fp_eflag_none));
+ assert(float_is_gt_quiet((fp32_neg_normal_0, fp32_neg_normal_0)) == (false, fp_eflag_none));
+
+ assert(float_is_gt_quiet((fp32_pos_denormal_0, fp32_pos_normal_0)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp32_neg_denormal_0, fp32_neg_normal_0)) == (true, fp_eflag_none));
+
+ /* Double floating point */
+ assert(float_is_gt_quiet((fp64_pos_snan_0, fp64_neg_snan_0)) == (false, fp_eflag_invalid));
+ assert(float_is_gt_quiet((fp64_pos_qnan_0, fp64_pos_normal_0)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp64_neg_denormal_0, fp64_neg_snan_0)) == (false, fp_eflag_invalid));
+
+ assert(float_is_gt_quiet((fp64_neg_zero, fp64_neg_zero)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp64_pos_zero, fp64_pos_zero)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp64_neg_zero, fp64_pos_zero)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp64_pos_zero, fp64_neg_zero)) == (false, fp_eflag_none));
+
+ assert(float_is_gt_quiet((fp64_pos_inf, fp64_pos_inf)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp64_neg_inf, fp64_pos_inf)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp64_neg_inf, fp64_neg_denormal_0)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp64_neg_inf, fp64_neg_zero)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp64_neg_inf, fp64_pos_denormal_0)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp64_neg_inf, fp64_pos_normal_0)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp64_pos_inf, fp64_pos_inf)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp64_pos_inf, fp64_neg_denormal_0)) == (true, fp_eflag_none));
+ assert(float_is_gt_quiet((fp64_pos_inf, fp64_neg_zero)) == (true, fp_eflag_none));
+ assert(float_is_gt_quiet((fp64_pos_inf, fp64_pos_denormal_0)) == (true, fp_eflag_none));
+ assert(float_is_gt_quiet((fp64_pos_inf, fp64_pos_normal_0)) == (true, fp_eflag_none));
+
+ assert(float_is_gt_quiet((fp64_pos_normal_0, fp64_pos_normal_1)) == (true, fp_eflag_none));
+ assert(float_is_gt_quiet((fp64_pos_normal_1, fp64_pos_normal_0)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp64_pos_normal_0, fp64_pos_normal_0)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp64_neg_normal_0, fp64_neg_normal_1)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp64_neg_normal_1, fp64_neg_normal_0)) == (true, fp_eflag_none));
+ assert(float_is_gt_quiet((fp64_neg_normal_0, fp64_neg_normal_0)) == (false, fp_eflag_none));
+
+ assert(float_is_gt_quiet((fp64_pos_denormal_0, fp64_pos_normal_0)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp64_neg_denormal_0, fp64_neg_normal_0)) == (true, fp_eflag_none));
+
+ /* Quad floating point */
+ assert(float_is_gt_quiet((fp128_pos_snan_0, fp128_neg_snan_0)) == (false, fp_eflag_invalid));
+ assert(float_is_gt_quiet((fp128_pos_qnan_0, fp128_pos_normal_0)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp128_neg_denormal_0, fp128_neg_snan_0)) == (false, fp_eflag_invalid));
+
+ assert(float_is_gt_quiet((fp128_neg_zero, fp128_neg_zero)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp128_pos_zero, fp128_pos_zero)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp128_neg_zero, fp128_pos_zero)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp128_pos_zero, fp128_neg_zero)) == (false, fp_eflag_none));
+
+ assert(float_is_gt_quiet((fp128_pos_inf, fp128_pos_inf)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp128_neg_inf, fp128_pos_inf)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp128_neg_inf, fp128_neg_denormal_0)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp128_neg_inf, fp128_neg_zero)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp128_neg_inf, fp128_pos_denormal_0)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp128_neg_inf, fp128_pos_normal_0)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp128_pos_inf, fp128_pos_inf)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp128_pos_inf, fp128_neg_denormal_0)) == (true, fp_eflag_none));
+ assert(float_is_gt_quiet((fp128_pos_inf, fp128_neg_zero)) == (true, fp_eflag_none));
+ assert(float_is_gt_quiet((fp128_pos_inf, fp128_pos_denormal_0)) == (true, fp_eflag_none));
+ assert(float_is_gt_quiet((fp128_pos_inf, fp128_pos_normal_0)) == (true, fp_eflag_none));
+
+ assert(float_is_gt_quiet((fp128_pos_normal_0, fp128_pos_normal_1)) == (true, fp_eflag_none));
+ assert(float_is_gt_quiet((fp128_pos_normal_1, fp128_pos_normal_0)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp128_pos_normal_0, fp128_pos_normal_0)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp128_neg_normal_0, fp128_neg_normal_1)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp128_neg_normal_1, fp128_neg_normal_0)) == (true, fp_eflag_none));
+ assert(float_is_gt_quiet((fp128_neg_normal_0, fp128_neg_normal_0)) == (false, fp_eflag_none));
+
+ assert(float_is_gt_quiet((fp128_pos_denormal_0, fp128_pos_normal_0)) == (false, fp_eflag_none));
+ assert(float_is_gt_quiet((fp128_neg_denormal_0, fp128_neg_normal_0)) == (true, fp_eflag_none));
+}
+
+function main () -> unit = {
+ test_float_is_gt_quiet();
+}