From feb2e2d504a10ed574a64f53043d135f3ea0d5ab Mon Sep 17 00:00:00 2001
From: Tim Hutt <timothy.hutt@codasip.com>
Date: Fri, 11 Oct 2024 14:49:07 +0100
Subject: [PATCH] Fix and simplify fmv execute clauses

Simplify the implementations with fewer intermediate variables, and fix compilation of RV64F.

I also added relevant quote from the spec because the spec for these instructions is very confusing. This is a prime candidate for getting Sail code into the spec.
---
 model/riscv_insts_dext.sail | 12 ++++--------
 model/riscv_insts_fext.sail | 12 ++++++------
 2 files changed, 10 insertions(+), 14 deletions(-)

diff --git a/model/riscv_insts_dext.sail b/model/riscv_insts_dext.sail
index 40284831d..6341b3f63 100644
--- a/model/riscv_insts_dext.sail
+++ b/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
 }
 
diff --git a/model/riscv_insts_fext.sail b/model/riscv_insts_fext.sail
index c0d994d48..6541f2c8d 100644
--- a/model/riscv_insts_fext.sail
+++ b/model/riscv_insts_fext.sail
@@ -1056,16 +1056,16 @@ 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;
+  // A narrower n-bit transfer out of the floating-point registers will
+  // transfer the lower n bits of the register ignoring the upper FLEN-n bits.
+  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);
+  // A narrower n-bit transfer, n<FLEN, into the f registers will create a valid
+  // NaN-boxed value.
+  F(rd) = nan_box(X(rs1)[31..0]);
   RETIRE_SUCCESS
 }