diff options
Diffstat (limited to 'mips_new_tc/mips_insts.sail')
| -rw-r--r-- | mips_new_tc/mips_insts.sail | 1692 |
1 files changed, 846 insertions, 846 deletions
diff --git a/mips_new_tc/mips_insts.sail b/mips_new_tc/mips_insts.sail index 51ef65a6..86ee1256 100644 --- a/mips_new_tc/mips_insts.sail +++ b/mips_new_tc/mips_insts.sail @@ -1,1118 +1,1118 @@ -(*========================================================================*) -(* *) -(* Copyright (c) 2015-2017 Robert M. Norton *) -(* Copyright (c) 2015-2017 Kathyrn Gray *) -(* All rights reserved. *) -(* *) -(* This software was developed by the University of Cambridge Computer *) -(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) -(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) -(* *) -(* Redistribution and use in source and binary forms, with or without *) -(* modification, are permitted provided that the following conditions *) -(* are met: *) -(* 1. Redistributions of source code must retain the above copyright *) -(* notice, this list of conditions and the following disclaimer. *) -(* 2. Redistributions in binary form must reproduce the above copyright *) -(* notice, this list of conditions and the following disclaimer in *) -(* the documentation and/or other materials provided with the *) -(* distribution. *) -(* *) -(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) -(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) -(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) -(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) -(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) -(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) -(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) -(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) -(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) -(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) -(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) -(* SUCH DAMAGE. *) -(*========================================================================*) - -(* misp_insts.sail: mips instruction decode and execute clauses and AST node - declarations *) - -(**************************************************************************************) -(* [D]ADD[I][U] various forms of ADD *) -(**************************************************************************************) - -(* DADDIU Doubleword Add Immediate Unsigned -- +/*========================================================================*/ +/* */ +/* Copyright (c) 2015-2017 Robert M. Norton */ +/* Copyright (c) 2015-2017 Kathyrn Gray */ +/* All rights reserved. */ +/* */ +/* This software was developed by the University of Cambridge Computer */ +/* Laboratory as part of the Rigorous Engineering of Mainstream Systems */ +/* (REMS) project, funded by EPSRC grant EP/K008528/1. */ +/* */ +/* Redistribution and use in source and binary forms, with or without */ +/* modification, are permitted provided that the following conditions */ +/* are met: */ +/* 1. Redistributions of source code must retain the above copyright */ +/* notice, this list of conditions and the following disclaimer. */ +/* 2. Redistributions in binary form must reproduce the above copyright */ +/* notice, this list of conditions and the following disclaimer in */ +/* the documentation and/or other materials provided with the */ +/* distribution. */ +/* */ +/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ +/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ +/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ +/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ +/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ +/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ +/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ +/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ +/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ +/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ +/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ +/* SUCH DAMAGE. */ +/*========================================================================*/ + +/* misp_insts.sail: mips instruction decode and execute clauses and AST node + declarations */ + +/**************************************************************************************/ +/* [D]ADD[I][U] various forms of ADD */ +/**************************************************************************************/ + +/* DADDIU Doubleword Add Immediate Unsigned -- the simplest possible instruction, no undefined behaviour or exceptions - reg, reg, immediate *) + reg, reg, immediate */ union ast member regregimm16 DADDIU -function clause decode (0b011001 : (regno) rs : (regno) rt : (imm16) imm) = +function clause decode (0b011001 @ rs : regno @ rt : regno @ imm : imm16) = Some(DADDIU(rs, rt, imm)) function clause execute (DADDIU (rs, rt, imm)) = { - wGPR(rt) := rGPR(rs) + (bit[64]) (EXTS(imm)) + wGPR(rt) = rGPR(rs) + (bits(64)) (EXTS(imm)) } -(* DADDU Doubleword Add Unsigned -- another very simple instruction, - reg, reg, reg *) +/* DADDU Doubleword Add Unsigned -- another very simple instruction, + reg, reg, reg */ union ast member regregreg DADDU -function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101101) = +function clause decode (0b000000 @ rs : regno @ rt : regno @ rd : regno @ 0b00000 @ 0b101101) = Some(DADDU(rs, rt, rd)) function clause execute (DADDU (rs, rt, rd)) = { - wGPR(rd) := rGPR(rs) + rGPR(rt) + wGPR(rd) = rGPR(rs) + rGPR(rt) } -(* DADDI Doubleword Add Immediate - reg, reg, imm with possible exception *) +/* DADDI Doubleword Add Immediate + reg, reg, imm with possible exception */ union ast member regregimm16 DADDI -function clause decode (0b011000 : (regno) rs : (regno) rt : (imm16) imm) = +function clause decode (0b011000 @ rs : regno @ rt : regno @ imm : imm16) = Some(DADDI(rs, rt, imm)) function clause execute (DADDI (rs, rt, imm)) = { - let (bit[65]) sum65 = ((bit[65]) (EXTS(rGPR(rs))) + (bit[65]) (EXTS(imm))) in + let sum65 : bits(65) = ((bits(65)) (EXTS(rGPR(rs))) + (bits(65)) (EXTS(imm))) in { if (sum65[64] != sum65[63]) then (SignalException(Ov)) else - wGPR(rt) := sum65[63..0] + wGPR(rt) = sum65[63..0] } } -(* DADD Doubleword Add - reg, reg, reg with possible exception *) +/* DADD Doubleword Add + reg, reg, reg with possible exception */ union ast member regregreg DADD -function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101100) = +function clause decode (0b000000 @ rs : regno @ rt : regno @ rd : regno @ 0b00000 @ 0b101100) = Some(DADD(rs, rt, rd)) function clause execute (DADD (rs, rt, rd)) = { - let (bit[65]) sum65 = ((bit[65]) (EXTS(rGPR(rs))) + (bit[65]) (EXTS(rGPR(rt)))) in + let sum65 : bits(65) = ((bits(65)) (EXTS(rGPR(rs))) + (bits(65)) (EXTS(rGPR(rt)))) in { if sum65[64] != sum65[63] then (SignalException(Ov)) else - wGPR(rd) := sum65[63..0] + wGPR(rd) = sum65[63..0] } } -(* ADD 32-bit add -- reg, reg, reg with possible undefined behaviour or exception *) +/* ADD 32-bit add -- reg, reg, reg with possible undefined behaviour or exception */ union ast member regregreg ADD -function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b100000) = +function clause decode (0b000000 @ rs : regno @ rt : regno @ rd : regno @ 0b00000 @ 0b100000) = Some(ADD(rs, rt, rd)) function clause execute (ADD(rs, rt, rd)) = { - (bit[64]) opA := rGPR(rs); - (bit[64]) opB := rGPR(rt); + (bits(64)) opA = rGPR(rs); + (bits(64)) opB = rGPR(rt); if NotWordVal(opA) | NotWordVal(opB) then - wGPR(rd) := (bit[64]) undefined (* XXX could exit instead *) + wGPR(rd) = (bits(64)) undefined /* XXX could exit instead */ else - let (bit[33]) sum33 = ((bit[33]) (EXTS(opA[31 .. 0])) + (bit[33]) (EXTS(opB[31 .. 0]))) in + let sum33 : bits(33) = ((bits(33)) (EXTS(opA[31 .. 0])) + (bits(33)) (EXTS(opB[31 .. 0]))) in if sum33[32] != sum33[31] then (SignalException(Ov)) else - wGPR(rd) := (bit[64]) (EXTS(sum33[31..0])) + wGPR(rd) = (bits(64)) (EXTS(sum33[31..0])) } -(* ADDI 32-bit add immediate -- reg, reg, imm with possible undefined behaviour or exception *) +/* ADDI 32-bit add immediate -- reg, reg, imm with possible undefined behaviour or exception */ union ast member regregimm16 ADDI -function clause decode (0b001000 : (regno) rs : (regno) rt : (imm16) imm) = +function clause decode (0b001000 @ rs : regno @ rt : regno @ imm : imm16) = Some(ADDI(rs, rt, imm)) function clause execute (ADDI(rs, rt, imm)) = { - (bit[64]) opA := rGPR(rs); + (bits(64)) opA = rGPR(rs); if NotWordVal(opA) then - wGPR(rt) := (bit[64]) undefined (* XXX could exit instead *) + wGPR(rt) = (bits(64)) undefined /* XXX could exit instead */ else - let sum33 = (bit[33]) (EXTS(opA[31 .. 0])) + (bit[33]) (EXTS(imm)) in + let sum33 = (bits(33)) (EXTS(opA[31 .. 0])) + (bits(33)) (EXTS(imm)) in if sum33[32] != sum33[31] then (SignalException(Ov)) else - wGPR(rt) := EXTS(sum33[31..0]) + wGPR(rt) = EXTS(sum33[31..0]) } -(* ADDU 32-bit add immediate -- reg, reg, reg with possible undefined behaviour *) +/* ADDU 32-bit add immediate -- reg, reg, reg with possible undefined behaviour */ union ast member regregreg ADDU -function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b100001) = +function clause decode (0b000000 @ rs : regno @ rt : regno @ rd : regno @ 0b00000 @ 0b100001) = Some(ADDU(rs, rt, rd)) function clause execute (ADDU(rs, rt, rd)) = { - (bit[64]) opA := rGPR(rs); - (bit[64]) opB := rGPR(rt); + (bits(64)) opA = rGPR(rs); + (bits(64)) opB = rGPR(rt); if NotWordVal(opA) | NotWordVal(opB) then - wGPR(rd) := (bit[64]) undefined + wGPR(rd) = (bits(64)) undefined else - wGPR(rd) := (bit[64]) (EXTS(opA[31..0] + opB[31..0])) + wGPR(rd) = (bits(64)) (EXTS(opA[31..0] + opB[31..0])) } -(* ADDIU 32-bit add immediate -- reg, reg, imm with possible undefined behaviour *) +/* ADDIU 32-bit add immediate -- reg, reg, imm with possible undefined behaviour */ union ast member regregimm16 ADDIU -function clause decode (0b001001 : (regno) rs : (regno) rt : (imm16) imm) = +function clause decode (0b001001 @ rs : regno @ rt : regno @ imm : imm16) = Some(ADDIU(rs, rt, imm)) function clause execute (ADDIU(rs, rt, imm)) = { - (bit[64]) opA := rGPR(rs); + (bits(64)) opA = rGPR(rs); if NotWordVal(opA) then - wGPR(rt) := (bit[64]) undefined (* XXX could exit instead *) + wGPR(rt) = (bits(64)) undefined /* XXX could exit instead */ else - wGPR(rt) := (bit[64]) (EXTS((opA[31 .. 0]) + (bit[32]) (EXTS(imm)))) + wGPR(rt) = (bits(64)) (EXTS((opA[31 .. 0]) + (bits(32)) (EXTS(imm)))) } -(**************************************************************************************) -(* [D]SUB[U] various forms of SUB *) -(**************************************************************************************) +/**************************************************************************************/ +/* [D]SUB[U] various forms of SUB */ +/**************************************************************************************/ -(* DSUBU doubleword subtract 'unsigned' reg, reg, reg *) +/* DSUBU doubleword subtract 'unsigned' reg, reg, reg */ union ast member regregreg DSUBU -function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101111) = +function clause decode (0b000000 @ rs : regno @ rt : regno @ rd : regno @ 0b00000 @ 0b101111) = Some(DSUBU(rs, rt, rd)) function clause execute (DSUBU (rs, rt, rd)) = { - wGPR(rd) := rGPR(rs) - rGPR(rt) + wGPR(rd) = rGPR(rs) - rGPR(rt) } -(* DSUB reg, reg, reg with possible exception *) +/* DSUB reg, reg, reg with possible exception */ union ast member regregreg DSUB -function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101110) = +function clause decode (0b000000 @ rs : regno @ rt : regno @ rd : regno @ 0b00000 @ 0b101110) = Some(DSUB(rs, rt, rd)) function clause execute (DSUB (rs, rt, rd)) = { - let (bit[65]) temp65 = (bit[65]) (EXTS(rGPR(rs))) - (bit[65]) (EXTS(rGPR(rt))) in + let temp65 : bits(65) = (bits(65)) (EXTS(rGPR(rs))) - (bits(65)) (EXTS(rGPR(rt))) in { if temp65[64] != temp65[63] then (SignalException(Ov)) else - wGPR(rd) := temp65[63..0] + wGPR(rd) = temp65[63..0] } } -(* SUB 32-bit sub -- reg, reg, reg with possible undefined behaviour or exception *) +/* SUB 32-bit sub -- reg, reg, reg with possible undefined behaviour or exception */ union ast member regregreg SUB -function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b100010) = +function clause decode (0b000000 @ rs : regno @ rt : regno @ rd : regno @ 0b00000 @ 0b100010) = Some(SUB(rs, rt, rd)) function clause execute (SUB(rs, rt, rd)) = { - (bit[64]) opA := rGPR(rs); - (bit[64]) opB := rGPR(rt); + (bits(64)) opA = rGPR(rs); + (bits(64)) opB = rGPR(rt); if NotWordVal(opA) | NotWordVal(opB) then - wGPR(rd) := (bit[64]) undefined (* XXX could instead *) + wGPR(rd) = (bits(64)) undefined /* XXX could instead */ else - let (bit[33]) temp33 = (EXTS(opA[31..0]) - EXTS(opB[31..0])) in + let temp33 : bits(33) = (EXTS(opA[31..0]) - EXTS(opB[31..0])) in if temp33[32] != temp33[31] then (SignalException(Ov)) else - wGPR(rd) := EXTS(temp33[31..0]) + wGPR(rd) = EXTS(temp33[31..0]) } -(* SUBU 32-bit 'unsigned' sub -- reg, reg, reg with possible undefined behaviour *) +/* SUBU 32-bit 'unsigned' sub -- reg, reg, reg with possible undefined behaviour */ union ast member regregreg SUBU -function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b100011) = +function clause decode (0b000000 @ rs : regno @ rt : regno @ rd : regno @ 0b00000 @ 0b100011) = Some(SUBU(rs, rt, rd)) function clause execute (SUBU(rs, rt, rd)) = { - (bit[64]) opA := rGPR(rs); - (bit[64]) opB := rGPR(rt); + (bits(64)) opA = rGPR(rs); + (bits(64)) opB = rGPR(rt); if NotWordVal(opA) | NotWordVal(opB) then - wGPR(rd) := undefined + wGPR(rd) = undefined else - wGPR(rd) := EXTS(opA[31..0] - opB[31..0]) + wGPR(rd) = EXTS(opA[31..0] - opB[31..0]) } -(**************************************************************************************) -(* Logical bitwise operations *) -(**************************************************************************************) +/**************************************************************************************/ +/* Logical bitwise operations */ +/**************************************************************************************/ -(* AND reg, reg, reg *) +/* 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 @ rs : regno @ rt : regno @ rd : regno @ 0b00000 @ 0b100100) = Some(AND(rs, rt, rd)) function clause execute (AND (rs, rt, rd)) = { - wGPR(rd) := (rGPR(rs) & rGPR(rt)) + wGPR(rd) = (rGPR(rs) & rGPR(rt)) } -(* ANDI reg, reg, imm *) +/* ANDI reg, reg, imm */ union ast member regregimm16 ANDI -function clause decode (0b001100 : (regno) rs : (regno) rt : (imm16) imm) = +function clause decode (0b001100 @ rs : regno @ rt : regno @ imm : imm16) = Some(ANDI(rs, rt, imm)) function clause execute (ANDI (rs, rt, imm)) = { - wGPR(rt) := (rGPR(rs) & EXTZ(imm)) + wGPR(rt) = (rGPR(rs) & EXTZ(imm)) } -(* OR reg, reg, reg *) +/* 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 @ rs : regno @ rt : regno @ rd : regno @ 0b00000 @ 0b100101) = Some(OR(rs, rt, rd)) function clause execute (OR (rs, rt, rd)) = { - wGPR(rd) := (rGPR(rs) | rGPR(rt)) + wGPR(rd) = (rGPR(rs) | rGPR(rt)) } -(* ORI reg, reg, imm *) +/* ORI reg, reg, imm */ union ast member regregimm16 ORI -function clause decode (0b001101 : (regno) rs : (regno) rt : (imm16) imm) = +function clause decode (0b001101 @ rs : regno @ rt : regno @ imm : imm16) = Some(ORI(rs, rt, imm)) function clause execute (ORI (rs, rt, imm)) = { - wGPR(rt) := (rGPR(rs) | EXTZ(imm)) + wGPR(rt) = (rGPR(rs) | EXTZ(imm)) } -(* NOR reg, reg, reg *) +/* 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 @ rs : regno @ rt : regno @ rd : regno @ 0b00000 @ 0b100111) = Some(NOR(rs, rt, rd)) function clause execute (NOR (rs, rt, rd)) = { - wGPR(rd) := ~(rGPR(rs) | rGPR(rt)) + wGPR(rd) = ~(rGPR(rs) | rGPR(rt)) } -(* XOR reg, reg, reg *) +/* 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 @ rs : regno @ rt : regno @ rd : regno @ 0b00000 @ 0b100110) = Some(XOR(rs, rt, rd)) function clause execute (XOR (rs, rt, rd)) = { - wGPR(rd) := (rGPR(rs) ^ rGPR(rt)) + wGPR(rd) = (rGPR(rs) ^ rGPR(rt)) } -(* XORI reg, reg, imm *) +/* XORI reg, reg, imm */ union ast member regregimm16 XORI -function clause decode (0b001110 : (regno) rs : (regno) rt : (imm16) imm) = +function clause decode (0b001110 @ rs : regno @ rt : regno @ imm : imm16) = Some(XORI(rs, rt, imm)) function clause execute (XORI (rs, rt, imm)) = { - wGPR(rt) := (rGPR(rs) ^ EXTZ(imm)) + wGPR(rt) = (rGPR(rs) ^ EXTZ(imm)) } -(* LUI reg, imm 32-bit load immediate into upper 16 bits *) +/* 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) = +function clause decode (0b001111 @ 0b00000 @ rt : regno @ imm : imm16) = Some(LUI(rt, imm)) function clause execute (LUI (rt, imm)) = { - wGPR(rt) := EXTS(imm : 0x0000) + wGPR(rt) = EXTS(imm : 0x0000) } -(**************************************************************************************) -(* 64-bit shift operations *) -(**************************************************************************************) +/**************************************************************************************/ +/* 64-bit shift operations */ +/**************************************************************************************/ -(* DSLL reg, reg, imm5 *) +/* 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 @ rt : regno @ rd : regno @ (bits(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 >> *) + wGPR(rd) = (rGPR(rt) << sa) /* make tuareg mode less blue >> */ } -(* DSLL32 reg, reg, imm5 *) +/* 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 @ rt : regno @ rd : regno @ (bits(5)) sa @ 0b111100) = Some(DSLL32(rt, rd, sa)) function clause execute (DSLL32 (rt, rd, sa)) = { - wGPR(rd) := (rGPR(rt) << (0b1 : sa)) (* make tuareg mode less blue >> *) + wGPR(rd) = (rGPR(rt) << (0b1 : sa)) /* make tuareg mode less blue >> */ } -(* DSLLV reg, reg, reg *) +/* 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 @ rs : regno @ rt : regno @ rd : regno @ 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 - sa := (rGPR(rt))[5 .. 0]; - v := rGPR(rs); - wGPR(rd) := v[(63-sa) .. 0] : (0b0 ^^ sa) *) + wGPR(rd) = (rGPR(rt) << ((rGPR(rs))[5 .. 0])) /* make tuareg mode less blue >> */ + /* alternative slicing based version of above + sa = (rGPR(rt))[5 .. 0]; + v = rGPR(rs); + wGPR(rd) = v[(63-sa) .. 0] : (0b0 ^^ sa) */ } -(* DSRA arithmetic shift duplicating sign bit - reg, reg, imm5 *) +/* 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 @ rt : regno @ rd : regno @ (bits(5)) sa @ 0b111011) = Some(DSRA(rt, rd, sa)) function clause execute (DSRA (rt, rd, sa)) = { - temp := rGPR(rt); - wGPR(rd) := EXTZ((temp[63] ^^ sa) : (temp[63 .. sa])) + temp = rGPR(rt); + wGPR(rd) = EXTZ((temp[63] ^^ sa) : (temp[63 .. sa])) } -(* DSRA32 reg, reg, imm5 *) +/* 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 @ rt : regno @ rd : regno @ (bits(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) := EXTZ((temp[63] ^^ sa32) : (temp[63 .. sa32])) + temp = rGPR(rt); + sa32 = (0b1 : sa); /* sa+32 */ + wGPR(rd) = EXTZ((temp[63] ^^ sa32) : (temp[63 .. sa32])) } -(* DSRAV reg, reg, reg *) +/* DSRAV reg, reg, reg */ union ast member regregreg DSRAV -function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b010111) = +function clause decode (0b000000 @ rs : regno @ rt : regno @ rd : regno @ 0b00000 @ 0b010111) = Some(DSRAV(rs, rt, rd)) function clause execute (DSRAV (rs, rt, rd)) = { - temp := rGPR(rt); - sa := (rGPR(rs)) [5..0]; - wGPR(rd) := EXTZ((temp[63] ^^ sa) : temp[63 .. sa]) + temp = rGPR(rt); + sa = (rGPR(rs)) [5..0]; + wGPR(rd) = EXTZ((temp[63] ^^ sa) : temp[63 .. sa]) } -(* DSRL shift right logical - reg, reg, imm5 *) +/* 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 @ rt : regno @ rd : regno @ (bits(5)) sa @ 0b111010) = Some(DSRL(rt, rd, sa)) function clause execute (DSRL (rt, rd, sa)) = { - temp := rGPR(rt); - wGPR(rd) := EXTZ((bitzero ^^ sa) : (temp[63 .. sa])) + temp = rGPR(rt); + wGPR(rd) = EXTZ((bitzero ^^ sa) : (temp[63 .. sa])) } -(* DSRL32 reg, reg, imm5 *) +/* 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 @ rt : regno @ rd : regno @ (bits(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) := EXTZ((bitzero ^^ sa32) : (temp[63 .. sa32])) + temp = rGPR(rt); + sa32 = (0b1 : sa); /* sa+32 */ + wGPR(rd) = EXTZ((bitzero ^^ sa32) : (temp[63 .. sa32])) } -(* DSRLV reg, reg, reg *) +/* 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 @ rs : regno @ rt : regno @ rd : regno @ 0b00000 @ 0b010110) = Some(DSRLV(rs, rt, rd)) function clause execute (DSRLV (rs, rt, rd)) = { - temp := rGPR(rt); - sa := (rGPR(rs)) [5..0]; - wGPR(rd) := EXTZ((bitzero ^^ sa) : temp[63 .. sa]) + temp = rGPR(rt); + sa = (rGPR(rs)) [5..0]; + wGPR(rd) = EXTZ((bitzero ^^ sa) : temp[63 .. sa]) } -(**************************************************************************************) -(* 32-bit shift operations *) -(**************************************************************************************) +/**************************************************************************************/ +/* 32-bit shift operations */ +/**************************************************************************************/ -(* SLL 32-bit shift left *) +/* 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 @ rt : regno @ rd : regno @ sa : regno @ 0b000000) = Some(SLL(rt, rd, sa)) function clause execute (SLL(rt, rd, sa)) = { - wGPR(rd) := EXTZ((rGPR(rt)) [31 - sa .. 0] : (bitzero ^^ sa)) + wGPR(rd) = EXTZ((rGPR(rt)) [31 - sa .. 0] : (bitzero ^^ sa)) } -(* SLLV 32-bit shift left variable *) +/* 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 @ rs : regno @ rt : regno @ rd : regno @ 0b00000 @ 0b000100) = Some(SLLV(rs, rt, rd)) function clause execute (SLLV(rs, rt, rd)) = { - sa := (rGPR(rs))[4..0]; - wGPR(rd) := EXTZ((rGPR(rt)) [31 - sa .. 0] : (bitzero ^^ sa)) + sa = (rGPR(rs))[4..0]; + wGPR(rd) = EXTZ((rGPR(rt)) [31 - sa .. 0] : (bitzero ^^ sa)) } -(* SRA 32-bit arithmetic shift right *) +/* 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 @ rt : regno @ rd : regno @ sa : regno @ 0b000011) = Some(SRA(rt, rd, sa)) function clause execute (SRA(rt, rd, sa)) = { - temp := rGPR(rt); + temp = rGPR(rt); if (NotWordVal(temp)) then - wGPR(rd) := undefined + wGPR(rd) = undefined else - wGPR(rd) := EXTZ((temp[31] ^^ (sa+32)) : temp [31..sa]) + wGPR(rd) = EXTZ((temp[31] ^^ (sa+32)) : temp [31..sa]) } -(* SRAV 32-bit arithmetic shift right variable *) +/* 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 @ rs : regno @ rt : regno @ rd : regno @ 0b00000 @ 0b000111) = Some(SRAV(rs, rt, rd)) function clause execute (SRAV(rs, rt, rd)) = { - temp := rGPR(rt); - sa := (rGPR(rs))[4..0]; + temp = rGPR(rt); + sa = (rGPR(rs))[4..0]; if (NotWordVal(temp)) then - wGPR(rd) := undefined + wGPR(rd) = undefined else - wGPR(rd) := EXTZ((temp[31] ^^ (sa+32)) : temp [31..sa]) + wGPR(rd) = EXTZ((temp[31] ^^ (sa+32)) : temp [31..sa]) } -(* SRL 32-bit shift right *) +/* 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 @ rt : regno @ rd : regno @ sa : regno @ 0b000010) = Some(SRL(rt, rd, sa)) function clause execute (SRL(rt, rd, sa)) = { - temp := rGPR(rt); + temp = rGPR(rt); if (NotWordVal(temp)) then - wGPR(rd) := undefined + wGPR(rd) = undefined else - wGPR(rd) := EXTZ((bitzero ^^ sa) : (temp [31..sa])) + wGPR(rd) = EXTZ((bitzero ^^ sa) : (temp [31..sa])) } -(* SRLV 32-bit shift right variable *) +/* 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 @ rs : regno @ rt : regno @ rd : regno @ 0b00000 @ 0b000110) = Some(SRLV(rs, rt, rd)) function clause execute (SRLV(rs, rt, rd)) = { - temp := rGPR(rt); - sa := (rGPR(rs))[4..0]; + temp = rGPR(rt); + sa = (rGPR(rs))[4..0]; if (NotWordVal(temp)) then - wGPR(rd) := undefined + wGPR(rd) = undefined else - wGPR(rd) := EXTZ((bitzero ^^ sa) : (temp [31..sa])) + wGPR(rd) = EXTZ((bitzero ^^ sa) : (temp [31..sa])) } -(**************************************************************************************) -(* set less than / conditional move *) -(**************************************************************************************) +/**************************************************************************************/ +/* set less than / conditional move */ +/**************************************************************************************/ -(* SLT set if less than (signed) *) +/* 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 @ rs : regno @ rt : regno @ rd : regno @ 0b00000 @ 0b101010) = Some(SLT(rs, rt, rd)) function clause execute (SLT(rs, rt, rd)) = { - wGPR(rd) := if (rGPR(rs) <_s rGPR(rt)) then 1 else 0 + wGPR(rd) = if (rGPR(rs) <_s rGPR(rt)) then 1 else 0 } -(* SLT set if less than immediate (signed) *) +/* 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 @ rs : regno @ rt : regno @ imm : imm16) = Some(SLTI(rs, rt, imm)) function clause execute (SLTI(rs, rt, imm)) = { - let imm_val = signed(imm) in - let rs_val = signed(rGPR(rs)) in - wGPR(rt) := if (rs_val < imm_val) then 0x0000000000000001 else 0x0000000000000000 + let imm_val in : = signed(imm) + let rs_val in : = signed(rGPR(rs)) + wGPR(rt) = if (rs_val 0x0000000000000000 : < imm_val) then 0x0000000000000001 else } -(* SLTU set if less than unsigned *) +/* 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 @ rs : regno @ rt : regno @ rd : regno @ 0b00000 @ 0b101011) = Some(SLTU(rs, rt, rd)) function clause execute (SLTU(rs, rt, rd)) = { - let rs_val = (0b0 : (rGPR(rs))) in - let rt_val = (0b0 : (rGPR(rt))) in - wGPR(rd) := (if (rs_val < rt_val) then 1 else 0) + let rs_val in : = (0b0 : (rGPR(rs))) + let rt_val in : = (0b0 : (rGPR(rt))) + wGPR(rd) = (if (rs_val 0 : < rt_val) then 1 else) } -(* SLTIU set if less than immediate unsigned *) +/* 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 @ rs : regno @ rt : regno @ imm : imm16) = Some(SLTIU(rs, rt, imm)) function clause execute (SLTIU(rs, rt, imm)) = { - let rs_val = (0b0 : (rGPR(rs))) in - let imm_val = (0b0 : ((bit[64])(EXTS(imm)))) in - wGPR(rt) := (if (rs_val < imm_val) then 1 else 0) + let rs_val in : = (0b0 : (rGPR(rs))) + let imm_val in : = (0b0 : ((bits(64))(EXTS(imm)))) + wGPR(rt) = (if (rs_val 0 : < imm_val) then 1 else) } -(* MOVN move if non-zero *) +/* 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 @ rs : regno @ rt : regno @ rd : regno @ 0b00000 @ 0b001011) = Some(MOVN(rs, rt, rd)) function clause execute (MOVN(rs, rt, rd)) = { if (rGPR(rt) != 0x0000000000000000) then - wGPR(rd) := rGPR(rs) + wGPR(rd) = rGPR(rs) } -(* MOVZ move if zero *) +/* 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 @ rs : regno @ rt : regno @ rd : regno @ 0b00000 @ 0b001010) = Some(MOVZ(rs, rt, rd)) function clause execute (MOVZ(rs, rt, rd)) = { if (rGPR(rt) == 0x0000000000000000) then - wGPR(rd) := rGPR(rs) + wGPR(rd) = rGPR(rs) } -(******************************************************************************) -(* MUL/DIV instructions *) -(******************************************************************************) +/******************************************************************************/ +/* MUL/DIV instructions */ +/******************************************************************************/ -(* MFHI move from HI register *) +/* MFHI move from HI register */ union ast member regno MFHI -function clause decode (0b000000 : 0b0000000000 : (regno) rd : 0b00000 : 0b010000) = +function clause decode (0b000000 @ 0b0000000000 @ rd : regno @ 0b00000 @ 0b010000) = Some(MFHI(rd)) function clause execute (MFHI(rd)) = { - wGPR(rd) := HI + wGPR(rd) = HI } -(* MFLO move from LO register *) +/* MFLO move from LO register */ union ast member regno MFLO -function clause decode (0b000000 : 0b0000000000 : (regno) rd : 0b00000 : 0b010010) = +function clause decode (0b000000 @ 0b0000000000 @ rd : regno @ 0b00000 @ 0b010010) = Some(MFLO(rd)) function clause execute (MFLO(rd)) = { - wGPR(rd) := LO + wGPR(rd) = LO } -(* MTHI move to HI register *) +/* MTHI move to HI register */ union ast member regno MTHI -function clause decode (0b000000 : (regno) rs : 0b000000000000000 : 0b010001) = +function clause decode (0b000000 @ rs : regno @ 0b000000000000000 @ 0b010001) = Some(MTHI(rs)) function clause execute (MTHI(rs)) = { - HI := rGPR(rs) + HI = rGPR(rs) } -(* MTLO move to LO register *) +/* MTLO move to LO register */ union ast member regno MTLO -function clause decode (0b000000 : (regno) rs : 0b000000000000000 : 0b010011) = +function clause decode (0b000000 @ rs : regno @ 0b000000000000000 @ 0b010011) = Some(MTLO(rs)) function clause execute (MTLO(rs)) = { - LO := rGPR(rs) + LO = rGPR(rs) } -(* MUL 32-bit multiply into GPR *) +/* MUL 32-bit multiply into GPR */ union ast member regregreg MUL -function clause decode (0b011100 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b000010) = +function clause decode (0b011100 @ rs : regno @ rt : regno @ rd : regno @ 0b00000 @ 0b000010) = Some(MUL(rs, rt, rd)) function clause execute (MUL(rs, rt, rd)) = { - rsVal := rGPR(rs); - rtVal := rGPR(rt); - (bit[64]) result := EXTS((rsVal[31..0]) *_s (rtVal[31..0])); - wGPR(rd) := if (NotWordVal(rsVal) | NotWordVal(rtVal)) then + rsVal = rGPR(rs); + rtVal = rGPR(rt); + (bits(64)) result = EXTS((rsVal[31..0]) *_s (rtVal[31..0])); + wGPR(rd) = if (NotWordVal(rsVal) | NotWordVal(rtVal)) then 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; - *) + HI = undefined; + LO = undefined; + */ } -(* MULT 32-bit multiply into HI/LO *) +/* MULT 32-bit multiply into HI/LO */ union ast member (regno, regno) MULT -function clause decode (0b000000 : (regno) rs : (regno) rt : 0b00000 : 0b00000 : 0b011000) = +function clause decode (0b000000 @ rs : regno @ rt : regno @ 0b00000 @ 0b00000 @ 0b011000) = Some(MULT(rs, rt)) function clause execute (MULT(rs, rt)) = { - rsVal := rGPR(rs); - rtVal := rGPR(rt); - (bit[64]) result := if (NotWordVal(rsVal) | NotWordVal(rtVal)) then + rsVal = rGPR(rs); + rtVal = rGPR(rt); + (bits(64)) result = if (NotWordVal(rsVal) | NotWordVal(rtVal)) then undefined else EXTS((rsVal[31..0]) *_s (rtVal[31..0])); - HI := EXTS(result[63..32]); - LO := EXTS(result[31..0]); + HI = EXTS(result[63..32]); + LO = EXTS(result[31..0]); } -(* MULTU 32-bit unsignedm rultiply into HI/LO *) +/* MULTU 32-bit unsignedm rultiply into HI/LO */ union ast member (regno, regno) MULTU -function clause decode (0b000000 : (regno) rs : (regno) rt : 0b00000 : 0b00000 : 0b011001) = +function clause decode (0b000000 @ rs : regno @ rt : regno @ 0b00000 @ 0b00000 @ 0b011001) = Some(MULTU(rs, rt)) function clause execute (MULTU(rs, rt)) = { - rsVal := rGPR(rs); - rtVal := rGPR(rt); - (bit[64]) result := if (NotWordVal(rsVal) | NotWordVal(rtVal)) then + rsVal = rGPR(rs); + rtVal = rGPR(rt); + (bits(64)) result = if (NotWordVal(rsVal) | NotWordVal(rtVal)) then undefined else EXTS((rsVal[31..0]) * (rtVal[31..0])); - HI := EXTS(result[63..32]); - LO := EXTS(result[31..0]); + HI = EXTS(result[63..32]); + LO = EXTS(result[31..0]); } -(* DMULT 64-bit multiply into HI/LO *) +/* DMULT 64-bit multiply into HI/LO */ union ast member (regno, regno) DMULT -function clause decode (0b000000 : (regno) rs : (regno) rt : 0b00000 : 0b00000 : 0b011100) = +function clause decode (0b000000 @ rs : regno @ rt : regno @ 0b00000 @ 0b00000 @ 0b011100) = Some(DMULT(rs, rt)) function clause execute (DMULT(rs, rt)) = { - (bit[128]) result := rGPR(rs) *_s rGPR(rt); - HI := (result[127..64]); - LO := (result[63..0]); + (bits(128)) result = rGPR(rs) *_s rGPR(rt); + HI = (result[127..64]); + LO = (result[63..0]); } -(* DMULTU 64-bit unsigned multiply into HI/LO *) +/* DMULTU 64-bit unsigned multiply into HI/LO */ union ast member (regno, regno) DMULTU -function clause decode (0b000000 : (regno) rs : (regno) rt : 0b00000 : 0b00000 : 0b011101) = +function clause decode (0b000000 @ rs : regno @ rt : regno @ 0b00000 @ 0b00000 @ 0b011101) = Some(DMULTU(rs, rt)) function clause execute (DMULTU(rs, rt)) = { - (bit[128]) result := rGPR(rs) * rGPR(rt); - HI := (result[127..64]); - LO := (result[63..0]); + (bits(128)) result = rGPR(rs) * rGPR(rt); + HI = (result[127..64]); + LO = (result[63..0]); } -(* MADD 32-bit signed multiply and add into HI/LO *) +/* MADD 32-bit signed multiply and add into HI/LO */ union ast member (regno, regno) MADD -function clause decode (0b011100 : (regno) rs : (regno) rt : 0b00000 : 0b00000 : 0b000000) = +function clause decode (0b011100 @ rs : regno @ rt : regno @ 0b00000 @ 0b00000 @ 0b000000) = Some(MADD(rs, rt)) function clause execute (MADD(rs, rt)) = { - rsVal := rGPR(rs); - rtVal := rGPR(rt); - (bit[64]) mul_result := if (NotWordVal(rsVal) | NotWordVal(rtVal)) then + rsVal = rGPR(rs); + rtVal = rGPR(rt); + (bits(64)) mul_result = if (NotWordVal(rsVal) | NotWordVal(rtVal)) then undefined else rsVal[31..0] *_s rtVal[31..0]; - (bit[64]) result := mul_result + (HI[31..0] : LO[31..0]); - HI := EXTS(result[63..32]); - LO := EXTS(result[31..0]); + (bits(64)) result = mul_result + (HI[31..0] : LO[31..0]); + HI = EXTS(result[63..32]); + LO = EXTS(result[31..0]); } -(* MADDU 32-bit unsigned multiply and add into HI/LO *) +/* MADDU 32-bit unsigned multiply and add into HI/LO */ union ast member (regno, regno) MADDU -function clause decode (0b011100 : (regno) rs : (regno) rt : 0b00000 : 0b00000 : 0b000001) = +function clause decode (0b011100 @ rs : regno @ rt : regno @ 0b00000 @ 0b00000 @ 0b000001) = Some(MADDU(rs, rt)) function clause execute (MADDU(rs, rt)) = { - rsVal := rGPR(rs); - rtVal := rGPR(rt); - (bit[64]) mul_result := if (NotWordVal(rsVal) | NotWordVal(rtVal)) then + rsVal = rGPR(rs); + rtVal = rGPR(rt); + (bits(64)) mul_result = if (NotWordVal(rsVal) | NotWordVal(rtVal)) then undefined else rsVal[31..0] * rtVal[31..0]; - (bit[64]) result := mul_result + (HI[31..0] : LO[31..0]); - HI := EXTS(result[63..32]); - LO := EXTS(result[31..0]); + (bits(64)) result = mul_result + (HI[31..0] : LO[31..0]); + HI = EXTS(result[63..32]); + LO = EXTS(result[31..0]); } -(* MSUB 32-bit signed multiply and sub from HI/LO *) +/* MSUB 32-bit signed multiply and sub from HI/LO */ union ast member (regno, regno) MSUB -function clause decode (0b011100 : (regno) rs : (regno) rt : 0b00000 : 0b00000 : 0b000100) = +function clause decode (0b011100 @ rs : regno @ rt : regno @ 0b00000 @ 0b00000 @ 0b000100) = Some(MSUB(rs, rt)) function clause execute (MSUB(rs, rt)) = { - rsVal := rGPR(rs); - rtVal := rGPR(rt); - (bit[64]) mul_result := if (NotWordVal(rsVal) | NotWordVal(rtVal)) then + rsVal = rGPR(rs); + rtVal = rGPR(rt); + (bits(64)) mul_result = if (NotWordVal(rsVal) | NotWordVal(rtVal)) then undefined else rsVal[31..0] *_s rtVal[31..0]; - (bit[64]) result := (HI[31..0] : LO[31..0]) - mul_result; - HI := EXTS(result[63..32]); - LO := EXTS(result[31..0]); + (bits(64)) result = (HI[31..0] : LO[31..0]) - mul_result; + HI = EXTS(result[63..32]); + LO = EXTS(result[31..0]); } -(* MSUBU 32-bit unsigned multiply and sub from HI/LO *) +/* MSUBU 32-bit unsigned multiply and sub from HI/LO */ union ast member (regno, regno) MSUBU -function clause decode (0b011100 : (regno) rs : (regno) rt : 0b00000 : 0b00000 : 0b000101) = +function clause decode (0b011100 @ rs : regno @ rt : regno @ 0b00000 @ 0b00000 @ 0b000101) = Some(MSUBU(rs, rt)) function clause execute (MSUBU(rs, rt)) = { - rsVal := rGPR(rs); - rtVal := rGPR(rt); - (bit[64]) mul_result := if (NotWordVal(rsVal) | NotWordVal(rtVal)) then + rsVal = rGPR(rs); + rtVal = rGPR(rt); + (bits(64)) mul_result = if (NotWordVal(rsVal) | NotWordVal(rtVal)) then undefined else rsVal[31..0] * rtVal[31..0]; - (bit[64]) result := (HI[31..0] : LO[31..0]) - mul_result; - HI := EXTS(result[63..32]); - LO := EXTS(result[31..0]); + (bits(64)) result = (HI[31..0] : LO[31..0]) - mul_result; + HI = EXTS(result[63..32]); + LO = EXTS(result[31..0]); } -(* DIV 32-bit divide into HI/LO *) +/* DIV 32-bit divide into HI/LO */ union ast member (regno, regno) DIV -function clause decode (0b000000 : (regno) rs : (regno) rt : 0b00000 : 0b00000 : 0b011010) = +function clause decode (0b000000 @ rs : regno @ rt : regno @ 0b00000 @ 0b00000 @ 0b011010) = Some(DIV(rs, rt)) function clause execute (DIV(rs, rt)) = { - rsVal := rGPR(rs); - rtVal := rGPR(rt); - let ((bit[32]) q, (bit[32])r) = ( + rsVal = rGPR(rs); + rtVal = rGPR(rt); + let q : (bits(32), (bits(32))r) = ( if (NotWordVal(rsVal) | NotWordVal(rtVal) | (rtVal == 0)) then - ((bit[32]) undefined, (bit[32]) undefined) + ((bits(32)) undefined, (bits(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]) (to_svec(qi)), (bit[32]) (to_svec(ri)))) + ((bits(32)) (to_svec(qi)), (bits(32)) (to_svec(ri)))) in { - HI := EXTS(r); - LO := EXTS(q); + HI = EXTS(r); + LO = EXTS(q); } } -(* DIVU 32-bit unsigned divide into HI/LO *) +/* DIVU 32-bit unsigned divide into HI/LO */ union ast member (regno, regno) DIVU -function clause decode (0b000000 : (regno) rs : (regno) rt : 0b00000 : 0b00000 : 0b011011) = +function clause decode (0b000000 @ rs : regno @ rt : regno @ 0b00000 @ 0b00000 @ 0b011011) = Some(DIVU(rs, rt)) function clause execute (DIVU(rs, rt)) = { - rsVal := rGPR(rs); - rtVal := rGPR(rt); - let ((bit[32]) q, (bit[32])r) = ( + rsVal = rGPR(rs); + rtVal = rGPR(rt); + let q : (bits(32), (bits(32))r) = ( if (NotWordVal(rsVal) | NotWordVal(rtVal) | rtVal == 0) then - ((bit[32]) undefined, (bit[32]) undefined) + ((bits(32)) undefined, (bits(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]) (to_svec(qi)), (bit[32]) (to_svec(ri)))) + ((bits(32)) (to_svec(qi)), (bits(32)) (to_svec(ri)))) in { - HI := EXTS(r); - LO := EXTS(q); + HI = EXTS(r); + LO = EXTS(q); } } -(* DDIV 64-bit divide into HI/LO *) +/* DDIV 64-bit divide into HI/LO */ union ast member (regno, regno) DDIV -function clause decode (0b000000 : (regno) rs : (regno) rt : 0b00000 : 0b00000 : 0b011110) = +function clause decode (0b000000 @ rs : regno @ rt : regno @ 0b00000 @ 0b00000 @ 0b011110) = Some(DDIV(rs, rt)) 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 ((bit[64]) undefined, (bit[64]) undefined) + rsVal = signed(rGPR(rs)); + rtVal = signed(rGPR(rt)); + let ((bits(64))q, (bits(64))r) = (if (rtVal == 0) + then ((bits(64)) undefined, (bits(64)) undefined) else let qi = (rsVal quot rtVal) in let ri = (rsVal - (qi * rtVal)) in - ((bit[64]) (to_svec(qi)), (bit[64]) (to_svec(ri)))) in + ((bits(64)) (to_svec(qi)), (bits(64)) (to_svec(ri)))) in { - LO := q; - HI := r; + LO = q; + HI = r; } } -(* DDIV 64-bit divide into HI/LO *) +/* DDIV 64-bit divide into HI/LO */ union ast member (regno, regno) DDIVU -function clause decode (0b000000 : (regno) rs : (regno) rt : 0b00000 : 0b00000 : 0b011111) = +function clause decode (0b000000 @ rs : regno @ rt : regno @ 0b00000 @ 0b00000 @ 0b011111) = Some(DDIVU(rs, rt)) 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 ((bit[64]) undefined, (bit[64]) undefined) + (int) rsVal = rGPR(rs); + (int) rtVal = rGPR(rt); + let ((bits(64))q, (bits(64))r) = (if (rtVal == 0) + then ((bits(64)) undefined, (bits(64)) undefined) else let qi = (rsVal quot rtVal) in let ri = (rsVal mod rtVal) in - ((bit[64]) (to_svec(qi)), (bit[64]) (to_svec(ri)))) in + ((bits(64)) (to_svec(qi)), (bits(64)) (to_svec(ri)))) in { - LO := q; - HI := r; + LO = q; + HI = r; } } -(**************************************************************************************) -(* Jump instructions -- unconditional branches *) -(**************************************************************************************) +/**************************************************************************************/ +/* Jump instructions -- unconditional branches */ +/**************************************************************************************/ -(* J - jump, the simplest control flow instruction, with branch delay slot *) -union ast member (bit[26]) J -function clause decode (0b000010 : (bit[26]) offset) = +/* J - jump, the simplest control flow instruction, with branch delay slot */ +union ast member (bits(26)) J +function clause decode (0b000010 @ (bits(26)) offset) = Some(J(offset)) function clause execute (J(offset)) = { - delayedPC := (PC + 4)[63..28] : offset : 0b00; - branchPending := 1 + delayedPC = (PC + 4)[63..28] : offset : 0b00; + branchPending = 1 } -(* JAL - jump and link *) -union ast member (bit[26]) JAL -function clause decode (0b000011 : (bit[26]) offset) = +/* JAL - jump and link */ +union ast member (bits(26)) JAL +function clause decode (0b000011 @ (bits(26)) offset) = Some(JAL(offset)) function clause execute (JAL(offset)) = { - delayedPC := (PC + 4)[63..28] : offset : 0b00; - branchPending := 1; - wGPR(0b11111) := PC + 8; + delayedPC = (PC + 4)[63..28] : offset : 0b00; + branchPending = 1; + wGPR(0b11111) = PC + 8; } -(* JR -- jump via register *) +/* JR -- jump via register */ union ast member regno JR -function clause decode (0b000000 : (regno) rs : 0b00000 : 0b00000 : (regno) hint : 0b001000) = - Some(JR(rs)) (* hint is ignored *) +function clause decode (0b000000 @ rs : regno @ 0b00000 @ 0b00000 @ hint : regno @ 0b001000) = + Some(JR(rs)) /* hint is ignored */ function clause execute (JR(rs)) = { - delayedPC := rGPR(rs); - branchPending := 1; + delayedPC = rGPR(rs); + branchPending = 1; } -(* JALR -- jump via register with link *) +/* JALR -- jump via register with link */ union ast member (regno, regno) JALR -function clause decode (0b000000 : (regno) rs : 0b00000 : (regno) rd : (regno) hint : 0b001001) = - Some(JALR(rs, rd)) (* hint is ignored *) +function clause decode (0b000000 @ rs : regno @ 0b00000 @ rd : regno @ hint : regno @ 0b001001) = + Some(JALR(rs, rd)) /* hint is ignored */ function clause execute (JALR(rs, rd)) = { - delayedPC := rGPR(rs); - branchPending := 1; - wGPR(rd) := PC + 8; + delayedPC = rGPR(rs); + branchPending = 1; + wGPR(rd) = PC + 8; } -(**************************************************************************************) -(* B[N]EQ[L] - branch on (not) equal (likely) *) -(* Conditional branch instructions with two register operands *) -(**************************************************************************************) +/**************************************************************************************/ +/* B[N]EQ[L] - branch on (not) equal (likely) */ +/* Conditional branch instructions with two register operands */ +/**************************************************************************************/ union ast member (regno, regno, imm16, bool, bool) BEQ -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) = - Some(BEQ(rs, rt, imm, false, true)) (* BEQL *) -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) = - Some(BEQ(rs, rt, imm, true , true)) (* BNEL *) +function clause decode (0b000100 @ rs : regno @ rt : regno @ imm : imm16) = + Some(BEQ(rs, rt, imm, false, false)) /* BEQ */ +function clause decode (0b010100 @ rs : regno @ rt : regno @ imm : imm16) = + Some(BEQ(rs, rt, imm, false, true)) /* BEQL */ +function clause decode (0b000101 @ rs : regno @ rt : regno @ imm : imm16) = + Some(BEQ(rs, rt, imm, true , false)) /* BNE */ +function clause decode (0b010101 @ rs : regno @ rt : regno @ imm : imm16) = + Some(BEQ(rs, rt, imm, true , true)) /* BNEL */ function clause execute (BEQ(rs, rd, imm, ne, likely)) = { if ((rGPR(rs) == rGPR(rd)) ^ ne) then { - let (bit[64]) offset = (EXTS(imm : 0b00) + 4) in - delayedPC := PC + offset; - branchPending := 1; + let offset : bits(64) = (EXTS(imm : 0b00) + 4) in + delayedPC = PC + offset; + branchPending = 1; } else { if (likely) then - nextPC := PC + 8; (* skip branch delay *) + nextPC = PC + 8; /* skip branch delay */ } } -(* +/* Branches comparing with zero (single register operand, possible link in r31) -*) +*/ -(**************************************************************************************) -(* BGEZ[AL][L] - branch on comparison with zero (possibly link, likely) *) -(* Conditional branch instructions with single register operand *) -(**************************************************************************************) +/**************************************************************************************/ +/* BGEZ[AL][L] - branch on comparison with zero (possibly link, likely) */ +/* Conditional branch instructions with single register operand */ +/**************************************************************************************/ union ast member (regno, imm16, Comparison, bool, bool) BCMPZ -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) = - Some(BCMPZ(rs, imm, LT, true, false)) (* BLTZAL *) -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) = - Some(BCMPZ(rs, imm, LT, true, true)) (* BLTZALL *) - -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) = - Some(BCMPZ(rs, imm, GE, true, false)) (* BGEZAL *) -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) = - Some(BCMPZ(rs, imm, GE, true, true)) (* BGEZALL *) - -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) = - Some(BCMPZ(rs, imm, GT, false, true)) (* BGTZL *) - -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) = - Some(BCMPZ(rs, imm, LE, false, true)) (* BLEZL *) +function clause decode (0b000001 @ rs : regno @ 0b00000 @ imm : imm16) = + Some(BCMPZ(rs, imm, LT, false, false)) /* BLTZ */ +function clause decode (0b000001 @ rs : regno @ 0b10000 @ imm : imm16) = + Some(BCMPZ(rs, imm, LT, true, false)) /* BLTZAL */ +function clause decode (0b000001 @ rs : regno @ 0b00010 @ imm : imm16) = + Some(BCMPZ(rs, imm, LT, false, true)) /* BLTZL */ +function clause decode (0b000001 @ rs : regno @ 0b10010 @ imm : imm16) = + Some(BCMPZ(rs, imm, LT, true, true)) /* BLTZALL */ + +function clause decode (0b000001 @ rs : regno @ 0b00001 @ imm : imm16) = + Some(BCMPZ(rs, imm, GE, false, false)) /* BGEZ */ +function clause decode (0b000001 @ rs : regno @ 0b10001 @ imm : imm16) = + Some(BCMPZ(rs, imm, GE, true, false)) /* BGEZAL */ +function clause decode (0b000001 @ rs : regno @ 0b00011 @ imm : imm16) = + Some(BCMPZ(rs, imm, GE, false, true)) /* BGEZL */ +function clause decode (0b000001 @ rs : regno @ 0b10011 @ imm : imm16) = + Some(BCMPZ(rs, imm, GE, true, true)) /* BGEZALL */ + +function clause decode (0b000111 @ rs : regno @ 0b00000 @ imm : imm16) = + Some(BCMPZ(rs, imm, GT, false, false)) /* BGTZ */ +function clause decode (0b010111 @ rs : regno @ 0b00000 @ imm : imm16) = + Some(BCMPZ(rs, imm, GT, false, true)) /* BGTZL */ + +function clause decode (0b000110 @ rs : regno @ 0b00000 @ imm : imm16) = + Some(BCMPZ(rs, imm, LE, false, false)) /* BLEZ */ +function clause decode (0b010110 @ rs : regno @ 0b00000 @ imm : imm16) = + Some(BCMPZ(rs, imm, LE, false, true)) /* BLEZL */ function clause execute (BCMPZ(rs, imm, cmp, link, likely)) = { - (bit[64]) linkVal := PC + 8; - regVal := rGPR(rs); - condition := compare(cmp, regVal, 0); + (bits(64)) linkVal = PC + 8; + regVal = rGPR(rs); + condition = compare(cmp, regVal, 0); if (condition) then { - let (bit[64]) offset = (EXTS(imm : 0b00) + 4) in - delayedPC := PC + offset; - branchPending := 1; + let offset : bits(64) = (EXTS(imm : 0b00) + 4) in + delayedPC = PC + offset; + branchPending = 1; } else if (likely) then { - nextPC := PC + 8 (* skip branch delay *) + nextPC = PC + 8 /* skip branch delay */ }; if (link) then - wGPR(0b11111) := linkVal + wGPR(0b11111) = linkVal } -(**************************************************************************************) -(* SYSCALL/BREAK/WAIT/Trap *) -(**************************************************************************************) +/**************************************************************************************/ +/* SYSCALL/BREAK/WAIT/Trap */ +/**************************************************************************************/ -(* Co-opt syscall 0xfffff for use as thread start in pccmem *) +/* Co-opt syscall 0xfffff for use as thread start in pccmem */ union ast member unit SYSCALL_THREAD_START -function clause decode (0b000000 : 0xfffff : 0b001100) = +function clause decode (0b000000 @ 0xfffff @ 0b001100) = Some((ast) SYSCALL_THREAD_START) function clause execute (SYSCALL_THREAD_START) = () -(* fake stop fetching instruction for ppcmem, execute doesn't do anything, - decode never produces it *) +/* fake stop fetching instruction for ppcmem, execute doesn't do anything, + decode never produces it */ union ast member unit ImplementationDefinedStopFetching function clause execute (ImplementationDefinedStopFetching) = () union ast member unit SYSCALL -function clause decode (0b000000 : (bit[20]) code : 0b001100) = - Some((ast) SYSCALL) (* code is ignored *) +function clause decode (0b000000 @ (bits(20)) code @ 0b001100) = + Some((ast) SYSCALL) /* code is ignored */ function clause execute (SYSCALL) = { (SignalException(Sys)) } -(* BREAK is identical to SYSCALL exception for the exception raised *) +/* BREAK is identical to SYSCALL exception for the exception raised */ union ast member unit BREAK -function clause decode (0b000000 : (bit[20]) code : 0b001101) = - Some((ast) BREAK) (* code is ignored *) +function clause decode (0b000000 @ (bits(20)) code @ 0b001101) = + Some((ast) BREAK) /* code is ignored */ function clause execute (BREAK) = { (SignalException(Bp)) } -(* Accept WAIT as a NOP *) +/* Accept WAIT as a NOP */ union ast member unit WAIT -function clause decode (0b010000 : 0x80000 : 0b100000) = - Some((ast) WAIT) (* we only accept code == 0 *) +function clause decode (0b010000 @ 0x80000 @ 0b100000) = + Some((ast) WAIT) /* we only accept code == 0 */ function clause execute (WAIT) = { - nextPC := PC; + nextPC = PC; } -(* Trap instructions with two register operands *) +/* 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) = - Some(TRAPREG(rs, rt, GE)) (* TGE *) -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) = - Some(TRAPREG(rs, rt, LT)) (* TLT *) -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) = - Some(TRAPREG(rs, rt, EQ)) (* TEQ *) -function clause decode (0b000000 : (regno) rs : (regno) rt : (bit[10]) code : 0b110110) = - Some(TRAPREG(rs, rt, NE)) (* TNE *) +function clause decode (0b000000 @ rs : regno @ rt : regno @ (bits(10)) code @ 0b110000) = + Some(TRAPREG(rs, rt, GE)) /* TGE */ +function clause decode (0b000000 @ rs : regno @ rt : regno @ (bits(10)) code @ 0b110001) = + Some(TRAPREG(rs, rt, GEU)) /* TGEU */ +function clause decode (0b000000 @ rs : regno @ rt : regno @ (bits(10)) code @ 0b110010) = + Some(TRAPREG(rs, rt, LT)) /* TLT */ +function clause decode (0b000000 @ rs : regno @ rt : regno @ (bits(10)) code @ 0b110011) = + Some(TRAPREG(rs, rt, LTU)) /* TLTU */ +function clause decode (0b000000 @ rs : regno @ rt : regno @ (bits(10)) code @ 0b110100) = + Some(TRAPREG(rs, rt, EQ)) /* TEQ */ +function clause decode (0b000000 @ rs : regno @ rt : regno @ (bits(10)) code @ 0b110110) = + Some(TRAPREG(rs, rt, NE)) /* TNE */ function clause execute (TRAPREG(rs, rt, cmp)) = { - rs_val := rGPR(rs); - rt_val := rGPR(rt); - condition := compare(cmp, rs_val, rt_val); + rs_val rGPR : =(rs); + rt_val rGPR : =(rt); + condition = compare(cmp, rs_val, rt_val); if (condition) then (SignalException(Tr)) } -(* Trap instructions with one register and one immediate operand *) +/* 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) = - Some(TRAPIMM(rs, imm, EQ)) (* TEQI *) -function clause decode (0b000001 : (regno) rs : 0b01110 : (imm16) imm) = - Some(TRAPIMM(rs, imm, NE)) (* TNEI *) -function clause decode (0b000001 : (regno) rs : 0b01000 : (imm16) imm) = - Some(TRAPIMM(rs, imm, GE)) (* TGEI *) -function clause decode (0b000001 : (regno) rs : 0b01001 : (imm16) imm) = - Some(TRAPIMM(rs, imm, GEU)) (* TGEIU *) -function clause decode (0b000001 : (regno) rs : 0b01010 : (imm16) imm) = - Some(TRAPIMM(rs, imm, LT)) (* TLTI *) -function clause decode (0b000001 : (regno) rs : 0b01011 : (imm16) imm) = - Some(TRAPIMM(rs, imm, LTU)) (* TLTIU *) +function clause decode (0b000001 @ rs : regno @ 0b01100 @ imm : imm16) = + Some(TRAPIMM(rs, imm, EQ)) /* TEQI */ +function clause decode (0b000001 @ rs : regno @ 0b01110 @ imm : imm16) = + Some(TRAPIMM(rs, imm, NE)) /* TNEI */ +function clause decode (0b000001 @ rs : regno @ 0b01000 @ imm : imm16) = + Some(TRAPIMM(rs, imm, GE)) /* TGEI */ +function clause decode (0b000001 @ rs : regno @ 0b01001 @ imm : imm16) = + Some(TRAPIMM(rs, imm, GEU)) /* TGEIU */ +function clause decode (0b000001 @ rs : regno @ 0b01010 @ imm : imm16) = + Some(TRAPIMM(rs, imm, LT)) /* TLTI */ +function clause decode (0b000001 @ rs : regno @ 0b01011 @ imm : imm16) = + Some(TRAPIMM(rs, imm, LTU)) /* TLTIU */ function clause execute (TRAPIMM(rs, imm, cmp)) = { - rs_val := rGPR(rs); - (bit[64]) imm_val := EXTS(imm); - condition := compare(cmp, rs_val, imm_val); + rs_val rGPR : =(rs); + (bits(64)) imm_val EXTS : =(imm); + condition = compare(cmp, rs_val, imm_val); if (condition) then (SignalException(Tr)) } -(**************************************************************************************) -(* Load instructions -- various width/signs *) -(**************************************************************************************) +/**************************************************************************************/ +/* Load instructions -- various width/signs */ +/**************************************************************************************/ union ast member (WordType, bool, bool, regno, regno, imm16) Load -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) = - Some(Load(B, false, false, base, rt, offset)) (* LBU *) -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) = - Some(Load(H, false, false, base, rt, offset)) (* LHU *) -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) = - Some(Load(W, false, false, base, rt, offset)) (* LWU *) -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) = - Some(Load(W, true, true, base, rt, offset)) (* LL *) -function clause decode (0b110100 : (regno) base : (regno) rt : (imm16) offset) = - Some(Load(D, false, true, base, rt, offset)) (* LLD *) - -val forall 'sz. (bit['sz], bool) -> bit[64] effect pure extendLoad +function clause decode (0b100000 @ base : regno @ rt : regno @ offset : imm16) = + Some(Load(B, true, false, base, rt, offset)) /* LB */ +function clause decode (0b100100 @ base : regno @ rt : regno @ offset : imm16) = + Some(Load(B, false, false, base, rt, offset)) /* LBU */ +function clause decode (0b100001 @ base : regno @ rt : regno @ offset : imm16) = + Some(Load(H, true, false, base, rt, offset)) /* LH */ +function clause decode (0b100101 @ base : regno @ rt : regno @ offset : imm16) = + Some(Load(H, false, false, base, rt, offset)) /* LHU */ +function clause decode (0b100011 @ base : regno @ rt : regno @ offset : imm16) = + Some(Load(W, true, false, base, rt, offset)) /* LW */ +function clause decode (0b100111 @ base : regno @ rt : regno @ offset : imm16) = + Some(Load(W, false, false, base, rt, offset)) /* LWU */ +function clause decode (0b110111 @ base : regno @ rt : regno @ offset : imm16) = + Some(Load(D, false, false, base, rt, offset)) /* LD */ +function clause decode (0b110000 @ base : regno @ rt : regno @ offset : imm16) = + Some(Load(W, true, true, base, rt, offset)) /* LL */ +function clause decode (0b110100 @ base : regno @ rt : regno @ offset : imm16) = + Some(Load(D, false, true, base, rt, offset)) /* LLD */ + +val extendLoad : forall 'sz. (bits('sz), bool) -> bits(64) effect pure function extendLoad(memResult, signed) = { if (signed) then EXTS(memResult) @@ -1122,17 +1122,17 @@ function extendLoad(memResult, signed) = { function clause execute (Load(width, signed, linked, base, rt, offset)) = { - (bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), LoadData, width); + (bits(64)) vAddr = addrWrapper(EXTS(offset) + rGPR(base), LoadData, width); if ~ (isAddressAligned(vAddr, width)) then - (SignalExceptionBadAddr(AdEL, vAddr)) (* unaligned access *) + (SignalExceptionBadAddr(AdEL, vAddr)) /* unaligned access */ else let pAddr = (TLBTranslate(vAddr, LoadData)) in { - (bit[64]) memResult := if (linked) then + (bits(64)) memResult = if (linked) then { - CP0LLBit := 0b1; - CP0LLAddr := pAddr; - w := wordWidthBytes(width); + CP0LLBit = 0b1; + CP0LLAddr = pAddr; + w = wordWidthBytes(width); if w == 1 then extendLoad(MEMr_reserve_wrapper(pAddr, 1), signed) else if w == 2 then extendLoad(MEMr_reserve_wrapper(pAddr, 2), signed) else if w == 4 then extendLoad(MEMr_reserve_wrapper(pAddr, 4), signed) @@ -1140,549 +1140,549 @@ function clause execute (Load(width, signed, linked, base, rt, offset)) = } else { - w := wordWidthBytes(width); + w = wordWidthBytes(width); if w == 1 then extendLoad(MEMr_reserve_wrapper(pAddr, 1), signed) else if w == 2 then extendLoad(MEMr_reserve_wrapper(pAddr, 2), signed) else if w == 4 then extendLoad(MEMr_reserve_wrapper(pAddr, 4), signed) else extendLoad(MEMr_reserve_wrapper(pAddr, 8), signed); }; - wGPR(rt) := memResult + wGPR(rt) = memResult } } -(**************************************************************************************) -(* Store instructions -- various widths *) -(**************************************************************************************) +/**************************************************************************************/ +/* Store instructions -- various widths */ +/**************************************************************************************/ union ast member (WordType, bool, regno, regno, imm16) Store -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) = - Some(Store(H, false, base, rt, offset)) (* SH *) -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) = - Some(Store(D, false, base, rt, offset)) (* SD *) -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) = - Some(Store(D, true, base, rt, offset)) (* SCD *) +function clause decode (0b101000 @ base : regno @ rt : regno @ offset : imm16) = + Some(Store(B, false, base, rt, offset)) /* SB */ +function clause decode (0b101001 @ base : regno @ rt : regno @ offset : imm16) = + Some(Store(H, false, base, rt, offset)) /* SH */ +function clause decode (0b101011 @ base : regno @ rt : regno @ offset : imm16) = + Some(Store(W, false, base, rt, offset)) /* SW */ +function clause decode (0b111111 @ base : regno @ rt : regno @ offset : imm16) = + Some(Store(D, false, base, rt, offset)) /* SD */ +function clause decode (0b111000 @ base : regno @ rt : regno @ offset : imm16) = + Some(Store(W, true, base, rt, offset)) /* SC */ +function clause decode (0b111100 @ base : regno @ rt : regno @ offset : imm16) = + Some(Store(D, true, base, rt, offset)) /* SCD */ function clause execute (Store(width, conditional, base, rt, offset)) = { - (bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), StoreData, width); - (bit[64]) rt_val := rGPR(rt); + (bits(64)) vAddr = addrWrapper(EXTS(offset) + rGPR(base), StoreData, width); + (bits(64)) rt_val rGPR : =(rt); if ~ (isAddressAligned(vAddr, width)) then - (SignalExceptionBadAddr(AdES, vAddr)) (* unaligned access *) + (SignalExceptionBadAddr(AdES, vAddr)) /* unaligned access */ else let pAddr = (TLBTranslate(vAddr, StoreData)) in { if (conditional) then { - success := if (CP0LLBit[0]) then (bool) switch(width) + success = if (CP0LLBit[0]) then (bool) match 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) + B => MEMw_conditional_wrapper(pAddr, 1, rt_val[7..0]) + H => MEMw_conditional_wrapper(pAddr, 2, rt_val[15..0]) + W => MEMw_conditional_wrapper(pAddr, 4, rt_val[31..0]) + D => MEMw_conditional_wrapper(pAddr, 8, rt_val) } else false; - wGPR(rt) := EXTZ([bool_to_bit(success)]) + wGPR(rt) = EXTZ([bool_to_bit(success)]) } else - switch(width) + match width { - case B -> MEMw_wrapper(pAddr, 1) := rt_val[7..0] - case H -> MEMw_wrapper(pAddr, 2) := rt_val[15..0] - case W -> MEMw_wrapper(pAddr, 4) := rt_val[31..0] - case D -> MEMw_wrapper(pAddr, 8) := rt_val + B => MEMw_wrapper(pAddr, 1) = rt_val[7..0] + H => MEMw_wrapper(pAddr, 2) = rt_val[15..0] + W => MEMw_wrapper(pAddr, 4) = rt_val[31..0] + D => MEMw_wrapper(pAddr, 8) = rt_val } } } -(* LWL - Load word left (big-endian only) *) +/* LWL - Load word left (big-endian only) */ union ast member regregimm16 LWL -function clause decode(0b100010 : (regno) base : (regno) rt : (imm16) offset) = +function clause decode(0b100010 @ base : regno @ rt : regno @ offset : imm16) = Some(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); + /* XXX length check not quite right, but conservative */ + (bits(64)) vAddr = addrWrapper(EXTS(offset) + rGPR(base), LoadData, W); let pAddr = (TLBTranslate(vAddr, LoadData)) in { - mem_val := MEMr_wrapper (pAddr[63..2] : 0b00, 4); (* read word of interest *) - reg_val := rGPR(rt); - wGPR(rt) := EXTS((bit[32]) switch(vAddr[1..0]) + mem_val interest : = MEMr_wrapper (pAddr[63..2] : 0b00, 4); /* read word of */ + reg_val rGPR : =(rt); + wGPR(rt) = EXTS((bits(32)) match 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] + 0b00 => mem_val + 0b01 => mem_val[23..0] : reg_val[07..0] + 0b10 => mem_val[15..0] : reg_val[15..0] + 0b11 => mem_val[07..0] : reg_val[23..0] }); } } union ast member regregimm16 LWR -function clause decode(0b100110 : (regno) base : (regno) rt : (imm16) offset) = +function clause decode(0b100110 @ base : regno @ rt : regno @ offset : imm16) = Some(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); + /* XXX length check not quite right, but conservative */ + (bits(64)) vAddr = addrWrapper(EXTS(offset) + rGPR(base), LoadData, W); let pAddr = (TLBTranslate(vAddr, LoadData)) in { - mem_val := MEMr_wrapper (pAddr[63..2] : 0b00, 4); (* read word of interest *) - reg_val := rGPR(rt); - wGPR(rt) := EXTS((bit[32]) switch(vAddr[1..0]) (* it is acceptable to sign extend in all cases *) + mem_val interest : = MEMr_wrapper (pAddr[63..2] : 0b00, 4); /* read word of */ + reg_val rGPR : =(rt); + wGPR(rt) = EXTS((bits(32)) match 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] - case 0b10 -> reg_val[31..24] : mem_val[31..8] - case 0b11 -> mem_val + 0b00 => reg_val[31..8] : mem_val[31..24] + 0b01 => reg_val[31..16] : mem_val[31..16] + 0b10 => reg_val[31..24] : mem_val[31..8] + 0b11 => mem_val }); } } -(* SWL - Store word left *) +/* SWL - Store word left */ union ast member regregimm16 SWL -function clause decode(0b101010 : (regno) base : (regno) rt : (imm16) offset) = +function clause decode(0b101010 @ base : regno @ rt : regno @ offset : imm16) = Some(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); + /* XXX length check not quite right, but conservative */ + (bits(64)) vAddr = addrWrapper(EXTS(offset) + rGPR(base), StoreData, W); let pAddr = (TLBTranslate(vAddr, StoreData)) in { - reg_val := rGPR(rt); - switch (vAddr[1..0]) + reg_val rGPR : =(rt); + match vAddr[1..0] { - case 0b00 -> (MEMw_wrapper(pAddr, 4) := reg_val[31..0]) - case 0b01 -> (MEMw_wrapper(pAddr, 3) := reg_val[31..8]) - case 0b10 -> (MEMw_wrapper(pAddr, 2) := reg_val[31..16]) - case 0b11 -> (MEMw_wrapper(pAddr, 1) := reg_val[31..24]) + 0b00 => (MEMw_wrapper(pAddr, 4) = reg_val[31..0]) + 0b01 => (MEMw_wrapper(pAddr, 3) = reg_val[31..8]) + 0b10 => (MEMw_wrapper(pAddr, 2) = reg_val[31..16]) + 0b11 => (MEMw_wrapper(pAddr, 1) = reg_val[31..24]) } } } union ast member regregimm16 SWR -function clause decode(0b101110 : (regno) base : (regno) rt : (imm16) offset) = +function clause decode(0b101110 @ base : regno @ rt : regno @ offset : imm16) = Some(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); - let (pAddr) = (TLBTranslate(vAddr, StoreData)) in + /* XXX length check not quite right, but conservative */ + (bits(64)) vAddr = addrWrapper(EXTS(offset) + rGPR(base), StoreData, W); + let TLBTranslate : pAddr(vAddr, StoreData)) in { - wordAddr := pAddr[63..2] : 0b00; - reg_val := rGPR(rt); - switch (vAddr[1..0]) + wordAddr = pAddr[63..2] : 0b00; + reg_val rGPR : =(rt); + match vAddr[1..0] { - case 0b00 -> (MEMw_wrapper(wordAddr, 1) := reg_val[7..0]) - case 0b01 -> (MEMw_wrapper(wordAddr, 2) := reg_val[15..0]) - case 0b10 -> (MEMw_wrapper(wordAddr, 3) := reg_val[23..0]) - case 0b11 -> (MEMw_wrapper(wordAddr, 4) := reg_val[31..0]) + 0b00 => (MEMw_wrapper(wordAddr, 1) = reg_val[7..0]) + 0b01 => (MEMw_wrapper(wordAddr, 2) = reg_val[15..0]) + 0b10 => (MEMw_wrapper(wordAddr, 3) = reg_val[23..0]) + 0b11 => (MEMw_wrapper(wordAddr, 4) = reg_val[31..0]) } } } -(* Load double-word left *) +/* Load double-word left */ union ast member regregimm16 LDL -function clause decode(0b011010 : (regno) base : (regno) rt : (imm16) offset) = +function clause decode(0b011010 @ base : regno @ rt : regno @ offset : imm16) = Some(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); + /* XXX length check not quite right, but conservative */ + (bits(64)) vAddr = addrWrapper(EXTS(offset) + rGPR(base), LoadData, D); let pAddr = (TLBTranslate(vAddr, StoreData)) in { - mem_val := MEMr_wrapper (pAddr[63..3] : 0b000, 8); (* read double of interest *) - reg_val := rGPR(rt); - wGPR(rt) := switch(vAddr[2..0]) + mem_val interest : = MEMr_wrapper (pAddr[63..3] : 0b000, 8); /* read double of */ + reg_val rGPR : =(rt); + wGPR(rt) = match vAddr[2..0] { - case 0b000 -> mem_val - case 0b001 -> mem_val[55..0] : reg_val[7..0] - case 0b010 -> mem_val[47..0] : reg_val[15..0] - case 0b011 -> mem_val[39..0] : reg_val[23..0] - case 0b100 -> mem_val[31..0] : reg_val[31..0] - case 0b101 -> mem_val[23..0] : reg_val[39..0] - case 0b110 -> mem_val[15..0] : reg_val[47..0] - case 0b111 -> mem_val[07..0] : reg_val[55..0] + 0b000 => mem_val + 0b001 => mem_val[55..0] : reg_val[7..0] + 0b010 => mem_val[47..0] : reg_val[15..0] + 0b011 => mem_val[39..0] : reg_val[23..0] + 0b100 => mem_val[31..0] : reg_val[31..0] + 0b101 => mem_val[23..0] : reg_val[39..0] + 0b110 => mem_val[15..0] : reg_val[47..0] + 0b111 => mem_val[07..0] : reg_val[55..0] }; } } -(* Load double-word right *) +/* Load double-word right */ union ast member regregimm16 LDR -function clause decode(0b011011 : (regno) base : (regno) rt : (imm16) offset) = +function clause decode(0b011011 @ base : regno @ rt : regno @ offset : imm16) = Some(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); + /* XXX length check not quite right, but conservative */ + (bits(64)) vAddr = addrWrapper(EXTS(offset) + rGPR(base), LoadData, D); let pAddr = (TLBTranslate(vAddr, StoreData)) in { - mem_val := MEMr_wrapper (pAddr[63..3] : 0b000, 8); (* read double of interest *) - reg_val := rGPR(rt); - wGPR(rt) := switch(vAddr[2..0]) + mem_val interest : = MEMr_wrapper (pAddr[63..3] : 0b000, 8); /* read double of */ + reg_val rGPR : =(rt); + wGPR(rt) = match vAddr[2..0] { - case 0b000 -> reg_val[63..08] : mem_val[63..56] - case 0b001 -> reg_val[63..16] : mem_val[63..48] - case 0b010 -> reg_val[63..24] : mem_val[63..40] - case 0b011 -> reg_val[63..32] : mem_val[63..32] - case 0b100 -> reg_val[63..40] : mem_val[63..24] - case 0b101 -> reg_val[63..48] : mem_val[63..16] - case 0b110 -> reg_val[63..56] : mem_val[63..08] - case 0b111 -> mem_val + 0b000 => reg_val[63..08] : mem_val[63..56] + 0b001 => reg_val[63..16] : mem_val[63..48] + 0b010 => reg_val[63..24] : mem_val[63..40] + 0b011 => reg_val[63..32] : mem_val[63..32] + 0b100 => reg_val[63..40] : mem_val[63..24] + 0b101 => reg_val[63..48] : mem_val[63..16] + 0b110 => reg_val[63..56] : mem_val[63..08] + 0b111 => mem_val }; } } -(* SDL - Store double-word left *) +/* SDL - Store double-word left */ union ast member regregimm16 SDL -function clause decode(0b101100 : (regno) base : (regno) rt : (imm16) offset) = +function clause decode(0b101100 @ base : regno @ rt : regno @ offset : imm16) = Some(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); + /* XXX length check not quite right, but conservative */ + (bits(64)) vAddr = addrWrapper(EXTS(offset) + rGPR(base), StoreData, D); let pAddr = (TLBTranslate(vAddr, StoreData)) in { - reg_val := rGPR(rt); - switch (vAddr[2..0]) + reg_val rGPR : =(rt); + match vAddr[2..0] { - case 0b000 -> (MEMw_wrapper(pAddr, 8) := reg_val[63..00]) - case 0b001 -> (MEMw_wrapper(pAddr, 7) := reg_val[63..08]) - case 0b010 -> (MEMw_wrapper(pAddr, 6) := reg_val[63..16]) - case 0b011 -> (MEMw_wrapper(pAddr, 5) := reg_val[63..24]) - case 0b100 -> (MEMw_wrapper(pAddr, 4) := reg_val[63..32]) - case 0b101 -> (MEMw_wrapper(pAddr, 3) := reg_val[63..40]) - case 0b110 -> (MEMw_wrapper(pAddr, 2) := reg_val[63..48]) - case 0b111 -> (MEMw_wrapper(pAddr, 1) := reg_val[63..56]) + 0b000 => (MEMw_wrapper(pAddr, 8) = reg_val[63..00]) + 0b001 => (MEMw_wrapper(pAddr, 7) = reg_val[63..08]) + 0b010 => (MEMw_wrapper(pAddr, 6) = reg_val[63..16]) + 0b011 => (MEMw_wrapper(pAddr, 5) = reg_val[63..24]) + 0b100 => (MEMw_wrapper(pAddr, 4) = reg_val[63..32]) + 0b101 => (MEMw_wrapper(pAddr, 3) = reg_val[63..40]) + 0b110 => (MEMw_wrapper(pAddr, 2) = reg_val[63..48]) + 0b111 => (MEMw_wrapper(pAddr, 1) = reg_val[63..56]) } } } -(* SDR - Store double-word right *) +/* SDR - Store double-word right */ union ast member regregimm16 SDR -function clause decode(0b101101 : (regno) base : (regno) rt : (imm16) offset) = +function clause decode(0b101101 @ base : regno @ rt : regno @ offset : imm16) = Some(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); + /* XXX length check not quite right, but conservative */ + (bits(64)) vAddr = addrWrapper(EXTS(offset) + rGPR(base), StoreData, D); let pAddr = (TLBTranslate(vAddr, StoreData)) in { - reg_val := rGPR(rt); - wordAddr := pAddr[63..3] : 0b000; - switch (vAddr[2..0]) + reg_val rGPR : =(rt); + wordAddr = pAddr[63..3] : 0b000; + match vAddr[2..0] { - case 0b000 -> (MEMw_wrapper(wordAddr, 1) := reg_val[07..0]) - case 0b001 -> (MEMw_wrapper(wordAddr, 2) := reg_val[15..0]) - case 0b010 -> (MEMw_wrapper(wordAddr, 3) := reg_val[23..0]) - case 0b011 -> (MEMw_wrapper(wordAddr, 4) := reg_val[31..0]) - case 0b100 -> (MEMw_wrapper(wordAddr, 5) := reg_val[39..0]) - case 0b101 -> (MEMw_wrapper(wordAddr, 6) := reg_val[47..0]) - case 0b110 -> (MEMw_wrapper(wordAddr, 7) := reg_val[55..0]) - case 0b111 -> (MEMw_wrapper(wordAddr, 8) := reg_val[63..0]) + 0b000 => (MEMw_wrapper(wordAddr, 1) = reg_val[07..0]) + 0b001 => (MEMw_wrapper(wordAddr, 2) = reg_val[15..0]) + 0b010 => (MEMw_wrapper(wordAddr, 3) = reg_val[23..0]) + 0b011 => (MEMw_wrapper(wordAddr, 4) = reg_val[31..0]) + 0b100 => (MEMw_wrapper(wordAddr, 5) = reg_val[39..0]) + 0b101 => (MEMw_wrapper(wordAddr, 6) = reg_val[47..0]) + 0b110 => (MEMw_wrapper(wordAddr, 7) = reg_val[55..0]) + 0b111 => (MEMw_wrapper(wordAddr, 8) = reg_val[63..0]) } } } -(* CACHE - manipulate (non-existent) caches *) +/* CACHE - manipulate (non-existent) caches */ union ast member regregimm16 CACHE -function clause decode (0b101111 : (regno) base : (regno) op : (imm16) imm) = +function clause decode (0b101111 @ base : regno @ op : regno @ imm : imm16) = Some(CACHE(base, op, imm)) function clause execute (CACHE(base, op, imm)) = - checkCP0Access () (* pretty much a NOP because no caches *) + checkCP0Access () /* pretty much a NOP because no caches */ -(* PREF - prefetching into (non-existent) caches *) +/* PREF - prefetching into (non-existent) caches */ union ast member regregimm16 PREF -function clause decode (0b110011 : (regno) base : (regno) op : (imm16) imm) = +function clause decode (0b110011 @ base : regno @ op : regno @ imm : imm16) = Some(PREF(base, op, imm)) function clause execute (PREF(base, op, imm)) = - () (* XXX NOP *) + () /* XXX NOP */ -(* SYNC - Memory barrier *) +/* SYNC - Memory barrier */ union ast member unit SYNC -function clause decode (0b000000 : 0b00000 : 0b00000 : 0b00000 : (regno) stype : 0b001111) = - Some((ast) SYNC) (* stype is currently ignored *) +function clause decode (0b000000 @ 0b00000 @ 0b00000 @ 0b00000 @ stype : regno @ 0b001111) = + Some((ast) SYNC) /* stype is currently ignored */ function clause execute(SYNC) = MEM_sync() -union ast member (regno, regno, bit[3], bool) MFC0 -function clause decode (0b010000 : 0b00000 : (regno) rt : (regno) rd : 0b00000000 : (bit[3]) sel) = - 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 *) +union ast member (regno, regno, bits(3), bool) MFC0 +function clause decode (0b010000 @ 0b00000 @ rt : regno @ rd : regno @ 0b00000000 @ (bits(3)) sel) = + Some(MFC0(rt, rd, sel, false)) /* MFC0 */ +function clause decode (0b010000 @ 0b00001 @ rt : regno @ rd : regno @ 0b00000000 @ (bits(3)) sel) = + Some(MFC0(rt, rd, sel, true)) /* DMFC0 */ function clause execute (MFC0(rt, rd, sel, double)) = { checkCP0Access(); - let (bit[64]) result = switch (rd, sel) + let result : bits(64) = match rd, sel { - case (0b00000,0b000) -> let (bit[31]) idx = EXTZ(TLBIndex) in - (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 *) - case (0b00100,0b000) -> TLBContext (* 4, TLB Context *) - case (0b00101,0b000) -> EXTZ(TLBPageMask : 0x000) (* 5, TLB PageMask *) - case (0b00110,0b000) -> EXTZ(TLBWired) (* 6, TLB Wired *) - case (0b00111,0b000) -> EXTZ(CP0HWREna) (* 7, HWREna *) - case (0b01000,0b000) -> CP0BadVAddr (* 8, BadVAddr reg *) - case (0b01000,0b001) -> 0 (* 8, BadInstr reg XXX TODO *) - case (0b01001,0b000) -> EXTZ(CP0Count) (* 9, Count reg *) - case (0b01010,0b000) -> TLBEntryHi (* 10, TLB EntryHi *) - case (0b01011,0b000) -> EXTZ(CP0Compare) (* 11, Compare reg *) - case (0b01100,0b000) -> EXTZ(CP0Status) (* 12, Status reg *) - case (0b01101,0b000) -> EXTZ(CP0Cause) (* 13, Cause reg *) - case (0b01110,0b000) -> CP0EPC (* 14, EPC *) - case (0b01111,0b000) -> EXTZ(0x00000400) (* 15, sel 0: PrID processor ID *) - 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 *) - : 0b000 (* AR *) - : 0b001 (* MT standard TLB *) - : 0b0000 (* zero *) + (0b00000,0b000) => let idx : bits(31) = EXTZ(TLBIndex) in + (0x00000000 : TLBProbe : idx) /* 0, TLB Index */ + (0b00001,0b000) => EXTZ(TLBRandom) /* 1, TLB Random */ + (0b00010,0b000) => TLBEntryLo0 /* 2, TLB EntryLo0 */ + (0b00011,0b000) => TLBEntryLo1 /* 3, TLB EntryLo1 */ + (0b00100,0b000) => TLBContext /* 4, TLB Context */ + (0b00101,0b000) => EXTZ(TLBPageMask : 0x000) /* 5, TLB PageMask */ + (0b00110,0b000) => EXTZ(TLBWired) /* 6, TLB Wired */ + (0b00111,0b000) => EXTZ(CP0HWREna) /* 7, HWREna */ + (0b01000,0b000) => CP0BadVAddr /* 8, BadVAddr reg */ + (0b01000,0b001) => 0 /* 8, BadInstr reg XXX TODO */ + (0b01001,0b000) => EXTZ(CP0Count) /* 9, Count reg */ + (0b01010,0b000) => TLBEntryHi /* 10, TLB EntryHi */ + (0b01011,0b000) => EXTZ(CP0Compare) /* 11, Compare reg */ + (0b01100,0b000) => EXTZ(CP0Status) /* 12, Status reg */ + (0b01101,0b000) => EXTZ(CP0Cause) /* 13, Cause reg */ + (0b01110,0b000) => CP0EPC /* 14, EPC */ + (0b01111,0b000) => EXTZ(0x00000400) /* 15, sel 0: PrID processor ID */ + (0b01111,0b110) => 0 /* 15, sel 6: CHERI core ID */ + (0b01111,0b111) => 0 /* 15, sel 7: CHERI thread ID */ + (0b10000,0b000) => EXTZ(0b1 /* M */ /* 16, sel 0: Config0 */ + : 0b000000000000000 /* Impl */ + : 0b1 /* BE */ + : 0b10 /* AT */ + : 0b000 /* AR */ + : 0b001 /* MT standard TLB */ + : 0b0000 /* zero */ : 0b000) - case (0b10000,0b001) -> EXTZ( (* 16, sel 1: Config1 *) - 0b1 (* M *) - : TLBIndexMax (* 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. *) - : [bool_to_bit(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 (0b10000,0b101) -> 0x0000000000000000 (* 16, sel 5: Config5 beri specific -- no extended TLB *) - case (0b10001,0b000) -> CP0LLAddr (* 17, sel 0: LLAddr *) - case (0b10010,0b000) -> 0 (* 18, WatchLo *) - case (0b10011,0b000) -> 0 (* 19, WatchHi *) - case (0b10100,0b000) -> TLBXContext (* 20, XContext *) - case (0b11110,0b000) -> CP0ErrorEPC (* 30, ErrorEPC *) - case _ -> (SignalException(ResI)) + (0b10000,0b001) => EXTZ( /* 16, sel 1: Config1 */ + 0b1 /* M */ + : TLBIndexMax /* 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. */ + : [bool_to_bit(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 */ + (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. */ + (0b10000,0b011) => 0x0000000000002000 /* 16, sel 3: Config3 zero except for bit 13 == ulri */ + (0b10000,0b101) => 0x0000000000000000 /* 16, sel 5: Config5 beri specific -- no extended TLB */ + (0b10001,0b000) => CP0LLAddr /* 17, sel 0: LLAddr */ + (0b10010,0b000) => 0 /* 18, WatchLo */ + (0b10011,0b000) => 0 /* 19, WatchHi */ + (0b10100,0b000) => TLBXContext /* 20, XContext */ + (0b11110,0b000) => CP0ErrorEPC /* 30, ErrorEPC */ + _ => (SignalException(ResI)) } in - wGPR(rt) := if (double) then result else EXTS(result[31..0]) + wGPR(rt) = if (double) then result else EXTS(result[31..0]) } -(* simulator halt instruction "MTC0 rt, r23" (cheri specific behaviour) *) +/* simulator halt instruction "MTC0 rt, r23" (cheri specific behaviour) */ union ast member unit HCF -function clause decode (0b010000 : 0b00100 : (regno) rt : 0b10111 : 0b00000000000) = +function clause decode (0b010000 @ 0b00100 @ rt : regno @ 0b10111 @ 0b00000000000) = Some((ast) HCF) -function clause decode (0b010000 : 0b00100 : (regno) rt : 0b11010 : 0b00000000000) = +function clause decode (0b010000 @ 0b00100 @ rt : regno @ 0b11010 @ 0b00000000000) = Some((ast) HCF) function clause execute (HCF) = - () (* halt instruction actually executed by interpreter framework *) + () /* halt instruction actually executed by interpreter framework */ -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 *) +union ast member (regno, regno, bits(3), bool) MTC0 +function clause decode (0b010000 @ 0b00100 @ rt : regno @ rd : regno @ 0b00000000 @ (bits(3)) sel) = + Some(MTC0(rt, rd, sel, false)) /* MTC0 */ +function clause decode (0b010000 @ 0b00101 @ rt : regno @ rd : regno @ 0b00000000 @ (bits(3)) sel) = + Some(MTC0(rt, rd, sel, true)) /* DMTC0 */ function clause execute (MTC0(rt, rd, sel, double)) = { checkCP0Access(); - let reg_val = (rGPR(rt)) in - switch (rd, sel) + let reg_val in : = (rGPR(rt)) + match rd, sel { - case (0b00000,0b000) -> TLBIndex := mask(reg_val) (* NB no write to TLBProbe *) - case (0b00001,0b000) -> () (* TLBRandom is read only *) - case (0b00010,0b000) -> TLBEntryLo0 := reg_val - case (0b00011,0b000) -> TLBEntryLo1 := reg_val - case (0b00100,0b000) -> (TLBContext.PTEBase) := (reg_val[63..23]) - case (0b00100,0b010) -> CP0UserLocal := reg_val - case (0b00101,0b000) -> TLBPageMask := (reg_val[28..13]) - case (0b00110,0b000) -> { - TLBWired := mask(reg_val); - TLBRandom := TLBIndexMax; + (0b00000,0b000) => TLBIndex = mask(reg_val) /* NB no write to TLBProbe */ + (0b00001,0b000) => () /* TLBRandom is read only */ + (0b00010,0b000) => TLBEntryLo0 = reg_val + (0b00011,0b000) => TLBEntryLo1 = reg_val + (0b00100,0b000) => (TLBContext.PTEBase) = (reg_val[63..23]) + (0b00100,0b010) => CP0UserLocal = reg_val + (0b00101,0b000) => TLBPageMask = (reg_val[28..13]) + (0b00110,0b000) => { + TLBWired = mask(reg_val); + TLBRandom = TLBIndexMax; } - case (0b00111,0b000) -> CP0HWREna := (reg_val[31..29] : 0b0000000000000000000000000 : reg_val[3..0]) - case (0b01000,0b000) -> () (* BadVAddr read only *) - case (0b01001,0b000) -> CP0Count := reg_val[31..0] - case (0b01010,0b000) -> { - (TLBEntryHi.R) := (reg_val[63..62]); - (TLBEntryHi.VPN2) := (reg_val[39..13]); - (TLBEntryHi.ASID) := (reg_val[7..0]); + (0b00111,0b000) => CP0HWREna = (reg_val[31..29] : 0b0000000000000000000000000 : reg_val[3..0]) + (0b01000,0b000) => () /* BadVAddr read only */ + (0b01001,0b000) => CP0Count = reg_val[31..0] + (0b01010,0b000) => { + (TLBEntryHi.R) = (reg_val[63..62]); + (TLBEntryHi.VPN2) = (reg_val[39..13]); + (TLBEntryHi.ASID) = (reg_val[7..0]); } - case (0b01011,0b000) -> { (* 11, sel 0: Compare reg *) - CP0Compare := reg_val[31..0]; - (CP0Cause[15]) := bitzero; + (0b01011,0b000) => { /* 11, sel 0: Compare reg */ + CP0Compare = reg_val[31..0]; + (CP0Cause[15]) = bitzero; } - case (0b01100,0b000) -> { (* 12 Status *) - (CP0Status.CU) := reg_val[31..28]; - (CP0Status.BEV) := reg_val[22]; - (CP0Status.IM) := reg_val[15..8]; - (CP0Status.KX) := reg_val[7]; - (CP0Status.SX) := reg_val[6]; - (CP0Status.UX) := reg_val[5]; - (CP0Status.KSU) := reg_val[4..3]; - (CP0Status.ERL) := reg_val[2]; - (CP0Status.EXL) := reg_val[1]; - (CP0Status.IE) := reg_val[0]; + (0b01100,0b000) => { /* 12 Status */ + (CP0Status.CU) = reg_val[31..28]; + (CP0Status.BEV) = reg_val[22]; + (CP0Status.IM) = reg_val[15..8]; + (CP0Status.KX) = reg_val[7]; + (CP0Status.SX) = reg_val[6]; + (CP0Status.UX) = reg_val[5]; + (CP0Status.KSU) = reg_val[4..3]; + (CP0Status.ERL) = reg_val[2]; + (CP0Status.EXL) = reg_val[1]; + (CP0Status.IE) = reg_val[0]; } - case (0b01101,0b000) -> { (* 13 Cause *) - CP0Cause.IV := reg_val[23]; (* TODO special interrupt vector not implemeneted *) - let ip = (bit[8]) (CP0Cause.IP) in - CP0Cause.IP := ((ip[7..2]) : (reg_val[9..8])); + (0b01101,0b000) => { /* 13 Cause */ + CP0Cause.IV = reg_val[23]; /* TODO special interrupt vector not implemeneted */ + let ip = (bits(8)) (CP0Cause.IP) in + CP0Cause.IP = ((ip[7..2]) : (reg_val[9..8])); } - case (0b01110,0b000) -> CP0EPC := reg_val (* 14, EPC *) - case (0b10000,0b000) -> () (* XXX ignore K0 cache config 16: Config0 *) - case (0b10100,0b000) -> (TLBXContext.PTEBase) := (reg_val[63..33]) - case (0b11110,0b000) -> CP0ErrorEPC := reg_val (* 30, ErrorEPC *) - case _ -> (SignalException(ResI)) + (0b01110,0b000) => CP0EPC = reg_val EPC : /* 14, */ + (0b10000,0b000) => () /* XXX ignore K0 cache config 16: Config0 */ + (0b10100,0b000) => (TLBXContext.PTEBase) = (reg_val[63..33]) + (0b11110,0b000) => CP0ErrorEPC = reg_val ErrorEPC : /* 30, */ + _ => (SignalException(ResI)) } } function unit TLBWriteEntry((TLBIndexT) idx) = { - pagemask := (bit[16]) (EXTZ(TLBPageMask)); (* XXX EXTZ here forces register read in ocaml shallow embedding *) - switch(pagemask) { - case 0x0000 -> () - case 0x0003 -> () - case 0x000f -> () - case 0x003f -> () - case 0x00ff -> () - case 0x03ff -> () - case 0x0fff -> () - case 0x3fff -> () - case 0xffff -> () - case _ -> (SignalException(MCheck)) + pagemask = (bits(16)) (EXTZ(TLBPageMask)); /* XXX EXTZ here forces register read in ocaml shallow embedding */ + match pagemask { + 0x0000 => () + 0x0003 => () + 0x000f => () + 0x003f => () + 0x00ff => () + 0x03ff => () + 0x0fff => () + 0x3fff => () + 0xffff => () + _ => (SignalException(MCheck)) }; 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; + ((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 decode (0b010000 @ 0b10000000000000000000 @ 0b000010) = Some(TLBWI : ast) function clause execute (TLBWI) = { checkCP0Access(); TLBWriteEntry(TLBIndex); } union ast member TLBWR -function clause decode (0b010000 : 0b10000000000000000000 : 0b000110) = Some((ast) TLBWR) +function clause decode (0b010000 @ 0b10000000000000000000 @ 0b000110) = Some(TLBWR : ast) function clause execute (TLBWR) = { checkCP0Access(); TLBWriteEntry(TLBRandom); } union ast member TLBR -function clause decode (0b010000 : 0b10000000000000000000 : 0b000001) = Some((ast) TLBR) +function clause decode (0b010000 @ 0b10000000000000000000 @ 0b000001) = Some(TLBR : ast) function clause execute (TLBR) = { checkCP0Access(); let entry = TLBEntries[unsigned(TLBIndex)] in { - TLBPageMask := entry.pagemask; - TLBEntryHi.R := entry.r; - TLBEntryHi.VPN2 := entry.vpn2; - TLBEntryHi.ASID := entry.asid; - TLBEntryLo0.CapS:= entry.caps0; - TLBEntryLo0.CapL:= entry.capl0; - TLBEntryLo0.PFN := entry.pfn0; - TLBEntryLo0.C := entry.c0; - TLBEntryLo0.D := entry.d0; - TLBEntryLo0.V := entry.v0; - TLBEntryLo0.G := entry.g; - TLBEntryLo1.CapS:= entry.caps1; - TLBEntryLo1.CapL:= entry.capl1; - TLBEntryLo1.PFN := entry.pfn1; - TLBEntryLo1.C := entry.c1; - TLBEntryLo1.D := entry.d1; - TLBEntryLo1.V := entry.v1; - TLBEntryLo1.G := entry.g; + TLBPageMask = entry.pagemask; + TLBEntryHi.R = entry.r; + TLBEntryHi.VPN2 = entry.vpn2; + TLBEntryHi.ASID = entry.asid; + TLBEntryLo0.CapS= entry.caps0; + TLBEntryLo0.CapL= entry.capl0; + TLBEntryLo0.PFN = entry.pfn0; + TLBEntryLo0.C = entry.c0; + TLBEntryLo0.D = entry.d0; + TLBEntryLo0.V = entry.v0; + TLBEntryLo0.G = entry.g; + TLBEntryLo1.CapS= entry.caps1; + TLBEntryLo1.CapL= entry.capl1; + TLBEntryLo1.PFN = entry.pfn1; + TLBEntryLo1.C = entry.c1; + TLBEntryLo1.D = entry.d1; + TLBEntryLo1.V = entry.v1; + TLBEntryLo1.G = entry.g; } } union ast member TLBP -function clause decode (0b010000 : 0b10000000000000000000 : 0b001000) = Some((ast) TLBP) +function clause decode (0b010000 @ 0b10000000000000000000 @ 0b001000) = Some(TLBP : ast) function clause execute ((TLBP)) = { checkCP0Access(); let result = tlbSearch(TLBEntryHi) in - switch(result) { - case (Some(idx)) -> { - TLBProbe := [bitzero]; - TLBIndex := idx; + match result { + (Some(idx)) => { + TLBProbe = [bitzero]; + TLBIndex = idx; } - case None -> { - TLBProbe := [bitone]; - TLBIndex := 0b000000; + None => { + TLBProbe = [bitone]; + TLBIndex = 0b000000; } } } union ast member (regno, regno) RDHWR -function clause decode (0b011111 : 0b00000 : (regno) rt : (regno) rd : 0b00000 : 0b111011) = +function clause decode (0b011111 @ 0b00000 @ rt : regno @ rd : regno @ 0b00000 @ 0b111011) = Some(RDHWR(rt, rd)) function clause execute (RDHWR(rt, rd)) = { let accessLevel = getAccessLevel() in if ((accessLevel != Kernel) & (~((CP0Status.CU)[28])) & ~(CP0HWREna[rd])) then (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 _ -> (SignalException(ResI)) + let temp : bits(64) = match rd { + 0b00000 => EXTZ([bitzero]) /* CPUNum */ + 0b00001 => EXTZ([bitzero]) /* SYNCI_step */ + 0b00010 => EXTZ(CP0Count) /* Count */ + 0b00011 => EXTZ([bitone]) /* Count resolution */ + 0b11101 => CP0UserLocal /* User local register */ + _ => (SignalException(ResI)) } in - wGPR(rt) := temp; + wGPR(rt) = temp; } union ast member unit ERET -function clause decode (0b010000 : 0b1 : 0b0000000000000000000 : 0b011000) = +function clause decode (0b010000 @ 0b1 @ 0b0000000000000000000 @ 0b011000) = Some((ast) ERET) function clause execute (ERET) = { checkCP0Access(); ERETHook(); - CP0LLBit := 0b0; + CP0LLBit = 0b0; if (CP0Status.ERL == bitone) then { - nextPC := CP0ErrorEPC; - CP0Status.ERL := 0; + nextPC = CP0ErrorEPC; + CP0Status.ERL = 0; } else { - nextPC := CP0EPC; - CP0Status.EXL := 0; + nextPC = CP0EPC; + CP0Status.EXL = 0; } } |