Float: Refactor bool == false into not function (#623)

* Float: Refactor bool == false into not function * Add new function not (bool) -> bool. * Leverage not (bool) function in float lib. Signed-off-by: Pan Li <[email protected]> * Leverage existing not_bool for alias. Signed-off-by: Pan Li <[email protected]> --------- Signed-off-by: Pan Li <[email protected]>
rems-project · Jul 12, 2024 · d8c5322 · d8c5322
1 parent 5194029
commit d8c5322
Show file tree

Hide file tree

Showing 4 changed files with 8 additions and 5 deletions.
diff --git a/lib/float/common.sail b/lib/float/common.sail
@@ -86,4 +86,7 @@ function float_decompose(op) = {
   }
 }
 
+val      not : forall ('p : Bool). bool('p) -> bool(not('p))
+function not(b) = not_bool(b)
+
 $endif
diff --git a/lib/float/eq.sail b/lib/float/eq.sail
@@ -43,7 +43,7 @@ function float_is_eq ((op_0, op_1)) = {
 
   let is_nan  = float_is_nan (op_0) | float_is_nan (op_1);
   let is_zero = float_is_zero (op_0) & float_is_zero (op_1);
-  let is_eq   = is_nan == false & ((op_0 == op_1) | is_zero);
+  let is_eq   = not (is_nan) & ((op_0 == op_1) | is_zero);
 
   (is_eq, flags);
 }

diff --git a/lib/float/lt.sail b/lib/float/lt.sail
@@ -45,17 +45,17 @@ function float_is_lt ((op_0, op_1)) = {
   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 diff_sign_lt = (fp_0.sign[0] == bitone) & not (is_zero);
 
   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 is_xor       = (is_neg & not (unsigned_lt)) | (not (is_neg) & 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;
+  let is_lt        = not (is_nan) & is_normal_lt;
 
   (is_lt, flags);
 }

diff --git a/lib/float/ne.sail b/lib/float/ne.sail
@@ -43,7 +43,7 @@ function float_is_ne ((op_0, op_1)) = {
 
   let is_nan  = float_is_nan (op_0) | float_is_nan (op_1);
   let is_zero = float_is_zero (op_0) & float_is_zero (op_1);
-  let is_ne   = is_nan == false & (op_0 != op_1) & is_zero == false;
+  let is_ne   = not (is_nan) & (op_0 != op_1) & not (is_zero);
 
   (is_ne, flags);
 }