diff --git a/Makefile b/Makefile index c2a0b332f..113d35573 100644 --- a/Makefile +++ b/Makefile @@ -96,7 +96,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)