summaryrefslogtreecommitdiff
path: root/mips_new_tc
diff options
context:
space:
mode:
authorRobert Norton2018-02-08 17:09:40 +0000
committerRobert Norton2018-02-08 17:10:23 +0000
commite9f6dd176d4f4791cc5c59e02b9eaaa0f3dc256f (patch)
tree83fccd65bd054fcce47b793e03c23a6ea2eebfd7 /mips_new_tc
parentb7e9ebcbbd660285e781b6912bf72751fa6b2b4e (diff)
work in progress mips sail2 port.
Diffstat (limited to 'mips_new_tc')
-rw-r--r--mips_new_tc/mips_ast_decl.sail78
-rw-r--r--mips_new_tc/mips_epilogue.sail70
-rw-r--r--mips_new_tc/mips_insts.sail1692
-rw-r--r--mips_new_tc/mips_prelude.sail806
-rw-r--r--mips_new_tc/mips_regfp.sail840
-rw-r--r--mips_new_tc/mips_ri.sail70
-rw-r--r--mips_new_tc/mips_tlb.sail154
-rw-r--r--mips_new_tc/mips_tlb_stub.sail72
-rw-r--r--mips_new_tc/mips_wrappers.sail96
-rw-r--r--mips_new_tc/prelude.sail393
10 files changed, 2255 insertions, 2016 deletions
diff --git a/mips_new_tc/mips_ast_decl.sail b/mips_new_tc/mips_ast_decl.sail
index 68e0558b..5d06eacb 100644
--- a/mips_new_tc/mips_ast_decl.sail
+++ b/mips_new_tc/mips_ast_decl.sail
@@ -1,44 +1,44 @@
-(*========================================================================*)
-(* *)
-(* 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. *)
-(*========================================================================*)
+/*========================================================================*/
+/* */
+/* 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 *)
+/* misp_insts.sail: mips instruction decode and execute clauses and AST node
+ declarations */
-scattered typedef ast = const union
+scattered type ast = const union
-val ast -> unit effect {barr, eamem, escape, rmem, rreg, undef, wmv, wreg} execute
+val execute : ast -> unit effect {barr, eamem, escape, rmem, rreg, undef, wmv, wreg}
scattered function unit execute
-val bit[32] -> option<ast> effect pure decode
-scattered function option<ast> decode
+val decode : bits(32) -> option(ast) effect pure
+scattered function option(ast) decode
diff --git a/mips_new_tc/mips_epilogue.sail b/mips_new_tc/mips_epilogue.sail
index 09ce7688..abec9ee9 100644
--- a/mips_new_tc/mips_epilogue.sail
+++ b/mips_new_tc/mips_epilogue.sail
@@ -1,41 +1,41 @@
-(*========================================================================*)
-(* *)
-(* 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. *)
-(*========================================================================*)
+/*========================================================================*/
+/* */
+/* 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. */
+/*========================================================================*/
-(* mips_epilogue.sail: end of decode, execute and AST definitions. *)
+/* mips_epilogue.sail: end of decode, execute and AST definitions. */
end decode
end execute
end ast
-function option<ast> supported_instructions (ast) instr = Some(instr)
+function option(ast) supported_instructions (ast) instr = Some(instr)
diff --git a/mips_new_tc/mips_insts.sail b/mips_new_tc/mips_insts.sail
index 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;
}
}
diff --git a/mips_new_tc/mips_prelude.sail b/mips_new_tc/mips_prelude.sail
index c026c85f..4c11a4b1 100644
--- a/mips_new_tc/mips_prelude.sail
+++ b/mips_new_tc/mips_prelude.sail
@@ -1,569 +1,408 @@
-(*========================================================================*)
-(* *)
-(* 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. *)
-(*========================================================================*)
-
-(* mips_prelude.sail: declarations of mips registers, and functions common
- to mips instructions (e.g. address translation) *)
-
-(* bit vectors have indices decreasing from left i.e. msb is highest index *)
+/*========================================================================*/
+/* */
+/* 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. */
+/*========================================================================*/
+
+/* mips_prelude.sail: declarations of mips registers, and functions common
+ to mips instructions (e.g. address translation) */
+
+/* bit vectors have indices decreasing from left i.e. msb is highest index */
default Order dec
-register (bit[64]) PC
-register (bit[64]) nextPC
-
-(* CP0 Registers *)
-
-typedef CauseReg = register bits [ 31 : 0 ] {
- 31 : BD; (* branch delay *)
- (*30 : Z0;*)
- 29 .. 28 : CE; (* for coprocessor enable exception *)
- (*27 .. 24 : Z1;*)
- 23 : IV; (* special interrupt vector not supported *)
- 22 : WP; (* watchpoint exception occurred *)
- (*21 .. 16 : Z2; *)
- 15 .. 8 : IP; (* interrupt pending bits *)
- (*7 : Z3;*)
- 6 .. 2 : ExcCode; (* code of last exception *)
- (*1 .. 0 : Z4;*)
+register PC : bits(64)
+register nextPC : bits(64)
+
+/* CP0 Registers */
+
+bitfield CauseReg : bits(32) = {
+ BD : 31, /* branch delay */
+ /*Z0 : 30,*/
+ CE : 29.. 28, /* for coprocessor enable exception */
+ /*Z1 : 27.. 24,*/
+ IV : 23, /* special interrupt vector not supported */
+ WP : 22, /* watchpoint exception occurred */
+ /*Z2 : 21.. 16, */
+ IP : 15.. 8, /* interrupt pending bits */
+ /*Z3 : 7,*/
+ ExcCode : 6.. 2, /* code of last exception */
+ /*Z4 : 1.. 0,*/
}
-typedef TLBEntryLoReg = register bits [63 : 0] {
- 63 : CapS;
- 62 : CapL;
- 29 .. 6 : PFN;
- 5 .. 3 : C;
- 2 : D;
- 1 : V;
- 0 : G;
+bitfield TLBEntryLoReg : bits(64) = {
+ CapS : 63,
+ CapL : 62,
+ PFN : 29.. 6,
+ C : 5.. 3,
+ D : 2,
+ V : 1,
+ G : 0,
}
-typedef TLBEntryHiReg = register bits [63 : 0] {
- 63 .. 62 : R;
- 39 .. 13 : VPN2;
- 7 .. 0 : ASID;
+bitfield TLBEntryHiReg : bits(64) = {
+ R : 63.. 62,
+ VPN2 : 39.. 13,
+ ASID : 7.. 0,
}
-typedef ContextReg = register bits [63 : 0] {
- 63 .. 23 : PTEBase;
- 22 .. 4 : BadVPN2;
- (*3 .. 0 : ZR;*)
+bitfield ContextReg : bits(64) = {
+ PTEBase : 63.. 23,
+ BadVPN2 : 22.. 4,
+ /*ZR : 3.. 0,*/
}
-typedef XContextReg = register bits [63 : 0] {
- 63 .. 33: PTEBase;
- 32 .. 31: R;
- 30 .. 4: BadVPN2;
+bitfield XContextReg : bits(64) = {
+ PTEBase : 63.. 33,
+ R : 32.. 31,
+ BadVPN2 : 30.. 4,
}
-let ([:64:]) TLBNumEntries = 64
-typedef TLBIndexT = (bit[6])
-let (TLBIndexT) TLBIndexMax = 0b111111
+let TLBNumEntries = 64
+type TLBIndexT = (bits(6))
+let TLBIndexMax : TLBIndexT = 0b111111
-val forall 'n. [:'n:] -> [:2**'n - 1:] effect pure MAX
+val MAX : forall 'n. atom('n) -> atom(2 ^ 'n - 1) effect pure
function MAX(n) = pow2(n) - 1
-let MAX_U64 = MAX(64) (*unsigned(0xffffffffffffffff)*)
-let MAX_VA = MAX(40) (*unsigned(0xffffffffff)*)
-let MAX_PA = MAX(36) (*unsigned(0xfffffffff)*)
-
-typedef TLBEntry = register bits [116 : 0] {
- 116 .. 101: pagemask;
- 100 .. 99 : r ;
- 98 .. 72 : vpn2 ;
- 71 .. 64 : asid ;
- 63 : g ;
- 62 : valid ;
- 61 : caps1 ;
- 60 : capl1 ;
- 59 .. 36 : pfn1 ;
- 35 .. 33 : c1 ;
- 32 : d1 ;
- 31 : v1 ;
- 30 : caps0 ;
- 29 : capl0 ;
- 28 .. 5 : pfn0 ;
- 4 .. 2 : c0 ;
- 1 : d0 ;
- 0 : v0 ;
+let MAX_U64 = MAX(64) /*unsigned(0xffffffffffffffff)*/
+let MAX_VA = MAX(40) /*unsigned(0xffffffffff)*/
+let MAX_PA = MAX(36) /*unsigned(0xfffffffff)*/
+
+bitfield TLBEntry : bits(117) = {
+ pagemask : 116.. 101,
+ r : 100.. 99,
+ vpn2 : 98.. 72,
+ asid : 71.. 64,
+ g : 63,
+ valid : 62,
+ caps1 : 61,
+ capl1 : 60,
+ pfn1 : 59.. 36,
+ c1 : 35.. 33,
+ d1 : 32,
+ v1 : 31,
+ caps0 : 30,
+ capl0 : 29,
+ pfn0 : 28.. 5,
+ c0 : 4.. 2,
+ d0 : 1,
+ v0 : 0,
}
-register (bit[1]) TLBProbe
-register (TLBIndexT) TLBIndex
-register (TLBIndexT) TLBRandom
-register (TLBEntryLoReg) TLBEntryLo0
-register (TLBEntryLoReg) TLBEntryLo1
-register (ContextReg) TLBContext
-register (bit[16]) TLBPageMask
-register (TLBIndexT) TLBWired
-register (TLBEntryHiReg) TLBEntryHi
-register (XContextReg) TLBXContext
-
-register (TLBEntry) TLBEntry00
-register (TLBEntry) TLBEntry01
-register (TLBEntry) TLBEntry02
-register (TLBEntry) TLBEntry03
-register (TLBEntry) TLBEntry04
-register (TLBEntry) TLBEntry05
-register (TLBEntry) TLBEntry06
-register (TLBEntry) TLBEntry07
-register (TLBEntry) TLBEntry08
-register (TLBEntry) TLBEntry09
-register (TLBEntry) TLBEntry10
-register (TLBEntry) TLBEntry11
-register (TLBEntry) TLBEntry12
-register (TLBEntry) TLBEntry13
-register (TLBEntry) TLBEntry14
-register (TLBEntry) TLBEntry15
-register (TLBEntry) TLBEntry16
-register (TLBEntry) TLBEntry17
-register (TLBEntry) TLBEntry18
-register (TLBEntry) TLBEntry19
-register (TLBEntry) TLBEntry20
-register (TLBEntry) TLBEntry21
-register (TLBEntry) TLBEntry22
-register (TLBEntry) TLBEntry23
-register (TLBEntry) TLBEntry24
-register (TLBEntry) TLBEntry25
-register (TLBEntry) TLBEntry26
-register (TLBEntry) TLBEntry27
-register (TLBEntry) TLBEntry28
-register (TLBEntry) TLBEntry29
-register (TLBEntry) TLBEntry30
-register (TLBEntry) TLBEntry31
-register (TLBEntry) TLBEntry32
-register (TLBEntry) TLBEntry33
-register (TLBEntry) TLBEntry34
-register (TLBEntry) TLBEntry35
-register (TLBEntry) TLBEntry36
-register (TLBEntry) TLBEntry37
-register (TLBEntry) TLBEntry38
-register (TLBEntry) TLBEntry39
-register (TLBEntry) TLBEntry40
-register (TLBEntry) TLBEntry41
-register (TLBEntry) TLBEntry42
-register (TLBEntry) TLBEntry43
-register (TLBEntry) TLBEntry44
-register (TLBEntry) TLBEntry45
-register (TLBEntry) TLBEntry46
-register (TLBEntry) TLBEntry47
-register (TLBEntry) TLBEntry48
-register (TLBEntry) TLBEntry49
-register (TLBEntry) TLBEntry50
-register (TLBEntry) TLBEntry51
-register (TLBEntry) TLBEntry52
-register (TLBEntry) TLBEntry53
-register (TLBEntry) TLBEntry54
-register (TLBEntry) TLBEntry55
-register (TLBEntry) TLBEntry56
-register (TLBEntry) TLBEntry57
-register (TLBEntry) TLBEntry58
-register (TLBEntry) TLBEntry59
-register (TLBEntry) TLBEntry60
-register (TLBEntry) TLBEntry61
-register (TLBEntry) TLBEntry62
-register (TLBEntry) TLBEntry63
-
-let (vector <0, 64, inc, (register<TLBEntry>)>) TLBEntries = [
-TLBEntry00,
-TLBEntry01,
-TLBEntry02,
-TLBEntry03,
-TLBEntry04,
-TLBEntry05,
-TLBEntry06,
-TLBEntry07,
-TLBEntry08,
-TLBEntry09,
-TLBEntry10,
-TLBEntry11,
-TLBEntry12,
-TLBEntry13,
-TLBEntry14,
-TLBEntry15,
-TLBEntry16,
-TLBEntry17,
-TLBEntry18,
-TLBEntry19,
-TLBEntry20,
-TLBEntry21,
-TLBEntry22,
-TLBEntry23,
-TLBEntry24,
-TLBEntry25,
-TLBEntry26,
-TLBEntry27,
-TLBEntry28,
-TLBEntry29,
-TLBEntry30,
-TLBEntry31,
-TLBEntry32,
-TLBEntry33,
-TLBEntry34,
-TLBEntry35,
-TLBEntry36,
-TLBEntry37,
-TLBEntry38,
-TLBEntry39,
-TLBEntry40,
-TLBEntry41,
-TLBEntry42,
-TLBEntry43,
-TLBEntry44,
-TLBEntry45,
-TLBEntry46,
-TLBEntry47,
-TLBEntry48,
-TLBEntry49,
-TLBEntry50,
-TLBEntry51,
-TLBEntry52,
-TLBEntry53,
-TLBEntry54,
-TLBEntry55,
-TLBEntry56,
-TLBEntry57,
-TLBEntry58,
-TLBEntry59,
-TLBEntry60,
-TLBEntry61,
-TLBEntry62,
-TLBEntry63
-]
-
-register (bit[32]) CP0Compare
-register (CauseReg) CP0Cause
-register (bit[64]) CP0EPC
-register (bit[64]) CP0ErrorEPC
-register (bit[1]) CP0LLBit
-register (bit[64]) CP0LLAddr
-register (bit[64]) CP0BadVAddr
-register (bit[32]) CP0Count
-register (bit[32]) CP0HWREna
-register (bit[64]) CP0UserLocal
-
-typedef StatusReg = register bits [31:0] {
- 31 .. 28 : CU; (* co-processor enable bits *)
- (* RP/FR/RE/MX/PX not implemented *)
- 22 : BEV; (* use boot exception vectors (initialised to one) *)
- (* TS/SR/NMI not implemented *)
- 15 .. 8 : IM; (* Interrupt mask *)
- 7 : KX; (* kernel 64-bit enable *)
- 6 : SX; (* supervisor 64-bit enable *)
- 5 : UX; (* user 64-bit enable *)
- 4 .. 3 : KSU; (* Processor mode *)
- 2 : ERL; (* error level (should be initialised to one, but BERI is different) *)
- 1 : EXL; (* exception level *)
- 0 : IE; (* interrupt enable *)
+register TLBProbe : bits(1)
+register TLBIndex : TLBIndexT
+register TLBRandom : TLBIndexT
+register TLBEntryLo0 : TLBEntryLoReg
+register TLBEntryLo1 : TLBEntryLoReg
+register TLBContext : ContextReg
+register TLBPageMask : bits(16)
+register TLBWired : TLBIndexT
+register TLBEntryHi : TLBEntryHiReg
+register TLBXContext : XContextReg
+
+register TLBEntries : vector(64, dec, TLBEntry)
+
+register CP0Compare : bits(32)
+register CP0Cause : CauseReg
+register CP0EPC : bits(64)
+register CP0ErrorEPC : bits(64)
+register CP0LLBit : bits(1)
+register CP0LLAddr : bits(64)
+register CP0BadVAddr : bits(64)
+register CP0Count : bits(32)
+register CP0HWREna : bits(32)
+register CP0UserLocal : bits(64)
+
+bitfield StatusReg : bits(32) = {
+ CU : 31.. 28, /* co-processor enable bits */
+ /* RP/FR/RE/MX/PX not implemented */
+ BEV : 22, /* use boot exception vectors (initialised to one) */
+ /* TS/SR/NMI not implemented */
+ IM : 15.. 8, /* Interrupt mask */
+ KX : 7, /* kernel 64-bit enable */
+ SX : 6, /* supervisor 64-bit enable */
+ UX : 5, /* user 64-bit enable */
+ KSU : 4.. 3, /* Processor mode */
+ ERL : 2, /* error level (should be initialised to one, but BERI is different) */
+ EXL : 1, /* exception level */
+ IE : 0, /* interrupt enable */
}
-register (StatusReg) CP0Status
-
-(* Implementation registers -- not ISA defined *)
-register (bit[1]) branchPending (* Set by branch instructions to implement branch delay *)
-register (bit[1]) inBranchDelay (* Needs to be set by outside world when in branch delay slot *)
-register (bit[64]) delayedPC (* Set by branch instructions to implement branch delay *)
-
-(* General purpose registers *)
-
-register (bit[64]) GPR00 (* should never be read or written *)
-register (bit[64]) GPR01
-register (bit[64]) GPR02
-register (bit[64]) GPR03
-register (bit[64]) GPR04
-register (bit[64]) GPR05
-register (bit[64]) GPR06
-register (bit[64]) GPR07
-register (bit[64]) GPR08
-register (bit[64]) GPR09
-register (bit[64]) GPR10
-register (bit[64]) GPR11
-register (bit[64]) GPR12
-register (bit[64]) GPR13
-register (bit[64]) GPR14
-register (bit[64]) GPR15
-register (bit[64]) GPR16
-register (bit[64]) GPR17
-register (bit[64]) GPR18
-register (bit[64]) GPR19
-register (bit[64]) GPR20
-register (bit[64]) GPR21
-register (bit[64]) GPR22
-register (bit[64]) GPR23
-register (bit[64]) GPR24
-register (bit[64]) GPR25
-register (bit[64]) GPR26
-register (bit[64]) GPR27
-register (bit[64]) GPR28
-register (bit[64]) GPR29
-register (bit[64]) GPR30
-register (bit[64]) GPR31
-
-(* Special registers For MUL/DIV *)
-register (bit[64]) HI
-register (bit[64]) LO
-
-let (vector <0, 32, inc, (register<(bit[64])>) >) GPR =
- [ GPR00, GPR01, GPR02, GPR03, GPR04, GPR05, GPR06, GPR07, GPR08, GPR09, GPR10,
- GPR11, GPR12, GPR13, GPR14, GPR15, GPR16, GPR17, GPR18, GPR19, GPR20,
- GPR21, GPR22, GPR23, GPR24, GPR25, GPR26, GPR27, GPR28, GPR29, GPR30, GPR31
- ]
-
-(* JTAG Uart registers *)
-
-register (bit[8]) UART_WDATA
-register (bit[1]) UART_WRITTEN
-register (bit[8]) UART_RDATA
-register (bit[1]) UART_RVALID
-
-(* Check whether a given 64-bit vector is a properly sign extended 32-bit word *)
-val bit[64] -> bool effect pure NotWordVal
+register CP0Status : StatusReg
+
+/* Implementation registers -- not ISA defined */
+register branchPending : bits(1) /* Set by branch instructions to implement branch delay */
+register inBranchDelay : bits(1) /* Needs to be set by outside world when in branch delay slot */
+register delayedPC : bits(64) /* Set by branch instructions to implement branch delay */
+
+/* General purpose registers */
+
+
+/* Special registers For MUL/DIV */
+register HI : bits(64)
+register LO : bits(64)
+
+register GPR : vector(32, dec, bits(64))
+
+/* JTAG Uart registers */
+
+register UART_WDATA : bits(8)
+register UART_WRITTEN : bits(1)
+register UART_RDATA : bits(8)
+register UART_RVALID : bits(1)
+
+/* Check whether a given 64-bit vector is a properly sign extended 32-bit word */
+val NotWordVal : bits(64) -> bool effect pure
function bool NotWordVal (word) =
(word[31] ^^ 32) != word[63..32]
-(* Read numbered GP reg. (r0 is always zero) *)
-val bit[5] -> bit[64] effect {rreg} rGPR
-function bit[64] rGPR idx = {
+/* Read numbered GP reg. (r0 is always zero) */
+val rGPR : bits(5) -> bits(64) effect {rreg}
+function rGPR idx = {
if idx == 0 then 0 else GPR[idx]
}
-(* Write numbered GP reg. (writes to r0 ignored) *)
-val (bit[5], bit[64]) -> unit effect {wreg} wGPR
-function unit wGPR (idx, v) = {
- if idx == 0 then () else GPR[idx] := v
+/* Write numbered GP reg. (writes to r0 ignored) */
+val wGPR : (bits(5), bits(64)) -> unit effect {wreg}
+function wGPR (idx, v) = {
+ if idx == 0 then () else GPR[idx] = v
}
-val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr
-val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr_reserve
-val extern unit -> unit effect { barr } MEM_sync
+val MEMr : forall 'n. ( bits(64) , atom('n) ) -> (bits(8 * 'n)) effect { rmem }
+val MEMr_reserve : forall 'n. ( bits(64) , atom('n) ) -> (bits(8 * 'n)) effect { rmem }
+val MEM_sync : unit -> unit effect { barr }
-val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea
-val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_conditional
-val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval
-val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> bool effect { wmv } MEMval_conditional
+val MEMea : forall 'n. ( bits(64) , atom('n)) -> unit effect { eamem }
+val MEMea_conditional : forall 'n. ( bits(64) , atom('n)) -> unit effect { eamem }
+val MEMval : forall 'n. ( bits(64) , atom('n), bits(8*'n)) -> unit effect { wmv }
+val MEMval_conditional : forall 'n. ( bits(64) , atom('n), bits(8*'n)) -> bool effect { wmv }
-typedef Exception = enumerate
+enum Exception =
{
- Int; TLBMod; TLBL; TLBS; AdEL; AdES; Sys; Bp; ResI; CpU; Ov; Tr; C2E; C2Trap;
- XTLBRefillL; XTLBRefillS; XTLBInvL; XTLBInvS; MCheck
+ Interrupt, TLBMod, TLBL, TLBS, AdEL, AdES, Sys, Bp, ResI, CpU, Ov, Tr, C2E, C2Trap,
+ XTLBRefillL, XTLBRefillS, XTLBInvL, XTLBInvS, MCheck
}
-(* Return the ISA defined code for an exception condition *)
-function (bit[5]) ExceptionCode ((Exception) ex) =
- switch (ex)
+/* Return the ISA defined code for an exception condition */
+function ExceptionCode (ex) : Exception -> bits(5)=
+ match ex
{
- case Int -> mask(0x00) (* Interrupt *)
- case TLBMod -> mask(0x01) (* TLB modification exception *)
- case TLBL -> mask(0x02) (* TLB exception (load or fetch) *)
- case TLBS -> mask(0x03) (* TLB exception (store) *)
- case AdEL -> mask(0x04) (* Address error (load or fetch) *)
- case AdES -> mask(0x05) (* Address error (store) *)
- case Sys -> mask(0x08) (* Syscall *)
- case Bp -> mask(0x09) (* Breakpoint *)
- case ResI -> mask(0x0a) (* Reserved instruction *)
- case CpU -> mask(0x0b) (* Coprocessor Unusable *)
- case Ov -> mask(0x0c) (* Arithmetic overflow *)
- case Tr -> mask(0x0d) (* Trap *)
- case C2E -> mask(0x12) (* C2E coprocessor 2 exception *)
- case C2Trap -> mask(0x12) (* C2Trap maps to same exception code, different vector *)
- case XTLBRefillL -> mask(0x02)
- case XTLBRefillS -> mask(0x03)
- case XTLBInvL -> mask(0x02)
- case XTLBInvS -> mask(0x03)
- case MCheck -> mask(0x18)
+ Interrupt => mask(0x00), /* Interrupt */
+ TLBMod => mask(0x01), /* TLB modification exception */
+ TLBL => mask(0x02), /* TLB exception (load or fetch) */
+ TLBS => mask(0x03), /* TLB exception (store) */
+ AdEL => mask(0x04), /* Address error (load or fetch) */
+ AdES => mask(0x05), /* Address error (store) */
+ Sys => mask(0x08), /* Syscall */
+ Bp => mask(0x09), /* Breakpoint */
+ ResI => mask(0x0a), /* Reserved instruction */
+ CpU => mask(0x0b), /* Coprocessor Unusable */
+ Ov => mask(0x0c), /* Arithmetic overflow */
+ Tr => mask(0x0d), /* Trap */
+ C2E => mask(0x12), /* C2E coprocessor 2 exception */
+ C2Trap => mask(0x12), /* C2Trap maps to same exception code, different vector */
+ XTLBRefillL => mask(0x02),
+ XTLBRefillS => mask(0x03),
+ XTLBInvL => mask(0x02),
+ XTLBInvS => mask(0x03),
+ MCheck => mask(0x18)
}
-
-function forall Type 'o. 'o SignalExceptionMIPS ((Exception) ex, (bit[64]) kccBase) =
+val SignalExceptionMIPS : forall ('o : Type) . (Exception, bits(64)) -> 'o effect {escape}
+function SignalExceptionMIPS (ex, kccBase) =
{
- (* Only update EPC and BD if not already in EXL mode *)
+ /* Only update EPC and BD if not already in EXL mode */
if (~ (CP0Status.EXL)) then
{
if (inBranchDelay[0]) then
{
- CP0EPC := PC - 4;
- CP0Cause.BD := 1;
+ CP0EPC = PC - 4;
+ CP0Cause.BD = 1;
}
else
{
- CP0EPC := PC;
- CP0Cause.BD := 0;
+ CP0EPC = PC;
+ CP0Cause.BD = 0;
}
};
- (* choose an exception vector to branch to. Some are not supported
- e.g. Reset *)
- vectorOffset :=
+ /* choose an exception vector to branch to. Some are not supported
+ e.g. Reset */
+ vectorOffset =
if (CP0Status.EXL) then
- 0x180 (* Always use common vector if in exception mode already *)
+ 0x180 /* Always use common vector if in exception mode already */
else if ((ex == XTLBRefillL) | (ex == XTLBRefillS)) then
0x080
else if (ex == C2Trap) then
- 0x280 (* Special vector for CHERI traps *)
+ 0x280 /* Special vector for CHERI traps */
else
- 0x180; (* Common vector *)
- (bit[64]) vectorBase := if CP0Status.BEV then
+ 0x180; /* Common vector */
+ vectorBase : bits(64) = if CP0Status.BEV then
0xFFFFFFFFBFC00200
else
0xFFFFFFFF80000000;
- (* On CHERI we have to subtract KCC.base so that we end up at the
- right absolute vector address after indirecting via new PCC *)
- nextPC := ((bit[64])(vectorBase + (bit[64]) (EXTS(vectorOffset)))) - kccBase;
- CP0Cause.ExcCode := ExceptionCode(ex);
- CP0Status.EXL := 1;
- exit ();
+ /* On CHERI we have to subtract KCC.base so that we end up at the
+ right absolute vector address after indirecting via new PCC */
+ nextPC = vectorBase + EXTS(vectorOffset) - kccBase;
+ CP0Cause.ExcCode = ExceptionCode(ex);
+ CP0Status.EXL = 1;
+ exit (());
}
-val forall Type 'o . Exception -> 'o effect {escape, rreg, wreg} SignalException
+val SignalException : forall ('o : Type) . Exception -> 'o effect {escape, rreg, wreg}
-function forall Type 'o. 'o SignalExceptionBadAddr((Exception) ex, (bit[64]) badAddr) =
+val SignalExceptionBadAddr : forall ('o : Type) . (Exception, bits(64)) -> 'o effect {escape, rreg, wreg}
+function SignalExceptionBadAddr(ex, badAddr) =
{
- CP0BadVAddr := badAddr;
+ CP0BadVAddr = badAddr;
SignalException(ex);
}
-function forall Type 'o. 'o SignalExceptionTLB((Exception) ex, (bit[64]) badAddr) = {
- CP0BadVAddr := badAddr;
- (TLBContext.BadVPN2) := (badAddr[31..13]);
- (TLBXContext.BadVPN2):= (badAddr[39..13]);
- (TLBXContext.R) := (badAddr[63..62]);
- (TLBEntryHi.R) := (badAddr[63..62]);
- (TLBEntryHi.VPN2) := (badAddr[39..13]);
+val SignalExceptionTLB : forall ('o : Type) . (Exception, bits(64)) -> 'o effect {escape, rreg, wreg}
+function SignalExceptionTLB(ex, badAddr) = {
+ CP0BadVAddr = badAddr;
+ (TLBContext.BadVPN2) = (badAddr[31..13]);
+ (TLBXContext.BadVPN2)= (badAddr[39..13]);
+ (TLBXContext.R) = (badAddr[63..62]);
+ (TLBEntryHi.R) = (badAddr[63..62]);
+ (TLBEntryHi.VPN2) = (badAddr[39..13]);
SignalException(ex);
}
-typedef MemAccessType = enumerate {Instruction; LoadData; StoreData}
-typedef AccessLevel = enumerate {User; Supervisor; Kernel}
+enum MemAccessType = {Instruction, LoadData, StoreData}
+enum AccessLevel = {User, Supervisor, Kernel}
-function AccessLevel getAccessLevel() =
+function getAccessLevel() : unit -> AccessLevel=
if ((CP0Status.EXL) | (CP0Status.ERL)) then
Kernel
- else switch (bit[2]) (CP0Status.KSU)
+ else match CP0Status.KSU
{
- case 0b00 -> Kernel
- case 0b01 -> Supervisor
- case 0b10 -> User
- case _ -> User (* behaviour undefined, assume user *)
+ 0b00 => Kernel,
+ 0b01 => Supervisor,
+ 0b10 => User,
+ _ => User /* behaviour undefined, assume user */
}
-function unit checkCP0Access () =
+function checkCP0Access () =
{
let accessLevel = getAccessLevel() in
- if ((accessLevel != Kernel) & (~(CP0Status[28] (*CU0*)))) then
+ if ((accessLevel != Kernel) & (~(CP0Status[28] /*CU0*/))) then
{
- (CP0Cause.CE) := 0b00;
+ (CP0Cause.CE) = 0b00;
SignalException(CpU);
}
}
-function unit incrementCP0Count() = {
- TLBRandom := (if (TLBRandom == TLBWired)
+function incrementCP0Count() = {
+ TLBRandom = (if (TLBRandom == TLBWired)
then (TLBIndexMax) else (TLBRandom - 1));
- CP0Count := (CP0Count + 1);
+ CP0Count = (CP0Count + 1);
if (CP0Count == CP0Compare) then {
- (CP0Cause[15]) := bitone; (* XXX indexing IP field here doesn't seem to work *)
+ (CP0Cause[15]) = bitone; /* XXX indexing IP field here doesn't seem to work */
};
- let ims = (bit[8]) (CP0Status.IM) in
- let ips = (bit[8]) (CP0Cause.IP) in
+ let ims = CP0Status.IM in
+ let ips = CP0Cause.IP in
let ie = CP0Status.IE in
let exl = CP0Status.EXL in
let erl = CP0Status.ERL in
if ((~(exl)) & (~(erl)) & ie & ((ips & ims) != 0x00)) then
- SignalException(Int);
+ SignalException(Interrupt);
}
-typedef regno = bit[5] (* a register number *)
-typedef imm16 = bit[16] (* 16-bit immediate *)
-(* a commonly used instruction format with three register operands *)
-typedef regregreg = (regno, regno, regno)
-(* a commonly used instruction format with two register operands and 16-bit immediate *)
-typedef regregimm16 = (regno, regno, imm16)
-
-typedef decode_failure = enumerate {
- no_matching_pattern;
- unsupported_instruction;
- illegal_instruction;
- internal_error
+type regno = bits(5) /* a register number */
+type imm16 = bits(16) /* 16-bit immediate */
+/* a commonly used instruction format with three register operands */
+type regregreg = (regno, regno, regno)
+/* a commonly used instruction format with two register operands and 16-bit immediate */
+type regregimm16 = (regno, regno, imm16)
+
+enum decode_failure = {
+ no_matching_pattern,
+ unsupported_instruction,
+ illegal_instruction,
+ internal_error
}
-(* Used by branch and trap instructions *)
-typedef Comparison = enumerate {
- EQ; (* equal *)
- NE; (* not equal *)
- GE; (* signed greater than or equal *)
- GEU;(* unsigned greater than or equal *)
- GT; (* signed strictly greater than *)
- LE; (* signed less than or equal *)
- LT; (* signed strictly less than *)
- LTU;(* unsigned less than or qual *)
+/* Used by branch and trap instructions */
+enum Comparison = {
+ EQ, /* equal */
+ NE, /* not equal */
+ GE, /* signed greater than or equal */
+ GEU,/* unsigned greater than or equal */
+ GT, /* signed strictly greater than */
+ LE, /* signed less than or equal */
+ LT, /* signed strictly less than */
+ LTU /* unsigned less than or qual */
}
-function bool compare ((Comparison)cmp, (bit[64]) valA, (bit[64]) valB) =
- (* sail comparisons are signed so extend to 65 bits for unsigned comparisons *)
+
+val compare : (Comparison, bits(64), bits(64)) -> bool
+function compare (cmp, valA, valB) =
+ /* sail comparisons are signed so extend to 65 bits for unsigned comparisons */
let valA65 = (0b0 : valA) in
let valB65 = (0b0 : valB) in
- switch(cmp) {
- case EQ -> valA == valB
- case NE -> valA != valB
- case GE -> valA >= valB
- case GEU -> valA65 >= valB65
- case GT -> valA > valB
- case LE -> valA <= valB
- case LT -> valA < valB
- case LTU -> valA65 < valB65
+ match cmp {
+ EQ => valA == valB,
+ NE => valA != valB,
+ GE => valA >= valB,
+ GEU => valA65 >= valB65,
+ GT => valA > valB,
+ LE => valA <= valB,
+ LT => valA < valB,
+ LTU => valA65 < valB65
}
-typedef WordType = enumerate { B; H; W; D}
-
-function [|1:8|] wordWidthBytes((WordType) w) =
- switch(w) {
- case B -> 1
- case H -> 2
- case W -> 4
- case D -> 8
+enum WordType = { B, H, W, D}
+
+val wordWidthBytes : Wordwidthbytes -> range(1, 8)
+function wordWidthBytes(w) =
+ match w {
+ B => 1,
+ H => 2,
+ W => 4,
+ D => 8
}
-(* This function checks that memory accesses are naturally aligned
+/* This function checks that memory accesses are naturally aligned
-- it is disabled in favour of BERI specific behaviour below.
function bool isAddressAligned(addr, (WordType) wordType) =
- switch (wordType) {
- case B -> true
- case H -> (addr[0] == 0)
- case W -> (addr[1..0] == 0b00)
- case D -> (addr[2..0] == 0b000)
+ match wordType {
+ B => true
+ H => (addr[0] == 0)
+ W => (addr[1..0] == 0b00)
+ D => (addr[2..0] == 0b000)
}
-*)
+*/
-(* BERI relaxes the natural alignment requirement for loads and stores
+/* BERI relaxes the natural alignment requirement for loads and stores
but still throws an exception if an access spans a cache line
boundary. Here we assume this is 32 bytes so that we don't have to
worry about clearing multiple tags when an access spans more than
@@ -571,43 +410,46 @@ function bool isAddressAligned(addr, (WordType) wordType) =
aligned. Provided this is a factor of smallest supported page size
(4k) we don't need to worry about accesses spanning page boundaries
either.
-*)
+*/
let alignment_width = 16
-function (bool) isAddressAligned ((bit[64]) addr, (WordType) wordType) =
+val isAddressAligned : (bits(64), WordType) -> bool
+function isAddressAligned (addr, wordType) =
let a = unsigned(addr) in
- ((a quot alignment_width) == (a + wordWidthBytes(wordType) - 1) quot alignment_width)
+ quot(a, alignment_width) == quot(a + wordWidthBytes(wordType) - 1, alignment_width)
-(*val forall Nat 'W, 'W >= 1. ([:'W:], bit[8 * 'W]) -> bit[8 * 'W] effect pure reverse_endianness'
+/*val reverse_endianness : forall Nat 'W, 'W >= 1. ([:'W:], bits(8 * 'W)) -> bits(8 * 'W) effect pure'
-function rec forall Nat 'W, 'W >= 1. bit[8 * 'W] reverse_endianness' (w, value) =
+function rec forall Nat 'W, 'W >= 1. bits(8 * 'W) reverse_endianness' (w, value) =
{
- ([:8 * 'W:]) width := length(value);
+ ([:8 * 'W:]) width = length(value);
if width <= 8
then value
else value[7..0] : reverse_endianness'(w - 1, value[(width - 1) .. 8])
}
-val forall Nat 'W, 'W >= 1. bit[8 * 'W] -> bit[8 * 'W] effect pure reverse_endianness
+val reverse_endianness : forall Nat 'W, 'W >= 1. bits(8 * 'W) -> bits(8 * 'W) effect pure
-function rec forall Nat 'W, 'W >= 1. bit[8 * 'W] reverse_endianness ((bit[8 * 'W]) value) =
+function rec forall Nat 'W, 'W >= 1. bits(8 * 'W) reverse_endianness ((bits(8 * 'W)) value) =
{
reverse_endianness'(sizeof 'W, value)
-}*)
+}*/
-function forall Nat 'n, 1 <= 'n, 'n <= 8. (bit[8 * 'n]) effect { rmem } MEMr_wrapper ((bit[64]) addr, ([:'n:]) size) =
+val MEMr_wrapper : forall 'n, 1 <= 'n <=8 . (bits(64), atom('n)) -> bits(8*n) effect {rmem}
+function MEMr_wrapper (addr, size) = reverse_endianness(MEMr (addr, size)) /* TODO
if (addr == 0x000000007f000000) then
{
- let rvalid = (bit[1]) UART_RVALID in
- let rdata = (bit[8 * 'n]) (mask(0x00000000 : UART_RDATA : rvalid : 0b0000000 : 0x0000)) in
+ let rvalid = UART_RVALID in
+ let rdata = (bits(8 * 'n)) (mask(0x00000000 : UART_RDATA : rvalid : 0b0000000 : 0x0000)) in
{
- UART_RVALID := [bitzero];
+ UART_RVALID = [bitzero];
rdata
}
}
else if (addr == 0x000000007f000004) then
- mask(0x000000000004ffff) (* Always plenty of write space available and jtag activity *)
+ mask(0x000000000004ffff) /* Always plenty of write space available and jtag activity */
else
- reverse_endianness(MEMr(addr, size)) (* MEMr assumes little endian *)
+ reverse_endianness(MEMr(addr, size)) /* MEMr assumes little endian */ */
-function forall Nat 'n, 'n >= 1. (bit[8 * 'n]) effect { rmem } MEMr_reserve_wrapper ((bit[64]) addr , ([:'n:]) size) =
+val MEMr_reserve_wrapper : forall 'n. ( bits(64) , atom('n) ) -> (bits(8 * 'n)) effect { rmem }
+function MEMr_reserve_wrapper (addr , size) =
reverse_endianness(MEMr_reserve(addr, size))
diff --git a/mips_new_tc/mips_regfp.sail b/mips_new_tc/mips_regfp.sail
index 4980aa2c..4bf96022 100644
--- a/mips_new_tc/mips_regfp.sail
+++ b/mips_new_tc/mips_regfp.sail
@@ -1,38 +1,38 @@
-(*========================================================================*)
-(* *)
-(* 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. *)
-(*========================================================================*)
+/*========================================================================*/
+/* */
+/* 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. */
+/*========================================================================*/
-let (vector <0, 32, inc, string >) GPRs =
+let GPRs : vector <0, 32, inc, string > =
[ "GPR00", "GPR01", "GPR02", "GPR03", "GPR04", "GPR05", "GPR06", "GPR07", "GPR08", "GPR09", "GPR10",
"GPR11", "GPR12", "GPR13", "GPR14", "GPR15", "GPR16", "GPR17", "GPR18", "GPR19", "GPR20",
"GPR21", "GPR22", "GPR23", "GPR24", "GPR25", "GPR26", "GPR27", "GPR28", "GPR29", "GPR30", "GPR31"
@@ -42,404 +42,404 @@ let CIA_fp = RFull("CIA")
let NIA_fp = RFull("NIA")
function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis ((ast) instr) = {
- (regfps) iR := [|| ||];
- (regfps) oR := [|| ||];
- (regfps) aR := [|| ||];
- (instruction_kind) ik := IK_simple;
- (niafps) Nias := [|| ||];
- (diafp) Dia := DIAFP_none;
+ (regfps) iR = [|| ||];
+ (regfps) oR = [|| ||];
+ (regfps) aR = [|| ||];
+ (instruction_kind) ik = IK_simple;
+ (niafps) Nias = [|| ||];
+ (diafp) Dia = DIAFP_none;
switch instr {
- case (DADDIU (rs, rt, imm)) -> {
- if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
- if rt == 0 then () else oR := RFull(GPRs[rt]) :: oR;
- }
- case (DADDU (rs, rt, rd)) -> {
- if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
- if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR;
- if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR;
- }
- case (DADDI (rs, rt, imm)) -> {
- if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
- if rt == 0 then () else oR := RFull(GPRs[rt]) :: oR;
- }
- case (DADD (rs, rt, rd)) -> {
- if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
- if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR;
- }
- case (ADD(rs, rt, rd)) -> {
- if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
- if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR;
- if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR;
- }
- case (ADDI(rs, rt, imm)) -> {
- if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
- if rt == 0 then () else oR := RFull(GPRs[rt]) :: oR;
- }
- case (ADDU(rs, rt, rd)) -> {
- if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
- if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR;
- if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR;
- }
- case (ADDIU(rs, rt, imm)) -> {
- if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
- if rt == 0 then () else oR := RFull(GPRs[rt]) :: oR;
- }
- case (DSUBU (rs, rt, rd)) -> {
- if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
- if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR;
- if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR;
- }
- case (DSUB (rs, rt, rd)) -> {
- if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
- if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR;
- if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR;
- }
- case (SUB(rs, rt, rd)) -> {
- if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
- if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR;
- if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR;
- }
- case (SUBU(rs, rt, rd)) -> {
- if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
- if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR;
- if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR;
- }
- case (AND (rs, rt, rd)) -> {
- if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
- if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR;
- if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR;
- }
- case (ANDI (rs, rt, imm)) -> {
- if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
- if rt == 0 then () else oR := RFull(GPRs[rt]) :: oR;
- }
- case (OR (rs, rt, rd)) -> {
- if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
- if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR;
- if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR;
- }
- case (ORI (rs, rt, imm)) -> {
- if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
- if rt == 0 then () else oR := RFull(GPRs[rt]) :: oR;
- }
- case (NOR (rs, rt, rd)) -> {
- if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
- if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR;
- if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR;
- }
- case (XOR (rs, rt, rd)) -> {
- if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
- if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR;
- if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR;
- }
- case (XORI (rs, rt, imm)) -> {
- if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
- if rt == 0 then () else oR := RFull(GPRs[rt]) :: oR;
- }
- case (LUI (rt, imm)) -> {
- if rt == 0 then () else oR := RFull(GPRs[rt]) :: oR;
- }
- case (DSLL (rt, rd, sa)) -> {
- if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR;
- if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR;
- }
- case (DSLL32 (rt, rd, sa)) -> {
- if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR;
- if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR;
- }
- case (DSLLV (rs, rt, rd)) -> {
- if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
- if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR;
- if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR;
- }
- case (DSRA (rt, rd, sa)) -> {
- if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR;
- if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR;
- }
- case (DSRA32 (rt, rd, sa)) -> {
- if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR;
- if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR;
- }
- case (DSRAV (rs, rt, rd)) -> {
- if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
- if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR;
- if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR;
- }
- case (DSRL (rt, rd, sa)) -> {
- if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR;
- if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR;
- }
- case (DSRL32 (rt, rd, sa)) -> {
- if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR;
- if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR;
- }
- case (DSRLV (rs, rt, rd)) -> {
- if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
- if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR;
- if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR;
- }
- case (SLL(rt, rd, sa)) -> {
- if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR;
- if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR;
- }
- case (SLLV(rs, rt, rd)) -> {
- if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
- if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR;
- if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR;
- }
- case (SRA(rt, rd, sa)) -> {
- if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR;
- if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR;
- }
- case (SRAV(rs, rt, rd)) -> {
- if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
- if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR;
- if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR;
- }
- case (SRL(rt, rd, sa)) -> {
- if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR;
- if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR;
- }
- case (SRLV(rs, rt, rd)) -> {
- if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
- if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR;
- if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR;
- }
- case (SLT(rs, rt, rd)) -> {
- if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
- if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR;
- if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR;
- }
- case (SLTI(rs, rt, imm)) -> {
- if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
- if rt == 0 then () else oR := RFull(GPRs[rt]) :: oR;
- }
- case (SLTU(rs, rt, rd)) -> {
- if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
- if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR;
- if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR;
- }
- case (SLTIU(rs, rt, imm)) -> {
- if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
- if rt == 0 then () else oR := RFull(GPRs[rt]) :: oR;
- }
- case (MOVN(rs, rt, rd)) -> {
- (* XXX don't always write rd *)
- if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
- if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR;
- if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR;
- }
- case (MOVZ(rs, rt, rd)) -> {
- (* XXX don't always write rd *)
- if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
- if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR;
- if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR;
- }
- case (MFHI(rd)) -> {
- iR := RFull("HI") :: iR;
- if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR;
- }
- case (MFLO(rd)) -> {
- iR := RFull("LO") :: iR;
- if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR;
- }
- case (MTHI(rs)) -> {
- oR := RFull("HI") :: oR;
- if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
- }
- case (MTLO(rs)) -> {
- oR := RFull("LO") :: oR;
- if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
- }
- case (MUL(rs, rt, rd)) -> {
- if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
- if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR;
- if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR;
- }
- case (MULT(rs, rt)) -> {
- if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
- if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR;
- oR := RFull("HI") :: RFull ("LO") :: oR;
- }
- case (MULTU(rs, rt)) -> {
- if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
- if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR;
- oR := RFull("HI") :: RFull ("LO") :: oR;
- }
- case (DMULT(rs, rt)) -> {
- if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
- if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR;
- oR := RFull("HI") :: RFull ("LO") :: oR;
- }
- case (DMULTU(rs, rt)) -> {
- if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
- if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR;
- oR := RFull("HI") :: RFull ("LO") :: oR;
- }
- case (MADD(rs, rt)) -> {
- if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
- if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR;
- iR := RFull("HI") :: RFull ("LO") :: iR;
- oR := RFull("HI") :: RFull ("LO") :: oR;
- }
- case (MADDU(rs, rt)) -> {
- if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
- if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR;
- iR := RFull("HI") :: RFull ("LO") :: iR;
- oR := RFull("HI") :: RFull ("LO") :: oR;
- }
- case (MSUB(rs, rt)) -> {
- if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
- if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR;
- iR := RFull("HI") :: RFull ("LO") :: iR;
- oR := RFull("HI") :: RFull ("LO") :: oR;
- }
- case (MSUBU(rs, rt)) -> {
- if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
- if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR;
- iR := RFull("HI") :: RFull ("LO") :: iR;
- oR := RFull("HI") :: RFull ("LO") :: oR;
- }
- case (DIV(rs, rt)) -> {
- if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
- if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR;
- oR := RFull("HI") :: RFull ("LO") :: oR;
- }
- case (DIVU(rs, rt)) -> {
- if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
- if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR;
- oR := RFull("HI") :: RFull ("LO") :: oR;
- }
- case (DDIV(rs, rt)) -> {
- if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
- if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR;
- oR := RFull("HI") :: RFull ("LO") :: oR;
- }
- case (DDIVU(rs, rt)) -> {
- if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
- if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR;
- oR := RFull("HI") :: RFull ("LO") :: oR;
- }
- case (J(offset)) -> {
- (* XXX actually unconditional jump *)
- (*ik := IK_cond_branch;*)
- Dia := DIAFP_concrete((PC + 4)[63..28] : offset : 0b00);
- }
- case (JAL(offset)) -> {
- (* XXX actually unconditional jump *)
- (*ik := IK_cond_branch;*)
- oR := RFull("GPR31") :: oR;
- Dia := DIAFP_concrete((PC + 4)[63..28] : offset : 0b00);
- }
- case (JR(rs)) -> {
- (* XXX actually unconditional jump *)
- (*ik := IK_cond_branch;*)
- iR := RFull(GPRs[rs]) :: iR;
- Dia := DIAFP_reg(RFull(GPRs[rs]));
- }
- case (JALR(rs, rd)) -> {
- (* XXX actually unconditional jump *)
- (*ik := IK_cond_branch;*)
- iR := RFull(GPRs[rs]) :: iR;
- oR := RFull("GPR31") :: oR;
- Dia := DIAFP_reg(RFull(GPRs[rs]));
- }
- case (BEQ(rs, rd, imm, ne, likely)) -> {
- ik := IK_cond_branch;
- if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
- if rd == 0 then () else iR := RFull(GPRs[rd]) :: iR;
- let (bit[64]) offset = (EXTS(imm : 0b00) + 4) in
- Dia := DIAFP_concrete (PC + offset);
- }
- case (BCMPZ(rs, imm, cmp, link, likely)) -> {
- ik := IK_cond_branch;
- if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
+ (DADDIU (rs, rt, imm)) => {
+ if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR;
+ if rt == 0 then () else oR = RFull(GPRs[rt]) :: oR;
+ }
+ (DADDU (rs, rt, rd)) => {
+ if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR;
+ if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR;
+ if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR;
+ }
+ (DADDI (rs, rt, imm)) => {
+ if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR;
+ if rt == 0 then () else oR = RFull(GPRs[rt]) :: oR;
+ }
+ (DADD (rs, rt, rd)) => {
+ if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR;
+ if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR;
+ }
+ (ADD(rs, rt, rd)) => {
+ if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR;
+ if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR;
+ if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR;
+ }
+ (ADDI(rs, rt, imm)) => {
+ if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR;
+ if rt == 0 then () else oR = RFull(GPRs[rt]) :: oR;
+ }
+ (ADDU(rs, rt, rd)) => {
+ if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR;
+ if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR;
+ if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR;
+ }
+ (ADDIU(rs, rt, imm)) => {
+ if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR;
+ if rt == 0 then () else oR = RFull(GPRs[rt]) :: oR;
+ }
+ (DSUBU (rs, rt, rd)) => {
+ if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR;
+ if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR;
+ if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR;
+ }
+ (DSUB (rs, rt, rd)) => {
+ if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR;
+ if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR;
+ if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR;
+ }
+ (SUB(rs, rt, rd)) => {
+ if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR;
+ if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR;
+ if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR;
+ }
+ (SUBU(rs, rt, rd)) => {
+ if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR;
+ if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR;
+ if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR;
+ }
+ (AND (rs, rt, rd)) => {
+ if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR;
+ if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR;
+ if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR;
+ }
+ (ANDI (rs, rt, imm)) => {
+ if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR;
+ if rt == 0 then () else oR = RFull(GPRs[rt]) :: oR;
+ }
+ (OR (rs, rt, rd)) => {
+ if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR;
+ if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR;
+ if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR;
+ }
+ (ORI (rs, rt, imm)) => {
+ if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR;
+ if rt == 0 then () else oR = RFull(GPRs[rt]) :: oR;
+ }
+ (NOR (rs, rt, rd)) => {
+ if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR;
+ if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR;
+ if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR;
+ }
+ (XOR (rs, rt, rd)) => {
+ if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR;
+ if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR;
+ if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR;
+ }
+ (XORI (rs, rt, imm)) => {
+ if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR;
+ if rt == 0 then () else oR = RFull(GPRs[rt]) :: oR;
+ }
+ (LUI (rt, imm)) => {
+ if rt == 0 then () else oR = RFull(GPRs[rt]) :: oR;
+ }
+ (DSLL (rt, rd, sa)) => {
+ if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR;
+ if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR;
+ }
+ (DSLL32 (rt, rd, sa)) => {
+ if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR;
+ if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR;
+ }
+ (DSLLV (rs, rt, rd)) => {
+ if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR;
+ if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR;
+ if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR;
+ }
+ (DSRA (rt, rd, sa)) => {
+ if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR;
+ if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR;
+ }
+ (DSRA32 (rt, rd, sa)) => {
+ if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR;
+ if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR;
+ }
+ (DSRAV (rs, rt, rd)) => {
+ if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR;
+ if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR;
+ if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR;
+ }
+ (DSRL (rt, rd, sa)) => {
+ if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR;
+ if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR;
+ }
+ (DSRL32 (rt, rd, sa)) => {
+ if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR;
+ if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR;
+ }
+ (DSRLV (rs, rt, rd)) => {
+ if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR;
+ if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR;
+ if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR;
+ }
+ (SLL(rt, rd, sa)) => {
+ if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR;
+ if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR;
+ }
+ (SLLV(rs, rt, rd)) => {
+ if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR;
+ if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR;
+ if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR;
+ }
+ (SRA(rt, rd, sa)) => {
+ if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR;
+ if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR;
+ }
+ (SRAV(rs, rt, rd)) => {
+ if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR;
+ if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR;
+ if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR;
+ }
+ (SRL(rt, rd, sa)) => {
+ if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR;
+ if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR;
+ }
+ (SRLV(rs, rt, rd)) => {
+ if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR;
+ if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR;
+ if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR;
+ }
+ (SLT(rs, rt, rd)) => {
+ if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR;
+ if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR;
+ if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR;
+ }
+ (SLTI(rs, rt, imm)) => {
+ if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR;
+ if rt == 0 then () else oR = RFull(GPRs[rt]) :: oR;
+ }
+ (SLTU(rs, rt, rd)) => {
+ if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR;
+ if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR;
+ if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR;
+ }
+ (SLTIU(rs, rt, imm)) => {
+ if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR;
+ if rt == 0 then () else oR = RFull(GPRs[rt]) :: oR;
+ }
+ (MOVN(rs, rt, rd)) => {
+ /* XXX don't always write rd */
+ if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR;
+ if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR;
+ if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR;
+ }
+ (MOVZ(rs, rt, rd)) => {
+ /* XXX don't always write rd */
+ if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR;
+ if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR;
+ if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR;
+ }
+ (MFHI(rd)) => {
+ iR = RFull("HI") :: iR;
+ if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR;
+ }
+ (MFLO(rd)) => {
+ iR = RFull("LO") :: iR;
+ if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR;
+ }
+ (MTHI(rs)) => {
+ oR = RFull("HI") :: oR;
+ if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR;
+ }
+ (MTLO(rs)) => {
+ oR = RFull("LO") :: oR;
+ if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR;
+ }
+ (MUL(rs, rt, rd)) => {
+ if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR;
+ if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR;
+ if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR;
+ }
+ (MULT(rs, rt)) => {
+ if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR;
+ if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR;
+ oR = RFull("HI") :: RFull ("LO") :: oR;
+ }
+ (MULTU(rs, rt)) => {
+ if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR;
+ if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR;
+ oR = RFull("HI") :: RFull ("LO") :: oR;
+ }
+ (DMULT(rs, rt)) => {
+ if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR;
+ if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR;
+ oR = RFull("HI") :: RFull ("LO") :: oR;
+ }
+ (DMULTU(rs, rt)) => {
+ if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR;
+ if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR;
+ oR = RFull("HI") :: RFull ("LO") :: oR;
+ }
+ (MADD(rs, rt)) => {
+ if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR;
+ if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR;
+ iR = RFull("HI") :: RFull ("LO") :: iR;
+ oR = RFull("HI") :: RFull ("LO") :: oR;
+ }
+ (MADDU(rs, rt)) => {
+ if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR;
+ if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR;
+ iR = RFull("HI") :: RFull ("LO") :: iR;
+ oR = RFull("HI") :: RFull ("LO") :: oR;
+ }
+ (MSUB(rs, rt)) => {
+ if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR;
+ if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR;
+ iR = RFull("HI") :: RFull ("LO") :: iR;
+ oR = RFull("HI") :: RFull ("LO") :: oR;
+ }
+ (MSUBU(rs, rt)) => {
+ if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR;
+ if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR;
+ iR = RFull("HI") :: RFull ("LO") :: iR;
+ oR = RFull("HI") :: RFull ("LO") :: oR;
+ }
+ (DIV(rs, rt)) => {
+ if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR;
+ if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR;
+ oR = RFull("HI") :: RFull ("LO") :: oR;
+ }
+ (DIVU(rs, rt)) => {
+ if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR;
+ if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR;
+ oR = RFull("HI") :: RFull ("LO") :: oR;
+ }
+ (DDIV(rs, rt)) => {
+ if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR;
+ if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR;
+ oR = RFull("HI") :: RFull ("LO") :: oR;
+ }
+ (DDIVU(rs, rt)) => {
+ if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR;
+ if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR;
+ oR = RFull("HI") :: RFull ("LO") :: oR;
+ }
+ (J(offset)) => {
+ /* XXX actually unconditional jump */
+ /*ik = IK_cond_branch;*/
+ Dia = DIAFP_concrete((PC + 4)[63..28] : offset : 0b00);
+ }
+ (JAL(offset)) => {
+ /* XXX actually unconditional jump */
+ /*ik = IK_cond_branch;*/
+ oR = RFull("GPR31") :: oR;
+ Dia = DIAFP_concrete((PC + 4)[63..28] : offset : 0b00);
+ }
+ (JR(rs)) => {
+ /* XXX actually unconditional jump */
+ /*ik = IK_cond_branch;*/
+ iR = RFull(GPRs[rs]) :: iR;
+ Dia = DIAFP_reg(RFull(GPRs[rs]));
+ }
+ (JALR(rs, rd)) => {
+ /* XXX actually unconditional jump */
+ /*ik = IK_cond_branch;*/
+ iR = RFull(GPRs[rs]) :: iR;
+ oR = RFull("GPR31") :: oR;
+ Dia = DIAFP_reg(RFull(GPRs[rs]));
+ }
+ (BEQ(rs, rd, imm, ne, likely)) => {
+ ik = IK_cond_branch;
+ if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR;
+ if rd == 0 then () else iR = RFull(GPRs[rd]) :: iR;
+ let offset : bits(64) = (EXTS(imm : 0b00) + 4) in
+ Dia = DIAFP_concrete (PC + offset);
+ }
+ (BCMPZ(rs, imm, cmp, link, likely)) => {
+ ik = IK_cond_branch;
+ if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR;
if link then
- oR := RFull("GPR31") :: oR;
- let (bit[64]) offset = (EXTS(imm : 0b00) + 4) in
- Dia := DIAFP_concrete (PC + offset);
+ oR = RFull("GPR31") :: oR;
+ let offset : bits(64) = (EXTS(imm : 0b00) + 4) in
+ Dia = DIAFP_concrete (PC + offset);
}
- case (SYSCALL_THREAD_START) -> ()
-(*
+ (SYSCALL_THREAD_START) => ()
+/*
case (SYSCALL) =
case (BREAK) =
case (WAIT) = {
case (TRAPREG(rs, rt, cmp)) =
case (TRAPIMM(rs, imm, cmp)) =
-*)
- case (Load(width, signed, linked, base, rt, offset)) -> {
- ik := IK_mem_read (if linked then Read_reserve else Read_plain);
- if linked then oR := RFull("CP0LLBit")::RFull("CP0LLAddr")::oR else ();
- if base == 0 then () else aR := RFull(GPRs[base]) :: aR;
- iR := aR;
- if rt == 0 then () else oR := RFull(GPRs[rt]) :: oR;
- }
- case (Store(width, conditional, base, rt, offset)) -> {
- ik := IK_mem_write(if conditional then Write_conditional else Write_plain);
- if base == 0 then () else aR := RFull(GPRs[base]) :: aR;
- iR := aR;
- if conditional then iR := RFull("CP0LLBit")::iR else ();
- if (conditional & (rt != 0)) then oR := RFull(GPRs[rt])::oR else ();
- if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR;
- }
- case (LWL(base, rt, offset)) -> {
- ik := IK_mem_read(Read_plain);
- if base == 0 then () else aR := RFull(GPRs[base]) :: aR;
- iR := aR;
- if rt == 0 then () else oR := RFull(GPRs[rt]) :: oR;
- }
- case (LWR(base, rt, offset)) -> {
- ik := IK_mem_read(Read_plain);
- if base == 0 then () else aR := RFull(GPRs[base]) :: aR;
- iR := aR;
- if rt == 0 then () else oR := RFull(GPRs[rt]) :: oR;
- }
- case (SWL(base, rt, offset)) -> {
- ik := IK_mem_write(Write_plain);
- if base == 0 then () else aR := RFull(GPRs[base]) :: aR;
- iR := aR;
- if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR;
- }
- case (SWR(base, rt, offset)) -> {
- ik := IK_mem_write(Write_plain);
- if base == 0 then () else aR := RFull(GPRs[base]) :: aR;
- iR := aR;
- if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR;
- }
- case (LDL(base, rt, offset)) -> {
- ik := IK_mem_read(Read_plain);
- if base == 0 then () else aR := RFull(GPRs[base]) :: aR;
- iR := aR;
- if rt == 0 then () else oR := RFull(GPRs[rt]) :: oR;
- }
- case (LDR(base, rt, offset)) -> {
- ik := IK_mem_read(Read_plain);
- if base == 0 then () else aR := RFull(GPRs[base]) :: aR;
- iR := aR;
- if rt == 0 then () else oR := RFull(GPRs[rt]) :: oR;
- }
- case (SDL(base, rt, offset)) -> {
- ik := IK_mem_write(Write_plain);
- if base == 0 then () else aR := RFull(GPRs[base]) :: aR;
- iR := aR;
- if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR;
- }
- case (SDR(base, rt, offset)) -> {
- ik := IK_mem_write(Write_plain);
- if base == 0 then () else aR := RFull(GPRs[base]) :: aR;
- iR := aR;
- if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR;
- }
-(*
+*/
+ (Load(width, signed, linked, base, rt, offset)) => {
+ ik = IK_mem_read (if linked then Read_reserve else Read_plain);
+ if linked then oR = RFull("CP0LLBit")::RFull("CP0LLAddr")::oR else ();
+ if base == 0 then () else aR = RFull(GPRs[base]) :: aR;
+ iR = aR;
+ if rt == 0 then () else oR = RFull(GPRs[rt]) :: oR;
+ }
+ (Store(width, conditional, base, rt, offset)) => {
+ ik = IK_mem_write(if conditional then Write_conditional else Write_plain);
+ if base == 0 then () else aR = RFull(GPRs[base]) :: aR;
+ iR = aR;
+ if conditional then iR = RFull("CP0LLBit")::iR else ();
+ if (conditional & (rt != 0)) then oR = RFull(GPRs[rt])::oR else ();
+ if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR;
+ }
+ (LWL(base, rt, offset)) => {
+ ik = IK_mem_read(Read_plain);
+ if base == 0 then () else aR = RFull(GPRs[base]) :: aR;
+ iR = aR;
+ if rt == 0 then () else oR = RFull(GPRs[rt]) :: oR;
+ }
+ (LWR(base, rt, offset)) => {
+ ik = IK_mem_read(Read_plain);
+ if base == 0 then () else aR = RFull(GPRs[base]) :: aR;
+ iR = aR;
+ if rt == 0 then () else oR = RFull(GPRs[rt]) :: oR;
+ }
+ (SWL(base, rt, offset)) => {
+ ik = IK_mem_write(Write_plain);
+ if base == 0 then () else aR = RFull(GPRs[base]) :: aR;
+ iR = aR;
+ if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR;
+ }
+ (SWR(base, rt, offset)) => {
+ ik = IK_mem_write(Write_plain);
+ if base == 0 then () else aR = RFull(GPRs[base]) :: aR;
+ iR = aR;
+ if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR;
+ }
+ (LDL(base, rt, offset)) => {
+ ik = IK_mem_read(Read_plain);
+ if base == 0 then () else aR = RFull(GPRs[base]) :: aR;
+ iR = aR;
+ if rt == 0 then () else oR = RFull(GPRs[rt]) :: oR;
+ }
+ (LDR(base, rt, offset)) => {
+ ik = IK_mem_read(Read_plain);
+ if base == 0 then () else aR = RFull(GPRs[base]) :: aR;
+ iR = aR;
+ if rt == 0 then () else oR = RFull(GPRs[rt]) :: oR;
+ }
+ (SDL(base, rt, offset)) => {
+ ik = IK_mem_write(Write_plain);
+ if base == 0 then () else aR = RFull(GPRs[base]) :: aR;
+ iR = aR;
+ if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR;
+ }
+ (SDR(base, rt, offset)) => {
+ ik = IK_mem_write(Write_plain);
+ if base == 0 then () else aR = RFull(GPRs[base]) :: aR;
+ iR = aR;
+ if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR;
+ }
+/*
case (CACHE(base, op, imm)) =
case (PREF(base, op, imm)) =
-*)
- case (SYNC) -> {
- iK := IK_barrier(Barrier_MIPS_SYNC);
+*/
+ (SYNC) => {
+ iK = IK_barrier(Barrier_MIPS_SYNC);
}
-(*
+/*
case (MFC0(rt, rd, sel, double))
case (HCF)
case (MTC0(rt, rd, sel, double))
@@ -449,7 +449,7 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis (
case ((TLBP))
case (RDHWR(rt, rd))
case (ERET)
-*)
+*/
};
(iR,oR,aR,Nias,Dia,ik)
}
diff --git a/mips_new_tc/mips_ri.sail b/mips_new_tc/mips_ri.sail
index 3f368111..eb047771 100644
--- a/mips_new_tc/mips_ri.sail
+++ b/mips_new_tc/mips_ri.sail
@@ -1,39 +1,39 @@
-(*========================================================================*)
-(* *)
-(* 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. *)
-(*========================================================================*)
+/*========================================================================*/
+/* */
+/* 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. */
+/*========================================================================*/
-(* mips_ri.sail: only use if want unknown instructions to throw
- exception (like real hardware) instead of die (convenient for ppcmem) *)
+/* mips_ri.sail: only use if want unknown instructions to throw
+ exception (like real hardware) instead of die (convenient for ppcmem) */
union ast member unit RI
function clause decode _ = Some(RI)
diff --git a/mips_new_tc/mips_tlb.sail b/mips_new_tc/mips_tlb.sail
index 8e1b03ff..fc6a68f4 100644
--- a/mips_new_tc/mips_tlb.sail
+++ b/mips_new_tc/mips_tlb.sail
@@ -1,38 +1,38 @@
-(*========================================================================*)
-(* *)
-(* 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. *)
-(*========================================================================*)
+/*========================================================================*/
+/* */
+/* 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. */
+/*========================================================================*/
-val (bit[2], bit[27], bit[8], TLBEntry) -> bool effect pure tlbEntryMatch
+val tlbEntryMatch : (bits(2), bits(27), bits(8), TLBEntry) -> bool effect pure
function bool tlbEntryMatch(r, vpn2, asid, (TLBEntry) entry) =
let entryValid = entry.valid in
@@ -43,10 +43,10 @@ function bool tlbEntryMatch(r, vpn2, asid, (TLBEntry) entry) =
let entryG = entry.g in
(entryValid &
(r == entryR) &
- ((vpn2 & ~((bit[27]) (EXTZ(entryMask)))) == ((entryVPN) & ~((bit[27]) (EXTZ(entryMask))))) &
+ ((vpn2 & ~((bits(27)) (EXTZ(entryMask)))) == ((entryVPN) & ~((bits(27)) (EXTZ(entryMask))))) &
((asid == (entryASID)) | (entryG)))
-function option<TLBIndexT> tlbSearch((bit[64]) VAddr) =
+function option(TLBIndexT) tlbSearch((bits(64)) VAddr) =
let r = (VAddr[63..62]) in
let vpn2 = (VAddr[39..13]) in
let asid = TLBEntryHi.ASID in {
@@ -57,76 +57,76 @@ function option<TLBIndexT> tlbSearch((bit[64]) VAddr) =
None
}
-function (bit[64], bool) TLBTranslate2 ((bit[64]) vAddr, (MemAccessType) accessType) = {
+function (bits(64), bool) TLBTranslate2 ((bits(64)) vAddr, (MemAccessType) accessType) = {
let idx = tlbSearch(vAddr) in
- switch(idx) {
- case (Some(idx)) ->
+ match idx {
+ (Some(idx)) =>
let entry = (TLBEntries[idx]) in
let entryMask = entry.pagemask in
- let evenOddBit = ([|12:28|]) switch((bit[16])(entryMask)) {
- case 0x0000 -> 12
- case 0x0003 -> 14
- case 0x000f -> 16
- case 0x003f -> 18
- case 0x00ff -> 20
- case 0x03ff -> 22
- case 0x0fff -> 24
- case 0x3fff -> 26
- case 0xffff -> 28
- case _ -> undefined
+ let evenOddBit = ([|12:28|]) match (bits(16))(entryMask) {
+ 0x0000 => 12
+ 0x0003 => 14
+ 0x000f => 16
+ 0x003f => 18
+ 0x00ff => 20
+ 0x03ff => 22
+ 0x0fff => 24
+ 0x3fff => 26
+ 0xffff => 28
+ _ => undefined
} in
let isOdd = (vAddr[evenOddBit]) in
- let (caps, capl, pfn, d, v) = if (isOdd) then
- ((bit[1]) (entry.caps1), (bit[1]) (entry.capl1), (bit[24]) (entry.pfn1), (bit[1]) (entry.d1), (bit[1]) (entry.v1))
+ let if : caps, capl, pfn, d, v (isOdd) then
+ ((bits(1)) (entry.caps1), (bits(1)) (entry.capl1), (bits(24)) (entry.pfn1), (bits(1)) (entry.d1), (bits(1)) (entry.v1))
else
- ((bit[1]) (entry.caps0), (bit[1]) (entry.capl0), (bit[24]) (entry.pfn0), (bit[1]) (entry.d0), (bit[1]) (entry.v0)) in
+ ((bits(1)) (entry.caps0), (bits(1)) (entry.capl0), (bits(24)) (entry.pfn0), (bits(1)) (entry.d0), (bits(1)) (entry.v0)) in
if (~(v)) then
(SignalExceptionTLB(if (accessType == StoreData) then XTLBInvS else XTLBInvL, vAddr))
else if ((accessType == StoreData) & ~(d)) then
(SignalExceptionTLB(TLBMod, vAddr))
else
- let res = (bit[64]) (EXTZ(pfn[23..(evenOddBit - 12)] : vAddr[(evenOddBit - 1) .. 0])) in
- (res, (bool) (if (accessType == StoreData) then caps else capl)) (* FIXME: get rid of explicit cast here *)
- case None -> (SignalExceptionTLB(
+ let res = (bits(64)) (EXTZ(pfn[23..(evenOddBit - 12)] : vAddr[(evenOddBit - 1) .. 0])) in
+ (res, (bool) (if (accessType == StoreData) then caps else capl)) /* FIXME: get rid of explicit cast here */
+ None => (SignalExceptionTLB(
if (accessType == StoreData) then XTLBRefillS else XTLBRefillL, vAddr))
}
}
-val cast AccessLevel -> [|0:2|] effect pure cast_AccessLevel
+val cast_AccessLevel : cast AccessLevel -> [|0:2|] effect pure
function [|0:2|] cast_AccessLevel level =
{
switch level {
- case User -> 0
- case Supervisor -> 1
- case Kernel -> 2
+ User => 0
+ Supervisor => 1
+ Kernel => 2
}
}
-(* perform TLB translation. bool is CHERI specific TLB bits noStoreCap/suppressTag *)
-function (bit[64], bool) TLBTranslateC ((bit[64]) vAddr, (MemAccessType) accessType) =
+/* perform TLB translation. bool is CHERI specific TLB bits noStoreCap/suppressTag */
+function (bits(64), bool) TLBTranslateC ((bits(64)) vAddr, (MemAccessType) accessType) =
{
let currentAccessLevel = getAccessLevel() in
let compat32 = (vAddr[61..31] == 0b1111111111111111111111111111111) in
- let (requiredLevel, addr) = ((AccessLevel, option<bit[64]>)) switch((bit[2]) (vAddr[63..62])) {
- case 0b11 -> switch(compat32, (bit[2]) (vAddr[30..29])) { (* xkseg *)
- case (true, 0b11) -> (Kernel, (option<bit[64]>) None) (* kseg3 mapped 32-bit compat *)
- case (true, 0b10) -> (Supervisor, (option<bit[64]>) None) (* sseg mapped 32-bit compat *)
- case (true, 0b01) -> (Kernel, Some((bit[64]) (EXTZ(vAddr[28..0])))) (* kseg1 unmapped uncached 32-bit compat *)
- case (true, 0b00) -> (Kernel, Some((bit[64]) (EXTZ(vAddr[28..0])))) (* kseg0 unmapped cached 32-bit compat *)
- case (_, _) -> (Kernel, (option<bit[64]>) None) (* xkseg mapped *)
+ let AccessLevel : requiredLevel, addr, option(bits(64)))) match (bits(2)) (vAddr[63..62]) {
+ 0b11 => match compat32, (bits(2)) (vAddr[30..29]) { /* xkseg */
+ (true, 0b11) => (Kernel, (option(bits(64))) None) /* kseg3 mapped 32-bit compat */
+ (true, 0b10) => (Supervisor, (option(bits(64))) None) /* sseg mapped 32-bit compat */
+ (true, 0b01) => (Kernel, Some((bits(64)) (EXTZ(vAddr[28..0])))) /* kseg1 unmapped uncached 32-bit compat */
+ (true, 0b00) => (Kernel, Some((bits(64)) (EXTZ(vAddr[28..0])))) /* kseg0 unmapped cached 32-bit compat */
+ (_, _) => (Kernel, (option(bits(64))) None) /* xkseg mapped */
}
- case 0b10 -> (Kernel, Some((bit[64]) (EXTZ(vAddr[58..0])))) (* xkphys bits 61-59 are cache mode (ignored) *)
- case 0b01 -> (Supervisor, (option<bit[64]>) None) (* xsseg - supervisor mapped *)
- case 0b00 -> (User, (option<bit[64]>) None) (* xuseg - user mapped *)
+ 0b10 => (Kernel, Some((bits(64)) (EXTZ(vAddr[58..0])))) /* xkphys bits 61-59 are cache mode (ignored) */
+ 0b01 => (Supervisor, (option(bits(64))) None) /* xsseg - supervisor mapped */
+ 0b00 => (User, (option(bits(64))) None) /* xuseg - user mapped */
} in
if (((nat)currentAccessLevel) < ((nat)requiredLevel)) then
(SignalExceptionBadAddr(if (accessType == StoreData) then AdES else AdEL, vAddr))
else
- let (pa, c) = ((bit[64], bool)) switch(addr) {
- case (Some(a)) -> (a, false)
- case None -> if ((~(compat32)) & (unsigned(vAddr[61..0]) > MAX_VA)) then
+ let bit : pa, c[64], bool)) match addr {
+ (Some(a)) => (a, false)
+ None => if ((~(compat32)) & (unsigned(vAddr[61..0]) > MAX_VA)) then
(SignalExceptionBadAddr(if (accessType == StoreData) then AdES else AdEL, vAddr))
else
TLBTranslate2(vAddr, accessType)
@@ -137,5 +137,5 @@ function (bit[64], bool) TLBTranslateC ((bit[64]) vAddr, (MemAccessType) accessT
(pa, c)
}
-function (bit[64]) TLBTranslate ((bit[64]) vAddr, (MemAccessType) accessType) =
- let (addr, c) = TLBTranslateC(vAddr, accessType) in addr
+function (bits(64)) TLBTranslate ((bits(64)) vAddr, (MemAccessType) accessType) =
+ let TLBTranslateC : addr, c(vAddr, accessType) in addr
diff --git a/mips_new_tc/mips_tlb_stub.sail b/mips_new_tc/mips_tlb_stub.sail
index a9970a4e..04f80c35 100644
--- a/mips_new_tc/mips_tlb_stub.sail
+++ b/mips_new_tc/mips_tlb_stub.sail
@@ -1,40 +1,40 @@
-(*========================================================================*)
-(* *)
-(* 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. *)
-(*========================================================================*)
+/*========================================================================*/
+/* */
+/* 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. */
+/*========================================================================*/
-function option<TLBIndexT> tlbSearch((bit[64]) VAddr) = None
+function tlbSearch(VAddr) : bits(64) -> option(TLBIndexT) = None
-function (bit[64]) TLBTranslate ((bit[64]) vAddr, (MemAccessType) accessType) =
+function TLBTranslate (vAddr, accessType) : (bits(64), MemAccessType) -> bits(64) =
vAddr
-function (bit[64], bool) TLBTranslateC ((bit[64]) vAddr, (MemAccessType) accessType) = (vAddr, false)
+function TLBTranslateC (vAddr, accessType) : (bits(64), MemAccessType) -> (bits(64), bool) = (vAddr, false)
diff --git a/mips_new_tc/mips_wrappers.sail b/mips_new_tc/mips_wrappers.sail
index 70033977..281cb452 100644
--- a/mips_new_tc/mips_wrappers.sail
+++ b/mips_new_tc/mips_wrappers.sail
@@ -1,67 +1,69 @@
-(*========================================================================*)
-(* *)
-(* 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. *)
-(*========================================================================*)
+/*========================================================================*/
+/* */
+/* 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. */
+/*========================================================================*/
-(* mips_wrappers.sail: wrappers functions and hooks for CHERI extensibility
- (mostly identity functions here) *)
+/* mips_wrappers.sail: wrappers functions and hooks for CHERI extensibility
+ (mostly identity functions here) */
-val forall Nat 'n, 'n >= 1, 'n <= 8. (bit[64], [:'n:], bit[8 * 'n]) -> unit effect {eamem, wmv, wreg} MEMw_wrapper
+val MEMw_wrapper : forall 'n, 1 <= 'n <= 8. (bits(64), atom('n), bits(8 * 'n)) -> unit effect {eamem, wmv, wreg}
-function unit MEMw_wrapper((bit[64]) addr, ([:'n:]) size, (bit[8 * 'n]) data) =
+function MEMw_wrapper(addr, size, data) =
let ledata = reverse_endianness(data) in
if (addr == 0x000000007f000000) then
{
- UART_WDATA := ledata[7..0];
- UART_WRITTEN := (bit[1]) 1;
+ UART_WDATA = ledata[7..0];
+ UART_WRITTEN = bitone;
} else {
MEMea(addr, size);
MEMval(addr, size, ledata);
}
-val forall Nat 'n, 'n >= 1, 'n <= 8. (bit[64], [:'n:], bit[8 * 'n]) -> bool effect {eamem, wmv} MEMw_conditional_wrapper
+val MEMw_conditional_wrapper : forall 'n, 1 <= 'n <= 8. (bits(64), atom('n), bits(8 * 'n)) -> bool effect {eamem, wmv}
-function bool MEMw_conditional_wrapper(addr, size, data) =
+function MEMw_conditional_wrapper(addr, size, data) =
{
MEMea_conditional(addr, size);
MEMval_conditional(addr, size, reverse_endianness(data))
}
-function bit[64] addrWrapper((bit[64]) addr, (MemAccessType) accessType, (WordType) width) =
+val addrWrapper : (bits(64), MemAccessType, WordType) -> bits(64)
+function addrWrapper(addr, accessType, width) =
addr
-function (bit[64]) TranslatePC ((bit[64]) vAddr) = {
+val TranslatePC : bits(64) -> bits(64)
+function TranslatePC (vAddr) = {
incrementCP0Count();
- if (vAddr[1..0] != 0b00) then (* bad PC alignment *)
+ if (vAddr[1..0] != 0b00) then /* bad PC alignment */
(SignalExceptionBadAddr(AdEL, vAddr))
else
TLBTranslate(vAddr, Instruction)
@@ -69,6 +71,8 @@ function (bit[64]) TranslatePC ((bit[64]) vAddr) = {
let have_cp2 = false
-function forall Type 'o. 'o SignalException ((Exception) ex) = SignalExceptionMIPS(ex, 0x0000000000000000)
-function unit ERETHook() = ()
+function SignalException (ex) = SignalExceptionMIPS(ex, 0x0000000000000000)
+
+val ERETHook : unit -> unit
+function ERETHook() = ()
diff --git a/mips_new_tc/prelude.sail b/mips_new_tc/prelude.sail
new file mode 100644
index 00000000..9d7c84cb
--- /dev/null
+++ b/mips_new_tc/prelude.sail
@@ -0,0 +1,393 @@
+default Order dec
+
+type bits ('n : Int) = vector('n, dec, bit)
+union option ('a : Type) = {None, Some : 'a}
+
+val eq_atom = {ocaml: "eq_int", lem: "eq"} : forall 'n 'm. (atom('n), atom('m)) -> bool
+val lteq_atom = "lteq" : forall 'n 'm. (atom('n), atom('m)) -> bool
+val gteq_atom = "gteq" : forall 'n 'm. (atom('n), atom('m)) -> bool
+val lt_atom = "lt" : forall 'n 'm. (atom('n), atom('m)) -> bool
+val gt_atom = "gt" : forall 'n 'm. (atom('n), atom('m)) -> bool
+
+val eq_int = {ocaml: "eq_int", lem: "eq"} : (int, int) -> bool
+
+val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
+
+val eq_string = {ocaml: "eq_string", lem: "eq"} : (string, string) -> bool
+
+val eq_real = {ocaml: "eq_real", lem: "eq"} : (real, real) -> bool
+
+val eq_anything = {ocaml: "(fun (x, y) -> x = y)", lem: "eq"} : forall ('a : Type). ('a, 'a) -> bool
+
+val bitvector_length = {ocaml: "length", lem: "length"} : forall 'n. bits('n) -> atom('n)
+val vector_length = {ocaml: "length", lem: "length_list"} : forall 'n ('a : Type). vector('n, dec, 'a) -> atom('n)
+val list_length = {ocaml: "length", lem: "length_list"} : forall ('a : Type). list('a) -> int
+
+overload length = {bitvector_length, vector_length, list_length}
+
+val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg}
+/* sneaky deref with no effect necessary for bitfield writes */
+val _reg_deref = "reg_deref" : forall ('a : Type). register('a) -> 'a
+
+overload operator == = {eq_atom, eq_int, eq_vec, eq_string, eq_real, eq_anything}
+
+val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_dec"} : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm <= 'n.
+ (bits('n), atom('m), atom('o)) -> bits('m - ('o - 1))
+
+val bitvector_access = {ocaml: "access", lem: "access_vec_dec"} : forall ('n : Int) ('m : Int), 0 <= 'm < 'n.
+ (bits('n), atom('m)) -> bit
+
+val any_vector_access = {ocaml: "access", lem: "access_list_dec"} : forall ('n : Int) ('m : Int) ('a : Type), 0 <= 'm < 'n.
+ (vector('n, dec, 'a), atom('m)) -> 'a
+
+overload vector_access = {bitvector_access, any_vector_access}
+
+val bitvector_update = {ocaml: "update", lem: "update_vec_dec"} : forall 'n.
+ (bits('n), int, bit) -> bits('n)
+
+val any_vector_update = {ocaml: "update", lem: "update_list_dec"} : forall 'n ('a : Type).
+ (vector('n, dec, 'a), int, 'a) -> vector('n, dec, 'a)
+
+overload vector_update = {bitvector_update, any_vector_update}
+
+val update_subrange = {ocaml: "update_subrange", lem: "update_subrange_vec_dec"} : forall 'n 'm 'o.
+ (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n)
+
+val vcons = {lem: "cons_vec"} : forall ('n : Int) ('a : Type).
+ ('a, vector('n, dec, 'a)) -> vector('n + 1, dec, 'a)
+
+val bitvector_concat = {ocaml: "append", lem: "concat_vec"} : forall ('n : Int) ('m : Int).
+ (bits('n), bits('m)) -> bits('n + 'm)
+
+val vector_concat = {ocaml: "append", lem: "append_list"} : forall ('n : Int) ('m : Int) ('a : Type).
+ (vector('n, dec, 'a), vector('m, dec, 'a)) -> vector('n + 'm, dec, 'a)
+
+overload append = {bitvector_concat, vector_concat}
+
+val not_bool = "not" : bool -> bool
+
+val not_vec = "not_vec" : forall 'n. bits('n) -> bits('n)
+
+overload ~ = {not_bool, not_vec}
+
+val neq_atom = {lem: "neq"} : forall 'n 'm. (atom('n), atom('m)) -> bool
+
+function neq_atom (x, y) = not_bool(eq_atom(x, y))
+
+val neq_int = {lem: "neq"} : (int, int) -> bool
+
+function neq_int (x, y) = not_bool(eq_int(x, y))
+
+val neq_vec = {lem: "neq"} : forall 'n. (bits('n), bits('n)) -> bool
+
+function neq_vec (x, y) = not_bool(eq_vec(x, y))
+
+val neq_anything = {lem: "neq"} : forall ('a : Type). ('a, 'a) -> bool
+
+function neq_anything (x, y) = not_bool(x == y)
+
+overload operator != = {neq_atom, neq_int, neq_vec, neq_anything}
+
+val and_bool = "and_bool" : (bool, bool) -> bool
+
+val builtin_and_vec = {ocaml: "and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
+
+val and_vec = {lem: "and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
+
+function and_vec (xs, ys) = builtin_and_vec(xs, ys)
+
+overload operator & = {and_bool, and_vec}
+
+val or_bool = "or_bool" : (bool, bool) -> bool
+
+val builtin_or_vec = {ocaml: "or_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
+
+val or_vec = {lem: "or_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
+
+function or_vec (xs, ys) = builtin_or_vec(xs, ys)
+
+overload operator | = {or_bool, or_vec}
+
+val unsigned = {ocaml: "uint", lem: "unsigned"} : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1)
+
+val signed = {ocaml: "sint", lem: "signed"} : forall 'n. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1)
+
+val hex_slice = "hex_slice" : forall 'n 'm. (string, atom('n), atom('m)) -> bits('n - 'm)
+
+val __SetSlice_bits = "set_slice" : forall 'n 'm.
+ (atom('n), atom('m), bits('n), int, bits('m)) -> bits('n)
+
+val __SetSlice_int = "set_slice_int" : forall 'w. (atom('w), int, int, bits('w)) -> int
+
+val __raw_SetSlice_int : forall 'w. (atom('w), int, int, bits('w)) -> int
+
+val __raw_GetSlice_int = "get_slice_int" : forall 'w. (atom('w), int, int) -> bits('w)
+
+val __GetSlice_int : forall 'n. (atom('n), int, int) -> bits('n)
+
+function __GetSlice_int (n, m, o) = __raw_GetSlice_int(n, m, o)
+
+val __raw_SetSlice_bits : forall 'n 'w.
+ (atom('n), atom('w), bits('n), int, bits('w)) -> bits('n)
+
+val __raw_GetSlice_bits : forall 'n 'w.
+ (atom('n), atom('w), bits('n), int) -> bits('w)
+
+val "shiftl" : forall 'm. (bits('m), int) -> bits('m)
+val "shiftr" : forall 'm. (bits('m), int) -> bits('m)
+
+val __SignExtendSlice = {lem: "exts_slice"} : forall 'm. (bits('m), int, int) -> bits('m)
+
+val __ZeroExtendSlice = {lem: "extz_slice"} : forall 'm. (bits('m), int, int) -> bits('m)
+
+val cast cast_unit_vec : bit -> bits(1)
+
+function cast_unit_vec bitzero = 0b0
+and cast_unit_vec bitone = 0b1
+
+val print = "prerr_endline" : string -> unit
+
+val putchar = "putchar" : forall ('a : Type). 'a -> unit
+
+val concat_str = {ocaml: "concat_str", lem: "stringAppend"} : (string, string) -> string
+
+val string_of_int = "string_of_int" : int -> string
+
+val DecStr : int -> string
+
+val HexStr : int -> string
+
+val BitStr = "string_of_bits" : forall 'n. bits('n) -> string
+
+val xor_vec = "xor_vec" : forall 'n. (bits('n), bits('n)) -> bits('n)
+
+val int_power = {ocaml: "int_power", lem: "pow"} : (int, int) -> int
+
+val real_power = {ocaml: "real_power", lem: "realPowInteger"} : (real, int) -> real
+
+overload operator ^ = {xor_vec, int_power, real_power}
+
+val add_range = {ocaml: "add_int", lem: "integerAdd"} : forall 'n 'm 'o 'p.
+ (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p)
+
+val add_int = {ocaml: "add_int", lem: "integerAdd"} : (int, int) -> int
+
+val add_vec = "add_vec" : forall 'n. (bits('n), bits('n)) -> bits('n)
+
+val add_vec_int = "add_vec_int" : forall 'n. (bits('n), int) -> bits('n)
+
+val add_real = {ocaml: "add_real", lem: "realAdd"} : (real, real) -> real
+
+overload operator + = {add_range, add_int, add_vec, add_vec_int, add_real}
+
+val sub_range = {ocaml: "sub_int", lem: "integerMinus"} : forall 'n 'm 'o 'p.
+ (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o)
+
+val sub_int = {ocaml: "sub_int", lem: "integerMinus"} : (int, int) -> int
+
+val "sub_vec" : forall 'n. (bits('n), bits('n)) -> bits('n)
+
+val "sub_vec_int" : forall 'n. (bits('n), int) -> bits('n)
+
+val sub_real = {ocaml: "sub_real", lem: "realMinus"} : (real, real) -> real
+
+val negate_range = {ocaml: "minus_big_int", lem: "integerNegate"} : forall 'n 'm. range('n, 'm) -> range(- 'm, - 'n)
+
+val negate_int = {ocaml: "minus_big_int", lem: "integerNegate"} : int -> int
+
+val negate_real = {ocaml: "Num.minus_num", lem: "realNegate"} : real -> real
+
+overload operator - = {sub_range, sub_int, sub_vec, sub_vec_int, sub_real}
+
+overload negate = {negate_range, negate_int, negate_real}
+
+val mult_range = {ocaml: "mult", lem: "integerMult"} : forall 'n 'm 'o 'p.
+ (range('n, 'm), range('o, 'p)) -> range('n * 'o, 'm * 'p)
+
+val mult_int = {ocaml: "mult", lem: "integerMult"} : (int, int) -> int
+
+val mult_real = {ocaml: "mult_real", lem: "realMult"} : (real, real) -> real
+
+overload operator * = {mult_range, mult_int, mult_real}
+
+val Sqrt = {ocaml: "sqrt_real", lem: "realSqrt"} : real -> real
+
+val gteq_int = "gteq" : (int, int) -> bool
+
+val gteq_real = {ocaml: "gteq_real", lem: "gteq"} : (real, real) -> bool
+
+overload operator >= = {gteq_atom, gteq_int, gteq_real}
+
+val lteq_int = "lteq" : (int, int) -> bool
+
+val lteq_real = {ocaml: "lteq_real", lem: "lteq"} : (real, real) -> bool
+
+overload operator <= = {lteq_atom, lteq_int, lteq_real}
+
+val gt_int = "gt" : (int, int) -> bool
+
+val gt_real = {ocaml: "gt_real", lem: "gt"} : (real, real) -> bool
+
+overload operator > = {gt_atom, gt_int, gt_real}
+
+val lt_int = "lt" : (int, int) -> bool
+
+val lt_real = {ocaml: "lt_real", lem: "lt"} : (real, real) -> bool
+
+overload operator < = {lt_atom, lt_int, lt_real}
+
+val RoundDown = {ocaml: "round_down", lem: "realFloor"} : real -> int
+
+val RoundUp = {ocaml: "round_up", lem: "realCeiling"} : real -> int
+
+val abs_int = {ocaml: "abs_int", lem: "abs"} : int -> int
+
+val abs_real = {ocaml: "abs_real", lem: "abs"} : real -> real
+
+overload abs = {abs_int, abs_real}
+
+val quotient_nat = {ocaml: "quotient", lem: "integerDiv"} : (nat, nat) -> nat
+
+val quotient_real = {ocaml: "quotient_real", lem: "realDiv"} : (real, real) -> real
+
+val quotient = {ocaml: "quotient", lem: "integerDiv"} : (int, int) -> int
+
+overload operator / = {quotient_nat, quotient, quotient_real}
+
+val quot_round_zero = {ocaml: "quot_round_zero", lem: "hardware_quot"} : (int, int) -> int
+val rem_round_zero = {ocaml: "rem_round_zero", lem: "hardware_mod"} : (int, int) -> int
+
+val modulus = {ocaml: "modulus", lem: "hardware_mod"} : (int, int) -> int
+
+overload operator % = {modulus}
+
+val Real = {ocaml: "Num.num_of_big_int", lem: "realFromInteger"} : int -> real
+
+val shl_int = "shl_int" : (int, int) -> int
+
+val shr_int = "shr_int" : (int, int) -> int
+
+val min_nat = {ocaml: "min_int", lem: "min"} : (nat, nat) -> nat
+
+val min_int = {ocaml: "min_int", lem: "min"} : (int, int) -> int
+
+val max_nat = {ocaml: "max_int", lem: "max"} : (nat, nat) -> nat
+
+val max_int = {ocaml: "max_int", lem: "max"} : (int, int) -> int
+
+overload min = {min_nat, min_int}
+
+overload max = {max_nat, max_int}
+
+val __WriteRAM = "write_ram" : forall 'n 'm.
+ (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> unit effect {wmv}
+
+val __RISCV_write : forall 'n. (bits(64), atom('n), bits(8 * 'n)) -> unit effect {wmv}
+function __RISCV_write (addr, width, data) = __WriteRAM(64, width, 0x0000_0000_0000_0000, addr, data)
+
+val __TraceMemoryWrite : forall 'n 'm.
+ (atom('n), bits('m), bits(8 * 'n)) -> unit
+
+val __ReadRAM = "read_ram" : forall 'n 'm.
+ (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
+
+val __RISCV_read : forall 'n. (bits(64), atom('n)) -> bits(8 * 'n) effect {rmem}
+function __RISCV_read (addr, width) = __ReadRAM(64, width, 0x0000_0000_0000_0000, addr)
+
+val __TraceMemoryRead : forall 'n 'm. (atom('n), bits('m), bits(8 * 'n)) -> unit
+
+val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm)
+
+infix 4 ^^
+function operator ^^ (bs, n) = replicate_bits (bs, n)
+
+val cast ex_nat : nat -> {'n, 'n >= 0. atom('n)}
+
+function ex_nat 'n = n
+
+val cast ex_int : int -> {'n, true. atom('n)}
+
+function ex_int 'n = n
+
+/*
+val cast ex_range : forall 'n 'm. range('n, 'm) -> {'o, 'n <= 'o <= 'm. atom('o)}
+
+function ex_range (n as 'N) = n
+*/
+
+val coerce_int_nat : int -> nat effect {escape}
+
+function coerce_int_nat 'x = {
+ assert(constraint('x >= 0));
+ x
+}
+
+val slice = "slice" : forall ('n : Int) ('m : Int), 'm >= 0 & 'n >= 0.
+ (bits('m), int, atom('n)) -> bits('n)
+
+val pow2 = "pow2" : forall 'n. atom('n) -> atom(2 ^ 'n)
+
+val print_int = "print_int" : (string, int) -> unit
+val print_bits = "print_bits" : forall 'n. (string, bits('n)) -> unit
+val print_string = "print_string" : (string, string) -> unit
+
+union exception = {
+ Error_not_implemented : string,
+ Error_misaligned_access,
+ Error_EBREAK,
+ Error_internal_error
+}
+
+val "sign_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m)
+val "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m)
+
+val EXTS : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m)
+val EXTZ : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m)
+
+function EXTS v = sign_extend(v, sizeof('m))
+function EXTZ v = zero_extend(v, sizeof('m))
+
+infix 4 <_s
+infix 4 >=_s
+infix 4 <_u
+infix 4 >=_u
+
+val operator <_s = {lem: "slt_vec"} : forall 'n. (bits('n), bits('n)) -> bool
+val operator >=_s = {lem: "sgteq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
+val operator <_u = {lem: "ult_vec"} : forall 'n. (bits('n), bits('n)) -> bool
+val operator >=_u = {lem: "ugteq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
+
+function operator <_s (x, y) = signed(x) < signed(y)
+function operator >=_s (x, y) = signed(x) >= signed(y)
+function operator <_u (x, y) = unsigned(x) < unsigned(y)
+function operator >=_u (x, y) = unsigned(x) >= unsigned(y)
+
+val cast bool_to_bits : bool -> bits(1)
+function bool_to_bits x = if x then 0b1 else 0b0
+
+val cast bit_to_bool : bit -> bool
+function bit_to_bool bitone = true
+and bit_to_bool bitzero = false
+
+infix 7 >>
+infix 7 <<
+
+val operator >> = "shift_bits_right" : forall 'n 'm. (bits('n), bits('m)) -> bits('n)
+val operator << = "shift_bits_left" : forall 'n 'm. (bits('n), bits('m)) -> bits('n)
+
+val vector64 : int -> bits(64)
+
+function vector64 n = __raw_GetSlice_int(64, n, 0)
+
+val to_bits : forall 'l.(atom('l), int) -> bits('l)
+function to_bits (l, n) = __raw_GetSlice_int(l, n, 0)
+
+function break () : unit -> unit = ()
+
+val vector_update_subrange_dec = {ocaml: "update_subrange", lem: "update_subrange_vec_dec"} : forall 'n 'm 'o.
+ (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n)
+
+val vector_update_subrange_inc = {ocaml: "update_subrange", lem: "update_subrange_vec_inc"} : forall 'n 'm 'o.
+ (vector('n, inc, bit), atom('m), atom('o), vector('o - ('m - 1), inc, bit)) -> vector('n, inc, bit)
+
+overload vector_update_subrange = {vector_update_subrange_dec, vector_update_subrange_inc}
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 23:09:57 +0000