Revert "Initial introduction of zfinx (#75)"

This reverts commit c5e62ea4b3d481fcd491b22b317cc319b089f05d.

7 files changed, 287 insertions, 367 deletions

diff --git a/model/riscv_fdext_regs.sail b/model/riscv_fdext_regs.sail
index 4180a72..13de44d 100644
--- a/model/riscv_fdext_regs.sail
+++ b/model/riscv_fdext_regs.sail
@@ -74,41 +74,6 @@
 /* Original version written by Rishiyur S. Nikhil, Sept-Oct 2019    */
 
 /* **************************************************************** */
-/* NaN boxing/unboxing.                                             */
-/* 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_S() -> bits(32) = 0x_7fc0_0000
-function canonical_NaN_D() -> bits(64) = 0x_7ff8_0000_0000_0000
-
-val nan_unbox_do : (bool, bits(64)) -> bits(32)
-function nan_unbox_do (zfinx_en, regval) =
-  if zfinx_en
-    then regval [31..0]
-  else if regval [63..32] == 0x_FFFF_FFFF
-    then regval [31..0]
-  else canonical_NaN_S()
-
-val nan_unbox_pass : (bool, bits(32)) -> bits(32)
-function nan_unbox_pass (zfinx_en, regval) =
-  regval
-
-val nan_box_do : (bool, bits(32)) -> bits(64)
-function nan_box_do (zfinx_en, regval) =
-  0x_FFFF_FFFF @ regval
-
-
-val nan_box_pass : (bool, bits(32)) -> bits(32)
-function nan_box_pass (zfinx_en, regval) =
-  regval
-
-overload nan_unbox = { nan_unbox_do, nan_unbox_pass }
-overload nan_box = { nan_box_do, nan_box_pass }
-
-
-/* **************************************************************** */
 /* Floating point register file                                     */
 
 register f0  : fregtype
@@ -245,58 +210,6 @@ function wF_bits(i: bits(5), data: flenbits) -> unit = {
 
 overload F = {rF_bits, wF_bits, rF, wF}
 
-/* ---- Register Read/ Writes */
-
-val rX_or_F_32 : (bool, bits(5)) -> bits(32) effect {escape, rreg}
-function rX_or_F_32(zfinx_en, i) = {
-  if zfinx_en then
-    nan_unbox(zfinx_en, rX(unsigned(i)))
-  else
-    nan_unbox(zfinx_en, rF(unsigned(i)))
-}
-
-val rX_or_F_64 : (bool, bits(5)) -> bits(64) effect {escape, rreg}
-function rX_or_F_64(zfinx_en, i) = {
-  assert (zfinx_en | sizeof(flen) == 64);
-  if zfinx_en & sizeof (xlen) == 32 then {
-    assert (i[0] == bitzero);
-    if i == 0b00000 then
-      sail_zeros(64)
-    else rX(unsigned(i+1)) @ rX(unsigned(i))
-  }
-  else if zfinx_en & sizeof(xlen) == 64 then
-    rX(unsigned(i))
-  else
-    rF(unsigned(i))
-}
-
-val wX_or_F_64 : (bool, bits(5), bits(64)) -> unit effect {escape, wreg}
-function wX_or_F_64(zfinx_en: bool, i: bits(5), data: bits(64)) = {
-  assert (zfinx_en | sizeof(flen) == 64);
-  if zfinx_en & sizeof(xlen) == 32 then {
-    assert (i[0] == bitzero);
-    if i != 0b00000 then {
-      wX(unsigned(i)) = data[31..0];
-      wX(unsigned(i+1)) = data[63..32];
-    }
-  }
-  else if zfinx_en & sizeof (xlen) == 64 then
-    wX(unsigned(i)) = data
-  else if ~ (zfinx_en) & sizeof (flen) == 64 then
-    wF(unsigned(i)) = data
-}
-
-val wX_or_F_32 : (bool, bits(5), bits(32)) -> unit effect {escape, wreg}
-function wX_or_F_32(zfinx_en: bool, i: bits(5), data : bits(32)) = {
-  if zfinx_en then
-    wX(unsigned(i)) = nan_box(zfinx_en, data)
-  else
-    wF(unsigned(i)) = nan_box(zfinx_en, data)
-}
-
-overload X_or_F_S = { rX_or_F_32, wX_or_F_32 }
-overload X_or_F_D = { rX_or_F_64, wX_or_F_64 }
-
 /* register names */
 
 val freg_name_abi : regidx <-> string
@@ -376,12 +289,6 @@ mapping freg_name = {
     0b11111 <-> "ft11"
 }
 
-val reg_or_freg_name : bits(5) <-> string
-mapping reg_or_freg_name = {
-  reg if sys_enable_zfinx()     <-> reg_name(reg)  if sys_enable_zfinx(),
-  reg if ~ (sys_enable_zfinx()) <-> freg_name(reg) if ~ (sys_enable_zfinx())
-}
-
 val init_fdext_regs : unit -> unit effect {wreg}
 function init_fdext_regs () = {
   f0  = zero_freg;
@@ -437,13 +344,13 @@ function ext_write_fcsr (frm, fflags) = {
   fcsr->FRM()    = frm;      /* Note: frm can be an illegal value, 101, 110, 111 */
   fcsr->FFLAGS() = fflags;
   update_softfloat_fflags(fflags);
-  if ~ (sys_enable_zfinx()) then dirty_fd_context();
+  dirty_fd_context();
 }
 
 /* called for softfloat paths (softfloat flags are consistent) */
 val write_fflags : (bits(5)) -> unit effect {rreg, wreg}
 function write_fflags(fflags) = {
-  if   fcsr.FFLAGS() != fflags & ~ (sys_enable_zfinx())
+  if   fcsr.FFLAGS() != fflags
   then dirty_fd_context();
   fcsr->FFLAGS() = fflags;
 }
@@ -456,6 +363,6 @@ function accrue_fflags(flags) = {
   then {
     fcsr->FFLAGS() = f;
     update_softfloat_fflags(f);
-    if ~ (sys_enable_zfinx()) then dirty_fd_context();
+    dirty_fd_context();
   }
 }
diff --git a/model/riscv_insts_cdext.sail b/model/riscv_insts_cdext.sail
index 0c6bbd1..77a6302 100644
--- a/model/riscv_insts_cdext.sail
+++ b/model/riscv_insts_cdext.sail
@@ -77,9 +77,9 @@
 union clause ast = C_FLDSP : (bits(6), regidx)
 
 mapping clause encdec_compressed = C_FLDSP(ui86 @ ui5 @ ui43, rd)
-      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() & ~ (sys_enable_zfinx())
+      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt()
   <-> 0b001 @ ui5 : bits(1) @ rd : regidx @ ui43 : bits(2) @ ui86 : bits(3) @ 0b10
-      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() & ~ (sys_enable_zfinx())
+      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt()
 
 function clause execute (C_FLDSP(uimm, rd)) = {
   let imm : bits(12) = EXTZ(uimm @ 0b000);
@@ -95,9 +95,9 @@ mapping clause assembly = C_FLDSP(uimm, rd)
 union clause ast = C_FSDSP : (bits(6), regidx)
 
 mapping clause encdec_compressed = C_FSDSP(ui86 @ ui53, rs2)
-      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() & ~ (sys_enable_zfinx())
+      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt()
   <-> 0b101 @ ui53 : bits(3) @ ui86 : bits(3) @ rs2 : regidx @ 0b10
-      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() & ~ (sys_enable_zfinx())
+      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt()
 
 function clause execute (C_FSDSP(uimm, rs2)) = {
   let imm : bits(12) = EXTZ(uimm @ 0b000);
@@ -113,9 +113,9 @@ mapping clause assembly = C_FSDSP(uimm, rs2)
 union clause ast = C_FLD : (bits(5), cregidx, cregidx)
 
 mapping clause encdec_compressed = C_FLD(ui76 @ ui53, rs1, rd)
-      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() & ~ (sys_enable_zfinx())
+      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt()
   <-> 0b001 @ ui53 : bits(3) @ rs1 : cregidx @ ui76 : bits(2) @ rd : cregidx @ 0b00
-      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() & ~ (sys_enable_zfinx())
+      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt()
 
 function clause execute (C_FLD(uimm, rsc, rdc)) = {
   let imm : bits(12) = EXTZ(uimm @ 0b000);
@@ -133,9 +133,9 @@ mapping clause assembly = C_FLD(uimm, rsc, rdc)
 union clause ast = C_FSD : (bits(5), cregidx, cregidx)
 
 mapping clause encdec_compressed = C_FSD(ui76 @ ui53, rs1, rs2)
-      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() & ~ (sys_enable_zfinx())
+      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt()
   <-> 0b101 @ ui53 : bits(3) @ rs1 : bits(3) @ ui76 : bits(2) @ rs2 : bits(3) @ 0b00
-      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() & ~ (sys_enable_zfinx())
+      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt()
 
 function clause execute (C_FSD(uimm, rsc1, rsc2)) = {
   let imm : bits(12) = EXTZ(uimm @ 0b000);
diff --git a/model/riscv_insts_cfext.sail b/model/riscv_insts_cfext.sail
index 98eea24..9aa94ef 100644
--- a/model/riscv_insts_cfext.sail
+++ b/model/riscv_insts_cfext.sail
@@ -77,9 +77,9 @@
 union clause ast = C_FLWSP : (bits(6), regidx)
 
 mapping clause encdec_compressed = C_FLWSP(ui76 @ ui5 @ ui42, rd)
-      if sizeof(xlen) == 32 & haveRVC() & haveFExt() & ~ (sys_enable_zfinx())
+      if sizeof(xlen) == 32 & haveRVC() & haveFExt()
   <-> 0b011 @ ui5 : bits(1) @ rd : regidx @ ui42 : bits(3) @ ui76 : bits(2) @ 0b10
-      if sizeof(xlen) == 32 & haveRVC() & haveFExt() & ~ (sys_enable_zfinx())
+      if sizeof(xlen) == 32 & haveRVC() & haveFExt()
 
 function clause execute (C_FLWSP(imm, rd)) = {
   let imm : bits(12) = EXTZ(imm @ 0b00);
@@ -95,9 +95,9 @@ mapping clause assembly = C_FLWSP(imm, rd)
 union clause ast = C_FSWSP : (bits(6), regidx)
 
 mapping clause encdec_compressed = C_FSWSP(ui76 @ ui52, rs2)
-      if sizeof(xlen) == 32 & haveRVC() & haveFExt() & ~ (sys_enable_zfinx())
+      if sizeof(xlen) == 32 & haveRVC() & haveFExt()
   <-> 0b111 @ ui52 : bits(4) @ ui76 : bits(2) @ rs2 : regidx @ 0b10
-      if sizeof(xlen) == 32 & haveRVC() & haveFExt() & ~ (sys_enable_zfinx())
+      if sizeof(xlen) == 32 & haveRVC() & haveFExt()
 
 function clause execute (C_FSWSP(uimm, rs2)) = {
   let imm : bits(12) = EXTZ(uimm @ 0b00);
@@ -113,9 +113,9 @@ mapping clause assembly = C_FSWSP(uimm, rd)
 union clause ast = C_FLW : (bits(5), cregidx, cregidx)
 
 mapping clause encdec_compressed = C_FLW(ui6 @ ui53 @ ui2, rs1, rd)
-      if sizeof(xlen) == 32 & haveRVC() & haveFExt() & ~ (sys_enable_zfinx())
+      if sizeof(xlen) == 32 & haveRVC() & haveFExt()
   <-> 0b011 @ ui53 : bits(3) @ rs1 : cregidx @ ui2 : bits(1) @ ui6 : bits(1) @ rd : cregidx @ 0b00
-      if sizeof(xlen) == 32 & haveRVC() & haveFExt() & ~ (sys_enable_zfinx())
+      if sizeof(xlen) == 32 & haveRVC() & haveFExt()
 
 function clause execute (C_FLW(uimm, rsc, rdc)) = {
   let imm : bits(12) = EXTZ(uimm @ 0b00);
@@ -133,9 +133,9 @@ mapping clause assembly = C_FLW(uimm, rsc, rdc)
 union clause ast = C_FSW : (bits(5), cregidx, cregidx)
 
 mapping clause encdec_compressed = C_FSW(ui6 @ ui53 @ ui2, rs1, rs2)
-      if sizeof(xlen) == 32 & haveRVC() & haveFExt() & ~ (sys_enable_zfinx())
+      if sizeof(xlen) == 32 & haveRVC() & haveFExt()
   <-> 0b111 @ ui53 : bits(3) @ rs1 : cregidx @ ui2 : bits(1) @ ui6 : bits(1) @ rs2 : cregidx @ 0b00
-      if sizeof(xlen) == 32 & haveRVC() & haveFExt() & ~ (sys_enable_zfinx())
+      if sizeof(xlen) == 32 & haveRVC() & haveFExt()
 
 function clause execute (C_FSW(uimm, rsc1, rsc2)) = {
   let imm : bits(12) = EXTZ(uimm @ 0b00);
diff --git a/model/riscv_insts_dext.sail b/model/riscv_insts_dext.sail
index 068bba6..ea6f280 100644
--- a/model/riscv_insts_dext.sail
+++ b/model/riscv_insts_dext.sail
@@ -98,6 +98,10 @@ function fsplit_D   x64 = (x64[63..63], x64[62..52], x64[51..0])
 val      fmake_D  : (bits(1), bits(11), bits(52)) -> bits(64)
 function fmake_D (sign, exp, mant) = sign @ exp @ mant
 
+/* ---- Canonical NaNs */
+
+function canonical_NaN_D() -> bits(64) = 0x_7ff8_0000_0000_0000
+
 /* ---- Structure tests */
 
 val      f_is_neg_inf_D : bits(64) -> bool
@@ -298,28 +302,27 @@ union clause ast = F_MADD_TYPE_D : (regidx, regidx, regidx, rounding_mode, regid
 /* AST <-> Binary encoding ================================ */
 
 mapping clause encdec =
-    F_MADD_TYPE_D(rs3, rs2, rs1, rm, rd, FMADD_D)                         if supports_RV32D_or_RV64D([rs3, rs2, rs1, rd])
-<-> rs3 @ 0b01 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_0011  if supports_RV32D_or_RV64D([rs3, rs2, rs1, rd])
+    F_MADD_TYPE_D(rs3, rs2, rs1, rm, rd, FMADD_D)                         if is_RV32D_or_RV64D()
+<-> rs3 @ 0b01 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_0011  if is_RV32D_or_RV64D()
 
 mapping clause encdec =
-    F_MADD_TYPE_D(rs3, rs2, rs1, rm, rd, FMSUB_D)                         if supports_RV32D_or_RV64D([rs3, rs2, rs1, rd])
-<-> rs3 @ 0b01 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_0111  if supports_RV32D_or_RV64D([rs3, rs2, rs1, rd])
+    F_MADD_TYPE_D(rs3, rs2, rs1, rm, rd, FMSUB_D)                         if is_RV32D_or_RV64D()
+<-> rs3 @ 0b01 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_0111  if is_RV32D_or_RV64D()
 
 mapping clause encdec =
-    F_MADD_TYPE_D(rs3, rs2, rs1, rm, rd, FNMSUB_D)                        if supports_RV32D_or_RV64D([rs3, rs2, rs1, rd])
-<-> rs3 @ 0b01 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_1011  if supports_RV32D_or_RV64D([rs3, rs2, rs1, rd])
+    F_MADD_TYPE_D(rs3, rs2, rs1, rm, rd, FNMSUB_D)                        if is_RV32D_or_RV64D()
+<-> rs3 @ 0b01 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_1011  if is_RV32D_or_RV64D()
 
 mapping clause encdec =
-    F_MADD_TYPE_D(rs3, rs2, rs1, rm, rd, FNMADD_D)                        if supports_RV32D_or_RV64D([rs3, rs2, rs1, rd])
-<-> rs3 @ 0b01 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_1111  if supports_RV32D_or_RV64D([rs3, rs2, rs1, rd])
+    F_MADD_TYPE_D(rs3, rs2, rs1, rm, rd, FNMADD_D)                        if is_RV32D_or_RV64D()
+<-> rs3 @ 0b01 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_1111  if is_RV32D_or_RV64D()
 
 /* Execution semantics ================================ */
 
 function clause execute (F_MADD_TYPE_D(rs3, rs2, rs1, rm, rd, op)) = {
-  let rs1_val_64b = X_or_F_D(sys_enable_zfinx(), rs1);
-  let rs2_val_64b = X_or_F_D(sys_enable_zfinx(), rs2);
-  let rs3_val_64b = X_or_F_D(sys_enable_zfinx(), rs3);
-
+  let rs1_val_64b = F(rs1);
+  let rs2_val_64b = F(rs2);
+  let rs3_val_64b = F(rs3);
   match (select_instr_or_fcsr_rm (rm)) {
     None() => { handle_illegal(); RETIRE_FAIL },
     Some(rm') => {
@@ -332,7 +335,7 @@ function clause execute (F_MADD_TYPE_D(rs3, rs2, rs1, rm, rd, op)) = {
           FNMADD_D => riscv_f64MulAdd (rm_3b, negate_D (rs1_val_64b), rs2_val_64b, negate_D (rs3_val_64b))
         };
       write_fflags(fflags);
-      X_or_F_D(sys_enable_zfinx(), rd, rd_val_64b);
+      F(rd) = rd_val_64b;
       RETIRE_SUCCESS
     }
   }
@@ -349,10 +352,10 @@ mapping f_madd_type_mnemonic_D : f_madd_op_D <-> string = {
 
 mapping clause assembly = F_MADD_TYPE_D(rs3, rs2, rs1, rm, rd, op)
                       <-> f_madd_type_mnemonic_D(op)
-                          ^ spc() ^ reg_or_freg_name(rd)
-                          ^ sep() ^ reg_or_freg_name(rs1)
-                          ^ sep() ^ reg_or_freg_name(rs2)
-                          ^ sep() ^ reg_or_freg_name(rs3)
+                          ^ spc() ^ freg_name(rd)
+                          ^ sep() ^ freg_name(rs1)
+                          ^ sep() ^ freg_name(rs2)
+                          ^ sep() ^ freg_name(rs3)
                           ^ sep() ^ frm_mnemonic(rm)
 
 /* ****************************************************************** */
@@ -365,26 +368,26 @@ union clause ast = F_BIN_RM_TYPE_D : (regidx, regidx, rounding_mode, regidx, f_b
 /* AST <-> Binary encoding ================================ */
 
 mapping clause encdec =
-    F_BIN_RM_TYPE_D(rs2, rs1, rm, rd, FADD_D)                             if supports_RV32D_or_RV64D([rs2, rs1, rd])
-<-> 0b000_0001 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if supports_RV32D_or_RV64D([rs2, rs1, rd])
+    F_BIN_RM_TYPE_D(rs2, rs1, rm, rd, FADD_D)                             if is_RV32D_or_RV64D()
+<-> 0b000_0001 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if is_RV32D_or_RV64D()
 
 mapping clause encdec =
-    F_BIN_RM_TYPE_D(rs2, rs1, rm, rd, FSUB_D)                             if supports_RV32D_or_RV64D([rs2, rs1, rd])
-<-> 0b000_0101 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if supports_RV32D_or_RV64D([rs2, rs1, rd])
+    F_BIN_RM_TYPE_D(rs2, rs1, rm, rd, FSUB_D)                             if is_RV32D_or_RV64D()
+<-> 0b000_0101 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if is_RV32D_or_RV64D()
 
 mapping clause encdec =
-    F_BIN_RM_TYPE_D(rs2, rs1, rm, rd, FMUL_D)                             if supports_RV32D_or_RV64D([rs2, rs1, rd])
-<-> 0b000_1001 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if supports_RV32D_or_RV64D([rs2, rs1, rd])
+    F_BIN_RM_TYPE_D(rs2, rs1, rm, rd, FMUL_D)                             if is_RV32D_or_RV64D()
+<-> 0b000_1001 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if is_RV32D_or_RV64D()
 
 mapping clause encdec =
-    F_BIN_RM_TYPE_D(rs2, rs1, rm, rd, FDIV_D)                             if supports_RV32D_or_RV64D([rs2, rs1, rd])
-<-> 0b000_1101 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if supports_RV32D_or_RV64D([rs2, rs1, rd])
+    F_BIN_RM_TYPE_D(rs2, rs1, rm, rd, FDIV_D)                             if is_RV32D_or_RV64D()
+<-> 0b000_1101 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if is_RV32D_or_RV64D()
 
 /* Execution semantics ================================ */
 
 function clause execute (F_BIN_RM_TYPE_D(rs2, rs1, rm, rd, op)) = {
-  rs1_val_64b = X_or_F_D(sys_enable_zfinx(), rs1);
-  rs2_val_64b = X_or_F_D(sys_enable_zfinx(), rs2);
+  let rs1_val_64b = F(rs1);
+  let rs2_val_64b = F(rs2);
   match (select_instr_or_fcsr_rm (rm)) {
     None() => { handle_illegal(); RETIRE_FAIL },
     Some(rm') => {
@@ -396,7 +399,7 @@ function clause execute (F_BIN_RM_TYPE_D(rs2, rs1, rm, rd, op)) = {
         FDIV_D  => riscv_f64Div (rm_3b, rs1_val_64b, rs2_val_64b)
       };
       write_fflags(fflags);
-      X_or_F_D(sys_enable_zfinx(), rd, rd_val_64b);
+      F(rd) = rd_val_64b;
       RETIRE_SUCCESS
     }
   }
@@ -413,9 +416,9 @@ mapping f_bin_rm_type_mnemonic_D : f_bin_rm_op_D <-> string = {
 
 mapping clause assembly = F_BIN_RM_TYPE_D(rs2, rs1, rm, rd, op)
                       <-> f_bin_rm_type_mnemonic_D(op)
-                          ^ spc() ^ reg_or_freg_name(rd)
-                          ^ sep() ^ reg_or_freg_name(rs1)
-                          ^ sep() ^ reg_or_freg_name(rs2)
+                          ^ spc() ^ freg_name(rd)
+                          ^ sep() ^ freg_name(rs1)
+                          ^ sep() ^ freg_name(rs2)
                           ^ sep() ^ frm_mnemonic(rm)
 
 /* ****************************************************************** */
@@ -428,32 +431,32 @@ union clause ast = F_UN_RM_TYPE_D : (regidx, rounding_mode, regidx, f_un_rm_op_D
 /* AST <-> Binary encoding ================================ */
 
 mapping clause encdec =
-    F_UN_RM_TYPE_D(rs1, rm, rd, FSQRT_D)                                      if supports_RV32D_or_RV64D([rs1, rd])
-<-> 0b010_1101 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if supports_RV32D_or_RV64D([rs1, rd])
+    F_UN_RM_TYPE_D(rs1, rm, rd, FSQRT_D)                                      if is_RV32D_or_RV64D()
+<-> 0b010_1101 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if is_RV32D_or_RV64D()
 
 mapping clause encdec =
-    F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_W_D)                                     if supports_RV32D_or_RV64D([rs1])
-<-> 0b110_0001 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if supports_RV32D_or_RV64D([rs1])
+    F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_W_D)                                     if is_RV32D_or_RV64D()
+<-> 0b110_0001 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if is_RV32D_or_RV64D()
 
 mapping clause encdec =
-    F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_WU_D)                                    if supports_RV32D_or_RV64D([rs1])
-<-> 0b110_0001 @ 0b00001 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if supports_RV32D_or_RV64D([rs1])
+    F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_WU_D)                                    if is_RV32D_or_RV64D()
+<-> 0b110_0001 @ 0b00001 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if is_RV32D_or_RV64D()
 
 mapping clause encdec =
-    F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_W)                                     if supports_RV32D_or_RV64D([rd])
-<-> 0b110_1001 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if supports_RV32D_or_RV64D([rd])
+    F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_W)                                     if is_RV32D_or_RV64D()
+<-> 0b110_1001 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if is_RV32D_or_RV64D()
 
 mapping clause encdec =
-    F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_WU)                                    if supports_RV32D_or_RV64D([rd])
-<-> 0b110_1001 @ 0b00001 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if supports_RV32D_or_RV64D([rd])
+    F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_WU)                                    if is_RV32D_or_RV64D()
+<-> 0b110_1001 @ 0b00001 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if is_RV32D_or_RV64D()
 
 mapping clause encdec =
-    F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_S_D)                                     if supports_RV32D_or_RV64D([rs1])
-<-> 0b010_0000 @ 0b00001 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if supports_RV32D_or_RV64D([rs1])
+    F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_S_D)                                     if is_RV32D_or_RV64D()
+<-> 0b010_0000 @ 0b00001 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if is_RV32D_or_RV64D()
 
 mapping clause encdec =
-    F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_S)                                     if supports_RV32D_or_RV64D([rd])
-<-> 0b010_0001 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if supports_RV32D_or_RV64D([rd])
+    F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_S)                                     if is_RV32D_or_RV64D()
+<-> 0b010_0001 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if is_RV32D_or_RV64D()
 
 /* D instructions, RV64 only */
 
@@ -476,7 +479,7 @@ mapping clause encdec =
 /* Execution semantics ================================ */
 
 function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FSQRT_D)) = {
-  let rs1_val_D = X_or_F_D(sys_enable_zfinx(), rs1);
+  let rs1_val_D = F(rs1);
   match (select_instr_or_fcsr_rm (rm)) {
     None() => { handle_illegal(); RETIRE_FAIL },
     Some(rm') => {
@@ -484,14 +487,14 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FSQRT_D)) = {
       let (fflags, rd_val_D) = riscv_f64Sqrt   (rm_3b, rs1_val_D);
 
       write_fflags(fflags);
-      X_or_F_D(sys_enable_zfinx(), rd, rd_val_D);
+      F(rd) = rd_val_D;
       RETIRE_SUCCESS
     }
   }
 }
 
 function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_W_D)) = {
-  let rs1_val_D = X_or_F_D(sys_enable_zfinx(), rs1);
+  let rs1_val_D = F(rs1);
   match (select_instr_or_fcsr_rm (rm)) {
     None() => { handle_illegal(); RETIRE_FAIL },
     Some(rm') => {
@@ -506,7 +509,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_W_D)) = {
 }
 
 function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_WU_D)) = {
-  let rs1_val_D = X_or_F_D(sys_enable_zfinx(), rs1);
+  let rs1_val_D = F(rs1);
   match (select_instr_or_fcsr_rm (rm)) {
     None() => { handle_illegal(); RETIRE_FAIL },
     Some(rm') => {
@@ -529,7 +532,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_W)) = {
       let (fflags, rd_val_D) = riscv_i32ToF64 (rm_3b, rs1_val_W);
 
       write_fflags(fflags);
-      X_or_F_D(sys_enable_zfinx(), rd, rd_val_D);
+      F(rd) = rd_val_D;
       RETIRE_SUCCESS
     }
   }
@@ -544,14 +547,14 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_WU)) = {
       let (fflags, rd_val_D) = riscv_ui32ToF64 (rm_3b, rs1_val_WU);
 
       write_fflags(fflags);
-      X_or_F_D(sys_enable_zfinx(), rd, rd_val_D);
+      F(rd) = rd_val_D;
       RETIRE_SUCCESS
     }
   }
 }
 
 function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_S_D)) = {
-  let rs1_val_D = X_or_F_D(sys_enable_zfinx(), rs1);
+  let rs1_val_D = F(rs1);
   match (select_instr_or_fcsr_rm (rm)) {
     None() => { handle_illegal(); RETIRE_FAIL },
     Some(rm') => {
@@ -559,14 +562,14 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_S_D)) = {
       let (fflags, rd_val_S) = riscv_f64ToF32 (rm_3b, rs1_val_D);
 
       write_fflags(fflags);
-      X_or_F_S(sys_enable_zfinx(), rd, rd_val_S);
+      F(rd) = nan_box (rd_val_S);
       RETIRE_SUCCESS
     }
   }
 }
 
 function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_S)) = {
-  rs1_val_S = X_or_F_S(sys_enable_zfinx(), rs1);
+  let rs1_val_S = nan_unbox (F(rs1));
   match (select_instr_or_fcsr_rm (rm)) {
     None() => { handle_illegal(); RETIRE_FAIL },
     Some(rm') => {
@@ -574,7 +577,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_S)) = {
       let (fflags, rd_val_D) = riscv_f32ToF64 (rm_3b, rs1_val_S);
 
       write_fflags(fflags);
-      X_or_F_D(sys_enable_zfinx(), rd, rd_val_D);
+      F(rd) = rd_val_D;
       RETIRE_SUCCESS
     }
   }
@@ -582,7 +585,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_S)) = {
 
 function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_L_D)) = {
   assert(sizeof(xlen) >= 64);
-  rs1_val_D = X_or_F_D(sys_enable_zfinx(), rs1);
+  let rs1_val_D = F(rs1);
   match (select_instr_or_fcsr_rm (rm)) {
     None() => { handle_illegal(); RETIRE_FAIL },
     Some(rm') => {
@@ -598,7 +601,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_L_D)) = {
 
 function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_LU_D)) = {
   assert(sizeof(xlen) >= 64);
-  let rs1_val_D = X_or_F_D(sys_enable_zfinx(), rs1);
+  let rs1_val_D = F(rs1);
   match (select_instr_or_fcsr_rm (rm)) {
     None() => { handle_illegal(); RETIRE_FAIL },
     Some(rm') => {
@@ -606,7 +609,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_LU_D)) = {
       let (fflags, rd_val_LU) = riscv_f64ToUi64 (rm_3b, rs1_val_D);
 
       write_fflags(fflags);
-      X(rd) = rd_val_LU;
+      X(rd) = EXTS(rd_val_LU);
       RETIRE_SUCCESS
     }
   }
@@ -622,7 +625,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_L)) = {
       let (fflags, rd_val_D) = riscv_i64ToF64 (rm_3b, rs1_val_L);
 
       write_fflags(fflags);
-      X_or_F_D(sys_enable_zfinx(), rd, rd_val_D);
+      F(rd) = rd_val_D;
       RETIRE_SUCCESS
     }
   }
@@ -638,7 +641,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_LU)) = {
       let (fflags, rd_val_D) = riscv_ui64ToF64 (rm_3b, rs1_val_LU);
 
       write_fflags(fflags);
-      X_or_F_D(sys_enable_zfinx(), rd, rd_val_D);
+      F(rd) = rd_val_D;
       RETIRE_SUCCESS
     }
   }
@@ -664,68 +667,68 @@ mapping f_un_rm_type_mnemonic_D : f_un_rm_op_D <-> string = {
 
 mapping clause assembly = F_UN_RM_TYPE_D(rs1, rm, rd, FSQRT_D)
                       <-> f_un_rm_type_mnemonic_D(FSQRT_D)
-                          ^ spc() ^ reg_or_freg_name(rd)
-                          ^ sep() ^ reg_or_freg_name(rs1)
+                          ^ spc() ^ freg_name(rd)
+                          ^ sep() ^ freg_name(rs1)
                           ^ sep() ^ frm_mnemonic(rm)
 
 mapping clause assembly = F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_W_D)
                       <-> f_un_rm_type_mnemonic_D(FCVT_W_D)
                           ^ spc() ^ reg_name(rd)
-                          ^ sep() ^ reg_or_freg_name(rs1)
+                          ^ sep() ^ freg_name(rs1)
                           ^ sep() ^ frm_mnemonic(rm)
 
 mapping clause assembly = F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_WU_D)
                       <-> f_un_rm_type_mnemonic_D(FCVT_WU_D)
                           ^ spc() ^ reg_name(rd)
-                          ^ sep() ^ reg_or_freg_name(rs1)
+                          ^ sep() ^ freg_name(rs1)
                           ^ sep() ^ frm_mnemonic(rm)
 
 mapping clause assembly = F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_W)
                       <-> f_un_rm_type_mnemonic_D(FCVT_D_W)
-                          ^ spc() ^ reg_or_freg_name(rd)
+                          ^ spc() ^ freg_name(rd)
                           ^ sep() ^ reg_name(rs1)
                           ^ sep() ^ frm_mnemonic(rm)
 
 mapping clause assembly = F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_WU)
                       <-> f_un_rm_type_mnemonic_D(FCVT_D_WU)
-                          ^ spc() ^ reg_or_freg_name(rd)
+                          ^ spc() ^ freg_name(rd)
                           ^ sep() ^ reg_name(rs1)
                           ^ sep() ^ frm_mnemonic(rm)
 
 mapping clause assembly = F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_L_D)
                       <-> f_un_rm_type_mnemonic_D(FCVT_L_D)
                           ^ spc() ^ reg_name(rd)
-                          ^ sep() ^ reg_or_freg_name(rs1)
+                          ^ sep() ^ freg_name(rs1)
                           ^ sep() ^ frm_mnemonic(rm)
 
 mapping clause assembly = F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_LU_D)
                       <-> f_un_rm_type_mnemonic_D(FCVT_LU_D)
                           ^ spc() ^ reg_name(rd)
-                          ^ sep() ^ reg_or_freg_name(rs1)
+                          ^ sep() ^ freg_name(rs1)
                           ^ sep() ^ frm_mnemonic(rm)
 
 mapping clause assembly = F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_L)
                       <-> f_un_rm_type_mnemonic_D(FCVT_D_L)
-                          ^ spc() ^ reg_or_freg_name(rd)
+                          ^ spc() ^ freg_name(rd)
                           ^ sep() ^ reg_name(rs1)
                           ^ sep() ^ frm_mnemonic(rm)
 
 mapping clause assembly = F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_LU)
                       <-> f_un_rm_type_mnemonic_D(FCVT_D_LU)
-                          ^ spc() ^ reg_or_freg_name(rd)
+                          ^ spc() ^ freg_name(rd)
                           ^ sep() ^ reg_name(rs1)
                           ^ sep() ^ frm_mnemonic(rm)
 
 mapping clause assembly = F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_S_D)
                       <-> f_un_rm_type_mnemonic_D(FCVT_S_D)
-                          ^ spc() ^ reg_or_freg_name(rd)
-                          ^ sep() ^ reg_or_freg_name(rs1)
+                          ^ spc() ^ freg_name(rd)
+                          ^ sep() ^ freg_name(rs1)
                           ^ sep() ^ frm_mnemonic(rm)
 
 mapping clause assembly = F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_S)
                       <-> f_un_rm_type_mnemonic_D(FCVT_D_S)
-                          ^ spc() ^ reg_or_freg_name(rd)
-                          ^ sep() ^ reg_or_freg_name(rs1)
+                          ^ spc() ^ freg_name(rd)
+                          ^ sep() ^ freg_name(rs1)
                           ^ sep() ^ frm_mnemonic(rm)
 
 /* ****************************************************************** */
@@ -737,69 +740,68 @@ union clause ast = F_BIN_TYPE_D : (regidx, regidx, regidx, f_bin_op_D)
 
 /* AST <-> Binary encoding ================================ */
 
-mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FSGNJ_D)               if supports_RV32D_or_RV64D([rs2, rs1, rd])
-                    <-> 0b001_0001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011  if supports_RV32D_or_RV64D([rs2, rs1, rd])
+mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FSGNJ_D)               if is_RV32D_or_RV64D()
+                    <-> 0b001_0001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011  if is_RV32D_or_RV64D()
 
-mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FSGNJN_D)              if supports_RV32D_or_RV64D([rs2, rs1, rd])
-                    <-> 0b001_0001 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011  if supports_RV32D_or_RV64D([rs2, rs1, rd])
+mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FSGNJN_D)              if is_RV32D_or_RV64D()
+                    <-> 0b001_0001 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011  if is_RV32D_or_RV64D()
 
-mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FSGNJX_D)              if supports_RV32D_or_RV64D([rs2, rs1, rd])
-                    <-> 0b001_0001 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011  if supports_RV32D_or_RV64D([rs2, rs1, rd])
+mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FSGNJX_D)              if is_RV32D_or_RV64D()
+                    <-> 0b001_0001 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011  if is_RV32D_or_RV64D()
 
-mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FMIN_D)                if supports_RV32D_or_RV64D([rs2, rs1, rd])
-                    <-> 0b001_0101 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011  if supports_RV32D_or_RV64D([rs2, rs1, rd])
+mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FMIN_D)                if is_RV32D_or_RV64D()
+                    <-> 0b001_0101 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011  if is_RV32D_or_RV64D()
 
-mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FMAX_D)                if supports_RV32D_or_RV64D([rs2, rs1, rd])
-                    <-> 0b001_0101 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011  if supports_RV32D_or_RV64D([rs2, rs1, rd])
+mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FMAX_D)                if is_RV32D_or_RV64D()
+                    <-> 0b001_0101 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011  if is_RV32D_or_RV64D()
 
-mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FEQ_D)                 if supports_RV32D_or_RV64D([rs2, rs1])
-                    <-> 0b101_0001 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011  if supports_RV32D_or_RV64D([rs2, rs1])
+mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FEQ_D)                 if is_RV32D_or_RV64D()
+                    <-> 0b101_0001 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011  if is_RV32D_or_RV64D()
 
-mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FLT_D)                 if supports_RV32D_or_RV64D([rs2, rs1])
-                    <-> 0b101_0001 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011  if supports_RV32D_or_RV64D([rs2, rs1])
+mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FLT_D)                 if is_RV32D_or_RV64D()
+                    <-> 0b101_0001 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011  if is_RV32D_or_RV64D()
 
-mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FLE_D)                 if supports_RV32D_or_RV64D([rs2, rs1])
-                    <-> 0b101_0001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011  if supports_RV32D_or_RV64D([rs2, rs1])
+mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FLE_D)                 if is_RV32D_or_RV64D()
+                    <-> 0b101_0001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011  if is_RV32D_or_RV64D()
 
 /* Execution semantics ================================ */
 
 function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FSGNJ_D)) = {
-  let rs1_val_D    = X_or_F_D(sys_enable_zfinx(), rs1);
-  let rs2_val_D    = X_or_F_D(sys_enable_zfinx(), rs2);
-
+  let rs1_val_D    = F(rs1);
+  let rs2_val_D    = F(rs2);
   let (s1, e1, m1) = fsplit_D (rs1_val_D);
   let (s2, e2, m2) = fsplit_D (rs2_val_D);
   let rd_val_D     = fmake_D (s2, e1, m1);
 
-  X_or_F_D(sys_enable_zfinx(), rd, rd_val_D);
+  F(rd) = rd_val_D;
   RETIRE_SUCCESS
 }
 
 function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FSGNJN_D)) = {
-  let rs1_val_D    = X_or_F_D(sys_enable_zfinx(), rs1);
-  let rs2_val_D    = X_or_F_D(sys_enable_zfinx(), rs2);
+  let rs1_val_D    = F(rs1);
+  let rs2_val_D    = F(rs2);
   let (s1, e1, m1) = fsplit_D (rs1_val_D);
   let (s2, e2, m2) = fsplit_D (rs2_val_D);
   let rd_val_D     = fmake_D (0b1 ^ s2, e1, m1);
 
-  X_or_F_D(sys_enable_zfinx(), rd, rd_val_D);
+  F(rd) = rd_val_D;
   RETIRE_SUCCESS
 }
 
 function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FSGNJX_D)) = {
-  let rs1_val_D    = X_or_F_D(sys_enable_zfinx(), rs1);
-  let rs2_val_D    = X_or_F_D(sys_enable_zfinx(), rs2);
+  let rs1_val_D    = F(rs1);
+  let rs2_val_D    = F(rs2);
   let (s1, e1, m1) = fsplit_D (rs1_val_D);
   let (s2, e2, m2) = fsplit_D (rs2_val_D);
   let rd_val_D     = fmake_D (s1 ^ s2, e1, m1);
 
-  X_or_F_D(sys_enable_zfinx(), rd, rd_val_D);
+  F(rd) = rd_val_D;
   RETIRE_SUCCESS
 }
 
 function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FMIN_D)) = {
-  let rs1_val_D = X_or_F_D(sys_enable_zfinx(), rs1);
-  let rs2_val_D = X_or_F_D(sys_enable_zfinx(), rs2);
+  let rs1_val_D = F(rs1);
+  let rs2_val_D = F(rs2);
 
   let is_quiet  = true;
   let (rs1_lt_rs2, fflags) = fle_D (rs1_val_D, rs2_val_D, is_quiet);
@@ -813,13 +815,13 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FMIN_D)) = {
                   else /* (not rs1_lt_rs2) */                                            rs2_val_D;
 
   accrue_fflags(fflags);
-  X_or_F_D(sys_enable_zfinx(), rd, rd_val_D);
+  F(rd) = rd_val_D;
   RETIRE_SUCCESS
 }
 
 function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FMAX_D)) = {
-  let rs1_val_D = X_or_F_D(sys_enable_zfinx(), rs1);
-  let rs2_val_D = X_or_F_D(sys_enable_zfinx(), rs2);
+  let rs1_val_D = F(rs1);
+  let rs2_val_D = F(rs2);
 
   let is_quiet  = true;
   let (rs2_lt_rs1, fflags) = fle_D (rs2_val_D, rs1_val_D, is_quiet);
@@ -833,13 +835,13 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FMAX_D)) = {
                   else /* (not rs2_lt_rs1) */                                            rs2_val_D;
 
   accrue_fflags(fflags);
-  X_or_F_D(sys_enable_zfinx(), rd, rd_val_D);
+  F(rd) = rd_val_D;
   RETIRE_SUCCESS
 }
 
 function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FEQ_D)) = {
-  let rs1_val_D = X_or_F_D(sys_enable_zfinx(), rs1);
-  let rs2_val_D = X_or_F_D(sys_enable_zfinx(), rs2);
+  let rs1_val_D = F(rs1);
+  let rs2_val_D = F(rs2);
 
   let (fflags, rd_val) : (bits_fflags, bool) =
       riscv_f64Eq (rs1_val_D, rs2_val_D);
@@ -850,11 +852,11 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FEQ_D)) = {
 }
 
 function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FLT_D)) = {
-  let rs1_val_D = X_or_F_D(sys_enable_zfinx(), rs1);
-  let rs2_val_D = X_or_F_D(sys_enable_zfinx(), rs2);
+  let rs1_val_D = F(rs1);
+  let rs2_val_D = F(rs2);
 
   let (fflags, rd_val) : (bits_fflags, bool) =
-    riscv_f64Lt (rs1_val_D, rs2_val_D);
+      riscv_f64Lt (rs1_val_D, rs2_val_D);
 
   write_fflags(fflags);
   X(rd) = EXTZ(bool_to_bits(rd_val));
@@ -862,8 +864,8 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FLT_D)) = {
 }
 
 function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FLE_D)) = {
-  let rs1_val_D = X_or_F_D(sys_enable_zfinx(), rs1);
-  let rs2_val_D = X_or_F_D(sys_enable_zfinx(), rs2);
+  let rs1_val_D = F(rs1);
+  let rs2_val_D = F(rs2);
 
   let (fflags, rd_val) : (bits_fflags, bool) =
       riscv_f64Le (rs1_val_D, rs2_val_D);
@@ -888,51 +890,51 @@ mapping f_bin_type_mnemonic_D : f_bin_op_D <-> string = {
 
 mapping clause assembly = F_BIN_TYPE_D(rs2, rs1, rd, FSGNJ_D)
                       <-> f_bin_type_mnemonic_D(FSGNJ_D)
-                          ^ spc() ^ reg_or_freg_name(rd)
-                          ^ sep() ^ reg_or_freg_name(rs1)
-                          ^ sep() ^ reg_or_freg_name(rs2)
+                          ^ spc() ^ freg_name(rd)
+                          ^ sep() ^ freg_name(rs1)
+                          ^ sep() ^ freg_name(rs2)
 
 mapping clause assembly = F_BIN_TYPE_D(rs2, rs1, rd, FSGNJN_D)
                       <-> f_bin_type_mnemonic_D(FSGNJN_D)
-                          ^ spc() ^ reg_or_freg_name(rd)
-                          ^ sep() ^ reg_or_freg_name(rs1)
-                          ^ sep() ^ reg_or_freg_name(rs2)
+                          ^ spc() ^ freg_name(rd)
+                          ^ sep() ^ freg_name(rs1)
+                          ^ sep() ^ freg_name(rs2)
 
 mapping clause assembly = F_BIN_TYPE_D(rs2, rs1, rd, FSGNJX_D)
                       <-> f_bin_type_mnemonic_D(FSGNJX_D)
-                          ^ spc() ^ reg_or_freg_name(rd)
-                          ^ sep() ^ reg_or_freg_name(rs1)
-                          ^ sep() ^ reg_or_freg_name(rs2)
+                          ^ spc() ^ freg_name(rd)
+                          ^ sep() ^ freg_name(rs1)
+                          ^ sep() ^ freg_name(rs2)
 
 mapping clause assembly = F_BIN_TYPE_D(rs2, rs1, rd, FMIN_D)
                       <-> f_bin_type_mnemonic_D(FMIN_D)
-                          ^ spc() ^ reg_or_freg_name(rd)
-                          ^ sep() ^ reg_or_freg_name(rs1)
-                          ^ sep() ^ reg_or_freg_name(rs2)
+                          ^ spc() ^ freg_name(rd)
+                          ^ sep() ^ freg_name(rs1)
+                          ^ sep() ^ freg_name(rs2)
 
 mapping clause assembly = F_BIN_TYPE_D(rs2, rs1, rd, FMAX_D)
                       <-> f_bin_type_mnemonic_D(FMAX_D)
-                          ^ spc() ^ reg_or_freg_name(rd)
-                          ^ sep() ^ reg_or_freg_name(rs1)
-                          ^ sep() ^ reg_or_freg_name(rs2)
+                          ^ spc() ^ freg_name(rd)
+                          ^ sep() ^ freg_name(rs1)
+                          ^ sep() ^ freg_name(rs2)
 
 mapping clause assembly = F_BIN_TYPE_D(rs2, rs1, rd, FEQ_D)
                       <-> f_bin_type_mnemonic_D(FEQ_D)
                           ^ spc() ^ reg_name(rd)
-                          ^ sep() ^ reg_or_freg_name(rs1)
-                          ^ sep() ^ reg_or_freg_name(rs2)
+                          ^ sep() ^ freg_name(rs1)
+                          ^ sep() ^ freg_name(rs2)
 
 mapping clause assembly = F_BIN_TYPE_D(rs2, rs1, rd, FLT_D)
                       <-> f_bin_type_mnemonic_D(FLT_D)
                           ^ spc() ^ reg_name(rd)
-                          ^ sep() ^ reg_or_freg_name(rs1)
-                          ^ sep() ^ reg_or_freg_name(rs2)
+                          ^ sep() ^ freg_name(rs1)
+                          ^ sep() ^ freg_name(rs2)
 
 mapping clause assembly = F_BIN_TYPE_D(rs2, rs1, rd, FLE_D)
                       <-> f_bin_type_mnemonic_D(FLE_D)
                           ^ spc() ^ reg_name(rd)
-                          ^ sep() ^ reg_or_freg_name(rs1)
-                          ^ sep() ^ reg_or_freg_name(rs2)
+                          ^ sep() ^ freg_name(rs1)
+                          ^ sep() ^ freg_name(rs2)
 
 /* ****************************************************************** */
 /* Unary, no rounding mode */
@@ -941,21 +943,21 @@ union clause ast = F_UN_TYPE_D : (regidx, regidx, f_un_op_D)
 
 /* AST <-> Binary encoding ================================ */
 
-mapping clause encdec = F_UN_TYPE_D(rs1, rd, FCLASS_D)                        if supports_RV32D_or_RV64D([rs1])
-                    <-> 0b111_0001 @ 0b00000 @ rs1 @ 0b001 @ rd @ 0b101_0011  if supports_RV32D_or_RV64D([rs1])
+mapping clause encdec = F_UN_TYPE_D(rs1, rd, FCLASS_D)                        if haveDExt()
+                    <-> 0b111_0001 @ 0b00000 @ rs1 @ 0b001 @ rd @ 0b101_0011  if haveDExt()
 
 /* D instructions, RV64 only */
 
-mapping clause encdec = F_UN_TYPE_D(rs1, rd, FMV_X_D)                         if is_RV64D() & ~ (sys_enable_zfinx())
-                    <-> 0b111_0001 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011  if is_RV64D() & ~ (sys_enable_zfinx())
+mapping clause encdec = F_UN_TYPE_D(rs1, rd, FMV_X_D)                         if is_RV64D()
+                    <-> 0b111_0001 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011  if is_RV64D()
 
-mapping clause encdec = F_UN_TYPE_D(rs1, rd, FMV_D_X)                         if is_RV64D() & ~ (sys_enable_zfinx())
-                    <-> 0b111_1001 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011  if is_RV64D() & ~ (sys_enable_zfinx())
+mapping clause encdec = F_UN_TYPE_D(rs1, rd, FMV_D_X)                         if is_RV64D()
+                    <-> 0b111_1001 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011  if is_RV64D()
 
 /* Execution semantics ================================ */
 
 function clause execute (F_UN_TYPE_D(rs1, rd, FCLASS_D)) = {
-  let rs1_val_D = X_or_F_D(sys_enable_zfinx(), rs1);
+  let rs1_val_D = F(rs1);
 
   let rd_val_10b : bits (10) =
     if      f_is_neg_inf_D     (rs1_val_D) then 0b_00_0000_0001
@@ -1011,6 +1013,6 @@ mapping clause assembly = F_UN_TYPE_D(rs1, rd, FMV_D_X)
 mapping clause assembly = F_UN_TYPE_D(rs1, rd, FCLASS_D)
                       <-> f_un_type_mnemonic_D(FCLASS_D)
                           ^ spc() ^ reg_name(rd)
-                          ^ sep() ^ reg_or_freg_name(rs1)
+                          ^ sep() ^ freg_name(rs1)
 
 /* ****************************************************************** */
diff --git a/model/riscv_insts_fext.sail b/model/riscv_insts_fext.sail
index 8e42b01..69fc528 100644
--- a/model/riscv_insts_fext.sail
+++ b/model/riscv_insts_fext.sail
@@ -134,6 +134,10 @@ function fsplit_S   x32 = (x32[31..31], x32[30..23], x32[22..0])
 val      fmake_S  : (bits(1), bits(8), bits(23)) -> bits(32)
 function fmake_S (sign, exp, mant) = sign @ exp @ mant
 
+/* ---- Canonical NaNs */
+
+function canonical_NaN_S() -> bits(32) = 0x_7fc0_0000
+
 /* ---- Structure tests */
 
 val      f_is_neg_inf_S : bits(32) -> bool
@@ -316,6 +320,27 @@ function fle_S   (v1,       v2,        is_quiet) = {
 }
 
 /* **************************************************************** */
+/* NaN boxing/unboxing.                                             */
+/* 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'.                                      */
+
+val      nan_box : bits(32) -> flenbits
+function nan_box   val_32b =
+  if (sizeof(flen) == 32)
+  then val_32b
+  else 0x_FFFF_FFFF @ val_32b
+
+val      nan_unbox : flenbits -> bits(32)
+function nan_unbox   regval =
+  if (sizeof(flen) == 32)
+  then regval
+  else if regval [63..32] == 0x_FFFF_FFFF
+       then regval [31..0]
+       else canonical_NaN_S()
+
+/* **************************************************************** */
 /* Help-functions for 'encdec()' to restrict to certain             */
 /* combinations of {F,D} x {RV32,RV64}                              */
 
@@ -325,17 +350,6 @@ function is_RV64F          () -> bool = (haveFExt() & sizeof(xlen) == 64)
 function is_RV32D_or_RV64D () -> bool = (haveDExt() & (sizeof(xlen) == 32 | sizeof(xlen) == 64))
 function is_RV64D          () -> bool = (haveDExt() & sizeof(xlen) == 64)
 
-val supports_RV32D_or_RV64D : forall 'n, 'n > 0. (implicit('n), vector('n, dec, bits(5))) -> bool effect {rreg}
-function supports_RV32D_or_RV64D (reg_vec_len, registers) = {
-  if ~ (sys_enable_zfinx()) then is_RV32D_or_RV64D()
-  else if sys_enable_zfinx() & is_RV64D() then true
-  else {
-    foreach (x from 0 to (reg_vec_len - 1) ) {
-      if (registers[x][0] == bitone) then return false
-    };
-    true
-  }
-}
 /* ****************************************************************** */
 /* Floating-point loads                                               */
 
@@ -346,11 +360,11 @@ union clause ast = LOAD_FP : (bits(12), regidx, regidx, word_width)
 
 /* AST <-> Binary encoding ================================ */
 
-mapping clause encdec = LOAD_FP(imm, rs1, rd, WORD)          if is_RV32F_or_RV64F() & ~ (sys_enable_zfinx())
-                    <-> imm @ rs1 @ 0b010 @ rd @ 0b000_0111  if is_RV32F_or_RV64F() & ~ (sys_enable_zfinx())
+mapping clause encdec = LOAD_FP(imm, rs1, rd, WORD)          if is_RV32F_or_RV64F()
+                    <-> imm @ rs1 @ 0b010 @ rd @ 0b000_0111  if is_RV32F_or_RV64F()
 
-mapping clause encdec = LOAD_FP(imm, rs1, rd, DOUBLE)        if is_RV32D_or_RV64D() & ~ (sys_enable_zfinx())
-                    <-> imm @ rs1 @ 0b011 @ rd @ 0b000_0111  if is_RV32D_or_RV64D() & ~ (sys_enable_zfinx())
+mapping clause encdec = LOAD_FP(imm, rs1, rd, DOUBLE)        if is_RV32D_or_RV64D()
+                    <-> imm @ rs1 @ 0b011 @ rd @ 0b000_0111  if is_RV32D_or_RV64D()
 
 /* Execution semantics ================================ */
 
@@ -371,7 +385,7 @@ val process_fload32 : (regidx, xlenbits, MemoryOpResult(bits(32)))
                       -> Retired effect {escape, rreg, wreg}
 function process_fload32(rd, addr, value) =
   match value {
-    MemValue(result) => { F(rd) = nan_box(false, result); RETIRE_SUCCESS },
+    MemValue(result) => { F(rd) = nan_box(result); RETIRE_SUCCESS },
     MemException(e)  => { handle_mem_exception(addr, e); RETIRE_FAIL }
   }
 
@@ -406,7 +420,7 @@ function clause execute(LOAD_FP(imm, rs1, rd, width)) = {
 
 mapping clause assembly = LOAD_FP(imm, rs1, rd, width)
                       <-> "fl" ^ size_mnemonic(width)
-                          ^ spc() ^ reg_or_freg_name(rd)
+                          ^ spc() ^ freg_name(rd)
                           ^ sep() ^ hex_bits_12(imm)
                           ^ opt_spc() ^ "(" ^ opt_spc() ^ reg_name(rs1) ^ opt_spc() ^ ")"
 
@@ -420,11 +434,11 @@ union clause ast = STORE_FP : (bits(12), regidx, regidx, word_width)
 
 /* AST <-> Binary encoding ================================ */
 
-mapping clause encdec = STORE_FP(imm7 @ imm5, rs2, rs1, WORD)                             if is_RV32F_or_RV64F() & ~ (sys_enable_zfinx())
-                    <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b010 @ imm5 : bits(5) @ 0b010_0111  if is_RV32F_or_RV64F() & ~ (sys_enable_zfinx())
+mapping clause encdec = STORE_FP(imm7 @ imm5, rs2, rs1, WORD)                             if is_RV32F_or_RV64F()
+                    <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b010 @ imm5 : bits(5) @ 0b010_0111  if is_RV32F_or_RV64F()
 
-mapping clause encdec = STORE_FP(imm7 @ imm5, rs2, rs1, DOUBLE)                           if is_RV32D_or_RV64D() & ~ (sys_enable_zfinx())
-                    <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b011 @ imm5 : bits(5) @ 0b010_0111  if is_RV32D_or_RV64D() & ~ (sys_enable_zfinx())
+mapping clause encdec = STORE_FP(imm7 @ imm5, rs2, rs1, DOUBLE)                           if is_RV32D_or_RV64D()
+                    <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b011 @ imm5 : bits(5) @ 0b010_0111  if is_RV32D_or_RV64D()
 
 /* Execution semantics ================================ */
 
@@ -508,9 +522,9 @@ mapping clause encdec =
 /* Execution semantics ================================ */
 
 function clause execute (F_MADD_TYPE_S(rs3, rs2, rs1, rm, rd, op)) = {
-  let rs1_val_32b = X_or_F_S(sys_enable_zfinx(), rs1);
-  let rs2_val_32b = X_or_F_S(sys_enable_zfinx(), rs2);
-  let rs3_val_32b = X_or_F_S(sys_enable_zfinx(), rs3);
+  let rs1_val_32b = nan_unbox (F(rs1));
+  let rs2_val_32b = nan_unbox (F(rs2));
+  let rs3_val_32b = nan_unbox (F(rs3));
   match (select_instr_or_fcsr_rm (rm)) {
     None() => { handle_illegal(); RETIRE_FAIL },
     Some(rm') => {
@@ -523,7 +537,7 @@ function clause execute (F_MADD_TYPE_S(rs3, rs2, rs1, rm, rd, op)) = {
           FNMADD_S => riscv_f32MulAdd (rm_3b, negate_S (rs1_val_32b), rs2_val_32b, negate_S (rs3_val_32b))
         };
       write_fflags(fflags);
-      X_or_F_S(sys_enable_zfinx(), rd, rd_val_32b);
+      F(rd) = nan_box (rd_val_32b);
       RETIRE_SUCCESS
     }
   }
@@ -540,10 +554,10 @@ mapping f_madd_type_mnemonic_S : f_madd_op_S <-> string = {
 
 mapping clause assembly = F_MADD_TYPE_S(rs3, rs2, rs1, rm, rd, op)
                       <-> f_madd_type_mnemonic_S(op)
-                          ^ spc() ^ reg_or_freg_name(rd)
-                          ^ sep() ^ reg_or_freg_name(rs1)
-                          ^ sep() ^ reg_or_freg_name(rs2)
-                          ^ sep() ^ reg_or_freg_name(rs3)
+                          ^ spc() ^ freg_name(rd)
+                          ^ sep() ^ freg_name(rs1)
+                          ^ sep() ^ freg_name(rs2)
+                          ^ sep() ^ freg_name(rs3)
                           ^ sep() ^ frm_mnemonic(rm)
 
 /* ****************************************************************** */
@@ -574,8 +588,8 @@ mapping clause encdec =
 /* Execution semantics ================================ */
 
 function clause execute (F_BIN_RM_TYPE_S(rs2, rs1, rm, rd, op)) = {
-  let rs1_val_32b = X_or_F_S(sys_enable_zfinx(), rs1);
-  let rs2_val_32b = X_or_F_S(sys_enable_zfinx(), rs2);
+  let rs1_val_32b = nan_unbox (F(rs1));
+  let rs2_val_32b = nan_unbox (F(rs2));
   match (select_instr_or_fcsr_rm (rm)) {
     None() => { handle_illegal(); RETIRE_FAIL },
     Some(rm') => {
@@ -587,7 +601,7 @@ function clause execute (F_BIN_RM_TYPE_S(rs2, rs1, rm, rd, op)) = {
         FDIV_S  => riscv_f32Div (rm_3b, rs1_val_32b, rs2_val_32b)
       };
       write_fflags(fflags);
-      X_or_F_S(sys_enable_zfinx(), rd, rd_val_32b);
+      F(rd) = nan_box (rd_val_32b);
       RETIRE_SUCCESS
     }
   }
@@ -604,9 +618,9 @@ mapping f_bin_rm_type_mnemonic_S : f_bin_rm_op_S <-> string = {
 
 mapping clause assembly = F_BIN_RM_TYPE_S(rs2, rs1, rm, rd, op)
                       <-> f_bin_rm_type_mnemonic_S(op)
-                          ^ spc() ^ reg_or_freg_name(rd)
-                          ^ sep() ^ reg_or_freg_name(rs1)
-                          ^ sep() ^ reg_or_freg_name(rs2)
+                          ^ spc() ^ freg_name(rd)
+                          ^ sep() ^ freg_name(rs1)
+                          ^ sep() ^ freg_name(rs2)
                           ^ sep() ^ frm_mnemonic(rm)
 
 /* ****************************************************************** */
@@ -659,7 +673,7 @@ mapping clause encdec =
 /* Execution semantics ================================ */
 
 function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FSQRT_S)) = {
-  let rs1_val_S = X_or_F_S(sys_enable_zfinx(), rs1);
+  let rs1_val_S = nan_unbox (F(rs1));
   match (select_instr_or_fcsr_rm (rm)) {
     None() => { handle_illegal(); RETIRE_FAIL },
     Some(rm') => {
@@ -667,14 +681,14 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FSQRT_S)) = {
       let (fflags, rd_val_S) = riscv_f32Sqrt   (rm_3b, rs1_val_S);
 
       write_fflags(fflags);
-      X_or_F_S(sys_enable_zfinx(), rd, rd_val_S);
+      F(rd) = nan_box (rd_val_S);
       RETIRE_SUCCESS
     }
   }
 }
 
 function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_W_S)) = {
-  let rs1_val_S = X_or_F_S(sys_enable_zfinx(), rs1);
+  let rs1_val_S = nan_unbox (F(rs1));
   match (select_instr_or_fcsr_rm (rm)) {
     None() => { handle_illegal(); RETIRE_FAIL },
     Some(rm') => {
@@ -689,7 +703,7 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_W_S)) = {
 }
 
 function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_WU_S)) = {
-  let rs1_val_S = X_or_F_S(sys_enable_zfinx(), rs1);
+  let rs1_val_S = nan_unbox (F(rs1));
   match (select_instr_or_fcsr_rm (rm)) {
     None() => { handle_illegal(); RETIRE_FAIL },
     Some(rm') => {
@@ -712,7 +726,7 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_W)) = {
       let (fflags, rd_val_S) = riscv_i32ToF32 (rm_3b, rs1_val_W);
 
       write_fflags(fflags);
-      X_or_F_S(sys_enable_zfinx(), rd, rd_val_S);
+      F(rd) = nan_box (rd_val_S);
       RETIRE_SUCCESS
     }
   }
@@ -727,7 +741,7 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_WU)) = {
       let (fflags, rd_val_S) = riscv_ui32ToF32 (rm_3b, rs1_val_WU);
 
       write_fflags(fflags);
-      X_or_F_S(sys_enable_zfinx(), rd, rd_val_S);
+      F(rd) = nan_box (rd_val_S);
       RETIRE_SUCCESS
     }
   }
@@ -735,7 +749,7 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_WU)) = {
 
 function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_L_S)) = {
   assert(sizeof(xlen) >= 64);
-  let rs1_val_S = X_or_F_S(sys_enable_zfinx(), rs1);
+  let rs1_val_S = nan_unbox (F(rs1));
   match (select_instr_or_fcsr_rm (rm)) {
     None() => { handle_illegal(); RETIRE_FAIL },
     Some(rm') => {
@@ -751,7 +765,7 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_L_S)) = {
 
 function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_LU_S)) = {
   assert(sizeof(xlen) >= 64);
-  let rs1_val_S = X_or_F_S(sys_enable_zfinx(), rs1);
+  let rs1_val_S = nan_unbox (F(rs1));
   match (select_instr_or_fcsr_rm (rm)) {
     None() => { handle_illegal(); RETIRE_FAIL },
     Some(rm') => {
@@ -775,7 +789,7 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_L)) = {
       let (fflags, rd_val_S) = riscv_i64ToF32 (rm_3b, rs1_val_L);
 
       write_fflags(fflags);
-      X_or_F_S(sys_enable_zfinx(), rd, rd_val_S);
+      F(rd) = nan_box (rd_val_S);
       RETIRE_SUCCESS
     }
   }
@@ -791,7 +805,7 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_LU)) = {
       let (fflags, rd_val_S) = riscv_ui64ToF32 (rm_3b, rs1_val_LU);
 
       write_fflags(fflags);
-      X_or_F_S(sys_enable_zfinx(), rd, rd_val_S);
+      F(rd) = nan_box (rd_val_S);
       RETIRE_SUCCESS
     }
   }
@@ -814,55 +828,55 @@ mapping f_un_rm_type_mnemonic_S : f_un_rm_op_S <-> string = {
 
 mapping clause assembly = F_UN_RM_TYPE_S(rs1, rm, rd, FSQRT_S)
                       <-> f_un_rm_type_mnemonic_S(FSQRT_S)
-                          ^ spc() ^ reg_or_freg_name(rd)
-                          ^ sep() ^ reg_or_freg_name(rs1)
+                          ^ spc() ^ freg_name(rd)
+                          ^ sep() ^ freg_name(rs1)
                           ^ sep() ^ frm_mnemonic(rm)
 
 mapping clause assembly = F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_W_S)
                       <-> f_un_rm_type_mnemonic_S(FCVT_W_S)
                           ^ spc() ^ reg_name(rd)
-                          ^ sep() ^ reg_or_freg_name(rs1)
+                          ^ sep() ^ freg_name(rs1)
                           ^ sep() ^ frm_mnemonic(rm)
 
 mapping clause assembly = F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_WU_S)
                       <-> f_un_rm_type_mnemonic_S(FCVT_WU_S)
                           ^ spc() ^ reg_name(rd)
-                          ^ sep() ^ reg_or_freg_name(rs1)
+                          ^ sep() ^ freg_name(rs1)
                           ^ sep() ^ frm_mnemonic(rm)
 
 mapping clause assembly = F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_W)
                       <-> f_un_rm_type_mnemonic_S(FCVT_S_W)
-                          ^ spc() ^ reg_or_freg_name(rd)
+                          ^ spc() ^ freg_name(rd)
                           ^ sep() ^ reg_name(rs1)
                           ^ sep() ^ frm_mnemonic(rm)
 
 mapping clause assembly = F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_WU)
                       <-> f_un_rm_type_mnemonic_S(FCVT_S_WU)
-                          ^ spc() ^ reg_or_freg_name(rd)
+                          ^ spc() ^ freg_name(rd)
                           ^ sep() ^ reg_name(rs1)
                           ^ sep() ^ frm_mnemonic(rm)
 
 mapping clause assembly = F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_L_S)
                       <-> f_un_rm_type_mnemonic_S(FCVT_L_S)
                           ^ spc() ^ reg_name(rd)
-                          ^ sep() ^ reg_or_freg_name(rs1)
+                          ^ sep() ^ freg_name(rs1)
                           ^ sep() ^ frm_mnemonic(rm)
 
 mapping clause assembly = F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_LU_S)
                       <-> f_un_rm_type_mnemonic_S(FCVT_LU_S)
                           ^ spc() ^ reg_name(rd)
-                          ^ sep() ^ reg_or_freg_name(rs1)
+                          ^ sep() ^ freg_name(rs1)
                           ^ sep() ^ frm_mnemonic(rm)
 
 mapping clause assembly = F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_L)
                       <-> f_un_rm_type_mnemonic_S(FCVT_S_L)
-                          ^ spc() ^ reg_or_freg_name(rd)
+                          ^ spc() ^ freg_name(rd)
                           ^ sep() ^ reg_name(rs1)
                           ^ sep() ^ frm_mnemonic(rm)
 
 mapping clause assembly = F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_LU)
                       <-> f_un_rm_type_mnemonic_S(FCVT_S_LU)
-                          ^ spc() ^ reg_or_freg_name(rd)
+                          ^ spc() ^ freg_name(rd)
                           ^ sep() ^ reg_name(rs1)
                           ^ sep() ^ frm_mnemonic(rm)
 
@@ -903,41 +917,41 @@ mapping clause encdec = F_BIN_TYPE_S(rs2, rs1, rd, FLE_S)                 if is_
 /* Execution semantics ================================ */
 
 function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FSGNJ_S)) = {
-  let rs1_val_S    = X_or_F_S(sys_enable_zfinx(), rs1);
-  let rs2_val_S    = X_or_F_S(sys_enable_zfinx(), rs2);
+  let rs1_val_S    = nan_unbox (F(rs1));
+  let rs2_val_S    = nan_unbox (F(rs2));
   let (s1, e1, m1) = fsplit_S (rs1_val_S);
   let (s2, e2, m2) = fsplit_S (rs2_val_S);
   let rd_val_S     = fmake_S (s2, e1, m1);
 
-  X_or_F_S(sys_enable_zfinx(), rd, rd_val_S);
+  F(rd) = nan_box (rd_val_S);
   RETIRE_SUCCESS
 }
 
 function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FSGNJN_S)) = {
-  let rs1_val_S    = X_or_F_S(sys_enable_zfinx(), rs1);
-  let rs2_val_S    = X_or_F_S(sys_enable_zfinx(), rs2);
+  let rs1_val_S    = nan_unbox (F(rs1));
+  let rs2_val_S    = nan_unbox (F(rs2));
   let (s1, e1, m1) = fsplit_S (rs1_val_S);
   let (s2, e2, m2) = fsplit_S (rs2_val_S);
   let rd_val_S     = fmake_S (0b1 ^ s2, e1, m1);
 
-  X_or_F_S(sys_enable_zfinx(), rd, rd_val_S);
+  F(rd) = nan_box (rd_val_S);
   RETIRE_SUCCESS
 }
 
 function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FSGNJX_S)) = {
-  let rs1_val_S    = X_or_F_S(sys_enable_zfinx(), rs1);
-  let rs2_val_S    = X_or_F_S(sys_enable_zfinx(), rs2);
+  let rs1_val_S    = nan_unbox (F(rs1));
+  let rs2_val_S    = nan_unbox (F(rs2));
   let (s1, e1, m1) = fsplit_S (rs1_val_S);
   let (s2, e2, m2) = fsplit_S (rs2_val_S);
   let rd_val_S     = fmake_S (s1 ^ s2, e1, m1);
 
-  X_or_F_S(sys_enable_zfinx(), rd, rd_val_S);
+  F(rd) = nan_box (rd_val_S);
   RETIRE_SUCCESS
 }
 
 function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FMIN_S)) = {
-  let rs1_val_S = X_or_F_S(sys_enable_zfinx(), rs1);
-  let rs2_val_S = X_or_F_S(sys_enable_zfinx(), rs2);
+  let rs1_val_S = nan_unbox (F(rs1));
+  let rs2_val_S = nan_unbox (F(rs2));
 
   let is_quiet  = true;
   let (rs1_lt_rs2, fflags) = fle_S (rs1_val_S, rs2_val_S, is_quiet);
@@ -951,13 +965,13 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FMIN_S)) = {
                   else /* (not rs1_lt_rs2) */                                            rs2_val_S;
 
   accrue_fflags(fflags);
-  X_or_F_S(sys_enable_zfinx(), rd, rd_val_S);
+  F(rd) = nan_box (rd_val_S);
   RETIRE_SUCCESS
 }
 
 function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FMAX_S)) = {
-  let rs1_val_S = X_or_F_S(sys_enable_zfinx(), rs1);
-  let rs2_val_S = X_or_F_S(sys_enable_zfinx(), rs2);
+  let rs1_val_S = nan_unbox (F(rs1));
+  let rs2_val_S = nan_unbox (F(rs2));
 
   let is_quiet  = true;
   let (rs2_lt_rs1, fflags) = fle_S (rs2_val_S, rs1_val_S, is_quiet);
@@ -971,13 +985,13 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FMAX_S)) = {
                   else /* (not rs2_lt_rs1) */                                            rs2_val_S;
 
   accrue_fflags(fflags);
-  X_or_F_S(sys_enable_zfinx(), rd, rd_val_S);
+  F(rd) = nan_box (rd_val_S);
   RETIRE_SUCCESS
 }
 
 function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FEQ_S)) = {
-  let rs1_val_S = X_or_F_S(sys_enable_zfinx(), rs1);
-  let rs2_val_S = X_or_F_S(sys_enable_zfinx(), rs2);
+  let rs1_val_S = nan_unbox (F(rs1));
+  let rs2_val_S = nan_unbox (F(rs2));
 
   let (fflags, rd_val) : (bits_fflags, bool) =
       riscv_f32Eq (rs1_val_S, rs2_val_S);
@@ -988,8 +1002,8 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FEQ_S)) = {
 }
 
 function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FLT_S)) = {
-  let rs1_val_S = X_or_F_S(sys_enable_zfinx(), rs1);
-  let rs2_val_S = X_or_F_S(sys_enable_zfinx(), rs2);
+  let rs1_val_S = nan_unbox (F(rs1));
+  let rs2_val_S = nan_unbox (F(rs2));
 
   let (fflags, rd_val) : (bits_fflags, bool) =
       riscv_f32Lt (rs1_val_S, rs2_val_S);
@@ -1000,8 +1014,8 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FLT_S)) = {
 }
 
 function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FLE_S)) = {
-  let rs1_val_S = X_or_F_S(sys_enable_zfinx(), rs1);
-  let rs2_val_S = X_or_F_S(sys_enable_zfinx(), rs2);
+  let rs1_val_S = nan_unbox (F(rs1));
+  let rs2_val_S = nan_unbox (F(rs2));
 
   let (fflags, rd_val) : (bits_fflags, bool) =
       riscv_f32Le (rs1_val_S, rs2_val_S);
@@ -1026,51 +1040,51 @@ mapping f_bin_type_mnemonic_S : f_bin_op_S <-> string = {
 
 mapping clause assembly = F_BIN_TYPE_S(rs2, rs1, rd, FSGNJ_S)
                       <-> f_bin_type_mnemonic_S(FSGNJ_S)
-                          ^ spc() ^ reg_or_freg_name(rd)
-                          ^ sep() ^ reg_or_freg_name(rs1)
-                          ^ sep() ^ reg_or_freg_name(rs2)
+                          ^ spc() ^ freg_name(rd)
+                          ^ sep() ^ freg_name(rs1)
+                          ^ sep() ^ freg_name(rs2)
 
 mapping clause assembly = F_BIN_TYPE_S(rs2, rs1, rd, FSGNJN_S)
                       <-> f_bin_type_mnemonic_S(FSGNJN_S)
-                          ^ spc() ^ reg_or_freg_name(rd)
-                          ^ sep() ^ reg_or_freg_name(rs1)
-                          ^ sep() ^ reg_or_freg_name(rs2)
+                          ^ spc() ^ freg_name(rd)
+                          ^ sep() ^ freg_name(rs1)
+                          ^ sep() ^ freg_name(rs2)
 
 mapping clause assembly = F_BIN_TYPE_S(rs2, rs1, rd, FSGNJX_S)
                       <-> f_bin_type_mnemonic_S(FSGNJX_S)
-                          ^ spc() ^ reg_or_freg_name(rd)
-                          ^ sep() ^ reg_or_freg_name(rs1)
-                          ^ sep() ^ reg_or_freg_name(rs2)
+                          ^ spc() ^ freg_name(rd)
+                          ^ sep() ^ freg_name(rs1)
+                          ^ sep() ^ freg_name(rs2)
 
 mapping clause assembly = F_BIN_TYPE_S(rs2, rs1, rd, FMIN_S)
                       <-> f_bin_type_mnemonic_S(FMIN_S)
-                          ^ spc() ^ reg_or_freg_name(rd)
-                          ^ sep() ^ reg_or_freg_name(rs1)
-                          ^ sep() ^ reg_or_freg_name(rs2)
+                          ^ spc() ^ freg_name(rd)
+                          ^ sep() ^ freg_name(rs1)
+                          ^ sep() ^ freg_name(rs2)
 
 mapping clause assembly = F_BIN_TYPE_S(rs2, rs1, rd, FMAX_S)
                       <-> f_bin_type_mnemonic_S(FMAX_S)
-                          ^ spc() ^ reg_or_freg_name(rd)
-                          ^ sep() ^ reg_or_freg_name(rs1)
-                          ^ sep() ^ reg_or_freg_name(rs2)
+                          ^ spc() ^ freg_name(rd)
+                          ^ sep() ^ freg_name(rs1)
+                          ^ sep() ^ freg_name(rs2)
 
 mapping clause assembly = F_BIN_TYPE_S(rs2, rs1, rd, FEQ_S)
                       <-> f_bin_type_mnemonic_S(FEQ_S)
                           ^ spc() ^ reg_name(rd)
-                          ^ sep() ^ reg_or_freg_name(rs1)
-                          ^ sep() ^ reg_or_freg_name(rs2)
+                          ^ sep() ^ freg_name(rs1)
+                          ^ sep() ^ freg_name(rs2)
 
 mapping clause assembly = F_BIN_TYPE_S(rs2, rs1, rd, FLT_S)
                       <-> f_bin_type_mnemonic_S(FLT_S)
                           ^ spc() ^ reg_name(rd)
-                          ^ sep() ^ reg_or_freg_name(rs1)
-                          ^ sep() ^ reg_or_freg_name(rs2)
+                          ^ sep() ^ freg_name(rs1)
+                          ^ sep() ^ freg_name(rs2)
 
 mapping clause assembly = F_BIN_TYPE_S(rs2, rs1, rd, FLE_S)
                       <-> f_bin_type_mnemonic_S(FLE_S)
                           ^ spc() ^ reg_name(rd)
-                          ^ sep() ^ reg_or_freg_name(rs1)
-                          ^ sep() ^ reg_or_freg_name(rs2)
+                          ^ sep() ^ freg_name(rs1)
+                          ^ sep() ^ freg_name(rs2)
 
 /* ****************************************************************** */
 /* Unary, no rounding mode */
@@ -1082,16 +1096,16 @@ union clause ast = F_UN_TYPE_S : (regidx, regidx, f_un_op_S)
 mapping clause encdec = F_UN_TYPE_S(rs1, rd, FCLASS_S)                        if haveFExt()
                     <-> 0b111_0000 @ 0b00000 @ rs1 @ 0b001 @ rd @ 0b101_0011  if haveFExt()
 
-mapping clause encdec = F_UN_TYPE_S(rs1, rd, FMV_X_W)                         if haveFExt()  & ~ (sys_enable_zfinx())
-                    <-> 0b111_0000 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011  if haveFExt()  & ~ (sys_enable_zfinx())
+mapping clause encdec = F_UN_TYPE_S(rs1, rd, FMV_X_W)                         if haveFExt()
+                    <-> 0b111_0000 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011  if haveFExt()
 
-mapping clause encdec = F_UN_TYPE_S(rs1, rd, FMV_W_X)                         if haveFExt()  & ~ (sys_enable_zfinx())
-                    <-> 0b111_1000 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011  if haveFExt()  & ~ (sys_enable_zfinx())
+mapping clause encdec = F_UN_TYPE_S(rs1, rd, FMV_W_X)                         if haveFExt()
+                    <-> 0b111_1000 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011  if haveFExt()
 
 /* Execution semantics ================================ */
 
 function clause execute (F_UN_TYPE_S(rs1, rd, FCLASS_S)) = {
-  let rs1_val_S = X_or_F_S(sys_enable_zfinx(), rs1);
+  let rs1_val_S = nan_unbox (F(rs1));
 
   let rd_val_10b : bits (10) =
     if      f_is_neg_inf_S     (rs1_val_S) then 0b_00_0000_0001
@@ -1120,7 +1134,7 @@ function clause execute (F_UN_TYPE_S(rs1, rd, FMV_X_W)) = {
 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(false, rd_val_S);
+  F(rd) = nan_box (rd_val_S);
   RETIRE_SUCCESS
 }
 
@@ -1145,6 +1159,6 @@ mapping clause assembly = F_UN_TYPE_S(rs1, rd, FMV_W_X)
 mapping clause assembly = F_UN_TYPE_S(rs1, rd, FCLASS_S)
                       <-> f_un_type_mnemonic_S(FCLASS_S)
                           ^ spc() ^ reg_name(rd)
-                          ^ sep() ^ reg_or_freg_name(rs1)
+                          ^ sep() ^ freg_name(rs1)
 
 /* ****************************************************************** */
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index 06be736..f5ee261 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -560,9 +560,9 @@ function init_sys() -> unit = {
   misa->S()   = 0b1;                            /* supervisor-mode */
 
   /* We currently support both F and D */
-  misa->F()   = bool_to_bits(sys_enable_fdext() & ~ (sys_enable_zfinx()));  /* single-precision */
-  misa->D()   = if   sizeof(flen) >= 64 & ~ (sys_enable_zfinx())
-                then bool_to_bits(sys_enable_fdext())                        /* double-precision */
+  misa->F()   = bool_to_bits(sys_enable_fdext());      /* single-precision */
+  misa->D()   = if   sizeof(flen) >= 64
+                then bool_to_bits(sys_enable_fdext())  /* double-precision */
                 else 0b0;
 
   mstatus = set_mstatus_SXL(mstatus, misa.MXL());
diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
index 28505e3..696d154 100644
--- a/model/riscv_sys_regs.sail
+++ b/model/riscv_sys_regs.sail
@@ -144,8 +144,6 @@ val sys_enable_writable_misa = {c: "sys_enable_writable_misa", ocaml: "Platform.
 val sys_enable_rvc = {c: "sys_enable_rvc", ocaml: "Platform.enable_rvc", _: "sys_enable_rvc"} : unit -> bool
 /* whether misa.{f,d} were enabled at boot */
 val sys_enable_fdext = {c: "sys_enable_fdext", ocaml: "Platform.enable_fdext", _: "sys_enable_fdext"} : unit -> bool
-/* whether zfinx was enabled at boot */
-val sys_enable_zfinx = {c: "sys_enable_zfinx",ocaml: "Platform.enable_zfinx", _: "sys_enable_zfinx"} : unit -> bool                       
 /* whether the N extension was enabled at boot */
 val sys_enable_next = {c: "sys_enable_next", ocaml: "Platform.enable_next", _: "sys_enable_next"} : unit -> bool
 
@@ -165,7 +163,7 @@ function legalize_misa(m : Misa, v : xlenbits) -> Misa = {
            then m
            else update_C(m, v.C());
          /* Handle updates for F/D. */
-         if   ~(sys_enable_fdext()) | (v.D() == 0b1 & v.F() == 0b0) | sys_enable_zfinx()
+         if   ~(sys_enable_fdext()) | (v.D() == 0b1 & v.F() == 0b0)
          then m
          else update_D(update_F(m, v.F()), v.D())
        }
@@ -280,7 +278,6 @@ function legalize_mstatus(o : Mstatus, v : xlenbits) -> Mstatus = {
 
   /* We don't have any extension context yet. */
   let m = update_XS(m, extStatus_to_bits(Off));
-  let m = if sys_enable_zfinx() then update_FS(m, extStatus_to_bits(Off)) else m;
   /* FS is WARL, and making FS writable can support the M-mode emulation of an FPU
    * to support code running in S/U-modes.  Spike does this, and for now, we match it.
    * FIXME: This should be made a platform parameter.
@@ -331,8 +328,8 @@ function in32BitMode() -> bool = {
 }
 
 /* F and D extensions have to enabled both via misa.{FD} as well as mstatus.FS */
-function haveFExt()    -> bool = (misa.F() == 0b1 & mstatus.FS() != 0b00) | sys_enable_zfinx()
-function haveDExt()    -> bool = (misa.D() == 0b1 & mstatus.FS() != 0b00) | (sys_enable_zfinx() & sizeof(flen)==64)
+function haveFExt()    -> bool = (misa.F() == 0b1) & (mstatus.FS() != 0b00)
+function haveDExt()    -> bool = (misa.D() == 0b1) & (mstatus.FS() != 0b00)
 
 /* interrupt processing state */