diff options
| -rw-r--r-- | cheri/cheri_prelude.sail | 1 | ||||
| -rw-r--r-- | mips/mips_insts.sail | 38 | ||||
| -rw-r--r-- | mips/mips_wrappers.sail | 2 |
3 files changed, 35 insertions, 6 deletions
diff --git a/cheri/cheri_prelude.sail b/cheri/cheri_prelude.sail index 0cb2a1f3..fd2e195d 100644 --- a/cheri/cheri_prelude.sail +++ b/cheri/cheri_prelude.sail @@ -119,6 +119,7 @@ let (CapStruct) null_cap = { let (nat) max_otype = 0xffffff def Nat cap_size_t = 32 (* cap size in bytes *) let ([:cap_size_t:]) cap_size = 32 +let have_cp2 = true function CapStruct capRegToCapStruct((CapReg) capReg) = { diff --git a/mips/mips_insts.sail b/mips/mips_insts.sail index ba0dc258..a265bd13 100644 --- a/mips/mips_insts.sail +++ b/mips/mips_insts.sail @@ -1344,13 +1344,39 @@ function clause execute (MFC0(rt, rd, sel, double)) = { case (0b01111,0b111) -> 0 (* 15, sel 7: CHERI thread ID *) case (0b10000,0b000) -> EXTZ(0b1 (* M *) (* 16, sel 0: Config0 *) : 0b000000000000000 (* Impl *) - : 0b1 (* BE *) - : 0b10 (* AT *) - : 0b000 (* AR *) - : 0b000 (* MT no MMU *) - : 0b0000 (* zero *) + : 0b1 (* BE *) + : 0b10 (* AT *) + : 0b000 (* AR *) + : 0b000 (* MT no MMU *) + : 0b0000 (* zero *) : 0b000) (* K0 TODO should be writable*) - case (0b10000,0b001) -> 0 (* 16, sel 1: Config1 *) + case (0b10000,0b001) -> EXTZ( (* 16, sel 1: Config1 *) + 0b1 (* M *) + : 0b000000 (* MMU size-1 *) + : 0b000 (* IS icache sets *) + : 0b000 (* IL icache lines *) + : 0b000 (* IA icache assoc. *) + : 0b000 (* DS dcache sets *) + : 0b000 (* DL dcache lines *) + : 0b000 (* DA dcache assoc. *) + : [have_cp2] (* C2 CP2 presence *) + : 0b0 (* MD MDMX implemented *) + : 0b0 (* PC performance counters *) + : 0b0 (* WR watch registers *) + : 0b0 (* CA 16e code compression *) + : 0b0 (* EP EJTAG *) + : 0b0) (* FP FPU present *) + case (0b10000,0b010) -> EXTZ( (* 16, sel 2: Config2 *) + 0b1 (* M *) + : 0b000 (* TU L3 control *) + : 0b0000 (* TS L3 sets *) + : 0b0000 (* TL L3 lines *) + : 0b0000 (* TA L3 assoc. *) + : 0b0000 (* SU L2 control *) + : 0b0000 (* SS L2 sets *) + : 0b0000 (* SL L2 lines *) + : 0b0000) (* SA L2 assoc. *) + case (0b10000,0b011) -> 0x0000000000002000 (* 16, sel 3: Config3 zero except for bit 13 == ulri *) case (0b10001,0b000) -> CP0LLAddr (* 17, sel 0: LLAddr *) case (0b10010,0b000) -> 0 (* 18, WatchLo *) case (0b10011,0b000) -> 0 (* 19, WatchHi *) diff --git a/mips/mips_wrappers.sail b/mips/mips_wrappers.sail index 7d9e73e6..08ce944b 100644 --- a/mips/mips_wrappers.sail +++ b/mips/mips_wrappers.sail @@ -13,6 +13,8 @@ function (bit[64]) TranslateAddress ((bit[64]) vAddr, (MemAccessType) accessType TLBTranslate(vAddr, accessType) } +let have_cp2 = false + function unit SignalException ((Exception) ex) = SignalExceptionMIPS(ex) function unit ERETHook() = () |