Implement sret.

2 files changed, 17 insertions, 4 deletions

diff --git a/riscv/riscv.sail b/riscv/riscv.sail
index fe11af98..c18c1f44 100644
--- a/riscv/riscv.sail
+++ b/riscv/riscv.sail
@@ -383,6 +383,14 @@ function clause execute MRET() =
   nextPC = handle_exception_ctl(cur_privilege, CTL_MRET(), PC)
 
 /* ****************************************************************** */
+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)
+
+/* ****************************************************************** */
 union clause ast = EBREAK : unit
 
 function clause decode 0b000000000001 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 = Some(EBREAK())
diff --git a/riscv/riscv_sys.sail b/riscv/riscv_sys.sail
index d9fe53bb..cee3ede4 100644
--- a/riscv/riscv_sys.sail
+++ b/riscv/riscv_sys.sail
@@ -487,10 +487,8 @@ function tval(excinfo : option(xlenbits)) -> xlenbits = {
 
 union ctl_result = {
   CTL_TRAP : sync_exception,
-/* TODO:
-  CTL_URET,
-  CTL_SRET,
-*/
+/* TODO: CTL_URET */
+  CTL_SRET : unit,
   CTL_MRET : unit
 }
 
@@ -550,6 +548,13 @@ function handle_exception_ctl(cur_priv : Privilege, ctl : ctl_result,
       cur_privilege   = privLevel_of_bits(mstatus.MPP());
       mstatus->MPP()  = privLevel_to_bits(User);
       mepc
+    },
+    (_, CTL_SRET())  => {
+      mstatus->SIE()  = mstatus.SPIE();
+      mstatus->SPIE() = true;
+      cur_privilege   = if mstatus.SPP() == true then Supervisor else User;
+      mstatus->SPP()  = false;
+      sepc
     }
   }