Tentative implemenatation of [MSU]TCC.

6 files changed, 23 insertions, 15 deletions

diff --git a/model/cheri_insts.sail b/model/cheri_insts.sail
index e7f5aab..4e9fbc9 100644
--- a/model/cheri_insts.sail
+++ b/model/cheri_insts.sail
@@ -262,7 +262,7 @@ function clause execute (CSpecialRW(cd, cs, idx)) =
       // write special cap
       match idx {
         1  => DDC = cs_val,
-        4  => UTCC = cs_val,
+        4  => UTCC = cs_val,   /* XXX should legalize mode? */
         6  => UScratchC = cs_val,
         7  => UEPCC = cs_val, /* XXX should legalize offset as per uepc etc? */
         12 => STCC = cs_val,
diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail
index 46df052..67d418a 100644
--- a/model/riscv_insts_zicsr.sail
+++ b/model/riscv_insts_zicsr.sail
@@ -26,7 +26,7 @@ function readCSR csr : csreg -> xlenbits = {
     0x302 => medeleg.bits(),
     0x303 => mideleg.bits(),
     0x304 => mie.bits(),
-    0x305 => mtvec.bits(),
+    0x305 => getCapOffsetBits(MTCC),
     0x306 => EXTZ(mcounteren.bits()),
     0x340 => mscratch,
     0x341 => getCapOffsetBits(MEPCC) & pc_alignment_mask(),
@@ -42,7 +42,7 @@ function readCSR csr : csreg -> xlenbits = {
     0x102 => sedeleg.bits(),
     0x103 => sideleg.bits(),
     0x104 => lower_mie(mie, mideleg).bits(),
-    0x105 => stvec.bits(),
+    0x105 => getCapOffsetBits(STCC),
     0x106 => EXTZ(scounteren.bits()),
     0x140 => sscratch,
     0x141 => getCapOffsetBits(SEPCC) & pc_alignment_mask(),
@@ -79,7 +79,9 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = {
     0x302 => { medeleg = legalize_medeleg(medeleg, value); Some(medeleg.bits()) },
     0x303 => { mideleg = legalize_mideleg(mideleg, value); Some(mideleg.bits()) },
     0x304 => { mie = legalize_mie(mie, value); Some(mie.bits()) },
-    0x305 => { mtvec = legalize_tvec(mtvec, value); Some(mtvec.bits()) },
+    0x305 => { let mtvec = legalize_tvec(Mk_Mtvec(getCapOffsetBits(MTCC)), value);
+               MTCC = setCapOffsetOrNull(MTCC, mtvec.bits());
+               Some(mtvec.bits()) },
     0x306 => { mcounteren = legalize_mcounteren(mcounteren, value); Some(EXTZ(mcounteren.bits())) },
     0x340 => { mscratch = value; Some(mscratch) },
     0x341 => { let mepc = legalize_xepc(value);
@@ -97,7 +99,9 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = {
     0x102 => { sedeleg = legalize_sedeleg(sedeleg, value); Some(sedeleg.bits()) },
     0x103 => { sideleg->bits() = value; Some(sideleg.bits()) }, /* TODO: does this need legalization? */
     0x104 => { mie = legalize_sie(mie, mideleg, value); Some(mie.bits()) },
-    0x105 => { stvec = legalize_tvec(stvec, value); Some(stvec.bits()) },
+    0x105 => { let stvec = legalize_tvec(Mk_Mtvec(getCapOffsetBits(STCC)), value);
+               STCC = setCapOffsetOrNull(STCC, stvec.bits());
+               Some(stvec.bits()) },
     0x106 => { scounteren = legalize_scounteren(scounteren, value); Some(EXTZ(scounteren.bits())) },
     0x140 => { sscratch = value; Some(sscratch) },
     0x141 => { let sepc = legalize_xepc(value);
diff --git a/model/riscv_next_control.sail b/model/riscv_next_control.sail
index 99bd176..2515743 100644
--- a/model/riscv_next_control.sail
+++ b/model/riscv_next_control.sail
@@ -18,7 +18,7 @@ function read_UExt_CSR csr : csreg -> option(xlenbits) = {
   match csr {
     0x000 => Some(lower_sstatus(lower_mstatus(mstatus)).bits()),
     0x004 => Some(lower_sie(lower_mie(mie, mideleg), sideleg).bits()),
-    0x005 => Some(utvec.bits()),
+    0x005 => Some(getCapOffsetBits(UTCC)),
     0x040 => Some(uscratch),
     0x041 => Some(getCapOffsetBits(UEPCC) & pc_alignment_mask()),
     0x042 => Some(ucause.bits()),
@@ -36,7 +36,9 @@ function write_UExt_CSR(csr : csreg, value : xlenbits) -> bool = {
     0x004 => { let sie = legalize_uie(lower_mie(mie, mideleg), sideleg, value);
                mie = lift_sie(mie, mideleg, sie);
                Some(mie.bits()) },
-    0x005 => { utvec = legalize_tvec(utvec, value); Some(utvec.bits()) },
+    0x005 => { let utvec = legalize_tvec(Mk_Mtvec(getCapOffsetBits(UTCC)), value);
+               UTCC = setCapOffsetOrNull(UTCC, utvec.bits());
+               Some(utvec.bits()) },
     0x040 => { uscratch = value; Some(uscratch) },
     0x041 => {let uepc = legalize_xepc(value);
               UEPCC = setCapOffsetOrNull(UEPCC, uepc);
diff --git a/model/riscv_next_regs.sail b/model/riscv_next_regs.sail
index 305404d..3c94625 100644
--- a/model/riscv_next_regs.sail
+++ b/model/riscv_next_regs.sail
@@ -76,7 +76,7 @@ function legalize_uie(s : Sinterrupts, d : Sinterrupts, v : xlenbits) -> Sinterr
   lift_uie(s, d, Mk_Uinterrupts(v))
 }
 
-register utvec    : Mtvec
+/*register utvec    : Mtvec*/
 register uscratch : xlenbits
 /*register uepc     : xlenbits*/
 register ucause   : Mcause
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index be5ddc4..89baee9 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -290,7 +290,8 @@ function handle_trap(del_priv : Privilege, intr : bool, c : exc_code, pc : xlenb
 
        print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits()));
 
-       match tvec_addr(mtvec, mcause) {
+       PCC = MTCC;
+       match tvec_addr(Mk_Mtvec(getCapOffsetBits(MTCC)), mcause) {
          Some(epc) => epc,
          None()    => internal_error("Invalid mtvec mode")
        }
@@ -318,11 +319,11 @@ function handle_trap(del_priv : Privilege, intr : bool, c : exc_code, pc : xlenb
 
        print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits()));
 
-       match tvec_addr(stvec, scause) {
+       PCC = STCC;
+       match tvec_addr(Mk_Mtvec(getCapOffsetBits(STCC)), scause) {
          Some(epc) => epc,
          None()    => internal_error("Invalid stvec mode")
        }
-
     },
     User => {
        //assert(haveUsrMode());
@@ -342,7 +343,8 @@ function handle_trap(del_priv : Privilege, intr : bool, c : exc_code, pc : xlenb
 
        print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits()));
 
-       match tvec_addr(utvec, ucause) {
+       PCC = UTCC;
+       match tvec_addr(Mk_Mtvec(getCapOffsetBits(UTCC)), ucause) {
          Some(epc) => epc,
          None()    => internal_error("Invalid utvec mode")
        }
@@ -434,7 +436,7 @@ function init_sys() -> unit = {
   mie->bits()     = EXTZ(0b0);
   mideleg->bits() = EXTZ(0b0);
   medeleg->bits() = EXTZ(0b0);
-  mtvec->bits()   = EXTZ(0b0);
+/*  mtvec->bits()   = EXTZ(0b0);*/
   mcause->bits()  = EXTZ(0b0);
 /*  mepc            = EXTZ(0b0);*/
   mtval           = EXTZ(0b0);
diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
index 524967a..3c6ccd9 100644
--- a/model/riscv_sys_regs.sail
+++ b/model/riscv_sys_regs.sail
@@ -254,7 +254,7 @@ bitfield Mtvec : bits(64) = {
   Base : 63 .. 2,
   Mode :  1 .. 0
 }
-register mtvec : Mtvec  /* Trap Vector */
+/*register mtvec : Mtvec x Trap Vector */
 
 function legalize_tvec(o : Mtvec, v : xlenbits) -> Mtvec = {
  let v = Mk_Mtvec(v);
@@ -527,7 +527,7 @@ function legalize_satp(a : Architecture, o : xlenbits, v : xlenbits) -> xlenbits
 }
 
 /* other supervisor state */
-register stvec    : Mtvec
+/*register stvec    : Mtvec*/
 register sscratch : xlenbits
 /*register sepc     : xlenbits*/
 register scause   : Mcause