diff options
Diffstat (limited to 'mips')
| -rw-r--r-- | mips/mips_insts.sail | 40 | ||||
| -rw-r--r-- | mips/mips_prelude.sail | 27 | ||||
| -rw-r--r-- | mips/mips_wrappers.sail | 4 |
3 files changed, 62 insertions, 9 deletions
diff --git a/mips/mips_insts.sail b/mips/mips_insts.sail index 722e3d00..d8a45730 100644 --- a/mips/mips_insts.sail +++ b/mips/mips_insts.sail @@ -1286,8 +1286,8 @@ function clause execute(SDR(base, rt, offset)) = union ast member regregimm16 CACHE function clause decode (0b101111 : (regno) base : (regno) op : (imm16) imm) = Some(CACHE(base, op, imm)) -function clause execute (CACHE(base, op, imm)) = - () (* XXX NOP *) +function clause execute (CACHE(base, op, imm)) = + checkCP0Access () (* pretty much a NOP because no caches *) (* PREF - prefetching into (non-existent) caches *) @@ -1317,7 +1317,8 @@ function clause decode (0b010000 : 0b00000 : (regno) rt : (regno) rd : 0b0000000 Some(MFC0(rt, rd, sel, false)) (* MFC0 *) function clause decode (0b010000 : 0b00001 : (regno) rt : (regno) rd : 0b00000000 : (bit[3]) sel) = Some(MFC0(rt, rd, sel, true)) (* DMFC0 *) -function clause execute (MFC0(rt, rd, sel, double)) = +function clause execute (MFC0(rt, rd, sel, double)) = { + checkCP0Access(); let (bit[64]) result = switch (rd, sel) { case (0b00000,0b000) -> 0 (* 0, TLB Index *) @@ -1327,10 +1328,10 @@ function clause execute (MFC0(rt, rd, sel, double)) = case (0b00100,0b000) -> 0 (* 4, TLB Context *) case (0b00101,0b000) -> 0 (* 5, TLB PageMask *) case (0b00110,0b000) -> 0 (* 6, TLB Wired *) - case (0b00111,0b000) -> 0 (* 6, HWREna *) + case (0b00111,0b000) -> EXTZ(CP0HWREna) (* 6, HWREna *) case (0b01000,0b000) -> CP0BadVAddr (* 8, BadVAddr reg *) case (0b01000,0b001) -> 0 (* 8, BadInstr reg XXX TODO *) - case (0b01001,0b000) -> 0 (* 9, Count reg XXX TODO *) + case (0b01001,0b000) -> EXTZ(CP0Count) (* 9, Count reg *) case (0b01010,0b000) -> 0 (* 10, TLB EntryHi *) case (0b01011,0b000) -> EXTZ(CP0Compare) (* 11, Compare reg *) case (0b01100,0b000) -> EXTZ(CP0Status) (* 12, Status reg *) @@ -1356,20 +1357,24 @@ function clause execute (MFC0(rt, rd, sel, double)) = case _ -> {exit (SignalException(ResI)); 0} } in wGPR(rt) := if (double) then result else EXTS(result[31..0]) - +} union ast member (regno, regno, bit[3], bool) MTC0 function clause decode (0b010000 : 0b00100 : (regno) rt : (regno) rd : 0b00000000 : (bit[3]) sel) = Some(MTC0(rt, rd, sel, false)) (* MTC0 *) function clause decode (0b010000 : 0b00101 : (regno) rt : (regno) rd : 0b00000000 : (bit[3]) sel) = Some(MTC0(rt, rd, sel, true)) (* DMTC0 *) -function clause execute (MTC0(rt, rd, sel, double)) = +function clause execute (MTC0(rt, rd, sel, double)) = { + checkCP0Access(); let reg_val = (rGPR(rt)) in switch (rd, sel) { + case (0b00100,0b010) -> CP0UserLocal := reg_val + case (0b00111,0b000) -> CP0HWREna := (reg_val[31..30] : 0b00000000000000000000000000 : reg_val[4..0]) + case (0b01001,0b000) -> CP0Count := reg_val[31..0] case (0b01011,0b000) -> { (* 11, sel 0: Compare reg *) CP0Compare := reg_val[31..0]; - (CP0Cause.IP)[8] := 0 + (CP0Cause.IP)[15] := 0 } case (0b01100,0b000) -> { (* 12 Status *) (CP0Status.CU) := reg_val[31..28]; @@ -1391,12 +1396,31 @@ function clause execute (MTC0(rt, rd, sel, double)) = case (0b11110,0b000) -> CP0ErrorEPC := reg_val (* 30, ErrorEPC *) case _ -> exit (SignalException(ResI)) } +} + +union ast member (regno, regno) RDHWR +function clause decode (0b011111 : 0b00000 : (regno) rt : (regno) rd : 0b00000 : 0b111011) = Some(RDHWR(rt, rd)) +function clause execute (RDHWR(rt, rd)) = { + let accessLevel = getAccessLevel() in + if ((accessLevel != Kernel) & (~((CP0Status.CU)[0])) & ~(CP0HWREna[rd])) then + exit (SignalException(ResI)); + let (bit[64]) temp = switch (rd) { + case 0b00000 -> EXTZ([bitzero]) (* CPUNum *) + case 0b00001 -> EXTZ([bitzero]) (* SYNCI_step *) + case 0b00010 -> EXTZ(CP0Count) (* Count *) + case 0b00011 -> EXTZ([bitone]) (* Count resolution *) + case 0b11101 -> CP0UserLocal (* User local register *) + case _ -> exit (SignalException(ResI)) + } in + wGPR(rt) := temp; +} union ast member unit ERET function clause decode (0b010000 : 0b1 : 0b0000000000000000000 : 0b011000) = Some(ERET) function clause execute (ERET) = { + checkCP0Access(); ERETHook(); CP0LLBit := 0b0; if (CP0Status.ERL == bitone) then diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail index a8d3f8d5..28afb156 100644 --- a/mips/mips_prelude.sail +++ b/mips/mips_prelude.sail @@ -30,6 +30,10 @@ register (bit[64]) CP0ErrorEPC register (bit[1]) CP0LLBit register (bit[64]) CP0LLAddr register (bit[64]) CP0BadVAddr +register (bit[32]) CP0Count +register (bit[32]) CP0Compare +register (bit[32]) CP0HWREna +register (bit[64]) CP0UserLocal typedef StatusReg = register bits [31:0] { 31 .. 28 : CU; (* co-processor enable bits *) @@ -208,6 +212,29 @@ function AccessLevel getAccessLevel() = case _ -> User (* behaviour undefined, assume user *) } +function unit checkCP0Access () = + { + let accessLevel = getAccessLevel() in + if ((accessLevel != Kernel) & (~((CP0Status.CU)[0]))) then + { + (CP0Cause.CE) := 0b00; + exit (SignalException(CpU)); + } + } + +function unit incrementCP0Count() = { + CP0Count := (CP0Count + 1); + if (CP0Count == CP0Compare) then { + ((CP0Cause.IP)[15]) := bitone; + }; + (* XXX Sail does not allow reading fields here :-( *) + let (bit[32])status = CP0Status in + let (bit[32])cause = CP0Cause in + let (bit[8]) ims = (status[15..8]) in + let (bit[8]) ips = (cause[15..8]) in + if ((CP0Status.IE) & ((ips & ims) != 0x00)) then + exit (SignalException(Int)); +} function (bit[64]) TLBTranslate ((bit[64]) vAddr, (MemAccessType) accessType) = { diff --git a/mips/mips_wrappers.sail b/mips/mips_wrappers.sail index 25b8936b..7d9e73e6 100644 --- a/mips/mips_wrappers.sail +++ b/mips/mips_wrappers.sail @@ -5,11 +5,13 @@ function bool effect {wmem} MEMw_conditional_wrapper(addr, size, data) = function bit[64] addrWrapper((bit[64]) addr, (MemAccessType) accessType, (WordType) width) = addr -function (bit[64]) TranslateAddress ((bit[64]) vAddr, (MemAccessType) accessType) = +function (bit[64]) TranslateAddress ((bit[64]) vAddr, (MemAccessType) accessType) = { + incrementCP0Count(); if (vAddr[1..0] != 0b00) then (* bad PC alignment *) exit (SignalExceptionBadAddr(AdEL, vAddr)) else TLBTranslate(vAddr, accessType) +} function unit SignalException ((Exception) ex) = SignalExceptionMIPS(ex) |