Merge branch 'master' into gdbgdb

38 files changed, 4094 insertions, 137 deletions

diff --git a/model/prelude_mem.sail b/model/prelude_mem.sail
index b8d47d0..85d141b 100644
--- a/model/prelude_mem.sail
+++ b/model/prelude_mem.sail
@@ -17,15 +17,16 @@
    would be even better if it could be <= 8 bytes so that data can
    also be a 64-bit int but CHERI needs 128-bit accesses for
    capabilities and SIMD / vector instructions will also need more. */
-   type max_mem_access : Int = 16
+type max_mem_access : Int = 16
 
-val write_ram : forall 'n, 0 < 'n <= max_mem_access . (write_kind, xlenbits, atom('n), bits(8 * 'n), mem_meta) -> bool effect {wmv, wmvt}
+val write_ram = {lem: "write_ram", coq: "write_ram"} : forall 'n, 0 < 'n <= max_mem_access . (write_kind, xlenbits, atom('n), bits(8 * 'n), mem_meta) -> bool effect {wmv, wmvt}
 function write_ram(wk, addr, width, data, meta) = {
   /* Write out metadata only if the value write succeeds.
    * It is assumed for now that this write always succeeds;
    * there is currently no return value.
-   * FIXME: We should convert the external API to consume
-   * the value along with the metadata to ensure atomicity.
+   * FIXME: We should convert the external API for all backends
+   * (not just for Lem) to consume the value along with the
+   * metadata to ensure atomicity.
    */
   let ret : bool = __write_mem(wk, sizeof(xlen), addr, width, data);
   if ret then __WriteRAM_Meta(addr, width, meta);
@@ -36,10 +37,10 @@ val write_ram_ea : forall 'n, 0 < 'n <= max_mem_access . (write_kind, xlenbits,
 function write_ram_ea(wk, addr, width) =
   __write_mem_ea(wk, sizeof(xlen), addr, width)
 
-/* FIXME: Make this also return the metadata, which will also require external API changes. */
-val read_ram : forall 'n, 0 < 'n <= max_mem_access .  (read_kind, xlenbits, atom('n)) -> bits(8 * 'n) effect {rmem}
-function read_ram(rk, addr, width) =
-  __read_mem(rk, sizeof(xlen), addr, width)
+val read_ram = {lem: "read_ram", coq: "read_ram"} : forall 'n, 0 < 'n <= max_mem_access .  (read_kind, xlenbits, atom('n), bool) -> (bits(8 * 'n), mem_meta) effect {rmem, rmemt}
+function read_ram(rk, addr, width, read_meta) =
+  let meta = if read_meta then __ReadRAM_Meta(addr, width) else default_meta in
+  (__read_mem(rk, sizeof(xlen), addr, width), meta)
 
 val __TraceMemoryWrite : forall 'n 'm. (atom('n), bits('m), bits(8 * 'n)) -> unit
 val __TraceMemoryRead  : forall 'n 'm. (atom('n), bits('m), bits(8 * 'n)) -> unit
diff --git a/model/riscv_csr_ext.sail b/model/riscv_csr_ext.sail
index 8c0cc17..9220534 100644
--- a/model/riscv_csr_ext.sail
+++ b/model/riscv_csr_ext.sail
@@ -1,8 +1,12 @@
 
-/* numeric fallback XXX apparent sail bug prevents this from compiling for C  */
-//mapping clause csr_name_map = reg <-> "UNKNOWN CSR: " ^ hex_bits_12(reg)
+mapping clause csr_name_map = reg <-> hex_bits_12(reg)
 end csr_name_map
 
+/* XXX due to an apparent Sail bug the definition of this function must appear
+   after the last csr_name_map clause and not by the val spec as it was 
+   previously. */
+function csr_name(csr) = csr_name_map(csr)
+
 function clause ext_is_CSR_defined(_, _) = false
 end ext_is_CSR_defined
 
diff --git a/model/riscv_csr_map.sail b/model/riscv_csr_map.sail
index 7ec161b..ba52da6 100644
--- a/model/riscv_csr_map.sail
+++ b/model/riscv_csr_map.sail
@@ -93,7 +93,6 @@ mapping clause csr_name_map = 0x7a2  <-> "tdata2"
 mapping clause csr_name_map = 0x7a3  <-> "tdata3"
 
 val csr_name : csreg -> string
-function csr_name(csr) = csr_name_map(csr)
 overload to_str = {csr_name}
 
 /* Extensions may want to add additional CSR registers to the CSR address map.
diff --git a/model/riscv_duopod.sail b/model/riscv_duopod.sail
index 395a332..b811824 100644
--- a/model/riscv_duopod.sail
+++ b/model/riscv_duopod.sail
@@ -1,4 +1,6 @@
-// This file depends on the xlen definitions in riscv_xlen.sail.
+
+$include "prelude.sail"
+$include "riscv_xlen64.sail"
 
 type regbits = bits(5)
 
@@ -23,7 +25,7 @@ function rX(r) =
 
 val wX : (regbits, xlenbits) -> unit effect {wreg}
 
-function wX (r, v) =
+function wX(r, v) =
   if r != 0b00000 then {
      Xs[unsigned(r)] = v;
   }
diff --git a/model/riscv_ext_regs.sail b/model/riscv_ext_regs.sail
index 9ff83b3..d9674f7 100644
--- a/model/riscv_ext_regs.sail
+++ b/model/riscv_ext_regs.sail
@@ -10,5 +10,22 @@ This function is called after above when running rvfi and allows the model
 to be initialised differently (e.g. CHERI cap regs are initialised
 to omnipotent instead of null).
  */
-val ext_rvfi_init : unit -> unit effect {wreg}
-function ext_rvfi_init () = ()
+val ext_rvfi_init : unit -> unit effect {rreg, wreg}
+function ext_rvfi_init () = {
+  x1 = x1 // to avoid hook being optimized out
+}
+
+
+/*!
+THIS(csrno, priv, isWrite) allows an extension to block access to csrno,
+at Privilege level priv. It should return true if the access is allowed.
+*/
+val ext_check_CSR : (bits(12), Privilege, bool) -> bool
+function ext_check_CSR (csrno, p, isWrite) = true
+
+/*!
+THIS is called if ext_check_CSR returns false. It should
+cause an appropriate RISCV exception.
+ */
+val ext_check_CSR_fail : unit->unit
+function ext_check_CSR_fail () = ()
diff --git a/model/riscv_fdext_control.sail b/model/riscv_fdext_control.sail
new file mode 100644
index 0000000..7155699
--- /dev/null
+++ b/model/riscv_fdext_control.sail
@@ -0,0 +1,24 @@
+/* **************************************************************** */
+/* Floating point register file and accessors for F, D extensions   */
+/* Floating point CSR and accessors                                 */
+/* **************************************************************** */
+
+/* Original version written by Rishiyur S. Nikhil, Sept-Oct 2019    */
+
+/* **************************************************************** */
+
+/* val clause ext_is_CSR_defined : (csreg, Privilege) -> bool effect {rreg} */
+
+function clause ext_is_CSR_defined (0x001, _) = haveFExt() | haveDExt()
+function clause ext_is_CSR_defined (0x002, _) = haveFExt() | haveDExt()
+function clause ext_is_CSR_defined (0x003, _) = haveFExt() | haveDExt()
+
+function clause ext_read_CSR (0x001) = Some (EXTZ (fcsr.FFLAGS()))
+function clause ext_read_CSR (0x002) = Some (EXTZ (fcsr.FRM()))
+function clause ext_read_CSR (0x003) = Some (EXTZ (fcsr.bits()))
+
+function clause ext_write_CSR (0x001, value) = write_fcsr (fcsr.FRM(), value [4..0])
+function clause ext_write_CSR (0x002, value) = write_fcsr (value [2..0], fcsr.FFLAGS())
+function clause ext_write_CSR (0x003, value) = write_fcsr (value [7..5], value [4..0])
+
+/* **************************************************************** */
diff --git a/model/riscv_fdext_regs.sail b/model/riscv_fdext_regs.sail
new file mode 100644
index 0000000..59efd22
--- /dev/null
+++ b/model/riscv_fdext_regs.sail
@@ -0,0 +1,294 @@
+/* **************************************************************** */
+/* Floating point register file and accessors for F, D extensions   */
+/* Floating point CSR and accessors                                 */
+/* **************************************************************** */
+
+/* Original version written by Rishiyur S. Nikhil, Sept-Oct 2019    */
+
+/* **************************************************************** */
+/* Floating point register file                                     */
+
+register fs : vector(32, dec, fregtype)
+
+register f0  : fregtype
+register f1  : fregtype
+register f2  : fregtype
+register f3  : fregtype
+register f4  : fregtype
+register f5  : fregtype
+register f6  : fregtype
+register f7  : fregtype
+register f8  : fregtype
+register f9  : fregtype
+register f10 : fregtype
+register f11 : fregtype
+register f12 : fregtype
+register f13 : fregtype
+register f14 : fregtype
+register f15 : fregtype
+register f16 : fregtype
+register f17 : fregtype
+register f18 : fregtype
+register f19 : fregtype
+register f20 : fregtype
+register f21 : fregtype
+register f22 : fregtype
+register f23 : fregtype
+register f24 : fregtype
+register f25 : fregtype
+register f26 : fregtype
+register f27 : fregtype
+register f28 : fregtype
+register f29 : fregtype
+register f30 : fregtype
+register f31 : fregtype
+
+function dirty_fd_context() -> unit = {
+  mstatus->FS() = extStatus_to_bits(Dirty);
+  mstatus->SD() = 0b1
+}
+
+val rF : forall 'n, 0 <= 'n < 32. regno('n) -> flenbits effect {rreg, escape}
+function rF r = {
+  let v : fregtype =
+    match r {
+      0 => f0,
+      1 => f1,
+      2 => f2,
+      3 => f3,
+      4 => f4,
+      5 => f5,
+      6 => f6,
+      7 => f7,
+      8 => f8,
+      9 => f9,
+      10 => f10,
+      11 => f11,
+      12 => f12,
+      13 => f13,
+      14 => f14,
+      15 => f15,
+      16 => f16,
+      17 => f17,
+      18 => f18,
+      19 => f19,
+      20 => f20,
+      21 => f21,
+      22 => f22,
+      23 => f23,
+      24 => f24,
+      25 => f25,
+      26 => f26,
+      27 => f27,
+      28 => f28,
+      29 => f29,
+      30 => f30,
+      31 => f31,
+      _  => {assert(false, "invalid floating point register number"); zero_freg}
+    };
+  fregval_from_freg(v)
+}
+
+val wF : forall 'n, 0 <= 'n < 32. (regno('n), flenbits) -> unit effect {wreg, escape}
+function wF (r, in_v) = {
+  let v = fregval_into_freg(in_v);
+  match r {
+    0  => f0 = v,
+    1  => f1 = v,
+    2  => f2 = v,
+    3  => f3 = v,
+    4  => f4 = v,
+    5  => f5 = v,
+    6  => f6 = v,
+    7  => f7 = v,
+    8  => f8 = v,
+    9  => f9 = v,
+    10 => f10 = v,
+    11 => f11 = v,
+    12 => f12 = v,
+    13 => f13 = v,
+    14 => f14 = v,
+    15 => f15 = v,
+    16 => f16 = v,
+    17 => f17 = v,
+    18 => f18 = v,
+    19 => f19 = v,
+    20 => f20 = v,
+    21 => f21 = v,
+    22 => f22 = v,
+    23 => f23 = v,
+    24 => f24 = v,
+    25 => f25 = v,
+    26 => f26 = v,
+    27 => f27 = v,
+    28 => f28 = v,
+    29 => f29 = v,
+    30 => f30 = v,
+    31 => f31 = v,
+    _  => assert(false, "invalid floating point register number")
+  };
+
+  dirty_fd_context();
+
+  if   get_config_print_reg()
+  then
+      /* TODO: will only print bits; should we print in floating point format? */
+      print_reg("f" ^ string_of_int(r) ^ " <- " ^ FRegStr(v));
+}
+
+function rF_bits(i: bits(5)) -> flenbits = rF(unsigned(i))
+
+function wF_bits(i: bits(5), data: flenbits) -> unit = {
+  wF(unsigned(i)) = data
+}
+
+overload F = {rF_bits, wF_bits, rF, wF}
+
+/* register names */
+
+val freg_name_abi : regidx <-> string
+
+mapping freg_name_abi = {
+    0b00000 <-> "ft0",
+    0b00001 <-> "ft1",
+    0b00010 <-> "ft2",
+    0b00011 <-> "ft3",
+    0b00100 <-> "ft4",
+    0b00101 <-> "ft5",
+    0b00110 <-> "ft6",
+    0b00111 <-> "ft7",
+    0b01000 <-> "fs0",
+    0b01001 <-> "fs1",
+    0b01010 <-> "fa0",
+    0b01011 <-> "fa1",
+    0b01100 <-> "fa2",
+    0b01101 <-> "fa3",
+    0b01110 <-> "fa4",
+    0b01111 <-> "fa5",
+    0b10000 <-> "fa6",
+    0b10001 <-> "fa7",
+    0b10010 <-> "fs2",
+    0b10011 <-> "fs3",
+    0b10100 <-> "fs4",
+    0b10101 <-> "fs5",
+    0b10110 <-> "fs6",
+    0b10111 <-> "fs7",
+    0b11000 <-> "fs8",
+    0b11001 <-> "fs9",
+    0b11010 <-> "fs10",
+    0b11011 <-> "fs11",
+    0b11100 <-> "ft8",
+    0b11101 <-> "ft9",
+    0b11110 <-> "ft10",
+    0b11111 <-> "ft11"
+}
+
+overload to_str = {freg_name_abi}
+
+/* mappings for assembly */
+
+val freg_name : bits(5) <-> string
+mapping freg_name = {
+    0b00000 <-> "ft0",
+    0b00001 <-> "ft1",
+    0b00010 <-> "ft2",
+    0b00011 <-> "ft3",
+    0b00100 <-> "ft4",
+    0b00101 <-> "ft5",
+    0b00110 <-> "ft6",
+    0b00111 <-> "ft7",
+    0b01000 <-> "fs0",
+    0b01001 <-> "fs1",
+    0b01010 <-> "fa0",
+    0b01011 <-> "fa1",
+    0b01100 <-> "fa2",
+    0b01101 <-> "fa3",
+    0b01110 <-> "fa4",
+    0b01111 <-> "fa5",
+    0b10000 <-> "fa6",
+    0b10001 <-> "fa7",
+    0b10010 <-> "fs2",
+    0b10011 <-> "fs3",
+    0b10100 <-> "fs4",
+    0b10101 <-> "fs5",
+    0b10110 <-> "fs6",
+    0b10111 <-> "fs7",
+    0b11000 <-> "fs8",
+    0b11001 <-> "fs9",
+    0b11010 <-> "fs10",
+    0b11011 <-> "fs11",
+    0b11100 <-> "ft8",
+    0b11101 <-> "ft9",
+    0b11110 <-> "ft10",
+    0b11111 <-> "ft11"
+}
+
+val init_fdext_regs : unit -> unit effect {wreg}
+function init_fdext_regs () = {
+  f0  = zero_freg;
+  f1  = zero_freg;
+  f2  = zero_freg;
+  f3  = zero_freg;
+  f4  = zero_freg;
+  f5  = zero_freg;
+  f6  = zero_freg;
+  f7  = zero_freg;
+  f8  = zero_freg;
+  f9  = zero_freg;
+  f10 = zero_freg;
+  f11 = zero_freg;
+  f12 = zero_freg;
+  f13 = zero_freg;
+  f14 = zero_freg;
+  f15 = zero_freg;
+  f16 = zero_freg;
+  f17 = zero_freg;
+  f18 = zero_freg;
+  f19 = zero_freg;
+  f20 = zero_freg;
+  f21 = zero_freg;
+  f22 = zero_freg;
+  f23 = zero_freg;
+  f24 = zero_freg;
+  f25 = zero_freg;
+  f26 = zero_freg;
+  f27 = zero_freg;
+  f28 = zero_freg;
+  f29 = zero_freg;
+  f30 = zero_freg;
+  f31 = zero_freg
+}
+
+/* **************************************************************** */
+/* Floating Point CSR                                               */
+/*     fflags    address 0x001    same as fcrs [4..0]               */
+/*     frm       address 0x002    same as fcrs [7..5]               */
+/*     fcsr      address 0x003                                      */
+
+
+bitfield Fcsr : bits(32) = {
+  FRM    : 7 .. 5,
+  FFLAGS : 4 .. 0,
+}
+
+register fcsr : Fcsr
+
+val write_fcsr : (bits(3), bits(5)) -> option(xlenbits) effect {rreg, wreg}
+function write_fcsr (frm, fflags) = {
+  fcsr->FRM()    = frm;      /* Note: frm can be an illegal value, 101, 110, 111 */
+  fcsr->FFLAGS() = fflags;
+  dirty_fd_context();
+  Some (EXTZ (fcsr.bits()))
+}
+
+val write_fflags : (bits(5)) -> unit effect {rreg, wreg}
+function write_fflags(fflags) = {
+  fcsr->FFLAGS() = fflags;
+  dirty_fd_context();
+}
+
+val write_frm : (bits(3)) -> unit effect {rreg, wreg}
+function write_frm(frm) = {
+  fcsr->FRM()    = frm;
+  dirty_fd_context();
+}
diff --git a/model/riscv_fetch.sail b/model/riscv_fetch.sail
index 64aff4b..cdda96e 100644
--- a/model/riscv_fetch.sail
+++ b/model/riscv_fetch.sail
@@ -4,7 +4,7 @@
 
 function isRVC(h : half) -> bool = ~ (h[1 .. 0] == 0b11)
 
-val fetch : unit -> FetchResult effect {escape, rmem, rreg, wmv, wmvt, wreg}
+val fetch : unit -> FetchResult effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
 function fetch() -> FetchResult =
   /* fetch PC check for extensions: extensions return a transformed PC to fetch,
    * but any exceptions use the untransformed PC.
@@ -22,7 +22,7 @@ function fetch() -> FetchResult =
            * exceptions.
            */
           match mem_read(Execute(), ppclo, 2, false, false, false) {
-            MemException(e) => F_Error(E_Fetch_Access_Fault(), PC),
+            MemException(e) => F_Error(e, PC),
             MemValue(ilo)   => {
               if   isRVC(ilo)
               then F_RVC(ilo)
@@ -36,7 +36,7 @@ function fetch() -> FetchResult =
                       TR_Failure(e, _)     => F_Error(e, PC_hi),
                       TR_Address(ppchi, _) => {
                         match mem_read(Execute(), ppchi, 2, false, false, false) {
-                          MemException(e) => F_Error(E_Fetch_Access_Fault(), PC_hi),
+                          MemException(e) => F_Error(e, PC_hi),
                           MemValue(ihi)   => F_Base(append(ihi, ilo))
                         }
                       }
diff --git a/model/riscv_flen_D.sail b/model/riscv_flen_D.sail
new file mode 100644
index 0000000..eabd613
--- /dev/null
+++ b/model/riscv_flen_D.sail
@@ -0,0 +1,5 @@
+/* Define the FLEN value for the 'D' extension. */
+
+type flen       : Int = 64
+type flen_bytes : Int = 8
+type flenbits         = bits(flen)
diff --git a/model/riscv_flen_F.sail b/model/riscv_flen_F.sail
new file mode 100644
index 0000000..ad5b381
--- /dev/null
+++ b/model/riscv_flen_F.sail
@@ -0,0 +1,5 @@
+/* Define the FLEN value for the 'F' extension. */
+
+type flen       : Int = 32
+type flen_bytes : Int = 4
+type flenbits         = bits(flen)
diff --git a/model/riscv_freg_type.sail b/model/riscv_freg_type.sail
new file mode 100644
index 0000000..3b099db
--- /dev/null
+++ b/model/riscv_freg_type.sail
@@ -0,0 +1,52 @@
+/* Definitions for floating point registers (F and D extensions) */
+
+/* default register type */
+type fregtype = flenbits
+
+/* default zero register */
+let zero_freg : fregtype = EXTZ(0x0)
+
+/* default register printer */
+val FRegStr : fregtype -> string
+function FRegStr(r) = BitStr(r)
+
+/* conversions */
+
+val fregval_from_freg : fregtype -> flenbits
+function fregval_from_freg(r) = r
+
+val fregval_into_freg : flenbits -> fregtype
+function fregval_into_freg(v) = v
+
+
+/* Rounding Mode
+    Rounding modes occur as a 3-bit field in F,D instructions,
+    and also as a 3-bit 'frm' field in the 'fcsr' CSR.
+    RISC-V uses the following IEEE-defined rounding modes.
+*/
+
+enum rounding_mode = {RM_RNE, RM_RTZ, RM_RDN, RM_RUP, RM_RMM, RM_DYN}
+
+enum f_madd_op_S = {FMADD_S, FMSUB_S, FNMSUB_S, FNMADD_S}
+
+enum f_bin_rm_op_S = {FADD_S, FSUB_S, FMUL_S, FDIV_S}
+
+enum f_un_rm_op_S = {FSQRT_S, FCVT_W_S, FCVT_WU_S, FCVT_S_W, FCVT_S_WU,    // RV32 and RV64
+                     FCVT_L_S, FCVT_LU_S, FCVT_S_L, FCVT_S_LU}             // RV64 only
+
+enum f_un_op_S = {FCLASS_S, FMV_X_W, FMV_W_X}    /* RV32 and RV64 */
+
+enum f_bin_op_S = {FSGNJ_S, FSGNJN_S, FSGNJX_S, FMIN_S, FMAX_S, FEQ_S, FLT_S, FLE_S}
+
+enum f_madd_op_D = {FMADD_D, FMSUB_D, FNMSUB_D, FNMADD_D}
+
+enum f_bin_rm_op_D = {FADD_D, FSUB_D, FMUL_D, FDIV_D}
+
+enum f_un_rm_op_D = {FSQRT_D, FCVT_W_D, FCVT_WU_D, FCVT_D_W, FCVT_D_WU,    // RV32 and RV64
+                     FCVT_S_D, FCVT_D_S,
+                     FCVT_L_D, FCVT_LU_D, FCVT_D_L, FCVT_D_LU}             // RV64 only
+
+enum f_bin_op_D = {FSGNJ_D, FSGNJN_D, FSGNJX_D, FMIN_D, FMAX_D, FEQ_D, FLT_D, FLE_D}
+
+enum f_un_op_D = {FCLASS_D,            /* RV32 and RV64 */
+                  FMV_X_D, FMV_D_X}    /* RV64 only */
diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail
index 7eb01c5..e760b90 100644
--- a/model/riscv_insts_aext.sail
+++ b/model/riscv_insts_aext.sail
@@ -198,21 +198,30 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
             let eares : MemoryOpResult(unit) = match (width, sizeof(xlen)) {
               (WORD, _)    => mem_write_ea(addr, 4, aq & rl, rl, true),
               (DOUBLE, 64) => mem_write_ea(addr, 8, aq & rl, rl, true),
-              _            => internal_error ("AMO expected WORD or DOUBLE")
+              _            => internal_error("AMO expected WORD or DOUBLE")
+            };
+            let is_unsigned : bool = match op {
+              AMOMINU => true,
+              AMOMAXU => true,
+              _       => false
+            };
+            let rs2_val : xlenbits = match width {
+              WORD   => if is_unsigned then EXTZ(X(rs2)[31..0]) else EXTS(X(rs2)[31..0]),
+              DOUBLE => X(rs2),
+              _      => internal_error("AMO expected WORD or DOUBLE")
             };
-            rs2_val : xlenbits = X(rs2);
             match (eares) {
               MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL },
               MemValue(_) => {
-                let rval : MemoryOpResult(xlenbits) = match (width, sizeof(xlen)) {
-                  (WORD, _)    => extend_value(false, mem_read(ReadWrite(Data), addr, 4, aq, aq & rl, true)),
-                  (DOUBLE, 64) => extend_value(false, mem_read(ReadWrite(Data), addr, 8, aq, aq & rl, true)),
-                  _            => internal_error ("AMO expected WORD or DOUBLE")
+                let mval : MemoryOpResult(xlenbits) = match (width, sizeof(xlen)) {
+                  (WORD, _)    => extend_value(is_unsigned, mem_read(ReadWrite(Data), addr, 4, aq, aq & rl, true)),
+                  (DOUBLE, 64) => extend_value(is_unsigned, mem_read(ReadWrite(Data), addr, 8, aq, aq & rl, true)),
+                  _            => internal_error("AMO expected WORD or DOUBLE")
                 };
-                match (rval) {
+                match (mval) {
                   MemException(e)  => { handle_mem_exception(addr, e); RETIRE_FAIL },
                   MemValue(loaded) => {
-                    result  : xlenbits =
+                    let result : xlenbits =
                       match op {
                         AMOSWAP => rs2_val,
                         AMOADD  => rs2_val + loaded,
@@ -228,14 +237,18 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
                         AMOMINU => to_bits(sizeof(xlen), min(unsigned(rs2_val), unsigned(loaded))),
                         AMOMAXU => to_bits(sizeof(xlen), max(unsigned(rs2_val), unsigned(loaded)))
                       };
-
+                    let rval : xlenbits = match width {
+                      WORD   => EXTS(loaded[31..0]),
+                      DOUBLE => loaded,
+                      _      => internal_error("AMO expected WORD or DOUBLE")
+                    };
                     let wval : MemoryOpResult(bool) = match (width, sizeof(xlen)) {
                       (WORD, _)    => mem_write_value(addr, 4, result[31..0], aq & rl, rl, true),
                       (DOUBLE, 64) => mem_write_value(addr, 8, result,        aq & rl, rl, true),
                       _            => internal_error("AMO expected WORD or DOUBLE")
                     };
                     match (wval) {
-                      MemValue(true)  => { X(rd) = loaded; RETIRE_SUCCESS },
+                      MemValue(true)  => { X(rd) = rval; RETIRE_SUCCESS },
                       MemValue(false) => { internal_error("AMO got false from mem_write_value") },
                       MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL }
                     }
@@ -266,4 +279,4 @@ mapping amo_mnemonic : amoop <-> string = {
 }
 
 mapping clause assembly = AMO(op, aq, rl, rs2, rs1, width, rd)
-  <-> amo_mnemonic(op) ^ "." ^ size_mnemonic(width) ^ maybe_aq(aq) ^ maybe_rl(rl) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
+  <-> amo_mnemonic(op) ^ "." ^ size_mnemonic(width) ^ maybe_aq(aq) ^ maybe_rl(rl) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs2) ^ sep() ^ "(" ^ reg_name(rs1) ^ ")"
diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail
index d80d34d..bc86859 100644
--- a/model/riscv_insts_base.sail
+++ b/model/riscv_insts_base.sail
@@ -714,9 +714,11 @@ mapping clause encdec = MRET()
   <-> 0b0011000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011
 
 function clause execute MRET() = {
-  if   cur_privilege == Machine
-  then set_next_pc(exception_handler(cur_privilege, CTL_MRET(), PC))
-  else handle_illegal();
+  if   cur_privilege != Machine
+  then handle_illegal()
+  else if ~(ext_check_xret_priv (Machine))
+  then ext_fail_xret_priv ()
+  else set_next_pc(exception_handler(cur_privilege, CTL_MRET(), PC));
   RETIRE_FAIL
 }
 
@@ -729,15 +731,16 @@ mapping clause encdec = SRET()
   <-> 0b0001000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011
 
 function clause execute SRET() = {
-  match cur_privilege {
-    User       => handle_illegal(),
-    Supervisor => if   (~ (haveSupMode ())) | mstatus.TSR() == 0b1
-                  then handle_illegal()
-                  else set_next_pc(exception_handler(cur_privilege, CTL_SRET(), PC)),
-    Machine    => if   (~ (haveSupMode ()))
-                  then handle_illegal()
-                  else set_next_pc(exception_handler(cur_privilege, CTL_SRET(), PC))
+  let sret_illegal : bool = match cur_privilege {
+    User       => true,
+    Supervisor => ~ (haveSupMode ()) | mstatus.TSR() == 0b1,
+    Machine    => ~ (haveSupMode ())
   };
+  if   sret_illegal
+  then handle_illegal()
+  else if ~(ext_check_xret_priv (Supervisor))
+  then ext_fail_xret_priv ()
+  else set_next_pc(exception_handler(cur_privilege, CTL_SRET(), PC));
   RETIRE_FAIL
 }
 
diff --git a/model/riscv_insts_begin.sail b/model/riscv_insts_begin.sail
index b27711b..661a353 100644
--- a/model/riscv_insts_begin.sail
+++ b/model/riscv_insts_begin.sail
@@ -12,7 +12,7 @@ scattered function execute
 val assembly : ast <-> string
 scattered mapping assembly
 
-val encdec : ast <-> bits(32)
+val encdec : ast <-> bits(32) effect {rreg}
 scattered mapping encdec
 
 val encdec_compressed : ast <-> bits(16)
diff --git a/model/riscv_insts_dext.sail b/model/riscv_insts_dext.sail
new file mode 100644
index 0000000..9e68248
--- /dev/null
+++ b/model/riscv_insts_dext.sail
@@ -0,0 +1,922 @@
+/* **************************************************************** */
+/* This file specifies the instructions in the D extension          */
+/* (double precision floating point).                               */
+
+/* RISC-V follows IEEE 754-2008 floating point arithmetic standard. */
+
+/* Original version written by Rishiyur S. Nikhil, Sept-Oct 2019    */
+
+/* **************************************************************** */
+/* IMPORTANT!                                                       */
+/* The files 'riscv_insts_fext.sail' and 'riscv_insts_dext.sail'    */
+/* define the F and D extensions, respectively.                     */
+/* The texts follow each other very closely; please try to maintain */
+/* this correspondence as the files are maintained for bug-fixes,   */
+/* improvements, and version updates.                               */
+
+/* **************************************************************** */
+/* Note: Rounding Modes and Floating point accrued exception flags  */
+/* are defined in riscv_insts_fext.sail.                            */
+/* In RISC-V, the D extension requires the F extension, so that     */
+/* should have been processed before this one.                      */
+
+/* **************************************************************** */
+/* S and D value structure (sign, exponent, mantissa)               */
+
+/* TODO: this should be a 'mapping' */
+val      fsplit_D : bits(64) -> (bits(1), bits(11), bits(52))
+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
+function f_is_neg_inf_D   x64 = {
+  let (sign, exp, mant) = fsplit_D (x64);
+  (  (sign == 0b1)
+   & (exp  == ones())
+   & (mant == zeros()))
+}
+
+val      f_is_neg_norm_D : bits(64) -> bool
+function f_is_neg_norm_D   x64 = {
+  let (sign, exp, mant) = fsplit_D (x64);
+  (  (sign == 0b1)
+   & (exp  != zeros())
+   & (exp  != ones()))
+}
+
+val      f_is_neg_subnorm_D : bits(64) -> bool
+function f_is_neg_subnorm_D   x64 = {
+  let (sign, exp, mant) = fsplit_D (x64);
+  (  (sign == 0b1)
+   & (exp  == zeros())
+   & (mant != zeros()))
+}
+
+val      f_is_neg_zero_D : bits(64) -> bool
+function f_is_neg_zero_D   x64 = {
+  let (sign, exp, mant) = fsplit_D (x64);
+  (  (sign == ones())
+   & (exp  == zeros())
+   & (mant == zeros()))
+}
+
+val      f_is_pos_zero_D : bits(64) -> bool
+function f_is_pos_zero_D   x64 = {
+  let (sign, exp, mant) = fsplit_D (x64);
+  (  (sign == zeros())
+   & (exp  == zeros())
+   & (mant == zeros()))
+}
+
+val      f_is_pos_subnorm_D : bits(64) -> bool
+function f_is_pos_subnorm_D   x64 = {
+  let (sign, exp, mant) = fsplit_D (x64);
+  (  (sign == zeros())
+   & (exp  == zeros())
+   & (mant != zeros()))
+}
+
+val      f_is_pos_norm_D : bits(64) -> bool
+function f_is_pos_norm_D   x64 = {
+  let (sign, exp, mant) = fsplit_D (x64);
+  (  (sign == zeros())
+   & (exp  != zeros())
+   & (exp  != ones()))
+}
+
+val      f_is_pos_inf_D : bits(64) -> bool
+function f_is_pos_inf_D   x64 = {
+  let (sign, exp, mant) = fsplit_D (x64);
+  (  (sign == zeros())
+   & (exp  == ones())
+   & (mant == zeros()))
+}
+
+val      f_is_SNaN_D : bits(64) -> bool
+function f_is_SNaN_D   x64 = {
+  let (sign, exp, mant) = fsplit_D (x64);
+  (  (exp == ones())
+   & (mant [51] == bitzero)
+   & (mant != zeros()))
+}
+
+val      f_is_QNaN_D : bits(64) -> bool
+function f_is_QNaN_D   x64 = {
+  let (sign, exp, mant) = fsplit_D (x64);
+  (  (exp == ones())
+   & (mant [51] == bitone))
+}
+
+/* **************************************************************** */
+/* Help functions used in the semantic functions                    */
+
+val      negate_D : bits(64) -> bits(64)
+function negate_D (x64) = {
+  let (sign, exp, mant) = fsplit_D (x64);
+  let new_sign = if (sign == 0b0) then 0b1 else 0b0;
+  fmake_D (new_sign, exp, mant)
+}
+
+val      feq_quiet_D : (bits(64), bits (64)) -> (bool, bits(5))
+function feq_quiet_D   (v1,       v2) = {
+  let (s1, e1, m1) = fsplit_D (v1);
+  let (s2, e2, m2) = fsplit_D (v2);
+
+  let v1Is0    = f_is_neg_zero_D(v1) | f_is_pos_zero_D(v1);
+  let v2Is0    = f_is_neg_zero_D(v2) | f_is_pos_zero_D(v2);
+
+  let result = ((v1 == v2) | (v1Is0 & v2Is0));
+
+  let fflags = if (f_is_SNaN_D(v1) | f_is_SNaN_D(v2)) then
+                 nvFlag()
+               else
+                 zeros();
+
+  (result, fflags)
+}
+
+val      flt_D : (bits(64), bits (64), bool) -> (bool, bits(5))
+function flt_D   (v1,       v2,        is_quiet) = {
+  let (s1, e1, m1) = fsplit_D (v1);
+  let (s2, e2, m2) = fsplit_D (v2);
+
+  let v1IsNaN  = f_is_QNaN_D(v1) | f_is_SNaN_D(v1);
+  let v2IsNaN  = f_is_QNaN_D(v2) | f_is_SNaN_D(v2);
+
+  let result : bool =
+    if (s1 == 0b0) & (s2 == 0b0) then
+      if (e1 == e2) then
+         unsigned (m1) < unsigned (m2)
+      else
+         unsigned (e1) < unsigned (e2)
+    else if (s1 == 0b0) & (s2 == 0b1) then
+      false
+    else if (s1 == 0b1) & (s2 == 0b0) then
+      true
+    else
+      if (e1 == e2) then
+        unsigned (m1) > unsigned (m2)
+      else
+        unsigned (e1) > unsigned (e2);
+
+  let fflags = if is_quiet then
+                 if (f_is_SNaN_D(v1) | f_is_SNaN_D(v2)) then
+                   nvFlag()
+                 else
+                   zeros()
+               else
+                 if (v1IsNaN | v2IsNaN) then
+                   nvFlag()
+                 else
+                   zeros();
+
+  (result, fflags)
+}
+
+val      fle_D : (bits(64), bits (64), bool) -> (bool, bits(5))
+function fle_D   (v1,       v2,        is_quiet) = {
+  let (s1, e1, m1) = fsplit_D (v1);
+  let (s2, e2, m2) = fsplit_D (v2);
+
+  let v1IsNaN  = f_is_QNaN_D(v1) | f_is_SNaN_D(v1);
+  let v2IsNaN  = f_is_QNaN_D(v2) | f_is_SNaN_D(v2);
+
+  let v1Is0    = f_is_neg_zero_D(v1) | f_is_pos_zero_D(v1);
+  let v2Is0    = f_is_neg_zero_D(v2) | f_is_pos_zero_D(v2);
+
+  let result : bool =
+    if (s1 == 0b0) & (s2 == 0b0) then
+      if (e1 == e2) then
+        unsigned (m1) <=  unsigned (m2)
+      else
+        unsigned (e1)  <  unsigned (e2)
+    else if (s1 == 0b0) & (s2 == 0b1) then
+      (v1Is0 & v2Is0)                         /* Equal in this case (+0=-0) */
+    else if (s1 == 0b1) & (s2 == 0b0) then
+      true
+    else
+      if (e1 == e2) then
+        unsigned (m1) >=  unsigned (m2)
+      else
+        unsigned (e1)  >  unsigned (e2);
+
+  let fflags = if is_quiet then
+                 if (f_is_SNaN_D(v1) | f_is_SNaN_D(v2)) then
+                   nvFlag()
+                 else
+                   zeros()
+               else
+                 if (v1IsNaN | v2IsNaN) then
+                   nvFlag()
+                 else
+                   zeros();
+
+  (result, fflags)
+}
+
+/* ****************************************************************** */
+/* Floating-point loads                                               */
+/* These are defined in: riscv_insts_fext.sail                        */
+
+/* ****************************************************************** */
+/* Floating-point stores                                              */
+/* These are defined in: riscv_insts_fext.sail                        */
+
+/* ****************************************************************** */
+/* Fused multiply-add */
+
+/* AST */
+
+union clause ast = F_MADD_TYPE_D : (regidx, regidx, regidx, rounding_mode, regidx, f_madd_op_D)
+
+/* AST <-> Binary encoding ================================ */
+
+mapping clause encdec =
+    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 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 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 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 = F(rs1);
+  let rs2_val_64b = F(rs2);
+  let rs3_val_64b = F(rs3);
+  let rm_3b       = encdec_rounding_mode (select_instr_or_fcsr_rm  (rm));
+  let (fflags, rd_val_64b) : (bits(5), bits(64)) =
+    match op {
+      FMADD_D  => riscv_f64MulAdd (rm_3b, rs1_val_64b, rs2_val_64b, rs3_val_64b),
+      FMSUB_D  => riscv_f64MulAdd (rm_3b, rs1_val_64b, rs2_val_64b, negate_D (rs3_val_64b)),
+      FNMSUB_D => riscv_f64MulAdd (rm_3b, negate_D (rs1_val_64b), rs2_val_64b, rs3_val_64b),
+      FNMADD_D => riscv_f64MulAdd (rm_3b, negate_D (rs1_val_64b), rs2_val_64b, negate_D (rs3_val_64b))
+    };
+  write_fflags(fflags);
+  F(rd) = rd_val_64b;
+  RETIRE_SUCCESS
+}
+
+/* AST -> Assembly notation ================================ */
+
+mapping f_madd_type_mnemonic_D : f_madd_op_D <-> string = {
+    FMADD_D  <-> "fmadd.d",
+    FMSUB_D  <-> "fmsub.d",
+    FNMSUB_D <-> "fnmsub.d",
+    FNMADD_D <-> "fnmadd.d"
+}
+
+mapping clause assembly = F_MADD_TYPE_D(rs3, rs2, rs1, rm, rd, op)
+                      <-> f_madd_type_mnemonic_D(op)
+                          ^ spc() ^ freg_name(rd)
+                          ^ sep() ^ freg_name(rs1)
+                          ^ sep() ^ freg_name(rs2)
+                          ^ sep() ^ freg_name(rs3)
+                          ^ sep() ^ frm_mnemonic(rm)
+
+/* ****************************************************************** */
+/* Binary ops with rounding mode */
+
+/* AST */
+
+union clause ast = F_BIN_RM_TYPE_D : (regidx, regidx, rounding_mode, regidx, f_bin_rm_op_D)
+
+/* AST <-> Binary encoding ================================ */
+
+mapping clause encdec =
+    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 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 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 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)) = {
+  let rs1_val_64b = F(rs1);
+  let rs2_val_64b = F(rs2);
+  let rm_3b       = encdec_rounding_mode (select_instr_or_fcsr_rm  (rm));
+  let (fflags, rd_val_64b) : (bits(5), bits(64)) = match op {
+    FADD_D  => riscv_f64Add (rm_3b, rs1_val_64b, rs2_val_64b),
+    FSUB_D  => riscv_f64Sub (rm_3b, rs1_val_64b, rs2_val_64b),
+    FMUL_D  => riscv_f64Mul (rm_3b, rs1_val_64b, rs2_val_64b),
+    FDIV_D  => riscv_f64Div (rm_3b, rs1_val_64b, rs2_val_64b)
+  };
+  write_fflags(fflags);
+  F(rd) = rd_val_64b;
+  RETIRE_SUCCESS
+}
+
+/* AST -> Assembly notation ================================ */
+
+mapping f_bin_rm_type_mnemonic_D : f_bin_rm_op_D <-> string = {
+  FADD_D  <-> "fadd.d",
+  FSUB_D  <-> "fsub.d",
+  FMUL_D  <-> "fmul.d",
+  FDIV_D  <-> "fdiv.d"
+}
+
+mapping clause assembly = F_BIN_RM_TYPE_D(rs2, rs1, rm, rd, op)
+                      <-> f_bin_rm_type_mnemonic_D(op)
+                          ^ spc() ^ freg_name(rd)
+                          ^ sep() ^ freg_name(rs1)
+                          ^ sep() ^ freg_name(rs2)
+                          ^ sep() ^ frm_mnemonic(rm)
+
+/* ****************************************************************** */
+/* Unary with rounding mode */
+
+/* AST */
+
+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 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 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 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 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 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 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 is_RV32D_or_RV64D()
+<-> 0b010_0001 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if is_RV32D_or_RV64D()
+
+/* D instructions, RV64 only */
+
+mapping clause encdec =
+    F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_L_D)                                     if is_RV64D()
+<-> 0b110_0001 @ 0b00010 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if is_RV64D()
+
+mapping clause encdec =
+    F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_LU_D)                                    if is_RV64D()
+<-> 0b110_0001 @ 0b00011 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if is_RV64D()
+
+mapping clause encdec =
+    F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_L)                                     if is_RV64D()
+<-> 0b110_1001 @ 0b00010 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if is_RV64D()
+
+mapping clause encdec =
+    F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_LU)                                    if is_RV64D()
+<-> 0b110_1001 @ 0b00011 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if is_RV64D()
+
+/* Execution semantics ================================ */
+
+function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FSQRT_D)) = {
+  let rs1_val_D = F(rs1);
+  let rm_3b     = encdec_rounding_mode (select_instr_or_fcsr_rm  (rm));
+
+  let (fflags, rd_val_D) = riscv_f64Sqrt   (rm_3b, rs1_val_D);
+
+  write_fflags(fflags);
+  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 = F(rs1);
+  let rm_3b     = encdec_rounding_mode (select_instr_or_fcsr_rm  (rm));
+
+  let (fflags, rd_val_W) = riscv_f64ToI32 (rm_3b, rs1_val_D);
+
+  write_fflags(fflags);
+  X(rd) = EXTS (rd_val_W);
+  RETIRE_SUCCESS
+}
+
+function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_WU_D)) = {
+  let rs1_val_D = F(rs1);
+  let rm_3b     = encdec_rounding_mode (select_instr_or_fcsr_rm  (rm));
+
+  let (fflags, rd_val_WU) = riscv_f64ToUi32 (rm_3b, rs1_val_D);
+
+  write_fflags(fflags);
+  X(rd) = EXTS (rd_val_WU);
+  RETIRE_SUCCESS
+}
+
+function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_W)) = {
+  let rs1_val_W = X(rs1) [31..0];
+  let rm_3b     = encdec_rounding_mode (select_instr_or_fcsr_rm  (rm));
+
+  let (fflags, rd_val_D) = riscv_i32ToF64 (rm_3b, rs1_val_W);
+
+  write_fflags(fflags);
+  F(rd) = rd_val_D;
+  RETIRE_SUCCESS
+}
+
+function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_WU)) = {
+  let rs1_val_WU = X(rs1) [31..0];
+  let rm_3b      = encdec_rounding_mode (select_instr_or_fcsr_rm  (rm));
+
+  let (fflags, rd_val_D) = riscv_ui32ToF64 (rm_3b, rs1_val_WU);
+
+  write_fflags(fflags);
+  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 = F(rs1);
+  let rm_3b     = encdec_rounding_mode (select_instr_or_fcsr_rm  (rm));
+
+  let (fflags, rd_val_S) = riscv_f64ToF32 (rm_3b, rs1_val_D);
+
+  write_fflags(fflags);
+  F(rd) = nan_box (rd_val_S);
+  RETIRE_SUCCESS
+}
+
+function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_S)) = {
+  let rs1_val_S = nan_unbox (F(rs1));
+  let rm_3b     = encdec_rounding_mode (select_instr_or_fcsr_rm  (rm));
+
+  let (fflags, rd_val_D) = riscv_f32ToF64 (rm_3b, rs1_val_S);
+
+  write_fflags(fflags);
+  F(rd) = rd_val_D;
+  RETIRE_SUCCESS
+}
+
+function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_L_D)) = {
+  let rs1_val_D = F(rs1);
+  let rm_3b     = encdec_rounding_mode (select_instr_or_fcsr_rm  (rm));
+
+  let (fflags, rd_val_L) = riscv_f64ToI64 (rm_3b, rs1_val_D);
+
+  write_fflags(fflags);
+  X(rd) = rd_val_L;
+  RETIRE_SUCCESS
+}
+
+function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_LU_D)) = {
+  let rs1_val_D = F(rs1);
+  let rm_3b     = encdec_rounding_mode (select_instr_or_fcsr_rm  (rm));
+
+  let (fflags, rd_val_LU) = riscv_f64ToUi64 (rm_3b, rs1_val_D);
+
+  write_fflags(fflags);
+  X(rd) = rd_val_LU;
+  RETIRE_SUCCESS
+}
+
+function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_L)) = {
+  let rs1_val_L = X(rs1);
+  let rm_3b     = encdec_rounding_mode (select_instr_or_fcsr_rm  (rm));
+
+  let (fflags, rd_val_D) = riscv_i64ToF64 (rm_3b, rs1_val_L);
+
+  write_fflags(fflags);
+  F(rd) = rd_val_D;
+  RETIRE_SUCCESS
+}
+
+function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_LU)) = {
+  let rs1_val_LU = X(rs1);
+  let rm_3b      = encdec_rounding_mode (select_instr_or_fcsr_rm  (rm));
+
+  let (fflags, rd_val_D) = riscv_ui64ToF64 (rm_3b, rs1_val_LU);
+
+  write_fflags(fflags);
+  F(rd) = rd_val_D;
+  RETIRE_SUCCESS
+}
+
+/* AST -> Assembly notation ================================ */
+
+mapping f_un_rm_type_mnemonic_D : f_un_rm_op_D <-> string = {
+    FSQRT_D   <-> "fsqrt.d",
+    FCVT_W_D  <-> "fcvt.w.d",
+    FCVT_WU_D <-> "fcvt.wu.d",
+    FCVT_D_W  <-> "fcvt.d.w",
+    FCVT_D_WU <-> "fcvt.d.wu",
+
+    FCVT_L_D  <-> "fcvt.l.d",
+    FCVT_LU_D <-> "fcvt.lu.d",
+    FCVT_D_L  <-> "fcvt.d.l",
+    FCVT_D_LU <-> "fcvt.d.lu",
+
+    FCVT_S_D  <-> "fcvt.s.d",
+    FCVT_D_S  <-> "fcvt.d.s"
+}
+
+mapping clause assembly = F_UN_RM_TYPE_D(rs1, rm, rd, FSQRT_D)
+                      <-> f_un_rm_type_mnemonic_D(FSQRT_D)
+                          ^ 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() ^ 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() ^ 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() ^ 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() ^ 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() ^ 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() ^ 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() ^ 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() ^ 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() ^ 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() ^ freg_name(rd)
+                          ^ sep() ^ freg_name(rs1)
+                          ^ sep() ^ frm_mnemonic(rm)
+
+/* ****************************************************************** */
+/* Binary, no rounding mode */
+
+/* AST */
+
+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 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 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 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 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 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 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 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 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    = 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);
+  let fflags       = 0b_00000;
+  write_fflags(fflags);
+  F(rd) = rd_val_D;
+  RETIRE_SUCCESS
+}
+
+function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FSGNJN_D)) = {
+  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);
+  let fflags       = 0b_00000;
+  write_fflags(fflags);
+  F(rd) = rd_val_D;
+  RETIRE_SUCCESS
+}
+
+function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FSGNJX_D)) = {
+  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);
+  let fflags       = 0b_00000;
+  write_fflags(fflags);
+  F(rd) = rd_val_D;
+  RETIRE_SUCCESS
+}
+
+function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FMIN_D)) = {
+  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);
+
+  let rd_val_D  = if      (f_is_SNaN_D(rs1_val_D) & f_is_SNaN_D(rs2_val_D))         then canonical_NaN_D()
+                  else if f_is_SNaN_D(rs1_val_D)                                    then rs2_val_D
+                  else if f_is_SNaN_D(rs2_val_D)                                    then rs1_val_D
+                  else if (f_is_QNaN_D(rs1_val_D) & f_is_QNaN_D(rs2_val_D))         then canonical_NaN_D()
+                  else if f_is_QNaN_D(rs1_val_D)                                    then rs2_val_D
+                  else if f_is_QNaN_D(rs2_val_D)                                    then rs1_val_D
+                  else if (f_is_neg_zero_D(rs1_val_D) & f_is_pos_zero_D(rs2_val_D)) then rs1_val_D
+                  else if (f_is_neg_zero_D(rs2_val_D) & f_is_pos_zero_D(rs1_val_D)) then rs2_val_D
+                  else if rs1_lt_rs2                                                then rs1_val_D
+                  else /* (not rs1_lt_rs2) */                                            rs2_val_D;
+
+  write_fflags(fflags);
+  F(rd) = rd_val_D;
+  RETIRE_SUCCESS
+}
+
+function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FMAX_D)) = {
+  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);
+
+  let rd_val_D  = if      (f_is_SNaN_D(rs1_val_D) & f_is_SNaN_D(rs2_val_D))         then canonical_NaN_D()
+                  else if f_is_SNaN_D(rs1_val_D)                                    then rs2_val_D
+                  else if f_is_SNaN_D(rs2_val_D)                                    then rs1_val_D
+                  else if (f_is_QNaN_D(rs1_val_D) & f_is_QNaN_D(rs2_val_D))         then canonical_NaN_D()
+                  else if f_is_QNaN_D(rs1_val_D)                                    then rs2_val_D
+                  else if f_is_QNaN_D(rs2_val_D)                                    then rs1_val_D
+                  else if (f_is_neg_zero_D(rs1_val_D) & f_is_pos_zero_D(rs2_val_D)) then rs2_val_D
+                  else if (f_is_neg_zero_D(rs2_val_D) & f_is_pos_zero_D(rs1_val_D)) then rs1_val_D
+                  else if rs2_lt_rs1                                                then rs1_val_D
+                  else /* (not rs2_lt_rs1) */                                            rs2_val_D;
+
+  write_fflags(fflags);
+  F(rd) = rd_val_D;
+  RETIRE_SUCCESS
+}
+
+function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FEQ_D)) = {
+  let rs1_val_D = F(rs1);
+  let rs2_val_D = F(rs2);
+
+  let (rs1_eq_rs2, fflags) = feq_quiet_D (rs1_val_D, rs2_val_D);
+
+  let rd_val : xlenbits =
+      if      (f_is_SNaN_D(rs1_val_D) | f_is_SNaN_D(rs2_val_D)) then zeros()
+      else if (f_is_QNaN_D(rs1_val_D) | f_is_QNaN_D(rs2_val_D)) then zeros()
+      else if rs1_eq_rs2                                        then EXTZ(0b1)
+      else                                                           zeros();
+
+  write_fflags(fflags);
+  X(rd) = rd_val;
+  RETIRE_SUCCESS
+}
+
+function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FLT_D)) = {
+  let rs1_val_D = F(rs1);
+  let rs2_val_D = F(rs2);
+
+  let is_quiet  = false;
+  let (rs1_lt_rs2, fflags) = flt_D (rs1_val_D, rs2_val_D, is_quiet);
+
+  let rd_val : xlenbits =
+      if      (f_is_SNaN_D(rs1_val_D) | f_is_SNaN_D(rs2_val_D)) then zeros()
+      else if (f_is_QNaN_D(rs1_val_D) | f_is_QNaN_D(rs2_val_D)) then zeros()
+      else if rs1_lt_rs2                                        then EXTZ(0b1)
+      else                                                           zeros();
+
+  write_fflags(fflags);
+  X(rd) = rd_val;
+  RETIRE_SUCCESS
+}
+
+function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FLE_D)) = {
+  let rs1_val_D = F(rs1);
+  let rs2_val_D = F(rs2);
+
+  let is_quiet  = false;
+  let (rs1_le_rs2, fflags) = fle_D (rs1_val_D, rs2_val_D, is_quiet);
+
+  let rd_val : xlenbits =
+      if      (f_is_SNaN_D(rs1_val_D) | f_is_SNaN_D(rs2_val_D)) then zeros()
+      else if (f_is_QNaN_D(rs1_val_D) | f_is_QNaN_D(rs2_val_D)) then zeros()
+      else if rs1_le_rs2                                        then EXTZ(0b1)
+      else                                                           zeros();
+
+  write_fflags(fflags);
+  X(rd) = rd_val;
+  RETIRE_SUCCESS
+}
+
+/* AST -> Assembly notation ================================ */
+
+mapping f_bin_type_mnemonic_D : f_bin_op_D <-> string = {
+    FSGNJ_D  <-> "fsgnj.d",
+    FSGNJN_D <-> "fsgnjn.d",
+    FSGNJX_D <-> "fsgnjx.d",
+    FMIN_D   <-> "fmin.d",
+    FMAX_D   <-> "fmax.d",
+    FEQ_D    <-> "feq.d",
+    FLT_D    <-> "flt.d",
+    FLE_D    <-> "fle.d"
+}
+
+mapping clause assembly = F_BIN_TYPE_D(rs2, rs1, rd, FSGNJ_D)
+                      <-> f_bin_type_mnemonic_D(FSGNJ_D)
+                          ^ 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() ^ 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() ^ 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() ^ 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() ^ 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() ^ 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() ^ 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() ^ freg_name(rs1)
+                          ^ sep() ^ freg_name(rs2)
+
+/* ****************************************************************** */
+/* Unary, no rounding mode */
+
+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 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()
+                    <-> 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()
+                    <-> 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 = F(rs1);
+
+  let rd_val_10b : bits (10) =
+    if      f_is_neg_inf_D     (rs1_val_D) then 0b_00_0000_0001
+    else if f_is_neg_norm_D    (rs1_val_D) then 0b_00_0000_0010
+    else if f_is_neg_subnorm_D (rs1_val_D) then 0b_00_0000_0100
+    else if f_is_neg_zero_D    (rs1_val_D) then 0b_00_0000_1000
+    else if f_is_pos_zero_D    (rs1_val_D) then 0b_00_0001_0000
+    else if f_is_pos_subnorm_D (rs1_val_D) then 0b_00_0010_0000
+    else if f_is_pos_norm_D    (rs1_val_D) then 0b_00_0100_0000
+    else if f_is_pos_inf_D     (rs1_val_D) then 0b_00_1000_0000
+    else if f_is_SNaN_D        (rs1_val_D) then 0b_01_0000_0000
+    else if f_is_QNaN_D        (rs1_val_D) then 0b_10_0000_0000
+    else zeros();
+
+  X(rd) = EXTZ (rd_val_10b);
+  RETIRE_SUCCESS
+}
+
+function clause execute (F_UN_TYPE_D(rs1, rd, FMV_X_D)) = {
+  let rs1_val_D = F(rs1);
+  let rd_val_X  = rs1_val_D;
+  X(rd)         = rd_val_X;
+  RETIRE_SUCCESS
+}
+
+function clause execute (F_UN_TYPE_D(rs1, rd, FMV_D_X)) = {
+  let rs1_val_X = X(rs1);
+  let rd_val_D  = rs1_val_X;
+  F(rd)         = rd_val_D;
+  RETIRE_SUCCESS
+}
+
+/* AST -> Assembly notation ================================ */
+
+mapping f_un_type_mnemonic_D : f_un_op_D <-> string = {
+    FMV_X_D  <-> "fmv.x.d",
+    FCLASS_D <-> "fclass.d",
+    FMV_D_X  <-> "fmv.d.x"
+}
+
+mapping clause assembly = F_UN_TYPE_D(rs1, rd, FMV_X_D)
+                      <-> f_un_type_mnemonic_D(FMV_X_D)
+                          ^ spc() ^ reg_name(rd)
+                          ^ sep() ^ freg_name(rs1)
+
+mapping clause assembly = F_UN_TYPE_D(rs1, rd, FMV_D_X)
+                      <-> f_un_type_mnemonic_D(FMV_D_X)
+                          ^ spc() ^ freg_name(rd)
+                          ^ sep() ^ reg_name(rs1)
+
+mapping clause assembly = F_UN_TYPE_D(rs1, rd, FCLASS_D)
+                      <-> f_un_type_mnemonic_D(FCLASS_D)
+                          ^ spc() ^ reg_name(rd)
+                          ^ sep() ^ freg_name(rs1)
+
+/* ****************************************************************** */
diff --git a/model/riscv_insts_end.sail b/model/riscv_insts_end.sail
index f6223dd..6c16417 100644
--- a/model/riscv_insts_end.sail
+++ b/model/riscv_insts_end.sail
@@ -34,7 +34,7 @@ function print_insn insn = assembly(insn)
 
 overload to_str = {print_insn}
 
-val decode : bits(32) -> ast effect pure
+val decode : bits(32) -> ast effect {rreg}
 function decode bv = encdec(bv)
 
 val decodeCompressed : bits(16) -> ast effect pure
diff --git a/model/riscv_insts_fext.sail b/model/riscv_insts_fext.sail
new file mode 100644
index 0000000..4b9e69e
--- /dev/null
+++ b/model/riscv_insts_fext.sail
@@ -0,0 +1,1096 @@
+/* **************************************************************** */
+/* This file specifies the instructions in the F extension          */
+/* (single precision floating point).                               */
+
+/* RISC-V follows IEEE 754-2008 floating point arithmetic standard. */
+
+/* Original version written by Rishiyur S. Nikhil, Sept-Oct 2019    */
+
+/* **************************************************************** */
+/* IMPORTANT!                                                       */
+/* The files 'riscv_insts_fext.sail' and 'riscv_insts_dext.sail'    */
+/* define the F and D extensions, respectively.                     */
+/* The texts follow each other very closely; please try to maintain */
+/* this correspondence as the files are maintained for bug-fixes,   */
+/* improvements, and version updates.                               */
+
+/* **************************************************************** */
+
+mapping encdec_rounding_mode : rounding_mode <-> bits(3) = {
+  RM_RNE <-> 0b000,
+  RM_RTZ <-> 0b001,
+  RM_RDN <-> 0b010,
+  RM_RUP <-> 0b011,
+  RM_RMM <-> 0b100,
+  RM_DYN <-> 0b111
+}
+
+mapping frm_mnemonic : rounding_mode <-> string = {
+  RM_RNE <-> "rne",
+  RM_RTZ <-> "rtz",
+  RM_RDN <-> "rdn",
+  RM_RUP <-> "rup",
+  RM_RMM <-> "rmm",
+  RM_DYN <-> "dyn"
+}
+
+val       select_instr_or_fcsr_rm : rounding_mode -> rounding_mode effect {rreg}
+function  select_instr_or_fcsr_rm   instr_rm =
+  if   (instr_rm == RM_DYN)
+  then encdec_rounding_mode (fcsr.FRM())
+  else instr_rm
+
+/* **************************************************************** */
+/* Floating point accrued exception flags                           */
+
+function nxFlag() -> bits(5) = 0b_00001
+function ufFlag() -> bits(5) = 0b_00010
+function ofFlag() -> bits(5) = 0b_00100
+function dzFlag() -> bits(5) = 0b_01000
+function nvFlag() -> bits(5) = 0b_10000
+
+/* **************************************************************** */
+/* S and D value structure (sign, exponent, mantissa)               */
+
+/* TODO: this should be a 'mapping' */
+val      fsplit_S : bits(32) -> (bits(1), bits(8), bits(23))
+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
+function f_is_neg_inf_S   x32 = {
+  let (sign, exp, mant) = fsplit_S (x32);
+  (  (sign == 0b1)
+   & (exp  == ones())
+   & (mant == zeros()))
+}
+
+val      f_is_neg_norm_S : bits(32) -> bool
+function f_is_neg_norm_S   x32 = {
+  let (sign, exp, mant) = fsplit_S (x32);
+  (  (sign == 0b1)
+   & (exp  != zeros())
+   & (exp  != ones()))
+}
+
+val      f_is_neg_subnorm_S : bits(32) -> bool
+function f_is_neg_subnorm_S   x32 = {
+  let (sign, exp, mant) = fsplit_S (x32);
+  (  (sign == 0b1)
+   & (exp  == zeros())
+   & (mant != zeros()))
+}
+
+val      f_is_neg_zero_S : bits(32) -> bool
+function f_is_neg_zero_S   x32 = {
+  let (sign, exp, mant) = fsplit_S (x32);
+  (  (sign == ones())
+   & (exp  == zeros())
+   & (mant == zeros()))
+}
+
+val      f_is_pos_zero_S : bits(32) -> bool
+function f_is_pos_zero_S   x32 = {
+  let (sign, exp, mant) = fsplit_S (x32);
+  (  (sign == zeros())
+   & (exp  == zeros())
+   & (mant == zeros()))
+}
+
+val      f_is_pos_subnorm_S : bits(32) -> bool
+function f_is_pos_subnorm_S   x32 = {
+  let (sign, exp, mant) = fsplit_S (x32);
+  (  (sign == zeros())
+   & (exp  == zeros())
+   & (mant != zeros()))
+}
+
+val      f_is_pos_norm_S : bits(32) -> bool
+function f_is_pos_norm_S   x32 = {
+  let (sign, exp, mant) = fsplit_S (x32);
+  (  (sign == zeros())
+   & (exp  != zeros())
+   & (exp  != ones()))
+}
+
+val      f_is_pos_inf_S : bits(32) -> bool
+function f_is_pos_inf_S   x32 = {
+  let (sign, exp, mant) = fsplit_S (x32);
+  (  (sign == zeros())
+   & (exp  == ones())
+   & (mant == zeros()))
+}
+
+val      f_is_SNaN_S : bits(32) -> bool
+function f_is_SNaN_S   x32 = {
+  let (sign, exp, mant) = fsplit_S (x32);
+  (  (exp == ones())
+   & (mant [22] == bitzero)
+   & (mant != zeros()))
+}
+
+val      f_is_QNaN_S : bits(32) -> bool
+function f_is_QNaN_S   x32 = {
+  let (sign, exp, mant) = fsplit_S (x32);
+  (  (exp == ones())
+   & (mant [22] == bitone))
+}
+
+/* **************************************************************** */
+/* Help functions used in the semantic functions                    */
+
+val      negate_S : bits(32) -> bits(32)
+function negate_S (x32) = {
+  let (sign, exp, mant) = fsplit_S (x32);
+  let new_sign = if (sign == 0b0) then 0b1 else 0b0;
+  fmake_S (new_sign, exp, mant)
+}
+
+val      feq_quiet_S : (bits(32), bits (32)) -> (bool, bits(5))
+function feq_quiet_S   (v1,       v2) = {
+  let (s1, e1, m1) = fsplit_S (v1);
+  let (s2, e2, m2) = fsplit_S (v2);
+
+  let v1Is0    = f_is_neg_zero_S(v1) | f_is_pos_zero_S(v1);
+  let v2Is0    = f_is_neg_zero_S(v2) | f_is_pos_zero_S(v2);
+
+  let result = ((v1 == v2) | (v1Is0 & v2Is0));
+
+  let fflags = if (f_is_SNaN_S(v1) | f_is_SNaN_S(v2)) then
+                 nvFlag()
+               else
+                 zeros();
+
+  (result, fflags)
+}
+
+val      flt_S : (bits(32), bits (32), bool) -> (bool, bits(5))
+function flt_S   (v1,       v2,        is_quiet) = {
+  let (s1, e1, m1) = fsplit_S (v1);
+  let (s2, e2, m2) = fsplit_S (v2);
+
+  let v1IsNaN  = f_is_QNaN_S(v1) | f_is_SNaN_S(v1);
+  let v2IsNaN  = f_is_QNaN_S(v2) | f_is_SNaN_S(v2);
+
+  let result : bool =
+    if (s1 == 0b0) & (s2 == 0b0) then
+      if (e1 == e2) then
+        unsigned (m1) < unsigned (m2)
+      else
+        unsigned (e1) < unsigned (e2)
+    else if (s1 == 0b0) & (s2 == 0b1) then
+        false
+    else if (s1 == 0b1) & (s2 == 0b0) then
+        true
+    else
+        if (e1 == e2) then
+          unsigned (m1) > unsigned (m2)
+        else
+          unsigned (e1) > unsigned (e2);
+
+  let fflags = if is_quiet then
+                 if (f_is_SNaN_S(v1) | f_is_SNaN_S(v2)) then
+                   nvFlag()
+                 else
+                   zeros()
+               else
+                 if (v1IsNaN | v2IsNaN) then
+                   nvFlag()
+                 else
+                   zeros();
+
+  (result, fflags)
+}
+
+val      fle_S : (bits(32), bits (32), bool) -> (bool, bits(5))
+function fle_S   (v1,       v2,        is_quiet) = {
+  let (s1, e1, m1) = fsplit_S (v1);
+  let (s2, e2, m2) = fsplit_S (v2);
+
+  let v1IsNaN  = f_is_QNaN_S(v1) | f_is_SNaN_S(v1);
+  let v2IsNaN  = f_is_QNaN_S(v2) | f_is_SNaN_S(v2);
+
+  let v1Is0    = f_is_neg_zero_S(v1) | f_is_pos_zero_S(v1);
+  let v2Is0    = f_is_neg_zero_S(v2) | f_is_pos_zero_S(v2);
+
+  let result : bool =
+    if (s1 == 0b0) & (s2 == 0b0) then
+      if (e1 == e2) then
+        unsigned (m1) <=  unsigned (m2)
+      else
+        unsigned (e1)  <  unsigned (e2)
+    else if (s1 == 0b0) & (s2 == 0b1) then
+      (v1Is0 & v2Is0)                         /* Equal in this case (+0=-0) */
+    else if (s1 == 0b1) & (s2 == 0b0) then
+      true
+    else
+      if (e1 == e2) then
+        unsigned (m1) >=  unsigned (m2)
+      else
+        unsigned (e1)  >  unsigned (e2);
+
+  let fflags = if is_quiet then
+                 if (f_is_SNaN_S(v1) | f_is_SNaN_S(v2)) then
+                   nvFlag()
+                 else
+                   zeros()
+               else
+                 if (v1IsNaN | v2IsNaN) then
+                   nvFlag()
+                 else
+                   zeros();
+
+  (result, fflags)
+}
+
+/* **************************************************************** */
+/* 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}                              */
+
+function is_RV32F_or_RV64F () -> bool = (haveFExt() & (sizeof(xlen) == 32 | sizeof(xlen) == 64))
+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)
+
+/* ****************************************************************** */
+/* Floating-point loads                                               */
+
+/* AST */
+/* FLW and FLD; W/D is encoded in 'word_width' */
+
+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()
+                    <-> 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()
+                    <-> imm @ rs1 @ 0b011 @ rd @ 0b000_0111  if is_RV32D_or_RV64D()
+
+/* Execution semantics ================================ */
+
+val process_fload64 : (regidx, xlenbits, MemoryOpResult(bits(64)))
+                      -> Retired effect {escape, rreg, wreg}
+function process_fload64(rd, addr, value) =
+  if   sizeof(flen) == 64
+  then match value {
+         MemValue(result) => { F(rd) = result; RETIRE_SUCCESS },
+         MemException(e)  => { handle_mem_exception(addr, e); RETIRE_FAIL }
+       }
+  else {
+    /* should not get here */
+    RETIRE_FAIL
+  }
+
+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(result); RETIRE_SUCCESS },
+    MemException(e)  => { handle_mem_exception(addr, e); RETIRE_FAIL }
+  }
+
+
+function clause execute(LOAD_FP(imm, rs1, rd, width)) = {
+  let offset : xlenbits = EXTS(imm);
+  /* Get the address, X(rs1) + offset.
+     Some extensions perform additional checks on address validity. */
+  match ext_data_get_addr(rs1, offset, Read(Data), width) {
+    Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); RETIRE_FAIL },
+    Ext_DataAddr_OK(vaddr) =>
+      if   check_misaligned(vaddr, width)
+      then { handle_mem_exception(vaddr, E_Load_Addr_Align()); RETIRE_FAIL }
+      else match translateAddr(vaddr, Read(Data)) {
+        TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
+        TR_Address(addr, _) => {
+          let (aq, rl, res) = (false, false, false);
+          match (width, sizeof(xlen)) {
+            (BYTE, _)   => { handle_illegal(); RETIRE_FAIL },
+            (HALF, _)   => { handle_illegal(); RETIRE_FAIL },
+            (WORD, _)   =>
+               process_fload32(rd, vaddr, mem_read(Read(Data), addr, 4, aq, rl, res)),
+            (DOUBLE, 64) =>
+               process_fload64(rd, vaddr, mem_read(Read(Data), addr, 8, aq, rl, res))
+          }
+        }
+      }
+  }
+}
+
+/* AST -> Assembly notation ================================ */
+
+mapping clause assembly = LOAD_FP(imm, rs1, rd, width)
+                      <-> "fl" ^ size_mnemonic(width)
+                          ^ spc() ^ freg_name(rd)
+                          ^ sep() ^ hex_bits_12(imm)
+                          ^ opt_spc() ^ "(" ^ opt_spc() ^ reg_name(rs1) ^ opt_spc() ^ ")"
+
+/* ****************************************************************** */
+/* Floating-point stores                                              */
+
+/* AST */
+/* FLW and FLD; W/D is encoded in 'width' */
+
+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()
+                    <-> 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()
+                    <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b011 @ imm5 : bits(5) @ 0b010_0111  if is_RV32D_or_RV64D()
+
+/* Execution semantics ================================ */
+
+val process_fstore : (xlenbits, MemoryOpResult(bool)) -> Retired effect {escape, rreg, wreg}
+function process_fstore(vaddr, value) =
+  match value {
+    MemValue(true)  => { RETIRE_SUCCESS },
+    MemValue(false) => { internal_error("store got false from mem_write_value") },
+    MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }
+  }
+
+function clause execute (STORE_FP(imm, rs2, rs1, width)) = {
+  let offset : xlenbits = EXTS(imm);
+  let (aq, rl, con) = (false, false, false);
+  /* Get the address, X(rs1) + offset.
+     Some extensions perform additional checks on address validity. */
+  match ext_data_get_addr(rs1, offset, Write(Data), width) {
+    Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); RETIRE_FAIL },
+    Ext_DataAddr_OK(vaddr) =>
+      if   check_misaligned(vaddr, width)
+      then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); RETIRE_FAIL }
+      else match translateAddr(vaddr, Write(Data)) {
+        TR_Failure(e, _)    => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
+        TR_Address(addr, _) => {
+          let eares : MemoryOpResult(unit) = match width {
+            BYTE   => MemValue () /* bogus placeholder for illegal size */,
+            HALF   => MemValue () /* bogus placeholder for illegal size */,
+            WORD   => mem_write_ea(addr, 4, aq, rl, false),
+            DOUBLE => mem_write_ea(addr, 8, aq, rl, false)
+          };
+          match (eares) {
+            MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL },
+            MemValue(_) => {
+              let rs2_val = F(rs2);
+              match (width, sizeof(xlen)) {
+                (BYTE, _)    => { handle_illegal(); RETIRE_FAIL },
+                (HALF, _)    => { handle_illegal(); RETIRE_FAIL },
+                (WORD, _)    => process_fstore (vaddr, mem_write_value(addr, 4, rs2_val[31..0], aq, rl, con)),
+                (DOUBLE, 64) => process_fstore (vaddr, mem_write_value(addr, 8, rs2_val,        aq, rl, con))
+              };
+            }
+          }
+        }
+      }
+  }
+}
+
+/* AST -> Assembly notation ================================ */
+
+mapping clause assembly = STORE_FP(imm, rs2, rs1, width)
+                      <-> "fs" ^ size_mnemonic(width)
+                          ^ spc() ^ freg_name(rs2)
+                          ^ sep() ^ hex_bits_12(imm)
+                          ^ opt_spc() ^ "(" ^ opt_spc() ^ reg_name(rs1) ^ opt_spc() ^ ")"
+
+/* ****************************************************************** */
+/* Fused multiply-add */
+
+/* AST */
+
+union clause ast = F_MADD_TYPE_S : (regidx, regidx, regidx, rounding_mode, regidx, f_madd_op_S)
+
+/* AST <-> Binary encoding ================================ */
+
+mapping clause encdec =
+    F_MADD_TYPE_S(rs3, rs2, rs1, rm, rd, FMADD_S)                         if is_RV32F_or_RV64F()
+<-> rs3 @ 0b00 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_0011  if is_RV32F_or_RV64F()
+
+mapping clause encdec =
+    F_MADD_TYPE_S(rs3, rs2, rs1, rm, rd, FMSUB_S)                         if is_RV32F_or_RV64F()
+<-> rs3 @ 0b00 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_0111  if is_RV32F_or_RV64F()
+
+mapping clause encdec =
+    F_MADD_TYPE_S(rs3, rs2, rs1, rm, rd, FNMSUB_S)                        if is_RV32F_or_RV64F()
+<-> rs3 @ 0b00 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_1011  if is_RV32F_or_RV64F()
+
+mapping clause encdec =
+    F_MADD_TYPE_S(rs3, rs2, rs1, rm, rd, FNMADD_S)                        if is_RV32F_or_RV64F()
+<-> rs3 @ 0b00 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_1111  if is_RV32F_or_RV64F()
+
+/* Execution semantics ================================ */
+
+function clause execute (F_MADD_TYPE_S(rs3, rs2, rs1, rm, rd, op)) = {
+  let rs1_val_32b = nan_unbox (F(rs1));
+  let rs2_val_32b = nan_unbox (F(rs2));
+  let rs3_val_32b = nan_unbox (F(rs3));
+  let rm_3b       = encdec_rounding_mode (select_instr_or_fcsr_rm  (rm));
+  let (fflags, rd_val_32b) : (bits(5), bits(32)) =
+    match op {
+      FMADD_S  => riscv_f32MulAdd (rm_3b, rs1_val_32b, rs2_val_32b, rs3_val_32b),
+      FMSUB_S  => riscv_f32MulAdd (rm_3b, rs1_val_32b, rs2_val_32b, negate_S (rs3_val_32b)),
+      FNMSUB_S => riscv_f32MulAdd (rm_3b, negate_S (rs1_val_32b), rs2_val_32b, rs3_val_32b),
+      FNMADD_S => riscv_f32MulAdd (rm_3b, negate_S (rs1_val_32b), rs2_val_32b, negate_S (rs3_val_32b))
+    };
+  write_fflags(fflags);
+  F(rd) = nan_box (rd_val_32b);
+  RETIRE_SUCCESS
+}
+
+/* AST -> Assembly notation ================================ */
+
+mapping f_madd_type_mnemonic_S : f_madd_op_S <-> string = {
+    FMADD_S  <-> "fmadd.s",
+    FMSUB_S  <-> "fmsub.s",
+    FNMSUB_S <-> "fnmsub.s",
+    FNMADD_S <-> "fnmadd.s"
+}
+
+mapping clause assembly = F_MADD_TYPE_S(rs3, rs2, rs1, rm, rd, op)
+                      <-> f_madd_type_mnemonic_S(op)
+                          ^ spc() ^ freg_name(rd)
+                          ^ sep() ^ freg_name(rs1)
+                          ^ sep() ^ freg_name(rs2)
+                          ^ sep() ^ freg_name(rs3)
+                          ^ sep() ^ frm_mnemonic(rm)
+
+/* ****************************************************************** */
+/* Binary ops with rounding mode */
+
+/* AST */
+
+union clause ast = F_BIN_RM_TYPE_S : (regidx, regidx, rounding_mode, regidx, f_bin_rm_op_S)
+
+/* AST <-> Binary encoding ================================ */
+
+mapping clause encdec =
+    F_BIN_RM_TYPE_S(rs2, rs1, rm, rd, FADD_S)                             if is_RV32F_or_RV64F()
+<-> 0b000_0000 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if is_RV32F_or_RV64F()
+
+mapping clause encdec =
+    F_BIN_RM_TYPE_S(rs2, rs1, rm, rd, FSUB_S)                             if is_RV32F_or_RV64F()
+<-> 0b000_0100 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if is_RV32F_or_RV64F()
+
+mapping clause encdec =
+    F_BIN_RM_TYPE_S(rs2, rs1, rm, rd, FMUL_S)                             if is_RV32F_or_RV64F()
+<-> 0b000_1000 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if is_RV32F_or_RV64F()
+
+mapping clause encdec =
+    F_BIN_RM_TYPE_S(rs2, rs1, rm, rd, FDIV_S)                             if is_RV32F_or_RV64F()
+<-> 0b000_1100 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if is_RV32F_or_RV64F()
+
+/* Execution semantics ================================ */
+
+function clause execute (F_BIN_RM_TYPE_S(rs2, rs1, rm, rd, op)) = {
+  let rs1_val_32b = nan_unbox (F(rs1));
+  let rs2_val_32b = nan_unbox (F(rs2));
+  let rm_3b       = encdec_rounding_mode (select_instr_or_fcsr_rm  (rm));
+  let (fflags, rd_val_32b) : (bits(5), bits(32)) = match op {
+    FADD_S  => riscv_f32Add (rm_3b, rs1_val_32b, rs2_val_32b),
+    FSUB_S  => riscv_f32Sub (rm_3b, rs1_val_32b, rs2_val_32b),
+    FMUL_S  => riscv_f32Mul (rm_3b, rs1_val_32b, rs2_val_32b),
+    FDIV_S  => riscv_f32Div (rm_3b, rs1_val_32b, rs2_val_32b)
+  };
+  write_fflags(fflags);
+  F(rd) = nan_box (rd_val_32b);
+  RETIRE_SUCCESS
+}
+
+/* AST -> Assembly notation ================================ */
+
+mapping f_bin_rm_type_mnemonic_S : f_bin_rm_op_S <-> string = {
+  FADD_S  <-> "fadd.s",
+  FSUB_S  <-> "fsub.s",
+  FMUL_S  <-> "fmul.s",
+  FDIV_S  <-> "fdiv.s"
+}
+
+mapping clause assembly = F_BIN_RM_TYPE_S(rs2, rs1, rm, rd, op)
+                      <-> f_bin_rm_type_mnemonic_S(op)
+                          ^ spc() ^ freg_name(rd)
+                          ^ sep() ^ freg_name(rs1)
+                          ^ sep() ^ freg_name(rs2)
+                          ^ sep() ^ frm_mnemonic(rm)
+
+/* ****************************************************************** */
+/* Unary with rounding mode */
+
+/* AST */
+
+union clause ast = F_UN_RM_TYPE_S : (regidx, rounding_mode, regidx, f_un_rm_op_S)
+
+/* AST <-> Binary encoding ================================ */
+
+mapping clause encdec =
+    F_UN_RM_TYPE_S(rs1, rm, rd, FSQRT_S)                                      if is_RV32F_or_RV64F()
+<-> 0b010_1100 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if is_RV32F_or_RV64F()
+
+mapping clause encdec =
+    F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_W_S)                                     if is_RV32F_or_RV64F()
+<-> 0b110_0000 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if is_RV32F_or_RV64F()
+
+mapping clause encdec =
+    F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_WU_S)                                    if is_RV32F_or_RV64F()
+<-> 0b110_0000 @ 0b00001 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if is_RV32F_or_RV64F()
+
+mapping clause encdec =
+    F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_W)                                     if is_RV32F_or_RV64F()
+<-> 0b110_1000 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if is_RV32F_or_RV64F()
+
+mapping clause encdec =
+    F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_WU)                                    if is_RV32F_or_RV64F()
+<-> 0b110_1000 @ 0b00001 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if is_RV32F_or_RV64F()
+
+/* F instructions, RV64 only */
+
+mapping clause encdec =
+    F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_L_S)                                     if is_RV64F()
+<-> 0b110_0000 @ 0b00010 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if is_RV64F()
+
+mapping clause encdec =
+    F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_LU_S)                                    if is_RV64F()
+<-> 0b110_0000 @ 0b00011 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if is_RV64F()
+
+mapping clause encdec =
+    F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_L)                                     if is_RV64F()
+<-> 0b110_1000 @ 0b00010 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if is_RV64F()
+
+mapping clause encdec =
+    F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_LU)                                    if is_RV64F()
+<-> 0b110_1000 @ 0b00011 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011  if is_RV64F()
+
+/* Execution semantics ================================ */
+
+function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FSQRT_S)) = {
+  let rs1_val_S = nan_unbox (F(rs1));
+  let rm_3b     = encdec_rounding_mode (select_instr_or_fcsr_rm  (rm));
+
+  let (fflags, rd_val_S) = riscv_f32Sqrt   (rm_3b, rs1_val_S);
+
+  write_fflags(fflags);
+  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 = nan_unbox (F(rs1));
+  let rm_3b     = encdec_rounding_mode (select_instr_or_fcsr_rm  (rm));
+
+  let (fflags, rd_val_W) = riscv_f32ToI32 (rm_3b, rs1_val_S);
+
+  write_fflags(fflags);
+  X(rd) = EXTS (rd_val_W);
+  RETIRE_SUCCESS
+}
+
+function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_WU_S)) = {
+  let rs1_val_S = nan_unbox (F(rs1));
+  let rm_3b     = encdec_rounding_mode (select_instr_or_fcsr_rm  (rm));
+
+  let (fflags, rd_val_WU) = riscv_f32ToUi32 (rm_3b, rs1_val_S);
+
+  write_fflags(fflags);
+  X(rd) = EXTS (rd_val_WU);
+  RETIRE_SUCCESS
+}
+
+function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_W)) = {
+  let rs1_val_W = X(rs1) [31..0];
+  let rm_3b     = encdec_rounding_mode (select_instr_or_fcsr_rm  (rm));
+
+  let (fflags, rd_val_S) = riscv_i32ToF32 (rm_3b, rs1_val_W);
+
+  write_fflags(fflags);
+  F(rd) = nan_box (rd_val_S);
+  RETIRE_SUCCESS
+}
+
+function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_WU)) = {
+  let rs1_val_WU = X(rs1) [31..0];
+  let rm_3b      = encdec_rounding_mode (select_instr_or_fcsr_rm  (rm));
+
+  let (fflags, rd_val_S) = riscv_ui32ToF32 (rm_3b, rs1_val_WU);
+
+  write_fflags(fflags);
+  F(rd) = nan_box (rd_val_S);
+  RETIRE_SUCCESS
+}
+
+function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_L_S)) = {
+  if   sizeof(flen) == 64
+  then {
+    let rs1_val_S = nan_unbox (F(rs1));
+    let rm_3b     = encdec_rounding_mode (select_instr_or_fcsr_rm  (rm));
+
+    let (fflags, rd_val_L) = riscv_f32ToI64 (rm_3b, rs1_val_S);
+
+    write_fflags(fflags);
+    X(rd) = rd_val_L;
+    RETIRE_SUCCESS
+  } else {
+    /* this would not decode on RV32 */
+    RETIRE_FAIL
+  }
+}
+
+function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_LU_S)) = {
+  if   sizeof(flen) == 64
+  then {
+    let rs1_val_S = nan_unbox (F(rs1));
+    let rm_3b     = encdec_rounding_mode (select_instr_or_fcsr_rm  (rm));
+
+    let (fflags, rd_val_LU) = riscv_f32ToUi64 (rm_3b, rs1_val_S);
+
+    write_fflags(fflags);
+    X(rd) = rd_val_LU;
+    RETIRE_SUCCESS
+  } else {
+    /* this would not decode on RV32 */
+    RETIRE_FAIL
+  }
+}
+
+function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_L)) = {
+  if   sizeof(flen) == 64
+  then {
+    let rs1_val_L = X(rs1);
+    let rm_3b     = encdec_rounding_mode (select_instr_or_fcsr_rm  (rm));
+
+    let (fflags, rd_val_S) = riscv_i64ToF32 (rm_3b, rs1_val_L);
+
+    write_fflags(fflags);
+    F(rd) = nan_box (rd_val_S);
+    RETIRE_SUCCESS
+  } else {
+    /* this would not decode on RV32 */
+    RETIRE_FAIL
+  }
+}
+
+function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_LU)) = {
+  if   sizeof(flen) == 64
+  then {
+    let rs1_val_LU = X(rs1);
+    let rm_3b      = encdec_rounding_mode (select_instr_or_fcsr_rm  (rm));
+
+    let (fflags, rd_val_S) = riscv_ui64ToF32 (rm_3b, rs1_val_LU);
+
+    write_fflags(fflags);
+    F(rd) = nan_box (rd_val_S);
+    RETIRE_SUCCESS
+  } else {
+    /* this would not decode on RV32 */
+    RETIRE_FAIL
+  }
+}
+
+/* AST -> Assembly notation ================================ */
+
+mapping f_un_rm_type_mnemonic_S : f_un_rm_op_S <-> string = {
+    FSQRT_S   <-> "fsqrt.s",
+    FCVT_W_S  <-> "fcvt.w.s",
+    FCVT_WU_S <-> "fcvt.wu.s",
+    FCVT_S_W  <-> "fcvt.s.w",
+    FCVT_S_WU <-> "fcvt.s.wu",
+
+    FCVT_L_S  <-> "fcvt.l.s",
+    FCVT_LU_S <-> "fcvt.lu.s",
+    FCVT_S_L  <-> "fcvt.s.l",
+    FCVT_S_LU <-> "fcvt.s.lu"
+}
+
+mapping clause assembly = F_UN_RM_TYPE_S(rs1, rm, rd, FSQRT_S)
+                      <-> f_un_rm_type_mnemonic_S(FSQRT_S)
+                          ^ 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() ^ 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() ^ 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() ^ 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() ^ 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() ^ 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() ^ 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() ^ 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() ^ freg_name(rd)
+                          ^ sep() ^ reg_name(rs1)
+                          ^ sep() ^ frm_mnemonic(rm)
+
+
+/* ****************************************************************** */
+/* Binary, no rounding mode */
+
+/* AST */
+
+union clause ast = F_BIN_TYPE_S : (regidx, regidx, regidx, f_bin_op_S)
+
+/* AST <-> Binary encoding ================================ */
+
+mapping clause encdec = F_BIN_TYPE_S(rs2, rs1, rd, FSGNJ_S)               if is_RV32F_or_RV64F()
+                    <-> 0b001_0000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011  if is_RV32F_or_RV64F()
+
+mapping clause encdec = F_BIN_TYPE_S(rs2, rs1, rd, FSGNJN_S)              if is_RV32F_or_RV64F()
+                    <-> 0b001_0000 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011  if is_RV32F_or_RV64F()
+
+mapping clause encdec = F_BIN_TYPE_S(rs2, rs1, rd, FSGNJX_S)              if is_RV32F_or_RV64F()
+                    <-> 0b001_0000 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011  if is_RV32F_or_RV64F()
+
+mapping clause encdec = F_BIN_TYPE_S(rs2, rs1, rd, FMIN_S)                if is_RV32F_or_RV64F()
+                    <-> 0b001_0100 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011  if is_RV32F_or_RV64F()
+
+mapping clause encdec = F_BIN_TYPE_S(rs2, rs1, rd, FMAX_S)                if is_RV32F_or_RV64F()
+                    <-> 0b001_0100 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011  if is_RV32F_or_RV64F()
+
+mapping clause encdec = F_BIN_TYPE_S(rs2, rs1, rd, FEQ_S)                 if is_RV32F_or_RV64F()
+                    <-> 0b101_0000 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011  if is_RV32F_or_RV64F()
+
+mapping clause encdec = F_BIN_TYPE_S(rs2, rs1, rd, FLT_S)                 if is_RV32F_or_RV64F()
+                    <-> 0b101_0000 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011  if is_RV32F_or_RV64F()
+
+mapping clause encdec = F_BIN_TYPE_S(rs2, rs1, rd, FLE_S)                 if is_RV32F_or_RV64F()
+                    <-> 0b101_0000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011  if is_RV32F_or_RV64F()
+
+/* Execution semantics ================================ */
+
+function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FSGNJ_S)) = {
+  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);
+  let fflags       = 0b_00000;
+  write_fflags(fflags);
+  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    = 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);
+  let fflags       = 0b_00000;
+  write_fflags(fflags);
+  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    = 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);
+  let fflags       = 0b_00000;
+  write_fflags(fflags);
+  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 = 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);
+
+  let rd_val_S  = if      (f_is_SNaN_S(rs1_val_S) & f_is_SNaN_S(rs2_val_S))         then canonical_NaN_S()
+                  else if f_is_SNaN_S(rs1_val_S)                                    then rs2_val_S
+                  else if f_is_SNaN_S(rs2_val_S)                                    then rs1_val_S
+                  else if (f_is_QNaN_S(rs1_val_S) & f_is_QNaN_S(rs2_val_S))         then canonical_NaN_S()
+                  else if f_is_QNaN_S(rs1_val_S)                                    then rs2_val_S
+                  else if f_is_QNaN_S(rs2_val_S)                                    then rs1_val_S
+                  else if (f_is_neg_zero_S(rs1_val_S) & f_is_pos_zero_S(rs2_val_S)) then rs1_val_S
+                  else if (f_is_neg_zero_S(rs2_val_S) & f_is_pos_zero_S(rs1_val_S)) then rs2_val_S
+                  else if rs1_lt_rs2                                                then rs1_val_S
+                  else /* (not rs1_lt_rs2) */                                            rs2_val_S;
+
+  write_fflags(fflags);
+  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 = 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);
+
+  let rd_val_S  = if      (f_is_SNaN_S(rs1_val_S) & f_is_SNaN_S(rs2_val_S))         then canonical_NaN_S()
+                  else if f_is_SNaN_S(rs1_val_S)                                    then rs2_val_S
+                  else if f_is_SNaN_S(rs2_val_S)                                    then rs1_val_S
+                  else if (f_is_QNaN_S(rs1_val_S) & f_is_QNaN_S(rs2_val_S))         then canonical_NaN_S()
+                  else if f_is_QNaN_S(rs1_val_S)                                    then rs2_val_S
+                  else if f_is_QNaN_S(rs2_val_S)                                    then rs1_val_S
+                  else if (f_is_neg_zero_S(rs1_val_S) & f_is_pos_zero_S(rs2_val_S)) then rs2_val_S
+                  else if (f_is_neg_zero_S(rs2_val_S) & f_is_pos_zero_S(rs1_val_S)) then rs1_val_S
+                  else if rs2_lt_rs1                                                then rs1_val_S
+                  else /* (not rs2_lt_rs1) */                                            rs2_val_S;
+
+  write_fflags(fflags);
+  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 = nan_unbox (F(rs1));
+  let rs2_val_S = nan_unbox (F(rs2));
+
+  let (rs1_eq_rs2, fflags) = feq_quiet_S (rs1_val_S, rs2_val_S);
+
+  let rd_val : xlenbits =
+      if      (f_is_SNaN_S(rs1_val_S) | f_is_SNaN_S(rs2_val_S)) then zeros()
+      else if (f_is_QNaN_S(rs1_val_S) | f_is_QNaN_S(rs2_val_S)) then zeros()
+      else if rs1_eq_rs2                                        then EXTZ(0b1)
+      else                                                           zeros();
+
+  write_fflags(fflags);
+  X(rd) = rd_val;
+  RETIRE_SUCCESS
+}
+
+function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FLT_S)) = {
+  let rs1_val_S = nan_unbox (F(rs1));
+  let rs2_val_S = nan_unbox (F(rs2));
+
+  let is_quiet  = false;
+  let (rs1_lt_rs2, fflags) = flt_S (rs1_val_S, rs2_val_S, is_quiet);
+
+  let rd_val : xlenbits =
+      if      (f_is_SNaN_S(rs1_val_S) | f_is_SNaN_S(rs2_val_S)) then zeros()
+      else if (f_is_QNaN_S(rs1_val_S) | f_is_QNaN_S(rs2_val_S)) then zeros()
+      else if rs1_lt_rs2                                        then EXTZ(0b1)
+      else                                                           zeros();
+
+  write_fflags(fflags);
+  X(rd) = rd_val;
+  RETIRE_SUCCESS
+}
+
+function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FLE_S)) = {
+  let rs1_val_S = nan_unbox (F(rs1));
+  let rs2_val_S = nan_unbox (F(rs2));
+
+  let is_quiet  = false;
+  let (rs1_le_rs2, fflags) = fle_S (rs1_val_S, rs2_val_S, is_quiet);
+
+  let rd_val : xlenbits =
+      if      (f_is_SNaN_S(rs1_val_S) | f_is_SNaN_S(rs2_val_S)) then zeros()
+      else if (f_is_QNaN_S(rs1_val_S) | f_is_QNaN_S(rs2_val_S)) then zeros()
+      else if rs1_le_rs2                                        then EXTZ(0b1)
+      else                                                           zeros();
+
+  write_fflags(fflags);
+  X(rd) = rd_val;
+  RETIRE_SUCCESS
+}
+
+/* AST -> Assembly notation ================================ */
+
+mapping f_bin_type_mnemonic_S : f_bin_op_S <-> string = {
+    FSGNJ_S  <-> "fsgnj.s",
+    FSGNJN_S <-> "fsgnjn.s",
+    FSGNJX_S <-> "fsgnjx.s",
+    FMIN_S   <-> "fmin.s",
+    FMAX_S   <-> "fmax.s",
+    FEQ_S    <-> "feq.s",
+    FLT_S    <-> "flt.s",
+    FLE_S    <-> "fle.s"
+}
+
+mapping clause assembly = F_BIN_TYPE_S(rs2, rs1, rd, FSGNJ_S)
+                      <-> f_bin_type_mnemonic_S(FSGNJ_S)
+                          ^ 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() ^ 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() ^ 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() ^ 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() ^ 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() ^ 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() ^ 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() ^ freg_name(rs1)
+                          ^ sep() ^ freg_name(rs2)
+
+/* ****************************************************************** */
+/* Unary, no rounding mode */
+
+union clause ast = F_UN_TYPE_S : (regidx, regidx, f_un_op_S)
+
+/* AST <-> Binary encoding ================================ */
+
+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()
+                    <-> 0b111_0000 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011  if haveFExt()
+
+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 = nan_unbox (F(rs1));
+
+  let rd_val_10b : bits (10) =
+    if      f_is_neg_inf_S     (rs1_val_S) then 0b_00_0000_0001
+    else if f_is_neg_norm_S    (rs1_val_S) then 0b_00_0000_0010
+    else if f_is_neg_subnorm_S (rs1_val_S) then 0b_00_0000_0100
+    else if f_is_neg_zero_S    (rs1_val_S) then 0b_00_0000_1000
+    else if f_is_pos_zero_S    (rs1_val_S) then 0b_00_0001_0000
+    else if f_is_pos_subnorm_S (rs1_val_S) then 0b_00_0010_0000
+    else if f_is_pos_norm_S    (rs1_val_S) then 0b_00_0100_0000
+    else if f_is_pos_inf_S     (rs1_val_S) then 0b_00_1000_0000
+    else if f_is_SNaN_S        (rs1_val_S) then 0b_01_0000_0000
+    else if f_is_QNaN_S        (rs1_val_S) then 0b_10_0000_0000
+    else zeros();
+
+  X(rd) = EXTZ (rd_val_10b);
+  RETIRE_SUCCESS
+}
+
+function clause execute (F_UN_TYPE_S(rs1, rd, FMV_X_W)) = {
+  let rs1_val_S            = F(rs1)[31..0];
+  let rd_val_X  : xlenbits = EXTS(rs1_val_S);
+  X(rd) = rd_val_X;
+  RETIRE_SUCCESS
+}
+
+function clause execute (F_UN_TYPE_S(rs1, rd, FMV_W_X)) = {
+  let rs1_val_X            = X(rs1);
+  let rd_val_S             = rs1_val_X [31..0];
+  F(rd) = nan_box (rd_val_S);
+  RETIRE_SUCCESS
+}
+
+/* AST -> Assembly notation ================================ */
+
+mapping f_un_type_mnemonic_S : f_un_op_S <-> string = {
+    FMV_X_W  <-> "fmv.x.w",
+    FCLASS_S <-> "fclass.s",
+    FMV_W_X  <-> "fmv.w.x"
+}
+
+mapping clause assembly = F_UN_TYPE_S(rs1, rd, FMV_X_W)
+                      <-> f_un_type_mnemonic_S(FMV_X_W)
+                          ^ spc() ^ reg_name(rd)
+                          ^ sep() ^ freg_name(rs1)
+
+mapping clause assembly = F_UN_TYPE_S(rs1, rd, FMV_W_X)
+                      <-> f_un_type_mnemonic_S(FMV_W_X)
+                          ^ spc() ^ freg_name(rd)
+                          ^ sep() ^ reg_name(rs1)
+
+mapping clause assembly = F_UN_TYPE_S(rs1, rd, FCLASS_S)
+                      <-> f_un_type_mnemonic_S(FCLASS_S)
+                          ^ spc() ^ reg_name(rd)
+                          ^ sep() ^ freg_name(rs1)
+
+/* ****************************************************************** */
diff --git a/model/riscv_insts_next.sail b/model/riscv_insts_next.sail
index 2af2eeb..0d23452 100644
--- a/model/riscv_insts_next.sail
+++ b/model/riscv_insts_next.sail
@@ -9,6 +9,8 @@ mapping clause encdec = URET()
 function clause execute URET() = {
   if   (~ (haveUsrMode()))
   then handle_illegal()
+  else if ~ (ext_check_xret_priv (User))
+  then ext_fail_xret_priv ()
   else set_next_pc(exception_handler(cur_privilege, CTL_URET(), PC));
   RETIRE_FAIL
 }
diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail
index dd8a4a0..3f8ccd8 100644
--- a/model/riscv_insts_zicsr.sail
+++ b/model/riscv_insts_zicsr.sail
@@ -122,22 +122,22 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = {
     (0x3A2,  _) => { pmpWriteCfgReg(2, value); Some(value) },  // pmpcfg2
     (0x3A3, 32) => { pmpWriteCfgReg(3, value); Some(value) },  // pmpcfg3
 
-    (0x3B0,  _) => { pmpaddr0  = pmpWriteAddr(pmp0cfg,  pmpaddr0,  value); Some(pmpaddr0) },
-    (0x3B1,  _) => { pmpaddr1  = pmpWriteAddr(pmp1cfg,  pmpaddr1,  value); Some(pmpaddr1) },
-    (0x3B2,  _) => { pmpaddr2  = pmpWriteAddr(pmp2cfg,  pmpaddr2,  value); Some(pmpaddr2) },
-    (0x3B3,  _) => { pmpaddr3  = pmpWriteAddr(pmp3cfg,  pmpaddr3,  value); Some(pmpaddr3) },
-    (0x3B4,  _) => { pmpaddr4  = pmpWriteAddr(pmp4cfg,  pmpaddr4,  value); Some(pmpaddr4) },
-    (0x3B5,  _) => { pmpaddr5  = pmpWriteAddr(pmp5cfg,  pmpaddr5,  value); Some(pmpaddr5) },
-    (0x3B6,  _) => { pmpaddr6  = pmpWriteAddr(pmp6cfg,  pmpaddr6,  value); Some(pmpaddr6) },
-    (0x3B7,  _) => { pmpaddr7  = pmpWriteAddr(pmp7cfg,  pmpaddr7,  value); Some(pmpaddr7) },
-    (0x3B8,  _) => { pmpaddr8  = pmpWriteAddr(pmp8cfg,  pmpaddr8,  value); Some(pmpaddr8) },
-    (0x3B9,  _) => { pmpaddr9  = pmpWriteAddr(pmp9cfg,  pmpaddr9,  value); Some(pmpaddr9) },
-    (0x3BA,  _) => { pmpaddr10 = pmpWriteAddr(pmp10cfg, pmpaddr10, value); Some(pmpaddr10) },
-    (0x3BB,  _) => { pmpaddr11 = pmpWriteAddr(pmp11cfg, pmpaddr11, value); Some(pmpaddr11) },
-    (0x3BC,  _) => { pmpaddr12 = pmpWriteAddr(pmp12cfg, pmpaddr12, value); Some(pmpaddr12) },
-    (0x3BD,  _) => { pmpaddr13 = pmpWriteAddr(pmp13cfg, pmpaddr13, value); Some(pmpaddr13) },
-    (0x3BE,  _) => { pmpaddr14 = pmpWriteAddr(pmp14cfg, pmpaddr14, value); Some(pmpaddr14) },
-    (0x3BF,  _) => { pmpaddr15 = pmpWriteAddr(pmp15cfg, pmpaddr15, value); Some(pmpaddr15) },
+    (0x3B0,  _) => { pmpaddr0  = pmpWriteAddr(pmpLocked(pmp0cfg),  pmpTORLocked(pmp1cfg),  pmpaddr0,  value); Some(pmpaddr0) },
+    (0x3B1,  _) => { pmpaddr1  = pmpWriteAddr(pmpLocked(pmp1cfg),  pmpTORLocked(pmp2cfg),  pmpaddr1,  value); Some(pmpaddr1) },
+    (0x3B2,  _) => { pmpaddr2  = pmpWriteAddr(pmpLocked(pmp2cfg),  pmpTORLocked(pmp3cfg),  pmpaddr2,  value); Some(pmpaddr2) },
+    (0x3B3,  _) => { pmpaddr3  = pmpWriteAddr(pmpLocked(pmp3cfg),  pmpTORLocked(pmp4cfg),  pmpaddr3,  value); Some(pmpaddr3) },
+    (0x3B4,  _) => { pmpaddr4  = pmpWriteAddr(pmpLocked(pmp4cfg),  pmpTORLocked(pmp5cfg),  pmpaddr4,  value); Some(pmpaddr4) },
+    (0x3B5,  _) => { pmpaddr5  = pmpWriteAddr(pmpLocked(pmp5cfg),  pmpTORLocked(pmp6cfg),  pmpaddr5,  value); Some(pmpaddr5) },
+    (0x3B6,  _) => { pmpaddr6  = pmpWriteAddr(pmpLocked(pmp6cfg),  pmpTORLocked(pmp7cfg),  pmpaddr6,  value); Some(pmpaddr6) },
+    (0x3B7,  _) => { pmpaddr7  = pmpWriteAddr(pmpLocked(pmp7cfg),  pmpTORLocked(pmp8cfg),  pmpaddr7,  value); Some(pmpaddr7) },
+    (0x3B8,  _) => { pmpaddr8  = pmpWriteAddr(pmpLocked(pmp8cfg),  pmpTORLocked(pmp9cfg),  pmpaddr8,  value); Some(pmpaddr8) },
+    (0x3B9,  _) => { pmpaddr9  = pmpWriteAddr(pmpLocked(pmp9cfg),  pmpTORLocked(pmp10cfg), pmpaddr9,  value); Some(pmpaddr9) },
+    (0x3BA,  _) => { pmpaddr10 = pmpWriteAddr(pmpLocked(pmp10cfg), pmpTORLocked(pmp11cfg), pmpaddr10, value); Some(pmpaddr10) },
+    (0x3BB,  _) => { pmpaddr11 = pmpWriteAddr(pmpLocked(pmp11cfg), pmpTORLocked(pmp12cfg), pmpaddr11, value); Some(pmpaddr11) },
+    (0x3BC,  _) => { pmpaddr12 = pmpWriteAddr(pmpLocked(pmp12cfg), pmpTORLocked(pmp13cfg), pmpaddr12, value); Some(pmpaddr12) },
+    (0x3BD,  _) => { pmpaddr13 = pmpWriteAddr(pmpLocked(pmp13cfg), pmpTORLocked(pmp14cfg), pmpaddr13, value); Some(pmpaddr13) },
+    (0x3BE,  _) => { pmpaddr14 = pmpWriteAddr(pmpLocked(pmp14cfg), pmpTORLocked(pmp15cfg), pmpaddr14, value); Some(pmpaddr14) },
+    (0x3BF,  _) => { pmpaddr15 = pmpWriteAddr(pmpLocked(pmp15cfg), false,                  pmpaddr15, value); Some(pmpaddr15) },
 
     /* machine mode counters */
     (0xB00,  _) => { mcycle[(sizeof(xlen) - 1) .. 0] = value; Some(value) },
@@ -179,6 +179,8 @@ function clause execute CSR(csr, rs1, rd, is_imm, op) = {
   };
   if ~ (check_CSR(csr, cur_privilege, isWrite))
   then { handle_illegal(); RETIRE_FAIL }
+  else if ~ (ext_check_CSR(csr, cur_privilege, isWrite))
+  then { ext_check_CSR_fail(); RETIRE_FAIL }
   else {
     let csr_val = readCSR(csr); /* could have side-effects, so technically shouldn't perform for CSRW[I] with rd == 0 */
     if isWrite then {
@@ -206,6 +208,6 @@ mapping csr_mnemonic : csrop <-> string = {
 }
 
 mapping clause assembly = CSR(csr, rs1, rd, true, op)
-  <-> csr_mnemonic(op) ^ "i" ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_5(rs1) ^ sep() ^ csr_name_map(csr)
+  <-> csr_mnemonic(op) ^ "i" ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_5(rs1) ^ sep() ^ hex_bits_12(csr)
 mapping clause assembly = CSR(csr, rs1, rd, false, op)
-  <-> csr_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ csr_name_map(csr)
+  <-> csr_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_12(csr)
diff --git a/model/riscv_iris.sail b/model/riscv_iris.sail
new file mode 100644
index 0000000..80f3515
--- /dev/null
+++ b/model/riscv_iris.sail
@@ -0,0 +1,1176 @@
+default Order dec
+
+$include <smt.sail>
+$include <option.sail>
+$include <arith.sail>
+$include <string.sail>
+$include <vector_dec.sail>
+$include <regfp.sail>
+
+val string_startswith = "string_startswith" : (string, string) -> bool
+val string_drop = "string_drop" : (string, nat) -> string
+val string_take = "string_take" : (string, nat) -> string
+val string_length = "string_length" : string -> nat
+val string_append = {c: "concat_str", _: "string_append"} : (string, string) -> string
+
+val eq_anything = {ocaml: "(fun (x, y) -> x = y)", interpreter: "eq_anything", lem: "eq", coq: "generic_eq", c: "eq_anything"} : forall ('a : Type). ('a, 'a) -> bool
+
+overload operator == = {eq_string, eq_anything}
+
+val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg}
+/* sneaky deref with no effect necessary for bitfield writes */
+val _reg_deref = "reg_deref" : forall ('a : Type). register('a) -> 'a
+
+val any_vector_update = {ocaml: "update", lem: "update_list_dec", coq: "vector_update"} : forall 'n ('a : Type).
+  (vector('n, dec, 'a), int, 'a) -> vector('n, dec, 'a)
+
+overload vector_update = {any_vector_update}
+
+val update_subrange = {ocaml: "update_subrange", interpreter: "update_subrange", lem: "update_subrange_vec_dec", coq: "update_subrange_vec_dec"} : forall 'n 'm 'o.
+  (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n)
+
+val vector_concat = {ocaml: "append", lem: "append_list", coq: "vec_concat"} : forall ('n : Int) ('m : Int) ('a : Type).
+  (vector('n, dec, 'a), vector('m, dec, 'a)) -> vector('n + 'm, dec, 'a)
+
+overload append = {vector_concat}
+
+overload ~ = {not_bool, not_vec}
+
+val neq_vec = {lem: "neq"} : forall 'n. (bits('n), bits('n)) -> bool
+
+function neq_vec (x, y) = not_bool(eq_bits(x, y))
+
+val neq_anything = {lem: "neq", coq: "generic_neq"} : forall ('a : Type). ('a, 'a) -> bool
+
+function neq_anything (x, y) = not_bool(x == y)
+
+overload operator != = {neq_vec, neq_anything}
+
+overload operator & = {and_vec}
+
+overload operator | = {or_vec}
+
+val string_of_int = {c: "string_of_int", ocaml: "string_of_int", interpreter: "string_of_int", lem: "stringFromInteger", coq: "string_of_int"} : int -> string
+
+val "string_of_bits" : forall 'n. bits('n) -> string
+
+function string_of_bit(b: bit) -> string =
+  match b {
+    bitzero => "0b0",
+    bitone => "0b1"
+  }
+
+overload BitStr = {string_of_bits, string_of_bit}
+
+val xor_vec = {c: "xor_bits", _: "xor_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
+
+val int_power = {ocaml: "int_power", interpreter: "int_power", lem: "pow", coq: "pow", c: "pow_int"} : (int, int) -> int
+
+overload operator ^ = {xor_vec, int_power, concat_str}
+
+val sub_vec = {c: "sub_bits", _: "sub_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
+
+val sub_vec_int = {c: "sub_bits_int", _: "sub_vec_int"} : forall 'n. (bits('n), int) -> bits('n)
+
+overload operator - = {sub_vec, sub_vec_int}
+
+val quot_round_zero = {ocaml: "quot_round_zero", interpreter: "quot_round_zero", lem: "hardware_quot", c: "tdiv_int", coq: "Z.quot"} : (int, int) -> int
+val rem_round_zero = {ocaml: "rem_round_zero", interpreter: "rem_round_zero", lem: "hardware_mod", c: "tmod_int", coq: "Z.rem"} : (int, int) -> int
+
+/* The following should get us euclidean modulus, and is compatible with pre and post 0.9 versions of sail */
+overload operator % = {emod_int, mod}
+
+val min_nat = {ocaml: "min_int", interpreter: "min_int", lem: "min", coq: "min_nat", c: "min_int"} : (nat, nat) -> nat
+
+val min_int = {ocaml: "min_int", interpreter: "min_int", lem: "min", coq: "Z.min", c: "min_int"} : (int, int) -> int
+
+val max_nat = {ocaml: "max_int", interpreter: "max_int", lem: "max", coq: "max_nat", c: "max_int"} : (nat, nat) -> nat
+
+val max_int = {ocaml: "max_int", interpreter: "max_int", lem: "max", coq: "Z.max", c: "max_int"} : (int, int) -> int
+
+overload min = {min_nat, min_int}
+
+overload max = {max_nat, max_int}
+
+val pow2 = "pow2" : forall 'n. atom('n) -> atom(2 ^ 'n)
+
+val print = "print_endline" : string -> unit
+val print_string = "print_string" : (string, string) -> unit
+
+val print_instr    = {ocaml: "Platform.print_instr", interpreter: "print_endline", c: "print_instr", lem: "print_dbg", _: "print_endline"} : string -> unit
+val print_reg      = {ocaml: "Platform.print_reg", interpreter: "print_endline", c: "print_reg", lem: "print_dbg", _: "print_endline"} : string -> unit
+val print_mem      = {ocaml: "Platform.print_mem_access", interpreter: "print_endline", c: "print_mem_access", lem: "print_dbg", _: "print_endline"} : string -> unit
+val print_platform = {ocaml: "Platform.print_platform", interpreter: "print_endline", c: "print_platform", lem: "print_dbg", _: "print_endline"} : string -> unit
+
+val get_config_print_instr = {ocaml: "Platform.get_config_print_instr", c:"get_config_print_instr"} : unit -> bool
+val get_config_print_reg = {ocaml: "Platform.get_config_print_reg", c:"get_config_print_reg"} : unit -> bool
+val get_config_print_mem = {ocaml: "Platform.get_config_print_mem", c:"get_config_print_mem"} : unit -> bool
+
+val get_config_print_platform = {ocaml: "Platform.get_config_print_platform", c:"get_config_print_platform"} : unit -> bool
+// defaults for other backends
+function get_config_print_instr () = false
+function get_config_print_reg () = false
+function get_config_print_mem () = false
+function get_config_print_platform () = false
+
+val EXTS : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m)
+val EXTZ : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m)
+
+function EXTS(m, v) = sail_sign_extend(v, m)
+function EXTZ(m, v) = sail_zero_extend(v, m)
+
+val zeros_implicit : forall 'n, 'n >= 0 . implicit('n) -> bits('n)
+function zeros_implicit (n) = sail_zeros(n)
+overload zeros = {zeros_implicit}
+
+val ones : forall 'n, 'n >= 0 . implicit('n) -> bits('n)
+function ones (n) = sail_ones (n)
+
+val bool_to_bits : bool -> bits(1)
+function bool_to_bits x = if x then 0b1 else 0b0
+
+val bit_to_bool : bit -> bool
+function bit_to_bool b = match b {
+  bitone  => true,
+  bitzero => false
+}
+
+val to_bits : forall 'l, 'l >= 0.(atom('l), int) -> bits('l)
+function to_bits (l, n) = get_slice_int(l, n, 0)
+
+infix 4 <_s
+infix 4 >=_s
+infix 4 <_u
+infix 4 >=_u
+infix 4 <=_u
+
+val operator <_s  : forall 'n, 'n > 0. (bits('n), bits('n)) -> bool
+val operator >=_s : forall 'n, 'n > 0. (bits('n), bits('n)) -> bool
+val operator <_u  : forall 'n. (bits('n), bits('n)) -> bool
+val operator >=_u : forall 'n. (bits('n), bits('n)) -> bool
+val operator <=_u : forall 'n. (bits('n), bits('n)) -> bool
+
+function operator <_s  (x, y) = signed(x) < signed(y)
+function operator >=_s (x, y) = signed(x) >= signed(y)
+function operator <_u  (x, y) = unsigned(x) < unsigned(y)
+function operator >=_u (x, y) = unsigned(x) >= unsigned(y)
+function operator <=_u (x, y) = unsigned(x) <= unsigned(y)
+
+infix 7 >>
+infix 7 <<
+
+val "shift_bits_right" : forall 'n 'm. (bits('n), bits('m)) -> bits('n)
+val "shift_bits_left"  : forall 'n 'm. (bits('n), bits('m)) -> bits('n)
+
+val "shiftl" : forall 'm 'n, 'n >= 0. (bits('m), atom('n)) -> bits('m)
+val "shiftr" : forall 'm 'n, 'n >= 0. (bits('m), atom('n)) -> bits('m)
+
+overload operator >> = {shift_bits_right, shiftr}
+overload operator << = {shift_bits_left, shiftl}
+
+/* Ideally these would be sail builtin */
+
+function shift_right_arith64 (v : bits(64), shift : bits(6)) -> bits(64) =
+    let v128 : bits(128) = EXTS(v) in
+    (v128 >> shift)[63..0]
+
+function shift_right_arith32 (v : bits(32), shift : bits(5)) -> bits(32) =
+    let v64 : bits(64) = EXTS(v) in
+    (v64 >> shift)[31..0]
+
+val "decimal_string_of_bits" : forall 'n. bits('n) -> string
+val hex_bits : forall 'n . (atom('n), bits('n)) <-> string
+
+/* Define the XLEN value for the architecture. */
+
+type xlen       : Int = 64
+type xlen_bytes : Int = 8
+type xlenbits         = bits(xlen)
+/* The default metadata carries no information, and is implemented
+ * using a unit type.
+ */
+
+type mem_meta = unit
+
+let default_meta : mem_meta = ()
+
+val __WriteRAM_Meta : forall 'n. (xlenbits, atom('n), mem_meta) -> unit effect {wmvt}
+function __WriteRAM_Meta(addr, width, meta) = ()
+
+val __ReadRAM_Meta  : forall 'n. (xlenbits, atom('n)) -> mem_meta effect {rmem}
+function __ReadRAM_Meta(addr, width) = ()
+/* These functions define the primitives for physical memory access.
+ * They depend on the XLEN of the architecture.
+ *
+ * They also depend on the type of metadata that is read and written
+ * to physical memory.  For models that do not require this metadata,
+ * a unit type can be used.
+ *
+ * The underlying __read_mem and __write_mem functions are from the
+ * Sail library.  The metadata primitives __{Read,Write}RAM_Meta are
+ * in prelude_mem_metadata.
+ */
+
+
+/* This is a slightly arbitrary limit on the maximum number of bytes
+   in a memory access.  It helps to generate slightly better C code
+   because it means width argument can be fast native integer. It
+   would be even better if it could be <= 8 bytes so that data can
+   also be a 64-bit int but CHERI needs 128-bit accesses for
+   capabilities and SIMD / vector instructions will also need more. */
+type max_mem_access : Int = 16
+
+val write_ram = {lem: "write_ram", coq: "write_ram"} : forall 'n, 0 < 'n <= max_mem_access . (write_kind, xlenbits, atom('n), bits(8 * 'n), mem_meta) -> bool effect {wmv, wmvt}
+
+val write_ram_ea : forall 'n, 0 < 'n <= max_mem_access . (write_kind, xlenbits, atom('n)) -> unit effect {eamem}
+function write_ram_ea(wk, addr, width) =
+  __write_mem_ea(wk, sizeof(xlen), addr, width)
+
+val read_ram = {lem: "read_ram", coq: "read_ram"} : forall 'n, 0 < 'n <= max_mem_access .  (read_kind, xlenbits, atom('n), bool) -> (bits(8 * 'n), mem_meta) effect {rmem, rmemt}
+function read_ram(rk, addr, width, read_meta) =
+  let meta = if read_meta then __ReadRAM_Meta(addr, width) else default_meta in
+  (__read_mem(rk, sizeof(xlen), addr, width), meta)
+
+
+/* Basic type and function definitions used pervasively in the model. */
+
+/* this value is only defined for the runtime platform for ELF loading
+ * checks, and not used in the model.
+ */
+let xlen_val = sizeof(xlen)
+
+let xlen_max_unsigned = 2 ^ sizeof(xlen) - 1
+let xlen_max_signed = 2 ^ (sizeof(xlen) - 1) - 1
+let xlen_min_signed = 0 - 2 ^ (sizeof(xlen) - 1)
+
+type half = bits(16)
+type word = bits(32)
+
+/* register identifiers */
+
+type regidx  = bits(5)
+type cregidx = bits(3)    /* identifiers in RVC instructions */
+type csreg   = bits(12)   /* CSR addressing */
+
+/* register file indexing */
+
+type regno ('n : Int), 0 <= 'n < 32 = atom('n)
+
+val regidx_to_regno : bits(5) -> {'n, 0 <= 'n < 32. regno('n)}
+function regidx_to_regno b = let 'r = unsigned(b) in r
+
+/* mapping RVC register indices into normal indices */
+val creg2reg_idx : cregidx -> regidx
+function creg2reg_idx(creg) = 0b01 @ creg
+
+/* some architecture and ABI relevant register identifiers */
+let zreg : regidx = 0b00000  /* x0, zero register  */
+let ra   : regidx = 0b00001  /* x1, return address */
+let sp   : regidx = 0b00010  /* x2, stack pointer  */
+
+/* instruction fields */
+
+type opcode = bits(7)
+type imm12  = bits(12)
+type imm20  = bits(20)
+type amo    = bits(1)  /* amo opcode flags */
+
+/* base architecture definitions */
+
+enum Architecture = {RV32, RV64, RV128}
+type arch_xlen = bits(2)
+function architecture(a : arch_xlen) -> option(Architecture) =
+  match (a) {
+    0b01 => Some(RV32),
+    0b10 => Some(RV64),
+    0b11 => Some(RV128),
+    _    => None()
+  }
+
+function arch_to_bits(a : Architecture) -> arch_xlen =
+  match (a) {
+    RV32  => 0b01,
+    RV64  => 0b10,
+    RV128 => 0b11
+  }
+
+/* enum denoting whether an executed instruction retires */
+
+enum Retired = {RETIRE_SUCCESS, RETIRE_FAIL}
+
+/* memory access types */
+
+union AccessType ('a : Type) = {
+  Read      : 'a,
+  Write     : 'a,
+  ReadWrite : 'a,
+  Execute   : unit
+}
+
+enum word_width = {BYTE, HALF, WORD, DOUBLE}
+/* model-internal exceptions */
+
+union exception = {
+  Error_not_implemented : string,
+  Error_internal_error  : unit
+}
+
+val not_implemented : forall ('a : Type). string -> 'a effect {escape}
+function not_implemented message = throw(Error_not_implemented(message))
+
+val internal_error : forall ('a : Type). string -> 'a effect {escape}
+function internal_error(s) = {
+    assert (false, s);
+    throw Error_internal_error()
+}
+
+/* instruction opcode grouping */
+enum bop = {RISCV_BEQ, RISCV_BNE, RISCV_BLT,
+            RISCV_BGE, RISCV_BLTU, RISCV_BGEU}    /* branch ops */
+enum iop = {RISCV_ADDI, RISCV_SLTI, RISCV_SLTIU,
+            RISCV_XORI, RISCV_ORI, RISCV_ANDI}    /* immediate ops */
+
+mapping bool_bits : bool <-> bits(1) = {
+  true   <-> 0b1,
+  false  <-> 0b0
+}
+
+mapping bool_not_bits : bool <-> bits(1) = {
+  true   <-> 0b0,
+  false  <-> 0b1
+}
+
+mapping size_bits : word_width <-> bits(2) = {
+  BYTE   <-> 0b00,
+  HALF   <-> 0b01,
+  WORD   <-> 0b10,
+  DOUBLE <-> 0b11
+}
+
+val word_width_bytes : word_width -> {'s, 's == 1 | 's == 2 | 's == 4 | 's == 8 . atom('s)}
+function word_width_bytes width = match width {
+  BYTE   => 1,
+  HALF   => 2,
+  WORD   => 4,
+  DOUBLE => 8
+}
+// Extensions for memory Accesstype.
+
+type ext_access_type = unit
+
+let Data  : ext_access_type = ()
+
+let default_write_acc : ext_access_type = Data
+
+val accessType_to_str : AccessType(ext_access_type) -> string
+function accessType_to_str (a) =
+  match (a) {
+    Read(Data)      => "R",
+    Write(Data)     => "W",
+    ReadWrite(Data) => "RW",
+    Execute()       => "X"
+  }
+
+overload to_str = {accessType_to_str}
+/* default register type */
+type regtype = xlenbits
+
+/* default zero register */
+let zero_reg : regtype = EXTZ(0x0)
+
+/* default register printer */
+val RegStr : regtype -> string
+function RegStr(r) = BitStr(r)
+
+/* conversions */
+
+val regval_from_reg : regtype -> xlenbits
+function regval_from_reg(r) = r
+
+val regval_into_reg : xlenbits -> regtype
+function regval_into_reg(v) = v
+/* program counter */
+
+register PC       : xlenbits
+register nextPC   : xlenbits
+
+/* internal state to hold instruction bits for faulting instructions */
+register instbits : xlenbits
+
+/* register file and accessors */
+
+register Xs : vector(32, dec, regtype)
+
+register x1  : regtype
+register x2  : regtype
+register x3  : regtype
+register x4  : regtype
+register x5  : regtype
+register x6  : regtype
+register x7  : regtype
+register x8  : regtype
+register x9  : regtype
+register x10 : regtype
+register x11 : regtype
+register x12 : regtype
+register x13 : regtype
+register x14 : regtype
+register x15 : regtype
+register x16 : regtype
+register x17 : regtype
+register x18 : regtype
+register x19 : regtype
+register x20 : regtype
+register x21 : regtype
+register x22 : regtype
+register x23 : regtype
+register x24 : regtype
+register x25 : regtype
+register x26 : regtype
+register x27 : regtype
+register x28 : regtype
+register x29 : regtype
+register x30 : regtype
+register x31 : regtype
+
+val rX : forall 'n, 0 <= 'n < 32. regno('n) -> xlenbits effect {rreg, escape}
+function rX r = {
+  let v : regtype =
+    match r {
+      0 => zero_reg,
+      1 => x1,
+      2 => x2,
+      3 => x3,
+      4 => x4,
+      5 => x5,
+      6 => x6,
+      7 => x7,
+      8 => x8,
+      9 => x9,
+      10 => x10,
+      11 => x11,
+      12 => x12,
+      13 => x13,
+      14 => x14,
+      15 => x15,
+      16 => x16,
+      17 => x17,
+      18 => x18,
+      19 => x19,
+      20 => x20,
+      21 => x21,
+      22 => x22,
+      23 => x23,
+      24 => x24,
+      25 => x25,
+      26 => x26,
+      27 => x27,
+      28 => x28,
+      29 => x29,
+      30 => x30,
+      31 => x31,
+      _  => {assert(false, "invalid register number"); zero_reg}
+    };
+  regval_from_reg(v)
+}
+
+val wX : forall 'n, 0 <= 'n < 32. (regno('n), xlenbits) -> unit effect {wreg, escape}
+function wX (r, in_v) = {
+  let v = regval_into_reg(in_v);
+  match r {
+    0  => (),
+    1  => x1 = v,
+    2  => x2 = v,
+    3  => x3 = v,
+    4  => x4 = v,
+    5  => x5 = v,
+    6  => x6 = v,
+    7  => x7 = v,
+    8  => x8 = v,
+    9  => x9 = v,
+    10 => x10 = v,
+    11 => x11 = v,
+    12 => x12 = v,
+    13 => x13 = v,
+    14 => x14 = v,
+    15 => x15 = v,
+    16 => x16 = v,
+    17 => x17 = v,
+    18 => x18 = v,
+    19 => x19 = v,
+    20 => x20 = v,
+    21 => x21 = v,
+    22 => x22 = v,
+    23 => x23 = v,
+    24 => x24 = v,
+    25 => x25 = v,
+    26 => x26 = v,
+    27 => x27 = v,
+    28 => x28 = v,
+    29 => x29 = v,
+    30 => x30 = v,
+    31 => x31 = v,
+    _  => assert(false, "invalid register number")
+  };
+  if (r != 0) then {
+     if   get_config_print_reg()
+     then print_reg("x" ^ string_of_int(r) ^ " <- " ^ RegStr(v));
+  }
+}
+
+function rX_bits(i: bits(5)) -> xlenbits = rX(unsigned(i))
+
+function wX_bits(i: bits(5), data: xlenbits) -> unit = {
+  wX(unsigned(i)) = data
+}
+
+overload X = {rX_bits, wX_bits, rX, wX}
+
+val init_base_regs : unit -> unit effect {wreg}
+function init_base_regs () = {
+  x1  = zero_reg;
+  x2  = zero_reg;
+  x3  = zero_reg;
+  x4  = zero_reg;
+  x5  = zero_reg;
+  x6  = zero_reg;
+  x7  = zero_reg;
+  x8  = zero_reg;
+  x9  = zero_reg;
+  x10 = zero_reg;
+  x11 = zero_reg;
+  x12 = zero_reg;
+  x13 = zero_reg;
+  x14 = zero_reg;
+  x15 = zero_reg;
+  x16 = zero_reg;
+  x17 = zero_reg;
+  x18 = zero_reg;
+  x19 = zero_reg;
+  x20 = zero_reg;
+  x21 = zero_reg;
+  x22 = zero_reg;
+  x23 = zero_reg;
+  x24 = zero_reg;
+  x25 = zero_reg;
+  x26 = zero_reg;
+  x27 = zero_reg;
+  x28 = zero_reg;
+  x29 = zero_reg;
+  x30 = zero_reg;
+  x31 = zero_reg
+}
+/* accessors for default architectural addresses, for use from within instructions */
+
+/*!
+  Retrieves the architectural PC value. This is not necessarily the value
+  found in the PC register as extensions may choose to override this function.
+  The value in the PC register is the absolute virtual address of the instruction
+  to fetch.
+ */
+val get_arch_pc : unit -> xlenbits effect {rreg}
+function get_arch_pc() = PC
+
+val get_next_pc : unit -> xlenbits effect {rreg}
+function get_next_pc() = nextPC
+
+val set_next_pc : xlenbits -> unit effect {wreg}
+function set_next_pc(pc) = {
+  nextPC = pc
+}
+
+val tick_pc : unit -> unit effect {rreg, wreg}
+function tick_pc() = {
+  PC = nextPC
+}
+
+/* Extensions may wish to interpose on fetch, control transfer, and data
+ * addresses used to access memory and perhaps modify them.  This file
+ * defines the return values used by functions that perform this interposition.
+ *
+ * The model defines defaults for these functions in riscv_addr_checks.sail;
+ * extensions would need to define their own functions to override them.
+ */
+
+union Ext_FetchAddr_Check ('a : Type) = {
+  Ext_FetchAddr_OK  : xlenbits,  /* PC value to use for the actual fetch */
+  Ext_FetchAddr_Error : 'a
+}
+
+union Ext_ControlAddr_Check ('a : Type) = {
+  Ext_ControlAddr_OK : xlenbits, /* PC value to use for the target of the control operation */
+  Ext_ControlAddr_Error : 'a
+}
+
+union Ext_DataAddr_Check ('a : Type) = {
+  Ext_DataAddr_OK : xlenbits,    /* Address to use for the data access */
+  Ext_DataAddr_Error : 'a
+}
+/* default fetch address checks */
+
+type ext_fetch_addr_error = unit
+
+/* Since fetch is done in granules, the check function gets two arguments:
+ * start_pc: the PC at the start of the current fetch sequence
+ * pc:       the PC for the current granule
+ *
+ * returns:  the *virtual* memory address to use for the fetch.
+ *           any address translation errors are reported for pc, not the returned value.
+ */
+function ext_fetch_check_pc(start_pc : xlenbits, pc : xlenbits) -> Ext_FetchAddr_Check(ext_fetch_addr_error) =
+  Ext_FetchAddr_OK(pc)
+
+function ext_handle_fetch_check_error(err : ext_fetch_addr_error) -> unit =
+  ()
+
+/* default control address checks */
+
+type ext_control_addr_error = unit
+
+/* these functions return the address to use as the target for
+ * the control transfer.  any address translation or other errors
+ * are reported for the original value, not the returned value.
+ *
+ * NOTE: the input value does *not* have bit[0] set to 0, to enable
+ * more accurate bounds checking.  There is no constraint on the output
+ * value, which will have bit[0] cleared by the caller if needed.
+ */
+
+/* the control address is derived from a non-PC register, e.g. in JALR */
+function ext_control_check_addr(pc : xlenbits) -> Ext_ControlAddr_Check(ext_control_addr_error) =
+  Ext_ControlAddr_OK(pc)
+
+/* the control address is derived from the PC register, e.g. in JAL */
+function ext_control_check_pc(pc : xlenbits) -> Ext_ControlAddr_Check(ext_control_addr_error) =
+  Ext_ControlAddr_OK(pc)
+
+function ext_handle_control_check_error(err : ext_control_addr_error) -> unit =
+  ()
+
+
+/* The default data address function does not perform any checks so
+   just uses unit for error type. */
+type ext_data_addr_error = unit
+
+/* Default data addr is just base register + immediate offset (may be zero).
+   Extensions might override and add additional checks. */
+function ext_data_get_addr(base : regidx, offset : xlenbits, acc : AccessType(ext_access_type), width : word_width)
+         -> Ext_DataAddr_Check(ext_data_addr_error) =
+  let addr = X(base) + offset in
+  Ext_DataAddr_OK(addr)
+
+/* Machine-mode and supervisor-mode functionality. */
+
+union ExceptionType = {
+ E_Fetch_Addr_Align   : unit,
+ E_Fetch_Access_Fault : unit,
+ E_Illegal_Instr      : unit,
+ E_Breakpoint         : unit,
+ E_Load_Addr_Align    : unit,
+ E_Load_Access_Fault  : unit,
+ E_SAMO_Addr_Align    : unit,
+ E_SAMO_Access_Fault  : unit,
+ E_U_EnvCall          : unit,
+ E_S_EnvCall          : unit,
+ E_Reserved_10        : unit,
+ E_M_EnvCall          : unit,
+ E_Fetch_Page_Fault   : unit,
+ E_Load_Page_Fault    : unit,
+ E_Reserved_14        : unit,
+ E_SAMO_Page_Fault    : unit,
+}
+
+function handle_mem_exception(addr : xlenbits, e : ExceptionType) -> unit = {
+  assert(false);
+}
+
+
+/* memory access exceptions, defined here for use by the platform model. */
+
+union MemoryOpResult ('a : Type) = {
+  MemValue     : 'a,
+  MemException : ExceptionType
+}
+
+val MemoryOpResult_add_meta : forall ('t : Type). (MemoryOpResult('t), mem_meta) -> MemoryOpResult(('t, mem_meta))
+function MemoryOpResult_add_meta(r, m) = match r {
+  MemValue(v)     => MemValue(v, m),
+  MemException(e) => MemException(e)
+}
+
+val MemoryOpResult_drop_meta : forall ('t : Type). MemoryOpResult(('t, mem_meta)) -> MemoryOpResult('t)
+function MemoryOpResult_drop_meta(r) = match r {
+  MemValue(v, m)  => MemValue(v),
+  MemException(e) => MemException(e)
+}
+
+/* whether the platform supports misaligned accesses without trapping to M-mode. if false,
+ * misaligned loads/stores are trapped to Machine mode.
+ */
+function plat_enable_misaligned_access ()  : unit -> bool = true
+
+/* Platform-specific handling of instruction faults */
+
+function handle_illegal() -> unit = {
+  assert(false);
+}
+
+/* Physical memory model.
+ *
+ * This assumes that the platform memory map has been defined, so that accesses
+ * to MMIO regions can be dispatched.
+ *
+ * The implementation below supports the reading and writing of memory
+ * metadata in addition to raw memory data.
+ *
+ * The external API for this module is
+ *   {mem_read, mem_read_meta, mem_write_ea, mem_write_value_meta, mem_write_value}
+ * where mem_write_value is a special case of mem_write_value_meta that uses
+ * a default value of the metadata.
+ *
+ * The internal implementation first performs a PMP check (if PMP is
+ * enabled), and then dispatches to MMIO regions or physical memory as
+ * per the platform memory map.
+ */
+
+function is_aligned_addr forall 'n. (addr : xlenbits, width : atom('n)) -> bool =
+  unsigned(addr) % width == 0
+
+function read_kind_of_flags (aq : bool, rl : bool, res : bool) -> option(read_kind) =
+  match (aq, rl, res) {
+    (false, false, false) => Some(Read_plain),
+    (true, false, false)  => Some(Read_RISCV_acquire),
+    (true, true, false)   => Some(Read_RISCV_strong_acquire),
+    (false, false, true)  => Some(Read_RISCV_reserved),
+    (true, false, true)   => Some(Read_RISCV_reserved_acquire),
+    (true, true, true)    => Some(Read_RISCV_reserved_strong_acquire),
+    (false, true, false)  => None(), /* should these be instead throwing error_not_implemented as below? */
+    (false, true, true)   => None()
+  }
+
+// only used for actual memory regions, to avoid MMIO effects
+function phys_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), paddr : xlenbits, width : atom('n), aq : bool, rl: bool, res : bool, meta : bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) = {
+  let result = (match read_kind_of_flags(aq, rl, res) {
+    Some(rk) => Some(read_ram(rk, paddr, width, meta)),
+    None()   => None()
+  }) : option((bits(8 * 'n), mem_meta));
+  match (t, result) {
+    (Execute(),  None()) => MemException(E_Fetch_Access_Fault()),
+    (Read(Data), None()) => MemException(E_Load_Access_Fault()),
+    (_,          None()) => MemException(E_SAMO_Access_Fault()),
+    (_,      Some(v, m)) => { MemValue(v, m) }
+  }
+}
+
+val mem_read      : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n))             effect {rmem, rmemt, rreg, escape}
+
+function mem_read (typ, paddr, width, aq, rl, res) = {
+ let result : MemoryOpResult(bits(8 * 'n)) =
+  if (aq | res) & (~ (is_aligned_addr(paddr, width)))
+  then MemException(E_Load_Addr_Align())
+  else match (aq, rl, res) {
+    (false, true,  false) => throw(Error_not_implemented("load.rl")),
+    (false, true,  true)  => throw(Error_not_implemented("lr.rl")),
+    (_, _, _)             => MemoryOpResult_drop_meta(phys_mem_read(typ, paddr, width, aq, rl, res, false))
+  };
+ result
+}
+
+val mem_write_ea : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(unit) effect {eamem, escape}
+
+function mem_write_ea (addr, width, aq, rl, con) = {
+  if (rl | con) & (~ (is_aligned_addr(addr, width)))
+  then MemException(E_SAMO_Addr_Align())
+  else match (aq, rl, con) {
+    (false, false, false) => MemValue(write_ram_ea(Write_plain, addr, width)),
+    (false, true,  false) => MemValue(write_ram_ea(Write_RISCV_release, addr, width)),
+    (false, false, true)  => MemValue(write_ram_ea(Write_RISCV_conditional, addr, width)),
+    (false, true , true)  => MemValue(write_ram_ea(Write_RISCV_conditional_release, addr, width)),
+    (true,  false, false) => throw(Error_not_implemented("store.aq")),
+    (true,  true,  false) => MemValue(write_ram_ea(Write_RISCV_strong_release, addr, width)),
+    (true,  false, true)  => throw(Error_not_implemented("sc.aq")),
+    (true,  true , true)  => MemValue(write_ram_ea(Write_RISCV_conditional_strong_release, addr, width))
+  }
+}
+
+// only used for actual memory regions, to avoid MMIO effects
+function phys_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk : write_kind, paddr : xlenbits, width : atom('n), data : bits(8 * 'n), meta : mem_meta) -> MemoryOpResult(bool) = {
+  let result = MemValue(write_ram(wk, paddr, width, data, meta));
+  result
+}
+
+/* Atomic accesses can be done to MMIO regions, e.g. in kernel access to device registers. */
+
+/* Memory write with an explicit metadata value.  Metadata writes are
+ * currently assumed to have the same alignment constraints as their
+ * data.
+ * NOTE: The wreg effect is due to MMIO, the rreg is due to checking mtime.
+ */
+val mem_write_value_meta : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bits(8 * 'n), ext_access_type, mem_meta, bool, bool, bool) -> MemoryOpResult(bool) effect {wmv, wmvt, rreg, wreg, escape}
+function mem_write_value_meta (paddr, width, value, ext_acc, meta, aq, rl, con) = {
+  if (rl | con) & (~ (is_aligned_addr(paddr, width)))
+  then MemException(E_SAMO_Addr_Align())
+  else match (aq, rl, con) {
+    (false, false, false) => phys_mem_write(Write_plain, paddr, width, value, meta),
+    (false, true,  false) => phys_mem_write(Write_RISCV_release, paddr, width, value, meta),
+    (false, false, true)  => phys_mem_write(Write_RISCV_conditional, paddr, width, value, meta),
+    (false, true , true)  => phys_mem_write(Write_RISCV_conditional_release, paddr, width, value, meta),
+    (true,  true,  false) => phys_mem_write(Write_RISCV_strong_release, paddr, width, value, meta),
+    (true,  true , true)  => phys_mem_write(Write_RISCV_conditional_strong_release, paddr, width, value, meta),
+    // throw an illegal instruction here?
+    (true,  false, false) => throw(Error_not_implemented("store.aq")),
+    (true,  false, true)  => throw(Error_not_implemented("sc.aq"))
+  }
+}
+
+/* Memory write with a default metadata value. */
+val mem_write_value : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bits(8 * 'n), bool, bool, bool) -> MemoryOpResult(bool) effect {wmv, wmvt, rreg, wreg, escape}
+function mem_write_value (paddr, width, value, aq, rl, con) =
+  mem_write_value_meta(paddr, width, value, default_write_acc, default_meta, aq, rl, con)
+
+/* Result of address translation */
+
+type ext_ptw = unit
+
+union TR_Result('paddr : Type, 'failure : Type) = {
+  TR_Address : ('paddr, ext_ptw),
+  TR_Failure : ('failure, ext_ptw)
+}
+
+val translateAddr : (xlenbits, AccessType(ext_access_type)) -> TR_Result(xlenbits, ExceptionType) effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
+function translateAddr(vAddr, ac) = {
+  TR_Address(vAddr, ());
+}
+
+/* Instruction definitions.
+ *
+ * This includes decoding, execution, and assembly parsing and printing.
+ */
+
+scattered union ast
+
+/* returns whether an instruction was retired, used for computing minstret */
+val execute : ast -> Retired effect {escape, wreg, rreg, wmv, wmvt, eamem, rmem, rmemt, barr, exmem, undef}
+scattered function execute
+
+val encdec : ast <-> bits(32)
+scattered mapping encdec
+
+///* see riscv_jalr_seq.sail or riscv_jalr_rmem.sail for the execute clause. */
+//
+///* *****************************************************************
+//union clause ast = BTYPE : (bits(13), regidx, regidx, bop)
+//
+//mapping encdec_bop : bop <-> bits(3) = {
+//  RISCV_BEQ  <-> 0b000,
+//  RISCV_BNE  <-> 0b001,
+//  RISCV_BLT  <-> 0b100,
+//  RISCV_BGE  <-> 0b101,
+//  RISCV_BLTU <-> 0b110,
+//  RISCV_BGEU <-> 0b111
+//}
+//
+//mapping clause encdec = BTYPE(imm7_6 @ imm5_0 @ imm7_5_0 @ imm5_4_1 @ 0b0, rs2, rs1, op)
+//  <-> imm7_6 : bits(1) @ imm7_5_0 : bits(6) @ rs2 @ rs1 @ encdec_bop(op) @ imm5_4_1 : bits(4) @ imm5_0 : bits(1) @ 0b1100011
+//
+//function clause execute (BTYPE(imm, rs2, rs1, op)) = {
+//  let rs1_val = X(rs1);
+//  let rs2_val = X(rs2);
+//  let taken : bool = match op {
+//    RISCV_BEQ  => rs1_val == rs2_val,
+//    RISCV_BNE  => rs1_val != rs2_val,
+//    RISCV_BLT  => rs1_val <_s rs2_val,
+//    RISCV_BGE  => rs1_val >=_s rs2_val,
+//    RISCV_BLTU => rs1_val <_u rs2_val,
+//    RISCV_BGEU => rs1_val >=_u rs2_val
+//  };
+//  let t : xlenbits = PC + EXTS(imm);
+//  if taken then {
+//    /* Extensions get the first checks on the prospective target address. */
+//    match ext_control_check_pc(t) {
+//      Ext_ControlAddr_Error(e) => {
+//        assert(false);
+//        RETIRE_FAIL
+//      },
+//      Ext_ControlAddr_OK(target) => {
+//        if bit_to_bool(target[1]) & (~ (haveRVC())) then {
+//          handle_mem_exception(target, E_Fetch_Addr_Align());
+//          RETIRE_FAIL;
+//        } else {
+//          set_next_pc(target);
+//          RETIRE_SUCCESS
+//        }
+//      }
+//    }
+//  } else RETIRE_SUCCESS
+//}
+
+/* ****************************************************************** */
+union clause ast = ITYPE : (bits(12), regidx, regidx, iop)
+
+mapping encdec_iop : iop <-> bits(3) = {
+  RISCV_ADDI  <-> 0b000,
+  RISCV_SLTI  <-> 0b010,
+  RISCV_SLTIU <-> 0b011,
+  RISCV_ANDI  <-> 0b111,
+  RISCV_ORI   <-> 0b110,
+  RISCV_XORI  <-> 0b100
+}
+
+mapping clause encdec = ITYPE(imm, rs1, rd, op)
+  <-> imm @ rs1 @ encdec_iop(op) @ rd @ 0b0010011
+
+function clause execute (ITYPE (imm, rs1, rd, op)) = {
+  let rs1_val = X(rs1);
+  let immext : xlenbits = EXTS(imm);
+  let result : xlenbits = match op {
+    RISCV_ADDI  => rs1_val + immext,
+    RISCV_SLTI  => EXTZ(bool_to_bits(rs1_val <_s immext)),
+    RISCV_SLTIU => EXTZ(bool_to_bits(rs1_val <_u immext)),
+    RISCV_ANDI  => rs1_val & immext,
+    RISCV_ORI   => rs1_val | immext,
+    RISCV_XORI  => rs1_val ^ immext
+  };
+  X(rd) = result;
+  RETIRE_SUCCESS
+}
+
+mapping itype_mnemonic : iop <-> string = {
+  RISCV_ADDI  <-> "addi",
+  RISCV_SLTI  <-> "slti",
+  RISCV_SLTIU <-> "sltiu",
+  RISCV_XORI  <-> "xori",
+  RISCV_ORI   <-> "ori",
+  RISCV_ANDI  <-> "andi"
+}
+
+/* ****************************************************************** */
+union clause ast = LOAD : (bits(12), regidx, regidx, bool, word_width, bool, bool)
+
+/* unsigned loads are only present for widths strictly less than xlen,
+   signed loads also present for widths equal to xlen */
+mapping clause encdec = LOAD(imm, rs1, rd, is_unsigned, size, false, false) if (word_width_bytes(size) < sizeof(xlen_bytes)) | (not_bool(is_unsigned) & word_width_bytes(size) <= sizeof(xlen_bytes))
+  <-> imm @ rs1 @ bool_bits(is_unsigned) @ size_bits(size) @ rd @ 0b0000011 if (word_width_bytes(size) < sizeof(xlen_bytes)) | (not_bool(is_unsigned) & word_width_bytes(size) <= sizeof(xlen_bytes))
+
+val extend_value : forall 'n, 0 < 'n <= xlen_bytes. (bool, MemoryOpResult(bits(8 * 'n))) -> MemoryOpResult(xlenbits)
+function extend_value(is_unsigned, value) = match (value) {
+  MemValue(v)     => MemValue(if is_unsigned then EXTZ(v) else EXTS(v) : xlenbits),
+  MemException(e) => MemException(e)
+}
+
+val process_load : forall 'n, 0 < 'n <= xlen_bytes. (regidx, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> Retired effect {escape, rreg, wreg}
+function process_load(rd, addr, value, is_unsigned) =
+  match extend_value(is_unsigned, value) {
+    MemValue(result) => { X(rd) = result; RETIRE_SUCCESS },
+    MemException(e)  => { handle_mem_exception(addr, e); RETIRE_FAIL }
+  }
+
+function check_misaligned(vaddr : xlenbits, width : word_width) -> bool =
+  if   plat_enable_misaligned_access() then false
+  else match width {
+         BYTE   => false,
+         HALF   => vaddr[0] == bitone,
+         WORD   => vaddr[0] == bitone | vaddr[1] == bitone,
+         DOUBLE => vaddr[0] == bitone | vaddr[1] == bitone | vaddr[2] == bitone
+       }
+
+function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = {
+  let offset : xlenbits = EXTS(imm);
+  /* Get the address, X(rs1) + offset.
+     Some extensions perform additional checks on address validity. */
+  match ext_data_get_addr(rs1, offset, Read(Data), width) {
+    Ext_DataAddr_Error(e)  => { assert(false); RETIRE_FAIL },
+    Ext_DataAddr_OK(vaddr) =>
+      if   check_misaligned(vaddr, width)
+      then { handle_mem_exception(vaddr, E_Load_Addr_Align()); RETIRE_FAIL }
+      else match translateAddr(vaddr, Read(Data)) {
+        TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
+        TR_Address(addr, _) =>
+          match (width, sizeof(xlen)) {
+            (BYTE, _)   =>
+               process_load(rd, vaddr, mem_read(Read(Data), addr, 1, aq, rl, false), is_unsigned),
+            (HALF, _)   =>
+               process_load(rd, vaddr, mem_read(Read(Data), addr, 2, aq, rl, false), is_unsigned),
+            (WORD, _)   =>
+               process_load(rd, vaddr, mem_read(Read(Data), addr, 4, aq, rl, false), is_unsigned),
+            (DOUBLE, 64) =>
+               process_load(rd, vaddr, mem_read(Read(Data), addr, 8, aq, rl, false), is_unsigned)
+          }
+      }
+  }
+}
+
+/* ****************************************************************** */
+union clause ast = STORE : (bits(12), regidx, regidx, word_width, bool, bool)
+
+mapping clause encdec = STORE(imm7 @ imm5, rs2, rs1, size, false, false)              if word_width_bytes(size) <= sizeof(xlen_bytes)
+  <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b0 @ size_bits(size) @ imm5 : bits(5) @ 0b0100011 if word_width_bytes(size) <= sizeof(xlen_bytes)
+
+/* NOTE: Currently, we only EA if address translation is successful.
+   This may need revisiting. */
+function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = {
+  let offset : xlenbits = EXTS(imm);
+  /* Get the address, X(rs1) + offset.
+     Some extensions perform additional checks on address validity. */
+  match ext_data_get_addr(rs1, offset, Write(Data), width) {
+    Ext_DataAddr_Error(e)  => { assert (false); RETIRE_FAIL },
+    Ext_DataAddr_OK(vaddr) =>
+      if   check_misaligned(vaddr, width)
+      then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); RETIRE_FAIL }
+      else match translateAddr(vaddr, Write(Data)) {
+        TR_Failure(e, _)    => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
+        TR_Address(addr, _) => {
+          let eares : MemoryOpResult(unit) = match width {
+            BYTE   => mem_write_ea(addr, 1, aq, rl, false),
+            HALF   => mem_write_ea(addr, 2, aq, rl, false),
+            WORD   => mem_write_ea(addr, 4, aq, rl, false),
+            DOUBLE => mem_write_ea(addr, 8, aq, rl, false)
+          };
+          match (eares) {
+            MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL },
+            MemValue(_) => {
+              let rs2_val = X(rs2);
+              let res : MemoryOpResult(bool) = match (width, sizeof(xlen)) {
+                (BYTE, _)    => mem_write_value(addr, 1, rs2_val[7..0],  aq, rl, false),
+                (HALF, _)    => mem_write_value(addr, 2, rs2_val[15..0], aq, rl, false),
+                (WORD, _)    => mem_write_value(addr, 4, rs2_val[31..0], aq, rl, false),
+                (DOUBLE, 64) => mem_write_value(addr, 8, rs2_val,        aq, rl, false)
+              };
+              match (res) {
+                MemValue(true)  => RETIRE_SUCCESS,
+                MemValue(false) => internal_error("store got false from mem_write_value"),
+                MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL }
+              }
+            }
+          }
+        }
+      }
+  }
+}
+
+/* Put the illegal instructions last to use their wildcard match. */
+
+/* ****************************************************************** */
+
+union clause ast = ILLEGAL : word
+
+mapping clause encdec = ILLEGAL(s) <-> s
+
+function clause execute (ILLEGAL(s)) = { handle_illegal(); RETIRE_FAIL }
+
+/* ****************************************************************** */
+
+/* End definitions */
+end ast
+end execute
+end encdec
+end encdec_compressed
+
+val decode : bits(32) -> ast effect pure
+function decode bv = encdec(bv)
+
+/* The result of a fetch, which includes any possible error
+ * from an extension that interposes on the fetch operation.
+ */
+
+union FetchResult = {
+  F_Ext_Error : ext_fetch_addr_error,      /* For extensions */
+  F_Base      : word,                      /* Base ISA */
+  F_RVC       : half,                      /* Compressed ISA */
+  F_Error     : (ExceptionType, xlenbits)  /* standard exception and PC */
+}
+/* The default implementation of hooks for the step() and main() functions. */
+
+function ext_init() -> unit = ()
+
+function ext_fetch_hook(f : FetchResult) -> FetchResult = f
+
+function ext_pre_step_hook()  -> unit = ()
+function ext_post_step_hook() -> unit = ()
+/* Extensions may wish to interpose and transform decoded instructions,
+ * based on other machine state.  This is supported via a post-decode
+ * instruction hook, the default implementation of which is provided below.
+ */
+
+val ext_post_decode_hook : ast -> ast effect {rreg}
+function ext_post_decode_hook(x) = x
+
+val fetch : unit -> FetchResult effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
+function fetch() -> FetchResult =
+  /* fetch PC check for extensions: extensions return a transformed PC to fetch,
+   * but any exceptions use the untransformed PC.
+   */
+  match ext_fetch_check_pc(PC, PC) {
+    Ext_FetchAddr_Error(e)   => F_Ext_Error(e),
+    Ext_FetchAddr_OK(use_pc) => {
+      if   (use_pc[0] != bitzero | (use_pc[1] != bitzero))
+      then F_Error(E_Fetch_Addr_Align(), PC)
+      else match translateAddr(use_pc, Execute()) {
+        TR_Failure(e, _)     => F_Error(e, PC),
+        TR_Address(ppc, _) => {
+          match mem_read(Execute(), ppc, 4, false, false, false) {
+            MemException(e) => F_Error(e, PC),
+            MemValue(ibits)   => F_Base(ibits)
+            }
+          }
+        }
+      }
+    }
+    
+/* The emulator fetch-execute-interrupt dispatch loop. */
+
+/* returns whether to increment the step count in the trace */
+function step(step_no : int) -> bool = {
+  /* for step extensions */
+  ext_pre_step_hook();
+
+  let (retired, stepped) : (Retired, bool) =
+      /* the extension hook interposes on the fetch result */
+      let f : FetchResult = ext_fetch_hook(fetch()) in
+      match f {
+        /* extension error */
+        F_Ext_Error(e)   => {
+          ext_handle_fetch_check_error(e);
+          (RETIRE_FAIL, false)
+        },
+        /* standard error */
+        F_Error(e, addr) => {
+          handle_mem_exception(addr, e);
+          (RETIRE_FAIL, false)
+        },
+        F_Base(w) => {
+          let ast = decode(w);
+          nextPC = PC + 4;
+          (execute(ext_post_decode_hook(ast)), true)
+        }
+      };
+
+  tick_pc();
+
+  /* for step extensions */
+  ext_post_step_hook();
+
+  stepped
+}
+
+function loop () : unit -> unit = {
+  step_no : int = 0;
+  while (true) do {
+    let stepped = step(step_no);
+    if stepped then step_no = step_no + 1;
+  }
+}
+
+
+function main () : unit -> unit = {
+  // PC = __GetSlice_int(64, elf_entry(), 0);
+  PC = sail_zero_extend(0x1000, sizeof(xlen));
+  print_bits("PC = ", PC);
+
+  try {
+    loop()
+  } catch {
+    Error_not_implemented(s) => print_string("Error: Not implemented: ", s),
+    Error_internal_error() => print("Error: internal error")
+  }
+}
diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail
index d02c49d..b3fa37d 100644
--- a/model/riscv_mem.sail
+++ b/model/riscv_mem.sail
@@ -7,7 +7,7 @@
  * metadata in addition to raw memory data.
  *
  * The external API for this module is
- *   {mem_read, mem_write_ea, mem_write_value_meta, mem_write_value}
+ *   {mem_read, mem_read_meta, mem_write_ea, mem_write_value_meta, mem_write_value}
  * where mem_write_value is a special case of mem_write_value_meta that uses
  * a default value of the metadata.
  *
@@ -19,43 +19,53 @@
 function is_aligned_addr forall 'n. (addr : xlenbits, width : atom('n)) -> bool =
   unsigned(addr) % width == 0
 
-// only used for actual memory regions, to avoid MMIO effects
-function phys_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), paddr : xlenbits, width : atom('n), aq : bool, rl: bool, res : bool) -> MemoryOpResult(bits(8 * 'n)) = {
-  let result = (match (aq, rl, res) {
-    (false, false, false) => Some(read_ram(Read_plain, paddr, width)),
-    (true, false, false)  => Some(read_ram(Read_RISCV_acquire, paddr, width)),
-    (true, true, false)   => Some(read_ram(Read_RISCV_strong_acquire, paddr, width)),
-    (false, false, true)  => Some(read_ram(Read_RISCV_reserved, paddr, width)),
-    (true, false, true)   => Some(read_ram(Read_RISCV_reserved_acquire, paddr, width)),
-    (true, true, true)    => Some(read_ram(Read_RISCV_reserved_strong_acquire, paddr, width)),
+function read_kind_of_flags (aq : bool, rl : bool, res : bool) -> option(read_kind) =
+  match (aq, rl, res) {
+    (false, false, false) => Some(Read_plain),
+    (true, false, false)  => Some(Read_RISCV_acquire),
+    (true, true, false)   => Some(Read_RISCV_strong_acquire),
+    (false, false, true)  => Some(Read_RISCV_reserved),
+    (true, false, true)   => Some(Read_RISCV_reserved_acquire),
+    (true, true, true)    => Some(Read_RISCV_reserved_strong_acquire),
     (false, true, false)  => None(), /* should these be instead throwing error_not_implemented as below? */
     (false, true, true)   => None()
-  }) : option(bits(8 * 'n));
+  }
+
+// only used for actual memory regions, to avoid MMIO effects
+function phys_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), paddr : xlenbits, width : atom('n), aq : bool, rl: bool, res : bool, meta : bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) = {
+  let result = (match read_kind_of_flags(aq, rl, res) {
+    Some(rk) => Some(read_ram(rk, paddr, width, meta)),
+    None()   => None()
+  }) : option((bits(8 * 'n), mem_meta));
   match (t, result) {
     (Execute(),  None()) => MemException(E_Fetch_Access_Fault()),
     (Read(Data), None()) => MemException(E_Load_Access_Fault()),
     (_,          None()) => MemException(E_SAMO_Access_Fault()),
-    (_,         Some(v)) => { if   get_config_print_mem()
+    (_,      Some(v, m)) => { if   get_config_print_mem()
                               then print_mem("mem[" ^ to_str(t) ^ "," ^ BitStr(paddr) ^ "] -> " ^ BitStr(v));
-                              MemValue(v) }
+                              MemValue(v, m) }
   }
 }
 
 /* dispatches to MMIO regions or physical memory regions depending on physical memory map */
-function checked_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), paddr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool) -> MemoryOpResult(bits(8 * 'n)) =
+function checked_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), paddr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool, meta : bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) =
   if   within_mmio_readable(paddr, width)
-  then mmio_read(paddr, width)
+  then MemoryOpResult_add_meta(mmio_read(t, paddr, width), default_meta)
   else if within_phys_mem(paddr, width)
-  then phys_mem_read(t, paddr, width, aq, rl, res)
-  else MemException(E_Load_Access_Fault())
+  then phys_mem_read(t, paddr, width, aq, rl, res, meta)
+  else match t {
+    Execute()  => MemException(E_Fetch_Access_Fault()),
+    Read(Data) => MemException(E_Load_Access_Fault()),
+    _          => MemException(E_SAMO_Access_Fault())
+  }
 
 /* PMP checks if enabled */
-function pmp_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), paddr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool) -> MemoryOpResult(bits(8 * 'n)) =
+function pmp_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), paddr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool, meta : bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) =
   if   (~ (plat_enable_pmp ()))
-  then checked_mem_read(t, paddr, width, aq, rl, res)
+  then checked_mem_read(t, paddr, width, aq, rl, res, meta)
   else {
     match pmpCheck(paddr, width, t, effectivePrivilege(mstatus, cur_privilege)) {
-      None()  => checked_mem_read(t, paddr, width, aq, rl, res),
+      None()  => checked_mem_read(t, paddr, width, aq, rl, res, meta),
       Some(e) => MemException(e)
     }
   }
@@ -70,7 +80,8 @@ function rvfi_read (addr, width, result) = {
     MemValue(v) => if   width <= 8
                    then { rvfi_exec->rvfi_mem_rdata() = sail_zero_extend(v,64);
                           rvfi_exec->rvfi_mem_rmask() = rvfi_encode_width_mask(width) }
-                   else (),
+                   else { rvfi_exec->rvfi_mem_rdata() = v[63..0];
+                          rvfi_exec->rvfi_mem_rmask() = 0xFF},
     MemException(_) => ()
   };
 }
@@ -81,24 +92,29 @@ $endif
 
 /* NOTE: The rreg effect is due to MMIO. */
 $ifdef RVFI_DII
-val mem_read : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) effect {wreg, rmem, rreg, escape}
+val mem_read      : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool)       -> MemoryOpResult(bits(8 * 'n))             effect {wreg, rmem, rmemt, rreg, escape}
+val mem_read_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) effect {wreg, rmem, rmemt, rreg, escape}
 $else
-val mem_read : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rreg, escape}
+val mem_read      : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool)       -> MemoryOpResult(bits(8 * 'n))             effect {rmem, rmemt, rreg, escape}
+val mem_read_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) effect {rmem, rmemt, rreg, escape}
 $endif
 
-function mem_read (typ, paddr, width, aq, rl, res) = {
- let result : MemoryOpResult(bits(8 * 'n)) =
-  if (aq | res) & (~ (is_aligned_addr(paddr, width)))
-  then MemException(E_Load_Addr_Align())
-  else match (aq, rl, res) {
-    (false, true,  false) => throw(Error_not_implemented("load.rl")),
-    (false, true,  true)  => throw(Error_not_implemented("lr.rl")),
-    (_, _, _)             => pmp_mem_read(typ, paddr, width, aq, rl, res)
-  };
- rvfi_read(paddr, width, result);
- result
+function mem_read_meta (typ, paddr, width, aq, rl, res, meta) = {
+  let result : MemoryOpResult((bits(8 * 'n), mem_meta)) =
+    if (aq | res) & (~ (is_aligned_addr(paddr, width)))
+    then MemException(E_Load_Addr_Align())
+    else match (aq, rl, res) {
+      (false, true,  false) => throw(Error_not_implemented("load.rl")),
+      (false, true,  true)  => throw(Error_not_implemented("lr.rl")),
+      (_, _, _)             => pmp_mem_read(typ, paddr, width, aq, rl, res, meta)
+    };
+  rvfi_read(paddr, width, MemoryOpResult_drop_meta(result));
+  result
 }
 
+function mem_read (typ, paddr, width, aq, rl, res) =
+  MemoryOpResult_drop_meta(mem_read_meta(typ, paddr, width, aq, rl, res, false))
+
 val mem_write_ea : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(unit) effect {eamem, escape}
 
 function mem_write_ea (addr, width, aq, rl, con) = {
@@ -123,6 +139,9 @@ function rvfi_write (addr, width, value) = {
   if width <= 8 then {
     rvfi_exec->rvfi_mem_wdata() = sail_zero_extend(value,64);
     rvfi_exec->rvfi_mem_wmask() = rvfi_encode_width_mask(width);
+  } else {
+    rvfi_exec->rvfi_mem_wdata() = value[63..0];
+    rvfi_exec->rvfi_mem_wmask() = 0xFF;
   }
 }
 $else
diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail
index 7cc63cc..7e07cf1 100644
--- a/model/riscv_platform.sail
+++ b/model/riscv_platform.sail
@@ -142,8 +142,8 @@ let MTIMECMP_BASE_HI : xlenbits = EXTZ(0x04004)
 let MTIME_BASE       : xlenbits = EXTZ(0x0bff8)
 let MTIME_BASE_HI    : xlenbits = EXTZ(0x0bffc)
 
-val clint_load : forall 'n, 'n > 0. (xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rreg}
-function clint_load(addr, width) = {
+val clint_load : forall 'n, 'n > 0. (AccessType(ext_access_type), xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rreg}
+function clint_load(t, addr, width) = {
   let addr = addr - plat_clint_base ();
   /* FIXME: For now, only allow exact aligned access. */
   if addr == MSIP_BASE & ('n == 8 | 'n == 4)
@@ -194,7 +194,11 @@ function clint_load(addr, width) = {
   else {
     if   get_config_print_platform()
     then print_platform("clint[" ^ BitStr(addr) ^ "] -> <not-mapped>");
-    MemException(E_Load_Access_Fault())
+    match t {
+      Execute()  => MemException(E_Fetch_Access_Fault()),
+      Read(Data) => MemException(E_Load_Access_Fault()),
+      _          => MemException(E_SAMO_Access_Fault())
+    }
   }
 }
 
@@ -274,8 +278,8 @@ register htif_exit_code : bits(64)
  * dispatched the address.
  */
 
-val htif_load : forall 'n, 'n > 0. (xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rreg}
-function htif_load(paddr, width) = {
+val htif_load : forall 'n, 'n > 0. (AccessType(ext_access_type), xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rreg}
+function htif_load(t, paddr, width) = {
   if   get_config_print_platform()
   then print_platform("htif[" ^ BitStr(paddr) ^ "] -> " ^ BitStr(htif_tohost));
   /* FIXME: For now, only allow the expected access widths. */
@@ -285,7 +289,11 @@ function htif_load(paddr, width) = {
   then    MemValue(sail_zero_extend(htif_tohost[31..0], 32))  /* FIXME: Redundant zero_extend currently required by Lem backend */
   else if width == 4 & paddr == plat_htif_tohost() + 4
   then    MemValue(sail_zero_extend(htif_tohost[63..32], 32)) /* FIXME: Redundant zero_extend currently required by Lem backend */
-  else    MemException(E_Load_Access_Fault())
+  else match t {
+    Execute()  => MemException(E_Fetch_Access_Fault()),
+    Read(Data) => MemException(E_Load_Access_Fault()),
+    _          => MemException(E_SAMO_Access_Fault())
+  }
 }
 
 /* The rreg,wreg effects are an artifact of using 'register' to implement device state. */
@@ -351,12 +359,16 @@ $else
 function within_mmio_writable forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : atom('n)) -> bool = false
 $endif
 
-function mmio_read forall 'n, 0 < 'n <= max_mem_access . (paddr : xlenbits, width : atom('n)) -> MemoryOpResult(bits(8 * 'n)) =
+function mmio_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), paddr : xlenbits, width : atom('n)) -> MemoryOpResult(bits(8 * 'n)) =
   if   within_clint(paddr, width)
-  then clint_load(paddr, width)
+  then clint_load(t, paddr, width)
   else if within_htif_readable(paddr, width) & (1 <= 'n)
-  then htif_load(paddr, width)
-  else MemException(E_Load_Access_Fault())
+  then htif_load(t, paddr, width)
+  else match t {
+    Execute()  => MemException(E_Fetch_Access_Fault()),
+    Read(Data) => MemException(E_Load_Access_Fault()),
+    _          => MemException(E_SAMO_Access_Fault())
+  }
 
 function mmio_write forall 'n, 0 <'n <= max_mem_access . (paddr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> MemoryOpResult(bool) =
   if   within_clint(paddr, width)
diff --git a/model/riscv_pmp_control.sail b/model/riscv_pmp_control.sail
index 4f43a6c..1970afc 100644
--- a/model/riscv_pmp_control.sail
+++ b/model/riscv_pmp_control.sail
@@ -40,7 +40,7 @@ function pmpCheckRWX(ent, acc) = {
 val pmpCheckPerms: (Pmpcfg_ent, AccessType(ext_access_type), Privilege) -> bool
 function pmpCheckPerms(ent, acc, priv) = {
   match priv {
-    Machine => if   ent.L() == 0b1
+    Machine => if   pmpLocked(ent)
                then pmpCheckRWX(ent, acc)
                else true,
     _       => pmpCheckRWX(ent, acc)
diff --git a/model/riscv_pmp_regs.sail b/model/riscv_pmp_regs.sail
index 978ef18..a823a06 100644
--- a/model/riscv_pmp_regs.sail
+++ b/model/riscv_pmp_regs.sail
@@ -85,9 +85,15 @@ function pmpReadCfgReg(n) = {
        }
 }
 
-/* Helper to handle locked entries */
+/* Helpers to handle locked entries */
+function pmpLocked(cfg: Pmpcfg_ent) -> bool =
+   cfg.L() == 0b1
+
+function pmpTORLocked(cfg: Pmpcfg_ent) -> bool =
+   (cfg.L() == 0b1) & (pmpAddrMatchType_of_bits(cfg.A()) == TOR)
+
 function pmpWriteCfg(cfg: Pmpcfg_ent, v: bits(8)) -> Pmpcfg_ent =
-  if cfg.L() == 0b1 then cfg else Mk_Pmpcfg_ent(v)
+  if pmpLocked(cfg) then cfg else Mk_Pmpcfg_ent(v)
 
 val pmpWriteCfgReg : forall 'n, 0 <= 'n < 4 . (atom('n), xlenbits) -> unit effect {rreg, wreg}
 function pmpWriteCfgReg(n, v) = {
@@ -137,7 +143,7 @@ function pmpWriteCfgReg(n, v) = {
        }
 }
 
-function pmpWriteAddr(cfg: Pmpcfg_ent, reg: xlenbits, v: xlenbits) -> xlenbits =
+function pmpWriteAddr(locked: bool, tor_locked: bool, reg: xlenbits, v: xlenbits) -> xlenbits =
   if   sizeof(xlen) == 32
-  then { if cfg.L() == 0b1 then reg else v }
-  else { if cfg.L() == 0b1 then reg else EXTZ(v[53..0]) }
+  then { if (locked | tor_locked) then reg else v }
+  else { if (locked | tor_locked) then reg else EXTZ(v[53..0]) }
diff --git a/model/riscv_softfloat_interface.sail b/model/riscv_softfloat_interface.sail
new file mode 100644
index 0000000..1cc16a9
--- /dev/null
+++ b/model/riscv_softfloat_interface.sail
@@ -0,0 +1,260 @@
+/* **************************************************************** */
+/* This file lists all the external Berkeley softfloat functions    */
+/* invoked from the SAIL spec for RISC-V F and D extensions         */
+/* (in:    riscv_insts_fdext.sail)                                  */
+/*                                                                  */
+/* Each of these functions corresponds to one in 'SoftFloat.hs'     */
+/* in    https://github.com/GaloisInc/softfloat-hs.git              */
+/* written by Ben Selfridge,                                        */
+/* which is a set of pure-functional Haskell wrappers on the        */
+/* Berkely softfloat C library written by John Hauser.              */
+
+/* For now, the bodies of all these functions are placeholders      */
+/* while we develop    riscv_insts_fdext.sail                       */
+/* They should be replaced with external calls to Berkeley softfloat*/
+/* functions in a similar manner to the Haskell softfloat wrappers. */
+
+/* **************************************************************** */
+/* All arguments and results have one of these types                */
+
+type bits_rm     = bits(3)    /* Rounding mode */
+type bits_fflags = bits(5)    /* Accrued exceptions: NV,DZ,OF,UF,NX */
+type bits_S      = bits(32)   /* Single-precision float value */
+type bits_D      = bits(64)   /* Double-precision float value */
+
+type bits_W      = bits(32)   /* Signed integer */
+type bits_WU     = bits(32)   /* Unsigned integer */
+
+type bits_L      = bits(64)   /* Signed integer */
+type bits_LU     = bits(64)   /* Unsigned integer */
+
+/* ***************************************************************** */
+/* Internal registers to pass results across the softfloat interface
+ * to avoid return types involving structures.
+ */
+register float_result : bits(64)
+register float_fflags : bits(64)
+
+/* **************************************************************** */
+/* ADD/SUB/MUL/DIV                                                  */
+
+val     extern_f32Add = {c: "softfloat_f32add", ocaml: "Softfloat.f32_add", lem: "softfloat_f32_add"} : (bits_rm, bits_S, bits_S) -> unit
+val      riscv_f32Add : (bits_rm, bits_S, bits_S) -> (bits_fflags, bits_S) effect {rreg}
+function riscv_f32Add (rm, v1, v2) = {
+  extern_f32Add(rm, v1, v2);
+  (float_fflags[4 .. 0], float_result[31 .. 0])
+}
+
+val     extern_f32Sub = {c: "softfloat_f32sub", ocaml: "Softfloat.f32_sub", lem: "softfloat_f32_sub"} : (bits_rm, bits_S, bits_S) -> unit
+val      riscv_f32Sub : (bits_rm, bits_S, bits_S) -> (bits_fflags, bits_S) effect {rreg}
+function riscv_f32Sub (rm, v1, v2) = {
+  extern_f32Sub(rm, v1, v2);
+  (float_fflags[4 .. 0], float_result[31 .. 0])
+}
+
+val     extern_f32Mul = {c: "softfloat_f32mul", ocaml: "Softfloat.f32_mul", lem: "softfloat_f32_mul"} : (bits_rm, bits_S, bits_S) -> unit
+val      riscv_f32Mul : (bits_rm, bits_S, bits_S) -> (bits_fflags, bits_S) effect {rreg}
+function riscv_f32Mul (rm, v1, v2) = {
+  extern_f32Mul(rm, v1, v2);
+  (float_fflags[4 .. 0], float_result[31 .. 0])
+}
+
+val     extern_f32Div = {c: "softfloat_f32div", ocaml: "Softfloat.f32_div", lem: "softfloat_f32_div"} : (bits_rm, bits_S, bits_S) -> unit
+val      riscv_f32Div : (bits_rm, bits_S, bits_S) -> (bits_fflags, bits_S) effect {rreg}
+function riscv_f32Div (rm, v1, v2) = {
+  extern_f32Div(rm, v1, v2);
+  (float_fflags[4 .. 0], float_result[31 .. 0])
+}
+
+val     extern_f64Add = {c: "softfloat_f64add", ocaml: "Softfloat.f64_add", lem: "softfloat_f64_add"} : (bits_rm, bits_D, bits_D) -> unit
+val      riscv_f64Add : (bits_rm, bits_D, bits_D) -> (bits_fflags, bits_D) effect {rreg}
+function riscv_f64Add (rm, v1, v2) = {
+  extern_f64Add(rm, v1, v2);
+  (float_fflags[4 .. 0], float_result)
+}
+
+val     extern_f64Sub = {c: "softfloat_f64sub", ocaml: "Softfloat.f64_sub", lem: "softfloat_f64_sub"} : (bits_rm, bits_D, bits_D) -> unit
+val      riscv_f64Sub : (bits_rm, bits_D, bits_D) -> (bits_fflags, bits_D) effect {rreg}
+function riscv_f64Sub (rm, v1, v2) = {
+  extern_f64Sub(rm, v1, v2);
+  (float_fflags[4 .. 0], float_result)
+}
+
+val     extern_f64Mul = {c: "softfloat_f64mul", ocaml: "Softfloat.f64_mul", lem: "softfloat_f64_mul"} : (bits_rm, bits_D, bits_D) -> unit
+val      riscv_f64Mul : (bits_rm, bits_D, bits_D) -> (bits_fflags, bits_D) effect {rreg}
+function riscv_f64Mul (rm, v1, v2) = {
+  extern_f64Mul(rm, v1, v2);
+  (float_fflags[4 .. 0], float_result)
+}
+
+val     extern_f64Div = {c: "softfloat_f64div", ocaml: "Softfloat.f64_div", lem: "softfloat_f64_div"} : (bits_rm, bits_D, bits_D) -> unit
+val      riscv_f64Div : (bits_rm, bits_D, bits_D) -> (bits_fflags, bits_D) effect {rreg}
+function riscv_f64Div (rm, v1, v2) = {
+  extern_f64Div(rm, v1, v2);
+  (float_fflags[4 .. 0], float_result)
+}
+
+/* **************************************************************** */
+/* MULTIPLY-ADD                                                     */
+
+val     extern_f32MulAdd = {c: "softfloat_f32muladd", ocaml: "Softfloat.f32_muladd", lem: "softfloat_f32_muladd"} : (bits_rm, bits_S, bits_S, bits_S) -> unit
+val      riscv_f32MulAdd : (bits_rm, bits_S, bits_S, bits_S) -> (bits_fflags, bits_S) effect {rreg}
+function riscv_f32MulAdd (rm, v1, v2, v3) = {
+  extern_f32MulAdd(rm, v1, v2, v3);
+  (float_fflags[4 .. 0], float_result[31 .. 0])
+}
+
+val     extern_f64MulAdd = {c: "softfloat_f64muladd", ocaml: "Softfloat.f64_muladd", lem: "softfloat_f64_muladd"} : (bits_rm, bits_D, bits_D, bits_D) -> unit
+val      riscv_f64MulAdd : (bits_rm, bits_D, bits_D, bits_D) -> (bits_fflags, bits_D) effect {rreg}
+function riscv_f64MulAdd (rm, v1, v2, v3) = {
+  extern_f64MulAdd(rm, v1, v2, v3);
+  (float_fflags[4 .. 0], float_result)
+}
+
+/* **************************************************************** */
+/* SQUARE ROOT                                                      */
+
+val     extern_f32Sqrt = {c: "softfloat_f32sqrt", ocaml: "Softfloat.f32_sqrt", lem: "softfloat_f32_sqrt"} : (bits_rm, bits_S) -> unit
+val      riscv_f32Sqrt : (bits_rm, bits_S) -> (bits_fflags, bits_S) effect {rreg}
+function riscv_f32Sqrt (rm, v) = {
+  extern_f32Sqrt(rm, v);
+  (float_fflags[4 .. 0], float_result[31 .. 0])
+}
+
+val     extern_f64Sqrt = {c: "softfloat_f64sqrt", ocaml: "Softfloat.f64_sqrt", lem: "softfloat_f64_sqrt"} : (bits_rm, bits_D) -> unit
+val      riscv_f64Sqrt : (bits_rm, bits_D) -> (bits_fflags, bits_D) effect {rreg}
+function riscv_f64Sqrt (rm, v) = {
+  extern_f64Sqrt(rm, v);
+  (float_fflags[4 .. 0], float_result)
+}
+
+/* **************************************************************** */
+/* CONVERSIONS                                                      */
+
+val     extern_f32ToI32 = {c: "softfloat_f32toi32", ocaml: "Softfloat.f32_to_i32", lem: "softfloat_f32_to_i32"} : (bits_rm, bits_S) -> unit
+val      riscv_f32ToI32 : (bits_rm, bits_S) -> (bits_fflags, bits_W) effect {rreg}
+function riscv_f32ToI32 (rm, v) = {
+  extern_f32ToI32(rm, v);
+  (float_fflags[4 .. 0], float_result[31 .. 0])
+}
+
+val     extern_f32ToUi32 = {c: "softfloat_f32toui32", ocaml: "Softfloat.f32_to_ui32", lem: "softfloat_f32_to_ui32"} : (bits_rm, bits_S) -> unit
+val      riscv_f32ToUi32 : (bits_rm, bits_S) -> (bits_fflags, bits_WU) effect {rreg}
+function riscv_f32ToUi32 (rm, v) = {
+  extern_f32ToUi32(rm, v);
+  (float_fflags[4 .. 0], float_result[31 .. 0])
+}
+
+val     extern_i32ToF32 = {c: "softfloat_i32tof32", ocaml: "Softfloat.i32_to_f32", lem: "softfloat_i32_to_f32"} : (bits_rm, bits_W) -> unit
+val      riscv_i32ToF32 : (bits_rm, bits_W) -> (bits_fflags, bits_S) effect {rreg}
+function riscv_i32ToF32 (rm, v) = {
+  extern_i32ToF32(rm, v);
+  (float_fflags[4 .. 0], float_result[31 .. 0])
+}
+
+val     extern_ui32ToF32 = {c: "softfloat_ui32tof32", ocaml: "Softfloat.ui32_to_f32", lem: "softfloat_ui32_to_f32"} : (bits_rm, bits_WU) -> unit
+val      riscv_ui32ToF32 : (bits_rm, bits_WU) -> (bits_fflags, bits_S) effect {rreg}
+function riscv_ui32ToF32 (rm, v) = {
+  extern_ui32ToF32(rm, v);
+  (float_fflags[4 .. 0], float_result[31 .. 0])
+}
+
+val     extern_f32ToI64 = {c: "softfloat_f32toi64", ocaml: "Softfloat.f32_to_i64", lem: "softfloat_f32_to_i64"} : (bits_rm, bits_S) -> unit
+val      riscv_f32ToI64 : (bits_rm, bits_S) -> (bits_fflags, bits_L) effect {rreg}
+function riscv_f32ToI64 (rm, v) = {
+  extern_f32ToI64(rm, v);
+  (float_fflags[4 .. 0], float_result)
+}
+
+val     extern_f32ToUi64 = {c: "softfloat_f32toui64", ocaml: "Softfloat.f32_to_ui64", lem: "softfloat_f32_to_ui64"} : (bits_rm, bits_S) -> unit
+val      riscv_f32ToUi64 : (bits_rm, bits_S) -> (bits_fflags, bits_LU) effect {rreg}
+function riscv_f32ToUi64 (rm, v) = {
+  extern_f32ToUi64(rm, v);
+  (float_fflags[4 .. 0], float_result)
+}
+
+val     extern_i64ToF32 = {c: "softfloat_i64tof32", ocaml: "Softfloat.i64_to_f32", lem: "softfloat_i64_to_f32"} : (bits_rm, bits_L) -> unit
+val      riscv_i64ToF32 : (bits_rm, bits_L) -> (bits_fflags, bits_S) effect {rreg}
+function riscv_i64ToF32 (rm, v) = {
+  extern_i64ToF32(rm, v);
+  (float_fflags[4 .. 0], float_result[31 .. 0])
+}
+
+val     extern_ui64ToF32 = {c: "softfloat_ui64tof32", ocaml: "Softfloat.ui64_to_f32", lem: "softfloat_ui64_to_f32"} : (bits_rm, bits_L) -> unit
+val      riscv_ui64ToF32 : (bits_rm, bits_LU) -> (bits_fflags, bits_S) effect {rreg}
+function riscv_ui64ToF32 (rm, v) = {
+  extern_ui64ToF32(rm, v);
+  (float_fflags[4 .. 0], float_result[31 .. 0])
+}
+
+val     extern_f64ToI32 = {c: "softfloat_f64toi32", ocaml: "Softfloat.f64_to_i32", lem: "softfloat_f64_to_i32"} : (bits_rm, bits_D) -> unit
+val      riscv_f64ToI32 : (bits_rm, bits_D) -> (bits_fflags, bits_W) effect {rreg}
+function riscv_f64ToI32 (rm, v) = {
+  extern_f64ToI32(rm, v);
+  (float_fflags[4 .. 0], float_result[31 .. 0])
+}
+
+val     extern_f64ToUi32 = {c: "softfloat_f64toui32", ocaml: "Softfloat.f64_to_ui32", lem: "softfloat_f64_to_ui32"} : (bits_rm, bits_D) -> unit
+val      riscv_f64ToUi32 : (bits_rm, bits_D) -> (bits_fflags, bits_WU) effect {rreg}
+function riscv_f64ToUi32 (rm, v) = {
+  extern_f64ToUi32(rm, v);
+  (float_fflags[4 .. 0], float_result[31 .. 0])
+}
+
+val     extern_i32ToF64 = {c: "softfloat_i32tof64", ocaml: "Softfloat.i32_to_f64", lem: "softfloat_i32_to_f64"} : (bits_rm, bits_W) -> unit
+val      riscv_i32ToF64 : (bits_rm, bits_W) -> (bits_fflags, bits_D) effect {rreg}
+function riscv_i32ToF64 (rm, v) = {
+  extern_i32ToF64(rm, v);
+  (float_fflags[4 .. 0], float_result)
+}
+
+val     extern_ui32ToF64 = {c: "softfloat_ui32tof64", ocaml: "Softfloat.ui32_to_f64", lem: "softfloat_ui32_to_f64"} : (bits_rm, bits_WU) -> unit
+val      riscv_ui32ToF64 : (bits_rm, bits_WU) -> (bits_fflags, bits_D) effect {rreg}
+function riscv_ui32ToF64 (rm, v) = {
+  extern_ui32ToF64(rm, v);
+  (float_fflags[4 .. 0], float_result)
+}
+
+val     extern_f64ToI64 = {c: "softfloat_f64toi64", ocaml: "Softfloat.f64_to_i64", lem: "softfloat_f64_to_i64"} : (bits_rm, bits_D) -> unit
+val      riscv_f64ToI64 : (bits_rm, bits_D) -> (bits_fflags, bits_L) effect {rreg}
+function riscv_f64ToI64 (rm, v) = {
+  extern_f64ToI64(rm, v);
+  (float_fflags[4 .. 0], float_result)
+}
+
+val     extern_f64ToUi64 = {c: "softfloat_f64toui64", ocaml: "Softfloat.f64_to_ui64", lem: "softfloat_f64_to_ui64"} : (bits_rm, bits_D) -> unit
+val      riscv_f64ToUi64 : (bits_rm, bits_D) -> (bits_fflags, bits_LU) effect {rreg}
+function riscv_f64ToUi64 (rm, v) = {
+  extern_f64ToUi64(rm, v);
+  (float_fflags[4 .. 0], float_result)
+}
+
+val     extern_i64ToF64 = {c: "softfloat_i64tof64", ocaml: "Softfloat.i64_to_f64", lem: "softfloat_i64_to_f64"} : (bits_rm, bits_L) -> unit
+val      riscv_i64ToF64 : (bits_rm, bits_L) -> (bits_fflags, bits_D) effect {rreg}
+function riscv_i64ToF64 (rm, v) = {
+  extern_i64ToF64(rm, v);
+  (float_fflags[4 .. 0], float_result)
+}
+
+val     extern_ui64ToF64 = {c: "softfloat_ui64tof64", ocaml: "Softfloat.ui64_to_f64", lem: "softfloat_ui64_to_f64"} : (bits_rm, bits_LU) -> unit
+val      riscv_ui64ToF64 : (bits_rm, bits_LU) -> (bits_fflags, bits_D) effect {rreg}
+function riscv_ui64ToF64 (rm, v) = {
+  extern_ui64ToF64(rm, v);
+  (float_fflags[4 .. 0], float_result)
+}
+
+val     extern_f32ToF64 = {c: "softfloat_f32tof64", ocaml: "Softfloat.f32_to_f64", lem: "softfloat_f32_to_f64"} : (bits_rm, bits_S) -> unit
+val      riscv_f32ToF64 : (bits_rm, bits_S) -> (bits_fflags, bits_D) effect {rreg}
+function riscv_f32ToF64 (rm, v) = {
+  extern_f32ToF64(rm, v);
+  (float_fflags[4 .. 0], float_result)
+}
+
+val     extern_f64ToF32 = {c: "softfloat_f64tof32", ocaml: "Softfloat.f64_to_f32", lem: "softfloat_f64_to_f32"} : (bits_rm, bits_D) -> unit
+val      riscv_f64ToF32 : (bits_rm, bits_D) -> (bits_fflags, bits_S) effect {rreg}
+function riscv_f64ToF32 (rm, v) = {
+  extern_f64ToF32(rm, v);
+  (float_fflags[4 .. 0], float_result[31 .. 0])
+}
+
+/* **************************************************************** */
diff --git a/model/riscv_step_rvfi.sail b/model/riscv_step_rvfi.sail
index 0ab482a..dd24365 100644
--- a/model/riscv_step_rvfi.sail
+++ b/model/riscv_step_rvfi.sail
@@ -12,6 +12,7 @@ function ext_post_step_hook() -> unit = {
 val ext_init : unit -> unit effect {wreg}
 function ext_init() = {
   init_base_regs();
+  init_fdext_regs();
   /* these are here so that the C backend doesn't prune them out. */
   rvfi_set_instr_packet(0x0000000000000000);
   print_bits("", rvfi_get_cmd());
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index 8162cb8..d906f5e 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -454,6 +454,14 @@ function init_sys() -> unit = {
   misa->U()   = 0b1;                            /* user-mode */
   misa->S()   = 0b1;                            /* supervisor-mode */
 
+  /* On RV64, we currently support either both F and D, or neither.
+   * On RV32, we currently only support F.
+   */
+  misa->F()   = bool_to_bits(sys_enable_fdext());      /* single-precision */
+  misa->D()   = if   sizeof(xlen) == 64
+                then bool_to_bits(sys_enable_fdext())  /* double-precision */
+                else 0b0;
+
   mstatus = set_mstatus_SXL(mstatus, misa.MXL());
   mstatus = set_mstatus_UXL(mstatus, misa.MXL());
   mstatus->SD()   = 0b0;
@@ -489,3 +497,15 @@ union MemoryOpResult ('a : Type) = {
   MemValue     : 'a,
   MemException : ExceptionType
 }
+
+val MemoryOpResult_add_meta : forall ('t : Type). (MemoryOpResult('t), mem_meta) -> MemoryOpResult(('t, mem_meta))
+function MemoryOpResult_add_meta(r, m) = match r {
+  MemValue(v)     => MemValue(v, m),
+  MemException(e) => MemException(e)
+}
+
+val MemoryOpResult_drop_meta : forall ('t : Type). MemoryOpResult(('t, mem_meta)) -> MemoryOpResult('t)
+function MemoryOpResult_drop_meta(r) = match r {
+  MemValue(v, m)  => MemValue(v),
+  MemException(e) => MemException(e)
+}
diff --git a/model/riscv_sys_exceptions.sail b/model/riscv_sys_exceptions.sail
index 94d869e..fa693e8 100644
--- a/model/riscv_sys_exceptions.sail
+++ b/model/riscv_sys_exceptions.sail
@@ -2,6 +2,11 @@
 
 type ext_exception = unit
 
+/* Is XRET from given mode permitted by extension? */
+function ext_check_xret_priv (p : Privilege) : Privilege -> bool = true
+/* Called if above check fails */
+function ext_fail_xret_priv () : unit -> unit = ()
+
 function handle_trap_extension(p : Privilege, pc : xlenbits, u : option(unit)) -> unit = ()
 
 /* used for traps and ECALL */
diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
index 722c1d5..3b808a6 100644
--- a/model/riscv_sys_regs.sail
+++ b/model/riscv_sys_regs.sail
@@ -74,6 +74,8 @@ register misa : Misa
 val sys_enable_writable_misa = {c: "sys_enable_writable_misa", ocaml: "Platform.enable_writable_misa", _: "sys_enable_writable_misa"} : unit -> bool
 /* whether misa.c was enabled at boot */
 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
 
 /* This function allows an extension to veto a write to Misa
    if it would violate an alignment restriction on
@@ -101,6 +103,7 @@ function haveMulDiv()  -> bool = misa.M() == 0b1
 function haveSupMode() -> bool = misa.S() == 0b1
 function haveUsrMode() -> bool = misa.U() == 0b1
 function haveNExt()    -> bool = misa.N() == 0b1
+/* see below for F and D extension tests */
 
 bitfield Mstatus : xlenbits = {
   SD   : xlen - 1,
@@ -177,7 +180,6 @@ function legalize_mstatus(o : Mstatus, v : xlenbits) -> Mstatus = {
    * 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.
    */
-  // let m = update_FS(m, extStatus_to_bits(Off));
 
   let dirty = extStatus_of_bits(m.FS()) == Dirty | extStatus_of_bits(m.XS()) == Dirty;
   let m = update_SD(m, bool_to_bits(dirty));
@@ -213,6 +215,10 @@ function in32BitMode() -> bool = {
   cur_Architecture() == RV32
 }
 
+/* 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)
+
 /* interrupt processing state */
 
 bitfield Minterrupts : xlenbits = {
diff --git a/model/riscv_termination_rv32.sail b/model/riscv_termination_rv32.sail
index 7cf8cb8..7318421 100644
--- a/model/riscv_termination_rv32.sail
+++ b/model/riscv_termination_rv32.sail
@@ -1 +1 @@
-termination_measure walk32(_,_,_,_,_,_,level,_) = level
+termination_measure walk32(_,_,_,_,_,_,level,_,_) = level
diff --git a/model/riscv_types.sail b/model/riscv_types.sail
index cacf0db..987743a 100644
--- a/model/riscv_types.sail
+++ b/model/riscv_types.sail
@@ -108,8 +108,6 @@ enum word_width = {BYTE, HALF, WORD, DOUBLE}
 
 /* architectural interrupt definitions */
 
-type exc_code = bits(8)
-
 enum InterruptType = {
   I_U_Software,
   I_S_Software,
@@ -181,7 +179,7 @@ function exceptionType_to_bits(e) =
     E_SAMO_Page_Fault()    => 0x0f,
 
     /* extensions */
-    E_Extension(e)         => 0x18    /* First code for a custom extension */
+    E_Extension(e)         => ext_exc_type_to_bits(e)
   }
 
 val num_of_ExceptionType : ExceptionType -> {'n, (0 <= 'n < xlen). int('n)}
@@ -205,7 +203,7 @@ function num_of_ExceptionType(e) =
     E_SAMO_Page_Fault()    => 15,
 
     /* extensions */
-    E_Extension(e)         => 24    /* First code for a custom extension */
+    E_Extension(e)         => num_of_ext_exc_type(e)
 
   }
 
@@ -230,7 +228,7 @@ function exceptionType_to_str(e) =
     E_SAMO_Page_Fault()    => "store/amo-page-fault",
 
     /* extensions */
-    E_Extension(e)         => "extension-exception"
+    E_Extension(e)         => ext_exc_type_to_str(e)
   }
 
 overload to_str = {exceptionType_to_str}
diff --git a/model/riscv_types_common.sail b/model/riscv_types_common.sail
new file mode 100644
index 0000000..9db34a0
--- /dev/null
+++ b/model/riscv_types_common.sail
@@ -0,0 +1 @@
+type exc_code = bits(8)
diff --git a/model/riscv_types_ext.sail b/model/riscv_types_ext.sail
index 5a05c39..6562981 100644
--- a/model/riscv_types_ext.sail
+++ b/model/riscv_types_ext.sail
@@ -20,3 +20,15 @@ type ext_exc_type = unit /* No exception extensions */
 /* Default translation of PTW errors into exception annotations */
 function ext_translate_exception(e : ext_ptw_error) -> ext_exc_type =
   e
+
+/* Default conversion of extension exceptions to bits */
+val ext_exc_type_to_bits : ext_exc_type -> exc_code
+function ext_exc_type_to_bits(e) = 0x18 /* First code for a custom extension */
+
+/* Default conversion of extension exceptions to integers */
+val num_of_ext_exc_type : ext_exc_type -> {'n, (0 <= 'n < xlen). int('n)}
+function num_of_ext_exc_type(e) = 24 /* First code for a custom extension */
+
+/* Default conversion of extension exceptions to strings */
+val ext_exc_type_to_str : ext_exc_type -> string
+function ext_exc_type_to_str(e) = "extension-exception"
diff --git a/model/riscv_vmem_rv32.sail b/model/riscv_vmem_rv32.sail
index 4ff7891..bea786c 100644
--- a/model/riscv_vmem_rv32.sail
+++ b/model/riscv_vmem_rv32.sail
@@ -26,7 +26,7 @@ function translationMode(priv) = {
 
 /* Top-level address translation dispatcher */
 
-val translateAddr : (xlenbits, AccessType(ext_access_type)) -> TR_Result(xlenbits, ExceptionType) effect {escape, rmem, rreg, wmv, wmvt, wreg}
+val translateAddr : (xlenbits, AccessType(ext_access_type)) -> TR_Result(xlenbits, ExceptionType) effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
 function translateAddr(vAddr, ac) = {
   let effPriv : Privilege = match ac {
     Execute() => cur_privilege,
diff --git a/model/riscv_vmem_rv64.sail b/model/riscv_vmem_rv64.sail
index c55e9dc..8b7dc44 100644
--- a/model/riscv_vmem_rv64.sail
+++ b/model/riscv_vmem_rv64.sail
@@ -33,7 +33,7 @@ function translationMode(priv) = {
 
 /* Top-level address translation dispatcher */
 
-val translateAddr : (xlenbits, AccessType(ext_access_type)) -> TR_Result(xlenbits, ExceptionType) effect {escape, rmem, rreg, wmv, wmvt, wreg}
+val translateAddr : (xlenbits, AccessType(ext_access_type)) -> TR_Result(xlenbits, ExceptionType) effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
 function translateAddr(vAddr, ac) = {
   let effPriv : Privilege = match ac {
     Execute() => cur_privilege,
diff --git a/model/riscv_vmem_sv32.sail b/model/riscv_vmem_sv32.sail
index e535915..1a27072 100644
--- a/model/riscv_vmem_sv32.sail
+++ b/model/riscv_vmem_sv32.sail
@@ -6,7 +6,7 @@
 
 function to_phys_addr(a : paddr32) -> xlenbits = a[31..0]
 
-val walk32 : (vaddr32, AccessType(ext_access_type), Privilege, bool, bool, paddr32, nat, bool, ext_ptw) -> PTW_Result(paddr32, SV32_PTE) effect {rmem, rreg, escape}
+val walk32 : (vaddr32, AccessType(ext_access_type), Privilege, bool, bool, paddr32, nat, bool, ext_ptw) -> PTW_Result(paddr32, SV32_PTE) effect {rmem, rmemt, rreg, escape}
 function walk32(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = {
   let va = Mk_SV32_Vaddr(vaddr);
   let pt_ofs : paddr32 = shiftl(EXTZ(shiftr(va.VPNi(), (level * SV32_LEVEL_BITS))[(SV32_LEVEL_BITS - 1) .. 0]),
@@ -37,13 +37,13 @@ function walk32(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = {
         PTW_Failure(PTW_Invalid_PTE(), ext_ptw)
       } else {
         if isPTEPtr(pbits, ext_pte) then {
-          if level == 0 then {
+          if level > 0 then {
+            /* walk down the pointer to the next level */
+            walk32(vaddr, ac, priv, mxr, do_sum, shiftl(EXTZ(pte.PPNi()), PAGESIZE_BITS), level - 1, is_global, ext_ptw)
+          } else {
             /* last-level PTE contains a pointer instead of a leaf */
 /*          print("walk32: last-level pte contains a ptr"); */
             PTW_Failure(PTW_Invalid_PTE(), ext_ptw)
-          } else {
-            /* walk down the pointer to the next level */
-            walk32(vaddr, ac, priv, mxr, do_sum, shiftl(EXTZ(pte.PPNi()), PAGESIZE_BITS), level - 1, is_global, ext_ptw)
           }
         } else { /* leaf PTE */
           match checkPTEPermission(ac, priv, mxr, do_sum, pattr, ext_pte, ext_ptw) {
@@ -115,7 +115,7 @@ function flush_TLB32(asid, addr) =
 
 /* address translation */
 
-val translate32 : (asid32, paddr32, vaddr32, AccessType(ext_access_type), Privilege, bool, bool, nat, ext_ptw) -> TR_Result(paddr32, PTW_Error) effect {rreg, wreg, wmv, wmvt, escape, rmem}
+val translate32 : (asid32, paddr32, vaddr32, AccessType(ext_access_type), Privilege, bool, bool, nat, ext_ptw) -> TR_Result(paddr32, PTW_Error) effect {rreg, wreg, wmv, wmvt, escape, rmem, rmemt}
 function translate32(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = {
   match lookup_TLB32(asid, vAddr) {
     Some(idx, ent) => {
diff --git a/model/riscv_vmem_sv39.sail b/model/riscv_vmem_sv39.sail
index a1edc4e..37c98a2 100644
--- a/model/riscv_vmem_sv39.sail
+++ b/model/riscv_vmem_sv39.sail
@@ -1,6 +1,6 @@
 /* Sv39 address translation for RV64. */
 
-val walk39 : (vaddr39, AccessType(ext_access_type), Privilege, bool, bool, paddr64, nat, bool, ext_ptw) -> PTW_Result(paddr64, SV39_PTE) effect {rmem, rreg, escape}
+val walk39 : (vaddr39, AccessType(ext_access_type), Privilege, bool, bool, paddr64, nat, bool, ext_ptw) -> PTW_Result(paddr64, SV39_PTE) effect {rmem, rmemt, rreg, escape}
 function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = {
   let va = Mk_SV39_Vaddr(vaddr);
   let pt_ofs : paddr64 = shiftl(EXTZ(shiftr(va.VPNi(), (level * SV39_LEVEL_BITS))[(SV39_LEVEL_BITS - 1) .. 0]),
@@ -31,13 +31,13 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = {
         PTW_Failure(PTW_Invalid_PTE(), ext_ptw)
       } else {
         if isPTEPtr(pbits, ext_pte) then {
-          if level == 0 then {
+          if level > 0 then {
+            /* walk down the pointer to the next level */
+            walk39(vaddr, ac, priv, mxr, do_sum, shiftl(EXTZ(pte.PPNi()), PAGESIZE_BITS), level - 1, is_global, ext_ptw)
+          } else {
             /* last-level PTE contains a pointer instead of a leaf */
 /*          print("walk39: last-level pte contains a ptr"); */
             PTW_Failure(PTW_Invalid_PTE(), ext_ptw)
-          } else {
-            /* walk down the pointer to the next level */
-            walk39(vaddr, ac, priv, mxr, do_sum, shiftl(EXTZ(pte.PPNi()), PAGESIZE_BITS), level - 1, is_global, ext_ptw)
           }
         } else { /* leaf PTE */
           match checkPTEPermission(ac, priv, mxr, do_sum, pattr, ext_pte, ext_ptw) {
@@ -109,7 +109,7 @@ function flush_TLB39(asid, addr) =
 
 /* address translation */
 
-val translate39 : (asid64, paddr64, vaddr39, AccessType(ext_access_type), Privilege, bool, bool, nat, ext_ptw) -> TR_Result(paddr64, PTW_Error) effect {rreg, wreg, wmv, wmvt, escape, rmem}
+val translate39 : (asid64, paddr64, vaddr39, AccessType(ext_access_type), Privilege, bool, bool, nat, ext_ptw) -> TR_Result(paddr64, PTW_Error) effect {rreg, wreg, wmv, wmvt, escape, rmem, rmemt}
 function translate39(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = {
   match lookup_TLB39(asid, vAddr) {
     Some(idx, ent) => {
diff --git a/model/riscv_vmem_sv48.sail b/model/riscv_vmem_sv48.sail
index 6bfeea4..36304cf 100644
--- a/model/riscv_vmem_sv48.sail
+++ b/model/riscv_vmem_sv48.sail
@@ -1,6 +1,6 @@
 /* Sv48 address translation for RV64. */
 
-val walk48 : (vaddr48, AccessType(ext_access_type), Privilege, bool, bool, paddr64, nat, bool, ext_ptw) -> PTW_Result(paddr64, SV48_PTE) effect {rmem, rreg, escape}
+val walk48 : (vaddr48, AccessType(ext_access_type), Privilege, bool, bool, paddr64, nat, bool, ext_ptw) -> PTW_Result(paddr64, SV48_PTE) effect {rmem, rmemt, rreg, escape}
 function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = {
   let va = Mk_SV48_Vaddr(vaddr);
   let pt_ofs : paddr64 = shiftl(EXTZ(shiftr(va.VPNi(), (level * SV48_LEVEL_BITS))[(SV48_LEVEL_BITS - 1) .. 0]),
@@ -31,13 +31,13 @@ function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = {
         PTW_Failure(PTW_Invalid_PTE(), ext_ptw)
       } else {
         if isPTEPtr(pbits, ext_pte) then {
-          if level == 0 then {
+          if level > 0 then {
+            /* walk down the pointer to the next level */
+            walk48(vaddr, ac, priv, mxr, do_sum, shiftl(EXTZ(pte.PPNi()), PAGESIZE_BITS), level - 1, is_global, ext_ptw)
+          } else {
             /* last-level PTE contains a pointer instead of a leaf */
 /*          print("walk48: last-level pte contains a ptr"); */
             PTW_Failure(PTW_Invalid_PTE(), ext_ptw)
-          } else {
-            /* walk down the pointer to the next level */
-            walk48(vaddr, ac, priv, mxr, do_sum, shiftl(EXTZ(pte.PPNi()), PAGESIZE_BITS), level - 1, is_global, ext_ptw)
           }
         } else { /* leaf PTE */
           match checkPTEPermission(ac, priv, mxr, do_sum, pattr, ext_pte, ext_ptw) {
@@ -109,7 +109,7 @@ function flush_TLB48(asid, addr) =
 
 /* address translation */
 
-val translate48 : (asid64, paddr64, vaddr48, AccessType(ext_access_type), Privilege, bool, bool, nat, ext_ptw) -> TR_Result(paddr64, PTW_Error) effect {rreg, wreg, wmv, wmvt, escape, rmem}
+val translate48 : (asid64, paddr64, vaddr48, AccessType(ext_access_type), Privilege, bool, bool, nat, ext_ptw) -> TR_Result(paddr64, PTW_Error) effect {rreg, wreg, wmv, wmvt, escape, rmem, rmemt}
 function translate48(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = {
   match walk48(vAddr, ac, priv, mxr, do_sum, ptb, level, false, ext_ptw) {
     PTW_Failure(f, ext_ptw) => TR_Failure(f, ext_ptw),