Float: Refactor bits predicate function for code reuse (#631)

* Float: Refactor bits predicate func for code reuse * Add some bits predicate func. * Leverage thest function in float lib. Signed-off-by: Pan Li <[email protected]> * Simplify the bit ops function Signed-off-by: Pan Li <[email protected]> --------- Signed-off-by: Pan Li <[email protected]>
rems-project · Jul 19, 2024 · 574ccb2 · 574ccb2
1 parent d8c5322
commit 574ccb2
Show file tree

Hide file tree

Showing 7 changed files with 31 additions and 24 deletions.
diff --git a/lib/float/common.sail b/lib/float/common.sail
@@ -89,4 +89,22 @@ function float_decompose(op) = {
 val      not : forall ('p : Bool). bool('p) -> bool(not('p))
 function not(b) = not_bool(b)
 
+val      is_lowest_one : forall 'n, 0 < 'n. bits('n) -> bool
+function is_lowest_one (op) = op[0] == bitone
+
+val      is_highest_one : forall 'n, 0 < 'n. bits('n) -> bool
+function is_highest_one (op) = op['n - 1] == bitone
+
+val      is_all_ones : forall 'n, 0 < 'n. bits('n) -> bool
+function is_all_ones (op) = op == sail_ones ('n)
+
+val      is_lowest_zero : forall 'n, 0 < 'n. bits('n) -> bool
+function is_lowest_zero (op) = op[0] == bitzero
+
+val      is_highest_zero : forall 'n, 0 < 'n. bits('n) -> bool
+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)
+
 $endif
diff --git a/lib/float/inf.sail b/lib/float/inf.sail
@@ -35,8 +35,7 @@ $include <float/common.sail>
 val      float_is_inf : fp_bits -> bool
 function float_is_inf (op) = {
   let struct {_, exp, mantissa} = float_decompose(op);
-  let is_inf = exp == sail_ones(length(exp))
-               & mantissa == sail_zeros(length(mantissa));
+  let is_inf                    = is_all_ones (exp) & is_all_zeros (mantissa);
 
   is_inf
 }

diff --git a/lib/float/lt.sail b/lib/float/lt.sail
@@ -45,9 +45,9 @@ 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) & not (is_zero);
+  let diff_sign_lt = is_lowest_one (fp_0.sign) & not (is_zero);
 
-  let is_neg       = fp_0.sign[0] == bitone;
+  let is_neg       = is_lowest_one (fp_0.sign);
   let unsigned_lt  = unsigned (op_0) < unsigned (op_1);
   let is_xor       = (is_neg & not (unsigned_lt)) | (not (is_neg) & unsigned_lt);
   let same_sign_lt = (op_0 != op_1) & is_xor;

diff --git a/lib/float/nan.sail b/lib/float/nan.sail
@@ -35,28 +35,23 @@ $include <float/common.sail>
 val      float_is_nan : fp_bits -> bool
 function float_is_nan (op) = {
   let struct {_, exp, mantissa} = float_decompose(op);
-  let is_nan = exp == sail_ones(length(exp))
-               & mantissa != sail_zeros(length(mantissa));
+  let is_nan                    = is_all_ones (exp) & not (is_all_zeros (mantissa));
 
   is_nan
 }
 
 val      float_is_snan : fp_bits -> bool
 function float_is_snan (op) = {
-  let struct {_, exp, mantissa} = float_decompose(op);
-  let is_snan = exp == sail_ones(length(exp))
-                & mantissa != sail_zeros(length(mantissa))
-                & mantissa[length(mantissa) - 1] == bitzero;
+  let struct {_, mantissa} = float_decompose(op);
+  let is_snan              = float_is_nan (op) & is_highest_zero (mantissa);
 
   is_snan
 }
 
 val      float_is_qnan : fp_bits -> bool
 function float_is_qnan (op) = {
-  let struct {_, exp, mantissa} = float_decompose(op);
-  let is_qnan = exp == sail_ones(length(exp))
-                & mantissa != sail_zeros(length(mantissa))
-                & mantissa[length(mantissa) - 1] == bitone;
+  let struct {_, mantissa} = float_decompose(op);
+  let is_qnan              = float_is_nan (op) & is_highest_one (mantissa);
 
   is_qnan
 }

diff --git a/lib/float/normal.sail b/lib/float/normal.sail
@@ -35,17 +35,15 @@ $include <float/common.sail>
 val      float_is_normal : fp_bits -> bool
 function float_is_normal (op) = {
   let struct {_, exp} = float_decompose(op);
-  let is_normal = exp != sail_ones(length(exp))
-                  & exp != sail_zeros(length(exp));
+  let is_normal       = not (is_all_ones (exp)) & not (is_all_zeros (exp));
 
   is_normal
 }
 
 val      float_is_denormal : fp_bits -> bool
 function float_is_denormal (op) = {
   let struct {_, exp, mantissa} = float_decompose(op);
-  let is_denormal = exp == sail_zeros(length(exp))
-                    & mantissa != sail_zeros(length(mantissa));
+  let is_denormal               = is_all_zeros (exp) & not (is_all_zeros (mantissa));
 
   is_denormal
 }

diff --git a/lib/float/sign.sail b/lib/float/sign.sail
@@ -34,16 +34,14 @@ $include <float/common.sail>
 
 val      float_is_positive : fp_bits -> bool
 function float_is_positive (op) = {
-  let struct {sign, _} = float_decompose(op);
-  let is_positive = sign[0] == bitzero;
+  let is_positive = is_highest_zero (op);
 
   is_positive
 }
 
 val      float_is_negative : fp_bits -> bool
 function float_is_negative (op) = {
-  let struct {sign, _} = float_decompose(op);
-  let is_negative = sign[0] == bitone;
+  let is_negative = is_highest_one (op);
 
   is_negative
 }

diff --git a/lib/float/zero.sail b/lib/float/zero.sail
@@ -35,8 +35,7 @@ $include <float/common.sail>
 val      float_is_zero : fp_bits -> bool
 function float_is_zero (op) = {
   let struct {_, exp, mantissa} = float_decompose(op);
-  let is_zero = exp == sail_zeros(length(exp))
-               & mantissa == sail_zeros(length(mantissa));
+  let is_zero                   = is_all_zeros (exp) & is_all_zeros (mantissa);
 
   is_zero
 }