summaryrefslogtreecommitdiff
path: root/mips_new_tc
diff options
context:
space:
mode:
authorRobert Norton2018-03-08 16:49:50 +0000
committerRobert Norton2018-03-08 16:51:03 +0000
commit7f894658e6cf53a3ebf4dec5ccf788450de53d1e (patch)
treefb8a1855311b2d0fdd9ed398bfcd8de70c374321 /mips_new_tc
parent9e48920689ed4290f0bf155d604292143d5f5ffa (diff)
rename mips_new_tc to mips
Diffstat (limited to 'mips_new_tc')
-rw-r--r--mips_new_tc/Makefile31
-rw-r--r--mips_new_tc/main.sail57
-rw-r--r--mips_new_tc/mips_ast_decl.sail44
-rw-r--r--mips_new_tc/mips_epilogue.sail42
-rw-r--r--mips_new_tc/mips_extras.lem94
-rw-r--r--mips_new_tc/mips_insts.sail1708
-rw-r--r--mips_new_tc/mips_prelude.sail620
-rw-r--r--mips_new_tc/mips_regfp.sail455
-rw-r--r--mips_new_tc/mips_ri.sail42
-rw-r--r--mips_new_tc/mips_tlb.sail148
-rw-r--r--mips_new_tc/mips_tlb_stub.sail48
-rw-r--r--mips_new_tc/mips_wrappers.sail86
-rw-r--r--mips_new_tc/prelude.sail391
13 files changed, 0 insertions, 3766 deletions
diff --git a/mips_new_tc/Makefile b/mips_new_tc/Makefile
deleted file mode 100644
index fb926c6e..00000000
--- a/mips_new_tc/Makefile
+++ /dev/null
@@ -1,31 +0,0 @@
-THIS_MAKEFILE := $(realpath $(lastword $(MAKEFILE_LIST)))
-SAIL_DIR:=$(realpath $(dir $(THIS_MAKEFILE))..)
-export SAIL_DIR
-SAIL_LIB_DIR:=$(SAIL_DIR)/lib
-MIPS_SAIL_DIR:=$(SAIL_DIR)/mips_new_tc
-
-SAIL:=$(SAIL_DIR)/sail
-
-MIPS_PRE:=$(SAIL_LIB_DIR)/flow.sail $(MIPS_SAIL_DIR)/prelude.sail $(MIPS_SAIL_DIR)/mips_prelude.sail
-MIPS_TLB:=$(MIPS_SAIL_DIR)/mips_tlb.sail
-MIPS_TLB_STUB:=$(MIPS_SAIL_DIR)/mips_tlb_stub.sail
-MIPS_SAILS:=$(MIPS_SAIL_DIR)/mips_wrappers.sail $(MIPS_SAIL_DIR)/mips_ast_decl.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail
-MIPS_MAIN:=$(MIPS_SAIL_DIR)/main.sail
-
-mips: $(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS) $(MIPS_MAIN)
- $(SAIL) -ocaml -o mips $^
-
-mips_no_tlb.lem: $(MIPS_PRE) $(MIPS_TLB_STUB) $(MIPS_SAILS)
- $(SAIL) -lem -o mips_no_tlb -lem_mwords -lem_lib Mips_extras -undefined_gen $^
-mips_no_tlb_types.lem: mips_no_tlb.lem
-
-# TODO: Use monomorphisation so that we can switch to machine words
-mips.lem: $(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS)
- $(SAIL) -lem -o mips -lem_lib Mips_extras -undefined_gen $^
-mips_types.lem: mips.lem
-
-M%.thy: m%.lem m%_types.lem mips_extras.lem
- lem -isa -outdir . -lib $(SAIL_DIR)/src/gen_lib -lib $(SAIL_DIR)/src/lem_interp $^
-
-clean:
- rm -rf mips Mips.thy mips.lem _sbuild
diff --git a/mips_new_tc/main.sail b/mips_new_tc/main.sail
deleted file mode 100644
index 2df5c0f8..00000000
--- a/mips_new_tc/main.sail
+++ /dev/null
@@ -1,57 +0,0 @@
-
-
-
-val fetch_and_execute : unit -> unit effect {barr, eamem, escape, rmem, rreg, wmv, wreg, undef, wmvt, rmemt}
-function fetch_and_execute () = {
- while true do {
- PC = nextPC;
- inBranchDelay = branchPending;
- branchPending = 0b0;
- nextPC = if inBranchDelay then delayedPC else PC + 4;
- cp2_next_pc();
-
- print_bits("PC: ", PC);
- try {
- let pc_pa = TranslatePC(PC);
- /*print_bits("pa: ", pc_pa);*/
- let instr = MEMr_wrapper(pc_pa, 4);
- /*print_bits("hex: ", instr);*/
- let instr_ast = decode(instr);
- match instr_ast {
- Some(HCF()) => {
- print("simulation stopped due to halt instruction.");
- return ();
- },
- Some(ast) => execute(ast),
- None() => {print("Decode failed"); exit (())} /* Never expect this -- unknown instruction should actually result in reserved instruction ISA-level exception (see mips_ri.sail). */
- }
- } catch {
- ISAException() => print("EXCEPTION")
- /* ISA-level exception occurrred either during TranslatePC or execute --
- just continue from nextPC, which should have been set to the appropriate
- exception vector (along with clearing branchPending etc.) . */
- };
- };
- skip_rmemt();
- skip_wmvt();
-}
-
-val elf_entry = "Elf_loader.elf_entry" : unit -> int
-
-val main : unit -> unit effect {barr, eamem, escape, rmem, rreg, undef, wmv, wreg, rmemt, wmvt}
-
-function dump_mips_state () : unit -> unit = {
- print_bits("DEBUG MIPS PC ", PC);
- foreach (idx from 0 to 31) {
- print(concat_str("DEBUG MIPS REG ", concat_str(string_of_int(idx), concat_str(" ", BitStr(rGPR(to_bits(5,idx)))))));
- }
-}
-
-function main () = {
- init_cp0_state();
- init_cp2_state();
- nextPC = to_bits(64, elf_entry());
- fetch_and_execute();
- dump_mips_state ();
- dump_cp2_state ()
-}
diff --git a/mips_new_tc/mips_ast_decl.sail b/mips_new_tc/mips_ast_decl.sail
deleted file mode 100644
index e39bc270..00000000
--- a/mips_new_tc/mips_ast_decl.sail
+++ /dev/null
@@ -1,44 +0,0 @@
-/*========================================================================*/
-/* */
-/* 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 */
-
-scattered union ast
-
-val execute : ast -> unit effect {barr, eamem, escape, rmem, rreg, undef, wmv, wreg}
-scattered function execute
-
-val decode : bits(32) -> option(ast) effect pure
-scattered function decode
diff --git a/mips_new_tc/mips_epilogue.sail b/mips_new_tc/mips_epilogue.sail
deleted file mode 100644
index c7477a50..00000000
--- a/mips_new_tc/mips_epilogue.sail
+++ /dev/null
@@ -1,42 +0,0 @@
-/*========================================================================*/
-/* */
-/* 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. */
-
-end decode
-end execute
-end ast
-
-val supported_instructions : ast -> option(ast)
-function supported_instructions instr = Some(instr)
diff --git a/mips_new_tc/mips_extras.lem b/mips_new_tc/mips_extras.lem
deleted file mode 100644
index 920277f6..00000000
--- a/mips_new_tc/mips_extras.lem
+++ /dev/null
@@ -1,94 +0,0 @@
-open import Pervasives
-open import Pervasives_extra
-open import Sail_instr_kinds
-open import Sail_values
-open import Sail_operators
-open import Prompt_monad
-open import Prompt
-
-val MEMr : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monad 'regval 'b 'e
-val MEMr_reserve : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monad 'regval 'b 'e
-val MEMr_tag : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monad 'regval (bool * 'b) 'e
-val MEMr_tag_reserve : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monad 'regval (bool * 'b) 'e
-
-let MEMr addr size = read_mem Read_plain addr size
-let MEMr_reserve addr size = read_mem Read_reserve addr size
-
-let MEMr_tag addr size =
- read_mem Read_plain addr size >>= fun v ->
- read_tag addr >>= fun t ->
- return (bool_of_bitU t, v)
-
-let MEMr_tag_reserve addr size =
- read_mem Read_plain addr size >>= fun v ->
- read_tag addr >>= fun t ->
- return (bool_of_bitU t, v)
-
-
-val MEMea : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monad 'regval unit 'e
-val MEMea_conditional : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monad 'regval unit 'e
-val MEMea_tag : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monad 'regval unit 'e
-val MEMea_tag_conditional : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monad 'regval unit 'e
-
-let MEMea addr size = write_mem_ea Write_plain addr size
-let MEMea_conditional addr size = write_mem_ea Write_conditional addr size
-
-let MEMea_tag addr size = write_mem_ea Write_plain addr size
-let MEMea_tag_conditional addr size = write_mem_ea Write_conditional addr size
-
-
-val MEMval : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> 'b -> monad 'regval unit 'e
-val MEMval_conditional : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> 'b -> monad 'regval bool 'e
-val MEMval_tag : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> bool -> 'b -> monad 'regval unit 'e
-val MEMval_tag_conditional : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> bool -> 'b -> monad 'regval bool 'e
-
-let MEMval _ size v = write_mem_val v >>= fun _ -> return ()
-let MEMval_conditional _ size v = write_mem_val v >>= fun b -> return (if b then true else false)
-let MEMval_tag _ size t v = write_mem_val v >>= fun _ -> write_tag_val (bitU_of_bool t) >>= fun _ -> return ()
-let MEMval_tag_conditional _ size t v = write_mem_val v >>= fun b -> write_tag_val (bitU_of_bool t) >>= fun _ -> return (if b then true else false)
-
-val MEM_sync : forall 'regval 'e. unit -> monad 'regval unit 'e
-
-let MEM_sync () = barrier Barrier_MIPS_SYNC
-
-(* Some wrappers copied from aarch64_extras *)
-(* TODO: Harmonise into a common library *)
-
-let get_slice_int_bl len n lo =
- (* TODO: Is this the intended behaviour? *)
- let hi = lo + len - 1 in
- let bits = bits_of_int (hi + 1) n in
- get_bits false bits hi lo
-
-val get_slice_int : forall 'a. Bitvector 'a => integer -> integer -> integer -> 'a
-let get_slice_int len n lo = of_bits (get_slice_int_bl len n lo)
-
-let write_ram _ size _ addr data =
- MEMea addr size >>
- MEMval addr size data
-
-let read_ram _ size _ addr = MEMr addr size
-
-let sign_extend bits len = exts_bv len bits
-let zero_extend bits len = extz_bv len bits
-
-let shift_bits_left v n = shiftl_bv v (unsigned n)
-let shift_bits_right v n = shiftr_bv v (unsigned n)
-let shift_bits_right_arith v n = arith_shiftr_bv v (unsigned n)
-
-(* TODO: These could be monadic instead of hardcoded *)
-let internal_pick vs = head vs
-let undefined_string () = ""
-let undefined_unit () = ()
-let undefined_int () = (0:ii)
-let undefined_bool () = false
-val undefined_vector : forall 'a. integer -> 'a -> list 'a
-let undefined_vector len u = repeat [u] len
-val undefined_bitvector : forall 'a. Bitvector 'a => integer -> 'a
-let undefined_bitvector len = of_bits (repeat [B0] len)
-let undefined_bits len = undefined_bitvector len
-let undefined_bit () = B0
-let undefined_real () = realFromFrac 0 1
-let undefined_range i j = i
-let undefined_atom i = i
-let undefined_nat () = (0:ii)
diff --git a/mips_new_tc/mips_insts.sail b/mips_new_tc/mips_insts.sail
deleted file mode 100644
index e8f9a0f7..00000000
--- a/mips_new_tc/mips_insts.sail
+++ /dev/null
@@ -1,1708 +0,0 @@
-/*========================================================================*/
-/* */
-/* 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 */
-
-union clause ast = DADDIU : (regno, regno, imm16)
-
-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) + EXTS(imm)
- }
-
-/* DADDU Doubleword Add Unsigned -- another very simple instruction,
- reg, reg, reg */
-
-union clause ast = DADDU : (regno, regno, regno)
-
-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)
- }
-
-/* DADDI Doubleword Add Immediate
- reg, reg, imm with possible exception */
-
-union clause ast = DADDI : (regno, regno, bits(16))
-
-function clause decode (0b011000 @ rs : regno @ rt : regno @ imm : imm16) =
- Some(DADDI(rs, rt, imm))
-
-function clause execute (DADDI (rs, rt, imm)) =
- {
- let sum65 : bits(65) = EXTS(rGPR(rs)) + EXTS(imm) in
- {
- if (sum65[64] != sum65[63]) then
- (SignalException(Ov))
- else
- wGPR(rt) = sum65[63..0]
- }
- }
-
-/* DADD Doubleword Add
- reg, reg, reg with possible exception */
-
-union clause ast = DADD : (regno, regno, regno)
-
-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 sum65 : bits(65) = EXTS(rGPR(rs)) + EXTS(rGPR(rt)) in
- {
- if sum65[64] != sum65[63] then
- (SignalException(Ov))
- else
- wGPR(rd) = sum65[63..0]
- }
- }
-
-/* ADD 32-bit add -- reg, reg, reg with possible undefined behaviour or exception */
-
-union clause ast = ADD : (regno, regno, regno)
-
-function clause decode (0b000000 @ rs : regno @ rt : regno @ rd : regno @ 0b00000 @ 0b100000) =
- Some(ADD(rs, rt, rd))
-
-function clause execute (ADD(rs, rt, rd)) =
- {
- opA : bits(64) = rGPR(rs);
- opB : bits(64) = rGPR(rt);
- if NotWordVal(opA) | NotWordVal(opB) then
- wGPR(rd) = undefined /* XXX could exit instead */
- else
- let sum33 : bits(33) = EXTS(opA[31 .. 0]) + EXTS(opB[31 .. 0])in
- if sum33[32] != sum33[31] then
- (SignalException(Ov))
- else
- wGPR(rd) = EXTS(sum33[31..0])
- }
-
-/* ADDI 32-bit add immediate -- reg, reg, imm with possible undefined behaviour or exception */
-
-union clause ast = ADDI : (regno, regno, bits(16))
-
-function clause decode (0b001000 @ rs : regno @ rt : regno @ imm : imm16) =
- Some(ADDI(rs, rt, imm))
-
-function clause execute (ADDI(rs, rt, imm)) =
- {
- opA = rGPR(rs);
- if NotWordVal(opA) then
- wGPR(rt) = undefined /* XXX could exit instead */
- else
- let sum33 : bits(33) = EXTS(opA[31 .. 0]) + EXTS(imm) in
- if sum33[32] != sum33[31] then
- (SignalException(Ov))
- else
- wGPR(rt) = EXTS(sum33[31..0])
- }
-
-/* ADDU 32-bit add immediate -- reg, reg, reg with possible undefined behaviour */
-
-union clause ast = ADDU : (regno, regno, regno)
-
-function clause decode (0b000000 @ rs : regno @ rt : regno @ rd : regno @ 0b00000 @ 0b100001) =
- Some(ADDU(rs, rt, rd))
-
-function clause execute (ADDU(rs, rt, rd)) =
- {
- opA = rGPR(rs);
- opB = rGPR(rt);
- if NotWordVal(opA) | NotWordVal(opB) then
- wGPR(rd) = undefined
- else
- wGPR(rd) = EXTS(opA[31..0] + opB[31..0])
- }
-
-
-/* ADDIU 32-bit add immediate -- reg, reg, imm with possible undefined behaviour */
-
-union clause ast = ADDIU : (regno, regno, bits(16))
-
-function clause decode (0b001001 @ rs : regno @ rt : regno @ imm : imm16) =
- Some(ADDIU(rs, rt, imm))
-
-function clause execute (ADDIU(rs, rt, imm)) =
- {
- opA = rGPR(rs);
- if NotWordVal(opA) then
- wGPR(rt) = undefined /* XXX could exit instead */
- else
- wGPR(rt) = EXTS((opA[31 .. 0]) + EXTS(imm))
- }
-
-/**************************************************************************************/
-/* [D]SUB[U] various forms of SUB */
-/**************************************************************************************/
-
-/* DSUBU doubleword subtract 'unsigned' reg, reg, reg */
-
-union clause ast = DSUBU : (regno, regno, regno)
-
-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)
- }
-
-/* DSUB reg, reg, reg with possible exception */
-
-union clause ast = DSUB : (regno, regno, regno)
-
-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 temp65 : bits(65) = EXTS(rGPR(rs)) - EXTS(rGPR(rt)) in
- {
- if temp65[64] != temp65[63] then
- (SignalException(Ov))
- else
- wGPR(rd) = temp65[63..0]
- }
- }
-
-/* SUB 32-bit sub -- reg, reg, reg with possible undefined behaviour or exception */
-
-union clause ast = SUB : (regno, regno, regno)
-
-function clause decode (0b000000 @ rs : regno @ rt : regno @ rd : regno @ 0b00000 @ 0b100010) =
- Some(SUB(rs, rt, rd))
-
-function clause execute (SUB(rs, rt, rd)) =
- {
- opA = rGPR(rs);
- opB = rGPR(rt);
- if NotWordVal(opA) | NotWordVal(opB) then
- wGPR(rd) = undefined /* XXX could instead */
- else
- 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])
- }
-
-/* SUBU 32-bit 'unsigned' sub -- reg, reg, reg with possible undefined behaviour */
-
-union clause ast = SUBU : (regno, regno, regno)
-function clause decode (0b000000 @ rs : regno @ rt : regno @ rd : regno @ 0b00000 @ 0b100011) =
- Some(SUBU(rs, rt, rd))
-
-function clause execute (SUBU(rs, rt, rd)) =
- {
- opA = rGPR(rs);
- opB = rGPR(rt);
- if NotWordVal(opA) | NotWordVal(opB) then
- wGPR(rd) = undefined
- else
- wGPR(rd) = EXTS(opA[31..0] - opB[31..0])
- }
-
-/**************************************************************************************/
-/* Logical bitwise operations */
-/**************************************************************************************/
-
-/* AND reg, reg, reg */
-
-union clause ast = AND : (regno, regno, regno)
-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))
- }
-
-/* ANDI reg, reg, imm */
-
-union clause ast = ANDI : (regno, regno, bits(16))
-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))
- }
-
-/* OR reg, reg, reg */
-
-union clause ast = OR : (regno, regno, regno)
-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))
- }
-
-/* ORI reg, reg, imm */
-
-union clause ast = ORI : (regno, regno, bits(16))
-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))
- }
-
-/* NOR reg, reg, reg */
-
-union clause ast = NOR : (regno, regno, regno)
-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))
- }
-
-/* XOR reg, reg, reg */
-
-union clause ast = XOR : (regno, regno, regno)
-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))
- }
-
-/* XORI reg, reg, imm */
-union clause ast = XORI : (regno, regno, bits(16))
-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))
- }
-
-/* LUI reg, imm 32-bit load immediate into upper 16 bits */
-union clause ast = LUI : (regno, imm16)
-function clause decode (0b001111 @ 0b00000 @ rt : regno @ imm : imm16) =
- Some(LUI(rt, imm))
-function clause execute (LUI (rt, imm)) =
- {
- wGPR(rt) = EXTS(imm @ 0x0000)
- }
-
-/**************************************************************************************/
-/* 64-bit shift operations */
-/**************************************************************************************/
-
-/* DSLL reg, reg, imm5 */
-
-union clause ast = DSLL : (regno, regno, regno)
-function clause decode (0b000000 @ 0b00000 @ rt : regno @ rd : regno @ sa : bits(5) @ 0b111000) =
- Some(DSLL(rt, rd, sa))
-function clause execute (DSLL (rt, rd, sa)) =
- {
-
- wGPR(rd) = (rGPR(rt) << sa)
- }
-
-/* DSLL32 reg, reg, imm5 */
-
-union clause ast = DSLL32 : (regno, regno, regno)
-function clause decode (0b000000 @ 0b00000 @ rt : regno @ rd : regno @ sa : bits(5) @ 0b111100) =
- Some(DSLL32(rt, rd, sa))
-function clause execute (DSLL32 (rt, rd, sa)) =
- {
- wGPR(rd) = (rGPR(rt) << (0b1 @ sa))
- }
-
-/* DSLLV reg, reg, reg */
-
-union clause ast = DSLLV : (regno, regno, regno)
-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]))
- }
-
-/* DSRA arithmetic shift duplicating sign bit - reg, reg, imm5 */
-
-union clause ast = DSRA : (regno, regno, regno)
-function clause decode (0b000000 @ 0b00000 @ rt : regno @ rd : regno @ sa : bits(5) @ 0b111011) =
- Some(DSRA(rt, rd, sa))
-function clause execute (DSRA (rt, rd, sa)) =
- {
- temp = rGPR(rt);
- wGPR(rd) = temp >>_s sa
- }
-
-/* DSRA32 reg, reg, imm5 */
-
-union clause ast = DSRA32 : (regno, regno, regno)
-function clause decode (0b000000 @ 0b00000 @ rt : regno @ rd : regno @ sa : bits(5) @ 0b111111) =
- Some(DSRA32(rt, rd, sa))
-function clause execute (DSRA32 (rt, rd, sa)) =
- {
- temp = rGPR(rt);
- sa32 = 0b1 @ sa; /* sa+32 */
- wGPR(rd) = temp >>_s sa32
- }
-
-/* DSRAV reg, reg, reg */
-union clause ast = DSRAV : (regno, regno, regno)
-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) = temp >>_s sa
- }
-
-/* DSRL shift right logical - reg, reg, imm5 */
-
-union clause ast = DSRL : (regno, regno, regno)
-function clause decode (0b000000 @ 0b00000 @ rt : regno @ rd : regno @ sa : bits(5) @ 0b111010) =
- Some(DSRL(rt, rd, sa))
-function clause execute (DSRL (rt, rd, sa)) =
- {
- temp = rGPR(rt);
- wGPR(rd) = temp >> sa;
- }
-
-/* DSRL32 reg, reg, imm5 */
-
-union clause ast = DSRL32 : (regno, regno, regno)
-function clause decode (0b000000 @ 0b00000 @ rt : regno @ rd : regno @ sa : bits(5) @ 0b111110) =
- Some(DSRL32(rt, rd, sa))
-function clause execute (DSRL32 (rt, rd, sa)) =
- {
- temp = rGPR(rt);
- sa32 = 0b1 @ sa; /* sa+32 */
- wGPR(rd) = temp >> sa32;
- }
-
-/* DSRLV reg, reg, reg */
-
-union clause ast = DSRLV : (regno, regno, regno)
-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) = temp >> sa;
- }
-
-/**************************************************************************************/
-/* 32-bit shift operations */
-/**************************************************************************************/
-
-/* SLL 32-bit shift left */
-
-union clause ast = SLL : (regno, regno, regno)
-function clause decode (0b000000 @ 0b00000 @ rt : regno @ rd : regno @ sa : regno @ 0b000000) =
- Some(SLL(rt, rd, sa))
-function clause execute (SLL(rt, rd, sa)) =
- {
- rt32 = rGPR(rt)[31..0];
- wGPR(rd) = EXTS(rt32 << sa);
- }
-
-/* SLLV 32-bit shift left variable */
-
-union clause ast = SLLV : (regno, regno, regno)
-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];
- rt32 = rGPR(rt)[31..0];
- wGPR(rd) = EXTS(rt32 << sa)
- }
-
-/* SRA 32-bit arithmetic shift right */
-
-union clause ast = SRA : (regno, regno, regno)
-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);
- if (NotWordVal(temp)) then
- wGPR(rd) = undefined
- else {
- rt32 = temp[31..0];
- wGPR(rd) = EXTS(rt32 >>_s sa);
- }
- }
-
-/* SRAV 32-bit arithmetic shift right variable */
-
-union clause ast = SRAV : (regno, regno, regno)
-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];
- if (NotWordVal(temp)) then
- wGPR(rd) = undefined
- else {
- rt32 = temp[31..0];
- wGPR(rd) = EXTS(rt32 >>_s sa)
- }
- }
-
-/* SRL 32-bit shift right */
-
-union clause ast = SRL : (regno, regno, regno)
-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);
- if (NotWordVal(temp)) then
- wGPR(rd) = undefined
- else {
- rt32 = temp[31..0];
- wGPR(rd) = EXTS(rt32 >> sa);
- }
- }
-
-/* SRLV 32-bit shift right variable */
-
-union clause ast = SRLV : (regno, regno, regno)
-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];
- if (NotWordVal(temp)) then
- wGPR(rd) = undefined
- else {
- rt32 = temp[31..0];
- wGPR(rd) = EXTS(rt32 >> sa);
- }
- }
-
-/**************************************************************************************/
-/* set less than / conditional move */
-/**************************************************************************************/
-
-/* SLT set if less than (signed) */
-
-union clause ast = SLT : (regno, regno, regno)
-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) = EXTZ(if (rGPR(rs) <_s rGPR(rt)) then 0b1 else 0b0)
- }
-
-/* SLT set if less than immediate (signed) */
-
-union clause ast = SLTI : (regno, regno, bits(16))
-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) = EXTZ(if (rs_val < imm_val) then 0b1 else 0b0)
- }
-
-/* SLTU set if less than unsigned */
-
-union clause ast = SLTU : (regno, regno, regno)
-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 = rGPR(rs) in
- let rt_val = rGPR(rt) in
- wGPR(rd) = EXTZ(if (rs_val <_u rt_val) then 0b1 else 0b0)
- }
-
-/* SLTIU set if less than immediate unsigned */
-
-union clause ast = SLTIU : (regno, regno, bits(16))
-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 = rGPR(rs) in
- let immext : bits(64) = EXTS(imm) in /* NB defined to sign extend here even though comparison is unsigned! */
- wGPR(rt) = EXTZ(if (rs_val <_u immext) then 0b1 else 0b0)
- }
-
-/* MOVN move if non-zero */
-
-union clause ast = MOVN : (regno, regno, regno)
-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)
- }
-
-/* MOVZ move if zero */
-
-union clause ast = MOVZ : (regno, regno, regno)
-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)
- }
-
-/******************************************************************************/
-/* MUL/DIV instructions */
-/******************************************************************************/
-
-/* MFHI move from HI register */
-union clause ast = MFHI : regno
-function clause decode (0b000000 @ 0b0000000000 @ rd : regno @ 0b00000 @ 0b010000) =
- Some(MFHI(rd))
-function clause execute (MFHI(rd)) =
- {
- wGPR(rd) = HI
- }
-
-/* MFLO move from LO register */
-union clause ast = MFLO : regno
-function clause decode (0b000000 @ 0b0000000000 @ rd : regno @ 0b00000 @ 0b010010) =
- Some(MFLO(rd))
-function clause execute (MFLO(rd)) =
- {
- wGPR(rd) = LO
- }
-
-/* MTHI move to HI register */
-union clause ast = MTHI : regno
-function clause decode (0b000000 @ rs : regno @ 0b000000000000000 @ 0b010001) =
- Some(MTHI(rs))
-function clause execute (MTHI(rs)) =
- {
- HI = rGPR(rs)
- }
-
-/* MTLO move to LO register */
-union clause ast = MTLO : regno
-function clause decode (0b000000 @ rs : regno @ 0b000000000000000 @ 0b010011) =
- Some(MTLO(rs))
-function clause execute (MTLO(rs)) =
- {
- LO = rGPR(rs)
- }
-
-/* MUL 32-bit multiply into GPR */
-union clause ast = MUL : (regno, regno, regno)
-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);
- result : bits(64) = 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
- (potentially) context switch so just leave them alone
- HI = undefined;
- LO = undefined;
- */
- }
-
-/* MULT 32-bit multiply into HI/LO */
-union clause ast = MULT : (regno, regno)
-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);
- result : bits(64) = if (NotWordVal(rsVal) | NotWordVal(rtVal)) then
- undefined
- else
- (rsVal[31..0]) *_s (rtVal[31..0]);
- HI = EXTS(result[63..32]);
- LO = EXTS(result[31..0]);
- }
-
-/* MULTU 32-bit unsignedm rultiply into HI/LO */
-union clause ast = MULTU : (regno, regno)
-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);
- result : bits(64) = if (NotWordVal(rsVal) | NotWordVal(rtVal)) then
- undefined
- else
- (rsVal[31..0]) *_u (rtVal[31..0]);
- HI = EXTS(result[63..32]);
- LO = EXTS(result[31..0]);
- }
-
-/* DMULT 64-bit multiply into HI/LO */
-union clause ast = DMULT : (regno, regno)
-function clause decode (0b000000 @ rs : regno @ rt : regno @ 0b00000 @ 0b00000 @ 0b011100) =
- Some(DMULT(rs, rt))
-function clause execute (DMULT(rs, rt)) =
- {
- result = rGPR(rs) *_s rGPR(rt);
- HI = (result[127..64]);
- LO = (result[63..0]);
- }
-
-/* DMULTU 64-bit unsigned multiply into HI/LO */
-union clause ast = DMULTU : (regno, regno)
-function clause decode (0b000000 @ rs : regno @ rt : regno @ 0b00000 @ 0b00000 @ 0b011101) =
- Some(DMULTU(rs, rt))
-function clause execute (DMULTU(rs, rt)) =
- {
- result = rGPR(rs) *_u rGPR(rt);
- HI = (result[127..64]);
- LO = (result[63..0]);
- }
-
-/* MADD 32-bit signed multiply and add into HI/LO */
-union clause ast = MADD : (regno, regno)
-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);
- mul_result : bits(64) = if (NotWordVal(rsVal) | NotWordVal(rtVal)) then
- undefined
- else
- rsVal[31..0] *_s rtVal[31..0];
- 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 */
-union clause ast = MADDU : (regno, regno)
-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);
- mul_result : bits(64) = if (NotWordVal(rsVal) | NotWordVal(rtVal)) then
- undefined
- else
- rsVal[31..0] *_u rtVal[31..0];
- 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 */
-union clause ast = MSUB : (regno, regno)
-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);
- mul_result : bits(64) = if (NotWordVal(rsVal) | NotWordVal(rtVal)) then
- undefined
- else
- rsVal[31..0] *_s rtVal[31..0];
- 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 */
-union clause ast = MSUBU : (regno, regno)
-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);
- mul_result : bits(64) = if (NotWordVal(rsVal) | NotWordVal(rtVal)) then
- undefined
- else
- rsVal[31..0] *_u rtVal[31..0];
- 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 */
-union clause ast = DIV : (regno, regno)
-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 (q, r) =
- if (NotWordVal(rsVal) | NotWordVal(rtVal) | (rtVal == 0x0000000000000000)) then
- (undefined : bits(32), undefined : bits(32))
- else
- let si = signed((rsVal[31..0])) in
- let ti = signed((rtVal[31..0])) in
- let qi = quot_round_zero(si, ti) in
- let ri = si - (ti*qi) in
- (to_bits(32, qi), to_bits(32, ri))
- in
- {
- HI = EXTS(r);
- LO = EXTS(q);
- }
- }
-
-/* DIVU 32-bit unsigned divide into HI/LO */
-union clause ast = DIVU : (regno, regno)
-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 (q, r) =
- if (NotWordVal(rsVal) | NotWordVal(rtVal) | rtVal == 0x0000000000000000) then
- (undefined : bits(32), undefined : bits(32))
- else
- let si = unsigned(rsVal[31..0]) in
- let ti = unsigned(rtVal[31..0]) in
- let qi = quot_round_zero(si, ti) in
- let ri = rem_round_zero(si, ti) in
- (to_bits(32, qi), to_bits(32, ri))
- in
- {
- HI = EXTS(r);
- LO = EXTS(q);
- }
- }
-
-/* DDIV 64-bit divide into HI/LO */
-union clause ast = DDIV : (regno, regno)
-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 (q , r) =
- if (rtVal == 0)
- then (undefined : bits(64), undefined : bits(64))
- else
- let qi = quot_round_zero(rsVal, rtVal) in
- let ri = (rsVal - (qi * rtVal)) in
- (to_bits(64, qi), to_bits(64, ri)) in
- {
- LO = q;
- HI = r;
- }
- }
-
-/* DDIV 64-bit divide into HI/LO */
-union clause ast = DDIVU : (regno, regno)
-function clause decode (0b000000 @ rs : regno @ rt : regno @ 0b00000 @ 0b00000 @ 0b011111) =
- Some(DDIVU(rs, rt))
-function clause execute (DDIVU(rs, rt)) =
- {
- rsVal = unsigned(rGPR(rs));
- rtVal = unsigned(rGPR(rt));
- let (q, r) =
- if (rtVal == 0)
- then (undefined : bits(64), undefined : bits(64))
- else
- let qi = quot_round_zero(rsVal, rtVal) in
- let ri = rem_round_zero(rsVal, rtVal) in
- (to_bits(64, qi), to_bits(64, ri)) in
- {
- LO = q;
- HI = r;
- }
- }
-
-/**************************************************************************************/
-/* Jump instructions -- unconditional branches */
-/**************************************************************************************/
-
-/* J - jump, the simplest control flow instruction, with branch delay slot */
-union clause ast = J : bits(26)
-function clause decode (0b000010 @ offset : bits(26)) =
- Some(J(offset))
-function clause execute (J(offset)) =
- {
- delayedPC = (PC + 4)[63..28] @ offset @ 0b00;
- branchPending = 0b1
- }
-
-/* JAL - jump and link */
-union clause ast = JAL : bits(26)
-function clause decode (0b000011 @ offset : bits(26)) =
- Some(JAL(offset))
-function clause execute (JAL(offset)) =
- {
- delayedPC = (PC + 4)[63..28] @ offset @ 0b00;
- branchPending = 0b1;
- wGPR(0b11111) = PC + 8;
- }
-
-/* JR -- jump via register */
-union clause ast = JR : regno
-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 = 0b1;
- }
-
-/* JALR -- jump via register with link */
-union clause ast = JALR : (regno, regno)
-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 = 0b1;
- wGPR(rd) = PC + 8;
- }
-
-/**************************************************************************************/
-/* B[N]EQ[L] - branch on (not) equal (likely) */
-/* Conditional branch instructions with two register operands */
-/**************************************************************************************/
-
-union clause ast = BEQ : (regno, regno, imm16, bool, bool)
-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 offset : bits(64) = (EXTS(imm @ 0b00) + 4) in
- delayedPC = PC + offset;
- branchPending = 0b1;
- }
- else
- {
- if (likely) then
- 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 */
-/**************************************************************************************/
-
-union clause ast = BCMPZ : (regno, imm16, Comparison, bool, bool)
-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)) =
- {
- linkVal = PC + 8;
- regVal = rGPR(rs);
- condition = compare(cmp, regVal, EXTZ(0b0));
- if (condition) then
- {
- let offset : bits(64) = (EXTS(imm @ 0b00) + 4) in
- delayedPC = PC + offset;
- branchPending = 0b1;
- }
- else if (likely) then
- {
- nextPC = PC + 8 /* skip branch delay */
- };
- if (link) then
- wGPR(0b11111) = linkVal
- }
-
-/**************************************************************************************/
-/* SYSCALL/BREAK/WAIT/Trap */
-/**************************************************************************************/
-
-/* Co-opt syscall 0xfffff for use as thread start in pccmem */
-union clause ast = SYSCALL_THREAD_START : unit
-function clause decode (0b000000 @ 0xfffff @ 0b001100) =
- Some(SYSCALL_THREAD_START())
-function clause execute (SYSCALL_THREAD_START()) = ()
-
-
-/* fake stop fetching instruction for ppcmem, execute doesn't do anything,
- decode never produces it */
-
-union clause ast = ImplementationDefinedStopFetching : unit
-function clause execute (ImplementationDefinedStopFetching()) = ()
-
-
-union clause ast = SYSCALL : unit
-function clause decode (0b000000 @ code : bits(20) @ 0b001100) =
- Some(SYSCALL()) /* code is ignored */
-function clause execute (SYSCALL()) =
- {
- (SignalException(Sys))
- }
-
-/* BREAK is identical to SYSCALL exception for the exception raised */
-union clause ast = BREAK : unit
-function clause decode (0b000000 @ code : bits(20) @ 0b001101) =
- Some(BREAK()) /* code is ignored */
-function clause execute (BREAK()) =
- {
- (SignalException(Bp))
- }
-
-/* Accept WAIT as a NOP */
-union clause ast = WAIT : unit
-function clause decode (0b010000 @ 0x80000 @ 0b100000) =
- Some(WAIT()) /* we only accept code == 0 */
-function clause execute (WAIT()) = {
- nextPC = PC;
-}
-
-/* Trap instructions with two register operands */
-union clause ast = TRAPREG : (regno, regno, Comparison)
-function clause decode (0b000000 @ rs : regno @ rt : regno @ code : bits(10) @ 0b110000) =
- Some(TRAPREG(rs, rt, GE)) /* TGE */
-function clause decode (0b000000 @ rs : regno @ rt : regno @ code : bits(10) @ 0b110001) =
- Some(TRAPREG(rs, rt, GEU)) /* TGEU */
-function clause decode (0b000000 @ rs : regno @ rt : regno @ code : bits(10) @ 0b110010) =
- Some(TRAPREG(rs, rt, LT)) /* TLT */
-function clause decode (0b000000 @ rs : regno @ rt : regno @ code : bits(10) @ 0b110011) =
- Some(TRAPREG(rs, rt, LTU)) /* TLTU */
-function clause decode (0b000000 @ rs : regno @ rt : regno @ code : bits(10) @ 0b110100) =
- Some(TRAPREG(rs, rt, EQ)) /* TEQ */
-function clause decode (0b000000 @ rs : regno @ rt : regno @ code : bits(10) @ 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);
- if (condition) then
- (SignalException(Tr))
- }
-
-
-/* Trap instructions with one register and one immediate operand */
-union clause ast = TRAPIMM : (regno, imm16, Comparison)
-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);
- imm_val : bits(64) = EXTS(imm);
- condition = compare(cmp, rs_val, imm_val);
- if (condition) then
- (SignalException(Tr))
- }
-
-/**************************************************************************************/
-/* Load instructions -- various width/signs */
-/**************************************************************************************/
-
-union clause ast = Load : (WordType, bool, bool, regno, regno, imm16)
-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, 'sz <= 64 . (bits('sz), bool) -> bits(64) effect pure
-function extendLoad(memResult, sign) = {
- if (sign) then
- EXTS(memResult)
- else
- EXTZ(memResult)
-}
-
-function clause execute (Load(width, sign, linked, base, rt, offset)) =
- {
- vAddr : bits(64) = addrWrapper(EXTS(offset) + rGPR(base), LoadData, width);
- if ~ (isAddressAligned(vAddr, width)) then
- (SignalExceptionBadAddr(AdEL, vAddr)) /* unaligned access */
- else
- let pAddr = (TLBTranslate(vAddr, LoadData)) in
- {
- memResult : bits(64) = if (linked) then
- {
- CP0LLBit = 0b1;
- CP0LLAddr = pAddr;
- match width {
- B => extendLoad(MEMr_reserve_wrapper(pAddr, 1), sign),
- H => extendLoad(MEMr_reserve_wrapper(pAddr, 2), sign),
- W => extendLoad(MEMr_reserve_wrapper(pAddr, 4), sign),
- D => extendLoad(MEMr_reserve_wrapper(pAddr, 8), sign)
- }
- }
- else
- {
- match width {
- B => extendLoad(MEMr_wrapper(pAddr, 1), sign),
- H => extendLoad(MEMr_wrapper(pAddr, 2), sign),
- W => extendLoad(MEMr_wrapper(pAddr, 4), sign),
- D => extendLoad(MEMr_wrapper(pAddr, 8), sign)
- }
- };
- wGPR(rt) = memResult
- }
- }
-
-/**************************************************************************************/
-/* Store instructions -- various widths */
-/**************************************************************************************/
-
-union clause ast = Store : (WordType, bool, regno, regno, imm16)
-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)) =
- {
- vAddr : bits(64) = addrWrapper(EXTS(offset) + rGPR(base), StoreData, width);
- rt_val = rGPR(rt);
- if ~ (isAddressAligned(vAddr, width)) then
- (SignalExceptionBadAddr(AdES, vAddr)) /* unaligned access */
- else
- let pAddr = (TLBTranslate(vAddr, StoreData)) in
- {
- if (conditional) then
- {
- success : bool = if (CP0LLBit[0]) then match width
- {
- 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(success)
- }
- else
- match width
- {
- 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) */
-
-union clause ast = LWL : (regno, regno, bits(16))
-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 */
- 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);
- result : bits(32) = match vAddr[1..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]
- };
- wGPR(rt) = EXTS(result);
- }
- }
-union clause ast = LWR : (regno, regno, bits(16))
-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 */
- 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);
- result : bits(32) = match vAddr[1..0]
- {
- 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
- };
- wGPR(rt) = EXTS(result)
- }
- }
-
-/* SWL - Store word left */
-union clause ast = SWL : (regno, regno, bits(16))
-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 */
- vAddr = addrWrapper(EXTS(offset) + rGPR(base), StoreData, W);
- let pAddr = TLBTranslate(vAddr, StoreData) in
- {
- reg_val = rGPR(rt);
- match vAddr[1..0]
- {
- 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 clause ast = SWR : (regno, regno, bits(16))
-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 */
- vAddr = addrWrapper(EXTS(offset) + rGPR(base), StoreData, W);
- let pAddr = TLBTranslate(vAddr, StoreData) in
- {
- wordAddr = pAddr[63..2] @ 0b00;
- reg_val = rGPR(rt);
- match vAddr[1..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 */
-union clause ast = LDL : (regno, regno, bits(16))
-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 */
- 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) = match vAddr[2..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 */
-union clause ast = LDR : (regno, regno, bits(16))
-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 */
- 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) = match vAddr[2..0]
- {
- 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 */
-union clause ast = SDL : (regno, regno, bits(16))
-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 */
- vAddr = addrWrapper(EXTS(offset) + rGPR(base), StoreData, D);
- let pAddr = TLBTranslate(vAddr, StoreData) in
- {
- reg_val = rGPR(rt);
- match vAddr[2..0]
- {
- 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 */
-union clause ast = SDR : (regno, regno, bits(16))
-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 */
- vAddr = addrWrapper(EXTS(offset) + rGPR(base), StoreData, D);
- let pAddr = TLBTranslate(vAddr, StoreData) in
- {
- reg_val = rGPR(rt);
- wordAddr = pAddr[63..3] @ 0b000;
- match vAddr[2..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 */
-
-union clause ast = CACHE : (regno, regno, bits(16))
-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 */
-
-/* PREF - prefetching into (non-existent) caches */
-
-union clause ast = PREF : (regno, regno, bits(16))
-function clause decode (0b110011 @ base : regno @ op : regno @ imm : imm16) =
- Some(PREF(base, op, imm))
-function clause execute (PREF(base, op, imm)) =
- () /* XXX NOP */
-
-
-/* SYNC - Memory barrier */
-union clause ast = SYNC : unit
-function clause decode (0b000000 @ 0b00000 @ 0b00000 @ 0b00000 @ stype : regno @ 0b001111) =
- Some(SYNC()) /* stype is currently ignored */
-function clause execute(SYNC()) =
- MEM_sync()
-
-union clause ast = MFC0 : (regno, regno, bits(3), bool)
-function clause decode (0b010000 @ 0b00000 @ rt : regno @ rd : regno @ 0b00000000 @ sel : bits(3)) =
- Some(MFC0(rt, rd, sel, false)) /* MFC0 */
-function clause decode (0b010000 @ 0b00001 @ rt : regno @ rd : regno @ 0b00000000 @ sel : bits(3)) =
- Some(MFC0(rt, rd, sel, true)) /* DMFC0 */
-function clause execute (MFC0(rt, rd, sel, double)) = {
- checkCP0Access();
- let result : bits(64) = match (rd, sel)
- {
- (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.bits(), /* 2, TLB EntryLo0 */
- (0b00011,0b000) => TLBEntryLo1.bits(), /* 3, TLB EntryLo1 */
- (0b00100,0b000) => TLBContext.bits(), /* 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) => EXTZ(0b0), /* 8, BadInstr reg XXX TODO */
- (0b01001,0b000) => EXTZ(CP0Count), /* 9, Count reg */
- (0b01010,0b000) => TLBEntryHi.bits(),/* 10, TLB EntryHi */
- (0b01011,0b000) => EXTZ(CP0Compare), /* 11, Compare reg */
- (0b01100,0b000) => EXTZ(CP0Status.bits()), /* 12, Status reg */
- (0b01101,0b000) => EXTZ(CP0Cause.bits()), /* 13, Cause reg */
- (0b01110,0b000) => CP0EPC, /* 14, EPC */
- (0b01111,0b000) => EXTZ(0x00000400), /* 15, sel 0: PrID processor ID */
- (0b01111,0b110) => EXTZ(0b0), /* 15, sel 6: CHERI core ID */
- (0b01111,0b111) => EXTZ(0b0), /* 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),
- (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_bits(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) => EXTZ(0b0), /* 18, WatchLo */
- (0b10011,0b000) => EXTZ(0b0), /* 19, WatchHi */
- (0b10100,0b000) => TLBXContext.bits(), /* 20, XContext */
- (0b11110,0b000) => CP0ErrorEPC, /* 30, ErrorEPC */
- _ => (SignalException(ResI))
- } in
- wGPR(rt) = if (double) then result else EXTS(result[31..0])
-}
-
-/* simulator halt instruction "MTC0 rt, r23" (cheri specific behaviour) */
-union clause ast = HCF : unit
-function clause decode (0b010000 @ 0b00100 @ rt : regno @ 0b10111 @ 0b00000000000) =
- Some(HCF())
-
-function clause decode (0b010000 @ 0b00100 @ rt : regno @ 0b11010 @ 0b00000000000) =
- Some(HCF())
-
-function clause execute (HCF()) =
- () /* halt instruction actually executed by interpreter framework */
-
-union clause ast = MTC0 : (regno, regno, bits(3), bool)
-function clause decode (0b010000 @ 0b00100 @ rt : regno @ rd : regno @ 0b00000000 @ sel : bits(3)) =
- Some(MTC0(rt, rd, sel, false)) /* MTC0 */
-function clause decode (0b010000 @ 0b00101 @ rt : regno @ rd : regno @ 0b00000000 @ sel : bits(3)) =
- Some(MTC0(rt, rd, sel, true)) /* DMTC0 */
-function clause execute (MTC0(rt, rd, sel, double)) = {
- checkCP0Access();
- let reg_val = rGPR(rt) in
- match (rd, sel)
- {
- (0b00000,0b000) => TLBIndex = mask(reg_val), /* NB no write to TLBProbe */
- (0b00001,0b000) => (), /* TLBRandom is read only */
- (0b00010,0b000) => TLBEntryLo0->bits() = reg_val,
- (0b00011,0b000) => TLBEntryLo1->bits() = 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;
- },
- (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];
- },
- (0b01011,0b000) => { /* 11, sel 0: Compare reg */
- CP0Compare = reg_val[31..0];
- CP0Cause->IP() = CP0Cause.IP() & 0x7f; /* clear IP7 */
- },
- (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];
- },
- (0b01101,0b000) => { /* 13 Cause */
- CP0Cause->IV() = reg_val[23]; /* TODO special interrupt vector not implemeneted */
- let ip = CP0Cause.IP() in
- CP0Cause->IP() = ((ip[7..2]) @ (reg_val[9..8]));
- },
- (0b01110,0b000) => CP0EPC = reg_val, /* 14, EPC */
- (0b10000,0b000) => (), /* XXX ignore K0 cache config 16: Config0 */
- (0b10100,0b000) => TLBXContext->XPTEBase() = reg_val[63..33],
- (0b11110,0b000) => CP0ErrorEPC = reg_val, /* 30, ErrorEPC */
- _ => (SignalException(ResI))
- }
-}
-
-val TLBWriteEntry : TLBIndexT -> unit effect {rreg, wreg, escape}
-function TLBWriteEntry(idx) = {
- pagemask = TLBPageMask;
- match pagemask {
- 0x0000 => (),
- 0x0003 => (),
- 0x000f => (),
- 0x003f => (),
- 0x00ff => (),
- 0x03ff => (),
- 0x0fff => (),
- 0x3fff => (),
- 0xffff => (),
- _ => (SignalException(MCheck))
- };
- let i as atom(_) = unsigned(idx) in
- let entry = TLBEntries[i] in {
- entry.pagemask() = pagemask;
- entry.r() = TLBEntryHi.R();
- entry.vpn2() = TLBEntryHi.VPN2();
- entry.asid() = TLBEntryHi.ASID();
- entry.g() = ((TLBEntryLo0.G()) & (TLBEntryLo1.G()));
- entry.valid() = bitone;
- entry.caps0() = TLBEntryLo0.CapS();
- entry.capl0() = TLBEntryLo0.CapL();
- entry.pfn0() = TLBEntryLo0.PFN();
- entry.c0() = TLBEntryLo0.C();
- entry.d0() = TLBEntryLo0.D();
- entry.v0() = TLBEntryLo0.V();
- entry.caps1() = TLBEntryLo1.CapS();
- entry.capl1() = TLBEntryLo1.CapL();
- entry.pfn1() = TLBEntryLo1.PFN();
- entry.c1() = TLBEntryLo1.C();
- entry.d1() = TLBEntryLo1.D();
- entry.v1() = TLBEntryLo1.V();
- }
-}
-
-union clause ast = TLBWI : unit
-function clause decode (0b010000 @ 0b10000000000000000000 @ 0b000010) = Some(TLBWI() : ast)
-function clause execute (TLBWI()) = {
- checkCP0Access();
- TLBWriteEntry(TLBIndex);
-}
-
-union clause ast = TLBWR : unit
-function clause decode (0b010000 @ 0b10000000000000000000 @ 0b000110) = Some(TLBWR() : ast)
-function clause execute (TLBWR()) = {
- checkCP0Access();
- TLBWriteEntry(TLBRandom);
-}
-
-union clause ast = TLBR : unit
-function clause decode (0b010000 @ 0b10000000000000000000 @ 0b000001) = Some(TLBR() : ast)
-function clause execute (TLBR()) = {
- checkCP0Access();
- let i as atom(_) = unsigned(TLBIndex) in
- let entry = reg_deref(TLBEntries[i]) 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();
- }
-}
-
-union clause ast = TLBP : unit
-function clause decode (0b010000 @ 0b10000000000000000000 @ 0b001000) = Some(TLBP() : ast)
-function clause execute (TLBP()) = {
- checkCP0Access();
- let result = tlbSearch(TLBEntryHi.bits()) in
- match result {
- (Some(idx)) => {
- TLBProbe = [bitzero];
- TLBIndex = idx;
- },
- None() => {
- TLBProbe = [bitone];
- TLBIndex = 0b000000;
- }
- }
-}
-
-union clause ast = RDHWR : (regno, regno)
-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
- let haveAccessLevel : bool = accessLevel == Kernel in
- let haveCU0 : bool = bitone == (CP0Status.CU()[0]) in
- let rdi as atom(_) = unsigned(rd) in
- let haveHWREna : bool = bitone == (CP0HWREna[rdi]) in
- if ~(haveAccessLevel | haveCU0 | haveHWREna) then
- (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;
-}
-
-union clause ast = ERET : unit
-
-function clause decode (0b010000 @ 0b1 @ 0b0000000000000000000 @ 0b011000) =
- Some(ERET())
-function clause execute (ERET()) =
- {
- checkCP0Access();
- ERETHook();
- CP0LLBit = 0b0;
- if (CP0Status.ERL() == bitone) then
- {
- nextPC = CP0ErrorEPC;
- CP0Status->ERL() = 0b0;
- }
- else
- {
- nextPC = CP0EPC;
- CP0Status->EXL() = 0b0;
- }
- }
diff --git a/mips_new_tc/mips_prelude.sail b/mips_new_tc/mips_prelude.sail
deleted file mode 100644
index b4f09548..00000000
--- a/mips_new_tc/mips_prelude.sail
+++ /dev/null
@@ -1,620 +0,0 @@
-/*========================================================================*/
-/* */
-/* 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) */
-
-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,*/
-}
-
-bitfield TLBEntryLoReg : bits(64) = {
- CapS : 63,
- CapL : 62,
- PFN : 29.. 6,
- C : 5.. 3,
- D : 2,
- V : 1,
- G : 0,
-}
-
-bitfield TLBEntryHiReg : bits(64) = {
- R : 63.. 62,
- VPN2 : 39.. 13,
- ASID : 7.. 0,
-}
-
-bitfield ContextReg : bits(64) = {
- PTEBase : 63.. 23,
- BadVPN2 : 22.. 4,
- /*ZR : 3.. 0,*/
-}
-
-bitfield XContextReg : bits(64) = {
- XPTEBase : 63.. 33,
- XR : 32.. 31,
- XBadVPN2 : 30.. 4,
-}
-
-let TLBNumEntries = 64
-type TLBIndexT = (bits(6))
-let TLBIndexMax : TLBIndexT = 0b111111
-
-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)*/
-
-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 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 TLBEntry00 : TLBEntry
-register TLBEntry01 : TLBEntry
-register TLBEntry02 : TLBEntry
-register TLBEntry03 : TLBEntry
-register TLBEntry04 : TLBEntry
-register TLBEntry05 : TLBEntry
-register TLBEntry06 : TLBEntry
-register TLBEntry07 : TLBEntry
-register TLBEntry08 : TLBEntry
-register TLBEntry09 : TLBEntry
-register TLBEntry10 : TLBEntry
-register TLBEntry11 : TLBEntry
-register TLBEntry12 : TLBEntry
-register TLBEntry13 : TLBEntry
-register TLBEntry14 : TLBEntry
-register TLBEntry15 : TLBEntry
-register TLBEntry16 : TLBEntry
-register TLBEntry17 : TLBEntry
-register TLBEntry18 : TLBEntry
-register TLBEntry19 : TLBEntry
-register TLBEntry20 : TLBEntry
-register TLBEntry21 : TLBEntry
-register TLBEntry22 : TLBEntry
-register TLBEntry23 : TLBEntry
-register TLBEntry24 : TLBEntry
-register TLBEntry25 : TLBEntry
-register TLBEntry26 : TLBEntry
-register TLBEntry27 : TLBEntry
-register TLBEntry28 : TLBEntry
-register TLBEntry29 : TLBEntry
-register TLBEntry30 : TLBEntry
-register TLBEntry31 : TLBEntry
-register TLBEntry32 : TLBEntry
-register TLBEntry33 : TLBEntry
-register TLBEntry34 : TLBEntry
-register TLBEntry35 : TLBEntry
-register TLBEntry36 : TLBEntry
-register TLBEntry37 : TLBEntry
-register TLBEntry38 : TLBEntry
-register TLBEntry39 : TLBEntry
-register TLBEntry40 : TLBEntry
-register TLBEntry41 : TLBEntry
-register TLBEntry42 : TLBEntry
-register TLBEntry43 : TLBEntry
-register TLBEntry44 : TLBEntry
-register TLBEntry45 : TLBEntry
-register TLBEntry46 : TLBEntry
-register TLBEntry47 : TLBEntry
-register TLBEntry48 : TLBEntry
-register TLBEntry49 : TLBEntry
-register TLBEntry50 : TLBEntry
-register TLBEntry51 : TLBEntry
-register TLBEntry52 : TLBEntry
-register TLBEntry53 : TLBEntry
-register TLBEntry54 : TLBEntry
-register TLBEntry55 : TLBEntry
-register TLBEntry56 : TLBEntry
-register TLBEntry57 : TLBEntry
-register TLBEntry58 : TLBEntry
-register TLBEntry59 : TLBEntry
-register TLBEntry60 : TLBEntry
-register TLBEntry61 : TLBEntry
-register TLBEntry62 : TLBEntry
-register TLBEntry63 : TLBEntry
-
-let TLBEntries : vector(64, dec, register(TLBEntry)) = [
- ref TLBEntry63,
- ref TLBEntry62,
- ref TLBEntry61,
- ref TLBEntry60,
- ref TLBEntry59,
- ref TLBEntry58,
- ref TLBEntry57,
- ref TLBEntry56,
- ref TLBEntry55,
- ref TLBEntry54,
- ref TLBEntry53,
- ref TLBEntry52,
- ref TLBEntry51,
- ref TLBEntry50,
- ref TLBEntry49,
- ref TLBEntry48,
- ref TLBEntry47,
- ref TLBEntry46,
- ref TLBEntry45,
- ref TLBEntry44,
- ref TLBEntry43,
- ref TLBEntry42,
- ref TLBEntry41,
- ref TLBEntry40,
- ref TLBEntry39,
- ref TLBEntry38,
- ref TLBEntry37,
- ref TLBEntry36,
- ref TLBEntry35,
- ref TLBEntry34,
- ref TLBEntry33,
- ref TLBEntry32,
- ref TLBEntry31,
- ref TLBEntry30,
- ref TLBEntry29,
- ref TLBEntry28,
- ref TLBEntry27,
- ref TLBEntry26,
- ref TLBEntry25,
- ref TLBEntry24,
- ref TLBEntry23,
- ref TLBEntry22,
- ref TLBEntry21,
- ref TLBEntry20,
- ref TLBEntry19,
- ref TLBEntry18,
- ref TLBEntry17,
- ref TLBEntry16,
- ref TLBEntry15,
- ref TLBEntry14,
- ref TLBEntry13,
- ref TLBEntry12,
- ref TLBEntry11,
- ref TLBEntry10,
- ref TLBEntry09,
- ref TLBEntry08,
- ref TLBEntry07,
- ref TLBEntry06,
- ref TLBEntry05,
- ref TLBEntry04,
- ref TLBEntry03,
- ref TLBEntry02,
- ref TLBEntry01,
- ref TLBEntry00
-]
-
-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 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 NotWordVal (word) =
- (word[31] ^^ 32) != word[63..32]
-
-/* Read numbered GP reg. (r0 is always zero) */
-val rGPR : bits(5) -> bits(64) effect {rreg}
-function rGPR idx = {
- let i as atom(_) = unsigned(idx) in
- if i == 0 then 0x0000000000000000 else GPR[i]
-}
-
-/* Write numbered GP reg. (writes to r0 ignored) */
-val wGPR : (bits(5), bits(64)) -> unit effect {wreg}
-function wGPR (idx, v) = {
- let i as atom(_) = unsigned(idx) in
- if i == 0 then () else GPR[i] = v
-}
-
-val MEMr = {lem: "MEMr"} : forall 'n.
- ( bits(64) , atom('n) ) -> (bits(8 * 'n)) effect { rmem }
-val MEMr_reserve = {lem: "MEMr_reserve"} : forall 'n.
- ( bits(64) , atom('n) ) -> (bits(8 * 'n)) effect { rmem }
-val MEM_sync = {lem: "MEM_sync"} :
- unit -> unit effect { barr }
-
-val MEMea = {lem: "MEMea"} : forall 'n.
- ( bits(64) , atom('n)) -> unit effect { eamem }
-val MEMea_conditional = {lem: "MEMea_conditional"} : forall 'n.
- ( bits(64) , atom('n)) -> unit effect { eamem }
-val MEMval = {lem: "MEMval"} : forall 'n.
- ( bits(64) , atom('n), bits(8*'n)) -> unit effect { wmv }
-val MEMval_conditional = {lem: "MEMval_conditional"} : forall 'n.
- ( bits(64) , atom('n), bits(8*'n)) -> bool effect { wmv }
-
-/* Extern nops with effects, sometimes useful for faking effect */
-val skip_eamem = "skip" : unit -> unit effect {eamem}
-val skip_barr = "skip" : unit -> unit effect {barr}
-val skip_wreg = "skip" : unit -> unit effect {wreg}
-val skip_rreg = "skip" : unit -> unit effect {rreg}
-val skip_wmvt = "skip" : unit -> unit effect {wmvt}
-val skip_rmemt = "skip" : unit -> unit effect {rmemt}
-val skip_escape = "skip" : unit -> unit effect {escape}
-
-function MEMr (addr, size) = __MIPS_read(addr, size)
-function MEMr_reserve (addr, size) = __MIPS_read(addr, size)
-function MEM_sync () = skip_barr()
-
-function MEMea (addr, size) = skip_eamem()
-function MEMea_conditional (addr, size) = skip_eamem()
-function MEMval (addr, size, data) = __MIPS_write(addr, size, data)
-function MEMval_conditional (addr, size, data) = { __MIPS_write(addr, size, data); true }
-
-enum Exception =
-{
- 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 ExceptionCode (ex) : Exception -> bits(5)=
- let x : bits(8) = match ex
- {
- Interrupt => 0x00, /* Interrupt */
- TLBMod => 0x01, /* TLB modification exception */
- TLBL => 0x02, /* TLB exception (load or fetch) */
- TLBS => 0x03, /* TLB exception (store) */
- AdEL => 0x04, /* Address error (load or fetch) */
- AdES => 0x05, /* Address error (store) */
- Sys => 0x08, /* Syscall */
- Bp => 0x09, /* Breakpoint */
- ResI => 0x0a, /* Reserved instruction */
- CpU => 0x0b, /* Coprocessor Unusable */
- Ov => 0x0c, /* Arithmetic overflow */
- Tr => 0x0d, /* Trap */
- C2E => 0x12, /* C2E coprocessor 2 exception */
- C2Trap => 0x12, /* C2Trap maps to same exception code, different vector */
- XTLBRefillL => 0x02,
- XTLBRefillS => 0x03,
- XTLBInvL => 0x02,
- XTLBInvS => 0x03,
- MCheck => 0x18
- } in x[4..0]
-
-
-val SignalExceptionMIPS : forall ('o : Type) . (Exception, bits(64)) -> 'o effect {escape, rreg, wreg}
-function SignalExceptionMIPS (ex, kccBase) =
- {
- /* Only update EPC and BD if not already in EXL mode */
- if (~ (CP0Status.EXL())) then
- {
- if (inBranchDelay[0]) then
- {
- CP0EPC = PC - 4;
- CP0Cause->BD() = 0b1;
- }
- else
- {
- CP0EPC = PC;
- CP0Cause->BD() = 0b0;
- }
- };
-
- /* 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 */
- else if ((ex == XTLBRefillL) | (ex == XTLBRefillS)) then
- 0x080
- else if (ex == C2Trap) then
- 0x280 /* Special vector for CHERI traps */
- else
- 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 = vectorBase + EXTS(vectorOffset) - kccBase;
- CP0Cause->ExcCode() = ExceptionCode(ex);
- CP0Status->EXL() = 0b1;
- throw (ISAException());
- }
-
-/* Defined either in mips_wrappers (directly calling SignalExceptionMIPS) or in cheri_prelude_common (cheri things plus above) */
-val SignalException : forall ('o : Type) . Exception -> 'o effect {escape, rreg, wreg}
-
-val SignalExceptionBadAddr : forall ('o : Type) . (Exception, bits(64)) -> 'o effect {escape, rreg, wreg}
-function SignalExceptionBadAddr(ex, badAddr) =
- {
- CP0BadVAddr = badAddr;
- SignalException(ex);
- }
-
-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->XBadVPN2()= (badAddr[39..13]);
- TLBXContext->XR() = (badAddr[63..62]);
- TLBEntryHi->R() = (badAddr[63..62]);
- TLBEntryHi->VPN2() = (badAddr[39..13]);
- SignalException(ex);
-}
-
-enum MemAccessType = {Instruction, LoadData, StoreData}
-enum AccessLevel = {User, Supervisor, Kernel}
-
-function getAccessLevel() : unit -> AccessLevel=
- if ((CP0Status.EXL()) | (CP0Status.ERL())) then
- Kernel
- else match CP0Status.KSU()
- {
- 0b00 => Kernel,
- 0b01 => Supervisor,
- 0b10 => User,
- _ => User /* behaviour undefined, assume user */
- }
-
-val checkCP0Access : unit->unit effect{escape, rreg, wreg}
-function checkCP0Access () =
- {
- let accessLevel = getAccessLevel() in
- if ((accessLevel != Kernel) & (~(CP0Status.CU()[0]))) then
- {
- CP0Cause->CE() = 0b00;
- SignalException(CpU);
- }
- }
-
-val incrementCP0Count : unit -> unit effect {rreg,wreg,escape}
-function incrementCP0Count() = {
- TLBRandom = (if (TLBRandom == TLBWired)
- then (TLBIndexMax) else (TLBRandom - 1));
-
- CP0Count = (CP0Count + 1);
- if (CP0Count == CP0Compare) then {
- CP0Cause->IP() = CP0Cause.IP() | 0x80; /* IP7 is timer interrupt */
- };
-
- 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(Interrupt);
-}
-
-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 */
-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 */
-}
-
-val compare : (Comparison, bits(64), bits(64)) -> bool
-function compare (cmp, valA, valB) =
- match cmp {
- EQ => valA == valB,
- NE => valA != valB,
- GE => valA >=_s valB,
- GEU => valA >=_u valB,
- GT => valB <_s valA,
- LE => valB >=_s valA,
- LT => valA <_s valB,
- LTU => valA <_u valB
- }
-enum WordType = { B, H, W, D}
-
-val wordWidthBytes : WordType -> 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
- -- it is disabled in favour of BERI specific behaviour below.
-function bool isAddressAligned(addr, (WordType) wordType) =
- 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
- 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
- one capability. Capability load/stores are still naturally
- 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
-val isAddressAligned : (bits(64), WordType) -> bool
-function isAddressAligned (addr, wordType) =
- let a = unsigned(addr) in
- a / alignment_width == (a + wordWidthBytes(wordType) - 1) / alignment_width
-
-val reverse_endianness = "reverse_endianness" : forall 'W, 'W >= 1. bits(8 * 'W) -> bits(8 * 'W) effect pure
-
-/*
-function rec forall Nat 'W, 'W >= 1. bits(8 * 'W) reverse_endianness' (w, value) =
-{
- ([:8 * 'W:]) width = length(value);
- if width <= 8
- then value
- else value[7..0] : reverse_endianness'(w - 1, value[(width - 1) .. 8])
-}
-
-
-
-function rec forall Nat 'W, 'W >= 1. bits(8 * 'W) reverse_endianness ((bits(8 * 'W)) value) =
-{
- reverse_endianness'(sizeof 'W, value)
-}*/
-
-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 = UART_RVALID in
- let rdata = (bits(8 * 'n)) (mask(0x00000000 : UART_RDATA : rvalid : 0b0000000 : 0x0000)) in
- {
- UART_RVALID = [bitzero];
- rdata
- }
- }
- else if (addr == 0x000000007f000004) then
- mask(0x000000000004ffff) /* Always plenty of write space available and jtag activity */
- else
- reverse_endianness(MEMr(addr, size)) /* MEMr assumes little endian */ */
-
-val MEMr_reserve_wrapper : forall 'n, 1 <= 'n <= 8 . ( bits(64) , atom('n) ) -> (bits(8 * 'n)) effect { rmem }
-function MEMr_reserve_wrapper (addr , size) =
- reverse_endianness(MEMr_reserve(addr, size))
-
-
-function init_cp0_state () : unit -> unit = {
- CP0Status->BEV() = bitone;
-}
-
-val init_cp2_state : unit -> unit effect {wreg}
-val cp2_next_pc: unit -> unit effect {rreg, wreg}
-val dump_cp2_state : unit -> unit effect {rreg, escape}
diff --git a/mips_new_tc/mips_regfp.sail b/mips_new_tc/mips_regfp.sail
deleted file mode 100644
index 4bf96022..00000000
--- a/mips_new_tc/mips_regfp.sail
+++ /dev/null
@@ -1,455 +0,0 @@
-/*========================================================================*/
-/* */
-/* 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 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"
- ]
-
-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;
-
- switch instr {
- (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 offset : bits(64) = (EXTS(imm : 0b00) + 4) in
- Dia = DIAFP_concrete (PC + offset);
- }
- (SYSCALL_THREAD_START) => ()
-/*
-
- case (SYSCALL) =
- case (BREAK) =
- case (WAIT) = {
- case (TRAPREG(rs, rt, cmp)) =
- case (TRAPIMM(rs, imm, cmp)) =
-*/
- (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)) =
-*/
- (SYNC) => {
- iK = IK_barrier(Barrier_MIPS_SYNC);
- }
-/*
- case (MFC0(rt, rd, sel, double))
- case (HCF)
- case (MTC0(rt, rd, sel, double))
- case (TLBWI)
- case (TLBWR)
- case (TLBR)
- 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
deleted file mode 100644
index edce0657..00000000
--- a/mips_new_tc/mips_ri.sail
+++ /dev/null
@@ -1,42 +0,0 @@
-/*========================================================================*/
-/* */
-/* 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) */
-
-union clause ast = RI : unit
-function clause decode _ = Some(RI())
-function clause execute (RI()) =
- SignalException (ResI)
-
diff --git a/mips_new_tc/mips_tlb.sail b/mips_new_tc/mips_tlb.sail
deleted file mode 100644
index 741eb84c..00000000
--- a/mips_new_tc/mips_tlb.sail
+++ /dev/null
@@ -1,148 +0,0 @@
-/*========================================================================*/
-/* */
-/* 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 tlbEntryMatch : (bits(2), bits(27), bits(8), TLBEntry) -> bool effect pure
-function tlbEntryMatch(r, vpn2, asid, entry) =
- let entryValid = entry.valid() in
- let entryR = entry.r() in
- let entryMask = entry.pagemask() in
- let entryVPN = entry.vpn2() in
- let entryASID = entry.asid() in
- let entryG = entry.g() in
- let vpnMask : bits(27) = ~(EXTZ(entryMask)) in
- (entryValid &
- (r == entryR) &
- ((vpn2 & vpnMask) == ((entryVPN) & vpnMask)) &
- ((asid == (entryASID)) | (entryG)))
-
-val tlbSearch : bits(64) -> option(TLBIndexT) effect {rreg}
-function tlbSearch(VAddr) =
- let r = (VAddr[63..62]) in
- let vpn2 = (VAddr[39..13]) in
- let asid = TLBEntryHi.ASID() in {
- foreach (idx from 0 to 63) {
- if(tlbEntryMatch(r, vpn2, asid, reg_deref(TLBEntries[idx]))) then
- return Some(to_bits(6, idx))
- };
- None()
- }
-
-/** For given virtual address and accessType returns physical address and
-bool flag indicating whether capability stores / loads are permitted for
-page (depending on access type). */
-
-val TLBTranslate2 : (bits(64), MemAccessType) -> (bits(64), bool) effect {rreg, wreg, undef, escape}
-function TLBTranslate2 (vAddr, accessType) = {
- let idx = tlbSearch(vAddr) in
- match idx {
- Some(idx) =>
- let i as atom(_) = unsigned(idx) in
- let entry = reg_deref(TLBEntries[i]) in
- let entryMask = entry.pagemask() in
- let 'evenOddBit : range(12,28) = match (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 : bits(1), capl : bits(1), pfn : bits(24), d : bits(1), v : bits(1)) =
- if (isOdd) then
- (entry.caps1(), entry.capl1(), entry.pfn1(), entry.d1(), entry.v1())
- else
- (entry.caps0(), entry.capl0(), entry.pfn0(), entry.d0(), 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 : bits(64) = EXTZ(pfn[23..(evenOddBit - 12)] @ vAddr[(evenOddBit - 1) .. 0]) in
- (res, bits_to_bool(if (accessType == StoreData) then caps else capl)),
- None() => SignalExceptionTLB(
- if (accessType == StoreData) then XTLBRefillS else XTLBRefillL, vAddr)
- }
-}
-
-val cast_AccessLevel : AccessLevel -> int effect pure
-function cast_AccessLevel level =
- match level {
- User => 0,
- Supervisor => 1,
- Kernel => 2
- }
-
-/* perform TLB translation. bool is CHERI specific TLB bits noStoreCap/suppressTag */
-val TLBTranslateC : (bits(64), MemAccessType) -> (bits(64), bool) effect {escape, rreg, undef, wreg}
-function TLBTranslateC (vAddr, accessType) =
- {
- let currentAccessLevel = getAccessLevel() in
- let compat32 = (vAddr[61..31] == 0b1111111111111111111111111111111) in
- let (requiredLevel, addr) : (AccessLevel, option(bits(64))) = match (vAddr[63..62]) {
- 0b11 => match (compat32, vAddr[30..29]) { /* xkseg */
- (true, 0b11) => (Kernel, None() : option(bits(64))), /* kseg3 mapped 32-bit compat */
- (true, 0b10) => (Supervisor, None() : option(bits(64))), /* sseg mapped 32-bit compat */
- (true, 0b01) => (Kernel, Some(0x00000000 @ 0b000 @ vAddr[28..0])), /* kseg1 unmapped uncached 32-bit compat */
- (true, 0b00) => (Kernel, Some(0x00000000 @ 0b000 @ vAddr[28..0])), /* kseg0 unmapped cached 32-bit compat */
- (_, _) => (Kernel, None() : option(bits(64))) /* xkseg mapped */
- },
- 0b10 => (Kernel, Some(0b00000 @ vAddr[58..0])), /* xkphys bits 61-59 are cache mode (ignored) */
- 0b01 => (Supervisor, None() : option(bits(64))), /* xsseg - supervisor mapped */
- 0b00 => (User, None() : option(bits(64))) /* xuseg - user mapped */
- } in
- if (cast_AccessLevel(currentAccessLevel) < cast_AccessLevel(requiredLevel)) then
- SignalExceptionBadAddr(if (accessType == StoreData) then AdES else AdEL, vAddr)
- else
- let (pa, c) : (bits(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)
- }
- in if (unsigned(pa) > MAX_PA) then
- SignalExceptionBadAddr(if (accessType == StoreData) then AdES else AdEL, vAddr)
- else
- (pa, c)
- }
-
-/* TLB translate function for MIPS (throws away capability flag) */
-val TLBTranslate : (bits(64), MemAccessType) -> bits(64) effect {rreg, wreg, escape, undef}
-function TLBTranslate (vAddr, accessType) =
- let (addr, c) = TLBTranslateC(vAddr, accessType) in addr
diff --git a/mips_new_tc/mips_tlb_stub.sail b/mips_new_tc/mips_tlb_stub.sail
deleted file mode 100644
index f0ffb9dd..00000000
--- a/mips_new_tc/mips_tlb_stub.sail
+++ /dev/null
@@ -1,48 +0,0 @@
-/*========================================================================*/
-/* */
-/* 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. */
-/*========================================================================*/
-
-$ifndef _MIPS_TLB_STUB
-$define _MIPS_TLB_STUB
-
-val tlbEntryMatch : (bits(2), bits(27), bits(8), TLBEntry) -> bool effect pure
-function tlbSearch(VAddr) : bits(64) -> option(TLBIndexT) = None
-
-val TLBTranslate2 : (bits(64), MemAccessType) -> (bits(64), bool) effect pure
-function TLBTranslate (vAddr, accessType) : (bits(64), MemAccessType) -> bits(64) =
- vAddr
-
-val TLBTranslateC : (bits(64), MemAccessType) -> (bits(64), bool) effect pure
-function TLBTranslateC (vAddr, accessType) : (bits(64), MemAccessType) -> (bits(64), bool) = (vAddr, false)
-
-$endif
diff --git a/mips_new_tc/mips_wrappers.sail b/mips_new_tc/mips_wrappers.sail
deleted file mode 100644
index 70e6fa83..00000000
--- a/mips_new_tc/mips_wrappers.sail
+++ /dev/null
@@ -1,86 +0,0 @@
-/*========================================================================*/
-/* */
-/* 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) */
-
-val MEMw_wrapper : forall 'n, 1 <= 'n <= 8. (bits(64), atom('n), bits(8 * 'n)) -> unit effect {eamem, wmv, wreg}
-
-function MEMw_wrapper(addr, size, data) =
- let ledata = reverse_endianness(data) in
- if (addr == 0x000000007f000000) then
- {
- UART_WDATA = ledata[7..0];
- UART_WRITTEN = bitone;
- } else {
- MEMea(addr, size);
- MEMval(addr, size, ledata);
- }
-
-val MEMw_conditional_wrapper : forall 'n, 1 <= 'n <= 8. (bits(64), atom('n), bits(8 * 'n)) -> bool effect {eamem, wmv}
-
-function MEMw_conditional_wrapper(addr, size, data) =
- {
- MEMea_conditional(addr, size);
- MEMval_conditional(addr, size, reverse_endianness(data))
- }
-
-val addrWrapper : (bits(64), MemAccessType, WordType) -> bits(64)
-function addrWrapper(addr, accessType, width) =
- addr
-
-$ifdef _MIPS_TLB_STUB
-val TranslatePC : bits(64) -> bits(64) effect {rreg, wreg, escape}
-$else
-val TranslatePC : bits(64) -> bits(64) effect {rreg, wreg, escape, undef}
-$endif
-
-function TranslatePC (vAddr) = {
- incrementCP0Count();
- if (vAddr[1..0] != 0b00) then /* bad PC alignment */
- (SignalExceptionBadAddr(AdEL, vAddr))
- else
- TLBTranslate(vAddr, Instruction)
-}
-
-let have_cp2 = false
-
-function SignalException (ex) = SignalExceptionMIPS(ex, 0x0000000000000000)
-
-val ERETHook : unit -> unit
-function ERETHook() = ()
-
-function init_cp2_state () = skip_wreg()
-function cp2_next_pc() = {skip_wreg(); skip_rreg()}
-function dump_cp2_state () = {skip_rreg(); skip_escape();}
diff --git a/mips_new_tc/prelude.sail b/mips_new_tc/prelude.sail
deleted file mode 100644
index 5b89521f..00000000
--- a/mips_new_tc/prelude.sail
+++ /dev/null
@@ -1,391 +0,0 @@
-default Order dec
-
-type bits ('n : Int) = vector('n, dec, bit)
-union option ('a : Type) = {None : unit, Some : 'a}
-
-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_vec = "not_vec" : forall 'n. bits('n) -> bits('n)
-
-overload ~ = {not_bool, not_vec}
-
-val not = "not" : bool -> bool
-
-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 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 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 __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_real = {ocaml: "gteq_real", lem: "gteq"} : (real, real) -> bool
-
-overload operator >= = {gteq_atom, gteq_int, gteq_real}
-
-val lteq_real = {ocaml: "lteq_real", lem: "lteq"} : (real, real) -> bool
-
-overload operator <= = {lteq_atom, lteq_int, lteq_real}
-
-val gt_real = {ocaml: "gt_real", lem: "gt"} : (real, real) -> bool
-
-overload operator > = {gt_atom, gt_int, gt_real}
-
-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"} : forall 'n, 'n > 0 . (int, atom('n)) -> range(0, 'n - 1)
-
-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
-
-val min_atom = {ocaml: "min_int", lem: "min"} : forall 'a 'b . (atom('a), atom('b)) -> {'c, ('c = 'a | 'c = 'b) & 'c <= 'a & 'c <= 'b . atom('c)}
-
-val max_atom = {ocaml: "max_int", lem: "max"} : forall 'a 'b . (atom('a), atom('b)) -> {'c, ('c = 'a | 'c = 'b) & 'c >= 'a & 'c >= 'b . atom('c)}
-
-overload min = {min_atom, min_nat, min_int}
-
-overload max = {max_atom, 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 __MIPS_write : forall 'n. (bits(64), atom('n), bits(8 * 'n)) -> unit effect {wmv}
-function __MIPS_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 __MIPS_read : forall 'n. (bits(64), atom('n)) -> bits(8 * 'n) effect {rmem}
-function __MIPS_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 8 ^^
-val operator ^^ = {lem: "replicate_bits"} : forall 'n 'm . (bits('n), atom('m)) -> bits('n * 'm)
-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 = {
- ISAException : unit,
- Error_not_implemented : string,
- Error_misaligned_access : unit,
- Error_EBREAK : unit,
- Error_internal_error : unit
-}
-
-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))
-
-val zeros : forall 'n, 'n >= 0 . unit -> bits('n)
-function zeros() = replicate_bits (0b0,'n)
-
-val ones : forall 'n, 'n >= 0 . unit -> bits('n)
-function ones() = replicate_bits (0b1,'n)
-
-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
-
-val cast bits_to_bool : bits(1) -> bool
-function bits_to_bool x = bit_to_bool(x[0])
-
-infix 1 >>
-infix 1 <<
-infix 1 >>_s
-
-val "shift_bits_right" : forall 'n 'm. (bits('n), bits('m)) -> bits('n)
-val "shift_bits_left" : forall 'n 'm. (bits('n), bits('m)) -> bits('n)
-
-val "shiftl" : forall 'm 'n, 'n >= 0. (bits('m), atom('n)) -> bits('m)
-val "shiftr" : forall 'm 'n, 'n >= 0. (bits('m), atom('n)) -> bits('m)
-
-overload operator >> = {shift_bits_right, shiftr}
-overload operator << = {shift_bits_left, shiftl}
-val operator >>_s = "shift_bits_right_arith" : forall 'n 'm. (bits('n), bits('m)) -> bits('n)
-
-infix 7 *_s
-val operator *_s = "smult_vec" : forall 'n . (bits('n), bits('n)) -> bits(2 * 'n)
-infix 7 *_u
-val operator *_u = "mult_vec" : forall 'n . (bits('n), bits('n)) -> bits(2 * '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}
-
-val mask : forall 'm 'n , 'm >= 'n > 0 . bits('m) -> bits('n)
-function mask bs = bs['n - 1 .. 0]
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 12:10:03 +0000