diff options
Diffstat (limited to 'mips')
| -rw-r--r-- | mips/Makefile | 23 | ||||
| -rw-r--r-- | mips/mips_epilogue.sail | 41 | ||||
| -rw-r--r-- | mips/mips_extras.lem | 73 | ||||
| -rw-r--r-- | mips/mips_extras_embed.lem | 53 | ||||
| -rw-r--r-- | mips/mips_extras_embed_sequential.lem | 58 | ||||
| -rw-r--r-- | mips/mips_extras_ml.ml | 120 | ||||
| -rw-r--r-- | mips/mips_insts.sail | 1675 | ||||
| -rw-r--r-- | mips/mips_prelude.sail | 609 | ||||
| -rw-r--r-- | mips/mips_regfp.sail | 451 | ||||
| -rw-r--r-- | mips/mips_ri.sail | 42 | ||||
| -rw-r--r-- | mips/mips_tlb.sail | 128 | ||||
| -rw-r--r-- | mips/mips_tlb_stub.sail | 40 | ||||
| -rw-r--r-- | mips/mips_wrappers.sail | 70 | ||||
| -rw-r--r-- | mips/run_embed.ml | 404 |
14 files changed, 0 insertions, 3787 deletions
diff --git a/mips/Makefile b/mips/Makefile deleted file mode 100644 index 03d7ae15..00000000 --- a/mips/Makefile +++ /dev/null @@ -1,23 +0,0 @@ -SAIL:=../src/sail.native -LEM:=../../lem/lem - -# SOURCES:=mips_prelude.sail mips_tlb.sail mips_wrappers.sail mips_insts.sail mips_ri.sail mips_epilogue.sail ../etc/regfp.sail mips_regfp.sail -SOURCES:=mips_prelude.sail mips_tlb_stub.sail mips_wrappers.sail mips_insts.sail mips_epilogue.sail ../etc/regfp.sail mips_regfp.sail - - -all: mips.lem mips.ml mips_embed.lem - -mips.lem: $(SOURCES) - $(SAIL) -lem_ast -o $(BUILD)/mips $(SOURCES) - -mips.ml: mips.lem ../src/lem_interp/interp_ast.lem - $(LEM) -ocaml -lib ../src/lem_interp/ $< - - -mips_embed.lem: $(SOURCES) -# also generates mips_embed_sequential.lem, mips_embed_types.lem, mips_toFromInterp.lem - $(SAIL) -lem -lem_lib Mips_extras_embed -o mips $(SOURCES) - -clean: - rm -f mips.lem mips.ml - rm -f mips_embed*.lem mips_toFromInterp.lem diff --git a/mips/mips_epilogue.sail b/mips/mips_epilogue.sail deleted file mode 100644 index 50993949..00000000 --- a/mips/mips_epilogue.sail +++ /dev/null @@ -1,41 +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 - -function option<ast> supported_instructions (instr) = Some(instr) diff --git a/mips/mips_extras.lem b/mips/mips_extras.lem deleted file mode 100644 index be576fb2..00000000 --- a/mips/mips_extras.lem +++ /dev/null @@ -1,73 +0,0 @@ -open import Pervasives -open import Interp_ast -open import Interp_interface -open import Sail_impl_base -open import Interp_inter_imp -import Set_extra - -let memory_parameter_transformer mode v = - match v with - | Interp_ast.V_tuple [location;length] -> - let (v,loc_regs) = extern_with_track mode extern_vector_value location in - - match length with - | Interp_ast.V_lit (L_aux (L_num len) _) -> - (v,(natFromInteger len),loc_regs) - | Interp_ast.V_track (Interp_ast.V_lit (L_aux (L_num len) _)) size_regs -> - match loc_regs with - | Nothing -> (v,(natFromInteger len),Just (List.map (fun r -> extern_reg r Nothing) (Set_extra.toList size_regs))) - | Just loc_regs -> (v,(natFromInteger len),Just (loc_regs++(List.map (fun r -> extern_reg r Nothing) (Set_extra.toList size_regs)))) - end - | _ -> Assert_extra.failwith "expected 'V_lit (L_aux (L_num _) _)' or 'V_track (V_lit (L_aux (L_num len) _)) _'" - end - | _ -> Assert_extra.failwith ("memory_parameter_transformer: expected 'V_tuple [_;_]' given " ^ (Interp.string_of_value v)) - end - -let memory_parameter_transformer_option_address _mode v = - match v with - | Interp_ast.V_tuple [location;_] -> - Just (extern_vector_value location) - | _ -> Assert_extra.failwith ("memory_parameter_transformer_option_address: expected 'V_tuple [_;_]' given " ^ (Interp.string_of_value v)) - end - - -let mips_read_memory_functions : memory_reads = - [ ("MEMr", (MR Read_plain memory_parameter_transformer)); - ("MEMr_reserve", (MR Read_reserve memory_parameter_transformer)); - ] - -let mips_read_memory_tagged_functions : memory_read_taggeds = - [ ("MEMr_tag", (MRT Read_plain memory_parameter_transformer)); - ("MEMr_tag_reserve", (MRT Read_reserve memory_parameter_transformer)); - ] - -let mips_memory_writes : memory_writes = - [] - -let mips_memory_eas : memory_write_eas = - [ ("MEMea", (MEA Write_plain memory_parameter_transformer)); - ("MEMea_conditional", (MEA Write_conditional memory_parameter_transformer)); - ] - -let mips_memory_vals : memory_write_vals = - [ ("MEMval", (MV memory_parameter_transformer_option_address Nothing)); - ("MEMval_conditional", (MV memory_parameter_transformer_option_address - (Just - (fun (IState interp context) b -> - let bit = Interp_ast.V_lit (L_aux (if b then L_one else L_zero) Interp_ast.Unknown) in - (IState (Interp.add_answer_to_stack interp bit) context))))); - ] - -let mips_memory_vals_tagged : memory_write_vals_tagged = - [ - ("MEMval_tag", (MVT memory_parameter_transformer_option_address Nothing)); - ("MEMval_tag_conditional", (MVT memory_parameter_transformer_option_address - (Just - (fun (IState interp context) b -> - let bit = Interp_ast.V_lit (L_aux (if b then L_one else L_zero) Interp_ast.Unknown) in - (IState (Interp.add_answer_to_stack interp bit) context))))); - ] - -let mips_barrier_functions = [ - ("MEM_sync", Barrier_MIPS_SYNC); - ] diff --git a/mips/mips_extras_embed.lem b/mips/mips_extras_embed.lem deleted file mode 100644 index 8abc9747..00000000 --- a/mips/mips_extras_embed.lem +++ /dev/null @@ -1,53 +0,0 @@ -open import Pervasives -open import Pervasives_extra -open import Sail_impl_base -open import Sail_values -open import Prompt - -val MEMr : (vector bitU * integer) -> M (vector bitU) -val MEMr_reserve : (vector bitU * integer) -> M (vector bitU) -val MEMr_tag : (vector bitU * integer) -> M (vector bitU) -val MEMr_tag_reserve : (vector bitU * integer) -> M (vector bitU) - -let MEMr (addr,size) = read_mem false Read_plain addr size -let MEMr_reserve (addr,size) = read_mem false Read_reserve addr size - -let MEMr_tag (addr,size) = read_mem false Read_plain addr size -let MEMr_tag_reserve (addr,size) = read_mem false Read_reserve addr size - - -val MEMea : (vector bitU * integer) -> M unit -val MEMea_conditional : (vector bitU * integer) -> M unit -val MEMea_tag : (vector bitU * integer) -> M unit -val MEMea_tag_conditional : (vector bitU * integer) -> M unit - -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 : (vector bitU * integer * vector bitU) -> M unit -val MEMval_conditional : (vector bitU * integer * vector bitU) -> M bitU -val MEMval_tag : (vector bitU * integer * vector bitU) -> M unit -val MEMval_tag_conditional : (vector bitU * integer * vector bitU) -> M bitU - -let MEMval (_,_,v) = write_mem_val v >>= fun _ -> return () -let MEMval_conditional (_,_,v) = write_mem_val v >>= fun b -> return (if b then B1 else B0) -let MEMval_tag (_,_,v) = write_mem_val v >>= fun _ -> return () -let MEMval_tag_conditional (_,_,v) = write_mem_val v >>= fun b -> return (if b then B1 else B0) - -(* TODO *) -val TAGw : (vector bitU * vector bitU) -> M unit -let TAGw (addr, tag) = failwith "TAGw not implemented" - -val MEM_sync : unit -> M unit - -let MEM_sync () = barrier Barrier_Isync - - -let duplicate (bit,len) = - let bits = repeat [bit] len in - let start = len - 1 in - Vector bits start false diff --git a/mips/mips_extras_embed_sequential.lem b/mips/mips_extras_embed_sequential.lem deleted file mode 100644 index 708c1f63..00000000 --- a/mips/mips_extras_embed_sequential.lem +++ /dev/null @@ -1,58 +0,0 @@ -open import Pervasives -open import Pervasives_extra -open import Sail_impl_base -open import Sail_values -open import State - -val MEMr : forall 'a 'b. Size 'b => (bitvector 'a * integer) -> M (bitvector 'b) -val MEMr_reserve : forall 'a 'b. Size 'b => (bitvector 'a * integer) -> M (bitvector 'b) -val MEMr_tag : forall 'a 'b. Size 'b => (bitvector 'a * integer) -> M (bitU * bitvector 'b) -val MEMr_tag_reserve : forall 'a 'b. Size 'b => (bitvector 'a * integer) -> M (bitU * bitvector 'b) - -let MEMr (addr,size) = read_mem false Read_plain addr size -let MEMr_reserve (addr,size) = read_mem false Read_reserve addr size - -let MEMr_tag (addr,size) = - read_mem false Read_plain addr size >>= fun v -> - read_tag false Read_plain addr >>= fun t -> - return (t, v) - -let MEMr_tag_reserve (addr,size) = - read_mem false Read_plain addr size >>= fun v -> - read_tag false Read_plain addr >>= fun t -> - return (t, v) - - -val MEMea : forall 'a. (bitvector 'a * integer) -> M unit -val MEMea_conditional : forall 'a. (bitvector 'a * integer) -> M unit -val MEMea_tag : forall 'a. (bitvector 'a * integer) -> M unit -val MEMea_tag_conditional : forall 'a. (bitvector 'a * integer) -> M unit - -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 'a 'b. (bitvector 'a * integer * bitvector 'b) -> M unit -val MEMval_conditional : forall 'a 'b. (bitvector 'a * integer * bitvector 'b) -> M bitU -val MEMval_tag : forall 'a 'b. (bitvector 'a * integer * bitU * bitvector 'b) -> M unit -val MEMval_tag_conditional : forall 'a 'b. (bitvector 'a * integer * bitU * bitvector 'b) -> M bitU - -let MEMval (_,_,v) = write_mem_val v >>= fun _ -> return () -let MEMval_conditional (_,_,v) = write_mem_val v >>= fun b -> return (if b then B1 else B0) -let MEMval_tag (_,_,t,v) = write_mem_val v >>= fun _ -> write_tag t >>= fun _ -> return () -let MEMval_tag_conditional (_,_,t,v) = write_mem_val v >>= fun b -> write_tag t >>= fun _ -> return (if b then B1 else B0) - -val MEM_sync : unit -> M unit - -let MEM_sync () = barrier Barrier_MIPS_SYNC - - -(* TODO: Consider moving this to sail_values.lem (after fixing and implementing - a default index ordering) *) -let duplicate (bit,len) = - let bits = repeat [bitU_to_bool bit] len in - let start = len - 1 in - Bitvector (wordFromBitlist bits) start false diff --git a/mips/mips_extras_ml.ml b/mips/mips_extras_ml.ml deleted file mode 100644 index d4ea0681..00000000 --- a/mips/mips_extras_ml.ml +++ /dev/null @@ -1,120 +0,0 @@ -open Sail_values -open Big_int_Z -open Printf - -let big_int_to_hex i = Z.format "%x" i - -module Mem = struct - include Map.Make(struct - type t = big_int - let compare = compare_big_int - end) -end - -let cap_size_shift = ref 5;; (* caps every 2**5 = 32 bytes *) -let mem_pages = (ref Mem.empty : (Bytes.t Mem.t) ref);; -let tag_mem = (ref Mem.empty : (bool Mem.t) ref);; - -let page_shift_bits = 20 (* 1M page *) -let page_size_bytes = 1 lsl page_shift_bits;; - - -let page_no_of_addr a = shift_right_big_int a page_shift_bits;; -let bottom_addr_of_page p = shift_left_big_int p page_shift_bits -let top_addr_of_page p = shift_left_big_int (succ_big_int p) page_shift_bits -let get_page p = - try - Mem.find p !mem_pages - with Not_found -> - let new_page = Bytes.create page_size_bytes in - mem_pages := Mem.add p new_page !mem_pages; - new_page - -let rec add_mem_bytes addr buf off len = - let page_no = page_no_of_addr addr in - let page_bot = bottom_addr_of_page page_no in - let page_top = top_addr_of_page page_no in - let page_off = int_of_big_int (sub_big_int addr page_bot) in - let page = get_page page_no in - let bytes_left_in_page = sub_big_int page_top addr in - let to_copy = min_int (int_of_big_int bytes_left_in_page) len in - Bytes.blit buf off page page_off to_copy; - if (to_copy < len) then - add_mem_bytes page_top buf (off + to_copy) (len - to_copy) - -let rec read_mem_bytes addr len = - let page_no = page_no_of_addr addr in - let page_bot = bottom_addr_of_page page_no in - let page_top = top_addr_of_page page_no in - let page_off = int_of_big_int (sub_big_int addr page_bot) in - let page = get_page page_no in - let bytes_left_in_page = sub_big_int page_top addr in - let to_get = min_int (int_of_big_int bytes_left_in_page) len in - let bytes = Bytes.sub page page_off to_get in - if to_get >= len then - bytes - else - Bytes.cat bytes (read_mem_bytes page_top (len - to_get)) - -let _MEMea (addr, size) = () -let _MEMea_conditional = _MEMea -let _MEMea_tag = _MEMea -let _MEMea_tag_conditional = _MEMea - -let _MEMval (addr, size, data) = - (* assumes data is decreasing vector to be stored in little-endian byte order in mem *) - let s = int_of_big_int size in - let a = unsigned_big(addr) in - let buf = Bytes.create s in - for i = 0 to (s - 1) do - let bit_idx = i * 8 in - let byte = unsigned_int(slice_raw (data, big_int_of_int bit_idx, big_int_of_int (bit_idx + 7))) in - Bytes.set buf (s-1-i) (char_of_int byte); - done; - if !trace_writes then - tracef "MEM[%s] <- %s\n" (big_int_to_hex a) (string_of_value data); - add_mem_bytes a buf 0 s - -let _MEMval_tag (addr, size, tag, data) = - let addr_bi = (unsigned_big(addr)) in - begin - _MEMval (addr, size, data); - tag_mem := Mem.add (shift_right_big_int addr_bi !cap_size_shift) (to_bool tag) !tag_mem; - end - - -let _MEMval_conditional (addr, size, data) = - let _ = _MEMval (addr, size, data) in - Vone - -let _MEMval_tag_conditional (addr, size, tag, data) = - let _ = _MEMval_tag (addr, size, tag, data) in - Vone - -let _MEMr (addr, size) = begin - let s = int_of_big_int size in - let a = unsigned_big(addr) in - let bytes = read_mem_bytes a s in - let ret = ref (to_vec_dec_int (0, 0)) in - for i = 0 to (s - 1) do - let byte = Bytes.get bytes i in - let byte_vec = to_vec_dec_int (8, int_of_char byte) in - ret := vector_concat byte_vec (!ret); - (*printf "MEM [%s] -> %x %s %s\n" (big_int_to_hex byte_addr) byte (string_of_value byte_vec) (string_of_value !ret);*) - done; - ret := set_start_to_length (!ret); - !ret; -end -let _MEMr_reserve = _MEMr - -let _MEMr_tag (addr, size) = - let data = _MEMr(addr, size) in - let addr_bi = unsigned_big(addr) in - let tag = try - Mem.find (shift_right_big_int addr_bi !cap_size_shift) !tag_mem - with Not_found -> false in - (bool_to_bit tag, data) - -let _MEMr_tag_reserve = _MEMr_tag - -let _MEM_sync _ = () diff --git a/mips/mips_insts.sail b/mips/mips_insts.sail deleted file mode 100644 index d127f6db..00000000 --- a/mips/mips_insts.sail +++ /dev/null @@ -1,1675 +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 function unit execute -scattered typedef ast = const union - -val bit[32] -> option<ast> effect pure decode -scattered function option<ast> decode - -(**************************************************************************************) -(* [D]ADD[I][U] various forms of ADD *) -(**************************************************************************************) - -(* DADDIU Doubleword Add Immediate Unsigned -- - the simplest possible instruction, no undefined behaviour or exceptions - reg, reg, immediate *) - -union ast member regregimm16 DADDIU - -function clause decode (0b011001 : (regno) rs : (regno) rt : (imm16) imm) = - 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 ast member regregreg DADDU - -function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 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 ast member regregimm16 DADDI - -function clause decode (0b011000 : (regno) rs : (regno) rt : (imm16) imm) = - Some(DADDI(rs, rt, imm)) - -function clause execute (DADDI (rs, rt, imm)) = - { - let (bit[65]) sum65 = (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 ast member regregreg DADD - -function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101100) = - Some(DADD(rs, rt, rd)) - -function clause execute (DADD (rs, rt, rd)) = - { - let (bit[65]) sum65 = (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 ast member regregreg ADD - -function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b100000) = - Some(ADD(rs, rt, rd)) - -function clause execute (ADD(rs, rt, rd)) = - { - (bit[64]) opA := rGPR(rs); - (bit[64]) opB := rGPR(rt); - if NotWordVal(opA) | NotWordVal(opB) then - wGPR(rd) := undefined (* XXX could exit instead *) - else - let (bit[33]) sum33 = (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 ast member regregimm16 ADDI - -function clause decode (0b001000 : (regno) rs : (regno) rt : (imm16) imm) = - Some(ADDI(rs, rt, imm)) - -function clause execute (ADDI(rs, rt, imm)) = - { - (bit[64]) opA := rGPR(rs); - if NotWordVal(opA) then - wGPR(rt) := undefined (* XXX could exit instead *) - else - let (bit[33]) sum33 = (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 ast member regregreg ADDU - -function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b100001) = - Some(ADDU(rs, rt, rd)) - -function clause execute (ADDU(rs, rt, rd)) = - { - (bit[64]) opA := rGPR(rs); - (bit[64]) 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 ast member regregimm16 ADDIU - -function clause decode (0b001001 : (regno) rs : (regno) rt : (imm16) imm) = - Some(ADDIU(rs, rt, imm)) - -function clause execute (ADDIU(rs, rt, imm)) = - { - (bit[64]) 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 ast member regregreg DSUBU - -function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 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 ast member regregreg DSUB - -function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101110) = - Some(DSUB(rs, rt, rd)) - -function clause execute (DSUB (rs, rt, rd)) = - { - let (bit[65]) temp65 = (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 ast member regregreg SUB - -function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b100010) = - Some(SUB(rs, rt, rd)) - -function clause execute (SUB(rs, rt, rd)) = - { - (bit[64]) opA := rGPR(rs); - (bit[64]) opB := rGPR(rt); - if NotWordVal(opA) | NotWordVal(opB) then - wGPR(rd) := undefined (* XXX could instead *) - else - let (bit[33]) temp33 = (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 ast member regregreg SUBU -function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b100011) = - Some(SUBU(rs, rt, rd)) - -function clause execute (SUBU(rs, rt, rd)) = - { - (bit[64]) opA := rGPR(rs); - (bit[64]) 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 ast member regregreg AND -function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 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 ast member regregimm16 ANDI -function clause decode (0b001100 : (regno) rs : (regno) rt : (imm16) imm) = - Some(ANDI(rs, rt, imm)) -function clause execute (ANDI (rs, rt, imm)) = - { - wGPR(rt) := (rGPR(rs) & EXTZ(imm)) - } - -(* OR reg, reg, reg *) - -union ast member regregreg OR -function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 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 ast member regregimm16 ORI -function clause decode (0b001101 : (regno) rs : (regno) rt : (imm16) imm) = - Some(ORI(rs, rt, imm)) -function clause execute (ORI (rs, rt, imm)) = - { - wGPR(rt) := (rGPR(rs) | EXTZ(imm)) - } - -(* NOR reg, reg, reg *) - -union ast member regregreg NOR -function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 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 ast member regregreg XOR -function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 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 ast member regregimm16 XORI -function clause decode (0b001110 : (regno) rs : (regno) rt : (imm16) imm) = - 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 ast member (regno, imm16) LUI -function clause decode (0b001111 : 0b00000 : (regno) rt : (imm16) imm) = - Some(LUI(rt, imm)) -function clause execute (LUI (rt, imm)) = - { - wGPR(rt) := EXTS(imm : 0x0000) - } - -(**************************************************************************************) -(* 64-bit shift operations *) -(**************************************************************************************) - -(* DSLL reg, reg, imm5 *) - -union ast member regregreg DSLL -function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (bit[5]) sa : 0b111000) = - Some(DSLL(rt, rd, sa)) -function clause execute (DSLL (rt, rd, sa)) = - { - - wGPR(rd) := (rGPR(rt) << sa) (* make tuareg mode less blue >> *) - } - -(* DSLL32 reg, reg, imm5 *) - -union ast member regregreg DSLL32 -function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (bit[5]) sa : 0b111100) = - Some(DSLL32(rt, rd, sa)) -function clause execute (DSLL32 (rt, rd, sa)) = - { - wGPR(rd) := (rGPR(rt) << (0b1 : sa)) (* make tuareg mode less blue >> *) - } - -(* DSLLV reg, reg, reg *) - -union ast member regregreg DSLLV -function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b010100) = - Some(DSLLV(rs, rt, rd)) -function clause execute (DSLLV (rs, rt, rd)) = - { - wGPR(rd) := (rGPR(rt) << ((rGPR(rs))[5 .. 0])) (* make tuareg mode less blue >> *) - (* alternative slicing based version of above - sa := (rGPR(rt))[5 .. 0]; - v := rGPR(rs); - wGPR(rd) := v[(63-sa) .. 0] : (0b0 ^^ sa) *) - } - -(* DSRA arithmetic shift duplicating sign bit - reg, reg, imm5 *) - -union ast member regregreg DSRA -function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (bit[5]) sa : 0b111011) = - Some(DSRA(rt, rd, sa)) -function clause execute (DSRA (rt, rd, sa)) = - { - temp := rGPR(rt); - wGPR(rd) := ((temp[63] ^^ sa) : (temp[63 .. sa])) - } - -(* DSRA32 reg, reg, imm5 *) - -union ast member regregreg DSRA32 -function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (bit[5]) sa : 0b111111) = - Some(DSRA32(rt, rd, sa)) -function clause execute (DSRA32 (rt, rd, sa)) = - { - temp := rGPR(rt); - sa32 := (0b1 : sa); (* sa+32 *) - wGPR(rd) := ((temp[63] ^^ sa32) : (temp[63 .. sa32])) - } - -(* DSRAV reg, reg, reg *) -union ast member regregreg DSRAV -function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 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[63] ^^ sa) : temp[63 .. sa]) - } - -(* DSRL shift right logical - reg, reg, imm5 *) - -union ast member regregreg DSRL -function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (bit[5]) sa : 0b111010) = - Some(DSRL(rt, rd, sa)) -function clause execute (DSRL (rt, rd, sa)) = - { - temp := rGPR(rt); - wGPR(rd) := ((bitzero ^^ sa) : (temp[63 .. sa])) - } - -(* DSRL32 reg, reg, imm5 *) - -union ast member regregreg DSRL32 -function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (bit[5]) sa : 0b111110) = - Some(DSRL32(rt, rd, sa)) -function clause execute (DSRL32 (rt, rd, sa)) = - { - temp := rGPR(rt); - sa32 := (0b1 : sa); (* sa+32 *) - wGPR(rd) := ((bitzero ^^ sa32) : (temp[63 .. sa32])) - } - -(* DSRLV reg, reg, reg *) - -union ast member regregreg DSRLV -function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b010110) = - Some(DSRLV(rs, rt, rd)) -function clause execute (DSRLV (rs, rt, rd)) = - { - temp := rGPR(rt); - sa := (rGPR(rs)) [5..0]; - wGPR(rd) := ((bitzero ^^ sa) : temp[63 .. sa]) - } - -(**************************************************************************************) -(* 32-bit shift operations *) -(**************************************************************************************) - -(* SLL 32-bit shift left *) - -union ast member regregreg SLL -function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (regno) sa : 0b000000) = - Some(SLL(rt, rd, sa)) -function clause execute (SLL(rt, rd, sa)) = - { - wGPR(rd) := EXTS((rGPR(rt)) [(31-sa)..0] : (bitzero ^^ sa)) - } - -(* SLLV 32-bit shift left variable *) - -union ast member regregreg SLLV -function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b000100) = - Some(SLLV(rs, rt, rd)) -function clause execute (SLLV(rs, rt, rd)) = - { - sa := (rGPR(rs))[4..0]; - wGPR(rd) := EXTS((rGPR(rt)) [(31-sa)..0] : (bitzero ^^ sa)) - } - -(* SRA 32-bit arithmetic shift right *) - -union ast member regregreg SRA -function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (regno) sa : 0b000011) = - Some(SRA(rt, rd, sa)) -function clause execute (SRA(rt, rd, sa)) = - { - temp := rGPR(rt); - if (NotWordVal(temp)) then - wGPR(rd) := undefined - else - wGPR(rd) := (temp[31] ^^ (sa+32)) : temp [31..sa] - } - -(* SRAV 32-bit arithmetic shift right variable *) - -union ast member regregreg SRAV -function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b000111) = - 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 - wGPR(rd) := (temp[31] ^^ (sa+32)) : temp [31..sa] - } - -(* SRL 32-bit shift right *) - -union ast member regregreg SRL -function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (regno) sa : 0b000010) = - Some(SRL(rt, rd, sa)) -function clause execute (SRL(rt, rd, sa)) = - { - temp := rGPR(rt); - if (NotWordVal(temp)) then - wGPR(rd) := undefined - else - wGPR(rd) := EXTS((bitzero ^^ sa) : (temp [31..sa])) - } - -(* SRLV 32-bit shift right variable *) - -union ast member regregreg SRLV -function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b000110) = - 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 - wGPR(rd) := EXTS((bitzero ^^ sa) : (temp [31..sa])) - } - -(**************************************************************************************) -(* set less than / conditional move *) -(**************************************************************************************) - -(* SLT set if less than (signed) *) - -union ast member regregreg SLT -function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101010) = - Some(SLT(rs, rt, rd)) -function clause execute (SLT(rs, rt, rd)) = - { - wGPR(rd) := if (rGPR(rs) <_s rGPR(rt)) then 1 else 0 - } - -(* SLT set if less than immediate (signed) *) - -union ast member regregimm16 SLTI -function clause decode (0b001010 : (regno) rs : (regno) rt : (imm16) imm) = - Some(SLTI(rs, rt, imm)) -function clause execute (SLTI(rs, rt, imm)) = - { - let imm_val = signed(imm) in - let rs_val = signed(rGPR(rs)) in - wGPR(rt) := if (rs_val < imm_val) then 0x0000000000000001 else 0x0000000000000000 - } - -(* SLTU set if less than unsigned *) - -union ast member regregreg SLTU -function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101011) = - Some(SLTU(rs, rt, rd)) -function clause execute (SLTU(rs, rt, rd)) = - { - let rs_val = (0b0 : (rGPR(rs))) in - let rt_val = (0b0 : (rGPR(rt))) in - wGPR(rd) := (if (rs_val < rt_val) then 1 else 0) - } - -(* SLTIU set if less than immediate unsigned *) - -union ast member regregimm16 SLTIU -function clause decode (0b001011 : (regno) rs : (regno) rt : (imm16) imm) = - Some(SLTIU(rs, rt, imm)) -function clause execute (SLTIU(rs, rt, imm)) = - { - let rs_val = (0b0 : (rGPR(rs))) in - let imm_val = (0b0 : ((bit[64])(EXTS(imm)))) in - wGPR(rt) := (if (rs_val < imm_val) then 1 else 0) - } - -(* MOVN move if non-zero *) - -union ast member regregreg MOVN -function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b001011) = - Some(MOVN(rs, rt, rd)) -function clause execute (MOVN(rs, rt, rd)) = - { - if (rGPR(rt) != 0x0000000000000000) then - wGPR(rd) := rGPR(rs) - } - -(* MOVZ move if zero *) - -union ast member regregreg MOVZ -function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b001010) = - 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 ast member regno MFHI -function clause decode (0b000000 : 0b0000000000 : (regno) rd : 0b00000 : 0b010000) = - Some(MFHI(rd)) -function clause execute (MFHI(rd)) = - { - wGPR(rd) := HI - } - -(* MFLO move from LO register *) -union ast member regno MFLO -function clause decode (0b000000 : 0b0000000000 : (regno) rd : 0b00000 : 0b010010) = - Some(MFLO(rd)) -function clause execute (MFLO(rd)) = - { - wGPR(rd) := LO - } - -(* MTHI move to HI register *) -union ast member regno MTHI -function clause decode (0b000000 : (regno) rs : 0b000000000000000 : 0b010001) = - Some(MTHI(rs)) -function clause execute (MTHI(rs)) = - { - HI := rGPR(rs) - } - -(* MTLO move to LO register *) -union ast member regno MTLO -function clause decode (0b000000 : (regno) rs : 0b000000000000000 : 0b010011) = - Some(MTLO(rs)) -function clause execute (MTLO(rs)) = - { - LO := rGPR(rs) - } - -(* MUL 32-bit multiply into GPR *) -union ast member regregreg MUL -function clause decode (0b011100 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b000010) = - Some(MUL(rs, rt, rd)) -function clause execute (MUL(rs, rt, rd)) = - { - rsVal := rGPR(rs); - rtVal := rGPR(rt); - (bit[64]) result := (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 ast member (regno, regno) MULT -function clause decode (0b000000 : (regno) rs : (regno) rt : 0b00000 : 0b00000 : 0b011000) = - Some(MULT(rs, rt)) -function clause execute (MULT(rs, rt)) = - { - rsVal := rGPR(rs); - rtVal := rGPR(rt); - (bit[64]) result := if (NotWordVal(rsVal) | NotWordVal(rtVal)) then - 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 ast member (regno, regno) MULTU -function clause decode (0b000000 : (regno) rs : (regno) rt : 0b00000 : 0b00000 : 0b011001) = - Some(MULTU(rs, rt)) -function clause execute (MULTU(rs, rt)) = - { - rsVal := rGPR(rs); - rtVal := rGPR(rt); - (bit[64]) result := if (NotWordVal(rsVal) | NotWordVal(rtVal)) then - undefined - else - (rsVal[31..0]) * (rtVal[31..0]); - HI := EXTS(result[63..32]); - LO := EXTS(result[31..0]); - } - -(* DMULT 64-bit multiply into HI/LO *) -union ast member (regno, regno) DMULT -function clause decode (0b000000 : (regno) rs : (regno) rt : 0b00000 : 0b00000 : 0b011100) = - Some(DMULT(rs, rt)) -function clause execute (DMULT(rs, rt)) = - { - (bit[128]) result := (rGPR(rs)) *_s (rGPR(rt)); - HI := (result[127..64]); - LO := (result[63..0]); - } - -(* DMULTU 64-bit unsigned multiply into HI/LO *) -union ast member (regno, regno) DMULTU -function clause decode (0b000000 : (regno) rs : (regno) rt : 0b00000 : 0b00000 : 0b011101) = - Some(DMULTU(rs, rt)) -function clause execute (DMULTU(rs, rt)) = - { - (bit[128]) result := (rGPR(rs)) * (rGPR(rt)); - HI := (result[127..64]); - LO := (result[63..0]); - } - -(* MADD 32-bit signed multiply and add into HI/LO *) -union ast member (regno, regno) MADD -function clause decode (0b011100 : (regno) rs : (regno) rt : 0b00000 : 0b00000 : 0b000000) = - Some(MADD(rs, rt)) -function clause execute (MADD(rs, rt)) = - { - rsVal := rGPR(rs); - rtVal := rGPR(rt); - (bit[64]) mul_result := if (NotWordVal(rsVal) | NotWordVal(rtVal)) then - undefined - else - ((rsVal[31..0]) *_s (rtVal[31..0])); - (bit[64]) result := mul_result + (HI[31..0] : LO[31..0]); - HI := EXTS(result[63..32]); - LO := EXTS(result[31..0]); - } - -(* MADDU 32-bit unsigned multiply and add into HI/LO *) -union ast member (regno, regno) MADDU -function clause decode (0b011100 : (regno) rs : (regno) rt : 0b00000 : 0b00000 : 0b000001) = - Some(MADDU(rs, rt)) -function clause execute (MADDU(rs, rt)) = - { - rsVal := rGPR(rs); - rtVal := rGPR(rt); - (bit[64]) mul_result := if (NotWordVal(rsVal) | NotWordVal(rtVal)) then - undefined - else - ((rsVal[31..0]) * (rtVal[31..0])); - (bit[64]) result := mul_result + (HI[31..0] : LO[31..0]); - HI := EXTS(result[63..32]); - LO := EXTS(result[31..0]); - } - -(* MSUB 32-bit signed multiply and sub from HI/LO *) -union ast member (regno, regno) MSUB -function clause decode (0b011100 : (regno) rs : (regno) rt : 0b00000 : 0b00000 : 0b000100) = - Some(MSUB(rs, rt)) -function clause execute (MSUB(rs, rt)) = - { - rsVal := rGPR(rs); - rtVal := rGPR(rt); - (bit[64]) mul_result := if (NotWordVal(rsVal) | NotWordVal(rtVal)) then - undefined - else - ((rsVal[31..0]) *_s (rtVal[31..0])); - (bit[64]) result := (HI[31..0] : LO[31..0]) - mul_result; - HI := EXTS(result[63..32]); - LO := EXTS(result[31..0]); - } - -(* MSUBU 32-bit unsigned multiply and sub from HI/LO *) -union ast member (regno, regno) MSUBU -function clause decode (0b011100 : (regno) rs : (regno) rt : 0b00000 : 0b00000 : 0b000101) = - Some(MSUBU(rs, rt)) -function clause execute (MSUBU(rs, rt)) = - { - rsVal := rGPR(rs); - rtVal := rGPR(rt); - (bit[64]) mul_result := if (NotWordVal(rsVal) | NotWordVal(rtVal)) then - undefined - else - ((rsVal[31..0]) * (rtVal[31..0])); - (bit[64]) result := (HI[31..0] : LO[31..0]) - mul_result; - HI := EXTS(result[63..32]); - LO := EXTS(result[31..0]); - } - -(* DIV 32-bit divide into HI/LO *) -union ast member (regno, regno) DIV -function clause decode (0b000000 : (regno) rs : (regno) rt : 0b00000 : 0b00000 : 0b011010) = - Some(DIV(rs, rt)) -function clause execute (DIV(rs, rt)) = - { - rsVal := rGPR(rs); - rtVal := rGPR(rt); - let ((bit[32]) q, (bit[32])r) = ( - if (NotWordVal(rsVal) | NotWordVal(rtVal) | (rtVal == 0)) then - (undefined, undefined) - else - let si = (signed((rsVal[31..0]))) in - let ti = (signed((rtVal[31..0]))) in - let qi = (si quot ti) in - let ri = (si - (ti*qi)) in - ((bit[32]) qi, (bit[32]) ri)) - in - { - HI := EXTS(r); - LO := EXTS(q); - } - } - -(* DIVU 32-bit unsigned divide into HI/LO *) -union ast member (regno, regno) DIVU -function clause decode (0b000000 : (regno) rs : (regno) rt : 0b00000 : 0b00000 : 0b011011) = - Some(DIVU(rs, rt)) -function clause execute (DIVU(rs, rt)) = - { - rsVal := rGPR(rs); - rtVal := rGPR(rt); - let ((bit[32]) q, (bit[32])r) = ( - if (NotWordVal(rsVal) | NotWordVal(rtVal) | rtVal == 0) then - (undefined, undefined) - else - let si = unsigned(rsVal[31..0]) in - let ti = unsigned(rtVal[31..0]) in - let qi = (si quot ti) in - let ri = (si mod ti) in - ((bit[32]) qi, (bit[32]) ri)) - in - { - HI := EXTS(r); - LO := EXTS(q); - } - } - -(* DDIV 64-bit divide into HI/LO *) -union ast member (regno, regno) DDIV -function clause decode (0b000000 : (regno) rs : (regno) rt : 0b00000 : 0b00000 : 0b011110) = - Some(DDIV(rs, rt)) -function clause execute (DDIV(rs, rt)) = - { - rsVal := signed(rGPR(rs)); - rtVal := signed(rGPR(rt)); - let ((bit[64])q, (bit[64])r) = (if (rtVal == 0) - then (undefined, undefined) - else - let qi = (rsVal quot rtVal) in - let ri = (rsVal - (qi * rtVal)) in - ((bit[64]) qi, (bit[64]) ri)) in - { - LO := q; - HI := r; - } - } - -(* DDIV 64-bit divide into HI/LO *) -union ast member (regno, regno) DDIVU -function clause decode (0b000000 : (regno) rs : (regno) rt : 0b00000 : 0b00000 : 0b011111) = - Some(DDIVU(rs, rt)) -function clause execute (DDIVU(rs, rt)) = - { - (int) rsVal := rGPR(rs); - (int) rtVal := rGPR(rt); - let ((bit[64])q, (bit[64])r) = (if (rtVal == 0) - then (undefined, undefined) - else let qi = (rsVal quot rtVal) in - let ri = (rsVal mod rtVal) in - ((bit[64]) qi, (bit[64]) ri)) in - { - LO := q; - HI := r; - } - } - -(**************************************************************************************) -(* Jump instructions -- unconditional branches *) -(**************************************************************************************) - -(* J - jump, the simplest control flow instruction, with branch delay slot *) -union ast member (bit[26]) J -function clause decode (0b000010 : (bit[26]) offset) = - Some(J(offset)) -function clause execute (J(offset)) = - { - delayedPC := (PC + 4)[63..28] : offset : 0b00; - branchPending := 1 - } - -(* JAL - jump and link *) -union ast member (bit[26]) JAL -function clause decode (0b000011 : (bit[26]) offset) = - Some(JAL(offset)) -function clause execute (JAL(offset)) = - { - delayedPC := (PC + 4)[63..28] : offset : 0b00; - branchPending := 1; - wGPR(31) := PC + 8; - } - -(* JR -- jump via register *) -union ast member regno JR -function clause decode (0b000000 : (regno) rs : 0b00000 : 0b00000 : (regno) hint : 0b001000) = - Some(JR(rs)) (* hint is ignored *) -function clause execute (JR(rs)) = - { - delayedPC := rGPR(rs); - branchPending := 1; - } - -(* JALR -- jump via register with link *) -union ast member (regno, regno) JALR -function clause decode (0b000000 : (regno) rs : 0b00000 : (regno) rd : (regno) hint : 0b001001) = - Some(JALR(rs, rd)) (* hint is ignored *) -function clause execute (JALR(rs, rd)) = - { - delayedPC := rGPR(rs); - branchPending := 1; - wGPR(rd) := PC + 8; - } - -(**************************************************************************************) -(* B[N]EQ[L] - branch on (not) equal (likely) *) -(* Conditional branch instructions with two register operands *) -(**************************************************************************************) - -union ast member (regno, regno, imm16, bool, bool) BEQ -function clause decode (0b000100 : (regno) rs : (regno) rt : (imm16) imm) = - Some(BEQ(rs, rt, imm, false, false)) (* BEQ *) -function clause decode (0b010100 : (regno) rs : (regno) rt : (imm16) imm) = - Some(BEQ(rs, rt, imm, false, true)) (* BEQL *) -function clause decode (0b000101 : (regno) rs : (regno) rt : (imm16) imm) = - Some(BEQ(rs, rt, imm, true , false)) (* BNE *) -function clause decode (0b010101 : (regno) rs : (regno) rt : (imm16) imm) = - Some(BEQ(rs, rt, imm, true , true)) (* BNEL *) -function clause execute (BEQ(rs, rd, imm, ne, likely)) = - { - if ((rGPR(rs) == rGPR(rd)) ^ ne) then - { - let (bit[64]) offset = (EXTS(imm : 0b00) + 4) in - delayedPC := PC + offset; - branchPending := 1; - } - 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 ast member (regno, imm16, Comparison, bool, bool) BCMPZ -function clause decode (0b000001 : (regno) rs : 0b00000 : (imm16) imm) = - Some(BCMPZ(rs, imm, LT, false, false)) (* BLTZ *) -function clause decode (0b000001 : (regno) rs : 0b10000 : (imm16) imm) = - Some(BCMPZ(rs, imm, LT, true, false)) (* BLTZAL *) -function clause decode (0b000001 : (regno) rs : 0b00010 : (imm16) imm) = - Some(BCMPZ(rs, imm, LT, false, true)) (* BLTZL *) -function clause decode (0b000001 : (regno) rs : 0b10010 : (imm16) imm) = - Some(BCMPZ(rs, imm, LT, true, true)) (* BLTZALL *) - -function clause decode (0b000001 : (regno) rs : 0b00001 : (imm16) imm) = - Some(BCMPZ(rs, imm, GE, false, false)) (* BGEZ *) -function clause decode (0b000001 : (regno) rs : 0b10001 : (imm16) imm) = - Some(BCMPZ(rs, imm, GE, true, false)) (* BGEZAL *) -function clause decode (0b000001 : (regno) rs : 0b00011 : (imm16) imm) = - Some(BCMPZ(rs, imm, GE, false, true)) (* BGEZL *) -function clause decode (0b000001 : (regno) rs : 0b10011 : (imm16) imm) = - Some(BCMPZ(rs, imm, GE, true, true)) (* BGEZALL *) - -function clause decode (0b000111 : (regno) rs : 0b00000 : (imm16) imm) = - Some(BCMPZ(rs, imm, GT, false, false)) (* BGTZ *) -function clause decode (0b010111 : (regno) rs : 0b00000 : (imm16) imm) = - Some(BCMPZ(rs, imm, GT, false, true)) (* BGTZL *) - -function clause decode (0b000110 : (regno) rs : 0b00000 : (imm16) imm) = - Some(BCMPZ(rs, imm, LE, false, false)) (* BLEZ *) -function clause decode (0b010110 : (regno) rs : 0b00000 : (imm16) imm) = - Some(BCMPZ(rs, imm, LE, false, true)) (* BLEZL *) - -function clause execute (BCMPZ(rs, imm, cmp, link, likely)) = - { - (bit[64]) linkVal := PC + 8; - regVal := rGPR(rs); - condition := compare(cmp, regVal, 0); - if (condition) then - { - let (bit[64]) offset = (EXTS(imm : 0b00) + 4) in - delayedPC := PC + offset; - branchPending := 1; - } - else if (likely) then - { - nextPC := PC + 8 (* skip branch delay *) - }; - if (link) then - wGPR(31) := linkVal - } - -(**************************************************************************************) -(* SYSCALL/BREAK/WAIT/Trap *) -(**************************************************************************************) - -(* Co-opt syscall 0xfffff for use as thread start in pccmem *) -union ast member unit SYSCALL_THREAD_START -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 ast member unit ImplementationDefinedStopFetching -function clause execute (ImplementationDefinedStopFetching) = () - - -union ast member unit SYSCALL -function clause decode (0b000000 : (bit[20]) code : 0b001100) = - Some(SYSCALL) (* code is ignored *) -function clause execute (SYSCALL) = - { - (SignalException(Sys)) - } - -(* BREAK is identical to SYSCALL exception for the exception raised *) -union ast member unit BREAK -function clause decode (0b000000 : (bit[20]) code : 0b001101) = - Some(BREAK) (* code is ignored *) -function clause execute (BREAK) = - { - (SignalException(Bp)) - } - -(* Accept WAIT as a NOP *) -union ast member unit WAIT -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 ast member (regno, regno, Comparison) TRAPREG -function clause decode (0b000000 : (regno) rs : (regno) rt : (bit[10]) code : 0b110000) = - Some(TRAPREG(rs, rt, GE)) (* TGE *) -function clause decode (0b000000 : (regno) rs : (regno) rt : (bit[10]) code : 0b110001) = - Some(TRAPREG(rs, rt, GEU)) (* TGEU *) -function clause decode (0b000000 : (regno) rs : (regno) rt : (bit[10]) code : 0b110010) = - Some(TRAPREG(rs, rt, LT)) (* TLT *) -function clause decode (0b000000 : (regno) rs : (regno) rt : (bit[10]) code : 0b110011) = - Some(TRAPREG(rs, rt, LTU)) (* TLTU *) -function clause decode (0b000000 : (regno) rs : (regno) rt : (bit[10]) code : 0b110100) = - Some(TRAPREG(rs, rt, EQ)) (* TEQ *) -function clause decode (0b000000 : (regno) rs : (regno) rt : (bit[10]) code : 0b110110) = - Some(TRAPREG(rs, rt, NE)) (* TNE *) -function clause 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 ast member (regno, imm16, Comparison) TRAPIMM -function clause decode (0b000001 : (regno) rs : 0b01100 : (imm16) imm) = - Some(TRAPIMM(rs, imm, EQ)) (* TEQI *) -function clause decode (0b000001 : (regno) rs : 0b01110 : (imm16) imm) = - Some(TRAPIMM(rs, imm, NE)) (* TNEI *) -function clause decode (0b000001 : (regno) rs : 0b01000 : (imm16) imm) = - Some(TRAPIMM(rs, imm, GE)) (* TGEI *) -function clause decode (0b000001 : (regno) rs : 0b01001 : (imm16) imm) = - Some(TRAPIMM(rs, imm, GEU)) (* TGEIU *) -function clause decode (0b000001 : (regno) rs : 0b01010 : (imm16) imm) = - Some(TRAPIMM(rs, imm, LT)) (* TLTI *) -function clause decode (0b000001 : (regno) rs : 0b01011 : (imm16) imm) = - Some(TRAPIMM(rs, imm, LTU)) (* TLTIU *) -function clause execute (TRAPIMM(rs, imm, cmp)) = - { - rs_val := rGPR(rs); - imm_val := EXTS(imm); - condition := compare(cmp, rs_val, imm_val); - if (condition) then - (SignalException(Tr)) - } - -(**************************************************************************************) -(* Load instructions -- various width/signs *) -(**************************************************************************************) - -union ast member (WordType, bool, bool, regno, regno, imm16) Load -function clause decode (0b100000 : (regno) base : (regno) rt : (imm16) offset) = - Some(Load(B, true, false, base, rt, offset)) (* LB *) -function clause decode (0b100100 : (regno) base : (regno) rt : (imm16) offset) = - Some(Load(B, false, false, base, rt, offset)) (* LBU *) -function clause decode (0b100001 : (regno) base : (regno) rt : (imm16) offset) = - Some(Load(H, true, false, base, rt, offset)) (* LH *) -function clause decode (0b100101 : (regno) base : (regno) rt : (imm16) offset) = - Some(Load(H, false, false, base, rt, offset)) (* LHU *) -function clause decode (0b100011 : (regno) base : (regno) rt : (imm16) offset) = - Some(Load(W, true, false, base, rt, offset)) (* LW *) -function clause decode (0b100111 : (regno) base : (regno) rt : (imm16) offset) = - Some(Load(W, false, false, base, rt, offset)) (* LWU *) -function clause decode (0b110111 : (regno) base : (regno) rt : (imm16) offset) = - Some(Load(D, false, false, base, rt, offset)) (* LD *) -function clause decode (0b110000 : (regno) base : (regno) rt : (imm16) offset) = - Some(Load(W, true, true, base, rt, offset)) (* LL *) -function clause decode (0b110100 : (regno) base : (regno) rt : (imm16) offset) = - Some(Load(D, false, true, base, rt, offset)) (* LLD *) -function clause execute (Load(width, signed, linked, base, rt, offset)) = - { - (bit[64]) vAddr := 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 := if (linked) then - { - CP0LLBit := 0b1; - CP0LLAddr := pAddr; - MEMr_reserve_wrapper(pAddr, wordWidthBytes(width)); - } - else - MEMr_wrapper(pAddr, wordWidthBytes(width)); - if (signed) then - wGPR(rt) := EXTS(memResult) - else - wGPR(rt) := EXTZ(memResult) - } - } - -(**************************************************************************************) -(* Store instructions -- various widths *) -(**************************************************************************************) - -union ast member (WordType, bool, regno, regno, imm16) Store -function clause decode (0b101000 : (regno) base : (regno) rt : (imm16) offset) = - Some(Store(B, false, base, rt, offset)) (* SB *) -function clause decode (0b101001 : (regno) base : (regno) rt : (imm16) offset) = - Some(Store(H, false, base, rt, offset)) (* SH *) -function clause decode (0b101011 : (regno) base : (regno) rt : (imm16) offset) = - Some(Store(W, false, base, rt, offset)) (* SW *) -function clause decode (0b111111 : (regno) base : (regno) rt : (imm16) offset) = - Some(Store(D, false, base, rt, offset)) (* SD *) -function clause decode (0b111000 : (regno) base : (regno) rt : (imm16) offset) = - Some(Store(W, true, base, rt, offset)) (* SC *) -function clause decode (0b111100 : (regno) base : (regno) rt : (imm16) offset) = - Some(Store(D, true, base, rt, offset)) (* SCD *) -function clause execute (Store(width, conditional, base, rt, offset)) = - { - (bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), StoreData, width); - (bit[64]) 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 := if (CP0LLBit[0]) then switch(width) - { - case B -> MEMw_conditional_wrapper(pAddr, 1, rt_val[7..0]) - case H -> MEMw_conditional_wrapper(pAddr, 2, rt_val[15..0]) - case W -> MEMw_conditional_wrapper(pAddr, 4, rt_val[31..0]) - case D -> MEMw_conditional_wrapper(pAddr, 8, rt_val) - } else false; - wGPR(rt) := EXTZ([success]) - } - else - switch(width) - { - case B -> MEMw_wrapper(pAddr, 1) := rt_val[7..0] - case H -> MEMw_wrapper(pAddr, 2) := rt_val[15..0] - case W -> MEMw_wrapper(pAddr, 4) := rt_val[31..0] - case D -> MEMw_wrapper(pAddr, 8) := rt_val - } - } - } - -(* LWL - Load word left (big-endian only) *) - -union ast member regregimm16 LWL -function clause decode(0b100010 : (regno) base : (regno) rt : (imm16) offset) = - Some(LWL(base, rt, offset)) -function clause execute(LWL(base, rt, offset)) = - { - (* XXX length check not quite right, but conservative *) - (bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), LoadData, W); - let pAddr = (TLBTranslate(vAddr, LoadData)) in - { - mem_val := MEMr_wrapper (pAddr[63..2] : 0b00, 4); (* read word of interest *) - reg_val := rGPR(rt); - wGPR(rt) := EXTS(switch(vAddr[1..0]) - { - case 0b00 -> mem_val - case 0b01 -> mem_val[23..0] : reg_val[07..0] - case 0b10 -> mem_val[15..0] : reg_val[15..0] - case 0b11 -> mem_val[07..0] : reg_val[23..0] - }); - } - } -union ast member regregimm16 LWR -function clause decode(0b100110 : (regno) base : (regno) rt : (imm16) offset) = - Some(LWR(base, rt, offset)) -function clause execute(LWR(base, rt, offset)) = - { - (* XXX length check not quite right, but conservative *) - (bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), LoadData, W); - let pAddr = (TLBTranslate(vAddr, LoadData)) in - { - mem_val := MEMr_wrapper (pAddr[63..2] : 0b00, 4); (* read word of interest *) - reg_val := rGPR(rt); - wGPR(rt) := EXTS(switch(vAddr[1..0]) (* it is acceptable to sign extend in all cases *) - { - case 0b00 -> reg_val[31..8] : mem_val[31..24] - case 0b01 -> reg_val[31..16] : mem_val[31..16] - case 0b10 -> reg_val[31..24] : mem_val[31..8] - case 0b11 -> mem_val - }); - } - } - -(* SWL - Store word left *) -union ast member regregimm16 SWL -function clause decode(0b101010 : (regno) base : (regno) rt : (imm16) offset) = - Some(SWL(base, rt, offset)) -function clause execute(SWL(base, rt, offset)) = - { - (* XXX length check not quite right, but conservative *) - (bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), StoreData, W); - let pAddr = (TLBTranslate(vAddr, StoreData)) in - { - reg_val := rGPR(rt); - switch (vAddr[1..0]) - { - case 0b00 -> (MEMw_wrapper(pAddr, 4) := reg_val[31..0]) - case 0b01 -> (MEMw_wrapper(pAddr, 3) := reg_val[31..8]) - case 0b10 -> (MEMw_wrapper(pAddr, 2) := reg_val[31..16]) - case 0b11 -> (MEMw_wrapper(pAddr, 1) := reg_val[31..24]) - } - } - } - -union ast member regregimm16 SWR -function clause decode(0b101110 : (regno) base : (regno) rt : (imm16) offset) = - Some(SWR(base, rt, offset)) -function clause execute(SWR(base, rt, offset)) = - { - (* XXX length check not quite right, but conservative *) - (bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), StoreData, W); - let (pAddr) = (TLBTranslate(vAddr, StoreData)) in - { - wordAddr := pAddr[63..2] : 0b00; - reg_val := rGPR(rt); - switch (vAddr[1..0]) - { - case 0b00 -> (MEMw_wrapper(wordAddr, 1) := reg_val[7..0]) - case 0b01 -> (MEMw_wrapper(wordAddr, 2) := reg_val[15..0]) - case 0b10 -> (MEMw_wrapper(wordAddr, 3) := reg_val[23..0]) - case 0b11 -> (MEMw_wrapper(wordAddr, 4) := reg_val[31..0]) - } - } - } - -(* Load double-word left *) -union ast member regregimm16 LDL -function clause decode(0b011010 : (regno) base : (regno) rt : (imm16) offset) = - Some(LDL(base, rt, offset)) -function clause execute(LDL(base, rt, offset)) = - { - (* XXX length check not quite right, but conservative *) - (bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), LoadData, D); - let pAddr = (TLBTranslate(vAddr, StoreData)) in - { - mem_val := MEMr_wrapper (pAddr[63..3] : 0b000, 8); (* read double of interest *) - reg_val := rGPR(rt); - wGPR(rt) := switch(vAddr[2..0]) - { - case 0b000 -> mem_val - case 0b001 -> mem_val[55..0] : reg_val[7..0] - case 0b010 -> mem_val[47..0] : reg_val[15..0] - case 0b011 -> mem_val[39..0] : reg_val[23..0] - case 0b100 -> mem_val[31..0] : reg_val[31..0] - case 0b101 -> mem_val[23..0] : reg_val[39..0] - case 0b110 -> mem_val[15..0] : reg_val[47..0] - case 0b111 -> mem_val[07..0] : reg_val[55..0] - }; - } - } - -(* Load double-word right *) -union ast member regregimm16 LDR -function clause decode(0b011011 : (regno) base : (regno) rt : (imm16) offset) = - Some(LDR(base, rt, offset)) -function clause execute(LDR(base, rt, offset)) = - { - (* XXX length check not quite right, but conservative *) - (bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), LoadData, D); - let pAddr = (TLBTranslate(vAddr, StoreData)) in - { - mem_val := MEMr_wrapper (pAddr[63..3] : 0b000, 8); (* read double of interest *) - reg_val := rGPR(rt); - wGPR(rt) := switch(vAddr[2..0]) - { - case 0b000 -> reg_val[63..08] : mem_val[63..56] - case 0b001 -> reg_val[63..16] : mem_val[63..48] - case 0b010 -> reg_val[63..24] : mem_val[63..40] - case 0b011 -> reg_val[63..32] : mem_val[63..32] - case 0b100 -> reg_val[63..40] : mem_val[63..24] - case 0b101 -> reg_val[63..48] : mem_val[63..16] - case 0b110 -> reg_val[63..56] : mem_val[63..08] - case 0b111 -> mem_val - }; - } - } - -(* SDL - Store double-word left *) -union ast member regregimm16 SDL -function clause decode(0b101100 : (regno) base : (regno) rt : (imm16) offset) = - Some(SDL(base, rt, offset)) -function clause execute(SDL(base, rt, offset)) = - { - (* XXX length check not quite right, but conservative *) - (bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), StoreData, D); - let pAddr = (TLBTranslate(vAddr, StoreData)) in - { - reg_val := rGPR(rt); - switch (vAddr[2..0]) - { - case 0b000 -> (MEMw_wrapper(pAddr, 8) := reg_val[63..00]) - case 0b001 -> (MEMw_wrapper(pAddr, 7) := reg_val[63..08]) - case 0b010 -> (MEMw_wrapper(pAddr, 6) := reg_val[63..16]) - case 0b011 -> (MEMw_wrapper(pAddr, 5) := reg_val[63..24]) - case 0b100 -> (MEMw_wrapper(pAddr, 4) := reg_val[63..32]) - case 0b101 -> (MEMw_wrapper(pAddr, 3) := reg_val[63..40]) - case 0b110 -> (MEMw_wrapper(pAddr, 2) := reg_val[63..48]) - case 0b111 -> (MEMw_wrapper(pAddr, 1) := reg_val[63..56]) - } - } - } - - -(* SDR - Store double-word right *) -union ast member regregimm16 SDR -function clause decode(0b101101 : (regno) base : (regno) rt : (imm16) offset) = - Some(SDR(base, rt, offset)) -function clause execute(SDR(base, rt, offset)) = - { - (* XXX length check not quite right, but conservative *) - (bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), StoreData, D); - let pAddr = (TLBTranslate(vAddr, StoreData)) in - { - reg_val := rGPR(rt); - wordAddr := pAddr[63..3] : 0b000; - switch (vAddr[2..0]) - { - case 0b000 -> (MEMw_wrapper(wordAddr, 1) := reg_val[07..0]) - case 0b001 -> (MEMw_wrapper(wordAddr, 2) := reg_val[15..0]) - case 0b010 -> (MEMw_wrapper(wordAddr, 3) := reg_val[23..0]) - case 0b011 -> (MEMw_wrapper(wordAddr, 4) := reg_val[31..0]) - case 0b100 -> (MEMw_wrapper(wordAddr, 5) := reg_val[39..0]) - case 0b101 -> (MEMw_wrapper(wordAddr, 6) := reg_val[47..0]) - case 0b110 -> (MEMw_wrapper(wordAddr, 7) := reg_val[55..0]) - case 0b111 -> (MEMw_wrapper(wordAddr, 8) := reg_val[63..0]) - } - } - } - -(* CACHE - manipulate (non-existent) caches *) - -union ast member regregimm16 CACHE -function clause decode (0b101111 : (regno) base : (regno) op : (imm16) imm) = - Some(CACHE(base, op, imm)) -function clause execute (CACHE(base, op, imm)) = - checkCP0Access () (* pretty much a NOP because no caches *) - -(* PREF - prefetching into (non-existent) caches *) - -union ast member regregimm16 PREF -function clause decode (0b110011 : (regno) base : (regno) op : (imm16) imm) = - Some(PREF(base, op, imm)) -function clause execute (PREF(base, op, imm)) = - () (* XXX NOP *) - - -(* SYNC - Memory barrier *) -union ast member unit SYNC -function clause decode (0b000000 : 0b00000 : 0b00000 : 0b00000 : (regno) stype : 0b001111) = - Some(SYNC()) (* stype is currently ignored *) -function clause execute(SYNC) = - MEM_sync() - -union ast member (regno, regno, bit[3], bool) MFC0 -function clause decode (0b010000 : 0b00000 : (regno) rt : (regno) rd : 0b00000000 : (bit[3]) sel) = - Some(MFC0(rt, rd, sel, false)) (* MFC0 *) -function clause decode (0b010000 : 0b00001 : (regno) rt : (regno) rd : 0b00000000 : (bit[3]) sel) = - Some(MFC0(rt, rd, sel, true)) (* DMFC0 *) -function clause execute (MFC0(rt, rd, sel, double)) = { - checkCP0Access(); - let (bit[64]) result = switch (rd, sel) - { - case (0b00000,0b000) -> let (bit[31]) idx = EXTZ(TLBIndex) in - (0x00000000 : [TLBProbe] : idx) (* 0, TLB Index *) - case (0b00001,0b000) -> EXTZ(TLBRandom) (* 1, TLB Random *) - case (0b00010,0b000) -> TLBEntryLo0 (* 2, TLB EntryLo0 *) - case (0b00011,0b000) -> TLBEntryLo1 (* 3, TLB EntryLo1 *) - case (0b00100,0b000) -> TLBContext (* 4, TLB Context *) - case (0b00101,0b000) -> EXTZ(TLBPageMask : 0x000) (* 5, TLB PageMask *) - case (0b00110,0b000) -> EXTZ(TLBWired) (* 6, TLB Wired *) - case (0b00111,0b000) -> EXTZ(CP0HWREna) (* 7, HWREna *) - case (0b01000,0b000) -> CP0BadVAddr (* 8, BadVAddr reg *) - case (0b01000,0b001) -> 0 (* 8, BadInstr reg XXX TODO *) - case (0b01001,0b000) -> EXTZ(CP0Count) (* 9, Count reg *) - case (0b01010,0b000) -> TLBEntryHi (* 10, TLB EntryHi *) - case (0b01011,0b000) -> EXTZ(CP0Compare) (* 11, Compare reg *) - case (0b01100,0b000) -> EXTZ(CP0Status) (* 12, Status reg *) - case (0b01101,0b000) -> EXTZ(CP0Cause) (* 13, Cause reg *) - case (0b01110,0b000) -> CP0EPC (* 14, EPC *) - case (0b01111,0b000) -> EXTZ(0x00000400) (* 15, sel 0: PrID processor ID *) - case (0b01111,0b110) -> 0 (* 15, sel 6: CHERI core ID *) - case (0b01111,0b111) -> 0 (* 15, sel 7: CHERI thread ID *) - case (0b10000,0b000) -> EXTZ(0b1 (* M *) (* 16, sel 0: Config0 *) - : 0b000000000000000 (* Impl *) - : 0b1 (* BE *) - : 0b10 (* AT *) - : 0b000 (* AR *) - : 0b001 (* MT standard TLB *) - : 0b0000 (* zero *) - : 0b000) - case (0b10000,0b001) -> EXTZ( (* 16, sel 1: Config1 *) - 0b1 (* M *) - : TLBIndexMax (* MMU size-1 *) - : 0b000 (* IS icache sets *) - : 0b000 (* IL icache lines *) - : 0b000 (* IA icache assoc. *) - : 0b000 (* DS dcache sets *) - : 0b000 (* DL dcache lines *) - : 0b000 (* DA dcache assoc. *) - : [have_cp2] (* C2 CP2 presence *) - : 0b0 (* MD MDMX implemented *) - : 0b0 (* PC performance counters *) - : 0b0 (* WR watch registers *) - : 0b0 (* CA 16e code compression *) - : 0b0 (* EP EJTAG *) - : 0b0) (* FP FPU present *) - case (0b10000,0b010) -> EXTZ( (* 16, sel 2: Config2 *) - 0b1 (* M *) - : 0b000 (* TU L3 control *) - : 0b0000 (* TS L3 sets *) - : 0b0000 (* TL L3 lines *) - : 0b0000 (* TA L3 assoc. *) - : 0b0000 (* SU L2 control *) - : 0b0000 (* SS L2 sets *) - : 0b0000 (* SL L2 lines *) - : 0b0000) (* SA L2 assoc. *) - case (0b10000,0b011) -> 0x0000000000002000 (* 16, sel 3: Config3 zero except for bit 13 == ulri *) - case (0b10000,0b101) -> 0x0000000000000000 (* 16, sel 5: Config5 beri specific -- no extended TLB *) - case (0b10001,0b000) -> CP0LLAddr (* 17, sel 0: LLAddr *) - case (0b10010,0b000) -> 0 (* 18, WatchLo *) - case (0b10011,0b000) -> 0 (* 19, WatchHi *) - case (0b10100,0b000) -> TLBXContext (* 20, XContext *) - case (0b11110,0b000) -> CP0ErrorEPC (* 30, ErrorEPC *) - case _ -> (SignalException(ResI)) - } in - wGPR(rt) := if (double) then result else EXTS(result[31..0]) -} - -(* simulator halt instruction "MTC0 rt, r23" (cheri specific behaviour) *) -union ast member unit HCF -function clause decode (0b010000 : 0b00100 : (regno) rt : 0b10111 : 0b00000000000) = - Some(HCF()) - -function clause decode (0b010000 : 0b00100 : (regno) rt : 0b11010 : 0b00000000000) = - Some(HCF()) - -function clause execute (HCF) = - () (* halt instruction actually executed by interpreter framework *) - -union ast member (regno, regno, bit[3], bool) MTC0 -function clause decode (0b010000 : 0b00100 : (regno) rt : (regno) rd : 0b00000000 : (bit[3]) sel) = - Some(MTC0(rt, rd, sel, false)) (* MTC0 *) -function clause decode (0b010000 : 0b00101 : (regno) rt : (regno) rd : 0b00000000 : (bit[3]) sel) = - Some(MTC0(rt, rd, sel, true)) (* DMTC0 *) -function clause execute (MTC0(rt, rd, sel, double)) = { - checkCP0Access(); - let reg_val = (rGPR(rt)) in - switch (rd, sel) - { - case (0b00000,0b000) -> TLBIndex := mask(reg_val) (* NB no write to TLBProbe *) - case (0b00001,0b000) -> () (* TLBRandom is read only *) - case (0b00010,0b000) -> TLBEntryLo0 := reg_val - case (0b00011,0b000) -> TLBEntryLo1 := reg_val - case (0b00100,0b000) -> (TLBContext.PTEBase) := (reg_val[63..23]) - case (0b00100,0b010) -> CP0UserLocal := reg_val - case (0b00101,0b000) -> TLBPageMask := (reg_val[28..13]) - case (0b00110,0b000) -> { - TLBWired := mask(reg_val); - TLBRandom := TLBIndexMax; - } - case (0b00111,0b000) -> CP0HWREna := (reg_val[31..29] : 0b0000000000000000000000000 : reg_val[3..0]) - case (0b01000,0b000) -> () (* BadVAddr read only *) - case (0b01001,0b000) -> CP0Count := reg_val[31..0] - case (0b01010,0b000) -> { - (TLBEntryHi.R) := (reg_val[63..62]); - (TLBEntryHi.VPN2) := (reg_val[39..13]); - (TLBEntryHi.ASID) := (reg_val[7..0]); - } - case (0b01011,0b000) -> { (* 11, sel 0: Compare reg *) - CP0Compare := reg_val[31..0]; - (CP0Cause[15]) := bitzero; - } - case (0b01100,0b000) -> { (* 12 Status *) - (CP0Status.CU) := reg_val[31..28]; - (CP0Status.BEV) := reg_val[22]; - (CP0Status.IM) := reg_val[15..8]; - (CP0Status.KX) := reg_val[7]; - (CP0Status.SX) := reg_val[6]; - (CP0Status.UX) := reg_val[5]; - (CP0Status.KSU) := reg_val[4..3]; - (CP0Status.ERL) := reg_val[2]; - (CP0Status.EXL) := reg_val[1]; - (CP0Status.IE) := reg_val[0]; - } - case (0b01101,0b000) -> { (* 13 Cause *) - CP0Cause.IV := reg_val[23]; (* TODO special interrupt vector not implemeneted *) - let ip = (bit[8]) (CP0Cause.IP) in - CP0Cause.IP := ((ip[7..2]) : (reg_val[9..8])); - } - case (0b01110,0b000) -> CP0EPC := reg_val (* 14, EPC *) - case (0b10000,0b000) -> () (* XXX ignore K0 cache config 16: Config0 *) - case (0b10100,0b000) -> (TLBXContext.PTEBase) := (reg_val[63..33]) - case (0b11110,0b000) -> CP0ErrorEPC := reg_val (* 30, ErrorEPC *) - case _ -> (SignalException(ResI)) - } -} - -function unit TLBWriteEntry((TLBIndexT) idx) = { - pagemask := EXTZ(TLBPageMask); (* XXX EXTZ here forces register read in ocaml shallow embedding *) - switch(pagemask) { - case 0x0000 -> () - case 0x0003 -> () - case 0x000f -> () - case 0x003f -> () - case 0x00ff -> () - case 0x03ff -> () - case 0x0fff -> () - case 0x3fff -> () - case 0xffff -> () - case _ -> (SignalException(MCheck)) - }; - ((TLBEntries[idx]).pagemask) := pagemask; - ((TLBEntries[idx]).r ) := TLBEntryHi.R; - ((TLBEntries[idx]).vpn2 ) := TLBEntryHi.VPN2; - ((TLBEntries[idx]).asid ) := TLBEntryHi.ASID; - ((TLBEntries[idx]).g ) := ((TLBEntryLo0.G) & (TLBEntryLo1.G)); - ((TLBEntries[idx]).valid ) := bitone; - ((TLBEntries[idx]).caps0 ) := TLBEntryLo0.CapS; - ((TLBEntries[idx]).capl0 ) := TLBEntryLo0.CapL; - ((TLBEntries[idx]).pfn0 ) := TLBEntryLo0.PFN; - ((TLBEntries[idx]).c0 ) := TLBEntryLo0.C; - ((TLBEntries[idx]).d0 ) := TLBEntryLo0.D; - ((TLBEntries[idx]).v0 ) := TLBEntryLo0.V; - ((TLBEntries[idx]).caps1 ) := TLBEntryLo1.CapS; - ((TLBEntries[idx]).capl1 ) := TLBEntryLo1.CapL; - ((TLBEntries[idx]).pfn1 ) := TLBEntryLo1.PFN; - ((TLBEntries[idx]).c1 ) := TLBEntryLo1.C; - ((TLBEntries[idx]).d1 ) := TLBEntryLo1.D; - ((TLBEntries[idx]).v1 ) := TLBEntryLo1.V; -} - -union ast member TLBWI -function clause decode (0b010000 : 0b10000000000000000000 : 0b000010) = Some(TLBWI) -function clause execute (TLBWI) = { - checkCP0Access(); - TLBWriteEntry(TLBIndex); -} - -union ast member TLBWR -function clause decode (0b010000 : 0b10000000000000000000 : 0b000110) = Some(TLBWR) -function clause execute (TLBWR) = { - checkCP0Access(); - TLBWriteEntry(TLBRandom); -} - -union ast member TLBR -function clause decode (0b010000 : 0b10000000000000000000 : 0b000001) = Some(TLBR) -function clause execute (TLBR) = { - checkCP0Access(); - let entry = TLBEntries[TLBIndex] in { - TLBPageMask := entry.pagemask; - TLBEntryHi.R := entry.r; - TLBEntryHi.VPN2 := entry.vpn2; - TLBEntryHi.ASID := entry.asid; - TLBEntryLo0.CapS:= entry.caps0; - TLBEntryLo0.CapL:= entry.capl0; - TLBEntryLo0.PFN := entry.pfn0; - TLBEntryLo0.C := entry.c0; - TLBEntryLo0.D := entry.d0; - TLBEntryLo0.V := entry.v0; - TLBEntryLo0.G := entry.g; - TLBEntryLo1.CapS:= entry.caps1; - TLBEntryLo1.CapL:= entry.capl1; - TLBEntryLo1.PFN := entry.pfn1; - TLBEntryLo1.C := entry.c1; - TLBEntryLo1.D := entry.d1; - TLBEntryLo1.V := entry.v1; - TLBEntryLo1.G := entry.g; - } -} - -union ast member TLBP -function clause decode (0b010000 : 0b10000000000000000000 : 0b001000) = Some(TLBP) -function clause execute ((TLBP)) = { - checkCP0Access(); - let result = tlbSearch(TLBEntryHi) in - switch(result) { - case (Some(idx)) -> { - TLBProbe := [bitzero]; - TLBIndex := idx; - } - case None -> { - TLBProbe := [bitone]; - TLBIndex := 0; - } - } -} - -union ast member (regno, regno) RDHWR -function clause decode (0b011111 : 0b00000 : (regno) rt : (regno) rd : 0b00000 : 0b111011) = - Some(RDHWR(rt, rd)) -function clause execute (RDHWR(rt, rd)) = { - let accessLevel = getAccessLevel() in - if ((accessLevel != Kernel) & (~((CP0Status.CU)[0])) & ~(CP0HWREna[rd])) then - (SignalException(ResI)); - let (bit[64]) temp = switch (rd) { - case 0b00000 -> EXTZ([bitzero]) (* CPUNum *) - case 0b00001 -> EXTZ([bitzero]) (* SYNCI_step *) - case 0b00010 -> EXTZ(CP0Count) (* Count *) - case 0b00011 -> EXTZ([bitone]) (* Count resolution *) - case 0b11101 -> CP0UserLocal (* User local register *) - case _ -> (SignalException(ResI)) - } in - wGPR(rt) := temp; -} - -union ast member unit ERET -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 := 0; - } - else - { - nextPC := CP0EPC; - CP0Status.EXL := 0; - } - } diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail deleted file mode 100644 index c3197eda..00000000 --- a/mips/mips_prelude.sail +++ /dev/null @@ -1,609 +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) *) - -(* bit vectors have indices decreasing from left i.e. msb is highest index *) -default Order dec - -register (bit[64]) PC -register (bit[64]) nextPC - -(* CP0 Registers *) - -typedef CauseReg = register bits [ 31 : 0 ] { - 31 : BD; (* branch delay *) - (*30 : Z0;*) - 29 .. 28 : CE; (* for coprocessor enable exception *) - (*27 .. 24 : Z1;*) - 23 : IV; (* special interrupt vector not supported *) - 22 : WP; (* watchpoint exception occurred *) - (*21 .. 16 : Z2; *) - 15 .. 8 : IP; (* interrupt pending bits *) - (*7 : Z3;*) - 6 .. 2 : ExcCode; (* code of last exception *) - (*1 .. 0 : Z4;*) -} - -typedef TLBEntryLoReg = register bits [63 : 0] { - 63 : CapS; - 62 : CapL; - 29 .. 6 : PFN; - 5 .. 3 : C; - 2 : D; - 1 : V; - 0 : G; -} - -typedef TLBEntryHiReg = register bits [63 : 0] { - 63 .. 62 : R; - 39 .. 13 : VPN2; - 7 .. 0 : ASID; -} - -typedef ContextReg = register bits [63 : 0] { - 63 .. 23 : PTEBase; - 22 .. 4 : BadVPN2; - (*3 .. 0 : ZR;*) -} - -typedef XContextReg = register bits [63 : 0] { - 63 .. 33: PTEBase; - 32 .. 31: R; - 30 .. 4: BadVPN2; -} - -let ([:64:]) TLBNumEntries = 64 -typedef TLBIndexT = (bit[6]) -let (TLBIndexT) TLBIndexMax = 0b111111 - -let MAX_U64 = unsigned(0xffffffffffffffff) -let MAX_VA = unsigned(0xffffffffff) -let MAX_PA = unsigned(0xfffffffff) - -typedef TLBEntry = register bits [116 : 0] { - 116 .. 101: pagemask; - 100 .. 99 : r ; - 98 .. 72 : vpn2 ; - 71 .. 64 : asid ; - 63 : g ; - 62 : valid ; - 61 : caps1 ; - 60 : capl1 ; - 59 .. 36 : pfn1 ; - 35 .. 33 : c1 ; - 32 : d1 ; - 31 : v1 ; - 30 : caps0 ; - 29 : capl0 ; - 28 .. 5 : pfn0 ; - 4 .. 2 : c0 ; - 1 : d0 ; - 0 : v0 ; -} - -register (bit[1]) TLBProbe -register (TLBIndexT) TLBIndex -register (TLBIndexT) TLBRandom -register (TLBEntryLoReg) TLBEntryLo0 -register (TLBEntryLoReg) TLBEntryLo1 -register (ContextReg) TLBContext -register (bit[16]) TLBPageMask -register (TLBIndexT) TLBWired -register (TLBEntryHiReg) TLBEntryHi -register (XContextReg) TLBXContext - -register (TLBEntry) TLBEntry00 -register (TLBEntry) TLBEntry01 -register (TLBEntry) TLBEntry02 -register (TLBEntry) TLBEntry03 -register (TLBEntry) TLBEntry04 -register (TLBEntry) TLBEntry05 -register (TLBEntry) TLBEntry06 -register (TLBEntry) TLBEntry07 -register (TLBEntry) TLBEntry08 -register (TLBEntry) TLBEntry09 -register (TLBEntry) TLBEntry10 -register (TLBEntry) TLBEntry11 -register (TLBEntry) TLBEntry12 -register (TLBEntry) TLBEntry13 -register (TLBEntry) TLBEntry14 -register (TLBEntry) TLBEntry15 -register (TLBEntry) TLBEntry16 -register (TLBEntry) TLBEntry17 -register (TLBEntry) TLBEntry18 -register (TLBEntry) TLBEntry19 -register (TLBEntry) TLBEntry20 -register (TLBEntry) TLBEntry21 -register (TLBEntry) TLBEntry22 -register (TLBEntry) TLBEntry23 -register (TLBEntry) TLBEntry24 -register (TLBEntry) TLBEntry25 -register (TLBEntry) TLBEntry26 -register (TLBEntry) TLBEntry27 -register (TLBEntry) TLBEntry28 -register (TLBEntry) TLBEntry29 -register (TLBEntry) TLBEntry30 -register (TLBEntry) TLBEntry31 -register (TLBEntry) TLBEntry32 -register (TLBEntry) TLBEntry33 -register (TLBEntry) TLBEntry34 -register (TLBEntry) TLBEntry35 -register (TLBEntry) TLBEntry36 -register (TLBEntry) TLBEntry37 -register (TLBEntry) TLBEntry38 -register (TLBEntry) TLBEntry39 -register (TLBEntry) TLBEntry40 -register (TLBEntry) TLBEntry41 -register (TLBEntry) TLBEntry42 -register (TLBEntry) TLBEntry43 -register (TLBEntry) TLBEntry44 -register (TLBEntry) TLBEntry45 -register (TLBEntry) TLBEntry46 -register (TLBEntry) TLBEntry47 -register (TLBEntry) TLBEntry48 -register (TLBEntry) TLBEntry49 -register (TLBEntry) TLBEntry50 -register (TLBEntry) TLBEntry51 -register (TLBEntry) TLBEntry52 -register (TLBEntry) TLBEntry53 -register (TLBEntry) TLBEntry54 -register (TLBEntry) TLBEntry55 -register (TLBEntry) TLBEntry56 -register (TLBEntry) TLBEntry57 -register (TLBEntry) TLBEntry58 -register (TLBEntry) TLBEntry59 -register (TLBEntry) TLBEntry60 -register (TLBEntry) TLBEntry61 -register (TLBEntry) TLBEntry62 -register (TLBEntry) TLBEntry63 - -let (vector <0, 64, inc, (TLBEntry)>) TLBEntries = [ -TLBEntry00, -TLBEntry01, -TLBEntry02, -TLBEntry03, -TLBEntry04, -TLBEntry05, -TLBEntry06, -TLBEntry07, -TLBEntry08, -TLBEntry09, -TLBEntry10, -TLBEntry11, -TLBEntry12, -TLBEntry13, -TLBEntry14, -TLBEntry15, -TLBEntry16, -TLBEntry17, -TLBEntry18, -TLBEntry19, -TLBEntry20, -TLBEntry21, -TLBEntry22, -TLBEntry23, -TLBEntry24, -TLBEntry25, -TLBEntry26, -TLBEntry27, -TLBEntry28, -TLBEntry29, -TLBEntry30, -TLBEntry31, -TLBEntry32, -TLBEntry33, -TLBEntry34, -TLBEntry35, -TLBEntry36, -TLBEntry37, -TLBEntry38, -TLBEntry39, -TLBEntry40, -TLBEntry41, -TLBEntry42, -TLBEntry43, -TLBEntry44, -TLBEntry45, -TLBEntry46, -TLBEntry47, -TLBEntry48, -TLBEntry49, -TLBEntry50, -TLBEntry51, -TLBEntry52, -TLBEntry53, -TLBEntry54, -TLBEntry55, -TLBEntry56, -TLBEntry57, -TLBEntry58, -TLBEntry59, -TLBEntry60, -TLBEntry61, -TLBEntry62, -TLBEntry63 -] - -register (bit[32]) CP0Compare -register (CauseReg) CP0Cause -register (bit[64]) CP0EPC -register (bit[64]) CP0ErrorEPC -register (bit[1]) CP0LLBit -register (bit[64]) CP0LLAddr -register (bit[64]) CP0BadVAddr -register (bit[32]) CP0Count -register (bit[32]) CP0HWREna -register (bit[64]) CP0UserLocal - -typedef StatusReg = register bits [31:0] { - 31 .. 28 : CU; (* co-processor enable bits *) - (* RP/FR/RE/MX/PX not implemented *) - 22 : BEV; (* use boot exception vectors (initialised to one) *) - (* TS/SR/NMI not implemented *) - 15 .. 8 : IM; (* Interrupt mask *) - 7 : KX; (* kernel 64-bit enable *) - 6 : SX; (* supervisor 64-bit enable *) - 5 : UX; (* user 64-bit enable *) - 4 .. 3 : KSU; (* Processor mode *) - 2 : ERL; (* error level (should be initialised to one, but BERI is different) *) - 1 : EXL; (* exception level *) - 0 : IE; (* interrupt enable *) -} -register (StatusReg) CP0Status - -(* Implementation registers -- not ISA defined *) -register (bit[1]) branchPending (* Set by branch instructions to implement branch delay *) -register (bit[1]) inBranchDelay (* Needs to be set by outside world when in branch delay slot *) -register (bit[64]) delayedPC (* Set by branch instructions to implement branch delay *) - -(* General purpose registers *) - -register (bit[64]) GPR00 (* should never be read or written *) -register (bit[64]) GPR01 -register (bit[64]) GPR02 -register (bit[64]) GPR03 -register (bit[64]) GPR04 -register (bit[64]) GPR05 -register (bit[64]) GPR06 -register (bit[64]) GPR07 -register (bit[64]) GPR08 -register (bit[64]) GPR09 -register (bit[64]) GPR10 -register (bit[64]) GPR11 -register (bit[64]) GPR12 -register (bit[64]) GPR13 -register (bit[64]) GPR14 -register (bit[64]) GPR15 -register (bit[64]) GPR16 -register (bit[64]) GPR17 -register (bit[64]) GPR18 -register (bit[64]) GPR19 -register (bit[64]) GPR20 -register (bit[64]) GPR21 -register (bit[64]) GPR22 -register (bit[64]) GPR23 -register (bit[64]) GPR24 -register (bit[64]) GPR25 -register (bit[64]) GPR26 -register (bit[64]) GPR27 -register (bit[64]) GPR28 -register (bit[64]) GPR29 -register (bit[64]) GPR30 -register (bit[64]) GPR31 - -(* Special registers For MUL/DIV *) -register (bit[64]) HI -register (bit[64]) LO - -let (vector <0, 32, inc, (register<(bit[64])>) >) GPR = - [ GPR00, GPR01, GPR02, GPR03, GPR04, GPR05, GPR06, GPR07, GPR08, GPR09, GPR10, - GPR11, GPR12, GPR13, GPR14, GPR15, GPR16, GPR17, GPR18, GPR19, GPR20, - GPR21, GPR22, GPR23, GPR24, GPR25, GPR26, GPR27, GPR28, GPR29, GPR30, GPR31 - ] - -(* JTAG Uart registers *) - -register (bit[8]) UART_WDATA -register (bit[1]) UART_WRITTEN -register (bit[8]) UART_RDATA -register (bit[1]) UART_RVALID - -(* Check whether a given 64-bit vector is a properly sign extended 32-bit word *) -val bit[64] -> bool effect pure NotWordVal -function bool NotWordVal (word) = - (word[31] ^^ 32) != word[63..32] - -(* Read numbered GP reg. (r0 is always zero) *) -val bit[5] -> bit[64] effect {rreg} rGPR -function bit[64] rGPR idx = { - if idx == 0 then 0 else GPR[idx] -} - -(* Write numbered GP reg. (writes to r0 ignored) *) -val (bit[5], bit[64]) -> unit effect {wreg} wGPR -function unit wGPR (idx, v) = { - if idx == 0 then () else GPR[idx] := v -} - -val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr -val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr_reserve -val extern unit -> unit effect { barr } MEM_sync - -val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea -val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_conditional -val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval -val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> bool effect { wmv } MEMval_conditional - -typedef Exception = enumerate -{ - Int; TLBMod; TLBL; TLBS; AdEL; AdES; Sys; Bp; ResI; CpU; Ov; Tr; C2E; C2Trap; - XTLBRefillL; XTLBRefillS; XTLBInvL; XTLBInvS; MCheck -} - -(* Return the ISA defined code for an exception condition *) -function (bit[5]) ExceptionCode ((Exception) ex) = - switch (ex) - { - case Int -> mask(0x00) (* Interrupt *) - case TLBMod -> mask(0x01) (* TLB modification exception *) - case TLBL -> mask(0x02) (* TLB exception (load or fetch) *) - case TLBS -> mask(0x03) (* TLB exception (store) *) - case AdEL -> mask(0x04) (* Address error (load or fetch) *) - case AdES -> mask(0x05) (* Address error (store) *) - case Sys -> mask(0x08) (* Syscall *) - case Bp -> mask(0x09) (* Breakpoint *) - case ResI -> mask(0x0a) (* Reserved instruction *) - case CpU -> mask(0x0b) (* Coprocessor Unusable *) - case Ov -> mask(0x0c) (* Arithmetic overflow *) - case Tr -> mask(0x0d) (* Trap *) - case C2E -> mask(0x12) (* C2E coprocessor 2 exception *) - case C2Trap -> mask(0x12) (* C2Trap maps to same exception code, different vector *) - case XTLBRefillL -> mask(0x02) - case XTLBRefillS -> mask(0x03) - case XTLBInvL -> mask(0x02) - case XTLBInvS -> mask(0x03) - case MCheck -> mask(0x18) - } - - - -function forall Type 'o. 'o SignalExceptionMIPS ((Exception) ex, (bit[64]) 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 := 1; - } - else - { - CP0EPC := PC; - CP0Cause.BD := 0; - } - }; - - (* 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 *) - (bit[64]) vectorBase := if CP0Status.BEV then - 0xFFFFFFFFBFC00200 - else - 0xFFFFFFFF80000000; - (* On CHERI we have to subtract KCC.base so that we end up at the - right absolute vector address after indirecting via new PCC *) - nextPC := ((bit[64])(vectorBase + EXTS(vectorOffset))) - kccBase; - CP0Cause.ExcCode := ExceptionCode(ex); - CP0Status.EXL := 1; - exit (); - } - -val forall Type 'o . Exception -> 'o effect {escape, rreg, wreg} SignalException - -function forall Type 'o. 'o SignalExceptionBadAddr((Exception) ex, (bit[64]) badAddr) = - { - CP0BadVAddr := badAddr; - SignalException(ex); - } - -function forall Type 'o. 'o SignalExceptionTLB((Exception) ex, (bit[64]) badAddr) = { - CP0BadVAddr := badAddr; - (TLBContext.BadVPN2) := (badAddr[31..13]); - (TLBXContext.BadVPN2):= (badAddr[39..13]); - (TLBXContext.R) := (badAddr[63..62]); - (TLBEntryHi.R) := (badAddr[63..62]); - (TLBEntryHi.VPN2) := (badAddr[39..13]); - SignalException(ex); -} - -typedef MemAccessType = enumerate {Instruction; LoadData; StoreData} -typedef AccessLevel = enumerate {User; Supervisor; Kernel} - -function AccessLevel getAccessLevel() = - if ((CP0Status.EXL) | (CP0Status.ERL)) then - Kernel - else switch (CP0Status.KSU) - { - case 0b00 -> Kernel - case 0b01 -> Supervisor - case 0b10 -> User - case _ -> User (* behaviour undefined, assume user *) - } - -function ([|2|]) int_of_accessLevel((AccessLevel)x) = - switch (x) { - case User -> 0 - case Supervisor -> 1 - case Kernel -> 2 - } - -function unit checkCP0Access () = - { - let accessLevel = getAccessLevel() in - if ((accessLevel != Kernel) & (~(CP0Status[28] (*CU0*)))) then - { - (CP0Cause.CE) := 0b00; - SignalException(CpU); - } - } - -function unit incrementCP0Count() = { - TLBRandom := (if (TLBRandom == TLBWired) - then (TLBIndexMax) else (TLBRandom - 1)); - - CP0Count := (CP0Count + 1); - if (CP0Count == CP0Compare) then { - (CP0Cause[15]) := bitone; (* XXX indexing IP field here doesn't seem to work *) - }; - - let (bit[8]) ims = CP0Status.IM in - let (bit[8]) ips = CP0Cause.IP in - let ie = CP0Status.IE in - let exl = CP0Status.EXL in - let erl = CP0Status.ERL in - if ((~(exl)) & (~(erl)) & ie & ((ips & ims) != 0x00)) then - SignalException(Int); -} - -typedef regno = bit[5] (* a register number *) -typedef imm16 = bit[16] (* 16-bit immediate *) -(* a commonly used instruction format with three register operands *) -typedef regregreg = (regno, regno, regno) -(* a commonly used instruction format with two register operands and 16-bit immediate *) -typedef regregimm16 = (regno, regno, imm16) - -typedef decode_failure = enumerate { - no_matching_pattern; - unsupported_instruction; - illegal_instruction; - internal_error -} - -(* Used by branch and trap instructions *) -typedef Comparison = enumerate { - EQ; (* equal *) - NE; (* not equal *) - GE; (* signed greater than or equal *) - GEU;(* unsigned greater than or equal *) - GT; (* signed strictly greater than *) - LE; (* signed less than or equal *) - LT; (* signed strictly less than *) - LTU;(* unsigned less than or qual *) -} -function bool compare ((Comparison)cmp, (bit[64]) valA, (bit[64]) valB) = - (* sail comparisons are signed so extend to 65 bits for unsigned comparisons *) - let valA65 = (0b0 : valA) in - let valB65 = (0b0 : valB) in - switch(cmp) { - case EQ -> valA == valB - case NE -> valA != valB - case GE -> valA >= valB - case GEU -> valA65 >= valB65 - case GT -> valA > valB - case LE -> valA <= valB - case LT -> valA < valB - case LTU -> valA65 < valB65 - } -typedef WordType = enumerate { B; H; W; D} - -function forall Nat 'r, 'r IN {1,2,4,8}.[:'r:] wordWidthBytes((WordType) w) = - switch(w) { - case B -> 1 - case H -> 2 - case W -> 4 - case 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) = - switch (wordType) { - case B -> true - case H -> (addr[0] == 0) - case W -> (addr[1..0] == 0b00) - case 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 -function (bool) isAddressAligned (addr, (WordType) wordType) = - let a = unsigned(addr) in - ((a quot alignment_width) == (a + wordWidthBytes(wordType) - 1) quot alignment_width) - -val forall Nat 'W. bit[8 * 'W] -> bit[8 * 'W] effect pure reverse_endianness -function rec forall Nat 'W . bit[8 * 'W] reverse_endianness ((bit[8 * 'W]) value) = -{ - (nat) width := length(value); - if width <= 8 then value - else value[7..0] : reverse_endianness(value[(width - 1) .. 8]) -} - -function forall Nat 'n. (bit[8 * 'n]) effect { rmem } MEMr_wrapper ((bit[64]) addr, ([:'n:]) size) = - if (addr == 0x000000007f000000) then - { - let rvalid = (bit[1]) UART_RVALID in - let rdata = 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 *) - -function forall Nat 'n. (bit[8 * 'n]) effect { rmem } MEMr_reserve_wrapper ((bit[64]) addr , ([:'n:]) size) = - reverse_endianness(MEMr_reserve(addr, size)) diff --git a/mips/mips_regfp.sail b/mips/mips_regfp.sail deleted file mode 100644 index 13165f67..00000000 --- a/mips/mips_regfp.sail +++ /dev/null @@ -1,451 +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 (vector <0, 32, inc, string >) GPRs = - [ "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 (instr) = { - iR := [|| ||]; - oR := [|| ||]; - aR := [|| ||]; - ik := IK_simple; - Nias := [|| ||]; - Dia := DIAFP_none; - - switch instr { - case (DADDIU (rs, rt, imm)) -> { - if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR; - if rt == 0 then () else oR := RFull(GPRs[rt]) :: oR; - } - case (DADDU (rs, rt, rd)) -> { - if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR; - if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR; - if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR; - } - case (DADDI (rs, rt, imm)) -> { - if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR; - if rt == 0 then () else oR := RFull(GPRs[rt]) :: oR; - } - case (DADD (rs, rt, rd)) -> { - if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR; - if rt == 0 then () else oR := RFull(GPRs[rt]) :: oR; - } - case (ADD(rs, rt, rd)) -> { - if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR; - if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR; - if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR; - } - case (ADDI(rs, rt, imm)) -> { - if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR; - if rt == 0 then () else oR := RFull(GPRs[rt]) :: oR; - } - case (ADDU(rs, rt, rd)) -> { - if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR; - if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR; - if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR; - } - case (ADDIU(rs, rt, imm)) -> { - if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR; - if rt == 0 then () else oR := RFull(GPRs[rt]) :: oR; - } - case (DSUBU (rs, rt, rd)) -> { - if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR; - if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR; - if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR; - } - case (DSUB (rs, rt, rd)) -> { - if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR; - if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR; - if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR; - } - case (SUB(rs, rt, rd)) -> { - if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR; - if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR; - if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR; - } - case (SUBU(rs, rt, rd)) -> { - if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR; - if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR; - if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR; - } - case (AND (rs, rt, rd)) -> { - if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR; - if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR; - if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR; - } - case (ANDI (rs, rt, imm)) -> { - if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR; - if rt == 0 then () else oR := RFull(GPRs[rt]) :: oR; - } - case (OR (rs, rt, rd)) -> { - if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR; - if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR; - if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR; - } - case (ORI (rs, rt, imm)) -> { - if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR; - if rt == 0 then () else oR := RFull(GPRs[rt]) :: oR; - } - case (NOR (rs, rt, rd)) -> { - if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR; - if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR; - if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR; - } - case (XOR (rs, rt, rd)) -> { - if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR; - if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR; - if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR; - } - case (XORI (rs, rt, imm)) -> { - if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR; - if rt == 0 then () else oR := RFull(GPRs[rt]) :: oR; - } - case (LUI (rt, imm)) -> { - if rt == 0 then () else oR := RFull(GPRs[rt]) :: oR; - } - case (DSLL (rt, rd, sa)) -> { - if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR; - if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR; - } - case (DSLL32 (rt, rd, sa)) -> { - if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR; - if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR; - } - case (DSLLV (rs, rt, rd)) -> { - if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR; - if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR; - if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR; - } - case (DSRA (rt, rd, sa)) -> { - if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR; - if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR; - } - case (DSRA32 (rt, rd, sa)) -> { - if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR; - if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR; - } - case (DSRAV (rs, rt, rd)) -> { - if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR; - if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR; - if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR; - } - case (DSRL (rt, rd, sa)) -> { - if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR; - if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR; - } - case (DSRL32 (rt, rd, sa)) -> { - if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR; - if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR; - } - case (DSRLV (rs, rt, rd)) -> { - if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR; - if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR; - if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR; - } - case (SLL(rt, rd, sa)) -> { - if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR; - if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR; - } - case (SLLV(rs, rt, rd)) -> { - if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR; - if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR; - if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR; - } - case (SRA(rt, rd, sa)) -> { - if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR; - if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR; - } - case (SRAV(rs, rt, rd)) -> { - if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR; - if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR; - if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR; - } - case (SRL(rt, rd, sa)) -> { - if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR; - if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR; - } - case (SRLV(rs, rt, rd)) -> { - if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR; - if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR; - if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR; - } - case (SLT(rs, rt, rd)) -> { - if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR; - if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR; - if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR; - } - case (SLTI(rs, rt, imm)) -> { - if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR; - if rt == 0 then () else oR := RFull(GPRs[rt]) :: oR; - } - case (SLTU(rs, rt, rd)) -> { - if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR; - if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR; - if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR; - } - case (SLTIU(rs, rt, imm)) -> { - if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR; - if rt == 0 then () else oR := RFull(GPRs[rt]) :: oR; - } - case (MOVN(rs, rt, rd)) -> { - (* XXX don't always write rd *) - if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR; - if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR; - if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR; - } - case (MOVZ(rs, rt, rd)) -> { - (* XXX don't always write rd *) - if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR; - if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR; - if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR; - } - case (MFHI(rd)) -> { - iR := RFull("HI") :: iR; - if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR; - } - case (MFLO(rd)) -> { - iR := RFull("LO") :: iR; - if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR; - } - case (MTHI(rs)) -> { - oR := RFull("HI") :: oR; - if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR; - } - case (MTLO(rs)) -> { - oR := RFull("LO") :: oR; - if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR; - } - case (MUL(rs, rt, rd)) -> { - if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR; - if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR; - if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR; - } - case (MULT(rs, rt)) -> { - if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR; - if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR; - oR := RFull("HI") :: RFull ("LO") :: oR; - } - case (MULTU(rs, rt)) -> { - if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR; - if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR; - oR := RFull("HI") :: RFull ("LO") :: oR; - } - case (DMULT(rs, rt)) -> { - if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR; - if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR; - oR := RFull("HI") :: RFull ("LO") :: oR; - } - case (DMULTU(rs, rt)) -> { - if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR; - if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR; - oR := RFull("HI") :: RFull ("LO") :: oR; - } - case (MADD(rs, rt)) -> { - if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR; - if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR; - iR := RFull("HI") :: RFull ("LO") :: iR; - oR := RFull("HI") :: RFull ("LO") :: oR; - } - case (MADDU(rs, rt)) -> { - if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR; - if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR; - iR := RFull("HI") :: RFull ("LO") :: iR; - oR := RFull("HI") :: RFull ("LO") :: oR; - } - case (MSUB(rs, rt)) -> { - if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR; - if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR; - iR := RFull("HI") :: RFull ("LO") :: iR; - oR := RFull("HI") :: RFull ("LO") :: oR; - } - case (MSUBU(rs, rt)) -> { - if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR; - if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR; - iR := RFull("HI") :: RFull ("LO") :: iR; - oR := RFull("HI") :: RFull ("LO") :: oR; - } - case (DIV(rs, rt)) -> { - if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR; - if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR; - oR := RFull("HI") :: RFull ("LO") :: oR; - } - case (DIVU(rs, rt)) -> { - if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR; - if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR; - oR := RFull("HI") :: RFull ("LO") :: oR; - } - case (DDIV(rs, rt)) -> { - if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR; - if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR; - oR := RFull("HI") :: RFull ("LO") :: oR; - } - case (DDIVU(rs, rt)) -> { - if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR; - if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR; - oR := RFull("HI") :: RFull ("LO") :: oR; - } - case (J(offset)) -> { - ik := IK_branch; - Dia := DIAFP_concrete((PC + 4)[63..28] : offset : 0b00); - } - case (JAL(offset)) -> { - ik := IK_branch; - oR := RFull("GPR31") :: oR; - Dia := DIAFP_concrete((PC + 4)[63..28] : offset : 0b00); - } - case (JR(rs)) -> { - ik := IK_branch; - iR := RFull(GPRs[rs]) :: iR; - Dia := DIAFP_reg(RFull(GPRs[rs])); - } - case (JALR(rs, rd)) -> { - ik := IK_branch; - iR := RFull(GPRs[rs]) :: iR; - oR := RFull("GPR31") :: oR; - Dia := DIAFP_reg(RFull(GPRs[rs])); - } - case (BEQ(rs, rd, imm, ne, likely)) -> { - ik := IK_branch; - if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR; - if rd == 0 then () else iR := RFull(GPRs[rd]) :: iR; - let (bit[64]) offset = (EXTS(imm : 0b00) + 4) in - Dia := DIAFP_concrete (PC + offset); - } - case (BCMPZ(rs, imm, cmp, link, likely)) -> { - ik := IK_branch; - if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR; - if link then - oR := RFull("GPR31") :: oR; - let (bit[64]) offset = (EXTS(imm : 0b00) + 4) in - Dia := DIAFP_concrete (PC + offset); - } - case (SYSCALL_THREAD_START) -> () -(* - - case (SYSCALL) = - case (BREAK) = - case (WAIT) = { - case (TRAPREG(rs, rt, cmp)) = - case (TRAPIMM(rs, imm, cmp)) = -*) - case (Load(width, signed, linked, base, rt, offset)) -> { - ik := IK_mem_read (if linked then Read_reserve else Read_plain); - if linked then oR := RFull("CP0LLBit")::RFull("CP0LLAddr")::oR else (); - if base == 0 then () else aR := RFull(GPRs[base]) :: aR; - iR := aR; - if rt == 0 then () else oR := RFull(GPRs[rt]) :: oR; - } - case (Store(width, conditional, base, rt, offset)) -> { - ik := IK_mem_write(if conditional then Write_conditional else Write_plain); - if base == 0 then () else aR := RFull(GPRs[base]) :: aR; - iR := aR; - if conditional then iR := RFull("CP0LLBit")::iR else (); - if (conditional & (rt != 0)) then oR := RFull(GPRs[rt])::oR else (); - if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR; - } - case (LWL(base, rt, offset)) -> { - ik := IK_mem_read(Read_plain); - if base == 0 then () else aR := RFull(GPRs[base]) :: aR; - iR := aR; - if rt == 0 then () else oR := RFull(GPRs[rt]) :: oR; - } - case (LWR(base, rt, offset)) -> { - ik := IK_mem_read(Read_plain); - if base == 0 then () else aR := RFull(GPRs[base]) :: aR; - iR := aR; - if rt == 0 then () else oR := RFull(GPRs[rt]) :: oR; - } - case (SWL(base, rt, offset)) -> { - ik := IK_mem_write(Write_plain); - if base == 0 then () else aR := RFull(GPRs[base]) :: aR; - iR := aR; - if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR; - } - case (SWR(base, rt, offset)) -> { - ik := IK_mem_write(Write_plain); - if base == 0 then () else aR := RFull(GPRs[base]) :: aR; - iR := aR; - if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR; - } - case (LDL(base, rt, offset)) -> { - ik := IK_mem_read(Read_plain); - if base == 0 then () else aR := RFull(GPRs[base]) :: aR; - iR := aR; - if rt == 0 then () else oR := RFull(GPRs[rt]) :: oR; - } - case (LDR(base, rt, offset)) -> { - ik := IK_mem_read(Read_plain); - if base == 0 then () else aR := RFull(GPRs[base]) :: aR; - iR := aR; - if rt == 0 then () else oR := RFull(GPRs[rt]) :: oR; - } - case (SDL(base, rt, offset)) -> { - ik := IK_mem_write(Write_plain); - if base == 0 then () else aR := RFull(GPRs[base]) :: aR; - iR := aR; - if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR; - } - case (SDR(base, rt, offset)) -> { - ik := IK_mem_write(Write_plain); - if base == 0 then () else aR := RFull(GPRs[base]) :: aR; - iR := aR; - if rt == 0 then () else iR := RFull(GPRs[rt]) :: iR; - } -(* - case (CACHE(base, op, imm)) = - case (PREF(base, op, imm)) = -*) - case (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/mips_ri.sail b/mips/mips_ri.sail deleted file mode 100644 index 3f368111..00000000 --- a/mips/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 ast member unit RI -function clause decode _ = Some(RI) -function clause execute (RI) = - SignalException (ResI) - diff --git a/mips/mips_tlb.sail b/mips/mips_tlb.sail deleted file mode 100644 index d72e0e75..00000000 --- a/mips/mips_tlb.sail +++ /dev/null @@ -1,128 +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. *) -(*========================================================================*) - -function bool tlbEntryMatch(r, vpn2, asid, (TLBEntry) 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 - (entryValid & - (r == entryR) & - ((vpn2 & ~(EXTZ(entryMask))) == ((entryVPN) & ~(EXTZ(entryMask)))) & - ((asid == (entryASID)) | (entryG))) - -function option<TLBIndexT> tlbSearch((bit[64]) 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, (TLBEntries[idx]))) then - return (Some ((TLBIndexT) idx)) - }; - None - } - -function (bit[64], bool) TLBTranslate2 ((bit[64]) vAddr, (MemAccessType) accessType) = { - let idx = tlbSearch(vAddr) in - switch(idx) { - case (Some(idx)) -> - let entry = (TLBEntries[idx]) in - let entryMask = entry.pagemask in - - let evenOddBit = switch(entryMask) { - case 0x0000 -> 12 - case 0x0003 -> 14 - case 0x000f -> 16 - case 0x003f -> 18 - case 0x00ff -> 20 - case 0x03ff -> 22 - case 0x0fff -> 24 - case 0x3fff -> 26 - case 0xffff -> 28 - case _ -> undefined - } in - let isOdd = (vAddr[evenOddBit]) in - let (caps, capl, (bit[24])pfn, d, v) = 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 - (EXTZ(pfn[23..((evenOddBit)-(12))] : vAddr[((evenOddBit)-(1)) .. 0]), - if (accessType == StoreData) then caps else capl) - case None -> (SignalExceptionTLB( - if (accessType == StoreData) then XTLBRefillS else XTLBRefillL, vAddr)) - } -} - -(* perform TLB translation. bool is CHERI specific TLB bits noStoreCap/suppressTag *) -function (bit[64], bool) TLBTranslateC ((bit[64]) vAddr, (MemAccessType) accessType) = - { - let currentAccessLevel = getAccessLevel() in - let compat32 = (vAddr[61..31] == 0b1111111111111111111111111111111) in - let (requiredLevel, addr) = switch(vAddr[63..62]) { - case 0b11 -> switch(compat32, vAddr[30..29]) { (* xkseg *) - case (true, 0b11) -> (Kernel, None) (* kseg3 mapped 32-bit compat *) - case (true, 0b10) -> (Supervisor, None) (* sseg mapped 32-bit compat *) - case (true, 0b01) -> (Kernel, Some(EXTZ(vAddr[28..0]))) (* kseg1 unmapped uncached 32-bit compat *) - case (true, 0b00) -> (Kernel, Some(EXTZ(vAddr[28..0]))) (* kseg0 unmapped cached 32-bit compat *) - case (_, _) -> (Kernel, None) (* xkseg mapped *) - } - case 0b10 -> (Kernel, Some(EXTZ(vAddr[58..0]))) (* xkphys bits 61-59 are cache mode (ignored) *) - case 0b01 -> (Supervisor, None) (* xsseg - supervisor mapped *) - case 0b00 -> (User, None) (* xuseg - user mapped *) - } in - if ((int_of_accessLevel(currentAccessLevel)) < (int_of_accessLevel(requiredLevel))) then - (SignalExceptionBadAddr(if (accessType == StoreData) then AdES else AdEL, vAddr)) - else - let (pa, c) = switch(addr) { - case (Some(a)) -> (a, false) - case 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) - } - -function (bit[64]) TLBTranslate ((bit[64]) vAddr, (MemAccessType) accessType) = - let (addr, c) = TLBTranslateC(vAddr, accessType) in addr diff --git a/mips/mips_tlb_stub.sail b/mips/mips_tlb_stub.sail deleted file mode 100644 index a9970a4e..00000000 --- a/mips/mips_tlb_stub.sail +++ /dev/null @@ -1,40 +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. *) -(*========================================================================*) - -function option<TLBIndexT> tlbSearch((bit[64]) VAddr) = None - -function (bit[64]) TLBTranslate ((bit[64]) vAddr, (MemAccessType) accessType) = - vAddr - -function (bit[64], bool) TLBTranslateC ((bit[64]) vAddr, (MemAccessType) accessType) = (vAddr, false) diff --git a/mips/mips_wrappers.sail b/mips/mips_wrappers.sail deleted file mode 100644 index 02131204..00000000 --- a/mips/mips_wrappers.sail +++ /dev/null @@ -1,70 +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) *) - -function unit effect {wmem} MEMw_wrapper(addr, size, data) = - let ledata = reverse_endianness(data) in - if (addr == 0x000000007f000000) then - { - UART_WDATA := ledata[7..0]; - UART_WRITTEN := 1; - } else { - MEMea(addr, size); - MEMval(addr, size, ledata); - } - -function bool effect {wmem} MEMw_conditional_wrapper(addr, size, data) = - { - MEMea_conditional(addr, size); - MEMval_conditional(addr, size, reverse_endianness(data)) - } - -function bit[64] addrWrapper((bit[64]) addr, (MemAccessType) accessType, (WordType) width) = - addr - -function (bit[64]) TranslatePC ((bit[64]) vAddr) = { - incrementCP0Count(); - if (vAddr[1..0] != 0b00) then (* bad PC alignment *) - (SignalExceptionBadAddr(AdEL, vAddr)) - else - TLBTranslate(vAddr, Instruction) -} - -let have_cp2 = false - -function unit SignalException ((Exception) ex) = SignalExceptionMIPS(ex, 0x0000000000000000) - -function unit ERETHook() = () diff --git a/mips/run_embed.ml b/mips/run_embed.ml deleted file mode 100644 index 1bb6d5f6..00000000 --- a/mips/run_embed.ml +++ /dev/null @@ -1,404 +0,0 @@ -(**************************************************************************) -(* Sail *) -(* *) -(* Copyright (c) 2013-2017 *) -(* Kathyrn Gray *) -(* Shaked Flur *) -(* Stephen Kell *) -(* Gabriel Kerneis *) -(* Robert Norton-Wright *) -(* Christopher Pulte *) -(* Peter Sewell *) -(* *) -(* 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. *) -(**************************************************************************) - -open Printf ;; -open Big_int_Z ;; -open Sail_values;; -open Mips_extras_ml;; - -let interact_print = ref true -let result_print = ref true -let error_print = ref true -let interactf : ('a, out_channel, unit) format -> 'a = - function f -> if !interact_print then printf f else ifprintf stderr f -let errorf : ('a, out_channel, unit) format -> 'a = - function f -> if !error_print then printf f else ifprintf stderr f -let resultf : ('a, out_channel, unit) format -> 'a = - function f -> if !result_print then printf f else ifprintf stderr f - -let rec foldli f acc ?(i=0) = function - | [] -> acc - | x::xs -> foldli f (f i acc x) ~i:(i+1) xs;; - -let big_int_to_hex i = Z.format "%x" i -let big_int_to_hex64 i = Z.format "%016x" i - -let input_buf = (ref [] : int list ref);; - -let max_cut_off = ref false -let max_instr = ref 0 -let model_arg = ref "cheri" -let raw_list = ref [] - -let args = [ - ("--model", Arg.Set_string model_arg, "CPU model to use (mips, cheri, cheri128)"); - ("--max_instruction", Arg.Int (fun i -> max_cut_off := true; max_instr := i), "only run i instructions, then stop"); - ("--trace", Arg.Set trace_writes, "trace all register writes"); (* trace_writes is in sail_values.ml *) - ("--quiet", Arg.Clear interact_print, "suppress trace of PC"); - ("--undef", Arg.String (fun s -> undef_val := bit_of_string s), "value to use for undef (u,0,1)"); -] - -module type ISA_model = sig - type ast - val init_model : unit -> unit - val inc_nextPC : unit -> unit - val get_pc : unit -> big_int - val translate_pc : unit -> big_int option - val get_opcode : big_int -> value - val decode : value -> ast option - val execute : ast -> unit - val is_halt : ast -> bool - val print_results : unit -> unit -end - -let rec debug_print_gprs gprs start stop = - let gpr_val = vector_access gprs (big_int_of_int start) in - let gpr_str = - if has_undef gpr_val then - "uuuuuuuuuuuuuuuu" - else - big_int_to_hex64 (unsigned_big(gpr_val)) in - resultf "DEBUG MIPS REG %.2d 0x%s\n" start gpr_str; - if start < stop - then debug_print_gprs gprs (start + 1) stop - else () - -let cap_reg_to_string reg = - "0b" ^ (string_of_bit_array (get_barray reg)) - -let read_bit_reg = function - | Vregister (array,_,_,_,_) -> (!array).(0) = Vone - | _ -> failwith "read_bit_reg of non-reg" - -let rec debug_print_caps capregs start stop = - let cap_val = vector_access capregs (big_int_of_int start) in - let cap_str = cap_reg_to_string cap_val in - resultf "DEBUG CAP REG %.2d %s\n" start cap_str; - if start < stop - then debug_print_caps capregs (start + 1) stop - else () - -let handle_uart uart_written uart_wdata uart_rdata uart_rvalid = - (try - let (pending, _, _) = Unix.select [Unix.stdin] [] [] 0.0 in - if pending != [] then - input_buf := (!input_buf) @ [(input_byte stdin)] - with _ -> ()); - - if (read_bit_reg uart_written) then - begin - let b = unsigned_int(uart_wdata) in - printf "%c" (Char.chr b); - printf "%!"; - set_register uart_written (to_vec_dec_int (1,0)) - end; - - if not (read_bit_reg uart_rvalid) then - (match !input_buf with - | x :: xs -> - begin - set_register uart_rdata (to_vec_dec_int (8, x)); - set_register uart_rvalid (to_vec_dec_int (1, 1)); - input_buf := xs; - end - | _ -> ()) - -module MIPS_model : ISA_model = struct - type ast = Mips_embed._ast - - let init_model () = - let start_addr = (to_vec_dec_big (bi64, big_int_of_string "0x9000000040000000")) in - set_register Mips_embed._nextPC start_addr; - set_register_field_bit Mips_embed._CP0Status "BEV" Vone - - let inc_nextPC () = - handle_uart Mips_embed._UART_WRITTEN Mips_embed._UART_WDATA Mips_embed._UART_RDATA Mips_embed._UART_RVALID; - - set_register Mips_embed._inBranchDelay Mips_embed._branchPending; - set_register Mips_embed._branchPending (to_vec_dec_int (1, 0)); - set_register Mips_embed._PC Mips_embed._nextPC; - let inBranchDelay = read_bit_reg Mips_embed._inBranchDelay in - if inBranchDelay then - set_register Mips_embed._nextPC Mips_embed._delayedPC - else - let pc_vaddr = unsigned_big(Mips_embed._PC) in - let npc_addr = add_int_big_int 4 pc_vaddr in - let npc_vec = to_vec_dec_big (bi64, npc_addr) in - set_register Mips_embed._nextPC npc_vec - - let get_pc () = unsigned_big (Mips_embed._PC) - - let translate_pc () = - try - Some (unsigned_big(Mips_embed._TranslatePC(Mips_embed._PC))) - with Sail_exit -> None - - let get_opcode pc_a = Mips_embed._reverse_endianness(_MEMr (to_vec_dec_big (bi64, pc_a), bi4)) - - let decode = Mips_embed._decode - - let execute = Mips_embed._execute - let is_halt i = (i = Mips_embed.HCF) - let print_results () = - begin - resultf "DEBUG MIPS PC 0x%s\n" (big_int_to_hex (unsigned_big Mips_embed._PC)); - debug_print_gprs Mips_embed._GPR 0 31; - end -end - -module CHERI_model : ISA_model = struct - type ast = Cheri_embed._ast - - let init_model () = - let start_addr = (to_vec_dec_big (bi64, big_int_of_string "0x9000000040000000")) in - set_register Cheri_embed._nextPC start_addr; - set_register_field_bit Cheri_embed._CP0Status "BEV" Vone; - let initial_cap_val_int = big_int_of_string "0x100000000fffffffe00000000000000000000000000000000ffffffffffffffff" in - let initial_cap_vec = to_vec_dec ((big_int_of_int 257), initial_cap_val_int) in - set_register Cheri_embed._PCC initial_cap_vec; - set_register Cheri_embed._nextPCC initial_cap_vec; - set_register Cheri_embed._delayedPCC initial_cap_vec; - cap_size_shift := 5; (* configure memory model cap_size in mips_extras_ml *) - for i = 0 to 31 do - set_register (vector_access_int Cheri_embed._CapRegs i) initial_cap_vec - done - - let inc_nextPC () = - handle_uart Cheri_embed._UART_WRITTEN Cheri_embed._UART_WDATA Cheri_embed._UART_RDATA Cheri_embed._UART_RVALID; - - set_register Cheri_embed._inBranchDelay Cheri_embed._branchPending; - set_register Cheri_embed._branchPending (to_vec_dec_int (1, 0)); - set_register Cheri_embed._PC Cheri_embed._nextPC; - set_register Cheri_embed._PCC Cheri_embed._nextPCC; - let inBranchDelay = read_bit_reg Cheri_embed._inBranchDelay in - if inBranchDelay then - begin - set_register Cheri_embed._nextPC Cheri_embed._delayedPC; - set_register Cheri_embed._nextPCC Cheri_embed._delayedPCC; - end - else - let pc_vaddr = unsigned_big(Cheri_embed._PC) in - let npc_addr = add_int_big_int 4 pc_vaddr in - let npc_vec = to_vec_dec_big (bi64, npc_addr) in - begin - set_register Cheri_embed._nextPC npc_vec; - set_register Cheri_embed._inCCallDelay (to_vec_dec_int (1, 0)) - end - - let get_pc () = unsigned_big (Cheri_embed._PC) - - let translate_pc () = - try - Some (unsigned_big(Cheri_embed._TranslatePC(Cheri_embed._PC))) - with Sail_exit -> None - - let get_opcode pc_a = Cheri_embed._reverse_endianness(_MEMr (to_vec_dec_big (bi64, pc_a), bi4)) - - let decode = Cheri_embed._decode - - let execute = Cheri_embed._execute - let is_halt i = (i = Cheri_embed.HCF) - let print_results () = - begin - resultf "DEBUG MIPS PC 0x%s\n" (big_int_to_hex (unsigned_big Cheri_embed._PC)); - debug_print_gprs Cheri_embed._GPR 0 31; - resultf "DEBUG CAP PCC %s\n" (cap_reg_to_string Cheri_embed._PCC); - debug_print_caps Cheri_embed._CapRegs 0 31; - end -end - -module CHERI128_model : ISA_model = struct - type ast = Cheri128_embed._ast - - let init_model () = - let start_addr = (to_vec_dec_big (bi64, big_int_of_string "0x9000000040000000")) in - set_register Cheri128_embed._nextPC start_addr; - set_register_field_bit Cheri128_embed._CP0Status "BEV" Vone; - let initial_cap_val_int = big_int_of_string "0x1fffe6000000100000000000000000000" in (* hex((0x10000 << 64) + (48 << 105) + (0x7fff << 113) + (1 << 128)) T=0x10000 E=48 perms=0x7fff tag=1 *) - let initial_cap_vec = to_vec_dec ((bi129), initial_cap_val_int) in - set_register Cheri128_embed._PCC initial_cap_vec; - set_register Cheri128_embed._nextPCC initial_cap_vec; - set_register Cheri128_embed._delayedPCC initial_cap_vec; - cap_size_shift := 4; (* configure memory model cap_size in mips_extras_ml *) - for i = 0 to 31 do - set_register (vector_access_int Cheri128_embed._CapRegs i) initial_cap_vec - done - - let inc_nextPC () = - handle_uart Cheri128_embed._UART_WRITTEN Cheri128_embed._UART_WDATA Cheri128_embed._UART_RDATA Cheri128_embed._UART_RVALID; - - set_register Cheri128_embed._inBranchDelay Cheri128_embed._branchPending; - set_register Cheri128_embed._branchPending (to_vec_dec_int (1, 0)); - set_register Cheri128_embed._PC Cheri128_embed._nextPC; - set_register Cheri128_embed._PCC Cheri128_embed._nextPCC; - let inBranchDelay = read_bit_reg Cheri128_embed._inBranchDelay in - if inBranchDelay then - begin - set_register Cheri128_embed._nextPC Cheri128_embed._delayedPC; - set_register Cheri128_embed._nextPCC Cheri128_embed._delayedPCC; - end - else - let pc_vaddr = unsigned_big(Cheri128_embed._PC) in - let npc_addr = add_int_big_int 4 pc_vaddr in - let npc_vec = to_vec_dec_big (bi64, npc_addr) in - begin - set_register Cheri128_embed._nextPC npc_vec; - set_register Cheri128_embed._inCCallDelay (to_vec_dec_int (1, 0)) - end - - let get_pc () = unsigned_big (Cheri128_embed._PC) - - let translate_pc () = - try - Some (unsigned_big(Cheri128_embed._TranslatePC(Cheri128_embed._PC))) - with Sail_exit -> None - - let get_opcode pc_a = Cheri128_embed._reverse_endianness(_MEMr (to_vec_dec_big (bi64, pc_a), bi4)) - - let decode = Cheri128_embed._decode - - let execute = Cheri128_embed._execute - let is_halt i = (i = Cheri128_embed.HCF) - let print_results () = - begin - resultf "DEBUG MIPS PC 0x%s\n" (big_int_to_hex (unsigned_big Cheri128_embed._PC)); - debug_print_gprs Cheri128_embed._GPR 0 31; - resultf "DEBUG CAP PCC %s\n" (cap_reg_to_string Cheri128_embed._PCC); - debug_print_caps Cheri128_embed._CapRegs 0 31; - end -end - -let time_it action arg = - let start_time = Sys.time () in - let ret = action arg in - let finish_time = Sys.time () in - (finish_time -. start_time, ret) - -let rec fde_loop (model, count) = - if !max_cut_off && count = !max_instr - then begin - resultf "\nEnding evaluation due to reaching cut off point of %d instructions\n" count; - count - end - else - begin - let module Model = (val model : ISA_model) in - - Model.inc_nextPC (); - if !interact_print then - interactf "\n**** instruction %d from address %s ****\n" - count (big_int_to_hex64 (Model.get_pc ())); - let m_paddr = Model.translate_pc () in - match m_paddr with - | Some pc -> - let opcode = Model.get_opcode pc in - if !interact_print then - interactf "decode: 0x%x\n" (unsigned_int(opcode)); - let instruction = Model.decode opcode in - let i = match instruction with - | Some (i) -> i - | _ -> begin - errorf "\n**** Decode error ****\n"; - exit 1; - end - in - if Model.is_halt i then - begin - Model.print_results (); - resultf "\nSUCCESS program terminated after %d instructions\n" count; - count - end - else - begin - (try - Model.execute(i) - with Sail_exit -> ()); (* exception during execute *) - fde_loop (model, count + 1) - end - | None -> (* Exception during PC translation *) - fde_loop (model, count + 1) - end - -let rec load_raw_file buf addr len chan = - let to_read = min_int len page_size_bytes in - really_input chan buf 0 to_read; - add_mem_bytes addr buf 0 to_read; - if (len > to_read) then - load_raw_file buf (add_int_big_int to_read addr) (len - to_read) chan - -let get_model = function - | "cheri128" -> (module CHERI128_model : ISA_model) - | "cheri" -> (module CHERI_model : ISA_model) - | "mips" -> (module MIPS_model : ISA_model) - | _ -> failwith "unknown model name" - -let anon_raw s = - (* some input validation would be nice... *) - let len = String.length s in - let atidx = try - String.index s '@' - with Not_found -> raise (Arg.Bad "expected argument of form file@addr") in - let f = String.sub s 0 atidx in - let addr = String.sub s (atidx+1) (len - atidx -1) in - raw_list := (!raw_list) @ [(f, big_int_of_string addr)] - -let load_raw_arg (f, a) = - let buf = Bytes.create page_size_bytes in - let chan = open_in_bin f in - let len = in_channel_length chan in - load_raw_file buf a len chan - -let run () = - (* Turn off line-buffering of standard input to allow responsive console input *) - if Unix.isatty (Unix.stdin) then begin - let tattrs = Unix.tcgetattr (Unix.stdin) in - Unix.tcsetattr (Unix.stdin) (Unix.TCSANOW) ({tattrs with c_icanon=false}) - end; - Arg.parse args anon_raw "" ; - List.iter load_raw_arg !raw_list; - let model = get_model !model_arg in - let module Model = (val model : ISA_model) in - Model.init_model (); - let (t, count) = time_it fde_loop (model, 0) in - resultf "Execution time: %f seconds %f IPS \n" t (float(count) /. t);; - -run () ;; |