aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile6
-rw-r--r--model/riscv_insts_base.sail8
-rw-r--r--model/riscv_insts_next.sail2
-rw-r--r--model/riscv_platform.sail2
-rw-r--r--model/riscv_sys_control.sail14
5 files changed, 16 insertions, 16 deletions
diff --git a/Makefile b/Makefile
index 7683b1e..a4ad166 100644
--- a/Makefile
+++ b/Makefile
@@ -18,8 +18,8 @@ endif
# Instruction sources, depending on target
SAIL_CHECK_SRCS = riscv_addr_checks_common.sail riscv_addr_checks.sail
SAIL_DEFAULT_INST = riscv_insts_base.sail riscv_insts_aext.sail riscv_insts_cext.sail riscv_insts_mext.sail riscv_insts_zicsr.sail riscv_insts_next.sail
-SAIL_SEQ_INST = $(SAIL_CHECK_SRCS) $(SAIL_DEFAULT_INST) riscv_jalr_seq.sail
-SAIL_RMEM_INST = $(SAIL_CHECK_SRCS) $(SAIL_DEFAULT_INST) riscv_jalr_rmem.sail riscv_insts_rmem.sail
+SAIL_SEQ_INST = $(SAIL_DEFAULT_INST) riscv_jalr_seq.sail
+SAIL_RMEM_INST = $(SAIL_DEFAULT_INST) riscv_jalr_rmem.sail riscv_insts_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
@@ -43,7 +43,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_REGS_SRCS = riscv_reg_type.sail riscv_regs.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_insts_base.sail b/model/riscv_insts_base.sail
index 5819a81..7cf3044 100644
--- a/model/riscv_insts_base.sail
+++ b/model/riscv_insts_base.sail
@@ -658,7 +658,7 @@ function clause execute ECALL() = {
},
excinfo = (None() : option(xlenbits)),
ext = None() };
- nextPC = handle_exception(cur_privilege, CTL_TRAP(t), PC);
+ set_next_pc(exception_handler(cur_privilege, CTL_TRAP(t), PC));
false
}
@@ -672,7 +672,7 @@ mapping clause encdec = MRET()
function clause execute MRET() = {
if cur_privilege == Machine
- then nextPC = handle_exception(cur_privilege, CTL_MRET(), PC)
+ then set_next_pc(exception_handler(cur_privilege, CTL_MRET(), PC))
else handle_illegal();
false
}
@@ -690,10 +690,10 @@ function clause execute SRET() = {
User => handle_illegal(),
Supervisor => if (~ (haveSupMode ())) | mstatus.TSR() == true
then handle_illegal()
- else nextPC = handle_exception(cur_privilege, CTL_SRET(), PC),
+ else set_next_pc(exception_handler(cur_privilege, CTL_SRET(), PC)),
Machine => if (~ (haveSupMode ()))
then handle_illegal()
- else nextPC = handle_exception(cur_privilege, CTL_SRET(), PC)
+ else set_next_pc(exception_handler(cur_privilege, CTL_SRET(), PC))
};
false
}
diff --git a/model/riscv_insts_next.sail b/model/riscv_insts_next.sail
index 926a3b5..7b87826 100644
--- a/model/riscv_insts_next.sail
+++ b/model/riscv_insts_next.sail
@@ -9,7 +9,7 @@ mapping clause encdec = URET()
function clause execute URET() = {
if (~ (haveUsrMode()))
then handle_illegal()
- else nextPC = handle_exception(cur_privilege, CTL_URET(), PC);
+ else set_next_pc(exception_handler(cur_privilege, CTL_URET(), PC));
false
}
diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail
index d21e912..87fa425 100644
--- a/model/riscv_platform.sail
+++ b/model/riscv_platform.sail
@@ -353,7 +353,7 @@ function handle_illegal() -> unit = {
let t : sync_exception = struct { trap = E_Illegal_Instr,
excinfo = info,
ext = None() };
- nextPC = handle_exception(cur_privilege, CTL_TRAP(t), PC)
+ set_next_pc(exception_handler(cur_privilege, CTL_TRAP(t), PC))
}
/* Platform-specific wait-for-interrupt */
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index 5c72058..41fe13a 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -279,8 +279,8 @@ $endif
/* handle exceptional ctl flow by updating nextPC and operating privilege */
-function handle_trap(del_priv : Privilege, intr : bool, c : exc_code, pc : xlenbits, info : option(xlenbits), ext : option(ext_exception))
- -> xlenbits = {
+function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlenbits, info : option(xlenbits), ext : option(ext_exception))
+ -> xlenbits = {
rvfi_trap();
print_platform("handling " ^ (if intr then "int#" else "exc#")
^ BitStr(c) ^ " at priv " ^ del_priv ^ " with tval " ^ BitStr(tval(info)));
@@ -352,14 +352,14 @@ function handle_trap(del_priv : Privilege, intr : bool, c : exc_code, pc : xlenb
};
}
-function handle_exception(cur_priv : Privilege, ctl : ctl_result,
- pc: xlenbits) -> xlenbits = {
+function exception_handler(cur_priv : Privilege, ctl : ctl_result,
+ pc: xlenbits) -> xlenbits = {
match (cur_priv, ctl) {
(_, CTL_TRAP(e)) => {
let del_priv = exception_delegatee(e.trap, cur_priv);
print_platform("trapping from " ^ cur_priv ^ " to " ^ del_priv
^ " to handle " ^ e.trap);
- handle_trap(del_priv, false, e.trap, pc, e.excinfo, e.ext)
+ trap_handler(del_priv, false, e.trap, pc, e.excinfo, e.ext)
},
(_, CTL_MRET()) => {
let prev_priv = cur_privilege;
@@ -407,11 +407,11 @@ function handle_mem_exception(addr : xlenbits, e : ExceptionType) -> unit = {
let t : sync_exception = struct { trap = e,
excinfo = Some(addr),
ext = None() } in
- nextPC = handle_exception(cur_privilege, CTL_TRAP(t), PC)
+ set_next_pc(exception_handler(cur_privilege, CTL_TRAP(t), PC))
}
function handle_interrupt(i : InterruptType, del_priv : Privilege) -> unit =
- nextPC = handle_trap(del_priv, true, i, PC, None(), None())
+ set_next_pc(trap_handler(del_priv, true, i, PC, None(), None()))
/* state state initialization */
generated by cgit v1.1 at 2024-07-24 11:15:45 +0000