Add support for Zhinx extension (#153)

Merged after code review. Thanks everybody for helping.

3 files changed, 180 insertions, 155 deletions

diff --git a/model/riscv_fdext_regs.sail b/model/riscv_fdext_regs.sail
index d3b3b43..e01a805 100644
--- a/model/riscv_fdext_regs.sail
+++ b/model/riscv_fdext_regs.sail
@@ -270,6 +270,15 @@ function wF_bits(i: bits(5), data: flenbits) -> unit = {
 
 overload F = {rF_bits, wF_bits, rF, wF}
 
+val rF_or_X_H : bits(5) -> bits(16) effect {escape, rreg}
+function rF_or_X_H(i) = {
+  assert(sizeof(flen) >= 16);
+  assert(sys_enable_fdext() != sys_enable_zfinx());
+  if   sys_enable_fdext()
+  then nan_unbox(F(i))
+  else X(i)[15..0]
+}
+
 val rF_or_X_S : bits(5) -> bits(32) effect {escape, rreg}
 function rF_or_X_S(i) = {
   assert(sizeof(flen) >= 32);
@@ -293,6 +302,15 @@ function rF_or_X_D(i) = {
   }
 }
 
+val wF_or_X_H : (bits(5), bits(16)) -> unit effect {escape, wreg}
+function wF_or_X_H(i, data) = {
+  assert(sizeof(flen) >= 16);
+  assert(sys_enable_fdext() != sys_enable_zfinx());
+  if   sys_enable_fdext()
+  then F(i) = nan_box(data)
+  else X(i) = EXTS(data)
+}
+
 val wF_or_X_S : (bits(5), bits(32)) -> unit effect {escape, wreg}
 function wF_or_X_S(i, data) = {
   assert(sizeof(flen) >= 32);
@@ -319,6 +337,7 @@ function wF_or_X_D(i, data) = {
   }
 }
 
+overload F_or_X_H = { rF_or_X_H, wF_or_X_H }
 overload F_or_X_S = { rF_or_X_S, wF_or_X_S }
 overload F_or_X_D = { rF_or_X_D, wF_or_X_D }
 
diff --git a/model/riscv_insts_zfh.sail b/model/riscv_insts_zfh.sail
index b825711..9bb06cb 100644
--- a/model/riscv_insts_zfh.sail
+++ b/model/riscv_insts_zfh.sail
@@ -151,6 +151,11 @@ function fle_H   (v1,       v2,        is_quiet) = {
   (result, fflags)
 }
 
+/* **************************************************************** */
+/* Helper functions for 'encdec()'                                  */
+
+function haveHalfFPU() -> bool = haveZfh() | haveZhinx()
+
 /* ****************************************************************** */
 /* Floating-point loads                                               */
 /* These are defined in: riscv_insts_fext.sail                        */
@@ -168,26 +173,26 @@ union clause ast = F_BIN_RM_TYPE_H : (regidx, regidx, rounding_mode, regidx, f_b
 /* AST <-> Binary encoding ================================ */
 
 mapping clause encdec =
-    F_BIN_RM_TYPE_H(rs2, rs1, rm, rd, FADD_H)                             if haveZfh()
-<-> 0b000_0010 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if haveZfh()
+    F_BIN_RM_TYPE_H(rs2, rs1, rm, rd, FADD_H)                             if haveHalfFPU()
+<-> 0b000_0010 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if haveHalfFPU()
 
 mapping clause encdec =
-    F_BIN_RM_TYPE_H(rs2, rs1, rm, rd, FSUB_H)                             if haveZfh()
-<-> 0b000_0110 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if haveZfh()
+    F_BIN_RM_TYPE_H(rs2, rs1, rm, rd, FSUB_H)                             if haveHalfFPU()
+<-> 0b000_0110 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if haveHalfFPU()
 
 mapping clause encdec =
-    F_BIN_RM_TYPE_H(rs2, rs1, rm, rd, FMUL_H)                             if haveZfh()
-<-> 0b000_1010 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if haveZfh()
+    F_BIN_RM_TYPE_H(rs2, rs1, rm, rd, FMUL_H)                             if haveHalfFPU()
+<-> 0b000_1010 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if haveHalfFPU()
 
 mapping clause encdec =
-    F_BIN_RM_TYPE_H(rs2, rs1, rm, rd, FDIV_H)                             if haveZfh()
-<-> 0b000_1110 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if haveZfh()
+    F_BIN_RM_TYPE_H(rs2, rs1, rm, rd, FDIV_H)                             if haveHalfFPU()
+<-> 0b000_1110 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if haveHalfFPU()
 
 /* Execution semantics ================================ */
 
 function clause execute (F_BIN_RM_TYPE_H(rs2, rs1, rm, rd, op)) = {
-  let rs1_val_16b = nan_unbox_H (F(rs1));
-  let rs2_val_16b = nan_unbox_H (F(rs2));
+  let rs1_val_16b = F_or_X_H(rs1);
+  let rs2_val_16b = F_or_X_H(rs2);
   match (select_instr_or_fcsr_rm (rm)) {
     None() => { handle_illegal(); RETIRE_FAIL },
     Some(rm') => {
@@ -199,7 +204,7 @@ function clause execute (F_BIN_RM_TYPE_H(rs2, rs1, rm, rd, op)) = {
         FDIV_H  => riscv_f16Div (rm_3b, rs1_val_16b, rs2_val_16b)
       };
       write_fflags(fflags);
-      F(rd) = nan_box (rd_val_16b);
+      F_or_X_H(rd) = rd_val_16b;
       RETIRE_SUCCESS
     }
   }
@@ -216,9 +221,9 @@ mapping f_bin_rm_type_mnemonic_H : f_bin_rm_op_H <-> string = {
 
 mapping clause assembly = F_BIN_RM_TYPE_H(rs2, rs1, rm, rd, op)
                       <-> f_bin_rm_type_mnemonic_H(op)
-                          ^ spc() ^ freg_name(rd)
-                          ^ sep() ^ freg_name(rs1)
-                          ^ sep() ^ freg_name(rs2)
+                          ^ spc() ^ freg_or_reg_name(rd)
+                          ^ sep() ^ freg_or_reg_name(rs1)
+                          ^ sep() ^ freg_or_reg_name(rs2)
                           ^ sep() ^ frm_mnemonic(rm)
 
 /* ****************************************************************** */
@@ -231,27 +236,27 @@ union clause ast = F_MADD_TYPE_H : (regidx, regidx, regidx, rounding_mode, regid
 /* AST <-> Binary encoding ================================ */
 
 mapping clause encdec =
-    F_MADD_TYPE_H(rs3, rs2, rs1, rm, rd, FMADD_H)                         if haveZfh()
-<-> rs3 @ 0b10 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_0011  if haveZfh()
+    F_MADD_TYPE_H(rs3, rs2, rs1, rm, rd, FMADD_H)                         if haveHalfFPU()
+<-> rs3 @ 0b10 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_0011  if haveHalfFPU()
 
 mapping clause encdec =
-    F_MADD_TYPE_H(rs3, rs2, rs1, rm, rd, FMSUB_H)                         if haveZfh()
-<-> rs3 @ 0b10 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_0111  if haveZfh()
+    F_MADD_TYPE_H(rs3, rs2, rs1, rm, rd, FMSUB_H)                         if haveHalfFPU()
+<-> rs3 @ 0b10 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_0111  if haveHalfFPU()
 
 mapping clause encdec =
-    F_MADD_TYPE_H(rs3, rs2, rs1, rm, rd, FNMSUB_H)                        if haveZfh()
-<-> rs3 @ 0b10 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_1011  if haveZfh()
+    F_MADD_TYPE_H(rs3, rs2, rs1, rm, rd, FNMSUB_H)                        if haveHalfFPU()
+<-> rs3 @ 0b10 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_1011  if haveHalfFPU()
 
 mapping clause encdec =
-    F_MADD_TYPE_H(rs3, rs2, rs1, rm, rd, FNMADD_H)                        if haveZfh()
-<-> rs3 @ 0b10 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_1111  if haveZfh()
+    F_MADD_TYPE_H(rs3, rs2, rs1, rm, rd, FNMADD_H)                        if haveHalfFPU()
+<-> rs3 @ 0b10 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_1111  if haveHalfFPU()
 
 /* Execution semantics ================================ */
 
 function clause execute (F_MADD_TYPE_H(rs3, rs2, rs1, rm, rd, op)) = {
-  let rs1_val_16b = nan_unbox_H (F(rs1));
-  let rs2_val_16b = nan_unbox_H (F(rs2));
-  let rs3_val_16b = nan_unbox_H (F(rs3));
+  let rs1_val_16b = F_or_X_H(rs1);
+  let rs2_val_16b = F_or_X_H(rs2);
+  let rs3_val_16b = F_or_X_H(rs3);
   match (select_instr_or_fcsr_rm (rm)) {
     None() => { handle_illegal(); RETIRE_FAIL },
     Some(rm') => {
@@ -264,7 +269,7 @@ function clause execute (F_MADD_TYPE_H(rs3, rs2, rs1, rm, rd, op)) = {
           FNMADD_H => riscv_f16MulAdd (rm_3b, negate_H (rs1_val_16b), rs2_val_16b, negate_H (rs3_val_16b))
         };
       write_fflags(fflags);
-      F(rd) = nan_box (rd_val_16b);
+      F_or_X_H(rd) = rd_val_16b;
       RETIRE_SUCCESS
     }
   }
@@ -281,10 +286,10 @@ mapping f_madd_type_mnemonic_H : f_madd_op_H <-> string = {
 
 mapping clause assembly = F_MADD_TYPE_H(rs3, rs2, rs1, rm, rd, op)
                       <-> f_madd_type_mnemonic_H(op)
-                          ^ spc() ^ freg_name(rd)
-                          ^ sep() ^ freg_name(rs1)
-                          ^ sep() ^ freg_name(rs2)
-                          ^ sep() ^ freg_name(rs3)
+                          ^ spc() ^ freg_or_reg_name(rd)
+                          ^ sep() ^ freg_or_reg_name(rs1)
+                          ^ sep() ^ freg_or_reg_name(rs2)
+                          ^ sep() ^ freg_or_reg_name(rs3)
                           ^ sep() ^ frm_mnemonic(rm)
 
 /* ****************************************************************** */
@@ -296,68 +301,68 @@ union clause ast = F_BIN_TYPE_H : (regidx, regidx, regidx, f_bin_op_H)
 
 /* AST <-> Binary encoding ================================ */
 
-mapping clause encdec = F_BIN_TYPE_H(rs2, rs1, rd, FSGNJ_H)               if haveZfh()
-                    <-> 0b001_0010 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011  if haveZfh()
+mapping clause encdec = F_BIN_TYPE_H(rs2, rs1, rd, FSGNJ_H)               if haveHalfFPU()
+                    <-> 0b001_0010 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011  if haveHalfFPU()
 
-mapping clause encdec = F_BIN_TYPE_H(rs2, rs1, rd, FSGNJN_H)              if haveZfh()
-                    <-> 0b001_0010 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011  if haveZfh()
+mapping clause encdec = F_BIN_TYPE_H(rs2, rs1, rd, FSGNJN_H)              if haveHalfFPU()
+                    <-> 0b001_0010 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011  if haveHalfFPU()
 
-mapping clause encdec = F_BIN_TYPE_H(rs2, rs1, rd, FSGNJX_H)              if haveZfh()
-                    <-> 0b001_0010 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011  if haveZfh()
+mapping clause encdec = F_BIN_TYPE_H(rs2, rs1, rd, FSGNJX_H)              if haveHalfFPU()
+                    <-> 0b001_0010 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011  if haveHalfFPU()
 
-mapping clause encdec = F_BIN_TYPE_H(rs2, rs1, rd, FMIN_H)                if haveZfh()
-                    <-> 0b001_0110 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011  if haveZfh()
+mapping clause encdec = F_BIN_TYPE_H(rs2, rs1, rd, FMIN_H)                if haveHalfFPU()
+                    <-> 0b001_0110 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011  if haveHalfFPU()
 
-mapping clause encdec = F_BIN_TYPE_H(rs2, rs1, rd, FMAX_H)                if haveZfh()
-                    <-> 0b001_0110 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011  if haveZfh()
+mapping clause encdec = F_BIN_TYPE_H(rs2, rs1, rd, FMAX_H)                if haveHalfFPU()
+                    <-> 0b001_0110 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011  if haveHalfFPU()
 
-mapping clause encdec = F_BIN_TYPE_H(rs2, rs1, rd, FEQ_H)                 if haveZfh()
-                    <-> 0b101_0010 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011  if haveZfh()
+mapping clause encdec = F_BIN_TYPE_H(rs2, rs1, rd, FEQ_H)                 if haveHalfFPU()
+                    <-> 0b101_0010 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011  if haveHalfFPU()
 
-mapping clause encdec = F_BIN_TYPE_H(rs2, rs1, rd, FLT_H)                 if haveZfh()
-                    <-> 0b101_0010 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011  if haveZfh()
+mapping clause encdec = F_BIN_TYPE_H(rs2, rs1, rd, FLT_H)                 if haveHalfFPU()
+                    <-> 0b101_0010 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011  if haveHalfFPU()
 
-mapping clause encdec = F_BIN_TYPE_H(rs2, rs1, rd, FLE_H)                 if haveZfh()
-                    <-> 0b101_0010 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011  if haveZfh()
+mapping clause encdec = F_BIN_TYPE_H(rs2, rs1, rd, FLE_H)                 if haveHalfFPU()
+                    <-> 0b101_0010 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011  if haveHalfFPU()
 
 /* Execution semantics ================================ */
 
 function clause execute (F_BIN_TYPE_H(rs2, rs1, rd, FSGNJ_H)) = {
-  let rs1_val_H    = nan_unbox_H (F(rs1));
-  let rs2_val_H    = nan_unbox_H (F(rs2));
+  let rs1_val_H    = F_or_X_H(rs1);
+  let rs2_val_H    = F_or_X_H(rs2);
   let (s1, e1, m1) = fsplit_H (rs1_val_H);
   let (s2, e2, m2) = fsplit_H (rs2_val_H);
   let rd_val_H     = fmake_H (s2, e1, m1);
 
-  F(rd) = nan_box (rd_val_H);
+  F_or_X_H(rd) = rd_val_H;
   RETIRE_SUCCESS
 }
 
 function clause execute (F_BIN_TYPE_H(rs2, rs1, rd, FSGNJN_H)) = {
-  let rs1_val_H    = nan_unbox_H (F(rs1));
-  let rs2_val_H    = nan_unbox_H (F(rs2));
+  let rs1_val_H    = F_or_X_H(rs1);
+  let rs2_val_H    = F_or_X_H(rs2);
   let (s1, e1, m1) = fsplit_H (rs1_val_H);
   let (s2, e2, m2) = fsplit_H (rs2_val_H);
   let rd_val_H     = fmake_H (0b1 ^ s2, e1, m1);
 
-  F(rd) = nan_box (rd_val_H);
+  F_or_X_H(rd) = rd_val_H;
   RETIRE_SUCCESS
 }
 
 function clause execute (F_BIN_TYPE_H(rs2, rs1, rd, FSGNJX_H)) = {
-  let rs1_val_H    = nan_unbox_H (F(rs1));
-  let rs2_val_H    = nan_unbox_H (F(rs2));
+  let rs1_val_H    = F_or_X_H(rs1);
+  let rs2_val_H    = F_or_X_H(rs2);
   let (s1, e1, m1) = fsplit_H (rs1_val_H);
   let (s2, e2, m2) = fsplit_H (rs2_val_H);
   let rd_val_H     = fmake_H (s1 ^ s2, e1, m1);
 
-  F(rd) = nan_box (rd_val_H);
+  F_or_X_H(rd) = rd_val_H;
   RETIRE_SUCCESS
 }
 
 function clause execute (F_BIN_TYPE_H(rs2, rs1, rd, FMIN_H)) = {
-  let rs1_val_H = nan_unbox_H (F(rs1));
-  let rs2_val_H = nan_unbox_H (F(rs2));
+  let rs1_val_H = F_or_X_H(rs1);
+  let rs2_val_H = F_or_X_H(rs2);
 
   let is_quiet  = true;
   let (rs1_lt_rs2, fflags) = fle_H (rs1_val_H, rs2_val_H, is_quiet);
@@ -371,13 +376,13 @@ function clause execute (F_BIN_TYPE_H(rs2, rs1, rd, FMIN_H)) = {
                   else /* (not rs1_lt_rs2) */                                            rs2_val_H;
 
   accrue_fflags(fflags);
-  F(rd) = nan_box (rd_val_H);
+  F_or_X_H(rd) = rd_val_H;
   RETIRE_SUCCESS
 }
 
 function clause execute (F_BIN_TYPE_H(rs2, rs1, rd, FMAX_H)) = {
-  let rs1_val_H = nan_unbox_H (F(rs1));
-  let rs2_val_H = nan_unbox_H (F(rs2));
+  let rs1_val_H = F_or_X_H(rs1);
+  let rs2_val_H = F_or_X_H(rs2);
 
   let is_quiet  = true;
   let (rs2_lt_rs1, fflags) = fle_H (rs2_val_H, rs1_val_H, is_quiet);
@@ -391,13 +396,13 @@ function clause execute (F_BIN_TYPE_H(rs2, rs1, rd, FMAX_H)) = {
                   else /* (not rs2_lt_rs1) */                                            rs2_val_H;
 
   accrue_fflags(fflags);
-  F(rd) = nan_box (rd_val_H);
+  F_or_X_H(rd) = rd_val_H;
   RETIRE_SUCCESS
 }
 
 function clause execute (F_BIN_TYPE_H(rs2, rs1, rd, FEQ_H)) = {
-  let rs1_val_H = nan_unbox_H (F(rs1));
-  let rs2_val_H = nan_unbox_H (F(rs2));
+  let rs1_val_H = F_or_X_H(rs1);
+  let rs2_val_H = F_or_X_H(rs2);
 
   let (fflags, rd_val) : (bits_fflags, bool) =
       riscv_f16Eq (rs1_val_H, rs2_val_H);
@@ -408,8 +413,8 @@ function clause execute (F_BIN_TYPE_H(rs2, rs1, rd, FEQ_H)) = {
 }
 
 function clause execute (F_BIN_TYPE_H(rs2, rs1, rd, FLT_H)) = {
-  let rs1_val_H = nan_unbox_H (F(rs1));
-  let rs2_val_H = nan_unbox_H (F(rs2));
+  let rs1_val_H = F_or_X_H(rs1);
+  let rs2_val_H = F_or_X_H(rs2);
 
   let (fflags, rd_val) : (bits_fflags, bool) =
       riscv_f16Lt (rs1_val_H, rs2_val_H);
@@ -420,8 +425,8 @@ function clause execute (F_BIN_TYPE_H(rs2, rs1, rd, FLT_H)) = {
 }
 
 function clause execute (F_BIN_TYPE_H(rs2, rs1, rd, FLE_H)) = {
-  let rs1_val_H = nan_unbox_H (F(rs1));
-  let rs2_val_H = nan_unbox_H (F(rs2));
+  let rs1_val_H = F_or_X_H(rs1);
+  let rs2_val_H = F_or_X_H(rs2);
 
   let (fflags, rd_val) : (bits_fflags, bool) =
       riscv_f16Le (rs1_val_H, rs2_val_H);
@@ -446,51 +451,51 @@ mapping f_bin_type_mnemonic_H : f_bin_op_H <-> string = {
 
 mapping clause assembly = F_BIN_TYPE_H(rs2, rs1, rd, FSGNJ_H)
                       <-> f_bin_type_mnemonic_H(FSGNJ_H)
-                          ^ spc() ^ freg_name(rd)
-                          ^ sep() ^ freg_name(rs1)
-                          ^ sep() ^ freg_name(rs2)
+                          ^ spc() ^ freg_or_reg_name(rd)
+                          ^ sep() ^ freg_or_reg_name(rs1)
+                          ^ sep() ^ freg_or_reg_name(rs2)
 
 mapping clause assembly = F_BIN_TYPE_H(rs2, rs1, rd, FSGNJN_H)
                       <-> f_bin_type_mnemonic_H(FSGNJN_H)
-                          ^ spc() ^ freg_name(rd)
-                          ^ sep() ^ freg_name(rs1)
-                          ^ sep() ^ freg_name(rs2)
+                          ^ spc() ^ freg_or_reg_name(rd)
+                          ^ sep() ^ freg_or_reg_name(rs1)
+                          ^ sep() ^ freg_or_reg_name(rs2)
 
 mapping clause assembly = F_BIN_TYPE_H(rs2, rs1, rd, FSGNJX_H)
                       <-> f_bin_type_mnemonic_H(FSGNJX_H)
-                          ^ spc() ^ freg_name(rd)
-                          ^ sep() ^ freg_name(rs1)
-                          ^ sep() ^ freg_name(rs2)
+                          ^ spc() ^ freg_or_reg_name(rd)
+                          ^ sep() ^ freg_or_reg_name(rs1)
+                          ^ sep() ^ freg_or_reg_name(rs2)
 
 mapping clause assembly = F_BIN_TYPE_H(rs2, rs1, rd, FMIN_H)
                       <-> f_bin_type_mnemonic_H(FMIN_H)
-                          ^ spc() ^ freg_name(rd)
-                          ^ sep() ^ freg_name(rs1)
-                          ^ sep() ^ freg_name(rs2)
+                          ^ spc() ^ freg_or_reg_name(rd)
+                          ^ sep() ^ freg_or_reg_name(rs1)
+                          ^ sep() ^ freg_or_reg_name(rs2)
 
 mapping clause assembly = F_BIN_TYPE_H(rs2, rs1, rd, FMAX_H)
                       <-> f_bin_type_mnemonic_H(FMAX_H)
-                          ^ spc() ^ freg_name(rd)
-                          ^ sep() ^ freg_name(rs1)
-                          ^ sep() ^ freg_name(rs2)
+                          ^ spc() ^ freg_or_reg_name(rd)
+                          ^ sep() ^ freg_or_reg_name(rs1)
+                          ^ sep() ^ freg_or_reg_name(rs2)
 
 mapping clause assembly = F_BIN_TYPE_H(rs2, rs1, rd, FEQ_H)
                       <-> f_bin_type_mnemonic_H(FEQ_H)
                           ^ spc() ^ reg_name(rd)
-                          ^ sep() ^ freg_name(rs1)
-                          ^ sep() ^ freg_name(rs2)
+                          ^ sep() ^ freg_or_reg_name(rs1)
+                          ^ sep() ^ freg_or_reg_name(rs2)
 
 mapping clause assembly = F_BIN_TYPE_H(rs2, rs1, rd, FLT_H)
                       <-> f_bin_type_mnemonic_H(FLT_H)
                           ^ spc() ^ reg_name(rd)
-                          ^ sep() ^ freg_name(rs1)
-                          ^ sep() ^ freg_name(rs2)
+                          ^ sep() ^ freg_or_reg_name(rs1)
+                          ^ sep() ^ freg_or_reg_name(rs2)
 
 mapping clause assembly = F_BIN_TYPE_H(rs2, rs1, rd, FLE_H)
                       <-> f_bin_type_mnemonic_H(FLE_H)
                           ^ spc() ^ reg_name(rd)
-                          ^ sep() ^ freg_name(rs1)
-                          ^ sep() ^ freg_name(rs2)
+                          ^ sep() ^ freg_or_reg_name(rs1)
+                          ^ sep() ^ freg_or_reg_name(rs2)
 
 /* ****************************************************************** */
 /* Unary with rounding mode */
@@ -502,40 +507,40 @@ union clause ast = F_UN_RM_TYPE_H : (regidx, rounding_mode, regidx, f_un_rm_op_H
 /* AST <-> Binary encoding ================================ */
 
 mapping clause encdec =
-    F_UN_RM_TYPE_H(rs1, rm, rd, FSQRT_H)                                      if haveZfh()
-<-> 0b010_1110 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if haveZfh()
+    F_UN_RM_TYPE_H(rs1, rm, rd, FSQRT_H)                                      if haveHalfFPU()
+<-> 0b010_1110 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if haveHalfFPU()
 
 mapping clause encdec =
-    F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_W_H)                                     if haveZfh()
-<-> 0b110_0010 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if haveZfh()
+    F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_W_H)                                     if haveHalfFPU()
+<-> 0b110_0010 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if haveHalfFPU()
 
 mapping clause encdec =
-    F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_WU_H)                                    if haveZfh()
-<-> 0b110_0010 @ 0b00001 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if haveZfh()
+    F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_WU_H)                                    if haveHalfFPU()
+<-> 0b110_0010 @ 0b00001 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if haveHalfFPU()
 
 mapping clause encdec =
-    F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_W)                                     if haveZfh()
-<-> 0b110_1010 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if haveZfh()
+    F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_W)                                     if haveHalfFPU()
+<-> 0b110_1010 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if haveHalfFPU()
 
 mapping clause encdec =
-    F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_WU)                                    if haveZfh()
-<-> 0b110_1010 @ 0b00001 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if haveZfh()
+    F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_WU)                                    if haveHalfFPU()
+<-> 0b110_1010 @ 0b00001 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if haveHalfFPU()
 
 mapping clause encdec =
-    F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_S)                                     if haveZfh()
-<-> 0b010_0010 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if haveZfh()
+    F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_S)                                     if haveHalfFPU()
+<-> 0b010_0010 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if haveHalfFPU()
 
 mapping clause encdec =
-    F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_D)                                     if haveZfh()
-<-> 0b010_0010 @ 0b00001 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if haveZfh()
+    F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_D)                                     if haveHalfFPU()
+<-> 0b010_0010 @ 0b00001 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if haveHalfFPU()
 
 mapping clause encdec =
-    F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_S_H)                                     if haveZfh()
-<-> 0b010_0000 @ 0b00010 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if haveZfh()
+    F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_S_H)                                     if haveHalfFPU()
+<-> 0b010_0000 @ 0b00010 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if haveHalfFPU()
 
 mapping clause encdec =
-    F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_D_H)                                     if haveZfh()
-<-> 0b010_0001 @ 0b00010 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if haveZfh()
+    F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_D_H)                                     if haveHalfFPU()
+<-> 0b010_0001 @ 0b00010 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if haveHalfFPU()
 
 // TODO:
 /* FCVT_H_Q, FCVT_Q_H : Will be added with Q Extension */
@@ -543,25 +548,25 @@ mapping clause encdec =
 /* F instructions, RV64 only */
 
 mapping clause encdec =
-    F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_L_H)                                     if haveZfh() & sizeof(xlen) >= 64
-<-> 0b110_0010 @ 0b00010 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if haveZfh() & sizeof(xlen) >= 64
+    F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_L_H)                                     if haveHalfFPU() & sizeof(xlen) >= 64
+<-> 0b110_0010 @ 0b00010 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if haveHalfFPU() & sizeof(xlen) >= 64
 
 mapping clause encdec =
-    F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_LU_H)                                    if haveZfh() & sizeof(xlen) >= 64
-<-> 0b110_0010 @ 0b00011 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if haveZfh() & sizeof(xlen) >= 64
+    F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_LU_H)                                    if haveHalfFPU() & sizeof(xlen) >= 64
+<-> 0b110_0010 @ 0b00011 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if haveHalfFPU() & sizeof(xlen) >= 64
 
 mapping clause encdec =
-    F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_L)                                     if haveZfh() & sizeof(xlen) >= 64
-<-> 0b110_1010 @ 0b00010 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if haveZfh() & sizeof(xlen) >= 64
+    F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_L)                                     if haveHalfFPU() & sizeof(xlen) >= 64
+<-> 0b110_1010 @ 0b00010 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if haveHalfFPU() & sizeof(xlen) >= 64
 
 mapping clause encdec =
-    F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_LU)                                    if haveZfh() & sizeof(xlen) >= 64
-<-> 0b110_1010 @ 0b00011 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if haveZfh() & sizeof(xlen) >= 64
+    F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_LU)                                    if haveHalfFPU() & sizeof(xlen) >= 64
+<-> 0b110_1010 @ 0b00011 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if haveHalfFPU() & sizeof(xlen) >= 64
 
 /* Execution semantics ================================ */
 
 function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FSQRT_H)) = {
-  let rs1_val_H = nan_unbox_H (F(rs1));
+  let rs1_val_H = F_or_X_H(rs1);
   match (select_instr_or_fcsr_rm (rm)) {
     None() => { handle_illegal(); RETIRE_FAIL },
     Some(rm') => {
@@ -569,14 +574,14 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FSQRT_H)) = {
       let (fflags, rd_val_H) = riscv_f16Sqrt   (rm_3b, rs1_val_H);
 
       write_fflags(fflags);
-      F(rd) = nan_box (rd_val_H);
+      F_or_X_H(rd) = rd_val_H;
       RETIRE_SUCCESS
     }
   }
 }
 
 function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_W_H)) = {
-  let rs1_val_H = nan_unbox_H (F(rs1));
+  let rs1_val_H = F_or_X_H(rs1);
   match (select_instr_or_fcsr_rm (rm)) {
     None() => { handle_illegal(); RETIRE_FAIL },
     Some(rm') => {
@@ -591,7 +596,7 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_W_H)) = {
 }
 
 function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_WU_H)) = {
-  let rs1_val_H = nan_unbox_H (F(rs1));
+  let rs1_val_H = F_or_X_H(rs1);
   match (select_instr_or_fcsr_rm (rm)) {
     None() => { handle_illegal(); RETIRE_FAIL },
     Some(rm') => {
@@ -614,7 +619,7 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_W)) = {
       let (fflags, rd_val_H) = riscv_i32ToF16 (rm_3b, rs1_val_W);
 
       write_fflags(fflags);
-      F(rd) = nan_box (rd_val_H);
+      F_or_X_H(rd) = rd_val_H;
       RETIRE_SUCCESS
     }
   }
@@ -629,14 +634,14 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_WU)) = {
       let (fflags, rd_val_H) = riscv_ui32ToF16 (rm_3b, rs1_val_WU);
 
       write_fflags(fflags);
-      F(rd) = nan_box (rd_val_H);
+      F_or_X_H(rd) = rd_val_H;
       RETIRE_SUCCESS
     }
   }
 }
 
 function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_S)) = {
-  let rs1_val_S = nan_unbox_S (F(rs1));
+  let rs1_val_S = F_or_X_S(rs1);
   match (select_instr_or_fcsr_rm (rm)) {
     None() => { handle_illegal(); RETIRE_FAIL },
     Some(rm') => {
@@ -644,14 +649,14 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_S)) = {
       let (fflags, rd_val_H) = riscv_f32ToF16 (rm_3b, rs1_val_S);
 
       write_fflags(fflags);
-      F(rd) = nan_box (rd_val_H);
+      F_or_X_H(rd) = rd_val_H;
       RETIRE_SUCCESS
     }
   }
 }
 
 function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_D)) = {
-  let rs1_val_D = F(rs1);
+  let rs1_val_D = F_or_X_D(rs1);
   match (select_instr_or_fcsr_rm (rm)) {
     None() => { handle_illegal(); RETIRE_FAIL },
     Some(rm') => {
@@ -659,14 +664,14 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_D)) = {
       let (fflags, rd_val_H) = riscv_f64ToF16 (rm_3b, rs1_val_D);
 
       write_fflags(fflags);
-      F(rd) = nan_box (rd_val_H);
+      F_or_X_H(rd) = rd_val_H;
       RETIRE_SUCCESS
     }
   }
 }
 
 function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_S_H)) = {
-  let rs1_val_H = nan_unbox_H (F(rs1));
+  let rs1_val_H = F_or_X_H(rs1);
   match (select_instr_or_fcsr_rm (rm)) {
     None() => { handle_illegal(); RETIRE_FAIL },
     Some(rm') => {
@@ -674,7 +679,7 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_S_H)) = {
       let (fflags, rd_val_S) = riscv_f16ToF32 (rm_3b, rs1_val_H);
 
       write_fflags(fflags);
-      F(rd) = nan_box (rd_val_S);
+      F_or_X_S(rd) = rd_val_S;
       RETIRE_SUCCESS
     }
   }
@@ -682,7 +687,7 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_S_H)) = {
 
 
 function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_D_H)) = {
-  let rs1_val_H = nan_unbox_H (F(rs1));
+  let rs1_val_H = F_or_X_H(rs1);
   match (select_instr_or_fcsr_rm (rm)) {
     None() => { handle_illegal(); RETIRE_FAIL },
     Some(rm') => {
@@ -690,7 +695,7 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_D_H)) = {
       let (fflags, rd_val_D) = riscv_f16ToF64 (rm_3b, rs1_val_H);
 
       write_fflags(fflags);
-      F(rd) = rd_val_D;
+      F_or_X_D(rd) = rd_val_D;
       RETIRE_SUCCESS
     }
   }
@@ -698,7 +703,7 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_D_H)) = {
 
 function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_L_H)) = {
   assert(sizeof(xlen) >= 64);
-  let rs1_val_H = nan_unbox_H (F(rs1));
+  let rs1_val_H = F_or_X_H(rs1);
   match (select_instr_or_fcsr_rm (rm)) {
     None() => { handle_illegal(); RETIRE_FAIL },
     Some(rm') => {
@@ -714,7 +719,7 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_L_H)) = {
 
 function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_LU_H)) = {
   assert(sizeof(xlen) >= 64);
-  let rs1_val_H = nan_unbox_H (F(rs1));
+  let rs1_val_H = F_or_X_H(rs1);
   match (select_instr_or_fcsr_rm (rm)) {
     None() => { handle_illegal(); RETIRE_FAIL },
     Some(rm') => {
@@ -738,7 +743,7 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_L)) = {
       let (fflags, rd_val_H) = riscv_i64ToF16 (rm_3b, rs1_val_L);
 
       write_fflags(fflags);
-      F(rd) = nan_box (rd_val_H);
+      F_or_X_H(rd) = rd_val_H;
       RETIRE_SUCCESS
     }
   }
@@ -754,7 +759,7 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_LU)) = {
       let (fflags, rd_val_H) = riscv_ui64ToF16 (rm_3b, rs1_val_LU);
 
       write_fflags(fflags);
-      F(rd) = nan_box (rd_val_H);
+      F_or_X_H(rd) = rd_val_H;
       RETIRE_SUCCESS
     }
   }
@@ -782,80 +787,80 @@ mapping f_un_rm_type_mnemonic_H : f_un_rm_op_H <-> string = {
 
 mapping clause assembly = F_UN_RM_TYPE_H(rs1, rm, rd, FSQRT_H)
                       <-> f_un_rm_type_mnemonic_H(FSQRT_H)
-                          ^ spc() ^ freg_name(rd)
-                          ^ sep() ^ freg_name(rs1)
+                          ^ spc() ^ freg_or_reg_name(rd)
+                          ^ sep() ^ freg_or_reg_name(rs1)
                           ^ sep() ^ frm_mnemonic(rm)
 
 mapping clause assembly = F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_W_H)
                       <-> f_un_rm_type_mnemonic_H(FCVT_W_H)
                           ^ spc() ^ reg_name(rd)
-                          ^ sep() ^ freg_name(rs1)
+                          ^ sep() ^ freg_or_reg_name(rs1)
                           ^ sep() ^ frm_mnemonic(rm)
 
 mapping clause assembly = F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_WU_H)
                       <-> f_un_rm_type_mnemonic_H(FCVT_WU_H)
                           ^ spc() ^ reg_name(rd)
-                          ^ sep() ^ freg_name(rs1)
+                          ^ sep() ^ freg_or_reg_name(rs1)
                           ^ sep() ^ frm_mnemonic(rm)
 
 mapping clause assembly = F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_W)
                       <-> f_un_rm_type_mnemonic_H(FCVT_H_W)
-                          ^ spc() ^ freg_name(rd)
+                          ^ spc() ^ freg_or_reg_name(rd)
                           ^ sep() ^ reg_name(rs1)
                           ^ sep() ^ frm_mnemonic(rm)
 
 mapping clause assembly = F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_WU)
                       <-> f_un_rm_type_mnemonic_H(FCVT_H_WU)
-                          ^ spc() ^ freg_name(rd)
+                          ^ spc() ^ freg_or_reg_name(rd)
                           ^ sep() ^ reg_name(rs1)
                           ^ sep() ^ frm_mnemonic(rm)
 
 mapping clause assembly = F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_L_H)
                       <-> f_un_rm_type_mnemonic_H(FCVT_L_H)
                           ^ spc() ^ reg_name(rd)
-                          ^ sep() ^ freg_name(rs1)
+                          ^ sep() ^ freg_or_reg_name(rs1)
                           ^ sep() ^ frm_mnemonic(rm)
 
 mapping clause assembly = F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_LU_H)
                       <-> f_un_rm_type_mnemonic_H(FCVT_LU_H)
                           ^ spc() ^ reg_name(rd)
-                          ^ sep() ^ freg_name(rs1)
+                          ^ sep() ^ freg_or_reg_name(rs1)
                           ^ sep() ^ frm_mnemonic(rm)
 
 mapping clause assembly = F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_L)
                       <-> f_un_rm_type_mnemonic_H(FCVT_H_L)
-                          ^ spc() ^ freg_name(rd)
+                          ^ spc() ^ freg_or_reg_name(rd)
                           ^ sep() ^ reg_name(rs1)
                           ^ sep() ^ frm_mnemonic(rm)
 
 mapping clause assembly = F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_LU)
                       <-> f_un_rm_type_mnemonic_H(FCVT_H_LU)
-                          ^ spc() ^ freg_name(rd)
+                          ^ spc() ^ freg_or_reg_name(rd)
                           ^ sep() ^ reg_name(rs1)
                           ^ sep() ^ frm_mnemonic(rm)
 
 mapping clause assembly = F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_S)
                       <-> f_un_rm_type_mnemonic_H(FCVT_H_S)
-                          ^ spc() ^ freg_name(rd)
-                          ^ sep() ^ freg_name(rs1)
+                          ^ spc() ^ freg_or_reg_name(rd)
+                          ^ sep() ^ freg_or_reg_name(rs1)
                           ^ sep() ^ frm_mnemonic(rm)
 
 mapping clause assembly = F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_D)
                       <-> f_un_rm_type_mnemonic_H(FCVT_H_D)
-                          ^ spc() ^ freg_name(rd)
-                          ^ sep() ^ freg_name(rs1)
+                          ^ spc() ^ freg_or_reg_name(rd)
+                          ^ sep() ^ freg_or_reg_name(rs1)
                           ^ sep() ^ frm_mnemonic(rm)
 
 mapping clause assembly = F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_S_H)
                       <-> f_un_rm_type_mnemonic_H(FCVT_S_H)
-                          ^ spc() ^ freg_name(rd)
-                          ^ sep() ^ freg_name(rs1)
+                          ^ spc() ^ freg_or_reg_name(rd)
+                          ^ sep() ^ freg_or_reg_name(rs1)
                           ^ sep() ^ frm_mnemonic(rm)
 
 mapping clause assembly = F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_D_H)
                       <-> f_un_rm_type_mnemonic_H(FCVT_D_H)
-                          ^ spc() ^ freg_name(rd)
-                          ^ sep() ^ freg_name(rs1)
+                          ^ spc() ^ freg_or_reg_name(rd)
+                          ^ sep() ^ freg_or_reg_name(rs1)
                           ^ sep() ^ frm_mnemonic(rm)
 
 /* ****************************************************************** */
@@ -865,8 +870,8 @@ union clause ast = F_UN_TYPE_H : (regidx, regidx, f_un_op_H)
 
 /* AST <-> Binary encoding ================================ */
 
-mapping clause encdec = F_UN_TYPE_H(rs1, rd, FCLASS_H)                        if haveZfh()
-                    <-> 0b111_0010 @ 0b00000 @ rs1 @ 0b001 @ rd @ 0b101_0011  if haveZfh()
+mapping clause encdec = F_UN_TYPE_H(rs1, rd, FCLASS_H)                        if haveHalfFPU()
+                    <-> 0b111_0010 @ 0b00000 @ rs1 @ 0b001 @ rd @ 0b101_0011  if haveHalfFPU()
 
 mapping clause encdec = F_UN_TYPE_H(rs1, rd, FMV_X_H)                         if haveZfh()
                     <-> 0b111_0010 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011  if haveZfh()
@@ -877,7 +882,7 @@ mapping clause encdec = F_UN_TYPE_H(rs1, rd, FMV_H_X)                         if
 /* Execution semantics ================================ */
 
 function clause execute (F_UN_TYPE_H(rs1, rd, FCLASS_H)) = {
-  let rs1_val_H = nan_unbox_H (F(rs1));
+  let rs1_val_H = F_or_X_H(rs1);
 
   let rd_val_10b : bits (10) =
     if      f_is_neg_inf_H     (rs1_val_H) then 0b_00_0000_0001
@@ -931,4 +936,4 @@ mapping clause assembly = F_UN_TYPE_H(rs1, rd, FMV_H_X)
 mapping clause assembly = F_UN_TYPE_H(rs1, rd, FCLASS_H)
                       <-> f_un_type_mnemonic_H(FCLASS_H)
                           ^ spc() ^ reg_name(rd)
-                          ^ sep() ^ freg_name(rs1)
+                          ^ sep() ^ freg_or_reg_name(rs1)
diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
index d1f643a..9cc5034 100644
--- a/model/riscv_sys_regs.sail
+++ b/model/riscv_sys_regs.sail
@@ -351,7 +351,8 @@ function in32BitMode() -> bool = {
 function haveFExt()    -> bool = (misa.F() == 0b1) & (mstatus.FS() != 0b00)
 function haveDExt()    -> bool = (misa.D() == 0b1) & (mstatus.FS() != 0b00)
 
-/* Zfinx and Zdinx extensions (TODO: gate FCSR access on [mhs]stateen0 bit 1 when implemented) */
+/* Zhinx, Zfinx and Zdinx extensions (TODO: gate FCSR access on [mhs]stateen0 bit 1 when implemented) */
+function haveZhinx()   -> bool = sys_enable_zfinx()
 function haveZfinx()   -> bool = sys_enable_zfinx()
 function haveZdinx()   -> bool = sys_enable_zfinx() & sizeof(flen) >= 64