4 files changed, 37 insertions, 38 deletions
diff --git a/riscv/Makefile b/riscv/Makefile
index 72abc5da..f4a7d8b5 100644
--- a/riscv/Makefile
+++ b/riscv/Makefile
@@ -1,4 +1,6 @@
-SAIL_SRCS = prelude.sail riscv_types.sail riscv_sys.sail riscv_platform.sail riscv_mem.sail riscv_vmem.sail riscv.sail riscv_step.sail riscv_analysis.sail
+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
 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 71ad0137..c0c1d6e2 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)
 
@@ -1585,14 +1559,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_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))