diff --git a/model/riscv_fdext_regs.sail b/model/riscv_fdext_regs.sail
index f94f08842..4806bfc38 100644
--- a/model/riscv_fdext_regs.sail
+++ b/model/riscv_fdext_regs.sail
@@ -37,7 +37,7 @@ function nan_box_H   val_16b =
 val      nan_unbox_H : flenbits -> bits(16)
 function nan_unbox_H   regval =
   if (sizeof(flen) == 32)
-  then if regval [32..16] == 0x_FFFF
+  then if regval [31..16] == 0x_FFFF
        then regval [15..0]
        else canonical_NaN_H()
   else if regval [63..16] == 0x_FFFF_FFFF_FFFF
diff --git a/model/riscv_insts_zfa.sail b/model/riscv_insts_zfa.sail
index b391b4c2e..9f1e19925 100644
--- a/model/riscv_insts_zfa.sail
+++ b/model/riscv_insts_zfa.sail
@@ -286,8 +286,8 @@ mapping clause assembly = RISCV_FMINM_D(rs2, rs1, rd)
                 ^ sep() ^ freg_name(rs2)
 
 function clause execute (RISCV_FMINM_D(rs2, rs1, rd)) = {
-  let rs1_val_D = F(rs1);
-  let rs2_val_D = F(rs2);
+  let rs1_val_D = F_D(rs1);
+  let rs2_val_D = F_D(rs2);
 
   let is_quiet  = true;
   let (rs1_lt_rs2, fflags) = fle_D (rs1_val_D, rs2_val_D, is_quiet);
@@ -299,7 +299,7 @@ function clause execute (RISCV_FMINM_D(rs2, rs1, rd)) = {
                   else                                                              rs2_val_D;
 
   accrue_fflags(fflags);
-  F(rd) = rd_val_D;
+  F_D(rd) = rd_val_D;
   RETIRE_SUCCESS
 }
 
@@ -316,8 +316,8 @@ mapping clause assembly = RISCV_FMAXM_D(rs2, rs1, rd)
                 ^ sep() ^ freg_name(rs2)
 
 function clause execute (RISCV_FMAXM_D(rs2, rs1, rd)) = {
-  let rs1_val_D = F(rs1);
-  let rs2_val_D = F(rs2);
+  let rs1_val_D = F_D(rs1);
+  let rs2_val_D = F_D(rs2);
 
   let is_quiet  = true;
   let (rs2_lt_rs1, fflags) = fle_D (rs2_val_D, rs1_val_D, is_quiet);
@@ -329,7 +329,7 @@ function clause execute (RISCV_FMAXM_D(rs2, rs1, rd)) = {
                   else                                                              rs2_val_D;
 
   accrue_fflags(fflags);
-  F(rd) = rd_val_D;
+  F_D(rd) = rd_val_D;
   RETIRE_SUCCESS
 }
 
@@ -458,7 +458,7 @@ mapping clause assembly = RISCV_FROUND_D(rs1, rm, rd)
                  ^ sep() ^ frm_mnemonic(rm)
 
 function clause execute (RISCV_FROUND_D(rs1, rm, rd)) = {
-  let rs1_val_D = F(rs1);
+  let rs1_val_D = F_D(rs1);
 
   match (select_instr_or_fcsr_rm(rm)) {
     None() => { handle_illegal(); RETIRE_FAIL },
@@ -467,7 +467,7 @@ function clause execute (RISCV_FROUND_D(rs1, rm, rd)) = {
       let (fflags, rd_val_D) = riscv_f64roundToInt(rm_3b, rs1_val_D, false);
 
       accrue_fflags(fflags);
-      F(rd) = rd_val_D;
+      F_D(rd) = rd_val_D;
       RETIRE_SUCCESS
     }
   }
diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
index fc20e4af4..33cbf876e 100644
--- a/model/riscv_sys_regs.sail
+++ b/model/riscv_sys_regs.sail
@@ -303,7 +303,7 @@ 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)
-function haveDExt()    -> bool = (misa[D] == 0b1) & (mstatus[FS] != 0b00)
+function haveDExt()    -> bool = (misa[D] == 0b1) & (mstatus[FS] != 0b00) & sizeof(flen) >= 64
 /* Zfh (half-precision) extension depends on misa.F and mstatus.FS */
 function haveZfh()     -> bool = (misa[F] == 0b1) & (mstatus[FS] != 0b00)
 /* V extension has to enable both via misa.V as well as mstatus.VS */