Factor out sync_exception to fix dependencies in cheri, and similarly split out pc access.

5 files changed, 28 insertions, 28 deletions

diff --git a/Makefile b/Makefile
index a4ad166..8f666b6 100644
--- a/Makefile
+++ b/Makefile
@@ -27,9 +27,10 @@ SAIL_RMEM_INST_SRCS = riscv_insts_begin.sail $(SAIL_RMEM_INST) riscv_insts_end.s
 # System and platform sources
 SAIL_SYS_SRCS =  riscv_csr_map.sail
 SAIL_SYS_SRCS += riscv_next_regs.sail
-SAIL_SYS_SRCS += riscv_sys_exceptions.sail
-SAIL_SYS_SRCS += riscv_next_control.sail
-SAIL_SYS_SRCS += riscv_sys_control.sail
+SAIL_SYS_SRCS += riscv_sys_exceptions.sail  # default basic helpers for exception handling
+SAIL_SYS_SRCS += riscv_sync_exception.sail  # define the exception structure used in the model
+SAIL_SYS_SRCS += riscv_next_control.sail    # helpers for the 'N' extension
+SAIL_SYS_SRCS += riscv_sys_control.sail     # general exception handling
 
 SAIL_RV32_VM_SRCS = riscv_vmem_sv32.sail riscv_vmem_rv32.sail
 SAIL_RV64_VM_SRCS = riscv_vmem_sv39.sail riscv_vmem_sv48.sail riscv_vmem_rv64.sail
@@ -43,7 +44,7 @@ endif
 
 # Non-instruction sources
 PRELUDE = prelude.sail prelude_mapping.sail $(SAIL_XLEN) prelude_mem_metadata.sail prelude_mem.sail
-SAIL_REGS_SRCS = riscv_reg_type.sail riscv_regs.sail riscv_sys_regs.sail riscv_ext_regs.sail $(SAIL_CHECK_SRCS)
+SAIL_REGS_SRCS = riscv_reg_type.sail riscv_regs.sail riscv_pc_access.sail riscv_sys_regs.sail riscv_ext_regs.sail $(SAIL_CHECK_SRCS)
 SAIL_ARCH_SRCS = $(PRELUDE) riscv_types.sail $(SAIL_REGS_SRCS) $(SAIL_SYS_SRCS) riscv_platform.sail
 SAIL_ARCH_SRCS += riscv_mem.sail $(SAIL_VM_SRCS)
 SAIL_ARCH_RVFI_SRCS = $(PRELUDE) rvfi_dii.sail riscv_types.sail $(SAIL_REGS_SRCS) $(SAIL_SYS_SRCS) riscv_platform.sail riscv_mem.sail $(SAIL_VM_SRCS)
diff --git a/model/riscv_addr_checks.sail b/model/riscv_addr_checks.sail
index 2471075..25b6396 100644
--- a/model/riscv_addr_checks.sail
+++ b/model/riscv_addr_checks.sail
@@ -53,20 +53,3 @@ function ext_data_get_addr(base : regbits, offset : xlenbits, acc : AccessType,
 
 function ext_handle_data_check_error(err : ext_data_addr_error) -> unit =
   ()
-
-/* accessors for default architectural addresses, for use from within instructions */
-/* FIXME: these don't really belong in this file. */
-/* FIXME: see note in cheri_addr_checks.sail */
-
-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
-}
diff --git a/model/riscv_pc_access.sail b/model/riscv_pc_access.sail
new file mode 100644
index 0000000..a51e627
--- /dev/null
+++ b/model/riscv_pc_access.sail
@@ -0,0 +1,15 @@
+/* accessors for default architectural addresses, for use from within instructions */
+/* FIXME: see note in cheri_addr_checks.sail */
+
+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
+}
diff --git a/model/riscv_sync_exception.sail b/model/riscv_sync_exception.sail
new file mode 100644
index 0000000..208d518
--- /dev/null
+++ b/model/riscv_sync_exception.sail
@@ -0,0 +1,7 @@
+/* model context for synchronous exceptions, parameterized for extensions */
+
+struct sync_exception = {
+  trap    : ExceptionType,
+  excinfo : option(xlenbits),
+  ext     : option(ext_exception)   /* for extensions */
+}
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index d37ffc9..52111f1 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -244,13 +244,7 @@ function dispatchInterrupt(priv : Privilege) -> option((InterruptType, Privilege
   }
 }
 
-/* model context for synchronous exceptions, parameterized for extensions */
-
-struct sync_exception = {
-  trap    : ExceptionType,
-  excinfo : option(xlenbits),
-  ext     : option(ext_exception)   /* for extensions */
-}
+/* types of privilege transitions */
 
 union ctl_result = {
   CTL_TRAP : sync_exception,