summaryrefslogtreecommitdiff
path: root/mips
diff options
context:
space:
mode:
authorRobert Norton2016-04-28 14:54:57 +0100
committerRobert Norton2016-04-28 14:55:04 +0100
commitef3deb63b3eead7e3b3ec826fd3d4f5695d642df (patch)
tree1898b9877ef98523925dfcf155b718626f1622e2 /mips
parentebea637489446114fb95863db861accf14a6b393 (diff)
implement (hopefully) correct exception behaviour wrt PCC/EPCC. Required shuffling function names and adding a hook in ERET.
Diffstat (limited to 'mips')
-rw-r--r--mips/mips_insts.sail1
-rw-r--r--mips/mips_prelude.sail4
-rw-r--r--mips/mips_wrappers.sail4
3 files changed, 8 insertions, 1 deletions
diff --git a/mips/mips_insts.sail b/mips/mips_insts.sail
index 26ef9fae..16af5c22 100644
--- a/mips/mips_insts.sail
+++ b/mips/mips_insts.sail
@@ -1393,6 +1393,7 @@ function clause decode (0b010000 : 0b1 : 0b0000000000000000000 : 0b011000) =
Some(ERET)
function clause execute (ERET) =
{
+ ERETHook();
if (CP0Status.ERL == bitone) then
{
nextPC := CP0ErrorEPC;
diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail
index 801802de..9161b929 100644
--- a/mips/mips_prelude.sail
+++ b/mips/mips_prelude.sail
@@ -146,7 +146,9 @@ function (bit[5]) ExceptionCode ((Exception) ex) =
}
-function unit SignalException ((Exception) ex) =
+val Exception -> unit effect {rreg, wreg} SignalException
+
+function unit SignalExceptionMIPS ((Exception) ex) =
{
(* Only update EPC and BD if not already in EXL mode *)
if (~ (CP0Status.EXL)) then
diff --git a/mips/mips_wrappers.sail b/mips/mips_wrappers.sail
index f9530b25..110b551d 100644
--- a/mips/mips_wrappers.sail
+++ b/mips/mips_wrappers.sail
@@ -7,3 +7,7 @@ function bit[64] addrWrapper((bit[64]) addr, (MemAccessType) accessType, (WordTy
function (option<Exception>, option<bit[64]>) TranslateAddress ((bit[64]) vAddr, (MemAccessType) accessType) =
TLBTranslate(vAddr, accessType)
+
+function unit SignalException ((Exception) ex) = SignalExceptionMIPS(ex)
+
+function unit ERETHook() = ()