Merge branch 'sail2' into rmem_interpreter

23 files changed, 851 insertions, 134 deletions

diff --git a/riscv/Makefile b/riscv/Makefile
index 73bd01c0..e6bbbd5c 100644
--- a/riscv/Makefile
+++ b/riscv/Makefile
@@ -1,10 +1,36 @@
-SAIL_SRCS = riscv_all.sail
+SAIL_SEQ_INST  = riscv.sail riscv_jalr_seq.sail
+SAIL_RMEM_INST = riscv.sail riscv_jalr_rmem.sail
+
+SAIL_SEQ_INST_SRCS  = riscv_insts_begin.sail $(SAIL_SEQ_INST) riscv_insts_end.sail
+SAIL_RMEM_INST_SRCS = riscv_insts_begin.sail $(SAIL_RMEM_INST) riscv_insts_end.sail
+
+# non-instruction sources
+SAIL_OTHER_SRCS = prelude.sail riscv_types.sail riscv_sys.sail riscv_platform.sail riscv_mem.sail riscv_vmem.sail
+
+SAIL_SRCS      = $(SAIL_OTHER_SRCS) $(SAIL_SEQ_INST_SRCS)  riscv_step.sail riscv_analysis.sail
+SAIL_RMEM_SRCS = $(SAIL_OTHER_SRCS) $(SAIL_RMEM_INST_SRCS) riscv_step.sail riscv_analysis.sail
+
 PLATFORM_OCAML_SRCS = platform.ml platform_impl.ml platform_main.ml
 SAIL_DIR ?= $(realpath ..)
 SAIL ?= $(SAIL_DIR)/sail
 C_WARNINGS ?=
 #-Wall -Wextra -Wno-unused-label -Wno-unused-parameter -Wno-unused-but-set-variable -Wno-unused-function
-C_SRCS = riscv_prelude.c riscv_platform.c
+C_FLAGS = -I ../lib
+C_INCS = riscv_prelude.h riscv_platform_impl.h riscv_platform.h
+C_SRCS = riscv_prelude.c riscv_platform_impl.c riscv_platform.c
+
+ENABLE_SPIKE = 0
+TV_SPIKE_DIR = /home/mundkur/src/hw/l3/l3riscv
+SPIKE_FLAGS = -I $(TV_SPIKE_DIR)/src/cpp
+SPIKE_LIBS  = -L $(TV_SPIKE_DIR) -ltv_spike -Wl,-rpath=$(TV_SPIKE_DIR)
+SPIKE_LIBS += -L $(RISCV)/lib -lfesvr -lriscv -Wl,-rpath=$(RISCV)/lib
+
+C_LIBS = -lgmp -lz
+
+ifeq ($(ENABLE_SPIKE),1)
+C_FLAGS += $(SPIKE_FLAGS)
+C_LIBS  += $(SPIKE_LIBS)
+endif
 
 export SAIL_DIR
 
@@ -38,9 +64,15 @@ coverage: _sbuild/coverage.native
 riscv.c: $(SAIL_SRCS) main.sail Makefile
 	$(SAIL) -O -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h $(SAIL_SRCS) main.sail 1> $@
 
-riscv_c: riscv.c riscv_prelude.h $(C_SRCS) Makefile
+riscv_c: riscv.c $(C_INCS) $(C_SRCS) Makefile
 	gcc $(C_WARNINGS) -O2 riscv.c $(C_SRCS) ../lib/*.c -lgmp -lz -I ../lib -o riscv_c
 
+riscv_model.c: $(SAIL_SRCS) main.sail Makefile
+	$(SAIL) -O -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_SRCS) main.sail 1> $@
+
+riscv_sim: riscv_model.c riscv_sim.c $(C_INCS) $(C_SRCS) $(CPP_SRCS) Makefile
+	gcc -g $(C_WARNINGS) $(C_FLAGS) -O2 riscv_model.c riscv_sim.c $(C_SRCS) ../lib/*.c $(C_LIBS) -o $@
+
 latex: $(SAIL_SRCS) Makefile
 	$(SAIL) -latex -latex_prefix sail -o sail_ltx $(SAIL_SRCS)
 
@@ -108,6 +140,6 @@ clean:
 	-rm -f platform_main.native platform coverage.native
 	-rm -f riscv.vo riscv_types.vo riscv_extras.vo riscv.v riscv_types.v
 	-rm -f riscv_duopod.vo riscv_duopod_types.vo riscv_duopod.v riscv_duopod_types.v
-	-rm -f riscv.c
+	-rm -f riscv.c riscv_model.c riscv_sim
 	-Holmake cleanAll
 	ocamlbuild -clean
diff --git a/riscv/README b/riscv/README
new file mode 100644
index 00000000..b925821e
--- /dev/null
+++ b/riscv/README
@@ -0,0 +1,23 @@
+Booting Linux with the C backend:
+---------------------------------
+
+The C model needs an ELF-version of the BBL (Berkeley-Boot-Loader) that contains
+the Linux kernel as an embedded payload.  It also needs a DTB (device-tree blob)
+file describing the platform.  Once those are available, the model should be run
+as:
+
+$ ./riscv_sim -b spike.dtb bbl > execution-trace.log 2>&1 &
+$ tail -f term.log
+
+The term.log file contains the console boot messages.
+
+
+Booting Linux with the OCaml backend:
+-------------------------------------
+
+The OCaml model only needs the ELF-version of the BBL, since it can generate its
+own DTB.
+
+$ ./platform bbl > execution-trace.log
+
+The console output is sent to stderr.
diff --git a/riscv/coq.patch b/riscv/coq.patch
index 2dc1b4aa..6c40e6e2 100644
--- a/riscv/coq.patch
+++ b/riscv/coq.patch
@@ -1,6 +1,34 @@
---- riscv.v	2018-10-01 18:21:50.121189040 +0100
-+++ riscv.v.good	2018-10-01 18:21:24.485040512 +0100
-@@ -10537,14 +10537,13 @@
+--- riscv.v	2018-10-22 18:20:01.512785981 +0100
++++ riscv.v.good	2018-10-22 18:19:27.556562080 +0100
+@@ -1260,6 +1260,9 @@
+    let v64 : bits 64 := EXTS 64 v in
+    subrange_vec_dec (shift_bits_right v64 shift) 31 0.
+ 
++Definition n_leading_spaces s : {n : Z & ArithFact (n >= 0)} :=
++ build_ex (Z.of_nat (n_leading_spaces s)).
++(*
+ Fixpoint n_leading_spaces (s : string) 
+ : {n : Z & ArithFact (n >= 0)} :=
+    build_ex(let p0_ := s in
+@@ -1273,7 +1276,7 @@
+                                                                              (string_drop s
+                                                                                 (build_ex 1)))))))
+                   : {n : Z & ArithFact (n >= 0)}))))
+-     else 0).
++     else 0).*)
+ 
+ Definition spc_forwards '(tt : unit)  : string := " ".
+ 
+@@ -1284,7 +1287,7 @@
+    let 'n := projT1 (n_leading_spaces s) in
+    let p0_ := n in
+    if sumbool_of_bool ((Z.eqb p0_ 0)) then None
+-   else Some ((tt, n)).
++   else Some ((tt, build_ex n)).
+ 
+ Definition opt_spc_forwards '(tt : unit)  : string := "".
+ 
+@@ -10432,14 +10435,13 @@
     returnm ((EXTZ 56 (shiftl (_get_Satp64_PPN satp64) PAGESIZE_BITS))
      : mword 56).
  
@@ -17,7 +45,7 @@
               (projT1 (sub_range (build_ex SV39_LEVEL_BITS) (build_ex 1))) 0)) PTE39_LOG_SIZE in
     let pte_addr := add_vec ptb pt_ofs in
     (phys_mem_read Data (EXTZ 64 pte_addr) 8 false false false) >>= fun w__0 : MemoryOpResult (mword (8 * 8)) =>
-@@ -10557,27 +10556,27 @@
+@@ -10452,27 +10454,27 @@
         let is_global := orb global (eq_vec (_get_PTE_Bits_G pattr) ((bool_to_bits true)  : mword 1)) in
         (if ((isInvalidPTE pbits)) then returnm ((PTW_Failure (PTW_Invalid_PTE))  : PTW_Result )
          else if ((isPTEPtr pbits)) then
@@ -51,7 +79,7 @@
                        if ((neq_vec (and_vec (_get_SV39_PTE_PPNi pte) mask)
                               (EXTZ 44 (vec_of_bits [B0]  : mword 1)))) then
                          PTW_Failure
-@@ -10587,10 +10586,10 @@
+@@ -10482,10 +10484,10 @@
                            or_vec (_get_SV39_PTE_PPNi pte)
                              (and_vec (EXTZ 44 (_get_SV39_Vaddr_VPNi va)) mask) in
                          PTW_Success
@@ -64,7 +92,7 @@
             : PTW_Result))
          : M (PTW_Result)
      end)
-@@ -10716,7 +10715,7 @@
+@@ -10611,7 +10613,7 @@
          : M (TR39_Result)
      | None =>
         (curPTB39 tt) >>= fun w__6 : mword 56 =>
@@ -73,7 +101,7 @@
         (match w__7 with
          | PTW_Failure (f) => returnm ((TR39_Failure (f))  : TR39_Result )
          | PTW_Success (pAddr,pte,pteAddr,(existT _ level _),global) =>
-@@ -15425,137 +15424,143 @@
+@@ -14651,137 +14653,144 @@
     returnm (true
      : bool).
  
@@ -274,32 +302,33 @@
 +: M (bool) :=
 +let merge_var := expand_ast merge_var in
 +   match merge_var with
++
     | UTYPE (imm,rd,op) => (execute_UTYPE imm rd op)  : M (bool)
     | RISCV_JAL (imm,rd) => (execute_RISCV_JAL imm rd)  : M (bool)
     | RISCV_JALR (imm,rs1,rd) => (execute_RISCV_JALR imm rs1 rd)  : M (bool)
-@@ -15595,6 +15600,7 @@
+@@ -14821,6 +14830,7 @@
     | THREAD_START (arg0) => returnm ((execute_THREAD_START arg0)  : bool)
     | ILLEGAL (s) => (execute_ILLEGAL s)  : M (bool)
-    | C_ILLEGAL (arg0) => (execute_C_ILLEGAL arg0)  : M (bool)
+    | C_ILLEGAL (s) => (execute_C_ILLEGAL s)  : M (bool)
 +| _ => Fail "Unexpanded instruction"
     end.
  
  Definition assembly_forwards (arg_ : ast) 
-@@ -27093,7 +27099,7 @@
-     else returnm (tt  : unit)) >>
+@@ -35792,7 +35802,7 @@
     returnm (stepped
      : bool).
--
-+(*
- Definition loop '(tt : unit) 
+ 
+-Definition loop '(tt : unit) 
++(*Definition loop '(tt : unit) 
  : M (unit) :=
     let insns_per_tick := plat_insns_per_tick tt in
-@@ -27135,7 +27141,7 @@
+    let i : Z := 0 in
+@@ -35832,7 +35842,7 @@
+            : M (Z)) >>= fun i : Z =>
         returnm (i, step_no))) >>= fun '(i, step_no) =>
     returnm (tt
-     : unit).
--
-+*)
+-    : unit).
++    : unit).*)
+ 
  Definition read_kind_of_num (arg_ : Z) `{ArithFact (0 <= arg_ /\ arg_ <= 11)} 
  : read_kind :=
-    let p0_ := arg_ in
diff --git a/riscv/platform.ml b/riscv/platform.ml
index f5324794..015d189b 100644
--- a/riscv/platform.ml
+++ b/riscv/platform.ml
@@ -56,6 +56,7 @@ module Elf = Elf_loader;;
 
 let config_enable_dirty_update = ref false
 let config_enable_misaligned_access = ref false
+let config_mtval_has_illegal_inst_bits = ref false
 
 (* Mapping to Sail externs *)
 
@@ -82,6 +83,7 @@ let make_rom start_pc =
 
 let enable_dirty_update () = !config_enable_dirty_update
 let enable_misaligned_access () = !config_enable_misaligned_access
+let mtval_has_illegal_inst_bits () = !config_mtval_has_illegal_inst_bits
 
 let rom_base () = bits_of_int64 P.rom_base
 let rom_size () = bits_of_int   !rom_size_ref
diff --git a/riscv/platform_impl.ml b/riscv/platform_impl.ml
index e593dce9..c5cc3fff 100644
--- a/riscv/platform_impl.ml
+++ b/riscv/platform_impl.ml
@@ -159,7 +159,7 @@ let make_dtb dts = (* Call the dtc compiler, assumed to be at /usr/bin/dtc *)
 (* Terminal I/O *)
 
 let term_write char =
-  ignore (Unix.write_substring Unix.stdout (String.make 1 char) 0 1)
+  ignore (Unix.write_substring Unix.stderr (String.make 1 char) 0 1)
 
 let rec term_read () =
   let buf = Bytes.make 1 '\000' in
diff --git a/riscv/platform_main.ml b/riscv/platform_main.ml
index e204daee..b33247f1 100644
--- a/riscv/platform_main.ml
+++ b/riscv/platform_main.ml
@@ -73,6 +73,9 @@ let options = Arg.align ([("-dump-dts",
                           ("-enable-misaligned-access",
                            Arg.Set P.config_enable_misaligned_access,
                            " enable misaligned accesses without M-mode traps");
+                          ("-mtval-has-illegal-inst-bits",
+                           Arg.Set P.config_mtval_has_illegal_inst_bits,
+                           " mtval stores instruction bits on an illegal instruction exception");
                           ("-with-dtc",
                            Arg.String PI.set_dtc,
                            " full path to dtc to use")
diff --git a/riscv/riscv.sail b/riscv/riscv.sail
index 1dc9ba8f..fa715f80 100644
--- a/riscv/riscv.sail
+++ b/riscv/riscv.sail
@@ -1,29 +1,3 @@
-/* Instruction definitions.
- *
- * This includes decoding, execution, and assembly parsing and printing.
- */
-
-scattered union ast
-
-val decode : bits(32) -> option(ast) effect pure
-
-val decodeCompressed : bits(16) -> option(ast) effect pure
-
-val cast print_insn : ast -> string
-
-/* returns whether an instruction was retired, used for computing minstret */
-val execute : ast -> bool effect {escape, wreg, rreg, wmv, eamem, rmem, barr, exmem}
-scattered function execute
-
-val assembly : ast <-> string
-scattered mapping assembly
-
-val encdec : ast <-> bits(32)
-scattered mapping encdec
-
-val encdec_compressed : ast <-> bits(16)
-scattered mapping encdec_compressed
-
 /* ****************************************************************** */
 union clause ast = UTYPE : (bits(20), regbits, uop)
 
@@ -87,25 +61,11 @@ union clause ast = RISCV_JALR : (bits(12), regbits, regbits)
 
 mapping clause encdec = RISCV_JALR(imm, rs1, rd) <-> imm @ rs1 @ 0b000 @ rd @ 0b1100111
 
-function clause execute (RISCV_JALR(imm, rs1, rd)) = {
-  /* write rd before anything else to prevent unintended strength */
-  X(rd) = nextPC; /* compatible with JALR, C.JR and C.JALR */
-  let newPC : xlenbits = X(rs1) + EXTS(imm);
-/*  RMEM FIXME: For the sequential model, the above definition doesn't work directly
-    if rs1 = rd.  We would effectively have to keep a regfile for reads and another for
-    writes, and swap on instruction fetch.  This could perhaps be optimized in
-    some manner, but for now, we just reorder the previous two lines to improve simulator
-    performance in the sequential model, as below:
-  let newPC : xlenbits = X(rs1) + EXTS(imm);
-  X(rd) = nextPC; /* compatible with JALR, C.JR and C.JALR */
-*/
-  nextPC = newPC[63..1] @ 0b0;
-  true
-}
-
 mapping clause assembly = RISCV_JALR(imm, rs1, rd)
                       <-> "jalr" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_12(imm)
 
+/* see riscv_jalr_seq.sail or riscv_jalr_rmem.sail for the execute clause. */
+
 /* ****************************************************************** */
 union clause ast = BTYPE : (bits(13), regbits, regbits, bop)
 
@@ -851,7 +811,7 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) =
        }
 
 mapping clause assembly = LOADRES(aq, rl, rs1, size, rd)
-                      <-> "lr." ^ maybe_aq(aq) ^ maybe_rl(rl) ^ size_mnemonic(size) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1)
+                      <-> "lr" ^ maybe_aq(aq) ^ maybe_rl(rl) ^ size_mnemonic(size) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1)
 
 /* ****************************************************************** */
 union clause ast = STORECON : (bool, bool, regbits, regbits, word_width, regbits)
@@ -916,7 +876,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
   }
 }
 
-mapping clause assembly = STORECON(aq, rl, rs2, rs1, size, rd) <-> "sc." ^ maybe_aq(aq) ^ maybe_rl(rl) ^ size_mnemonic(size) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
+mapping clause assembly = STORECON(aq, rl, rs2, rs1, size, rd) <-> "sc" ^ maybe_aq(aq) ^ maybe_rl(rl) ^ size_mnemonic(size) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
 
 /* ****************************************************************** */
 union clause ast = AMO : (amoop, bool, bool, regbits, regbits, word_width, regbits)
@@ -1585,14 +1545,3 @@ function clause execute C_ILLEGAL(s) = { handle_illegal(); false }
 mapping clause assembly = C_ILLEGAL(s) <-> "c.illegal" ^ spc() ^ hex_bits_16(s)
 
 /* ****************************************************************** */
-
-
-end ast
-end execute
-end assembly
-end encdec
-end encdec_compressed
-
-function decode bv = Some(encdec(bv))
-function decodeCompressed bv = Some(encdec_compressed(bv))
-function print_insn insn = assembly(insn)
\ No newline at end of file
diff --git a/riscv/riscv_extras.lem b/riscv/riscv_extras.lem
index a6fa1298..7028d5b8 100644
--- a/riscv/riscv_extras.lem
+++ b/riscv/riscv_extras.lem
@@ -97,6 +97,10 @@ val plat_enable_misaligned_access : unit -> bool
 let plat_enable_misaligned_access () = false
 declare ocaml target_rep function plat_enable_misaligned_access = `Platform.enable_misaligned_access`
 
+val plat_mtval_has_illegal_inst_bits : unit -> bool
+let plat_mtval_has_illegal_inst_bits () = false
+declare ocaml target_rep function plat_mtval_has_illegal_inst_bits = `Platform.mtval_has_illegal_inst_bits`
+
 val plat_insns_per_tick : unit -> integer
 let plat_insns_per_tick () = 1
 declare ocaml target_rep function plat_insns_per_tick = `Platform.insns_per_tick`
diff --git a/riscv/riscv_extras_sequential.lem b/riscv/riscv_extras_sequential.lem
index a6fa1298..7028d5b8 100644
--- a/riscv/riscv_extras_sequential.lem
+++ b/riscv/riscv_extras_sequential.lem
@@ -97,6 +97,10 @@ val plat_enable_misaligned_access : unit -> bool
 let plat_enable_misaligned_access () = false
 declare ocaml target_rep function plat_enable_misaligned_access = `Platform.enable_misaligned_access`
 
+val plat_mtval_has_illegal_inst_bits : unit -> bool
+let plat_mtval_has_illegal_inst_bits () = false
+declare ocaml target_rep function plat_mtval_has_illegal_inst_bits = `Platform.mtval_has_illegal_inst_bits`
+
 val plat_insns_per_tick : unit -> integer
 let plat_insns_per_tick () = 1
 declare ocaml target_rep function plat_insns_per_tick = `Platform.insns_per_tick`
diff --git a/riscv/riscv_insts_begin.sail b/riscv/riscv_insts_begin.sail
new file mode 100644
index 00000000..56fd8b43
--- /dev/null
+++ b/riscv/riscv_insts_begin.sail
@@ -0,0 +1,19 @@
+/* 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 -> bool effect {escape, wreg, rreg, wmv, eamem, rmem, barr, exmem}
+scattered function execute
+
+val assembly : ast <-> string
+scattered mapping assembly
+
+val encdec : ast <-> bits(32)
+scattered mapping encdec
+
+val encdec_compressed : ast <-> bits(16)
+scattered mapping encdec_compressed
diff --git a/riscv/riscv_insts_end.sail b/riscv/riscv_insts_end.sail
new file mode 100644
index 00000000..144f06e3
--- /dev/null
+++ b/riscv/riscv_insts_end.sail
@@ -0,0 +1,15 @@
+/* End definitions */
+end ast
+end execute
+end assembly
+end encdec
+end encdec_compressed
+
+val cast print_insn : ast -> string
+function print_insn insn = assembly(insn)
+
+val decode : bits(32) -> option(ast) effect pure
+function decode bv = Some(encdec(bv))
+
+val decodeCompressed : bits(16) -> option(ast) effect pure
+function decodeCompressed bv = Some(encdec_compressed(bv))
diff --git a/riscv/riscv_jalr_rmem.sail b/riscv/riscv_jalr_rmem.sail
new file mode 100644
index 00000000..3e5eec9a
--- /dev/null
+++ b/riscv/riscv_jalr_rmem.sail
@@ -0,0 +1,9 @@
+/* The definition for the memory model. */
+
+function clause execute (RISCV_JALR(imm, rs1, rd)) = {
+  /* write rd before anything else to prevent unintended strength */
+  X(rd) = nextPC; /* compatible with JALR, C.JR and C.JALR */
+  let newPC : xlenbits = X(rs1) + EXTS(imm);
+  nextPC = newPC[63..1] @ 0b0;
+  true
+}
diff --git a/riscv/riscv_jalr_seq.sail b/riscv/riscv_jalr_seq.sail
new file mode 100644
index 00000000..b38563ef
--- /dev/null
+++ b/riscv/riscv_jalr_seq.sail
@@ -0,0 +1,14 @@
+/* The definition for the sequential model. */
+
+function clause execute (RISCV_JALR(imm, rs1, rd)) = {
+/* For the sequential model, the memory-model definition doesn't work directly
+   if rs1 = rd.  We would effectively have to keep a regfile for reads and another for
+   writes, and swap on instruction completion.  This could perhaps be optimized in
+   some manner, but for now, we just keep a reordered definition to improve simulator
+   performance.
+*/
+  let newPC : xlenbits = X(rs1) + EXTS(imm);
+  X(rd) = nextPC;
+  nextPC = newPC[63..1] @ 0b0;
+  true
+}
diff --git a/riscv/riscv_platform.c b/riscv/riscv_platform.c
index 7f6ec470..f0aff76a 100644
--- a/riscv/riscv_platform.c
+++ b/riscv/riscv_platform.c
@@ -1,68 +1,68 @@
 #include "sail.h"
 #include "rts.h"
 #include "riscv_prelude.h"
+#include "riscv_platform_impl.h"
+
+/* This file contains the definitions of the C externs of Sail model. */
+
+static mach_bits reservation = 0;
+static bool reservation_valid = false;
 
 bool plat_enable_dirty_update(unit u)
-{ return false; }
+{ return rv_enable_dirty_update; }
 
 bool plat_enable_misaligned_access(unit u)
-{ return false; }
+{ return rv_enable_misaligned; }
+
+bool plat_mtval_has_illegal_inst_bits(unit u)
+{ return rv_mtval_has_illegal_inst_bits; }
 
 mach_bits plat_ram_base(unit u)
-{
-  return UINT64_C(0x80000000);
-}
+{ return rv_ram_base; }
 
 mach_bits plat_ram_size(unit u)
-{
-  return UINT64_C(0x80000000);
-}
+{ return rv_ram_size; }
 
 mach_bits plat_rom_base(unit u)
-{
-  return UINT64_C(0x1000);
-}
+{ return rv_rom_base; }
 
 mach_bits plat_rom_size(unit u)
-{
-  return UINT64_C(0x100);
-}
+{ return rv_rom_size; }
 
 mach_bits plat_clint_base(unit u)
-{
-  return UINT64_C(0x2000000);
-}
+{ return rv_clint_base; }
 
 mach_bits plat_clint_size(unit u)
-{
-  return UINT64_C(0xc0000);
-}
+{ return rv_clint_size; }
 
-bool within_phys_mem(mach_bits addr, sail_int len)
+unit load_reservation(mach_bits addr)
 {
-  printf("within_phys_mem\n");
-  exit(EXIT_FAILURE);
-  return 0;
+  reservation = addr;
+  reservation_valid = true;
+  return UNIT;
 }
 
-unit load_reservation(mach_bits addr)
-{ return UNIT; }
-
 bool match_reservation(mach_bits addr)
-{ return false; }
+{ return reservation_valid && reservation == addr; }
 
 unit cancel_reservation(unit u)
-{ return UNIT; }
+{
+  reservation_valid = false;
+  return UNIT;
+}
 
-unit plat_term_write(mach_bits c)
-{ return UNIT; }
+unit plat_term_write(mach_bits s)
+{ char c = s & 0xff;
+  plat_term_write_impl(c);
+  return UNIT;
+}
 
 void plat_insns_per_tick(sail_int *rop, unit u)
 { }
 
 mach_bits plat_htif_tohost(unit u)
 {
-  return UINT64_C(0x80001000);
+  return rv_htif_tohost;
 }
 
 unit memea(mach_bits len, sail_int n)
diff --git a/riscv/riscv_platform.h b/riscv/riscv_platform.h
index 4401ad49..93782660 100644
--- a/riscv/riscv_platform.h
+++ b/riscv/riscv_platform.h
@@ -3,6 +3,7 @@
 
 bool plat_enable_dirty_update(unit);
 bool plat_enable_misaligned_access(unit);
+bool plat_mtval_has_illegal_inst_bits(unit);
 
 mach_bits plat_ram_base(unit);
 mach_bits plat_ram_size(unit);
diff --git a/riscv/riscv_platform.sail b/riscv/riscv_platform.sail
index 728b25f9..aac6b587 100644
--- a/riscv/riscv_platform.sail
+++ b/riscv/riscv_platform.sail
@@ -38,6 +38,11 @@ val plat_enable_misaligned_access = {ocaml: "Platform.enable_misaligned_access",
                                      lem: "plat_enable_misaligned_access"} : unit -> bool
 function plat_enable_misaligned_access () = false
 
+/* whether mtval stores the bits of a faulting instruction on illegal instruction exceptions */
+val plat_mtval_has_illegal_inst_bits = {ocaml: "Platform.mtval_has_illegal_inst_bits",
+                                        c: "plat_mtval_has_illegal_inst_bits",
+                                        lem: "plat_mtval_has_illegal_inst_bits"} : unit -> bool
+
 /* ROM holding reset vector and device-tree DTB */
 val plat_rom_base   = {ocaml: "Platform.rom_base", c: "plat_rom_base", lem: "plat_rom_base"} : unit -> xlenbits
 function plat_rom_base () = 0x0000000000001000
@@ -63,15 +68,28 @@ function phys_mem_segments() =
 
 /* Physical memory map predicates */
 
-function within_phys_mem(addr : xlenbits, width : atom('n)) -> forall 'n. bool =
+function within_phys_mem(addr : xlenbits, width : atom('n)) -> forall 'n. bool = {
+  let ram_base = plat_ram_base ();
+  let rom_base = plat_rom_base ();
+  let ram_size = plat_ram_size ();
+  let rom_size = plat_rom_size ();
+
   /* todo: iterate over segment list */
-  if (  plat_ram_base() <=_u addr
-      & (addr + sizeof('n)) <=_u (plat_ram_base() + plat_ram_size ()))
+  if (  ram_base <=_u addr
+      & (addr + sizeof('n)) <=_u (ram_base + ram_size))
        then true
-  else if (  plat_rom_base() <=_u addr
-           & (addr + sizeof('n)) <=_u (plat_rom_base() + plat_rom_size()))
+  else if (  rom_base <=_u addr
+           & (addr + sizeof('n)) <=_u (rom_base + rom_size))
        then true
-  else false
+  else {
+    print("within_phys_mem: " ^ BitStr(addr) ^ " not within phys-mem:");
+    print("  plat_rom_base: " ^ BitStr(rom_base));
+    print("  plat_rom_size: " ^ BitStr(rom_size));
+    print("  plat_ram_base: " ^ BitStr(ram_base));
+    print("  plat_ram_size: " ^ BitStr(ram_size));
+    false
+  }
+}
 
 function within_clint(addr : xlenbits, width : atom('n)) -> forall 'n. bool =
     plat_clint_base() <=_u addr
@@ -274,3 +292,14 @@ function tick_platform() -> unit = {
   cancel_reservation();
   htif_tick();
 }
+
+/* Platform-specific handling of instruction faults */
+
+function handle_illegal() -> unit = {
+  let info = if plat_mtval_has_illegal_inst_bits ()
+             then Some(instbits)
+             else None();
+  let t : sync_exception = struct { trap    = E_Illegal_Instr,
+                                    excinfo = info };
+  nextPC = handle_exception(cur_privilege, CTL_TRAP(t), PC)
+}
diff --git a/riscv/riscv_platform_impl.c b/riscv/riscv_platform_impl.c
new file mode 100644
index 00000000..04a661c0
--- /dev/null
+++ b/riscv/riscv_platform_impl.c
@@ -0,0 +1,29 @@
+#include "riscv_platform_impl.h"
+#include <unistd.h>
+#include <stdio.h>
+
+/* Settings of the platform implementation, with common defaults. */
+
+bool rv_enable_dirty_update         = false;
+bool rv_enable_misaligned           = false;
+bool rv_mtval_has_illegal_inst_bits = false;
+
+uint64_t rv_ram_base = UINT64_C(0x80000000);
+uint64_t rv_ram_size = UINT64_C(0x80000000);
+
+uint64_t rv_rom_base = UINT64_C(0x1000);
+uint64_t rv_rom_size = UINT64_C(0x100);
+
+uint64_t rv_clint_base = UINT64_C(0x2000000);
+uint64_t rv_clint_size = UINT64_C(0xc0000);
+
+uint64_t rv_htif_tohost = UINT64_C(0x80001000);
+uint64_t rv_insns_per_tick = UINT64_C(100);
+
+int term_fd = 1; // set during startup
+void plat_term_write_impl(char c)
+{
+  if (write(term_fd, &c, sizeof(c)) < 0) {
+    fprintf(stderr, "Unable to write to terminal!\n");
+  }
+}
diff --git a/riscv/riscv_platform_impl.h b/riscv/riscv_platform_impl.h
new file mode 100644
index 00000000..85e25c95
--- /dev/null
+++ b/riscv/riscv_platform_impl.h
@@ -0,0 +1,28 @@
+#pragma once
+
+#include <stdbool.h>
+#include <stdint.h>
+
+/* Settings of the platform implementation. */
+
+#define DEFAULT_RSTVEC     0x00001000
+#define SAIL_XLEN          64
+
+extern bool rv_enable_dirty_update;
+extern bool rv_enable_misaligned;
+extern bool rv_mtval_has_illegal_inst_bits;
+
+extern uint64_t rv_ram_base;
+extern uint64_t rv_ram_size;
+
+extern uint64_t rv_rom_base;
+extern uint64_t rv_rom_size;
+
+extern uint64_t rv_clint_base;
+extern uint64_t rv_clint_size;
+
+extern uint64_t rv_htif_tohost;
+extern uint64_t rv_insns_per_tick;
+
+extern int term_fd;
+void plat_term_write_impl(char c);
diff --git a/riscv/riscv_sail.h b/riscv/riscv_sail.h
new file mode 100644
index 00000000..f2569b3b
--- /dev/null
+++ b/riscv/riscv_sail.h
@@ -0,0 +1,44 @@
+/* Top-level interfaces to the Sail model.
+   Ideally, this would be autogenerated.
+ */
+
+typedef int unit;
+#define UNIT 0
+typedef uint64_t mach_bits;
+
+void model_init(void);
+void model_fini(void);
+
+unit zinit_platform(unit);
+unit zinit_sys(unit);
+bool zstep(sail_int);
+unit ztick_clock(unit);
+unit ztick_platform(unit);
+
+extern bool zhtif_done;
+extern mach_bits zhtif_exit_code;
+extern bool have_exception;
+
+/* machine state */
+
+extern uint32_t zcur_privilege;
+
+extern mach_bits zPC;
+
+extern mach_bits
+        zx1,  zx2,  zx3,  zx4,  zx5,  zx6,  zx7,
+  zx8,  zx9,  zx10, zx11, zx12, zx13, zx14, zx15,
+  zx16, zx17, zx18, zx19, zx20, zx21, zx22, zx23,
+  zx24, zx25, zx26, zx27, zx28, zx29, zx30, zx31;
+
+extern mach_bits zmstatus;
+extern mach_bits zmepc, zmtval;
+extern mach_bits zsepc, zstval;
+
+struct zMcause {mach_bits zMcause_chunk_0;};
+struct zMcause zmcause, zscause;
+
+extern mach_bits zminstret;
+
+struct zMisa {mach_bits zMisa_chunk_0;};
+struct zMisa zmisa;
diff --git a/riscv/riscv_sim.c b/riscv/riscv_sim.c
new file mode 100644
index 00000000..276c7b1b
--- /dev/null
+++ b/riscv/riscv_sim.c
@@ -0,0 +1,486 @@
+#include <getopt.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <errno.h>
+#include <unistd.h>
+#include <sys/types.h>
+#include <sys/stat.h>
+#include <sys/mman.h>
+#include <fcntl.h>
+
+#include "elf.h"
+#include "sail.h"
+#include "rts.h"
+#include "riscv_platform.h"
+#include "riscv_platform_impl.h"
+#include "riscv_sail.h"
+
+//#define SPIKE 1
+#ifdef SPIKE
+#include "tv_spike_intf.h"
+#else
+struct tv_spike_t;
+#endif
+
+/* Selected CSRs from riscv-isa-sim/riscv/encoding.h */
+#define CSR_STVEC 0x105
+#define CSR_SEPC 0x141
+#define CSR_SCAUSE 0x142
+#define CSR_STVAL 0x143
+
+#define CSR_MSTATUS 0x300
+#define CSR_MISA 0x301
+#define CSR_MEDELEG 0x302
+#define CSR_MIDELEG 0x303
+#define CSR_MIE 0x304
+#define CSR_MTVEC 0x305
+#define CSR_MEPC 0x341
+#define CSR_MCAUSE 0x342
+#define CSR_MTVAL 0x343
+#define CSR_MIP 0x344
+
+static bool do_dump_dts = false;
+struct tv_spike_t *s = NULL;
+char *term_log = NULL;
+char *dtb_file = NULL;
+unsigned char *dtb = NULL;
+size_t dtb_len = 0;
+
+unsigned char *spike_dtb = NULL;
+size_t spike_dtb_len = 0;
+
+static struct option options[] = {
+  {"enable-dirty",                no_argument,       0, 'd'},
+  {"enable-misaligned",           no_argument,       0, 'm'},
+  {"mtval-has-illegal-inst-bits", no_argument,       0, 'i'},
+  {"dump-dts",                    no_argument,       0, 's'},
+  {"device-tree-blob",            required_argument, 0, 'b'},
+  {"terminal-log",                required_argument, 0, 't'},
+  {"help",                        no_argument,       0, 'h'},
+  {0, 0, 0, 0}
+};
+
+static void print_usage(const char *argv0, int ec)
+{
+  fprintf(stdout, "Usage: %s [options] <elf_file>\n", argv0);
+  struct option *opt = options;
+  while (opt->name) {
+    fprintf(stdout, "\t -%c\t %s\n", (char)opt->val, opt->name);
+    opt++;
+  }
+  exit(ec);
+}
+
+static void dump_dts(void)
+{
+#ifdef SPIKE
+  size_t dts_len = 0;
+  struct tv_spike_t *s = tv_init("RV64IMAC", 0);
+  tv_get_dts(s, NULL, &dts_len);
+  if (dts_len > 0) {
+    unsigned char *dts = (unsigned char *)malloc(dts_len + 1);
+    dts[dts_len] = '\0';
+    tv_get_dts(s, dts, &dts_len);
+    fprintf(stdout, "%s\n", dts);
+  }
+#else
+  fprintf(stdout, "Spike linkage is currently needed to generate DTS.\n");
+#endif
+  exit(0);
+}
+
+static void read_dtb(const char *path)
+{
+  int fd = open(path, O_RDONLY);
+  if (fd < 0) {
+    fprintf(stderr, "Unable to read DTB file %s: %s\n", path, strerror(errno));
+    exit(1);
+  }
+  struct stat st;
+  if (fstat(fd, &st) < 0) {
+    fprintf(stderr, "Unable to stat DTB file %s: %s\n", path, strerror(errno));
+    exit(1);
+  }
+  char *m = (char *)mmap(NULL, st.st_size, PROT_READ, MAP_PRIVATE, fd, 0);
+  if (m == MAP_FAILED) {
+    fprintf(stderr, "Unable to map DTB file %s: %s\n", path, strerror(errno));
+    exit(1);
+  }
+  dtb = (unsigned char *)malloc(st.st_size);
+  if (dtb == NULL) {
+    fprintf(stderr, "Cannot allocate DTB from file %s!\n", path);
+    exit(1);
+  }
+  memcpy(dtb, m, st.st_size);
+  dtb_len = st.st_size;
+  munmap(m, st.st_size);
+  close(fd);
+
+  fprintf(stdout, "Read %ld bytes of DTB from %s.\n", dtb_len, path);
+}
+
+char *process_args(int argc, char **argv)
+{
+  int c, idx = 1;
+  while(true) {
+    c = getopt_long(argc, argv, "dmsb:t:v:h", options, &idx);
+    if (c == -1) break;
+    switch (c) {
+    case 'd':
+      rv_enable_dirty_update = true;
+      break;
+    case 'm':
+      rv_enable_misaligned = true;
+      break;
+    case 'i':
+      rv_mtval_has_illegal_inst_bits = true;
+    case 's':
+      do_dump_dts = true;
+      break;
+    case 'b':
+      dtb_file = strdup(optarg);
+      break;
+    case 't':
+      term_log = strdup(optarg);
+      break;
+    case 'h':
+      print_usage(argv[0], 0);
+      break;
+    default:
+      fprintf(stderr, "Unrecognized optchar %c\n", c);
+      print_usage(argv[0], 1);
+    }
+  }
+  if (do_dump_dts) dump_dts();
+  if (idx >= argc) print_usage(argv[0], 0);
+  if (term_log == NULL) term_log = strdup("term.log");
+  if (dtb_file) read_dtb(dtb_file);
+
+  fprintf(stdout, "Running file %s.\n", argv[optind]);
+  return argv[optind];
+}
+
+uint64_t load_sail(char *f)
+{
+  bool is32bit;
+  uint64_t entry;
+  load_elf(f, &is32bit, &entry);
+  if (is32bit) {
+    fprintf(stderr, "32-bit RISC-V not yet supported.\n");
+    exit(1);
+  }
+  fprintf(stdout, "ELF Entry @ %lx\n", entry);
+  /* locate htif ports */
+  if (lookup_sym(f, "tohost", &rv_htif_tohost) < 0) {
+    fprintf(stderr, "Unable to locate htif tohost port.\n");
+    exit(1);
+  }
+  fprintf(stderr, "tohost located at %0" PRIx64 "\n", rv_htif_tohost);
+  return entry;
+}
+
+void init_spike(const char *f, uint64_t entry)
+{
+#ifdef SPIKE
+  /* The initialization order below matters. */
+  s = tv_init("RV64IMAC", 1);
+  tv_set_verbose(s, 1);
+  tv_set_dtb_in_rom(s, 1);
+  tv_load_elf(s, f);
+  tv_reset(s);
+
+  /* sync the insns per tick */
+  rv_insns_per_tick = tv_get_insns_per_tick(s);
+
+  /* get DTB from spike */
+  tv_get_dtb(s, NULL, &spike_dtb_len);
+  if (spike_dtb_len > 0) {
+    spike_dtb = (unsigned char *)malloc(spike_dtb_len + 1);
+    dtb[spike_dtb_len] = '\0';
+    if (!tv_get_dtb(s, spike_dtb, &spike_dtb_len)) {
+      fprintf(stderr, "Got %ld bytes of dtb at %p\n", spike_dtb_len, spike_dtb);
+    } else {
+      fprintf(stderr, "Error getting DTB from Spike.\n");
+      exit(1);
+    }
+  } else {
+    fprintf(stderr, "No DTB available from Spike.\n");
+  }
+#else
+  s = NULL;
+#endif
+}
+
+void tick_spike()
+{
+#ifdef SPIKE
+  tv_tick_clock(s);
+  tv_step_io(s);
+#endif
+}
+
+void init_sail_reset_vector(uint64_t entry)
+{
+#define RST_VEC_SIZE 8
+  uint32_t reset_vec[RST_VEC_SIZE] = {
+    0x297,                                      // auipc  t0,0x0
+    0x28593 + (RST_VEC_SIZE * 4 << 20),         // addi   a1, t0, &dtb
+    0xf1402573,                                 // csrr   a0, mhartid
+    SAIL_XLEN == 32 ?
+      0x0182a283u :                             // lw     t0,24(t0)
+      0x0182b283u,                              // ld     t0,24(t0)
+    0x28067,                                    // jr     t0
+    0,
+    (uint32_t) (entry & 0xffffffff),
+    (uint32_t) (entry >> 32)
+  };
+
+  rv_rom_base = DEFAULT_RSTVEC;
+  uint64_t addr = rv_rom_base;
+  for (int i = 0; i < sizeof(reset_vec); i++)
+    write_mem(addr++, (uint64_t)((char *)reset_vec)[i]);
+
+  if (dtb && dtb_len) {
+    for (size_t i = 0; i < dtb_len; i++)
+      write_mem(addr++, dtb[i]);
+  }
+
+#ifdef SPIKE
+  if (dtb && dtb_len) {
+    // Ensure that Spike's DTB matches the one provided.
+    bool matched = dtb_len == spike_dtb_len;
+    if (matched) {
+      for (size_t i = 0; i < dtb_len; i++)
+        matched = matched && (dtb[i] == spike_dtb[i]);
+    }
+    if (!matched) {
+      fprintf(stderr, "Provided DTB does not match Spike's!\n");
+      exit(1);
+    }
+  } else {
+    if (spike_dtb_len > 0) {
+      // Use the DTB from Spike.
+      for (size_t i = 0; i < spike_dtb_len; i++)
+        write_mem(addr++, spike_dtb[i]);
+    } else {
+      fprintf(stderr, "Running without rom device tree.\n");
+    }
+  }
+#endif
+
+  /* zero-fill to page boundary */
+  const int align = 0x1000;
+  uint64_t rom_end = (addr + align -1)/align * align;
+  for (int i = addr; i < rom_end; i++)
+    write_mem(addr++, 0);
+
+  /* set rom size */
+  rv_rom_size = rom_end - rv_rom_base;
+  /* boot at reset vector */
+  zPC = rv_rom_base;
+}
+
+void init_sail(uint64_t elf_entry)
+{
+  model_init();
+  zinit_platform(UNIT);
+  zinit_sys(UNIT);
+  init_sail_reset_vector(elf_entry);
+}
+
+int init_check(struct tv_spike_t *s)
+{
+  int passed = 1;
+#ifdef SPIKE
+  passed &= tv_check_csr(s, CSR_MISA, zmisa.zMisa_chunk_0);
+#endif
+  return passed;
+}
+
+void finish(int ec)
+{
+  model_fini();
+#ifdef SPIKE
+  tv_free(s);
+#endif
+  exit(ec);
+}
+
+int compare_states(struct tv_spike_t *s)
+{
+  int passed = 1;
+
+#ifdef SPIKE
+  // fix default C enum map for cur_privilege
+  uint8_t priv = (zcur_privilege == 2) ? 3 : zcur_privilege;
+  passed &= tv_check_priv(s, priv);
+
+  passed &= tv_check_pc(s, zPC);
+
+  passed &= tv_check_gpr(s, 1, zx1);
+  passed &= tv_check_gpr(s, 2, zx2);
+  passed &= tv_check_gpr(s, 3, zx3);
+  passed &= tv_check_gpr(s, 4, zx4);
+  passed &= tv_check_gpr(s, 5, zx5);
+  passed &= tv_check_gpr(s, 6, zx6);
+  passed &= tv_check_gpr(s, 7, zx7);
+  passed &= tv_check_gpr(s, 8, zx8);
+  passed &= tv_check_gpr(s, 9, zx9);
+  passed &= tv_check_gpr(s, 10, zx10);
+  passed &= tv_check_gpr(s, 11, zx11);
+  passed &= tv_check_gpr(s, 12, zx12);
+  passed &= tv_check_gpr(s, 13, zx13);
+  passed &= tv_check_gpr(s, 14, zx14);
+  passed &= tv_check_gpr(s, 15, zx15);
+  passed &= tv_check_gpr(s, 15, zx15);
+  passed &= tv_check_gpr(s, 16, zx16);
+  passed &= tv_check_gpr(s, 17, zx17);
+  passed &= tv_check_gpr(s, 18, zx18);
+  passed &= tv_check_gpr(s, 19, zx19);
+  passed &= tv_check_gpr(s, 20, zx20);
+  passed &= tv_check_gpr(s, 21, zx21);
+  passed &= tv_check_gpr(s, 22, zx22);
+  passed &= tv_check_gpr(s, 23, zx23);
+  passed &= tv_check_gpr(s, 24, zx24);
+  passed &= tv_check_gpr(s, 25, zx25);
+  passed &= tv_check_gpr(s, 25, zx25);
+  passed &= tv_check_gpr(s, 26, zx26);
+  passed &= tv_check_gpr(s, 27, zx27);
+  passed &= tv_check_gpr(s, 28, zx28);
+  passed &= tv_check_gpr(s, 29, zx29);
+  passed &= tv_check_gpr(s, 30, zx30);
+  passed &= tv_check_gpr(s, 31, zx31);
+
+  /* some selected CSRs for now */
+
+  passed &= tv_check_csr(s, CSR_MCAUSE, zmcause.zMcause_chunk_0);
+  passed &= tv_check_csr(s, CSR_MEPC, zmepc);
+  passed &= tv_check_csr(s, CSR_MTVAL, zmtval);
+  passed &= tv_check_csr(s, CSR_MSTATUS, zmstatus);
+
+  passed &= tv_check_csr(s, CSR_SCAUSE, zscause.zMcause_chunk_0);
+  passed &= tv_check_csr(s, CSR_SEPC, zsepc);
+  passed &= tv_check_csr(s, CSR_STVAL, zstval);
+#endif
+
+  return passed;
+}
+
+void flush_logs(void)
+{
+  fprintf(stderr, "\n");
+  fflush(stderr);
+  fprintf(stdout, "\n");
+  fflush(stdout);
+}
+
+void run_sail(void)
+{
+  bool spike_done;
+  bool stepped;
+  bool diverged = false;
+
+  /* initialize the step number */
+  mach_int step_no = 0;
+  int insn_cnt = 0;
+
+  while (!zhtif_done) {
+    { /* run a Sail step */
+      sail_int sail_step;
+      CREATE(sail_int)(&sail_step);
+      CONVERT_OF(sail_int, mach_int)(&sail_step, step_no);
+      stepped = zstep(sail_step);
+      if (have_exception) goto step_exception;
+      flush_logs();
+    }
+    if (stepped) {
+      step_no++;
+      insn_cnt++;
+    }
+
+#ifdef SPIKE
+    { /* run a Spike step */
+      tv_step(s);
+      spike_done = tv_is_done(s);
+      flush_logs();
+    }
+
+    if (zhtif_done) {
+      if (!spike_done) {
+        fprintf(stdout, "Sail done (exit-code %ld), but not Spike!\n", zhtif_exit_code);
+        exit(1);
+      }
+    } else {
+      if (spike_done) {
+        fprintf(stdout, "Spike done, but not Sail!\n");
+        exit(1);
+      }
+    }
+    if (!compare_states(s)) {
+      diverged = true;
+      break;
+    }
+#endif
+    if (zhtif_done) {
+      /* check exit code */
+      if (zhtif_exit_code == 0)
+        fprintf(stdout, "SUCCESS\n");
+      else
+        fprintf(stdout, "FAILURE: %ld\n", zhtif_exit_code);
+    }
+
+    if (insn_cnt == rv_insns_per_tick) {
+      insn_cnt = 0;
+      ztick_clock(UNIT);
+      ztick_platform(UNIT);
+
+      tick_spike();
+    }
+  }
+
+ dump_state:
+  if (diverged) {
+    /* TODO */
+  }
+  finish(diverged);
+
+ step_exception:
+  fprintf(stderr, "Sail exception!");
+  goto dump_state;
+}
+
+void init_logs()
+{
+#ifdef SPIKE
+  // The Spike interface uses stdout for terminal output, and stderr for logs.
+  // Do the same here.
+  if (dup2(1, 2) < 0) {
+    fprintf(stderr, "Unable to dup 1 -> 2: %s\n", strerror(errno));
+    exit(1);
+  }
+#endif
+
+  if ((term_fd = open(term_log, O_WRONLY|O_CREAT|O_TRUNC, S_IRUSR|S_IRGRP|S_IROTH|S_IWUSR)) < 0) {
+    fprintf(stderr, "Cannot create terminal log '%s': %s\n", term_log, strerror(errno));
+    exit(1);
+  }
+}
+
+int main(int argc, char **argv)
+{
+  char *file = process_args(argc, argv);
+  init_logs();
+
+  uint64_t entry = load_sail(file);
+
+  /* initialize spike before sail so that we can access the device-tree blob,
+   * until we roll our own.
+   */
+  init_spike(file, entry);
+  init_sail(entry);
+
+  if (!init_check(s)) finish(1);
+
+  run_sail();
+  flush_logs();
+}
diff --git a/riscv/riscv_step.sail b/riscv/riscv_step.sail
index 7d883f24..ef923762 100644
--- a/riscv/riscv_step.sail
+++ b/riscv/riscv_step.sail
@@ -63,7 +63,8 @@ function step(step_no) = {
             match decodeCompressed(h) {
               None() => {
                 print("[" ^ string_of_int(step_no) ^ "] [" ^ cur_privilege ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(h) ^ ") <no-decode>");
-                handle_decode_exception(EXTZ(h));
+                instbits = EXTZ(h);
+                handle_illegal();
                 (false, true)
               },
               Some(ast) => {
@@ -77,7 +78,8 @@ function step(step_no) = {
             match decode(w) {
               None() => {
                 print("[" ^ string_of_int(step_no) ^ "] [" ^ cur_privilege ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(w) ^ ") <no-decode>");
-                handle_decode_exception(EXTZ(w));
+                instbits = EXTZ(w);
+                handle_illegal();
                 (false, true)
               },
               Some(ast) => {
diff --git a/riscv/riscv_sys.sail b/riscv/riscv_sys.sail
index 2669ee3f..818700b4 100644
--- a/riscv/riscv_sys.sail
+++ b/riscv/riscv_sys.sail
@@ -375,13 +375,17 @@ function lower_mstatus(m : Mstatus) -> Sstatus = {
 }
 
 function lift_sstatus(m : Mstatus, s : Sstatus) -> Mstatus = {
-  let m = update_SD(m, s.SD());
   // FIXME: This should be parameterized by a platform setting.  For now, match spike.
   // let m = update_UXL(m, s.UXL());
   let m = update_MXR(m, s.MXR());
   let m = update_SUM(m, s.SUM());
+
+  // FIXME: Should XS and FS check whether X and F|D are supported in misa?
   let m = update_XS(m, s.XS());
   let m = update_FS(m, s.FS());
+  let m = update_SD(m, extStatus_of_bits(m.FS()) == Dirty
+                     | extStatus_of_bits(m.XS()) == Dirty);
+
   let m = update_SPP(m, s.SPP());
   let m = update_SPIE(m, s.SPIE());
   let m = update_UPIE(m, s.UPIE());
@@ -990,21 +994,9 @@ function handle_mem_exception(addr : xlenbits, e : ExceptionType) -> unit = {
   nextPC = handle_exception(cur_privilege, CTL_TRAP(t), PC)
 }
 
-function handle_decode_exception(instbits : xlenbits) -> unit = {
-  let t : sync_exception = struct { trap    = E_Illegal_Instr,
-                                    excinfo = Some(instbits) };
-  nextPC = handle_exception(cur_privilege, CTL_TRAP(t), PC)
-}
-
 function handle_interrupt(i : InterruptType, del_priv : Privilege) -> unit =
   nextPC = handle_trap(del_priv, true, i, PC, None())
 
-function handle_illegal() -> unit = {
-  let t : sync_exception = struct { trap    = E_Illegal_Instr,
-                                    excinfo = None() };
-  nextPC = handle_exception(cur_privilege, CTL_TRAP(t), PC)
-}
-
 /* state state initialization */
 
 function init_sys() -> unit = {
diff --git a/riscv/riscv_types.sail b/riscv/riscv_types.sail
index d269356c..4cbc6f87 100644
--- a/riscv/riscv_types.sail
+++ b/riscv/riscv_types.sail
@@ -34,8 +34,11 @@ let sp   : regbits = 0b00010  /* x2, stack pointer  */
 
 /* program counter */
 
-register PC     : xlenbits
-register nextPC : xlenbits
+register PC       : xlenbits
+register nextPC   : xlenbits
+
+/* internal state to hold instruction bits for faulting instructions */
+register instbits : xlenbits
 
 /* register file and accessors */