4 files changed, 37 insertions, 19 deletions
diff --git a/riscv/Makefile b/riscv/Makefile
index f4a7d8b5..e6bbbd5c 100644
--- a/riscv/Makefile
+++ b/riscv/Makefile
@@ -1,6 +1,15 @@
-SAIL_INSTS = riscv.sail
-SAIL_INST_SRCS = riscv_insts_begin.sail $(SAIL_INSTS) riscv_insts_end.sail
-SAIL_SRCS = prelude.sail riscv_types.sail riscv_sys.sail riscv_platform.sail riscv_mem.sail riscv_vmem.sail $(SAIL_INST_SRCS) riscv_step.sail riscv_analysis.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
diff --git a/riscv/riscv.sail b/riscv/riscv.sail
index c0c1d6e2..47d714f5 100644
--- a/riscv/riscv.sail
+++ b/riscv/riscv.sail
@@ -61,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)
 
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
+}