summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--riscv/main.sail4
-rw-r--r--riscv/riscv.sail10
-rw-r--r--riscv/riscv_step.sail5
-rw-r--r--riscv/riscv_sys.sail50
4 files changed, 38 insertions, 31 deletions
diff --git a/riscv/main.sail b/riscv/main.sail
index 80a637a0..6337826e 100644
--- a/riscv/main.sail
+++ b/riscv/main.sail
@@ -35,7 +35,7 @@ function fetch_and_execute () =
if (misa.C() == 0b0 & (instr_sz == 2)) then {
let t : sync_exception = struct { trap = E_Illegal_Instr,
excinfo = Some(cur_inst) } in
- nextPC = handle_exception_ctl(cur_privilege, CTL_TRAP(t), PC)
+ nextPC = handle_exception(cur_privilege, CTL_TRAP(t), PC)
} else {
nextPC = PC + instr_sz;
match instr_ast {
@@ -47,7 +47,7 @@ function fetch_and_execute () =
MemException(e) => {
let t : sync_exception = struct { trap = e,
excinfo = Some(PC) } in
- nextPC = handle_exception_ctl(cur_privilege, CTL_TRAP(t), PC)
+ nextPC = handle_exception(cur_privilege, CTL_TRAP(t), PC)
}
};
let tohost_val = __ReadRAM(64, 4, 0x0000_0000_0000_0000, tohost);
diff --git a/riscv/riscv.sail b/riscv/riscv.sail
index d4be6eb4..2653269e 100644
--- a/riscv/riscv.sail
+++ b/riscv/riscv.sail
@@ -530,7 +530,7 @@ function clause execute ECALL() =
Machine => E_M_EnvCall
},
excinfo = (None() : option(xlenbits)) } in
- nextPC = handle_exception_ctl(cur_privilege, CTL_TRAP(t), PC)
+ nextPC = handle_exception(cur_privilege, CTL_TRAP(t), PC)
function clause print_insn (ECALL()) =
"ecall"
@@ -541,7 +541,7 @@ union clause ast = MRET : unit
function clause decode 0b0011000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 = Some(MRET())
function clause execute MRET() =
- nextPC = handle_exception_ctl(cur_privilege, CTL_MRET(), PC)
+ nextPC = handle_exception(cur_privilege, CTL_MRET(), PC)
function clause print_insn (MRET()) =
"mret"
@@ -552,7 +552,7 @@ union clause ast = SRET : unit
function clause decode 0b0001000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 = Some(MRET())
function clause execute SRET() =
- nextPC = handle_exception_ctl(cur_privilege, CTL_SRET(), PC)
+ nextPC = handle_exception(cur_privilege, CTL_SRET(), PC)
function clause print_insn (SRET()) =
"sret"
@@ -855,7 +855,7 @@ function clause execute CSR(csr, rs1, rd, is_imm, op) =
let t : sync_exception =
struct { trap = E_Illegal_Instr,
excinfo = Some (instr) } in
- nextPC = handle_exception_ctl(cur_privilege, CTL_TRAP(t), PC)
+ nextPC = handle_exception(cur_privilege, CTL_TRAP(t), PC)
} else {
let csr_val = readCSR(csr); /* could have side-effects, so technically shouldn't perform for CSRW[I] with rd == 0 */
if isWrite then {
@@ -904,7 +904,7 @@ function clause execute ILLEGAL() = {
let t : sync_exception =
struct { trap = E_Illegal_Instr,
excinfo = Some (EXTZ(0b0)) } in
- nextPC = handle_exception_ctl(cur_privilege, CTL_TRAP(t), PC)
+ nextPC = handle_exception(cur_privilege, CTL_TRAP(t), PC)
}
function clause print_insn (ILLEGAL()) =
diff --git a/riscv/riscv_step.sail b/riscv/riscv_step.sail
index ca0e102a..e670e2b8 100644
--- a/riscv/riscv_step.sail
+++ b/riscv/riscv_step.sail
@@ -46,9 +46,8 @@ function step() = {
tick_clock();
match curInterrupt(mip, mie, mideleg) {
- Some(intr, priv) => {
- ()
- },
+ Some(intr, priv) =>
+ handle_interrupt(intr, priv),
None() => {
match fetch() {
F_Error(e, addr) => handle_mem_exception(addr, e),
diff --git a/riscv/riscv_sys.sail b/riscv/riscv_sys.sail
index e692e62d..89beea49 100644
--- a/riscv/riscv_sys.sail
+++ b/riscv/riscv_sys.sail
@@ -610,26 +610,26 @@ function tval(excinfo : option(xlenbits)) -> xlenbits = {
union ctl_result = {
CTL_TRAP : sync_exception,
-/* TODO: CTL_URET */
+ CTL_INTR : (InterruptType, Privilege),
CTL_SRET : unit,
CTL_MRET : unit
+/* TODO: CTL_URET */
}
-/* handle exceptional ctl flow by updating nextPC */
+/* handle exceptional ctl flow by updating nextPC and operating privilege */
-function handle_trap(curp : Privilege, e : sync_exception,
- pc : xlenbits) -> xlenbits = {
- let priv = exception_delegatee(e.trap, curp);
- cur_privilege = priv;
- match (priv) {
+function handle_trap(del_priv : Privilege, intr : bool, c : exc_code, pc : xlenbits, info : option(xlenbits))
+ -> xlenbits = {
+ cur_privilege = del_priv;
+ match (del_priv) {
Machine => {
- mcause->IsInterrupt() = false;
- mcause->Cause() = EXTZ(exceptionType_to_bits(e.trap));
+ mcause->IsInterrupt() = intr;
+ mcause->Cause() = EXTZ(c);
mstatus->MPIE() = mstatus.MIE();
mstatus->MIE() = false;
- mstatus->MPP() = privLevel_to_bits(curp);
- mtval = tval(e.excinfo);
+ mstatus->MPP() = privLevel_to_bits(del_priv);
+ mtval = tval(info);
mepc = pc;
match tvec_addr(mtvec, mcause) {
@@ -638,17 +638,17 @@ function handle_trap(curp : Privilege, e : sync_exception,
}
},
Supervisor => {
- scause->IsInterrupt() = false;
- scause->Cause() = EXTZ(exceptionType_to_bits(e.trap));
+ scause->IsInterrupt() = intr;
+ scause->Cause() = EXTZ(c);
mstatus->SPIE() = mstatus.SIE();
mstatus->SIE() = false;
- mstatus->SPP() = match (curp) {
+ mstatus->SPP() = match (del_priv) {
User => false,
Supervisor => true,
Machine => internal_error("invalid privilege for s-mode trap")
};
- stval = tval(e.excinfo);
+ stval = tval(info);
sepc = pc;
match tvec_addr(stvec, scause) {
@@ -661,10 +661,15 @@ function handle_trap(curp : Privilege, e : sync_exception,
}
}
-function handle_exception_ctl(cur_priv : Privilege, ctl : ctl_result,
- pc: xlenbits) -> xlenbits =
+function handle_exception(cur_priv : Privilege, ctl : ctl_result,
+ pc: xlenbits) -> xlenbits =
match (cur_priv, ctl) {
- (_, CTL_TRAP(e)) => handle_trap(cur_priv, e, pc),
+ (_, CTL_TRAP(e)) => {
+ let del_priv = exception_delegatee(e.trap, cur_priv);
+ handle_trap(del_priv, false, e.trap, pc, e.excinfo)
+ },
+ (_, CTL_INTR(intr, del_priv)) =>
+ handle_trap(del_priv, true, intr, pc, None()),
(_, CTL_MRET()) => {
mstatus->MIE() = mstatus.MPIE();
mstatus->MPIE() = true;
@@ -684,15 +689,18 @@ function handle_exception_ctl(cur_priv : Privilege, ctl : ctl_result,
function handle_mem_exception(addr : xlenbits, e : ExceptionType) -> unit = {
let t : sync_exception = struct { trap = e,
excinfo = Some(addr) } in
- nextPC = handle_exception_ctl(cur_privilege, CTL_TRAP(t), PC)
+ nextPC = handle_exception(cur_privilege, CTL_TRAP(t), PC)
}
function handle_decode_exception(instbits : xlenbits) -> unit = {
- let t : sync_exception = struct { trap = E_Illegal_Instr,
+ let t : sync_exception = struct { trap = E_Illegal_Instr,
excinfo = Some(instbits) };
- nextPC = handle_exception_ctl(cur_privilege, CTL_TRAP(t), PC)
+ nextPC = handle_exception(cur_privilege, CTL_TRAP(t), PC)
}
+function handle_interrupt(i : InterruptType, del_priv : Privilege) -> unit =
+ nextPC = handle_trap(del_priv, false, i, PC, None())
+
function init_sys() -> unit = {
cur_privilege = Machine;
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 23:00:08 +0000