summaryrefslogtreecommitdiff
path: root/mips_new_tc
diff options
context:
space:
mode:
authorAlasdair Armstrong2017-07-13 16:42:57 +0100
committerAlasdair Armstrong2017-07-13 16:42:57 +0100
commit249079742b63d43cdc4c445de3229f594c6d59fc (patch)
tree97bdad0820cea632912b5c22e34bc91741cf1cd9 /mips_new_tc
parentc19b8e2b934149b6670f43d875d773115b08410e (diff)
Modified MIPS model so it typechecks with the new typechecker
Diffstat (limited to 'mips_new_tc')
-rw-r--r--mips_new_tc/mips_epilogue.sail2
-rw-r--r--mips_new_tc/mips_insts.sail362
-rw-r--r--mips_new_tc/mips_wrappers.sail12
3 files changed, 196 insertions, 180 deletions
diff --git a/mips_new_tc/mips_epilogue.sail b/mips_new_tc/mips_epilogue.sail
index 50993949..09ce7688 100644
--- a/mips_new_tc/mips_epilogue.sail
+++ b/mips_new_tc/mips_epilogue.sail
@@ -38,4 +38,4 @@ end decode
end execute
end ast
-function option<ast> supported_instructions (instr) = Some(instr)
+function option<ast> supported_instructions (ast) instr = Some(instr)
diff --git a/mips_new_tc/mips_insts.sail b/mips_new_tc/mips_insts.sail
index 19176c72..88c78e80 100644
--- a/mips_new_tc/mips_insts.sail
+++ b/mips_new_tc/mips_insts.sail
@@ -32,12 +32,12 @@
(* SUCH DAMAGE. *)
(*========================================================================*)
-(* misp_insts.sail: mips instruction decode and execute clauses and AST node
+(* misp_insts.sail: mips instruction decode and execute clauses and AST node
declarations *)
scattered typedef ast = const union
-val ast -> unit effect pure execute
+val ast -> unit effect {barr, eamem, escape, rmem, rreg, undef, wmv, wreg} execute
scattered function unit execute
val bit[32] -> option<ast> effect pure decode
@@ -47,13 +47,13 @@ scattered function option<ast> decode
(* [D]ADD[I][U] various forms of ADD *)
(**************************************************************************************)
-(* DADDIU Doubleword Add Immediate Unsigned --
- the simplest possible instruction, no undefined behaviour or exceptions
+(* DADDIU Doubleword Add Immediate Unsigned --
+ the simplest possible instruction, no undefined behaviour or exceptions
reg, reg, immediate *)
union ast member regregimm16 DADDIU
-function clause decode (0b011001 : (regno) rs : (regno) rt : (imm16) imm) =
+function clause decode (0b011001 : (regno) rs : (regno) rt : (imm16) imm) =
Some(DADDIU(rs, rt, imm))
function clause execute (DADDIU (rs, rt, imm)) =
@@ -66,7 +66,7 @@ function clause execute (DADDIU (rs, rt, imm)) =
union ast member regregreg DADDU
-function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101101) =
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101101) =
Some(DADDU(rs, rt, rd))
function clause execute (DADDU (rs, rt, rd)) =
@@ -79,7 +79,7 @@ function clause execute (DADDU (rs, rt, rd)) =
union ast member regregimm16 DADDI
-function clause decode (0b011000 : (regno) rs : (regno) rt : (imm16) imm) =
+function clause decode (0b011000 : (regno) rs : (regno) rt : (imm16) imm) =
Some(DADDI(rs, rt, imm))
function clause execute (DADDI (rs, rt, imm)) =
@@ -98,7 +98,7 @@ function clause execute (DADDI (rs, rt, imm)) =
union ast member regregreg DADD
-function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101100) =
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101100) =
Some(DADD(rs, rt, rd))
function clause execute (DADD (rs, rt, rd)) =
@@ -140,7 +140,7 @@ union ast member regregimm16 ADDI
function clause decode (0b001000 : (regno) rs : (regno) rt : (imm16) imm) =
Some(ADDI(rs, rt, imm))
-function clause execute (ADDI(rs, rt, imm)) =
+function clause execute (ADDI(rs, rt, imm)) =
{
(bit[64]) opA := rGPR(rs);
if NotWordVal(opA) then
@@ -160,7 +160,7 @@ union ast member regregreg ADDU
function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b100001) =
Some(ADDU(rs, rt, rd))
-function clause execute (ADDU(rs, rt, rd)) =
+function clause execute (ADDU(rs, rt, rd)) =
{
(bit[64]) opA := rGPR(rs);
(bit[64]) opB := rGPR(rt);
@@ -178,7 +178,7 @@ union ast member regregimm16 ADDIU
function clause decode (0b001001 : (regno) rs : (regno) rt : (imm16) imm) =
Some(ADDIU(rs, rt, imm))
-function clause execute (ADDIU(rs, rt, imm)) =
+function clause execute (ADDIU(rs, rt, imm)) =
{
(bit[64]) opA := rGPR(rs);
if NotWordVal(opA) then
@@ -195,7 +195,7 @@ function clause execute (ADDIU(rs, rt, imm)) =
union ast member regregreg DSUBU
-function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101111) =
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101111) =
Some(DSUBU(rs, rt, rd))
function clause execute (DSUBU (rs, rt, rd)) =
@@ -207,7 +207,7 @@ function clause execute (DSUBU (rs, rt, rd)) =
union ast member regregreg DSUB
-function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101110) =
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101110) =
Some(DSUB(rs, rt, rd))
function clause execute (DSUB (rs, rt, rd)) =
@@ -248,7 +248,7 @@ union ast member regregreg SUBU
function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b100011) =
Some(SUBU(rs, rt, rd))
-function clause execute (SUBU(rs, rt, rd)) =
+function clause execute (SUBU(rs, rt, rd)) =
{
(bit[64]) opA := rGPR(rs);
(bit[64]) opB := rGPR(rt);
@@ -265,7 +265,7 @@ function clause execute (SUBU(rs, rt, rd)) =
(* AND reg, reg, reg *)
union ast member regregreg AND
-function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b100100) =
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b100100) =
Some(AND(rs, rt, rd))
function clause execute (AND (rs, rt, rd)) =
@@ -276,7 +276,7 @@ function clause execute (AND (rs, rt, rd)) =
(* ANDI reg, reg, imm *)
union ast member regregimm16 ANDI
-function clause decode (0b001100 : (regno) rs : (regno) rt : (imm16) imm) =
+function clause decode (0b001100 : (regno) rs : (regno) rt : (imm16) imm) =
Some(ANDI(rs, rt, imm))
function clause execute (ANDI (rs, rt, imm)) =
{
@@ -286,7 +286,7 @@ function clause execute (ANDI (rs, rt, imm)) =
(* OR reg, reg, reg *)
union ast member regregreg OR
-function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b100101) =
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b100101) =
Some(OR(rs, rt, rd))
function clause execute (OR (rs, rt, rd)) =
{
@@ -296,7 +296,7 @@ function clause execute (OR (rs, rt, rd)) =
(* ORI reg, reg, imm *)
union ast member regregimm16 ORI
-function clause decode (0b001101 : (regno) rs : (regno) rt : (imm16) imm) =
+function clause decode (0b001101 : (regno) rs : (regno) rt : (imm16) imm) =
Some(ORI(rs, rt, imm))
function clause execute (ORI (rs, rt, imm)) =
{
@@ -306,7 +306,7 @@ function clause execute (ORI (rs, rt, imm)) =
(* NOR reg, reg, reg *)
union ast member regregreg NOR
-function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b100111) =
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b100111) =
Some(NOR(rs, rt, rd))
function clause execute (NOR (rs, rt, rd)) =
{
@@ -316,7 +316,7 @@ function clause execute (NOR (rs, rt, rd)) =
(* XOR reg, reg, reg *)
union ast member regregreg XOR
-function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b100110) =
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b100110) =
Some(XOR(rs, rt, rd))
function clause execute (XOR (rs, rt, rd)) =
{
@@ -325,7 +325,7 @@ function clause execute (XOR (rs, rt, rd)) =
(* XORI reg, reg, imm *)
union ast member regregimm16 XORI
-function clause decode (0b001110 : (regno) rs : (regno) rt : (imm16) imm) =
+function clause decode (0b001110 : (regno) rs : (regno) rt : (imm16) imm) =
Some(XORI(rs, rt, imm))
function clause execute (XORI (rs, rt, imm)) =
{
@@ -333,8 +333,8 @@ function clause execute (XORI (rs, rt, imm)) =
}
(* LUI reg, imm 32-bit load immediate into upper 16 bits *)
-union ast member (regno, imm16) LUI
-function clause decode (0b001111 : 0b00000 : (regno) rt : (imm16) imm) =
+union ast member (regno, imm16) LUI
+function clause decode (0b001111 : 0b00000 : (regno) rt : (imm16) imm) =
Some(LUI(rt, imm))
function clause execute (LUI (rt, imm)) =
{
@@ -348,18 +348,18 @@ function clause execute (LUI (rt, imm)) =
(* DSLL reg, reg, imm5 *)
union ast member regregreg DSLL
-function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (bit[5]) sa : 0b111000) =
+function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (bit[5]) sa : 0b111000) =
Some(DSLL(rt, rd, sa))
function clause execute (DSLL (rt, rd, sa)) =
{
-
+
wGPR(rd) := (rGPR(rt) << sa) (* make tuareg mode less blue >> *)
}
(* DSLL32 reg, reg, imm5 *)
union ast member regregreg DSLL32
-function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (bit[5]) sa : 0b111100) =
+function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (bit[5]) sa : 0b111100) =
Some(DSLL32(rt, rd, sa))
function clause execute (DSLL32 (rt, rd, sa)) =
{
@@ -369,12 +369,12 @@ function clause execute (DSLL32 (rt, rd, sa)) =
(* DSLLV reg, reg, reg *)
union ast member regregreg DSLLV
-function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b010100) =
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b010100) =
Some(DSLLV(rs, rt, rd))
function clause execute (DSLLV (rs, rt, rd)) =
{
wGPR(rd) := (rGPR(rt) << ((rGPR(rs))[5 .. 0])) (* make tuareg mode less blue >> *)
- (* alternative slicing based version of above
+ (* alternative slicing based version of above
sa := (rGPR(rt))[5 .. 0];
v := rGPR(rs);
wGPR(rd) := v[(63-sa) .. 0] : (0b0 ^^ sa) *)
@@ -383,24 +383,24 @@ function clause execute (DSLLV (rs, rt, rd)) =
(* DSRA arithmetic shift duplicating sign bit - reg, reg, imm5 *)
union ast member regregreg DSRA
-function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (bit[5]) sa : 0b111011) =
+function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (bit[5]) sa : 0b111011) =
Some(DSRA(rt, rd, sa))
function clause execute (DSRA (rt, rd, sa)) =
{
temp := rGPR(rt);
- wGPR(rd) := EXTS((temp[63] ^^ sa) : (temp[63 .. sa]))
+ wGPR(rd) := EXTZ((temp[63] ^^ sa) : (temp[63 .. sa]))
}
(* DSRA32 reg, reg, imm5 *)
union ast member regregreg DSRA32
-function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (bit[5]) sa : 0b111111) =
+function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (bit[5]) sa : 0b111111) =
Some(DSRA32(rt, rd, sa))
function clause execute (DSRA32 (rt, rd, sa)) =
{
temp := rGPR(rt);
sa32 := (0b1 : sa); (* sa+32 *)
- wGPR(rd) := EXTS((temp[63] ^^ sa32) : (temp[63 .. sa32]))
+ wGPR(rd) := EXTZ((temp[63] ^^ sa32) : (temp[63 .. sa32]))
}
(* DSRAV reg, reg, reg *)
@@ -411,42 +411,42 @@ function clause execute (DSRAV (rs, rt, rd)) =
{
temp := rGPR(rt);
sa := (rGPR(rs)) [5..0];
- wGPR(rd) := EXTS((temp[63] ^^ sa) : temp[63 .. sa])
+ wGPR(rd) := EXTZ((temp[63] ^^ sa) : temp[63 .. sa])
}
(* DSRL shift right logical - reg, reg, imm5 *)
union ast member regregreg DSRL
-function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (bit[5]) sa : 0b111010) =
+function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (bit[5]) sa : 0b111010) =
Some(DSRL(rt, rd, sa))
function clause execute (DSRL (rt, rd, sa)) =
{
temp := rGPR(rt);
- wGPR(rd) := EXTS((bitzero ^^ sa) : (temp[63 .. sa]))
+ wGPR(rd) := EXTZ((bitzero ^^ sa) : (temp[63 .. sa]))
}
(* DSRL32 reg, reg, imm5 *)
union ast member regregreg DSRL32
-function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (bit[5]) sa : 0b111110) =
+function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (bit[5]) sa : 0b111110) =
Some(DSRL32(rt, rd, sa))
function clause execute (DSRL32 (rt, rd, sa)) =
{
temp := rGPR(rt);
sa32 := (0b1 : sa); (* sa+32 *)
- wGPR(rd) := EXTS((bitzero ^^ sa32) : (temp[63 .. sa32]))
+ wGPR(rd) := EXTZ((bitzero ^^ sa32) : (temp[63 .. sa32]))
}
(* DSRLV reg, reg, reg *)
union ast member regregreg DSRLV
-function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b010110) =
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b010110) =
Some(DSRLV(rs, rt, rd))
function clause execute (DSRLV (rs, rt, rd)) =
{
temp := rGPR(rt);
sa := (rGPR(rs)) [5..0];
- wGPR(rd) := EXTS((bitzero ^^ sa) : temp[63 .. sa])
+ wGPR(rd) := EXTZ((bitzero ^^ sa) : temp[63 .. sa])
}
(**************************************************************************************)
@@ -456,28 +456,28 @@ function clause execute (DSRLV (rs, rt, rd)) =
(* SLL 32-bit shift left *)
union ast member regregreg SLL
-function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (regno) sa : 0b000000) =
+function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (regno) sa : 0b000000) =
Some(SLL(rt, rd, sa))
function clause execute (SLL(rt, rd, sa)) =
{
- wGPR(rd) := EXTS((rGPR(rt)) [31 - sa .. 0] : (bitzero ^^ sa))
+ wGPR(rd) := EXTZ((rGPR(rt)) [31 - sa .. 0] : (bitzero ^^ sa))
}
(* SLLV 32-bit shift left variable *)
union ast member regregreg SLLV
-function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b000100) =
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b000100) =
Some(SLLV(rs, rt, rd))
function clause execute (SLLV(rs, rt, rd)) =
{
sa := (rGPR(rs))[4..0];
- wGPR(rd) := EXTS((rGPR(rt)) [31 - sa .. 0] : (bitzero ^^ sa))
+ wGPR(rd) := EXTZ((rGPR(rt)) [31 - sa .. 0] : (bitzero ^^ sa))
}
(* SRA 32-bit arithmetic shift right *)
union ast member regregreg SRA
-function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (regno) sa : 0b000011) =
+function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (regno) sa : 0b000011) =
Some(SRA(rt, rd, sa))
function clause execute (SRA(rt, rd, sa)) =
{
@@ -485,13 +485,13 @@ function clause execute (SRA(rt, rd, sa)) =
if (NotWordVal(temp)) then
wGPR(rd) := undefined
else
- wGPR(rd) := EXTS((temp[31] ^^ (sa+32)) : temp [31..sa])
+ wGPR(rd) := EXTZ((temp[31] ^^ (sa+32)) : temp [31..sa])
}
(* SRAV 32-bit arithmetic shift right variable *)
union ast member regregreg SRAV
-function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b000111) =
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b000111) =
Some(SRAV(rs, rt, rd))
function clause execute (SRAV(rs, rt, rd)) =
{
@@ -500,13 +500,13 @@ function clause execute (SRAV(rs, rt, rd)) =
if (NotWordVal(temp)) then
wGPR(rd) := undefined
else
- wGPR(rd) := EXTS((temp[31] ^^ (sa+32)) : temp [31..sa])
+ wGPR(rd) := EXTZ((temp[31] ^^ (sa+32)) : temp [31..sa])
}
(* SRL 32-bit shift right *)
union ast member regregreg SRL
-function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (regno) sa : 0b000010) =
+function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (regno) sa : 0b000010) =
Some(SRL(rt, rd, sa))
function clause execute (SRL(rt, rd, sa)) =
{
@@ -514,13 +514,13 @@ function clause execute (SRL(rt, rd, sa)) =
if (NotWordVal(temp)) then
wGPR(rd) := undefined
else
- wGPR(rd) := EXTS((bitzero ^^ sa) : (temp [31..sa]))
+ wGPR(rd) := EXTZ((bitzero ^^ sa) : (temp [31..sa]))
}
(* SRLV 32-bit shift right variable *)
union ast member regregreg SRLV
-function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b000110) =
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b000110) =
Some(SRLV(rs, rt, rd))
function clause execute (SRLV(rs, rt, rd)) =
{
@@ -529,7 +529,7 @@ function clause execute (SRLV(rs, rt, rd)) =
if (NotWordVal(temp)) then
wGPR(rd) := undefined
else
- wGPR(rd) := EXTS((bitzero ^^ sa) : (temp [31..sa]))
+ wGPR(rd) := EXTZ((bitzero ^^ sa) : (temp [31..sa]))
}
(**************************************************************************************)
@@ -539,7 +539,7 @@ function clause execute (SRLV(rs, rt, rd)) =
(* SLT set if less than (signed) *)
union ast member regregreg SLT
-function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101010) =
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101010) =
Some(SLT(rs, rt, rd))
function clause execute (SLT(rs, rt, rd)) =
{
@@ -549,7 +549,7 @@ function clause execute (SLT(rs, rt, rd)) =
(* SLT set if less than immediate (signed) *)
union ast member regregimm16 SLTI
-function clause decode (0b001010 : (regno) rs : (regno) rt : (imm16) imm) =
+function clause decode (0b001010 : (regno) rs : (regno) rt : (imm16) imm) =
Some(SLTI(rs, rt, imm))
function clause execute (SLTI(rs, rt, imm)) =
{
@@ -561,7 +561,7 @@ function clause execute (SLTI(rs, rt, imm)) =
(* SLTU set if less than unsigned *)
union ast member regregreg SLTU
-function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101011) =
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101011) =
Some(SLTU(rs, rt, rd))
function clause execute (SLTU(rs, rt, rd)) =
{
@@ -573,7 +573,7 @@ function clause execute (SLTU(rs, rt, rd)) =
(* SLTIU set if less than immediate unsigned *)
union ast member regregimm16 SLTIU
-function clause decode (0b001011 : (regno) rs : (regno) rt : (imm16) imm) =
+function clause decode (0b001011 : (regno) rs : (regno) rt : (imm16) imm) =
Some(SLTIU(rs, rt, imm))
function clause execute (SLTIU(rs, rt, imm)) =
{
@@ -585,22 +585,22 @@ function clause execute (SLTIU(rs, rt, imm)) =
(* MOVN move if non-zero *)
union ast member regregreg MOVN
-function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b001011) =
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b001011) =
Some(MOVN(rs, rt, rd))
function clause execute (MOVN(rs, rt, rd)) =
{
- if (rGPR(rt) != 0x0000000000000000) then
+ if (rGPR(rt) != 0x0000000000000000) then
wGPR(rd) := rGPR(rs)
}
(* MOVZ move if zero *)
union ast member regregreg MOVZ
-function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b001010) =
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b001010) =
Some(MOVZ(rs, rt, rd))
function clause execute (MOVZ(rs, rt, rd)) =
{
- if (rGPR(rt) == 0x0000000000000000) then
+ if (rGPR(rt) == 0x0000000000000000) then
wGPR(rd) := rGPR(rs)
}
@@ -610,7 +610,7 @@ function clause execute (MOVZ(rs, rt, rd)) =
(* MFHI move from HI register *)
union ast member regno MFHI
-function clause decode (0b000000 : 0b0000000000 : (regno) rd : 0b00000 : 0b010000) =
+function clause decode (0b000000 : 0b0000000000 : (regno) rd : 0b00000 : 0b010000) =
Some(MFHI(rd))
function clause execute (MFHI(rd)) =
{
@@ -619,7 +619,7 @@ function clause execute (MFHI(rd)) =
(* MFLO move from LO register *)
union ast member regno MFLO
-function clause decode (0b000000 : 0b0000000000 : (regno) rd : 0b00000 : 0b010010) =
+function clause decode (0b000000 : 0b0000000000 : (regno) rd : 0b00000 : 0b010010) =
Some(MFLO(rd))
function clause execute (MFLO(rd)) =
{
@@ -628,7 +628,7 @@ function clause execute (MFLO(rd)) =
(* MTHI move to HI register *)
union ast member regno MTHI
-function clause decode (0b000000 : (regno) rs : 0b000000000000000 : 0b010001) =
+function clause decode (0b000000 : (regno) rs : 0b000000000000000 : 0b010001) =
Some(MTHI(rs))
function clause execute (MTHI(rs)) =
{
@@ -637,7 +637,7 @@ function clause execute (MTHI(rs)) =
(* MTLO move to LO register *)
union ast member regno MTLO
-function clause decode (0b000000 : (regno) rs : 0b000000000000000 : 0b010011) =
+function clause decode (0b000000 : (regno) rs : 0b000000000000000 : 0b010011) =
Some(MTLO(rs))
function clause execute (MTLO(rs)) =
{
@@ -657,7 +657,7 @@ function clause execute (MUL(rs, rt, rd)) =
undefined
else
EXTS(result[31..0]);
- (* HI and LO are technically undefined after MUL, but this causes problems with tests and
+ (* HI and LO are technically undefined after MUL, but this causes problems with tests and
(potentially) context switch so just leave them alone
HI := undefined;
LO := undefined;
@@ -691,7 +691,7 @@ function clause execute (MULTU(rs, rt)) =
(bit[64]) result := if (NotWordVal(rsVal) | NotWordVal(rtVal)) then
undefined
else
- (rsVal[31..0]) * (rtVal[31..0]);
+ EXTS((rsVal[31..0]) * (rtVal[31..0]));
HI := EXTS(result[63..32]);
LO := EXTS(result[31..0]);
}
@@ -796,13 +796,13 @@ function clause execute (DIV(rs, rt)) =
rtVal := rGPR(rt);
let ((bit[32]) q, (bit[32])r) = (
if (NotWordVal(rsVal) | NotWordVal(rtVal) | (rtVal == 0)) then
- (undefined, undefined)
+ ((bit[32]) undefined, (bit[32]) undefined)
else
let si = (signed((rsVal[31..0]))) in
let ti = (signed((rtVal[31..0]))) in
let qi = (si quot ti) in
let ri = (si - (ti*qi)) in
- ((bit[32]) qi, (bit[32]) ri))
+ ((bit[32]) (to_svec(qi)), (bit[32]) (to_svec(ri))))
in
{
HI := EXTS(r);
@@ -820,13 +820,13 @@ function clause execute (DIVU(rs, rt)) =
rtVal := rGPR(rt);
let ((bit[32]) q, (bit[32])r) = (
if (NotWordVal(rsVal) | NotWordVal(rtVal) | rtVal == 0) then
- (undefined, undefined)
+ ((bit[32]) undefined, (bit[32]) undefined)
else
let si = unsigned(rsVal[31..0]) in
let ti = unsigned(rtVal[31..0]) in
let qi = (si quot ti) in
let ri = (si mod ti) in
- ((bit[32]) qi, (bit[32]) ri))
+ ((bit[32]) (to_svec(qi)), (bit[32]) (to_svec(ri))))
in
{
HI := EXTS(r);
@@ -843,11 +843,11 @@ function clause execute (DDIV(rs, rt)) =
rsVal := signed(rGPR(rs));
rtVal := signed(rGPR(rt));
let ((bit[64])q, (bit[64])r) = (if (rtVal == 0)
- then (undefined, undefined)
- else
+ then ((bit[64]) undefined, (bit[64]) undefined)
+ else
let qi = (rsVal quot rtVal) in
let ri = (rsVal - (qi * rtVal)) in
- ((bit[64]) qi, (bit[64]) ri)) in
+ ((bit[64]) (to_svec(qi)), (bit[64]) (to_svec(ri)))) in
{
LO := q;
HI := r;
@@ -863,10 +863,10 @@ function clause execute (DDIVU(rs, rt)) =
(int) rsVal := rGPR(rs);
(int) rtVal := rGPR(rt);
let ((bit[64])q, (bit[64])r) = (if (rtVal == 0)
- then (undefined, undefined)
+ then ((bit[64]) undefined, (bit[64]) undefined)
else let qi = (rsVal quot rtVal) in
let ri = (rsVal mod rtVal) in
- ((bit[64]) qi, (bit[64]) ri)) in
+ ((bit[64]) (to_svec(qi)), (bit[64]) (to_svec(ri)))) in
{
LO := q;
HI := r;
@@ -881,7 +881,7 @@ function clause execute (DDIVU(rs, rt)) =
union ast member (bit[26]) J
function clause decode (0b000010 : (bit[26]) offset) =
Some(J(offset))
-function clause execute (J(offset)) =
+function clause execute (J(offset)) =
{
delayedPC := (PC + 4)[63..28] : offset : 0b00;
branchPending := 1
@@ -891,11 +891,11 @@ function clause execute (J(offset)) =
union ast member (bit[26]) JAL
function clause decode (0b000011 : (bit[26]) offset) =
Some(JAL(offset))
-function clause execute (JAL(offset)) =
+function clause execute (JAL(offset)) =
{
delayedPC := (PC + 4)[63..28] : offset : 0b00;
branchPending := 1;
- wGPR(31) := PC + 8;
+ wGPR(0b11111) := PC + 8;
}
(* JR -- jump via register *)
@@ -925,13 +925,13 @@ function clause execute (JALR(rs, rd)) =
(**************************************************************************************)
union ast member (regno, regno, imm16, bool, bool) BEQ
-function clause decode (0b000100 : (regno) rs : (regno) rt : (imm16) imm) =
+function clause decode (0b000100 : (regno) rs : (regno) rt : (imm16) imm) =
Some(BEQ(rs, rt, imm, false, false)) (* BEQ *)
-function clause decode (0b010100 : (regno) rs : (regno) rt : (imm16) imm) =
+function clause decode (0b010100 : (regno) rs : (regno) rt : (imm16) imm) =
Some(BEQ(rs, rt, imm, false, true)) (* BEQL *)
-function clause decode (0b000101 : (regno) rs : (regno) rt : (imm16) imm) =
+function clause decode (0b000101 : (regno) rs : (regno) rt : (imm16) imm) =
Some(BEQ(rs, rt, imm, true , false)) (* BNE *)
-function clause decode (0b010101 : (regno) rs : (regno) rt : (imm16) imm) =
+function clause decode (0b010101 : (regno) rs : (regno) rt : (imm16) imm) =
Some(BEQ(rs, rt, imm, true , true)) (* BNEL *)
function clause execute (BEQ(rs, rd, imm, ne, likely)) =
{
@@ -948,8 +948,8 @@ function clause execute (BEQ(rs, rd, imm, ne, likely)) =
}
}
-(*
-
+(*
+
Branches comparing with zero (single register operand, possible link in r31)
*)
@@ -959,32 +959,32 @@ function clause execute (BEQ(rs, rd, imm, ne, likely)) =
(**************************************************************************************)
union ast member (regno, imm16, Comparison, bool, bool) BCMPZ
-function clause decode (0b000001 : (regno) rs : 0b00000 : (imm16) imm) =
+function clause decode (0b000001 : (regno) rs : 0b00000 : (imm16) imm) =
Some(BCMPZ(rs, imm, LT, false, false)) (* BLTZ *)
-function clause decode (0b000001 : (regno) rs : 0b10000 : (imm16) imm) =
+function clause decode (0b000001 : (regno) rs : 0b10000 : (imm16) imm) =
Some(BCMPZ(rs, imm, LT, true, false)) (* BLTZAL *)
-function clause decode (0b000001 : (regno) rs : 0b00010 : (imm16) imm) =
+function clause decode (0b000001 : (regno) rs : 0b00010 : (imm16) imm) =
Some(BCMPZ(rs, imm, LT, false, true)) (* BLTZL *)
-function clause decode (0b000001 : (regno) rs : 0b10010 : (imm16) imm) =
+function clause decode (0b000001 : (regno) rs : 0b10010 : (imm16) imm) =
Some(BCMPZ(rs, imm, LT, true, true)) (* BLTZALL *)
-function clause decode (0b000001 : (regno) rs : 0b00001 : (imm16) imm) =
+function clause decode (0b000001 : (regno) rs : 0b00001 : (imm16) imm) =
Some(BCMPZ(rs, imm, GE, false, false)) (* BGEZ *)
-function clause decode (0b000001 : (regno) rs : 0b10001 : (imm16) imm) =
+function clause decode (0b000001 : (regno) rs : 0b10001 : (imm16) imm) =
Some(BCMPZ(rs, imm, GE, true, false)) (* BGEZAL *)
-function clause decode (0b000001 : (regno) rs : 0b00011 : (imm16) imm) =
+function clause decode (0b000001 : (regno) rs : 0b00011 : (imm16) imm) =
Some(BCMPZ(rs, imm, GE, false, true)) (* BGEZL *)
-function clause decode (0b000001 : (regno) rs : 0b10011 : (imm16) imm) =
+function clause decode (0b000001 : (regno) rs : 0b10011 : (imm16) imm) =
Some(BCMPZ(rs, imm, GE, true, true)) (* BGEZALL *)
-function clause decode (0b000111 : (regno) rs : 0b00000 : (imm16) imm) =
+function clause decode (0b000111 : (regno) rs : 0b00000 : (imm16) imm) =
Some(BCMPZ(rs, imm, GT, false, false)) (* BGTZ *)
-function clause decode (0b010111 : (regno) rs : 0b00000 : (imm16) imm) =
+function clause decode (0b010111 : (regno) rs : 0b00000 : (imm16) imm) =
Some(BCMPZ(rs, imm, GT, false, true)) (* BGTZL *)
-function clause decode (0b000110 : (regno) rs : 0b00000 : (imm16) imm) =
+function clause decode (0b000110 : (regno) rs : 0b00000 : (imm16) imm) =
Some(BCMPZ(rs, imm, LE, false, false)) (* BLEZ *)
-function clause decode (0b010110 : (regno) rs : 0b00000 : (imm16) imm) =
+function clause decode (0b010110 : (regno) rs : 0b00000 : (imm16) imm) =
Some(BCMPZ(rs, imm, LE, false, true)) (* BLEZL *)
function clause execute (BCMPZ(rs, imm, cmp, link, likely)) =
@@ -1003,7 +1003,7 @@ function clause execute (BCMPZ(rs, imm, cmp, link, likely)) =
nextPC := PC + 8 (* skip branch delay *)
};
if (link) then
- wGPR(31) := linkVal
+ wGPR(0b11111) := linkVal
}
(**************************************************************************************)
@@ -1051,17 +1051,17 @@ function clause execute (WAIT) = {
(* Trap instructions with two register operands *)
union ast member (regno, regno, Comparison) TRAPREG
-function clause decode (0b000000 : (regno) rs : (regno) rt : (bit[10]) code : 0b110000) =
+function clause decode (0b000000 : (regno) rs : (regno) rt : (bit[10]) code : 0b110000) =
Some(TRAPREG(rs, rt, GE)) (* TGE *)
-function clause decode (0b000000 : (regno) rs : (regno) rt : (bit[10]) code : 0b110001) =
+function clause decode (0b000000 : (regno) rs : (regno) rt : (bit[10]) code : 0b110001) =
Some(TRAPREG(rs, rt, GEU)) (* TGEU *)
-function clause decode (0b000000 : (regno) rs : (regno) rt : (bit[10]) code : 0b110010) =
+function clause decode (0b000000 : (regno) rs : (regno) rt : (bit[10]) code : 0b110010) =
Some(TRAPREG(rs, rt, LT)) (* TLT *)
-function clause decode (0b000000 : (regno) rs : (regno) rt : (bit[10]) code : 0b110011) =
+function clause decode (0b000000 : (regno) rs : (regno) rt : (bit[10]) code : 0b110011) =
Some(TRAPREG(rs, rt, LTU)) (* TLTU *)
-function clause decode (0b000000 : (regno) rs : (regno) rt : (bit[10]) code : 0b110100) =
+function clause decode (0b000000 : (regno) rs : (regno) rt : (bit[10]) code : 0b110100) =
Some(TRAPREG(rs, rt, EQ)) (* TEQ *)
-function clause decode (0b000000 : (regno) rs : (regno) rt : (bit[10]) code : 0b110110) =
+function clause decode (0b000000 : (regno) rs : (regno) rt : (bit[10]) code : 0b110110) =
Some(TRAPREG(rs, rt, NE)) (* TNE *)
function clause execute (TRAPREG(rs, rt, cmp)) =
{
@@ -1075,22 +1075,22 @@ function clause execute (TRAPREG(rs, rt, cmp)) =
(* Trap instructions with one register and one immediate operand *)
union ast member (regno, imm16, Comparison) TRAPIMM
-function clause decode (0b000001 : (regno) rs : 0b01100 : (imm16) imm) =
+function clause decode (0b000001 : (regno) rs : 0b01100 : (imm16) imm) =
Some(TRAPIMM(rs, imm, EQ)) (* TEQI *)
-function clause decode (0b000001 : (regno) rs : 0b01110 : (imm16) imm) =
+function clause decode (0b000001 : (regno) rs : 0b01110 : (imm16) imm) =
Some(TRAPIMM(rs, imm, NE)) (* TNEI *)
-function clause decode (0b000001 : (regno) rs : 0b01000 : (imm16) imm) =
+function clause decode (0b000001 : (regno) rs : 0b01000 : (imm16) imm) =
Some(TRAPIMM(rs, imm, GE)) (* TGEI *)
-function clause decode (0b000001 : (regno) rs : 0b01001 : (imm16) imm) =
+function clause decode (0b000001 : (regno) rs : 0b01001 : (imm16) imm) =
Some(TRAPIMM(rs, imm, GEU)) (* TGEIU *)
-function clause decode (0b000001 : (regno) rs : 0b01010 : (imm16) imm) =
+function clause decode (0b000001 : (regno) rs : 0b01010 : (imm16) imm) =
Some(TRAPIMM(rs, imm, LT)) (* TLTI *)
-function clause decode (0b000001 : (regno) rs : 0b01011 : (imm16) imm) =
+function clause decode (0b000001 : (regno) rs : 0b01011 : (imm16) imm) =
Some(TRAPIMM(rs, imm, LTU)) (* TLTIU *)
function clause execute (TRAPIMM(rs, imm, cmp)) =
{
rs_val := rGPR(rs);
- imm_val := EXTS(imm);
+ (bit[64]) imm_val := EXTS(imm);
condition := compare(cmp, rs_val, imm_val);
if (condition) then
(SignalException(Tr))
@@ -1101,23 +1101,23 @@ function clause execute (TRAPIMM(rs, imm, cmp)) =
(**************************************************************************************)
union ast member (WordType, bool, bool, regno, regno, imm16) Load
-function clause decode (0b100000 : (regno) base : (regno) rt : (imm16) offset) =
+function clause decode (0b100000 : (regno) base : (regno) rt : (imm16) offset) =
Some(Load(B, true, false, base, rt, offset)) (* LB *)
-function clause decode (0b100100 : (regno) base : (regno) rt : (imm16) offset) =
+function clause decode (0b100100 : (regno) base : (regno) rt : (imm16) offset) =
Some(Load(B, false, false, base, rt, offset)) (* LBU *)
-function clause decode (0b100001 : (regno) base : (regno) rt : (imm16) offset) =
+function clause decode (0b100001 : (regno) base : (regno) rt : (imm16) offset) =
Some(Load(H, true, false, base, rt, offset)) (* LH *)
-function clause decode (0b100101 : (regno) base : (regno) rt : (imm16) offset) =
+function clause decode (0b100101 : (regno) base : (regno) rt : (imm16) offset) =
Some(Load(H, false, false, base, rt, offset)) (* LHU *)
-function clause decode (0b100011 : (regno) base : (regno) rt : (imm16) offset) =
+function clause decode (0b100011 : (regno) base : (regno) rt : (imm16) offset) =
Some(Load(W, true, false, base, rt, offset)) (* LW *)
-function clause decode (0b100111 : (regno) base : (regno) rt : (imm16) offset) =
+function clause decode (0b100111 : (regno) base : (regno) rt : (imm16) offset) =
Some(Load(W, false, false, base, rt, offset)) (* LWU *)
-function clause decode (0b110111 : (regno) base : (regno) rt : (imm16) offset) =
+function clause decode (0b110111 : (regno) base : (regno) rt : (imm16) offset) =
Some(Load(D, false, false, base, rt, offset)) (* LD *)
-function clause decode (0b110000 : (regno) base : (regno) rt : (imm16) offset) =
+function clause decode (0b110000 : (regno) base : (regno) rt : (imm16) offset) =
Some(Load(W, true, true, base, rt, offset)) (* LL *)
-function clause decode (0b110100 : (regno) base : (regno) rt : (imm16) offset) =
+function clause decode (0b110100 : (regno) base : (regno) rt : (imm16) offset) =
Some(Load(D, false, true, base, rt, offset)) (* LLD *)
function clause execute (Load(width, signed, linked, base, rt, offset)) =
{
@@ -1127,15 +1127,25 @@ function clause execute (Load(width, signed, linked, base, rt, offset)) =
else
let pAddr = (TLBTranslate(vAddr, LoadData)) in
{
- memResult := if (linked) then
+ (bit[64]) memResult := if (linked) then
{
CP0LLBit := 0b1;
- CP0LLAddr := pAddr;
- MEMr_reserve_wrapper(pAddr, wordWidthBytes(width));
+ CP0LLAddr := pAddr;
+ switch wordWidthBytes(width) {
+ case ([:1:]) w -> MEMr_reserve_wrapper(pAddr, w)
+ case ([:2:]) w -> MEMr_reserve_wrapper(pAddr, w)
+ case ([:4:]) w -> MEMr_reserve_wrapper(pAddr, w)
+ case ([:8:]) w -> MEMr_reserve_wrapper(pAddr, w)
+ }
}
else
- MEMr_wrapper(pAddr, wordWidthBytes(width));
- if (signed) then
+ switch wordWidthBytes(width) {
+ case ([:1:]) w -> MEMr_reserve_wrapper(pAddr, w)
+ case ([:2:]) w -> MEMr_reserve_wrapper(pAddr, w)
+ case ([:4:]) w -> MEMr_reserve_wrapper(pAddr, w)
+ case ([:8:]) w -> MEMr_reserve_wrapper(pAddr, w)
+ };
+ if (signed) then
wGPR(rt) := EXTS(memResult)
else
wGPR(rt) := EXTZ(memResult)
@@ -1147,17 +1157,17 @@ function clause execute (Load(width, signed, linked, base, rt, offset)) =
(**************************************************************************************)
union ast member (WordType, bool, regno, regno, imm16) Store
-function clause decode (0b101000 : (regno) base : (regno) rt : (imm16) offset) =
+function clause decode (0b101000 : (regno) base : (regno) rt : (imm16) offset) =
Some(Store(B, false, base, rt, offset)) (* SB *)
-function clause decode (0b101001 : (regno) base : (regno) rt : (imm16) offset) =
+function clause decode (0b101001 : (regno) base : (regno) rt : (imm16) offset) =
Some(Store(H, false, base, rt, offset)) (* SH *)
-function clause decode (0b101011 : (regno) base : (regno) rt : (imm16) offset) =
+function clause decode (0b101011 : (regno) base : (regno) rt : (imm16) offset) =
Some(Store(W, false, base, rt, offset)) (* SW *)
-function clause decode (0b111111 : (regno) base : (regno) rt : (imm16) offset) =
+function clause decode (0b111111 : (regno) base : (regno) rt : (imm16) offset) =
Some(Store(D, false, base, rt, offset)) (* SD *)
-function clause decode (0b111000 : (regno) base : (regno) rt : (imm16) offset) =
+function clause decode (0b111000 : (regno) base : (regno) rt : (imm16) offset) =
Some(Store(W, true, base, rt, offset)) (* SC *)
-function clause decode (0b111100 : (regno) base : (regno) rt : (imm16) offset) =
+function clause decode (0b111100 : (regno) base : (regno) rt : (imm16) offset) =
Some(Store(D, true, base, rt, offset)) (* SCD *)
function clause execute (Store(width, conditional, base, rt, offset)) =
{
@@ -1170,14 +1180,14 @@ function clause execute (Store(width, conditional, base, rt, offset)) =
{
if (conditional) then
{
- success := if (CP0LLBit[0]) then switch(width)
+ success := if (CP0LLBit[0]) then (bool) switch(width)
{
case B -> MEMw_conditional_wrapper(pAddr, 1, rt_val[7..0])
case H -> MEMw_conditional_wrapper(pAddr, 2, rt_val[15..0])
case W -> MEMw_conditional_wrapper(pAddr, 4, rt_val[31..0])
case D -> MEMw_conditional_wrapper(pAddr, 8, rt_val)
} else false;
- wGPR(rt) := EXTZ([success])
+ wGPR(rt) := EXTZ([bool_to_bit(success)])
}
else
switch(width)
@@ -1195,7 +1205,7 @@ function clause execute (Store(width, conditional, base, rt, offset)) =
union ast member regregimm16 LWL
function clause decode(0b100010 : (regno) base : (regno) rt : (imm16) offset) =
Some(LWL(base, rt, offset))
-function clause execute(LWL(base, rt, offset)) =
+function clause execute(LWL(base, rt, offset)) =
{
(* XXX length check not quite right, but conservative *)
(bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), LoadData, W);
@@ -1203,19 +1213,19 @@ function clause execute(LWL(base, rt, offset)) =
{
mem_val := MEMr_wrapper (pAddr[63..2] : 0b00, 4); (* read word of interest *)
reg_val := rGPR(rt);
- wGPR(rt) := EXTS(switch(vAddr[1..0])
+ wGPR(rt) := EXTS((bit[32]) switch(vAddr[1..0])
{
case 0b00 -> mem_val
case 0b01 -> mem_val[23..0] : reg_val[07..0]
case 0b10 -> mem_val[15..0] : reg_val[15..0]
case 0b11 -> mem_val[07..0] : reg_val[23..0]
- });
+ });
}
}
union ast member regregimm16 LWR
function clause decode(0b100110 : (regno) base : (regno) rt : (imm16) offset) =
Some(LWR(base, rt, offset))
-function clause execute(LWR(base, rt, offset)) =
+function clause execute(LWR(base, rt, offset)) =
{
(* XXX length check not quite right, but conservative *)
(bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), LoadData, W);
@@ -1223,7 +1233,7 @@ function clause execute(LWR(base, rt, offset)) =
{
mem_val := MEMr_wrapper (pAddr[63..2] : 0b00, 4); (* read word of interest *)
reg_val := rGPR(rt);
- wGPR(rt) := EXTS(switch(vAddr[1..0]) (* it is acceptable to sign extend in all cases *)
+ wGPR(rt) := EXTS((bit[32]) switch(vAddr[1..0]) (* it is acceptable to sign extend in all cases *)
{
case 0b00 -> reg_val[31..8] : mem_val[31..24]
case 0b01 -> reg_val[31..16] : mem_val[31..16]
@@ -1237,7 +1247,7 @@ function clause execute(LWR(base, rt, offset)) =
union ast member regregimm16 SWL
function clause decode(0b101010 : (regno) base : (regno) rt : (imm16) offset) =
Some(SWL(base, rt, offset))
-function clause execute(SWL(base, rt, offset)) =
+function clause execute(SWL(base, rt, offset)) =
{
(* XXX length check not quite right, but conservative *)
(bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), StoreData, W);
@@ -1257,7 +1267,7 @@ function clause execute(SWL(base, rt, offset)) =
union ast member regregimm16 SWR
function clause decode(0b101110 : (regno) base : (regno) rt : (imm16) offset) =
Some(SWR(base, rt, offset))
-function clause execute(SWR(base, rt, offset)) =
+function clause execute(SWR(base, rt, offset)) =
{
(* XXX length check not quite right, but conservative *)
(bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), StoreData, W);
@@ -1279,7 +1289,7 @@ function clause execute(SWR(base, rt, offset)) =
union ast member regregimm16 LDL
function clause decode(0b011010 : (regno) base : (regno) rt : (imm16) offset) =
Some(LDL(base, rt, offset))
-function clause execute(LDL(base, rt, offset)) =
+function clause execute(LDL(base, rt, offset)) =
{
(* XXX length check not quite right, but conservative *)
(bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), LoadData, D);
@@ -1305,7 +1315,7 @@ function clause execute(LDL(base, rt, offset)) =
union ast member regregimm16 LDR
function clause decode(0b011011 : (regno) base : (regno) rt : (imm16) offset) =
Some(LDR(base, rt, offset))
-function clause execute(LDR(base, rt, offset)) =
+function clause execute(LDR(base, rt, offset)) =
{
(* XXX length check not quite right, but conservative *)
(bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), LoadData, D);
@@ -1331,7 +1341,7 @@ function clause execute(LDR(base, rt, offset)) =
union ast member regregimm16 SDL
function clause decode(0b101100 : (regno) base : (regno) rt : (imm16) offset) =
Some(SDL(base, rt, offset))
-function clause execute(SDL(base, rt, offset)) =
+function clause execute(SDL(base, rt, offset)) =
{
(* XXX length check not quite right, but conservative *)
(bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), StoreData, D);
@@ -1357,7 +1367,7 @@ function clause execute(SDL(base, rt, offset)) =
union ast member regregimm16 SDR
function clause decode(0b101101 : (regno) base : (regno) rt : (imm16) offset) =
Some(SDR(base, rt, offset))
-function clause execute(SDR(base, rt, offset)) =
+function clause execute(SDR(base, rt, offset)) =
{
(* XXX length check not quite right, but conservative *)
(bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), StoreData, D);
@@ -1384,7 +1394,7 @@ 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)) =
+function clause execute (CACHE(base, op, imm)) =
checkCP0Access () (* pretty much a NOP because no caches *)
(* PREF - prefetching into (non-existent) caches *)
@@ -1398,7 +1408,7 @@ function clause execute (PREF(base, op, imm)) =
(* SYNC - Memory barrier *)
union ast member unit SYNC
-function clause decode (0b000000 : 0b00000 : 0b00000 : 0b00000 : (regno) stype : 0b001111) =
+function clause decode (0b000000 : 0b00000 : 0b00000 : 0b00000 : (regno) stype : 0b001111) =
Some((ast) SYNC) (* stype is currently ignored *)
function clause execute(SYNC) =
MEM_sync()
@@ -1413,7 +1423,7 @@ function clause execute (MFC0(rt, rd, sel, double)) = {
let (bit[64]) result = switch (rd, sel)
{
case (0b00000,0b000) -> let (bit[31]) idx = EXTZ(TLBIndex) in
- (0x00000000 : [TLBProbe] : idx) (* 0, TLB Index *)
+ (0x00000000 : TLBProbe : idx) (* 0, TLB Index *)
case (0b00001,0b000) -> EXTZ(TLBRandom) (* 1, TLB Random *)
case (0b00010,0b000) -> TLBEntryLo0 (* 2, TLB EntryLo0 *)
case (0b00011,0b000) -> TLBEntryLo1 (* 3, TLB EntryLo1 *)
@@ -1433,9 +1443,9 @@ function clause execute (MFC0(rt, rd, sel, double)) = {
case (0b01111,0b110) -> 0 (* 15, sel 6: CHERI core ID *)
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 *)
+ : 0b000000000000000 (* Impl *)
+ : 0b1 (* BE *)
+ : 0b10 (* AT *)
: 0b000 (* AR *)
: 0b001 (* MT standard TLB *)
: 0b0000 (* zero *)
@@ -1449,7 +1459,7 @@ function clause execute (MFC0(rt, rd, sel, double)) = {
: 0b000 (* DS dcache sets *)
: 0b000 (* DL dcache lines *)
: 0b000 (* DA dcache assoc. *)
- : [have_cp2] (* C2 CP2 presence *)
+ : [bool_to_bit(have_cp2)] (* C2 CP2 presence *)
: 0b0 (* MD MDMX implemented *)
: 0b0 (* PC performance counters *)
: 0b0 (* WR watch registers *)
@@ -1476,7 +1486,7 @@ function clause execute (MFC0(rt, rd, sel, double)) = {
case _ -> (SignalException(ResI))
} in
wGPR(rt) := if (double) then result else EXTS(result[31..0])
-}
+}
(* simulator halt instruction "MTC0 rt, r23" (cheri specific behaviour) *)
union ast member unit HCF
@@ -1519,7 +1529,7 @@ function clause execute (MTC0(rt, rd, sel, double)) = {
(TLBEntryHi.ASID) := (reg_val[7..0]);
}
case (0b01011,0b000) -> { (* 11, sel 0: Compare reg *)
- CP0Compare := reg_val[31..0];
+ CP0Compare := reg_val[31..0];
(CP0Cause[15]) := bitzero;
}
case (0b01100,0b000) -> { (* 12 Status *)
@@ -1546,7 +1556,7 @@ function clause execute (MTC0(rt, rd, sel, double)) = {
case _ -> (SignalException(ResI))
}
}
-(*
+
function unit TLBWriteEntry((TLBIndexT) idx) = {
pagemask := (bit[16]) (EXTZ(TLBPageMask)); (* XXX EXTZ here forces register read in ocaml shallow embedding *)
switch(pagemask) {
@@ -1561,26 +1571,28 @@ function unit TLBWriteEntry((TLBIndexT) idx) = {
case 0xffff -> ()
case _ -> (SignalException(MCheck))
};
- ((TLBEntries[idx]).pagemask) := pagemask;
- ((TLBEntries[idx]).r ) := TLBEntryHi.R;
- ((TLBEntries[idx]).vpn2 ) := TLBEntryHi.VPN2;
- ((TLBEntries[idx]).asid ) := TLBEntryHi.ASID;
- ((TLBEntries[idx]).g ) := ((TLBEntryLo0.G) & (TLBEntryLo1.G));
- ((TLBEntries[idx]).valid ) := bitone;
- ((TLBEntries[idx]).caps0 ) := TLBEntryLo0.CapS;
- ((TLBEntries[idx]).capl0 ) := TLBEntryLo0.CapL;
- ((TLBEntries[idx]).pfn0 ) := TLBEntryLo0.PFN;
- ((TLBEntries[idx]).c0 ) := TLBEntryLo0.C;
- ((TLBEntries[idx]).d0 ) := TLBEntryLo0.D;
- ((TLBEntries[idx]).v0 ) := TLBEntryLo0.V;
- ((TLBEntries[idx]).caps1 ) := TLBEntryLo1.CapS;
- ((TLBEntries[idx]).capl1 ) := TLBEntryLo1.CapL;
- ((TLBEntries[idx]).pfn1 ) := TLBEntryLo1.PFN;
- ((TLBEntries[idx]).c1 ) := TLBEntryLo1.C;
- ((TLBEntries[idx]).d1 ) := TLBEntryLo1.D;
- ((TLBEntries[idx]).v1 ) := TLBEntryLo1.V;
+ let idxr = unsigned(idx) in {
+ ((TLBEntries[idxr]).pagemask) := pagemask;
+ ((TLBEntries[idxr]).r ) := TLBEntryHi.R;
+ ((TLBEntries[idxr]).vpn2 ) := TLBEntryHi.VPN2;
+ ((TLBEntries[idxr]).asid ) := TLBEntryHi.ASID;
+ ((TLBEntries[idxr]).g ) := ((TLBEntryLo0.G) & (TLBEntryLo1.G));
+ ((TLBEntries[idxr]).valid ) := bitone;
+ ((TLBEntries[idxr]).caps0 ) := TLBEntryLo0.CapS;
+ ((TLBEntries[idxr]).capl0 ) := TLBEntryLo0.CapL;
+ ((TLBEntries[idxr]).pfn0 ) := TLBEntryLo0.PFN;
+ ((TLBEntries[idxr]).c0 ) := TLBEntryLo0.C;
+ ((TLBEntries[idxr]).d0 ) := TLBEntryLo0.D;
+ ((TLBEntries[idxr]).v0 ) := TLBEntryLo0.V;
+ ((TLBEntries[idxr]).caps1 ) := TLBEntryLo1.CapS;
+ ((TLBEntries[idxr]).capl1 ) := TLBEntryLo1.CapL;
+ ((TLBEntries[idxr]).pfn1 ) := TLBEntryLo1.PFN;
+ ((TLBEntries[idxr]).c1 ) := TLBEntryLo1.C;
+ ((TLBEntries[idxr]).d1 ) := TLBEntryLo1.D;
+ ((TLBEntries[idxr]).v1 ) := TLBEntryLo1.V;
+ }
}
-*)
+
union ast member TLBWI
function clause decode (0b010000 : 0b10000000000000000000 : 0b000010) = Some((ast) TLBWI)
function clause execute (TLBWI) = {
@@ -1599,7 +1611,7 @@ union ast member TLBR
function clause decode (0b010000 : 0b10000000000000000000 : 0b000001) = Some((ast) TLBR)
function clause execute (TLBR) = {
checkCP0Access();
- let entry = TLBEntries[TLBIndex] in {
+ let entry = TLBEntries[unsigned(TLBIndex)] in {
TLBPageMask := entry.pagemask;
TLBEntryHi.R := entry.r;
TLBEntryHi.VPN2 := entry.vpn2;
@@ -1633,17 +1645,17 @@ function clause execute ((TLBP)) = {
}
case None -> {
TLBProbe := [bitone];
- TLBIndex := 0;
+ TLBIndex := 0b000000;
}
}
}
union ast member (regno, regno) RDHWR
-function clause decode (0b011111 : 0b00000 : (regno) rt : (regno) rd : 0b00000 : 0b111011) =
+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
+ if ((accessLevel != Kernel) & (~((CP0Status.CU)[28])) & ~(CP0HWREna[rd])) then
(SignalException(ResI));
let (bit[64]) temp = switch (rd) {
case 0b00000 -> EXTZ([bitzero]) (* CPUNum *)
diff --git a/mips_new_tc/mips_wrappers.sail b/mips_new_tc/mips_wrappers.sail
index cdb4316c..5b36983d 100644
--- a/mips_new_tc/mips_wrappers.sail
+++ b/mips_new_tc/mips_wrappers.sail
@@ -35,8 +35,10 @@
(* mips_wrappers.sail: wrappers functions and hooks for CHERI extensibility
(mostly identity functions here) *)
-function unit effect {wmem} MEMw_wrapper((bit[64]) addr, ([:8:]) size, (bit[64]) data) =
- let ledata = reverse_endianness'(8, data) in
+val forall Nat 'n, 'n >= 1, 'n <= 8. (bit[64], [:'n:], bit[8 * 'n]) -> unit effect {eamem, wmv, wreg} MEMw_wrapper
+
+function unit MEMw_wrapper((bit[64]) addr, ([:'n:]) size, (bit[8 * 'n]) data) =
+ let ledata = reverse_endianness'(sizeof 'n, data) in
if (addr == 0x000000007f000000) then
{
UART_WDATA := ledata[7..0];
@@ -46,10 +48,12 @@ function unit effect {wmem} MEMw_wrapper((bit[64]) addr, ([:8:]) size, (bit[64])
MEMval(addr, size, ledata);
}
-function bool effect {wmem} MEMw_conditional_wrapper((bit[64]) addr, ([:8:]) size, (bit[64]) data) =
+val forall Nat 'n, 'n >= 1, 'n <= 8. (bit[64], [:'n:], bit[8 * 'n]) -> bool effect {eamem, wmv} MEMw_conditional_wrapper
+
+function bool MEMw_conditional_wrapper(addr, size, data) =
{
MEMea_conditional(addr, size);
- MEMval_conditional(addr, size, reverse_endianness'(8, data))
+ MEMval_conditional(addr, size, reverse_endianness'(sizeof 'n, data))
}
function bit[64] addrWrapper((bit[64]) addr, (MemAccessType) accessType, (WordType) width) =
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-12 07:04:36 +0000