From 3ce09b89ab7fe178250498b048d7de6c55f92c78 Mon Sep 17 00:00:00 2001
From: Tim Hutt <timothy.hutt@codasip.com>
Date: Thu, 31 Oct 2024 13:14:20 +0000
Subject: [PATCH] Move Sail exception code into its own file

This is not necessary for the model currently, however internally we wanted to use `internal_error` in a file that was before `riscv_types.sail`. Putting it in its own file makes that possible, and I think it's an organisational improvement even if the model currently does not need it.
---
 Makefile                |  2 +-
 model/riscv_errors.sail | 23 +++++++++++++++++++++++
 model/riscv_types.sail  | 17 -----------------
 3 files changed, 24 insertions(+), 18 deletions(-)
 create mode 100644 model/riscv_errors.sail

diff --git a/Makefile b/Makefile
index 119d4e321..e97081e29 100644
--- a/Makefile
+++ b/Makefile
@@ -94,7 +94,7 @@ SAIL_VM_SRCS += riscv_vmem_tlb.sail
 SAIL_VM_SRCS += riscv_vmem.sail
 
 # Non-instruction sources
-PRELUDE = prelude.sail $(SAIL_XLEN) $(SAIL_FLEN) $(SAIL_VLEN) prelude_mem_metadata.sail prelude_mem.sail
+PRELUDE = prelude.sail riscv_errors.sail $(SAIL_XLEN) $(SAIL_FLEN) $(SAIL_VLEN) prelude_mem_metadata.sail prelude_mem.sail
 
 SAIL_REGS_SRCS = riscv_reg_type.sail riscv_freg_type.sail riscv_regs.sail riscv_pc_access.sail riscv_sys_regs.sail
 SAIL_REGS_SRCS += riscv_pmp_regs.sail riscv_pmp_control.sail
diff --git a/model/riscv_errors.sail b/model/riscv_errors.sail
new file mode 100644
index 000000000..fd12bca1e
--- /dev/null
+++ b/model/riscv_errors.sail
@@ -0,0 +1,23 @@
+/*=======================================================================================*/
+/*  This Sail RISC-V architecture model, comprising all files and                        */
+/*  directories except where otherwise noted is subject the BSD                          */
+/*  two-clause license in the LICENSE file.                                              */
+/*                                                                                       */
+/*  SPDX-License-Identifier: BSD-2-Clause                                                */
+/*=======================================================================================*/
+
+/* model-internal exceptions */
+
+union exception = {
+  Error_not_implemented : string,
+  Error_internal_error  : unit
+}
+
+val not_implemented : forall ('a : Type). string -> 'a
+function not_implemented message = throw(Error_not_implemented(message))
+
+val internal_error : forall ('a : Type). (string, int, string) -> 'a
+function internal_error(file, line, s) = {
+    assert (false, file ^ ":" ^ dec_str(line) ^ ": " ^ s);
+    throw Error_internal_error()
+}
diff --git a/model/riscv_types.sail b/model/riscv_types.sail
index c333c4e17..4a4de0772 100644
--- a/model/riscv_types.sail
+++ b/model/riscv_types.sail
@@ -78,23 +78,6 @@ function arch_to_bits(a : Architecture) -> arch_xlen =
     RV128 => 0b11
   }
 
-
-/* model-internal exceptions */
-
-union exception = {
-  Error_not_implemented : string,
-  Error_internal_error  : unit
-}
-
-val not_implemented : forall ('a : Type). string -> 'a
-function not_implemented message = throw(Error_not_implemented(message))
-
-val internal_error : forall ('a : Type). (string, int, string) -> 'a
-function internal_error(file, line, s) = {
-    assert (false, file ^ ":" ^ dec_str(line) ^ ": " ^ s);
-    throw Error_internal_error()
-}
-
 /* privilege levels */
 
 type priv_level = bits(2)