Fix RV64F compilation, simplify fmv implementation, and make nan boxing functions generic

model/riscv_fdext_regs.sail

@@ -15,55 +15,39 @@
 
 /* **************************************************************** */
 /* 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)
+
+// n-bit writes to a >n-bit floating point register "box" the value
+// by prepending 1s, which turn it into 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
+
+// Except for floating-point transfer instructions (FSn and FMV.n.X),
+// n-bit reads of a >n-bit floating point register "unbox" the value stored
+// in the register. If the register does not contain a valid boxed value
+// then a canonical NaN value is returned instead.
+// 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                                     */

model/riscv_insts_dext.sail

@@ -934,18 +934,14 @@ function clause execute (F_UN_TYPE_D(rs1, rd, FCLASS_D)) = {
 }
 
 function clause execute (F_UN_TYPE_D(rs1, rd, FMV_X_D)) = {
-  assert(xlen >= 64);
-  let rs1_val_D            = F(rs1)[63..0];
-  let rd_val_X  : xlenbits = sign_extend(rs1_val_D);
-  X(rd) = rd_val_X;
+  assert(xlen >= 64 & flen >= 64);
+  X(rd) = sign_extend(F(rs1)[63..0]);
   RETIRE_SUCCESS
 }
 
 function clause execute (F_UN_TYPE_D(rs1, rd, FMV_D_X)) = {
-  assert(xlen >= 64);
-  let rs1_val_X            = X(rs1);
-  let rd_val_D             = rs1_val_X [63..0];
-  F(rd) = rd_val_D;
+  assert(xlen >= 64 & flen >= 64);
+  F(rd) = nan_box(X(rs1)[63..0]);
   RETIRE_SUCCESS
 }
 

model/riscv_insts_fext.sail

@@ -1061,16 +1061,12 @@ function clause execute (F_UN_TYPE_S(rs1, rd, FCLASS_S)) = {
 }
 
 function clause execute (F_UN_TYPE_S(rs1, rd, FMV_X_W)) = {
-  let rs1_val_S            = F(rs1)[31..0];
-  let rd_val_X  : xlenbits = sign_extend(rs1_val_S);
-  X(rd) = rd_val_X;
+  X(rd) = sign_extend(F(rs1)[31..0]);
   RETIRE_SUCCESS
 }
 
 function clause execute (F_UN_TYPE_S(rs1, rd, FMV_W_X)) = {
-  let rs1_val_X            = X(rs1);
-  let rd_val_S             = rs1_val_X [31..0];
-  F(rd) = nan_box (rd_val_S);
+  F(rd) = nan_box(X(rs1)[31..0]);
   RETIRE_SUCCESS
 }
 

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) = {