From c7902ae840061ceb383e101d77d4afd440e9d284 Mon Sep 17 00:00:00 2001
From: Tim Hutt <timothy.hutt@codasip.com>
Date: Thu, 31 Oct 2024 21:56:52 +0000
Subject: [PATCH] Make nan boxing functions generic

This simplifies the code and allows easily supporting the Q extension.
---
 model/riscv_fdext_regs.sail          | 76 +++++++++++-----------------
 model/riscv_insts_vext_fp_utils.sail | 10 ----
 2 files changed, 29 insertions(+), 57 deletions(-)

diff --git a/model/riscv_fdext_regs.sail b/model/riscv_fdext_regs.sail
index bb6860121..00daea98a 100644
--- a/model/riscv_fdext_regs.sail
+++ b/model/riscv_fdext_regs.sail
@@ -15,55 +15,37 @@
 
 /* **************************************************************** */
 /* NaN boxing/unboxing.                                             */
-/* When 16-bit floats (half-precision) are stored in 32/64-bit regs  */
-/* they must be 'NaN boxed'.                                         */
-/* When 16-bit floats (half-precision) are read from 32/64-bit regs  */
-/* they must be 'NaN unboxed'.                                       */
-/* When 32-bit floats (single-precision) are stored in 64-bit regs  */
-/* they must be 'NaN boxed' (upper 32b all ones).                   */
-/* When 32-bit floats (single-precision) are read from 64-bit regs  */
-/* they must be 'NaN unboxed'.                                      */
-
-function canonical_NaN_H() -> bits(16) = 0x_7e00
-function canonical_NaN_S() -> bits(32) = 0x_7fc0_0000
-function canonical_NaN_D() -> bits(64) = 0x_7ff8_0000_0000_0000
-
-val      nan_box_H : bits(16) -> flenbits
-function nan_box_H   val_16b =
-  if (flen == 32)
-  then 0x_FFFF @ val_16b
-  else 0x_FFFF_FFFF_FFFF @ val_16b
-
-val      nan_unbox_H : flenbits -> bits(16)
-function nan_unbox_H   regval =
-  if (flen == 32)
-  then if regval [31..16] == 0x_FFFF
-       then regval [15..0]
-       else canonical_NaN_H()
-  else if regval [63..16] == 0x_FFFF_FFFF_FFFF
-       then regval [15..0]
-       else canonical_NaN_H()
-
-val nan_box_S : bits(32) -> flenbits
-function nan_box_S val_32b = {
-  assert(sys_enable_fdext());
-  if (flen == 32)
-  then val_32b
-  else 0x_FFFF_FFFF @ val_32b
-}
 
-val nan_unbox_S : flenbits -> bits(32)
-function nan_unbox_S regval = {
-  assert(sys_enable_fdext());
-  if (flen == 32)
-  then regval
-  else if regval [63..32] == 0x_FFFF_FFFF
-       then regval [31..0]
-       else canonical_NaN_S()
-}
+// Canonical NaNs are used when an invalid boxed value is unboxed.
+val canonical_NaN : forall 'n, 'n in {16, 32, 64, 128} . (implicit('n)) -> bits('n)
+function canonical_NaN(n) =
+  match 'n {
+    //     sign  exponent    significand
+    16  => 0b0 @ ones(5)  @ 0b1 @ zeros(9),
+    32  => 0b0 @ ones(8)  @ 0b1 @ zeros(22),
+    64  => 0b0 @ ones(11) @ 0b1 @ zeros(51),
+    128 => 0b0 @ ones(15) @ 0b1 @ zeros(111),
+  }
 
-overload nan_box = { nan_box_H, nan_box_S }
-overload nan_unbox = { nan_unbox_H, nan_unbox_S }
+// For backwards compatibility with code that existed before the
+// generic version above.
+function canonical_NaN_H() -> bits(16)  = canonical_NaN(16)
+function canonical_NaN_S() -> bits(32)  = canonical_NaN(32)
+function canonical_NaN_D() -> bits(64)  = canonical_NaN(64)
+function canonical_NaN_Q() -> bits(128) = canonical_NaN(128)
+
+// When an n-bit float is stored in a larger m-bit register it is "boxed"
+// by prepending 1s, which make it appear as a qNaN.
+val nan_box : forall 'n 'm, 'n <= 'm . (implicit('m), bits('n)) -> bits('m)
+function nan_box(n, x) = ones('m - 'n) @ x
+
+// When an n-bit float is stored ina smaller m-bit register it is "unboxed"
+// - only if it is a valid boxed NaN. Otherwise a canonical NaN value is stored.
+// TODO: Use right-open interval when available. See https://github.com/rems-project/sail/issues/471
+val nan_unbox : forall 'n 'm, 'm in {16, 32, 64, 128} & 'n >= 'm . (implicit('m), bits('n)) -> bits('m)
+function nan_unbox(m, x) = if 'n == 'm then x else (
+  if x['n - 1 .. 'm] == ones() then x['m - 1 .. 0] else canonical_NaN()
+)
 
 /* **************************************************************** */
 /* Floating point register file                                     */
diff --git a/model/riscv_insts_vext_fp_utils.sail b/model/riscv_insts_vext_fp_utils.sail
index d8e10d2e7..931e457c2 100755
--- a/model/riscv_insts_vext_fp_utils.sail
+++ b/model/riscv_insts_vext_fp_utils.sail
@@ -60,16 +60,6 @@ function illegal_fp_reduction_widen(SEW, rm_3b, SEW_widen, LMUL_pow_widen) = {
   not(valid_eew_emul(SEW_widen, LMUL_pow_widen))
 }
 
-/* Floating point canonical NaN for 16-bit, 32-bit and 64-bit types */
-val canonical_NaN : forall 'm, 'm in {16, 32, 64}. int('m) -> bits('m)
-function canonical_NaN('m) = {
-  match 'm {
-    16 => canonical_NaN_H(),
-    32 => canonical_NaN_S(),
-    64 => canonical_NaN_D()
-  }
-}
-
 /* Floating point classification functions */
 val f_is_neg_inf : forall 'm, 'm in {16, 32, 64}. bits('m) -> bool
 function f_is_neg_inf(xf) = {