More structured riscv trap vector handling.

3 files changed, 97 insertions, 63 deletions

diff --git a/riscv/riscv.sail b/riscv/riscv.sail
index a91bbbc5..34fc53fe 100644
--- a/riscv/riscv.sail
+++ b/riscv/riscv.sail
@@ -533,10 +533,10 @@ function readCSR csr: bits(12) -> xlenbits =
     0x302 => medeleg.bits(),
     0x303 => mideleg.bits(),
     0x304 => mie.bits(),
-    0x305 => mtvec,
+    0x305 => mtvec.bits(),
     0x340 => mscratch,
     0x341 => mepc,
-    0x342 => mcause,
+    0x342 => mcause.bits(),
     0x343 => mtval,
     0x344 => mip.bits(),
     _     => { print_bits("unhandled read to CSR ", csr);
@@ -544,15 +544,16 @@ function readCSR csr: bits(12) -> xlenbits =
   }
 
 function writeCSR (csr : bits(12), value : xlenbits) -> unit =
+  /* FIXME: need legalizers */
   match csr {
     0x300 => mstatus->bits() = value,
     0x302 => medeleg->bits() = value,
     0x303 => mideleg->bits() = value,
     0x304 => mie->bits() = value,
-    0x305 => mtvec = value,
+    0x305 => mtvec->bits() = value,
     0x340 => mscratch = value,
     0x341 => mepc = value,
-    0x342 => mcause = value,
+    0x342 => mcause->bits() = value,
     0x343 => mtval = value,
     0x344 => mip->bits() = value,
     _     => print_bits("unhandled write to CSR ", csr)
diff --git a/riscv/riscv_sys.sail b/riscv/riscv_sys.sail
index de209eec..1786766f 100644
--- a/riscv/riscv_sys.sail
+++ b/riscv/riscv_sys.sail
@@ -63,76 +63,73 @@ bitfield Mstatus : bits(64) = {
 }
 register mstatus : Mstatus
 
-bitfield Mip : bits(64) = {
-  MEIP : 11,
-  SEIP : 9,
-  UEIP : 8,
+/* interrupt registers */
 
-  MTIP : 7,
-  STIP : 5,
-  UTIP : 4,
+bitfield Minterrupts : bits(64) = {
+  MEI : 11, /* external interrupts */
+  SEI : 9,
+  UEI : 8,
 
-  MSIP : 3,
-  SSIP : 1,
-  USIP : 0,
+  MTI : 7,  /* timers interrupts */
+  STI : 5,
+  UTI : 4,
 
-}
-register mip : Mip
-
-bitfield Mie : bits(64) = {
-  MEIE : 11,
-  SEIE : 9,
-  UEIE : 8,
-
-  MTIE : 7,
-  STIE : 5,
-  UTIE : 4,
-
-  MSIE : 3,
-  SSIE : 1,
-  USIE : 0,
+  MSI : 3,  /* software interrupts */
+  SSI : 1,
+  USI : 0,
 
 }
-register mie : Mie
+register mip     : Minterrupts /* Pending */
+register mie     : Minterrupts /* Enabled */
+register mideleg : Minterrupts /* Delegation to S-mode */
 
-bitfield Mideleg : bits(64) = {
-  MEID : 6,
-  SEID : 5,
-  UEID : 4,
+/* exception registers */
 
-  MTID : 6,
-  STID : 5,
-  UTID : 4,
+bitfield Medeleg : bits(64) = {
+  SAMO_Page_Fault   : 15,
+  Load_Page_Fault   : 13,
+  Fetch_Page_Fault  : 12,
+  MEnvCall          : 10,
+  SEnvCall          : 9,
+  UEnvCall          : 8,
+  SAMO_Access_Fault : 7,
+  SAMO_Addr_Align   : 6,
+  Load_Access_Fault : 5,
+  Load_Addr_Align   : 4,
+  Breakpoint        : 3,
+  Illegal_Instr     : 2,
+  Fetch_Access_Fault: 1,
+  Fetch_Addr_Align  : 0
+}
+register medeleg : Medeleg  /* Delegation to S-mode */
 
-  MSID : 3,
-  SSID : 1,
-  USID : 0
+bitfield Mcause : bits(64) = {
+  IsInterrupt : 63,
+  Cause       : 62 .. 0
 }
-register mideleg : Mideleg
+register mcause : Mcause
 
-bitfield Medeleg : bits(64) = {
-  STORE_PAGE_FAULT  : 15,
-  LOAD_PAGE_FAULT   : 13,
-  FETCH_PAGE_FAULT  : 12,
-  MACHINE_ECALL     : 10,
-  SUPERVISOR_ECALL  : 9,
-  USER_ECALL        : 8,
-  STORE_ACCESS      : 7,
-  MISALIGNED_STORE  : 6,
-  LOAD_ACCESS       : 5,
-  MISALIGNED_LOAD   : 4,
-  BREAKPOINT        : 3,
-  ILLEGAL_INSTR     : 2,
-  FETCH_ACCESS      : 1,
-  MISALIGNED_FETCH  : 0
+bitfield Mtvec : bits(64) = {
+  Base : 63 .. 2,
+  Mode :  1 .. 0
+}
+register mtvec : Mtvec  /* Trap Vector */
+
+/* Interpreting the trap-vector address */
+function tvec_addr(m : Mtvec, c : Mcause) -> option(xlenbits) = {
+  let base : xlenbits = m.Base() @ 0b00;
+  match (trapVectorMode_of_bits(m.Mode())) {
+    TV_Direct => Some(base),
+    TV_Vector => if   mcause.IsInterrupt() == 0b1  /* FIXME: Why not already boolean? */
+                 then Some(base + (EXTZ(c.Cause()) << 0b10))
+                 else Some(base),
+    TV_Reserved => None()
+  }
 }
-register medeleg : Medeleg
 
-/* exception registers */
+/* auxiliary exception registers */
 register mepc : xlenbits
 register mtval : xlenbits
-register mtvec : xlenbits
-register mcause : xlenbits
 register mscratch : xlenbits
 
 /* other registers */
@@ -170,7 +167,9 @@ function handle_exception_ctl(cur_priv : Privilege, ctl : ctl_result,
   match (cur_priv, ctl) {
     (_, CTL_TRAP(e)) => {
       mepc            = pc;
-      mcause          = EXTZ(exceptionType_to_bits(e.trap));
+
+      mcause->IsInterrupt() = false;
+      mcause->Cause()       = EXTZ(exceptionType_to_bits(e.trap));
 
       mstatus->MPIE() = mstatus.MIE();
       mstatus->MIE()  = false;
@@ -255,7 +254,10 @@ function handle_exception_ctl(cur_priv : Privilege, ctl : ctl_result,
         _ => throw Error_internal_error() /* Don't expect ReservedExc0 etc. here */
       };
       /* TODO: make register read explicit */
-      mtvec
+      match (tvec_addr(mtvec, mcause)) {
+        Some(addr) => addr,
+        None()     => throw Error_internal_error()
+      }
     },
     (_, CTL_MRET()) => {
       mstatus->MIE()  = mstatus.MPIE();
diff --git a/riscv/riscv_types.sail b/riscv/riscv_types.sail
index f5942631..a858c317 100644
--- a/riscv/riscv_types.sail
+++ b/riscv/riscv_types.sail
@@ -157,6 +157,18 @@ function interruptType_to_bits (i) = {
   }
 }
 
+type tv_mode = bits(2)
+enum TrapVectorMode = {TV_Direct, TV_Vector, TV_Reserved}
+
+val cast trapVectorMode_of_bits : tv_mode -> TrapVectorMode
+function trapVectorMode_of_bits (m) = {
+  match (m) {
+    0b00 => TV_Direct,
+    0b01 => TV_Vector,
+    _    => TV_Reserved
+  }
+}
+
 /* other exceptions */
 
 union exception = {
@@ -178,9 +190,28 @@ function internal_error(s) = {
 /* extension context status */
 
 type ext_status = bits(2)
-
 enum ExtStatus = {Off, Initial, Clean, Dirty}
 
+val cast extStatus_to_bits : ExtStatus -> ext_status
+function extStatus_to_bits(e) = {
+  match (e) {
+    Off => 0b00,
+    Initial => 0b01,
+    Clean => 0b10,
+    Dirty => 0b11
+  }
+}
+
+val cast extStatus_of_bits : ext_status -> ExtStatus
+function extStatus_of_bits(e) = {
+  match (e) {
+    0b00 => Off,
+    0b01 => Initial,
+    0b10 => Clean,
+    0b11 => Dirty
+  }
+}
+
 /* supervisor-level address translation modes */
 
 type satp_mode = bits(4)