From 574ccb20c1e007903093e264942603456d11ad92 Mon Sep 17 00:00:00 2001 From: Pan Li Date: Sat, 20 Jul 2024 07:47:09 +0800 Subject: [PATCH] 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 * Simplify the bit ops function Signed-off-by: Pan Li --------- Signed-off-by: Pan Li --- lib/float/common.sail | 18 ++++++++++++++++++ lib/float/inf.sail | 3 +-- lib/float/lt.sail | 4 ++-- lib/float/nan.sail | 15 +++++---------- lib/float/normal.sail | 6 ++---- lib/float/sign.sail | 6 ++---- lib/float/zero.sail | 3 +-- 7 files changed, 31 insertions(+), 24 deletions(-) diff --git a/lib/float/common.sail b/lib/float/common.sail index 18828f230..7c6f19511 100644 --- 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 index f77baa605..7be5604da 100644 --- a/lib/float/inf.sail +++ b/lib/float/inf.sail @@ -35,8 +35,7 @@ $include 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 index 5befeac76..5961a5337 100644 --- 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 index 2fccb310e..42d0db845 100644 --- a/lib/float/nan.sail +++ b/lib/float/nan.sail @@ -35,28 +35,23 @@ $include 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 index d906a2774..7ba5fdd8d 100644 --- a/lib/float/normal.sail +++ b/lib/float/normal.sail @@ -35,8 +35,7 @@ $include 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 } @@ -44,8 +43,7 @@ function float_is_normal (op) = { 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 index cd8646128..1fd14fc98 100644 --- a/lib/float/sign.sail +++ b/lib/float/sign.sail @@ -34,16 +34,14 @@ $include 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 index 46ce4b1fc..924f95d0e 100644 --- a/lib/float/zero.sail +++ b/lib/float/zero.sail @@ -35,8 +35,7 @@ $include 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 }