Update riscv to use the new system definitions, remove duplicates.

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,