summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--riscv/main.sail2
-rw-r--r--riscv/riscv.sail9
-rw-r--r--riscv/riscv_sys.sail148
-rw-r--r--riscv/riscv_types.sail31
4 files changed, 70 insertions, 120 deletions
diff --git a/riscv/main.sail b/riscv/main.sail
index b2bda58f..b686f768 100644
--- a/riscv/main.sail
+++ b/riscv/main.sail
@@ -23,7 +23,7 @@ function fetch_and_execute () =
/* check whether a compressed instruction is legal. */
if (misa.C() == 0b0 & (instr_sz == 2)) then {
let t : sync_exception =
- struct { trap = Illegal_Instr,
+ struct { trap = E_Illegal_Instr,
excinfo = Some (EXTZ(instr)) } in
nextPC = handle_exception_ctl(cur_privilege, CTL_TRAP(t), PC)
} else {
diff --git a/riscv/riscv.sail b/riscv/riscv.sail
index 21c6fd64..a91bbbc5 100644
--- a/riscv/riscv.sail
+++ b/riscv/riscv.sail
@@ -367,8 +367,9 @@ function clause decode 0b000000000000 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 =
function clause execute ECALL() =
let t : sync_exception =
struct { trap = match (cur_privilege) {
- USER => User_ECall,
- MACHINE => Machine_ECall
+ User => E_U_EnvCall,
+ Supervisor => E_S_EnvCall,
+ Machine => E_M_EnvCall
},
excinfo = (None() : option(xlenbits)) } in
nextPC = handle_exception_ctl(cur_privilege, CTL_TRAP(t), PC)
@@ -573,7 +574,7 @@ function clause execute CSR(csr, rs1, rd, is_imm, op) =
if ~ (isCSRImplemented(csr) & haveCSRPriv(csr, isWrite)) then {
let instr : xlenbits = EXTZ(__RISCV_read(PC, 4));
let t : sync_exception =
- struct { trap = Illegal_Instr,
+ struct { trap = E_Illegal_Instr,
excinfo = Some (instr) } in
nextPC = handle_exception_ctl(cur_privilege, CTL_TRAP(t), PC)
} else {
@@ -608,7 +609,7 @@ function clause decodeCompressed (0b0000 @ 0b00000 @ 0b00000 @ 0b00) : bits(16)
function clause execute ILLEGAL() = {
let t : sync_exception =
- struct { trap = Illegal_Instr,
+ struct { trap = E_Illegal_Instr,
excinfo = Some (EXTZ(0b0)) } in
nextPC = handle_exception_ctl(cur_privilege, CTL_TRAP(t), PC)
}
diff --git a/riscv/riscv_sys.sail b/riscv/riscv_sys.sail
index 4a80bf3a..de209eec 100644
--- a/riscv/riscv_sys.sail
+++ b/riscv/riscv_sys.sail
@@ -1,69 +1,3 @@
-/* exception codes */
-
-enum Interrupts = {
- UserSWIntr,
- SupervisorSWIntr,
- ReservedIntr0,
- MachineSWIntr,
-
- UserTimerIntr,
- SupervisorTimerIntr,
- ReservedIntr1,
- MachineTimerIntr,
-
- UserExternalIntr,
- SupervisorExternalIntr,
- ReservedIntr2,
- MachineExternalIntr
-}
-
-enum ExceptionCode = {
- Misaligned_Fetch,
- Fetch_Access,
- Illegal_Instr,
- Breakpoint,
- Misaligned_Load,
-
- Load_Access,
- Misaligned_Store,
- Store_Access,
-
- User_ECall,
- Supervisor_ECall,
- ReservedExc0,
- Machine_ECall,
-
- Fetch_PageFault,
- Load_PageFault,
- ReservedExc1,
- Store_PageFault
-}
-
-val exc_to_bits : ExceptionCode -> bits(4)
-function exc_to_bits e =
- match (e) {
- Misaligned_Fetch => 0x0,
- Fetch_Access => 0x1,
- Illegal_Instr => 0x2,
- Breakpoint => 0x3,
- Misaligned_Load => 0x4,
-
- Load_Access => 0x5,
- Misaligned_Store => 0x6,
- Store_Access => 0x7,
-
- User_ECall => 0x8,
- Supervisor_ECall => 0x9,
- ReservedExc0 => 0xa,
- Machine_ECall => 0xb,
-
- Fetch_PageFault => 0xc,
- Load_PageFault => 0xd,
- ReservedExc1 => 0xe,
- Store_PageFaul => 0xf
- }
-
-
/* machine mode registers */
/* FIXME: currently we have only those used by riscv-tests. */
@@ -211,7 +145,7 @@ register mhartid : xlenbits
/* instruction control flow */
struct sync_exception = {
- trap : ExceptionCode,
+ trap : ExceptionType,
excinfo : option(xlenbits)
}
@@ -226,112 +160,96 @@ union ctl_result = {
/* privilege level */
-enum privilege = {
- MACHINE,
- USER
-}
-
-register cur_privilege : privilege
-
-function priv_to_bits(p : privilege) -> bits(2) =
- match (p) {
- USER => 0b00,
- MACHINE => 0b11
- }
-function bits_to_priv(b : bits(2)) -> privilege =
- match (b) {
- 0b00 => USER,
- 0b11 => MACHINE
- }
+register cur_privilege : Privilege
/* handle exceptional ctl flow by updating nextPC */
-function handle_exception_ctl(cur_priv : privilege, ctl : ctl_result,
+function handle_exception_ctl(cur_priv : Privilege, ctl : ctl_result,
pc: xlenbits) -> xlenbits =
/* TODO: check delegation */
match (cur_priv, ctl) {
(_, CTL_TRAP(e)) => {
mepc = pc;
- mcause = EXTZ(exc_to_bits(e.trap));
+ mcause = EXTZ(exceptionType_to_bits(e.trap));
mstatus->MPIE() = mstatus.MIE();
mstatus->MIE() = false;
- mstatus->MPP() = priv_to_bits(cur_priv);
- cur_privilege = MACHINE;
+ mstatus->MPP() = privLevel_to_bits(cur_priv);
+ cur_privilege = Machine;
match (e.trap) {
- Misaligned_Fetch => {
+ E_Fetch_Addr_Align => {
match (e.excinfo) {
Some(a) => mtval = a,
- None() => throw Error_internal_error()
+ None() => throw Error_internal_error()
}
},
- Fetch_Access => {
+ E_Fetch_Access_Fault => {
match (e.excinfo) {
Some(a) => mtval = a,
- None() => throw Error_internal_error()
+ None() => throw Error_internal_error()
}
},
- Illegal_Instr => {
+ E_Illegal_Instr => {
match (e.excinfo) {
Some(a) => mtval = a,
- None() => throw Error_internal_error()
+ None() => throw Error_internal_error()
}
},
- Breakpoint => not_implemented("breakpoint"),
+ E_Breakpoint => not_implemented("breakpoint"),
- Misaligned_Load => {
+ E_Load_Addr_Align => {
match (e.excinfo) {
Some(a) => mtval = a,
- None() => throw Error_internal_error()
+ None() => throw Error_internal_error()
}
},
- Load_Access => {
+ E_Load_Access_Fault => {
match (e.excinfo) {
Some(a) => mtval = a,
- None() => throw Error_internal_error()
+ None() => throw Error_internal_error()
}
},
- Misaligned_Store => {
+ E_SAMO_Addr_Align => {
match (e.excinfo) {
Some(a) => mtval = a,
- None() => throw Error_internal_error()
+ None() => throw Error_internal_error()
}
},
- Store_Access => {
+ E_SAMO_Access_Fault => {
match (e.excinfo) {
Some(a) => mtval = a,
- None() => throw Error_internal_error()
+ None() => throw Error_internal_error()
}
},
- User_ECall => {
+ E_U_EnvCall => {
mtval = EXTZ(0b0)
},
- Supervisor_ECall => {
+ E_S_EnvCall => {
mtval = EXTZ(0b0)
},
- Machine_ECall => {
+ E_M_EnvCall => {
mtval = EXTZ(0b0)
},
- Fetch_PageFault => {
+ E_Fetch_Page_Fault => {
match (e.excinfo) {
Some(a) => mtval = a,
- None() => throw Error_internal_error()
+ None() => throw Error_internal_error()
}
},
- Load_PageFault => {
+ E_Load_Page_Fault => {
match (e.excinfo) {
Some(a) => mtval = a,
- None() => throw Error_internal_error()
+ None() => throw Error_internal_error()
}
},
- Store_PageFault => {
+ E_SAMO_Page_Fault => {
match (e.excinfo) {
Some(a) => mtval = a,
- None() => throw Error_internal_error()
+ None() => throw Error_internal_error()
}
},
_ => throw Error_internal_error() /* Don't expect ReservedExc0 etc. here */
@@ -342,13 +260,13 @@ function handle_exception_ctl(cur_priv : privilege, ctl : ctl_result,
(_, CTL_MRET()) => {
mstatus->MIE() = mstatus.MPIE();
mstatus->MPIE() = true;
- cur_privilege = bits_to_priv(mstatus.MPP());
- mstatus->MPP() = priv_to_bits(USER);
+ cur_privilege = privLevel_of_bits(mstatus.MPP());
+ mstatus->MPP() = privLevel_to_bits(User);
mepc
}
}
function init_sys () : unit -> unit = {
- cur_privilege = MACHINE;
+ cur_privilege = Machine;
misa->C() = true;
}
diff --git a/riscv/riscv_types.sail b/riscv/riscv_types.sail
index 6c83d5b4..f5942631 100644
--- a/riscv/riscv_types.sail
+++ b/riscv/riscv_types.sail
@@ -67,6 +67,15 @@ function privLevel_to_bits (p) = {
}
}
+val cast privLevel_of_bits : priv_level -> Privilege
+function privLevel_of_bits (p) = {
+ match (p) {
+ 0b00 => User,
+ 0b01 => Supervisor,
+ 0b11 => Machine
+ }
+}
+
val cast privLevel_to_str : Privilege -> string
function privLevel_to_str (p) = {
match (p) {
@@ -99,6 +108,28 @@ enum ExceptionType = {
E_SAMO_Page_Fault
}
+val cast exceptionType_to_bits : ExceptionType -> exc_code
+function exceptionType_to_bits(e) = {
+ match (e) {
+ E_Fetch_Addr_Align => 0x0,
+ E_Fetch_Access_Fault => 0x1,
+ E_Illegal_Instr => 0x2,
+ E_Breakpoint => 0x3,
+ E_Load_Addr_Align => 0x4,
+ E_Load_Access_Fault => 0x5,
+ E_SAMO_Addr_Align => 0x6,
+ E_SAMO_Access_Fault => 0x7,
+ E_U_EnvCall => 0x8,
+ E_S_EnvCall => 0x9,
+ E_Reserved_10 => 0xa,
+ E_M_EnvCall => 0xb,
+ E_Fetch_Page_Fault => 0xc,
+ E_Load_Page_Fault => 0xd,
+ E_Reserved_14 => 0xe,
+ E_SAMO_Page_Fault => 0xf
+ }
+}
+
enum InterruptType = {
I_U_Software,
I_S_Software,
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 09:57:49 +0000