diff --git a/Makefile b/Makefile index 923c6a3d0..255224125 100644 --- a/Makefile +++ b/Makefile @@ -82,7 +82,7 @@ SAIL_VM_SRCS += $(SAIL_RV64_VM_SRCS) endif # Non-instruction sources -PRELUDE = prelude.sail prelude_mapping.sail $(SAIL_XLEN) $(SAIL_FLEN) $(SAIL_VLEN) prelude_mem_metadata.sail prelude_mem.sail +PRELUDE = prelude.sail $(SAIL_XLEN) $(SAIL_FLEN) $(SAIL_VLEN) prelude_mem_metadata.sail prelude_mem.sail SAIL_REGS_SRCS = riscv_reg_type.sail riscv_freg_type.sail riscv_regs.sail riscv_pc_access.sail riscv_sys_regs.sail SAIL_REGS_SRCS += riscv_pmp_regs.sail riscv_pmp_control.sail @@ -247,9 +247,11 @@ gcovr: ocaml_emulator/tracecmp: ocaml_emulator/tracecmp.ml ocamlfind ocamlopt -annot -linkpkg -package unix $^ -o $@ +c_preserve_fns=-c_preserve _set_Misa_C + generated_definitions/c/riscv_model_$(ARCH).c: $(SAIL_SRCS) model/main.sail Makefile mkdir -p generated_definitions/c - $(SAIL) $(SAIL_FLAGS) -O -Oconstant_fold -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_SRCS) model/main.sail -o $(basename $@) + $(SAIL) $(SAIL_FLAGS) $(c_preserve_fns) -O -Oconstant_fold -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_SRCS) model/main.sail -o $(basename $@) generated_definitions/c2/riscv_model_$(ARCH).c: $(SAIL_SRCS) model/main.sail Makefile mkdir -p generated_definitions/c2 @@ -288,7 +290,7 @@ rvfi_preserve_fns=-c_preserve rvfi_set_instr_packet \ # sed -i isn't posix compliant, unfortunately generated_definitions/c/riscv_rvfi_model_$(ARCH).c: $(SAIL_RVFI_SRCS) model/main.sail Makefile mkdir -p generated_definitions/c - $(SAIL) $(rvfi_preserve_fns) $(SAIL_FLAGS) -O -Oconstant_fold -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_RVFI_SRCS) model/main.sail -o $(basename $@) + $(SAIL) $(c_preserve_fns) $(rvfi_preserve_fns) $(SAIL_FLAGS) -O -Oconstant_fold -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_RVFI_SRCS) model/main.sail -o $(basename $@) sed -e '/^[[:space:]]*$$/d' $@ > $@.new mv $@.new $@ diff --git a/c_emulator/riscv_platform.c b/c_emulator/riscv_platform.c index f4831c60d..4d9356786 100644 --- a/c_emulator/riscv_platform.c +++ b/c_emulator/riscv_platform.c @@ -47,6 +47,16 @@ bool sys_enable_vext(unit u) return rv_enable_vext; } +uint64_t sys_pmp_count(unit u) +{ + return rv_pmp_count; +} + +uint64_t sys_pmp_grain(unit u) +{ + return rv_pmp_grain; +} + bool sys_enable_writable_misa(unit u) { return rv_enable_writable_misa; @@ -67,9 +77,14 @@ bool plat_mtval_has_illegal_inst_bits(unit u) return rv_mtval_has_illegal_inst_bits; } -bool plat_enable_pmp(unit u) +bool sys_enable_svnapot(unit u) { - return rv_enable_pmp; + return rv_enable_svnapot; +} + +bool sys_enable_svpbmt(unit u) +{ + return rv_enable_svpbmt; } bool sys_enable_svnapot(unit u) diff --git a/c_emulator/riscv_platform.h b/c_emulator/riscv_platform.h index 2d6277dd4..4f635b83c 100644 --- a/c_emulator/riscv_platform.h +++ b/c_emulator/riscv_platform.h @@ -11,10 +11,12 @@ bool sys_enable_vext(unit); bool sys_enable_svnapot(unit); bool sys_enable_svpbmt(unit); +uint64_t sys_pmp_count(unit); +uint64_t sys_pmp_grain(unit); + bool plat_enable_dirty_update(unit); bool plat_enable_misaligned_access(unit); bool plat_mtval_has_illegal_inst_bits(unit); -bool plat_enable_pmp(unit); mach_bits plat_ram_base(unit); mach_bits plat_ram_size(unit); diff --git a/c_emulator/riscv_platform_impl.c b/c_emulator/riscv_platform_impl.c index aa1191d0f..4e36d0fb1 100644 --- a/c_emulator/riscv_platform_impl.c +++ b/c_emulator/riscv_platform_impl.c @@ -3,7 +3,9 @@ #include /* Settings of the platform implementation, with common defaults. */ -bool rv_enable_pmp = false; +uint64_t rv_pmp_count = 0; +uint64_t rv_pmp_grain = 0; + bool rv_enable_zfinx = false; bool rv_enable_rvc = true; bool rv_enable_next = false; diff --git a/c_emulator/riscv_platform_impl.h b/c_emulator/riscv_platform_impl.h index 378f1d28e..88d9d5458 100644 --- a/c_emulator/riscv_platform_impl.h +++ b/c_emulator/riscv_platform_impl.h @@ -8,7 +8,9 @@ #define DEFAULT_RSTVEC 0x00001000 -extern bool rv_enable_pmp; +extern uint64_t rv_pmp_count; +extern uint64_t rv_pmp_grain; + extern bool rv_enable_zfinx; extern bool rv_enable_rvc; extern bool rv_enable_next; diff --git a/c_emulator/riscv_sim.c b/c_emulator/riscv_sim.c index 2c1a4f449..de8f6b76d 100644 --- a/c_emulator/riscv_sim.c +++ b/c_emulator/riscv_sim.c @@ -51,8 +51,10 @@ const char *RV32ISA = "RV32IMAC"; #define OPT_TRACE_OUTPUT 1000 #define OPT_ENABLE_WRITABLE_FIOM 1001 -#define OPT_ENABLE_SVNAPOT 1002 -#define OPT_ENABLE_SVPBMT 1003 +#define OPT_PMP_COUNT 1002 +#define OPT_PMP_GRAIN 1003 +#define OPT_ENABLE_SVNAPOT 1004 +#define OPT_ENABLE_SVPBMT 1005 static bool do_dump_dts = false; static bool do_show_times = false; @@ -121,7 +123,8 @@ char *sailcov_file = NULL; static struct option options[] = { {"enable-dirty-update", no_argument, 0, 'd' }, {"enable-misaligned", no_argument, 0, 'm' }, - {"enable-pmp", no_argument, 0, 'P' }, + {"pmp-count", required_argument, 0, OPT_PMP_COUNT }, + {"pmp-grain", required_argument, 0, OPT_PMP_GRAIN }, {"enable-next", no_argument, 0, 'N' }, {"ram-size", required_argument, 0, 'z' }, {"disable-compressed", no_argument, 0, 'C' }, @@ -240,6 +243,8 @@ static int process_args(int argc, char **argv) { int c; uint64_t ram_size = 0; + uint64_t pmp_count = 0; + uint64_t pmp_grain = 0; while (true) { c = getopt_long(argc, argv, "a" @@ -285,9 +290,23 @@ static int process_args(int argc, char **argv) fprintf(stderr, "enabling misaligned access.\n"); rv_enable_misaligned = true; break; - case 'P': - fprintf(stderr, "enabling PMP support.\n"); - rv_enable_pmp = true; + case OPT_PMP_COUNT: + pmp_count = atol(optarg); + fprintf(stderr, "PMP count: %lld\n", pmp_count); + if (pmp_count != 0 && pmp_count != 16 && pmp_count != 64) { + fprintf(stderr, "invalid PMP count: must be 0, 16 or 64"); + exit(1); + } + rv_pmp_count = pmp_count; + break; + case OPT_PMP_GRAIN: + pmp_grain = atol(optarg); + fprintf(stderr, "PMP grain: %lld\n", pmp_grain); + if (pmp_grain >= 64) { + fprintf(stderr, "invalid PMP grain: must less than 64"); + exit(1); + } + rv_pmp_grain = pmp_grain; break; case 'C': fprintf(stderr, "disabling RVC compressed instructions.\n"); diff --git a/handwritten_support/riscv_extras.lem b/handwritten_support/riscv_extras.lem index bc04c2df5..27e8ee5ed 100644 --- a/handwritten_support/riscv_extras.lem +++ b/handwritten_support/riscv_extras.lem @@ -201,10 +201,6 @@ val plat_enable_misaligned_access : unit -> bool let plat_enable_misaligned_access () = false declare ocaml target_rep function plat_enable_misaligned_access = `Platform.enable_misaligned_access` -val plat_enable_pmp : unit -> bool -let plat_enable_pmp () = false -declare ocaml target_rep function plat_enable_pmp = `Platform.enable_pmp` - val plat_mtval_has_illegal_inst_bits : unit -> bool let plat_mtval_has_illegal_inst_bits () = false declare ocaml target_rep function plat_mtval_has_illegal_inst_bits = `Platform.mtval_has_illegal_inst_bits` diff --git a/handwritten_support/riscv_extras_sequential.lem b/handwritten_support/riscv_extras_sequential.lem index 102d08242..d1139081d 100644 --- a/handwritten_support/riscv_extras_sequential.lem +++ b/handwritten_support/riscv_extras_sequential.lem @@ -189,10 +189,6 @@ val plat_enable_misaligned_access : unit -> bool let plat_enable_misaligned_access () = false declare ocaml target_rep function plat_enable_misaligned_access = `Platform.enable_misaligned_access` -val plat_enable_pmp : unit -> bool -let plat_enable_pmp () = false -declare ocaml target_rep function plat_enable_pmp = `Platform.enable_pmp` - val plat_mtval_has_illegal_inst_bits : unit -> bool let plat_mtval_has_illegal_inst_bits () = false declare ocaml target_rep function plat_mtval_has_illegal_inst_bits = `Platform.mtval_has_illegal_inst_bits` diff --git a/model/hex_bits.sail b/model/hex_bits.sail new file mode 100644 index 000000000..81e25e155 --- /dev/null +++ b/model/hex_bits.sail @@ -0,0 +1,124 @@ +// Note: This file is temporarily copied here from the Sail compiler. It can +// be removed when Sail 0.18 is released. + +/*==========================================================================*/ +/* Sail */ +/* */ +/* Sail and the Sail architecture models here, comprising all files and */ +/* directories except the ASL-derived Sail code in the aarch64 directory, */ +/* are subject to the BSD two-clause licence below. */ +/* */ +/* The ASL derived parts of the ARMv8.3 specification in */ +/* aarch64/no_vector and aarch64/full are copyright ARM Ltd. */ +/* */ +/* Copyright (c) 2013-2021 */ +/* Kathyrn Gray */ +/* Shaked Flur */ +/* Stephen Kell */ +/* Gabriel Kerneis */ +/* Robert Norton-Wright */ +/* Christopher Pulte */ +/* Peter Sewell */ +/* Alasdair Armstrong */ +/* Brian Campbell */ +/* Thomas Bauereiss */ +/* Anthony Fox */ +/* Jon French */ +/* Dominic Mulligan */ +/* Stephen Kell */ +/* Mark Wassell */ +/* Alastair Reid (Arm Ltd) */ +/* */ +/* All rights reserved. */ +/* */ +/* This work was partially supported by EPSRC grant EP/K008528/1 REMS: Rigorous */ +/* Engineering for Mainstream Systems, an ARM iCASE award, EPSRC IAA */ +/* KTF funding, and donations from Arm. This project has received */ +/* funding from the European Research Council (ERC) under the European */ +/* Union’s Horizon 2020 research and innovation programme (grant */ +/* agreement No 789108, ELVER). */ +/* */ +/* This software was developed by SRI International and the University of */ +/* Cambridge Computer Laboratory (Department of Computer Science and */ +/* Technology) under DARPA/AFRL contracts FA8650-18-C-7809 ("CIFV") */ +/* and FA8750-10-C-0237 ("CTSRD"). */ +/* */ +/* Redistribution and use in source and binary forms, with or without */ +/* modification, are permitted provided that the following conditions */ +/* are met: */ +/* 1. Redistributions of source code must retain the above copyright */ +/* notice, this list of conditions and the following disclaimer. */ +/* 2. Redistributions in binary form must reproduce the above copyright */ +/* notice, this list of conditions and the following disclaimer in */ +/* the documentation and/or other materials provided with the */ +/* distribution. */ +/* */ +/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ +/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ +/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ +/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ +/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ +/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ +/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ +/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ +/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ +/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ +/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ +/* SUCH DAMAGE. */ +/*==========================================================================*/ + +$ifndef _HEX_BITS +$define _HEX_BITS + +$include +$include + +val "parse_hex_bits" : forall 'n, 'n > 0. (int('n), string) -> bits('n) +val "valid_hex_bits" : forall 'n, 'n > 0. (int('n), string) -> bool + +val hex_bits : forall 'n, 'n > 0. bits('n) <-> (int('n), string) + +function hex_bits_forwards(bv) = (length(bv), hex_str(unsigned(bv))) +function hex_bits_forwards_matches(bv) = true + +function hex_bits_backwards(n, str) = parse_hex_bits(n, str) +function hex_bits_backwards_matches(n, str) = valid_hex_bits(n, str) + +mapping hex_bits_1 : bits(1) <-> string = { hex_bits(1, s) <-> s } +mapping hex_bits_2 : bits(2) <-> string = { hex_bits(2, s) <-> s } +mapping hex_bits_3 : bits(3) <-> string = { hex_bits(3, s) <-> s } +mapping hex_bits_4 : bits(4) <-> string = { hex_bits(4, s) <-> s } +mapping hex_bits_5 : bits(5) <-> string = { hex_bits(5, s) <-> s } +mapping hex_bits_6 : bits(6) <-> string = { hex_bits(6, s) <-> s } +mapping hex_bits_7 : bits(7) <-> string = { hex_bits(7, s) <-> s } +mapping hex_bits_8 : bits(8) <-> string = { hex_bits(8, s) <-> s } +mapping hex_bits_9 : bits(9) <-> string = { hex_bits(9, s) <-> s } + +mapping hex_bits_10 : bits(10) <-> string = { hex_bits(10, s) <-> s } +mapping hex_bits_11 : bits(11) <-> string = { hex_bits(11, s) <-> s } +mapping hex_bits_12 : bits(12) <-> string = { hex_bits(12, s) <-> s } +mapping hex_bits_13 : bits(13) <-> string = { hex_bits(13, s) <-> s } +mapping hex_bits_14 : bits(14) <-> string = { hex_bits(14, s) <-> s } +mapping hex_bits_15 : bits(15) <-> string = { hex_bits(15, s) <-> s } +mapping hex_bits_16 : bits(16) <-> string = { hex_bits(16, s) <-> s } +mapping hex_bits_17 : bits(17) <-> string = { hex_bits(17, s) <-> s } +mapping hex_bits_18 : bits(18) <-> string = { hex_bits(18, s) <-> s } +mapping hex_bits_19 : bits(19) <-> string = { hex_bits(19, s) <-> s } + +mapping hex_bits_20 : bits(20) <-> string = { hex_bits(20, s) <-> s } +mapping hex_bits_21 : bits(21) <-> string = { hex_bits(21, s) <-> s } +mapping hex_bits_22 : bits(22) <-> string = { hex_bits(22, s) <-> s } +mapping hex_bits_23 : bits(23) <-> string = { hex_bits(23, s) <-> s } +mapping hex_bits_24 : bits(24) <-> string = { hex_bits(24, s) <-> s } +mapping hex_bits_25 : bits(25) <-> string = { hex_bits(25, s) <-> s } +mapping hex_bits_26 : bits(26) <-> string = { hex_bits(26, s) <-> s } +mapping hex_bits_27 : bits(27) <-> string = { hex_bits(27, s) <-> s } +mapping hex_bits_28 : bits(28) <-> string = { hex_bits(28, s) <-> s } +mapping hex_bits_29 : bits(29) <-> string = { hex_bits(29, s) <-> s } + +mapping hex_bits_30 : bits(30) <-> string = { hex_bits(30, s) <-> s } +mapping hex_bits_31 : bits(31) <-> string = { hex_bits(31, s) <-> s } +mapping hex_bits_32 : bits(32) <-> string = { hex_bits(32, s) <-> s } + +$endif _HEX_BITS diff --git a/model/mapping.sail b/model/mapping.sail new file mode 100644 index 000000000..ec8b75979 --- /dev/null +++ b/model/mapping.sail @@ -0,0 +1,136 @@ +// Note: This file is temporarily copied here from the Sail compiler. It can +// be removed when Sail 0.18 is released. + +/*==========================================================================*/ +/* Sail */ +/* */ +/* Sail and the Sail architecture models here, comprising all files and */ +/* directories except the ASL-derived Sail code in the aarch64 directory, */ +/* are subject to the BSD two-clause licence below. */ +/* */ +/* The ASL derived parts of the ARMv8.3 specification in */ +/* aarch64/no_vector and aarch64/full are copyright ARM Ltd. */ +/* */ +/* Copyright (c) 2013-2021 */ +/* Kathyrn Gray */ +/* Shaked Flur */ +/* Stephen Kell */ +/* Gabriel Kerneis */ +/* Robert Norton-Wright */ +/* Christopher Pulte */ +/* Peter Sewell */ +/* Alasdair Armstrong */ +/* Brian Campbell */ +/* Thomas Bauereiss */ +/* Anthony Fox */ +/* Jon French */ +/* Dominic Mulligan */ +/* Stephen Kell */ +/* Mark Wassell */ +/* Alastair Reid (Arm Ltd) */ +/* */ +/* All rights reserved. */ +/* */ +/* This work was partially supported by EPSRC grant EP/K008528/1 REMS: Rigorous */ +/* Engineering for Mainstream Systems, an ARM iCASE award, EPSRC IAA */ +/* KTF funding, and donations from Arm. This project has received */ +/* funding from the European Research Council (ERC) under the European */ +/* Union’s Horizon 2020 research and innovation programme (grant */ +/* agreement No 789108, ELVER). */ +/* */ +/* This software was developed by SRI International and the University of */ +/* Cambridge Computer Laboratory (Department of Computer Science and */ +/* Technology) under DARPA/AFRL contracts FA8650-18-C-7809 ("CIFV") */ +/* and FA8750-10-C-0237 ("CTSRD"). */ +/* */ +/* Redistribution and use in source and binary forms, with or without */ +/* modification, are permitted provided that the following conditions */ +/* are met: */ +/* 1. Redistributions of source code must retain the above copyright */ +/* notice, this list of conditions and the following disclaimer. */ +/* 2. Redistributions in binary form must reproduce the above copyright */ +/* notice, this list of conditions and the following disclaimer in */ +/* the documentation and/or other materials provided with the */ +/* distribution. */ +/* */ +/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ +/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ +/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ +/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ +/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ +/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ +/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ +/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ +/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ +/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ +/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ +/* SUCH DAMAGE. */ +/*==========================================================================*/ + +$ifndef _MAPPING +$define _MAPPING + +$include +$include + +val string_take = pure "string_take" : (string, nat) -> string +val string_drop = pure "string_drop" : (string, nat) -> string +val string_length = pure "string_length" : string -> nat +val string_append = pure {coq: "String.append", c: "concat_str", _: "string_append"} : (string, string) -> string +val string_startswith = pure "string_startswith" : (string, string) -> bool + +val n_leading_spaces = pure { coq: "n_leading_spaces_Z" } : string -> nat +function n_leading_spaces s = + match s { + "" => 0, + _ => match string_take(s, 1) { + " " => 1 + n_leading_spaces(string_drop(s, 1)), + _ => 0 + } + } + +/*! +In a string mapping this is treated as `[ ]+`, i.e one or more space +characters. It is printed as a single space `" "`. +*/ +val spc : unit <-> string + +function spc_forwards() = " " +function spc_forwards_matches() = true + +function spc_backwards _ = () +function spc_backwards_matches s = { + let len = string_length(s); + n_leading_spaces(s) == len & len > 0 +} + +/*! +In a string mapping this is treated as `[ ]*`, i.e. zero or more space +characters. It is printed as the empty string. +*/ +val opt_spc : unit <-> string + +function opt_spc_forwards() = "" +function opt_spc_forwards_matches() = true + +function opt_spc_backwards _ = () +function opt_spc_backwards_matches s = n_leading_spaces(s) == string_length(s) + +/*! +Like `opt_spc`, in a string mapping this is treated as `[ ]*`, i.e. zero or more space +characters. It differs however in that it is printed as a single space `" "`. +*/ +val def_spc : unit <-> string + +function def_spc_forwards() = " " +function def_spc_forwards_matches() = true + +function def_spc_backwards _ = () +function def_spc_backwards_matches s = n_leading_spaces(s) == string_length(s) + +mapping sep : unit <-> string = { + () <-> opt_spc() ^ "," ^ def_spc() +} + +$endif diff --git a/model/prelude.sail b/model/prelude.sail index 6b5e46c5d..3edec051d 100644 --- a/model/prelude.sail +++ b/model/prelude.sail @@ -74,69 +74,33 @@ $include $include $include $include +$include "mapping.sail" $include $include +$include +$include "hex_bits.sail" -val string_startswith = "string_startswith" : (string, string) -> bool -val string_drop = "string_drop" : (string, nat) -> string -val string_take = "string_take" : (string, nat) -> string -val string_length = "string_length" : string -> nat -val string_append = {c: "concat_str", _: "string_append"} : (string, string) -> string - -val eq_anything = {ocaml: "(fun (x, y) -> x = y)", interpreter: "eq_anything", lem: "eq", coq: "generic_eq", c: "eq_anything"} : forall ('a : Type). ('a, 'a) -> bool - -overload operator == = {eq_string, eq_anything} - -val "reg_deref" : forall ('a : Type). register('a) -> 'a -/* sneaky deref with no effect necessary for bitfield writes */ -val _reg_deref = "reg_deref" : forall ('a : Type). register('a) -> 'a - -val any_vector_update = {ocaml: "update", lem: "update_list_dec", coq: "vector_update"} : forall 'n ('a : Type). - (vector('n, dec, 'a), int, 'a) -> vector('n, dec, 'a) - -overload vector_update = {any_vector_update} - -val update_subrange = {ocaml: "update_subrange", interpreter: "update_subrange", lem: "update_subrange_vec_dec", coq: "update_subrange_vec_dec"} : forall 'n 'm 'o. - (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n) - -val vector_concat = {ocaml: "append", lem: "append_list", coq: "vec_concat"} : forall ('n : Int) ('m : Int) ('a : Type). - (vector('n, dec, 'a), vector('m, dec, 'a)) -> vector('n + 'm, dec, 'a) - -overload append = {vector_concat} val not_bit : bit -> bit - function not_bit(b) = if b == bitone then bitzero else bitone overload ~ = {not_bool, not_vec, not_bit} -val not = pure {coq: "negb", _: "not"} : forall ('p : Bool). bool('p) -> bool(not('p)) - -val neq_vec = {lem: "neq"} : forall 'n. (bits('n), bits('n)) -> bool - -function neq_vec (x, y) = not_bool(eq_bits(x, y)) - -val neq_anything = {lem: "neq", coq: "generic_neq"} : forall ('a : Type). ('a, 'a) -> bool - -function neq_anything (x, y) = not_bool(x == y) - -overload operator != = {neq_vec, neq_anything} +// not_bool alias. +val not : forall ('p : Bool). bool('p) -> bool(not('p)) +function not(b) = not_bool(b) overload operator & = {and_vec} overload operator | = {or_vec} -val string_of_int = {c: "string_of_int", ocaml: "string_of_int", interpreter: "string_of_int", lem: "stringFromInteger", coq: "string_of_int"} : int -> string - -val "string_of_bits" : forall 'n. bits('n) -> string - -function string_of_bit(b: bit) -> string = +function bit_str(b: bit) -> string = match b { bitzero => "0b0", bitone => "0b1" } -overload BitStr = {string_of_bits, string_of_bit} +overload BitStr = {bits_str, bit_str} val int_power = {ocaml: "int_power", interpreter: "int_power", lem: "pow", coq: "pow", c: "pow_int"} : (int, int) -> int @@ -284,53 +248,6 @@ function reverse_bits_in_byte (xs : bits(8)) -> bits(8) = { overload reverse = {reverse_bits_in_byte} -/* helpers for mappings */ - -val spc : unit <-> string -val opt_spc : unit <-> string -val def_spc : unit <-> string - -val "decimal_string_of_bits" : forall 'n. bits('n) -> string -val hex_bits : forall 'n . (atom('n), bits('n)) <-> string - -val n_leading_spaces : string -> nat -function n_leading_spaces s = - match s { - "" => 0, - _ => match string_take(s, 1) { - " " => 1 + n_leading_spaces(string_drop(s, 1)), - _ => 0 - } - } - -val spc_forwards : unit -> string -function spc_forwards () = " " -val spc_backwards : string -> unit -function spc_backwards s = () -val spc_matches_prefix : string -> option((unit, nat)) -function spc_matches_prefix s = { - let n = n_leading_spaces(s); - match n { - 0 => None(), - _ => Some((), n) - } -} - -val opt_spc_forwards : unit -> string -function opt_spc_forwards () = "" -val opt_spc_backwards : string -> unit -function opt_spc_backwards s = () -val opt_spc_matches_prefix : string -> option((unit, nat)) -function opt_spc_matches_prefix s = - Some((), n_leading_spaces(s)) - -val def_spc_forwards : unit -> string -function def_spc_forwards () = " " -val def_spc_backwards : string -> unit -function def_spc_backwards s = () -val def_spc_matches_prefix : string -> option((unit, nat)) -function def_spc_matches_prefix s = opt_spc_matches_prefix(s) - overload operator / = {quot_round_zero} overload operator * = {mult_atom, mult_int} diff --git a/model/prelude_mapping.sail b/model/prelude_mapping.sail deleted file mode 100644 index ff449d1ab..000000000 --- a/model/prelude_mapping.sail +++ /dev/null @@ -1,771 +0,0 @@ -/*=======================================================================================*/ -/* RISCV Sail Model */ -/* */ -/* This Sail RISC-V architecture model, comprising all files and */ -/* directories except for the snapshots of the Lem and Sail libraries */ -/* in the prover_snapshots directory (which include copies of their */ -/* licences), is subject to the BSD two-clause licence below. */ -/* */ -/* Copyright (c) 2017-2023 */ -/* Prashanth Mundkur */ -/* Rishiyur S. Nikhil and Bluespec, Inc. */ -/* Jon French */ -/* Brian Campbell */ -/* Robert Norton-Wright */ -/* Alasdair Armstrong */ -/* Thomas Bauereiss */ -/* Shaked Flur */ -/* Christopher Pulte */ -/* Peter Sewell */ -/* Alexander Richardson */ -/* Hesham Almatary */ -/* Jessica Clarke */ -/* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ -/* Peter Rugg */ -/* Aril Computer Corp., for contributions by Scott Johnson */ -/* Philipp Tomsich */ -/* VRULL GmbH, for contributions by its employees */ -/* */ -/* All rights reserved. */ -/* */ -/* This software was developed by the above within the Rigorous */ -/* Engineering of Mainstream Systems (REMS) project, partly funded by */ -/* EPSRC grant EP/K008528/1, at the Universities of Cambridge and */ -/* Edinburgh. */ -/* */ -/* This software was developed by SRI International and the University of */ -/* Cambridge Computer Laboratory (Department of Computer Science and */ -/* Technology) under DARPA/AFRL contract FA8650-18-C-7809 ("CIFV"), and */ -/* under DARPA contract HR0011-18-C-0016 ("ECATS") as part of the DARPA */ -/* SSITH research programme. */ -/* */ -/* This project has received funding from the European Research Council */ -/* (ERC) under the European Union’s Horizon 2020 research and innovation */ -/* programme (grant agreement 789108, ELVER). */ -/* */ -/* */ -/* 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. */ -/*=======================================================================================*/ - -/* Some helper functions for the assembler mappings. */ - -/* These mappings produce a lot of pattern match warnings that are not useful. - The following directive suppresses them (and will be ignored by older versions of Sail - with one additional warning). Would be better to fix the warnings properly but I don't - know how. */ -$suppress_warnings - -/* Python: -f = """val hex_bits_{0} : bits({0}) <-> string -val hex_bits_{0}_forwards = "decimal_string_of_bits" : bits({0}) -> string -val hex_bits_{0}_forwards_matches : bits({0}) -> bool -function hex_bits_{0}_forwards_matches bv = true -val "hex_bits_{0}_matches_prefix" : string -> option((bits({0}), nat)) -val hex_bits_{0}_backwards_matches : string -> bool -function hex_bits_{0}_backwards_matches s = match s {{ - s if match hex_bits_{0}_matches_prefix(s) {{ - Some (_, n) if n == string_length(s) => true, - _ => false - }} => true, - _ => false -}} -val hex_bits_{0}_backwards : string -> bits({0}) -function hex_bits_{0}_backwards s = - match hex_bits_{0}_matches_prefix(s) {{ - Some (bv, n) if n == string_length(s) => bv - }} -""" - -for i in list(range(1, 34)) + [48, 64]: - print(f.format(i)) - -*/ -val hex_bits_1 : bits(1) <-> string -val hex_bits_1_forwards = "decimal_string_of_bits" : bits(1) -> string -val hex_bits_1_forwards_matches : bits(1) -> bool -function hex_bits_1_forwards_matches bv = true -val "hex_bits_1_matches_prefix" : string -> option((bits(1), nat)) -val hex_bits_1_backwards_matches : string -> bool -function hex_bits_1_backwards_matches s = match s { - s if match hex_bits_1_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_1_backwards : string -> bits(1) -function hex_bits_1_backwards s = - match hex_bits_1_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_2 : bits(2) <-> string -val hex_bits_2_forwards = "decimal_string_of_bits" : bits(2) -> string -val hex_bits_2_forwards_matches : bits(2) -> bool -function hex_bits_2_forwards_matches bv = true -val "hex_bits_2_matches_prefix" : string -> option((bits(2), nat)) -val hex_bits_2_backwards_matches : string -> bool -function hex_bits_2_backwards_matches s = match s { - s if match hex_bits_2_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_2_backwards : string -> bits(2) -function hex_bits_2_backwards s = - match hex_bits_2_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_3 : bits(3) <-> string -val hex_bits_3_forwards = "decimal_string_of_bits" : bits(3) -> string -val hex_bits_3_forwards_matches : bits(3) -> bool -function hex_bits_3_forwards_matches bv = true -val "hex_bits_3_matches_prefix" : string -> option((bits(3), nat)) -val hex_bits_3_backwards_matches : string -> bool -function hex_bits_3_backwards_matches s = match s { - s if match hex_bits_3_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_3_backwards : string -> bits(3) -function hex_bits_3_backwards s = - match hex_bits_3_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_4 : bits(4) <-> string -val hex_bits_4_forwards = "decimal_string_of_bits" : bits(4) -> string -val hex_bits_4_forwards_matches : bits(4) -> bool -function hex_bits_4_forwards_matches bv = true -val "hex_bits_4_matches_prefix" : string -> option((bits(4), nat)) -val hex_bits_4_backwards_matches : string -> bool -function hex_bits_4_backwards_matches s = match s { - s if match hex_bits_4_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_4_backwards : string -> bits(4) -function hex_bits_4_backwards s = - match hex_bits_4_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_5 : bits(5) <-> string -val hex_bits_5_forwards = "decimal_string_of_bits" : bits(5) -> string -val hex_bits_5_forwards_matches : bits(5) -> bool -function hex_bits_5_forwards_matches bv = true -val "hex_bits_5_matches_prefix" : string -> option((bits(5), nat)) -val hex_bits_5_backwards_matches : string -> bool -function hex_bits_5_backwards_matches s = match s { - s if match hex_bits_5_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_5_backwards : string -> bits(5) -function hex_bits_5_backwards s = - match hex_bits_5_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_6 : bits(6) <-> string -val hex_bits_6_forwards = "decimal_string_of_bits" : bits(6) -> string -val hex_bits_6_forwards_matches : bits(6) -> bool -function hex_bits_6_forwards_matches bv = true -val "hex_bits_6_matches_prefix" : string -> option((bits(6), nat)) -val hex_bits_6_backwards_matches : string -> bool -function hex_bits_6_backwards_matches s = match s { - s if match hex_bits_6_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_6_backwards : string -> bits(6) -function hex_bits_6_backwards s = - match hex_bits_6_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_7 : bits(7) <-> string -val hex_bits_7_forwards = "decimal_string_of_bits" : bits(7) -> string -val hex_bits_7_forwards_matches : bits(7) -> bool -function hex_bits_7_forwards_matches bv = true -val "hex_bits_7_matches_prefix" : string -> option((bits(7), nat)) -val hex_bits_7_backwards_matches : string -> bool -function hex_bits_7_backwards_matches s = match s { - s if match hex_bits_7_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_7_backwards : string -> bits(7) -function hex_bits_7_backwards s = - match hex_bits_7_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_8 : bits(8) <-> string -val hex_bits_8_forwards = "decimal_string_of_bits" : bits(8) -> string -val hex_bits_8_forwards_matches : bits(8) -> bool -function hex_bits_8_forwards_matches bv = true -val "hex_bits_8_matches_prefix" : string -> option((bits(8), nat)) -val hex_bits_8_backwards_matches : string -> bool -function hex_bits_8_backwards_matches s = match s { - s if match hex_bits_8_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_8_backwards : string -> bits(8) -function hex_bits_8_backwards s = - match hex_bits_8_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_9 : bits(9) <-> string -val hex_bits_9_forwards = "decimal_string_of_bits" : bits(9) -> string -val hex_bits_9_forwards_matches : bits(9) -> bool -function hex_bits_9_forwards_matches bv = true -val "hex_bits_9_matches_prefix" : string -> option((bits(9), nat)) -val hex_bits_9_backwards_matches : string -> bool -function hex_bits_9_backwards_matches s = match s { - s if match hex_bits_9_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_9_backwards : string -> bits(9) -function hex_bits_9_backwards s = - match hex_bits_9_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_10 : bits(10) <-> string -val hex_bits_10_forwards = "decimal_string_of_bits" : bits(10) -> string -val hex_bits_10_forwards_matches : bits(10) -> bool -function hex_bits_10_forwards_matches bv = true -val "hex_bits_10_matches_prefix" : string -> option((bits(10), nat)) -val hex_bits_10_backwards_matches : string -> bool -function hex_bits_10_backwards_matches s = match s { - s if match hex_bits_10_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_10_backwards : string -> bits(10) -function hex_bits_10_backwards s = - match hex_bits_10_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_11 : bits(11) <-> string -val hex_bits_11_forwards = "decimal_string_of_bits" : bits(11) -> string -val hex_bits_11_forwards_matches : bits(11) -> bool -function hex_bits_11_forwards_matches bv = true -val "hex_bits_11_matches_prefix" : string -> option((bits(11), nat)) -val hex_bits_11_backwards_matches : string -> bool -function hex_bits_11_backwards_matches s = match s { - s if match hex_bits_11_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_11_backwards : string -> bits(11) -function hex_bits_11_backwards s = - match hex_bits_11_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_12 : bits(12) <-> string -val hex_bits_12_forwards = "decimal_string_of_bits" : bits(12) -> string -val hex_bits_12_forwards_matches : bits(12) -> bool -function hex_bits_12_forwards_matches bv = true -// XXX TODO the following builtin does not exist (at least for C backend) so I have -// substituted a dummy one that always returns None. This means that assembly_backwards -// (i.e. string -> ast) might not work but we don't actually use that for anything. -//val "hex_bits_12_matches_prefix" : string -> option((bits(12), nat)) -function hex_bits_12_matches_prefix (s : string) -> option((bits(12), nat)) = None() -val hex_bits_12_backwards_matches : string -> bool -function hex_bits_12_backwards_matches s = match s { - s if match hex_bits_12_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_12_backwards : string -> bits(12) -function hex_bits_12_backwards s = - match hex_bits_12_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_13 : bits(13) <-> string -val hex_bits_13_forwards = "decimal_string_of_bits" : bits(13) -> string -val hex_bits_13_forwards_matches : bits(13) -> bool -function hex_bits_13_forwards_matches bv = true -val "hex_bits_13_matches_prefix" : string -> option((bits(13), nat)) -val hex_bits_13_backwards_matches : string -> bool -function hex_bits_13_backwards_matches s = match s { - s if match hex_bits_13_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_13_backwards : string -> bits(13) -function hex_bits_13_backwards s = - match hex_bits_13_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_14 : bits(14) <-> string -val hex_bits_14_forwards = "decimal_string_of_bits" : bits(14) -> string -val hex_bits_14_forwards_matches : bits(14) -> bool -function hex_bits_14_forwards_matches bv = true -val "hex_bits_14_matches_prefix" : string -> option((bits(14), nat)) -val hex_bits_14_backwards_matches : string -> bool -function hex_bits_14_backwards_matches s = match s { - s if match hex_bits_14_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_14_backwards : string -> bits(14) -function hex_bits_14_backwards s = - match hex_bits_14_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_15 : bits(15) <-> string -val hex_bits_15_forwards = "decimal_string_of_bits" : bits(15) -> string -val hex_bits_15_forwards_matches : bits(15) -> bool -function hex_bits_15_forwards_matches bv = true -val "hex_bits_15_matches_prefix" : string -> option((bits(15), nat)) -val hex_bits_15_backwards_matches : string -> bool -function hex_bits_15_backwards_matches s = match s { - s if match hex_bits_15_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_15_backwards : string -> bits(15) -function hex_bits_15_backwards s = - match hex_bits_15_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_16 : bits(16) <-> string -val hex_bits_16_forwards = "decimal_string_of_bits" : bits(16) -> string -val hex_bits_16_forwards_matches : bits(16) -> bool -function hex_bits_16_forwards_matches bv = true -val "hex_bits_16_matches_prefix" : string -> option((bits(16), nat)) -val hex_bits_16_backwards_matches : string -> bool -function hex_bits_16_backwards_matches s = match s { - s if match hex_bits_16_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_16_backwards : string -> bits(16) -function hex_bits_16_backwards s = - match hex_bits_16_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_17 : bits(17) <-> string -val hex_bits_17_forwards = "decimal_string_of_bits" : bits(17) -> string -val hex_bits_17_forwards_matches : bits(17) -> bool -function hex_bits_17_forwards_matches bv = true -val "hex_bits_17_matches_prefix" : string -> option((bits(17), nat)) -val hex_bits_17_backwards_matches : string -> bool -function hex_bits_17_backwards_matches s = match s { - s if match hex_bits_17_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_17_backwards : string -> bits(17) -function hex_bits_17_backwards s = - match hex_bits_17_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_18 : bits(18) <-> string -val hex_bits_18_forwards = "decimal_string_of_bits" : bits(18) -> string -val hex_bits_18_forwards_matches : bits(18) -> bool -function hex_bits_18_forwards_matches bv = true -val "hex_bits_18_matches_prefix" : string -> option((bits(18), nat)) -val hex_bits_18_backwards_matches : string -> bool -function hex_bits_18_backwards_matches s = match s { - s if match hex_bits_18_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_18_backwards : string -> bits(18) -function hex_bits_18_backwards s = - match hex_bits_18_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_19 : bits(19) <-> string -val hex_bits_19_forwards = "decimal_string_of_bits" : bits(19) -> string -val hex_bits_19_forwards_matches : bits(19) -> bool -function hex_bits_19_forwards_matches bv = true -val "hex_bits_19_matches_prefix" : string -> option((bits(19), nat)) -val hex_bits_19_backwards_matches : string -> bool -function hex_bits_19_backwards_matches s = match s { - s if match hex_bits_19_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_19_backwards : string -> bits(19) -function hex_bits_19_backwards s = - match hex_bits_19_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_20 : bits(20) <-> string -val hex_bits_20_forwards = "decimal_string_of_bits" : bits(20) -> string -val hex_bits_20_forwards_matches : bits(20) -> bool -function hex_bits_20_forwards_matches bv = true -val "hex_bits_20_matches_prefix" : string -> option((bits(20), nat)) -val hex_bits_20_backwards_matches : string -> bool -function hex_bits_20_backwards_matches s = match s { - s if match hex_bits_20_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_20_backwards : string -> bits(20) -function hex_bits_20_backwards s = - match hex_bits_20_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_21 : bits(21) <-> string -val hex_bits_21_forwards = "decimal_string_of_bits" : bits(21) -> string -val hex_bits_21_forwards_matches : bits(21) -> bool -function hex_bits_21_forwards_matches bv = true -val "hex_bits_21_matches_prefix" : string -> option((bits(21), nat)) -val hex_bits_21_backwards_matches : string -> bool -function hex_bits_21_backwards_matches s = match s { - s if match hex_bits_21_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_21_backwards : string -> bits(21) -function hex_bits_21_backwards s = - match hex_bits_21_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_22 : bits(22) <-> string -val hex_bits_22_forwards = "decimal_string_of_bits" : bits(22) -> string -val hex_bits_22_forwards_matches : bits(22) -> bool -function hex_bits_22_forwards_matches bv = true -val "hex_bits_22_matches_prefix" : string -> option((bits(22), nat)) -val hex_bits_22_backwards_matches : string -> bool -function hex_bits_22_backwards_matches s = match s { - s if match hex_bits_22_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_22_backwards : string -> bits(22) -function hex_bits_22_backwards s = - match hex_bits_22_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_23 : bits(23) <-> string -val hex_bits_23_forwards = "decimal_string_of_bits" : bits(23) -> string -val hex_bits_23_forwards_matches : bits(23) -> bool -function hex_bits_23_forwards_matches bv = true -val "hex_bits_23_matches_prefix" : string -> option((bits(23), nat)) -val hex_bits_23_backwards_matches : string -> bool -function hex_bits_23_backwards_matches s = match s { - s if match hex_bits_23_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_23_backwards : string -> bits(23) -function hex_bits_23_backwards s = - match hex_bits_23_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_24 : bits(24) <-> string -val hex_bits_24_forwards = "decimal_string_of_bits" : bits(24) -> string -val hex_bits_24_forwards_matches : bits(24) -> bool -function hex_bits_24_forwards_matches bv = true -val "hex_bits_24_matches_prefix" : string -> option((bits(24), nat)) -val hex_bits_24_backwards_matches : string -> bool -function hex_bits_24_backwards_matches s = match s { - s if match hex_bits_24_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_24_backwards : string -> bits(24) -function hex_bits_24_backwards s = - match hex_bits_24_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_25 : bits(25) <-> string -val hex_bits_25_forwards = "decimal_string_of_bits" : bits(25) -> string -val hex_bits_25_forwards_matches : bits(25) -> bool -function hex_bits_25_forwards_matches bv = true -val "hex_bits_25_matches_prefix" : string -> option((bits(25), nat)) -val hex_bits_25_backwards_matches : string -> bool -function hex_bits_25_backwards_matches s = match s { - s if match hex_bits_25_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_25_backwards : string -> bits(25) -function hex_bits_25_backwards s = - match hex_bits_25_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_26 : bits(26) <-> string -val hex_bits_26_forwards = "decimal_string_of_bits" : bits(26) -> string -val hex_bits_26_forwards_matches : bits(26) -> bool -function hex_bits_26_forwards_matches bv = true -val "hex_bits_26_matches_prefix" : string -> option((bits(26), nat)) -val hex_bits_26_backwards_matches : string -> bool -function hex_bits_26_backwards_matches s = match s { - s if match hex_bits_26_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_26_backwards : string -> bits(26) -function hex_bits_26_backwards s = - match hex_bits_26_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_27 : bits(27) <-> string -val hex_bits_27_forwards = "decimal_string_of_bits" : bits(27) -> string -val hex_bits_27_forwards_matches : bits(27) -> bool -function hex_bits_27_forwards_matches bv = true -val "hex_bits_27_matches_prefix" : string -> option((bits(27), nat)) -val hex_bits_27_backwards_matches : string -> bool -function hex_bits_27_backwards_matches s = match s { - s if match hex_bits_27_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_27_backwards : string -> bits(27) -function hex_bits_27_backwards s = - match hex_bits_27_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_28 : bits(28) <-> string -val hex_bits_28_forwards = "decimal_string_of_bits" : bits(28) -> string -val hex_bits_28_forwards_matches : bits(28) -> bool -function hex_bits_28_forwards_matches bv = true -val "hex_bits_28_matches_prefix" : string -> option((bits(28), nat)) -val hex_bits_28_backwards_matches : string -> bool -function hex_bits_28_backwards_matches s = match s { - s if match hex_bits_28_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_28_backwards : string -> bits(28) -function hex_bits_28_backwards s = - match hex_bits_28_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_29 : bits(29) <-> string -val hex_bits_29_forwards = "decimal_string_of_bits" : bits(29) -> string -val hex_bits_29_forwards_matches : bits(29) -> bool -function hex_bits_29_forwards_matches bv = true -val "hex_bits_29_matches_prefix" : string -> option((bits(29), nat)) -val hex_bits_29_backwards_matches : string -> bool -function hex_bits_29_backwards_matches s = match s { - s if match hex_bits_29_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_29_backwards : string -> bits(29) -function hex_bits_29_backwards s = - match hex_bits_29_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_30 : bits(30) <-> string -val hex_bits_30_forwards = "decimal_string_of_bits" : bits(30) -> string -val hex_bits_30_forwards_matches : bits(30) -> bool -function hex_bits_30_forwards_matches bv = true -val "hex_bits_30_matches_prefix" : string -> option((bits(30), nat)) -val hex_bits_30_backwards_matches : string -> bool -function hex_bits_30_backwards_matches s = match s { - s if match hex_bits_30_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_30_backwards : string -> bits(30) -function hex_bits_30_backwards s = - match hex_bits_30_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_31 : bits(31) <-> string -val hex_bits_31_forwards = "decimal_string_of_bits" : bits(31) -> string -val hex_bits_31_forwards_matches : bits(31) -> bool -function hex_bits_31_forwards_matches bv = true -val "hex_bits_31_matches_prefix" : string -> option((bits(31), nat)) -val hex_bits_31_backwards_matches : string -> bool -function hex_bits_31_backwards_matches s = match s { - s if match hex_bits_31_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_31_backwards : string -> bits(31) -function hex_bits_31_backwards s = - match hex_bits_31_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_32 : bits(32) <-> string -val hex_bits_32_forwards = "decimal_string_of_bits" : bits(32) -> string -val hex_bits_32_forwards_matches : bits(32) -> bool -function hex_bits_32_forwards_matches bv = true -val "hex_bits_32_matches_prefix" : string -> option((bits(32), nat)) -val hex_bits_32_backwards_matches : string -> bool -function hex_bits_32_backwards_matches s = match s { - s if match hex_bits_32_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_32_backwards : string -> bits(32) -function hex_bits_32_backwards s = - match hex_bits_32_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_33 : bits(33) <-> string -val hex_bits_33_forwards = "decimal_string_of_bits" : bits(33) -> string -val hex_bits_33_forwards_matches : bits(33) -> bool -function hex_bits_33_forwards_matches bv = true -val "hex_bits_33_matches_prefix" : string -> option((bits(33), nat)) -val hex_bits_33_backwards_matches : string -> bool -function hex_bits_33_backwards_matches s = match s { - s if match hex_bits_33_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_33_backwards : string -> bits(33) -function hex_bits_33_backwards s = - match hex_bits_33_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_48 : bits(48) <-> string -val hex_bits_48_forwards = "decimal_string_of_bits" : bits(48) -> string -val hex_bits_48_forwards_matches : bits(48) -> bool -function hex_bits_48_forwards_matches bv = true -val "hex_bits_48_matches_prefix" : string -> option((bits(48), nat)) -val hex_bits_48_backwards_matches : string -> bool -function hex_bits_48_backwards_matches s = match s { - s if match hex_bits_48_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_48_backwards : string -> bits(48) -function hex_bits_48_backwards s = - match hex_bits_48_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_64 : bits(64) <-> string -val hex_bits_64_forwards = "decimal_string_of_bits" : bits(64) -> string -val hex_bits_64_forwards_matches : bits(64) -> bool -function hex_bits_64_forwards_matches bv = true -val "hex_bits_64_matches_prefix" : string -> option((bits(64), nat)) -val hex_bits_64_backwards_matches : string -> bool -function hex_bits_64_backwards_matches s = match s { - s if match hex_bits_64_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_64_backwards : string -> bits(64) -function hex_bits_64_backwards s = - match hex_bits_64_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } diff --git a/model/riscv_csr_map.sail b/model/riscv_csr_map.sail index da68556f0..dcc865117 100644 --- a/model/riscv_csr_map.sail +++ b/model/riscv_csr_map.sail @@ -138,6 +138,18 @@ mapping clause csr_name_map = 0x3A0 <-> "pmpcfg0" mapping clause csr_name_map = 0x3A1 <-> "pmpcfg1" mapping clause csr_name_map = 0x3A2 <-> "pmpcfg2" mapping clause csr_name_map = 0x3A3 <-> "pmpcfg3" +mapping clause csr_name_map = 0x3A4 <-> "pmpcfg4" +mapping clause csr_name_map = 0x3A5 <-> "pmpcfg5" +mapping clause csr_name_map = 0x3A6 <-> "pmpcfg6" +mapping clause csr_name_map = 0x3A7 <-> "pmpcfg7" +mapping clause csr_name_map = 0x3A8 <-> "pmpcfg8" +mapping clause csr_name_map = 0x3A9 <-> "pmpcfg9" +mapping clause csr_name_map = 0x3AA <-> "pmpcfg10" +mapping clause csr_name_map = 0x3AB <-> "pmpcfg11" +mapping clause csr_name_map = 0x3AC <-> "pmpcfg12" +mapping clause csr_name_map = 0x3AD <-> "pmpcfg13" +mapping clause csr_name_map = 0x3AE <-> "pmpcfg14" +mapping clause csr_name_map = 0x3AF <-> "pmpcfg15" mapping clause csr_name_map = 0x3B0 <-> "pmpaddr0" mapping clause csr_name_map = 0x3B1 <-> "pmpaddr1" mapping clause csr_name_map = 0x3B2 <-> "pmpaddr2" @@ -154,6 +166,54 @@ mapping clause csr_name_map = 0x3BC <-> "pmpaddr12" mapping clause csr_name_map = 0x3BD <-> "pmpaddr13" mapping clause csr_name_map = 0x3BE <-> "pmpaddr14" mapping clause csr_name_map = 0x3BF <-> "pmpaddr15" +mapping clause csr_name_map = 0x3C0 <-> "pmpaddr16" +mapping clause csr_name_map = 0x3C1 <-> "pmpaddr17" +mapping clause csr_name_map = 0x3C2 <-> "pmpaddr18" +mapping clause csr_name_map = 0x3C3 <-> "pmpaddr19" +mapping clause csr_name_map = 0x3C4 <-> "pmpaddr20" +mapping clause csr_name_map = 0x3C5 <-> "pmpaddr21" +mapping clause csr_name_map = 0x3C6 <-> "pmpaddr22" +mapping clause csr_name_map = 0x3C7 <-> "pmpaddr23" +mapping clause csr_name_map = 0x3C8 <-> "pmpaddr24" +mapping clause csr_name_map = 0x3C9 <-> "pmpaddr25" +mapping clause csr_name_map = 0x3CA <-> "pmpaddr26" +mapping clause csr_name_map = 0x3CB <-> "pmpaddr27" +mapping clause csr_name_map = 0x3CC <-> "pmpaddr28" +mapping clause csr_name_map = 0x3CD <-> "pmpaddr29" +mapping clause csr_name_map = 0x3CE <-> "pmpaddr30" +mapping clause csr_name_map = 0x3CF <-> "pmpaddr31" +mapping clause csr_name_map = 0x3D0 <-> "pmpaddr32" +mapping clause csr_name_map = 0x3D1 <-> "pmpaddr33" +mapping clause csr_name_map = 0x3D2 <-> "pmpaddr34" +mapping clause csr_name_map = 0x3D3 <-> "pmpaddr35" +mapping clause csr_name_map = 0x3D4 <-> "pmpaddr36" +mapping clause csr_name_map = 0x3D5 <-> "pmpaddr37" +mapping clause csr_name_map = 0x3D6 <-> "pmpaddr38" +mapping clause csr_name_map = 0x3D7 <-> "pmpaddr39" +mapping clause csr_name_map = 0x3D8 <-> "pmpaddr40" +mapping clause csr_name_map = 0x3D9 <-> "pmpaddr41" +mapping clause csr_name_map = 0x3DA <-> "pmpaddr42" +mapping clause csr_name_map = 0x3DB <-> "pmpaddr43" +mapping clause csr_name_map = 0x3DC <-> "pmpaddr44" +mapping clause csr_name_map = 0x3DD <-> "pmpaddr45" +mapping clause csr_name_map = 0x3DE <-> "pmpaddr46" +mapping clause csr_name_map = 0x3DF <-> "pmpaddr47" +mapping clause csr_name_map = 0x3E0 <-> "pmpaddr48" +mapping clause csr_name_map = 0x3E1 <-> "pmpaddr49" +mapping clause csr_name_map = 0x3E2 <-> "pmpaddr50" +mapping clause csr_name_map = 0x3E3 <-> "pmpaddr51" +mapping clause csr_name_map = 0x3E4 <-> "pmpaddr52" +mapping clause csr_name_map = 0x3E5 <-> "pmpaddr53" +mapping clause csr_name_map = 0x3E6 <-> "pmpaddr54" +mapping clause csr_name_map = 0x3E7 <-> "pmpaddr55" +mapping clause csr_name_map = 0x3E8 <-> "pmpaddr56" +mapping clause csr_name_map = 0x3E9 <-> "pmpaddr57" +mapping clause csr_name_map = 0x3EA <-> "pmpaddr58" +mapping clause csr_name_map = 0x3EB <-> "pmpaddr59" +mapping clause csr_name_map = 0x3EC <-> "pmpaddr60" +mapping clause csr_name_map = 0x3ED <-> "pmpaddr61" +mapping clause csr_name_map = 0x3EE <-> "pmpaddr62" +mapping clause csr_name_map = 0x3EF <-> "pmpaddr63" /* machine counters/timers */ mapping clause csr_name_map = 0xB00 <-> "mcycle" mapping clause csr_name_map = 0xB02 <-> "minstret" diff --git a/model/riscv_fdext_control.sail b/model/riscv_fdext_control.sail index 563d60088..4ea958f03 100644 --- a/model/riscv_fdext_control.sail +++ b/model/riscv_fdext_control.sail @@ -83,12 +83,12 @@ function clause ext_is_CSR_defined (0x001, _) = haveFExt() | haveZfinx() function clause ext_is_CSR_defined (0x002, _) = haveFExt() | haveZfinx() function clause ext_is_CSR_defined (0x003, _) = haveFExt() | haveZfinx() -function clause ext_read_CSR (0x001) = Some (zero_extend (fcsr.FFLAGS())) -function clause ext_read_CSR (0x002) = Some (zero_extend (fcsr.FRM())) -function clause ext_read_CSR (0x003) = Some (zero_extend (fcsr.bits())) +function clause ext_read_CSR (0x001) = Some(zero_extend(fcsr[FFLAGS])) +function clause ext_read_CSR (0x002) = Some(zero_extend(fcsr[FRM])) +function clause ext_read_CSR (0x003) = Some(zero_extend(fcsr.bits)) -function clause ext_write_CSR (0x001, value) = { ext_write_fcsr (fcsr.FRM(), value [4..0]); Some(zero_extend(fcsr.FFLAGS())) } -function clause ext_write_CSR (0x002, value) = { ext_write_fcsr (value [2..0], fcsr.FFLAGS()); Some(zero_extend(fcsr.FRM())) } -function clause ext_write_CSR (0x003, value) = { ext_write_fcsr (value [7..5], value [4..0]); Some(zero_extend(fcsr.bits())) } +function clause ext_write_CSR (0x001, value) = { ext_write_fcsr(fcsr[FRM], value[4..0]); Some(zero_extend(fcsr[FFLAGS])) } +function clause ext_write_CSR (0x002, value) = { ext_write_fcsr(value[2..0], fcsr[FFLAGS]); Some(zero_extend(fcsr[FRM])) } +function clause ext_write_CSR (0x003, value) = { ext_write_fcsr(value[7..5], value[4..0]); Some(zero_extend(fcsr.bits)) } /* **************************************************************** */ diff --git a/model/riscv_fdext_regs.sail b/model/riscv_fdext_regs.sail index 795801644..479348600 100644 --- a/model/riscv_fdext_regs.sail +++ b/model/riscv_fdext_regs.sail @@ -165,8 +165,8 @@ register f31 : fregtype function dirty_fd_context() -> unit = { assert(sys_enable_fdext()); - mstatus->FS() = extStatus_to_bits(Dirty); - mstatus->SD() = 0b1 + mstatus[FS] = extStatus_to_bits(Dirty); + mstatus[SD] = 0b1 } function dirty_fd_context_if_present() -> unit = { @@ -261,7 +261,7 @@ function wF (r, in_v) = { if get_config_print_reg() then /* TODO: will only print bits; should we print in floating point format? */ - print_reg("f" ^ string_of_int(r) ^ " <- " ^ FRegStr(v)); + print_reg("f" ^ dec_str(r) ^ " <- " ^ FRegStr(v)); } function rF_bits(i: bits(5)) -> flenbits = rF(unsigned(i)) @@ -526,18 +526,18 @@ register fcsr : Fcsr val ext_write_fcsr : (bits(3), bits(5)) -> unit function ext_write_fcsr (frm, fflags) = { - fcsr->FRM() = frm; /* Note: frm can be an illegal value, 101, 110, 111 */ - fcsr->FFLAGS() = fflags; + fcsr[FRM] = frm; /* Note: frm can be an illegal value, 101, 110, 111 */ + fcsr[FFLAGS] = fflags; dirty_fd_context_if_present(); } /* OR flags into the fflags register. */ val accrue_fflags : (bits(5)) -> unit function accrue_fflags(flags) = { - let f = fcsr.FFLAGS() | flags; - if fcsr.FFLAGS() != f + let f = fcsr[FFLAGS] | flags; + if fcsr[FFLAGS] != f then { - fcsr->FFLAGS() = f; + fcsr[FFLAGS] = f; dirty_fd_context_if_present(); } } diff --git a/model/riscv_fetch_rvfi.sail b/model/riscv_fetch_rvfi.sail index b036c1b84..f4567ff31 100644 --- a/model/riscv_fetch_rvfi.sail +++ b/model/riscv_fetch_rvfi.sail @@ -69,10 +69,10 @@ /*=======================================================================================*/ function fetch() -> FetchResult = { - rvfi_inst_data->rvfi_order() = minstret; - rvfi_pc_data->rvfi_pc_rdata() = zero_extend(get_arch_pc()); - rvfi_inst_data->rvfi_mode() = zero_extend(privLevel_to_bits(cur_privilege)); - rvfi_inst_data->rvfi_ixl() = zero_extend(misa.MXL()); + rvfi_inst_data[rvfi_order] = minstret; + rvfi_pc_data[rvfi_pc_rdata] = zero_extend(get_arch_pc()); + rvfi_inst_data[rvfi_mode] = zero_extend(privLevel_to_bits(cur_privilege)); + rvfi_inst_data[rvfi_ixl] = zero_extend(misa[MXL]); /* First allow extensions to check pc */ match ext_fetch_check_pc(PC, PC) { @@ -84,7 +84,7 @@ function fetch() -> FetchResult = { else match translateAddr(use_pc, Execute()) { TR_Failure(e, _) => F_Error(e, PC), TR_Address(_, _) => { - let i = rvfi_instruction.rvfi_insn(); + let i = rvfi_instruction[rvfi_insn]; rvfi_inst_data->rvfi_insn() = zero_extend(i); if (i[1 .. 0] != 0b11) then F_RVC(i[15 .. 0]) diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail index eec5fbdc7..7d53d99c7 100644 --- a/model/riscv_insts_base.sail +++ b/model/riscv_insts_base.sail @@ -789,7 +789,7 @@ mapping clause encdec = SRET() function clause execute SRET() = { let sret_illegal : bool = match cur_privilege { User => true, - Supervisor => not(haveSupMode ()) | mstatus.TSR() == 0b1, + Supervisor => not(haveSupMode ()) | mstatus[TSR] == 0b1, Machine => not(haveSupMode ()) }; if sret_illegal @@ -826,7 +826,7 @@ mapping clause encdec = WFI() function clause execute WFI() = match cur_privilege { Machine => { platform_wfi(); RETIRE_SUCCESS }, - Supervisor => if mstatus.TW() == 0b1 + Supervisor => if mstatus[TW] == 0b1 then { handle_illegal(); RETIRE_FAIL } else { platform_wfi(); RETIRE_SUCCESS }, User => { handle_illegal(); RETIRE_FAIL } @@ -845,7 +845,7 @@ function clause execute SFENCE_VMA(rs1, rs2) = { let asid : option(xlenbits) = if rs2 == 0b00000 then None() else Some(X(rs2)); match cur_privilege { User => { handle_illegal(); RETIRE_FAIL }, - Supervisor => match (architecture(get_mstatus_SXL(mstatus)), mstatus.TVM()) { + Supervisor => match (architecture(get_mstatus_SXL(mstatus)), mstatus[TVM]) { (Some(_), 0b1) => { handle_illegal(); RETIRE_FAIL }, (Some(_), 0b0) => { flush_TLB(asid, addr); RETIRE_SUCCESS }, (_, _) => internal_error(__FILE__, __LINE__, "unimplemented sfence architecture") diff --git a/model/riscv_insts_cdext.sail b/model/riscv_insts_cdext.sail index 8851e348f..af0366e77 100644 --- a/model/riscv_insts_cdext.sail +++ b/model/riscv_insts_cdext.sail @@ -71,7 +71,7 @@ /* ********************************************************************* */ /* This file specifies the compressed floating-point instructions. * - * These instructions are only legal if misa.C() and misa.D() + * These instructions are only legal if misa[C] and misa[D] * are set. */ diff --git a/model/riscv_insts_cext.sail b/model/riscv_insts_cext.sail index 8b9fa8f0e..83d0d88a7 100644 --- a/model/riscv_insts_cext.sail +++ b/model/riscv_insts_cext.sail @@ -71,7 +71,7 @@ /* ********************************************************************* */ /* This file specifies the compressed instructions in the 'C' extension. */ -/* These instructions are only legal if misa.C() is true. Instead of +/* These instructions are only legal if misa[C] is true. Instead of * checking this in every execute clause, we currently do the check in one place * in the fetch-execute logic. */ diff --git a/model/riscv_insts_cfext.sail b/model/riscv_insts_cfext.sail index 5380aa261..878bb6588 100644 --- a/model/riscv_insts_cfext.sail +++ b/model/riscv_insts_cfext.sail @@ -71,7 +71,7 @@ /* ********************************************************************* */ /* This file specifies the compressed floating-point instructions. * - * These instructions are only legal if misa.C() and misa.F() + * These instructions are only legal if misa[C] and misa[F] * are set. */ diff --git a/model/riscv_insts_fext.sail b/model/riscv_insts_fext.sail index e0ea5513b..7bfef08e5 100644 --- a/model/riscv_insts_fext.sail +++ b/model/riscv_insts_fext.sail @@ -112,7 +112,7 @@ val select_instr_or_fcsr_rm : rounding_mode -> option(rounding_mode) function select_instr_or_fcsr_rm instr_rm = if (instr_rm == RM_DYN) then { - let fcsr_rm = fcsr.FRM(); + let fcsr_rm = fcsr[FRM]; if (valid_rounding_mode(fcsr_rm) & fcsr_rm != encdec_rounding_mode(RM_DYN)) then Some(encdec_rounding_mode(fcsr_rm)) else None() } diff --git a/model/riscv_insts_vext_fp.sail b/model/riscv_insts_vext_fp.sail index 05f36fdf9..1c8fe1ed0 100755 --- a/model/riscv_insts_vext_fp.sail +++ b/model/riscv_insts_vext_fp.sail @@ -61,7 +61,7 @@ mapping clause encdec = FVVTYPE(funct6, vm, vs2, vs1, vd) if haveVExt() <-> encdec_fvvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b001 @ vd @ 0b1010111 if haveVExt() function clause execute(FVVTYPE(funct6, vm, vs2, vs1, vd)) = { - let rm_3b = fcsr.FRM(); + let rm_3b = fcsr[FRM]; let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); @@ -136,7 +136,7 @@ mapping clause encdec = FVVMATYPE(funct6, vm, vs2, vs1, vd) if haveVExt() <-> encdec_fvvmafunct6(funct6) @ vm @ vs2 @ vs1 @ 0b001 @ vd @ 0b1010111 if haveVExt() function clause execute(FVVMATYPE(funct6, vm, vs2, vs1, vd)) = { - let rm_3b = fcsr.FRM(); + let rm_3b = fcsr[FRM]; let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); @@ -203,7 +203,7 @@ mapping clause encdec = FWVVTYPE(funct6, vm, vs2, vs1, vd) if haveVExt() <-> encdec_fwvvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b001 @ vd @ 0b1010111 if haveVExt() function clause execute(FWVVTYPE(funct6, vm, vs2, vs1, vd)) = { - let rm_3b = fcsr.FRM(); + let rm_3b = fcsr[FRM]; let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); @@ -268,7 +268,7 @@ mapping clause encdec = FWVVMATYPE(funct6, vm, vs1, vs2, vd) if haveVExt() <-> encdec_fwvvmafunct6(funct6) @ vm @ vs1 @ vs2 @ 0b001 @ vd @ 0b1010111 if haveVExt() function clause execute(FWVVMATYPE(funct6, vm, vs1, vs2, vd)) = { - let rm_3b = fcsr.FRM(); + let rm_3b = fcsr[FRM]; let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); @@ -332,7 +332,7 @@ mapping clause encdec = FWVTYPE(funct6, vm, vs2, vs1, vd) if haveVExt() <-> encdec_fwvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b001 @ vd @ 0b1010111 if haveVExt() function clause execute(FWVTYPE(funct6, vm, vs2, vs1, vd)) = { - let rm_3b = fcsr.FRM(); + let rm_3b = fcsr[FRM]; let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); @@ -395,7 +395,7 @@ mapping clause encdec = VFUNARY0(vm, vs2, vfunary0, vd) if haveVExt() <-> 0b010010 @ vm @ vs2 @ encdec_vfunary0_vs1(vfunary0) @ 0b001 @ vd @ 0b1010111 if haveVExt() function clause execute(VFUNARY0(vm, vs2, vfunary0, vd)) = { - let rm_3b = fcsr.FRM(); + let rm_3b = fcsr[FRM]; let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); @@ -508,7 +508,7 @@ mapping clause encdec = VFWUNARY0(vm, vs2, vfwunary0, vd) if haveVExt() <-> 0b010010 @ vm @ vs2 @ encdec_vfwunary0_vs1(vfwunary0) @ 0b001 @ vd @ 0b1010111 if haveVExt() function clause execute(VFWUNARY0(vm, vs2, vfwunary0, vd)) = { - let rm_3b = fcsr.FRM(); + let rm_3b = fcsr[FRM]; let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); @@ -638,7 +638,7 @@ mapping clause encdec = VFNUNARY0(vm, vs2, vfnunary0, vd) if haveVExt() <-> 0b010010 @ vm @ vs2 @ encdec_vfnunary0_vs1(vfnunary0) @ 0b001 @ vd @ 0b1010111 if haveVExt() function clause execute(VFNUNARY0(vm, vs2, vfnunary0, vd)) = { - let rm_3b = fcsr.FRM(); + let rm_3b = fcsr[FRM]; let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); @@ -773,7 +773,7 @@ mapping clause encdec = VFUNARY1(vm, vs2, vfunary1, vd) if haveVExt() <-> 0b010011 @ vm @ vs2 @ encdec_vfunary1_vs1(vfunary1) @ 0b001 @ vd @ 0b1010111 if haveVExt() function clause execute(VFUNARY1(vm, vs2, vfunary1, vd)) = { - let rm_3b = fcsr.FRM(); + let rm_3b = fcsr[FRM]; let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); @@ -849,7 +849,7 @@ mapping clause encdec = VFMVFS(vs2, rd) if haveVExt() <-> 0b010000 @ 0b1 @ vs2 @ 0b00000 @ 0b001 @ rd @ 0b1010111 if haveVExt() function clause execute(VFMVFS(vs2, rd)) = { - let rm_3b = fcsr.FRM(); + let rm_3b = fcsr[FRM]; let SEW = get_sew(); let num_elem = get_num_elem(0, SEW); @@ -897,7 +897,7 @@ mapping clause encdec = FVFTYPE(funct6, vm, vs2, rs1, vd) if haveVExt() <-> encdec_fvffunct6(funct6) @ vm @ vs2 @ rs1 @ 0b101 @ vd @ 0b1010111 if haveVExt() function clause execute(FVFTYPE(funct6, vm, vs2, rs1, vd)) = { - let rm_3b = fcsr.FRM(); + let rm_3b = fcsr[FRM]; let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); @@ -987,7 +987,7 @@ mapping clause encdec = FVFMATYPE(funct6, vm, vs2, rs1, vd) if haveVExt() <-> encdec_fvfmafunct6(funct6) @ vm @ vs2 @ rs1 @ 0b101 @ vd @ 0b1010111 if haveVExt() function clause execute(FVFMATYPE(funct6, vm, vs2, rs1, vd)) = { - let rm_3b = fcsr.FRM(); + let rm_3b = fcsr[FRM]; let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); @@ -1054,7 +1054,7 @@ mapping clause encdec = FWVFTYPE(funct6, vm, vs2, rs1, vd) if haveVExt() <-> encdec_fwvffunct6(funct6) @ vm @ vs2 @ rs1 @ 0b101 @ vd @ 0b1010111 if haveVExt() function clause execute(FWVFTYPE(funct6, vm, vs2, rs1, vd)) = { - let rm_3b = fcsr.FRM(); + let rm_3b = fcsr[FRM]; let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); @@ -1118,7 +1118,7 @@ mapping clause encdec = FWVFMATYPE(funct6, vm, rs1, vs2, vd) if haveVExt() <-> encdec_fwvfmafunct6(funct6) @ vm @ vs2 @ rs1 @ 0b101 @ vd @ 0b1010111 if haveVExt() function clause execute(FWVFMATYPE(funct6, vm, rs1, vs2, vd)) = { - let rm_3b = fcsr.FRM(); + let rm_3b = fcsr[FRM]; let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); @@ -1181,7 +1181,7 @@ mapping clause encdec = FWFTYPE(funct6, vm, vs2, rs1, vd) if haveVExt() <-> encdec_fwffunct6(funct6) @ vm @ vs2 @ rs1 @ 0b101 @ vd @ 0b1010111 if haveVExt() function clause execute(FWFTYPE(funct6, vm, vs2, rs1, vd)) = { - let rm_3b = fcsr.FRM(); + let rm_3b = fcsr[FRM]; let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); @@ -1235,7 +1235,7 @@ mapping clause encdec = VFMERGE(vs2, rs1, vd) if haveVExt() <-> 0b010111 @ 0b0 @ vs2 @ rs1 @ 0b101 @ vd @ 0b1010111 if haveVExt() function clause execute(VFMERGE(vs2, rs1, vd)) = { - let rm_3b = fcsr.FRM(); + let rm_3b = fcsr[FRM]; let start_element = get_start_element(); let end_element = get_end_element(); let SEW = get_sew(); @@ -1286,7 +1286,7 @@ mapping clause encdec = VFMV(rs1, vd) if haveVExt() <-> 0b010111 @ 0b1 @ 0b00000 @ rs1 @ 0b101 @ vd @ 0b1010111 if haveVExt() function clause execute(VFMV(rs1, vd)) = { - let rm_3b = fcsr.FRM(); + let rm_3b = fcsr[FRM]; let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); @@ -1324,7 +1324,7 @@ mapping clause encdec = VFMVSF(rs1, vd) if haveVExt() <-> 0b010000 @ 0b1 @ 0b00000 @ rs1 @ 0b101 @ vd @ 0b1010111 if haveVExt() function clause execute(VFMVSF(rs1, vd)) = { - let rm_3b = fcsr.FRM(); + let rm_3b = fcsr[FRM]; let SEW = get_sew(); let num_elem = get_num_elem(0, SEW); diff --git a/model/riscv_insts_vext_red.sail b/model/riscv_insts_vext_red.sail index be6afc34e..80ee8f220 100755 --- a/model/riscv_insts_vext_red.sail +++ b/model/riscv_insts_vext_red.sail @@ -190,7 +190,7 @@ mapping clause encdec = RFVVTYPE(funct6, vm, vs2, vs1, vd) if haveVExt() val process_rfvv_single: forall 'n 'm 'p, 'n >= 0 & 'm in {8, 16, 32, 64}. (rfvvfunct6, bits(1), regidx, regidx, regidx, int('n), int('m), int('p)) -> Retired function process_rfvv_single(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_pow) = { - let rm_3b = fcsr.FRM(); + let rm_3b = fcsr[FRM]; let num_elem_vd = get_num_elem(0, SEW); /* vd regardless of LMUL setting */ if illegal_fp_reduction(SEW, rm_3b) then { handle_illegal(); return RETIRE_FAIL }; @@ -229,7 +229,7 @@ function process_rfvv_single(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_po val process_rfvv_widen: forall 'n 'm 'p, 'n >= 0 & 'm in {8, 16, 32, 64}. (rfvvfunct6, bits(1), regidx, regidx, regidx, int('n), int('m), int('p)) -> Retired function process_rfvv_widen(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_pow) = { - let rm_3b = fcsr.FRM(); + let rm_3b = fcsr[FRM]; let SEW_widen = SEW * 2; let LMUL_pow_widen = LMUL_pow + 1; let num_elem_vd = get_num_elem(0, SEW_widen); /* vd regardless of LMUL setting */ diff --git a/model/riscv_insts_vext_utils.sail b/model/riscv_insts_vext_utils.sail index 45935cb7e..7b29a0f4f 100755 --- a/model/riscv_insts_vext_utils.sail +++ b/model/riscv_insts_vext_utils.sail @@ -63,7 +63,7 @@ function valid_eew_emul(EEW, EMUL_pow) = { */ val valid_vtype : unit -> bool function valid_vtype() = { - vtype.vill() == 0b0 + vtype[vill] == 0b0 } /* Check for vstart value */ @@ -643,7 +643,7 @@ function signed_saturation(len, elem) = { /* Get the floating point rounding mode from csr fcsr */ val get_fp_rounding_mode : unit -> rounding_mode -function get_fp_rounding_mode() = encdec_rounding_mode(fcsr.FRM()) +function get_fp_rounding_mode() = encdec_rounding_mode(fcsr[FRM]) /* Negate a floating point number */ val negate_fp : forall 'm, 'm in {16, 32, 64}. bits('m) -> bits('m) @@ -863,7 +863,7 @@ function fp_class(xf) = { val fp_widen : forall 'm, 'm in {16, 32}. bits('m) -> bits('m * 2) function fp_widen(nval) = { - let rm_3b = fcsr.FRM(); + let rm_3b = fcsr[FRM]; let (fflags, wval) : (bits_fflags, bits('m * 2)) = match 'm { 16 => riscv_f16ToF32(rm_3b, nval), 32 => riscv_f32ToF64(rm_3b, nval) diff --git a/model/riscv_insts_vext_vm.sail b/model/riscv_insts_vext_vm.sail index b75b0799c..a144505ef 100755 --- a/model/riscv_insts_vext_vm.sail +++ b/model/riscv_insts_vext_vm.sail @@ -767,7 +767,7 @@ mapping clause encdec = FVVMTYPE(funct6, vm, vs2, vs1, vd) if haveVExt() <-> encdec_fvvmfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b001 @ vd @ 0b1010111 if haveVExt() function clause execute(FVVMTYPE(funct6, vm, vs2, vs1, vd)) = { - let rm_3b = fcsr.FRM(); + let rm_3b = fcsr[FRM]; let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); @@ -831,7 +831,7 @@ mapping clause encdec = FVFMTYPE(funct6, vm, vs2, rs1, vd) if haveVExt() <-> encdec_fvfmfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b101 @ vd @ 0b1010111 if haveVExt() function clause execute(FVFMTYPE(funct6, vm, vs2, rs1, vd)) = { - let rm_3b = fcsr.FRM(); + let rm_3b = fcsr[FRM]; let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); diff --git a/model/riscv_insts_vext_vset.sail b/model/riscv_insts_vext_vset.sail index 960036237..263b40b8f 100644 --- a/model/riscv_insts_vext_vset.sail +++ b/model/riscv_insts_vext_vset.sail @@ -92,11 +92,11 @@ function clause execute VSET_TYPE(op, ma, ta, sew, lmul, rs1, rd) = { /* set vtype */ match op { VSETVLI => { - vtype->bits() = 0b0 @ zeros(sizeof(xlen) - 9) @ ma @ ta @ sew @ lmul + vtype.bits = 0b0 @ zeros(sizeof(xlen) - 9) @ ma @ ta @ sew @ lmul }, VSETVL => { let rs2 : regidx = sew[1 .. 0] @ lmul; - vtype->bits() = X(rs2) + vtype.bits = X(rs2) } }; @@ -107,9 +107,9 @@ function clause execute VSET_TYPE(op, ma, ta, sew, lmul, rs1, rd) = { /* Note: Implementations can set vill or trap if the vtype setting is not supported. * TODO: configuration support for both solutions */ - vtype->bits() = 0b1 @ zeros(sizeof(xlen) - 1); /* set vtype.vill */ + vtype.bits = 0b1 @ zeros(sizeof(xlen) - 1); /* set vtype.vill */ vl = zeros(); - print_reg("CSR vtype <- " ^ BitStr(vtype.bits())); + print_reg("CSR vtype <- " ^ BitStr(vtype.bits)); print_reg("CSR vl <- " ^ BitStr(vl)); return RETIRE_SUCCESS }; @@ -137,11 +137,11 @@ function clause execute VSET_TYPE(op, ma, ta, sew, lmul, rs1, rd) = { /* Note: Implementations can set vill or trap if the vtype setting is not supported. * TODO: configuration support for both solutions */ - vtype->bits() = 0b1 @ zeros(sizeof(xlen) - 1); /* set vtype.vill */ + vtype.bits = 0b1 @ zeros(sizeof(xlen) - 1); /* set vtype.vill */ vl = zeros(); } }; - print_reg("CSR vtype <- " ^ BitStr(vtype.bits())); + print_reg("CSR vtype <- " ^ BitStr(vtype.bits)); print_reg("CSR vl <- " ^ BitStr(vl)); /* reset vstart to 0 */ @@ -173,7 +173,7 @@ function clause execute VSETI_TYPE(ma, ta, sew, lmul, uimm, rd) = { let ratio_pow_ori = SEW_pow_ori - LMUL_pow_ori; /* set vtype */ - vtype->bits() = 0b0 @ zeros(sizeof(xlen) - 9) @ ma @ ta @ sew @ lmul; + vtype.bits = 0b0 @ zeros(sizeof(xlen) - 9) @ ma @ ta @ sew @ lmul; /* check legal SEW and LMUL and calculate VLMAX */ let LMUL_pow_new = get_lmul_pow(); @@ -182,9 +182,9 @@ function clause execute VSETI_TYPE(ma, ta, sew, lmul, uimm, rd) = { /* Note: Implementations can set vill or trap if the vtype setting is not supported. * TODO: configuration support for both solutions */ - vtype->bits() = 0b1 @ zeros(sizeof(xlen) - 1); /* set vtype.vill */ + vtype.bits = 0b1 @ zeros(sizeof(xlen) - 1); /* set vtype.vill */ vl = zeros(); - print_reg("CSR vtype <- " ^ BitStr(vtype.bits())); + print_reg("CSR vtype <- " ^ BitStr(vtype.bits)); print_reg("CSR vl <- " ^ BitStr(vl)); return RETIRE_SUCCESS }; @@ -199,7 +199,7 @@ function clause execute VSETI_TYPE(ma, ta, sew, lmul, uimm, rd) = { * TODO: configuration support for either using ceil(AVL / 2) or VLMAX */ X(rd) = vl; - print_reg("CSR vtype <- " ^ BitStr(vtype.bits())); + print_reg("CSR vtype <- " ^ BitStr(vtype.bits)); print_reg("CSR vl <- " ^ BitStr(vl)); /* reset vstart to 0 */ diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail index dfb024746..8318aa982 100644 --- a/model/riscv_insts_zicsr.sail +++ b/model/riscv_insts_zicsr.sail @@ -91,45 +91,31 @@ function readCSR csr : csreg -> xlenbits = { (0xF12, _) => marchid, (0xF13, _) => mimpid, (0xF14, _) => mhartid, - (0x300, _) => mstatus.bits(), - (0x301, _) => misa.bits(), - (0x302, _) => medeleg.bits(), - (0x303, _) => mideleg.bits(), - (0x304, _) => mie.bits(), + (0x300, _) => mstatus.bits, + (0x301, _) => misa.bits, + (0x302, _) => medeleg.bits, + (0x303, _) => mideleg.bits, + (0x304, _) => mie.bits, (0x305, _) => get_mtvec(), - (0x306, _) => zero_extend(mcounteren.bits()), - (0x30A, _) => menvcfg.bits()[sizeof(xlen) - 1 .. 0], - (0x310, 32) => mstatush.bits(), - (0x31A, 32) => menvcfg.bits()[63 .. 32], - (0x320, _) => zero_extend(mcountinhibit.bits()), + (0x306, _) => zero_extend(mcounteren.bits), + (0x30A, _) => menvcfg.bits[sizeof(xlen) - 1 .. 0], + (0x310, 32) => mstatush.bits, + (0x31A, 32) => menvcfg.bits[63 .. 32], + (0x320, _) => zero_extend(mcountinhibit.bits), (0x340, _) => mscratch, (0x341, _) => get_xret_target(Machine) & pc_alignment_mask(), - (0x342, _) => mcause.bits(), + (0x342, _) => mcause.bits, (0x343, _) => mtval, - (0x344, _) => mip.bits(), + (0x344, _) => mip.bits, - (0x3A0, _) => pmpReadCfgReg(0), // pmpcfg0 - (0x3A1, 32) => pmpReadCfgReg(1), // pmpcfg1 - (0x3A2, _) => pmpReadCfgReg(2), // pmpcfg2 - (0x3A3, 32) => pmpReadCfgReg(3), // pmpcfg3 - - (0x3B0, _) => pmpaddr0, - (0x3B1, _) => pmpaddr1, - (0x3B2, _) => pmpaddr2, - (0x3B3, _) => pmpaddr3, - (0x3B4, _) => pmpaddr4, - (0x3B5, _) => pmpaddr5, - (0x3B6, _) => pmpaddr6, - (0x3B7, _) => pmpaddr7, - (0x3B8, _) => pmpaddr8, - (0x3B9, _) => pmpaddr9, - (0x3BA, _) => pmpaddr10, - (0x3BB, _) => pmpaddr11, - (0x3BC, _) => pmpaddr12, - (0x3BD, _) => pmpaddr13, - (0x3BE, _) => pmpaddr14, - (0x3BF, _) => pmpaddr15, + // pmpcfgN + (0x3A @ idx : bits(4), _) if idx[0] == bitzero | sizeof(xlen) == 32 => pmpReadCfgReg(unsigned(idx)), + // pmpaddrN. Unfortunately the PMP index does not nicely align with the CSR index bits. + (0x3B @ idx : bits(4), _) => pmpReadAddrReg(unsigned(0b00 @ idx)), + (0x3C @ idx : bits(4), _) => pmpReadAddrReg(unsigned(0b01 @ idx)), + (0x3D @ idx : bits(4), _) => pmpReadAddrReg(unsigned(0b10 @ idx)), + (0x3E @ idx : bits(4), _) => pmpReadAddrReg(unsigned(0b11 @ idx)), /* machine mode counters */ (0xB00, _) => mcycle[(sizeof(xlen) - 1) .. 0], @@ -141,27 +127,27 @@ function readCSR csr : csreg -> xlenbits = { (0x008, _) => zero_extend(vstart), (0x009, _) => zero_extend(vxsat), (0x00A, _) => zero_extend(vxrm), - (0x00F, _) => zero_extend(vcsr.bits()), + (0x00F, _) => zero_extend(vcsr.bits), (0xC20, _) => vl, - (0xC21, _) => vtype.bits(), + (0xC21, _) => vtype.bits, (0xC22, _) => vlenb, /* trigger/debug */ (0x7a0, _) => ~(tselect), /* this indicates we don't have any trigger support */ /* supervisor mode */ - (0x100, _) => lower_mstatus(mstatus).bits(), - (0x102, _) => sedeleg.bits(), - (0x103, _) => sideleg.bits(), - (0x104, _) => lower_mie(mie, mideleg).bits(), + (0x100, _) => lower_mstatus(mstatus).bits, + (0x102, _) => sedeleg.bits, + (0x103, _) => sideleg.bits, + (0x104, _) => lower_mie(mie, mideleg).bits, (0x105, _) => get_stvec(), - (0x106, _) => zero_extend(scounteren.bits()), - (0x10A, _) => senvcfg.bits()[sizeof(xlen) - 1 .. 0], + (0x106, _) => zero_extend(scounteren.bits), + (0x10A, _) => senvcfg.bits[sizeof(xlen) - 1 .. 0], (0x140, _) => sscratch, (0x141, _) => get_xret_target(Supervisor) & pc_alignment_mask(), - (0x142, _) => scause.bits(), + (0x142, _) => scause.bits, (0x143, _) => stval, - (0x144, _) => lower_mip(mip, mideleg).bits(), + (0x144, _) => lower_mip(mip, mideleg).bits, (0x180, _) => satp, /* user mode counters */ @@ -191,46 +177,35 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = { let res : option(xlenbits) = match (csr, sizeof(xlen)) { /* machine mode */ - (0x300, _) => { mstatus = legalize_mstatus(mstatus, value); Some(mstatus.bits()) }, - (0x301, _) => { misa = legalize_misa(misa, value); Some(misa.bits()) }, - (0x302, _) => { medeleg = legalize_medeleg(medeleg, value); Some(medeleg.bits()) }, - (0x303, _) => { mideleg = legalize_mideleg(mideleg, value); Some(mideleg.bits()) }, - (0x304, _) => { mie = legalize_mie(mie, value); Some(mie.bits()) }, + (0x300, _) => { mstatus = legalize_mstatus(mstatus, value); Some(mstatus.bits) }, + (0x301, _) => { misa = legalize_misa(misa, value); Some(misa.bits) }, + (0x302, _) => { medeleg = legalize_medeleg(medeleg, value); Some(medeleg.bits) }, + (0x303, _) => { mideleg = legalize_mideleg(mideleg, value); Some(mideleg.bits) }, + (0x304, _) => { mie = legalize_mie(mie, value); Some(mie.bits) }, (0x305, _) => { Some(set_mtvec(value)) }, - (0x306, _) => { mcounteren = legalize_mcounteren(mcounteren, value); Some(zero_extend(mcounteren.bits())) }, - (0x30A, 32) => { menvcfg = legalize_menvcfg(menvcfg, menvcfg.bits()[63 .. 32] @ value); Some(menvcfg.bits()[31 .. 0]) }, - (0x30A, 64) => { menvcfg = legalize_menvcfg(menvcfg, value); Some(menvcfg.bits()) }, - (0x310, 32) => { Some(mstatush.bits()) }, // ignore writes for now - (0x31A, 32) => { menvcfg = legalize_menvcfg(menvcfg, value @ menvcfg.bits()[31 .. 0]); Some(menvcfg.bits()[63 .. 32]) }, - (0x320, _) => { mcountinhibit = legalize_mcountinhibit(mcountinhibit, value); Some(zero_extend(mcountinhibit.bits())) }, + (0x306, _) => { mcounteren = legalize_mcounteren(mcounteren, value); Some(zero_extend(mcounteren.bits)) }, + (0x30A, 32) => { menvcfg = legalize_menvcfg(menvcfg, menvcfg.bits[63 .. 32] @ value); Some(menvcfg.bits[31 .. 0]) }, + (0x30A, 64) => { menvcfg = legalize_menvcfg(menvcfg, value); Some(menvcfg.bits) }, + (0x310, 32) => { Some(mstatush.bits) }, // ignore writes for now + (0x31A, 32) => { menvcfg = legalize_menvcfg(menvcfg, value @ menvcfg.bits[31 .. 0]); Some(menvcfg.bits[63 .. 32]) }, + (0x320, _) => { mcountinhibit = legalize_mcountinhibit(mcountinhibit, value); Some(zero_extend(mcountinhibit.bits)) }, (0x340, _) => { mscratch = value; Some(mscratch) }, (0x341, _) => { Some(set_xret_target(Machine, value)) }, - (0x342, _) => { mcause->bits() = value; Some(mcause.bits()) }, + (0x342, _) => { mcause.bits = value; Some(mcause.bits) }, (0x343, _) => { mtval = value; Some(mtval) }, - (0x344, _) => { mip = legalize_mip(mip, value); Some(mip.bits()) }, + (0x344, _) => { mip = legalize_mip(mip, value); Some(mip.bits) }, - // Note: Some(value) returned below is not the legalized value due to locked entries - (0x3A0, _) => { pmpWriteCfgReg(0, value); Some(pmpReadCfgReg(0)) }, // pmpcfg0 - (0x3A1, 32) => { pmpWriteCfgReg(1, value); Some(pmpReadCfgReg(1)) }, // pmpcfg1 - (0x3A2, _) => { pmpWriteCfgReg(2, value); Some(pmpReadCfgReg(2)) }, // pmpcfg2 - (0x3A3, 32) => { pmpWriteCfgReg(3, value); Some(pmpReadCfgReg(3)) }, // pmpcfg3 + // pmpcfgN + (0x3A @ idx : bits(4), _) if idx[0] == bitzero | sizeof(xlen) == 32 => { + let idx = unsigned(idx); + pmpWriteCfgReg(idx, value); Some(pmpReadCfgReg(idx)) + }, - (0x3B0, _) => { pmpaddr0 = pmpWriteAddr(pmpLocked(pmp0cfg), pmpTORLocked(pmp1cfg), pmpaddr0, value); Some(pmpaddr0) }, - (0x3B1, _) => { pmpaddr1 = pmpWriteAddr(pmpLocked(pmp1cfg), pmpTORLocked(pmp2cfg), pmpaddr1, value); Some(pmpaddr1) }, - (0x3B2, _) => { pmpaddr2 = pmpWriteAddr(pmpLocked(pmp2cfg), pmpTORLocked(pmp3cfg), pmpaddr2, value); Some(pmpaddr2) }, - (0x3B3, _) => { pmpaddr3 = pmpWriteAddr(pmpLocked(pmp3cfg), pmpTORLocked(pmp4cfg), pmpaddr3, value); Some(pmpaddr3) }, - (0x3B4, _) => { pmpaddr4 = pmpWriteAddr(pmpLocked(pmp4cfg), pmpTORLocked(pmp5cfg), pmpaddr4, value); Some(pmpaddr4) }, - (0x3B5, _) => { pmpaddr5 = pmpWriteAddr(pmpLocked(pmp5cfg), pmpTORLocked(pmp6cfg), pmpaddr5, value); Some(pmpaddr5) }, - (0x3B6, _) => { pmpaddr6 = pmpWriteAddr(pmpLocked(pmp6cfg), pmpTORLocked(pmp7cfg), pmpaddr6, value); Some(pmpaddr6) }, - (0x3B7, _) => { pmpaddr7 = pmpWriteAddr(pmpLocked(pmp7cfg), pmpTORLocked(pmp8cfg), pmpaddr7, value); Some(pmpaddr7) }, - (0x3B8, _) => { pmpaddr8 = pmpWriteAddr(pmpLocked(pmp8cfg), pmpTORLocked(pmp9cfg), pmpaddr8, value); Some(pmpaddr8) }, - (0x3B9, _) => { pmpaddr9 = pmpWriteAddr(pmpLocked(pmp9cfg), pmpTORLocked(pmp10cfg), pmpaddr9, value); Some(pmpaddr9) }, - (0x3BA, _) => { pmpaddr10 = pmpWriteAddr(pmpLocked(pmp10cfg), pmpTORLocked(pmp11cfg), pmpaddr10, value); Some(pmpaddr10) }, - (0x3BB, _) => { pmpaddr11 = pmpWriteAddr(pmpLocked(pmp11cfg), pmpTORLocked(pmp12cfg), pmpaddr11, value); Some(pmpaddr11) }, - (0x3BC, _) => { pmpaddr12 = pmpWriteAddr(pmpLocked(pmp12cfg), pmpTORLocked(pmp13cfg), pmpaddr12, value); Some(pmpaddr12) }, - (0x3BD, _) => { pmpaddr13 = pmpWriteAddr(pmpLocked(pmp13cfg), pmpTORLocked(pmp14cfg), pmpaddr13, value); Some(pmpaddr13) }, - (0x3BE, _) => { pmpaddr14 = pmpWriteAddr(pmpLocked(pmp14cfg), pmpTORLocked(pmp15cfg), pmpaddr14, value); Some(pmpaddr14) }, - (0x3BF, _) => { pmpaddr15 = pmpWriteAddr(pmpLocked(pmp15cfg), false, pmpaddr15, value); Some(pmpaddr15) }, + // pmpaddrN. Unfortunately the PMP index does not nicely align with the CSR index bits. + (0x3B @ idx : bits(4), _) => { let idx = unsigned(0b00 @ idx); pmpWriteAddrReg(idx, value); Some(pmpReadAddrReg(idx)) }, + (0x3C @ idx : bits(4), _) => { let idx = unsigned(0b01 @ idx); pmpWriteAddrReg(idx, value); Some(pmpReadAddrReg(idx)) }, + (0x3D @ idx : bits(4), _) => { let idx = unsigned(0b10 @ idx); pmpWriteAddrReg(idx, value); Some(pmpReadAddrReg(idx)) }, + (0x3E @ idx : bits(4), _) => { let idx = unsigned(0b11 @ idx); pmpWriteAddrReg(idx, value); Some(pmpReadAddrReg(idx)) }, /* machine mode counters */ (0xB00, _) => { mcycle[(sizeof(xlen) - 1) .. 0] = value; Some(value) }, @@ -242,18 +217,18 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = { (0x7a0, _) => { tselect = value; Some(tselect) }, /* supervisor mode */ - (0x100, _) => { mstatus = legalize_sstatus(mstatus, value); Some(mstatus.bits()) }, - (0x102, _) => { sedeleg = legalize_sedeleg(sedeleg, value); Some(sedeleg.bits()) }, - (0x103, _) => { sideleg->bits() = value; Some(sideleg.bits()) }, /* TODO: does this need legalization? */ - (0x104, _) => { mie = legalize_sie(mie, mideleg, value); Some(mie.bits()) }, + (0x100, _) => { mstatus = legalize_sstatus(mstatus, value); Some(mstatus.bits) }, + (0x102, _) => { sedeleg = legalize_sedeleg(sedeleg, value); Some(sedeleg.bits) }, + (0x103, _) => { sideleg.bits = value; Some(sideleg.bits) }, /* TODO: does this need legalization? */ + (0x104, _) => { mie = legalize_sie(mie, mideleg, value); Some(mie.bits) }, (0x105, _) => { Some(set_stvec(value)) }, - (0x106, _) => { scounteren = legalize_scounteren(scounteren, value); Some(zero_extend(scounteren.bits())) }, - (0x10A, _) => { senvcfg = legalize_senvcfg(senvcfg, zero_extend(value)); Some(senvcfg.bits()[sizeof(xlen) - 1 .. 0]) }, + (0x106, _) => { scounteren = legalize_scounteren(scounteren, value); Some(zero_extend(scounteren.bits)) }, + (0x10A, _) => { senvcfg = legalize_senvcfg(senvcfg, zero_extend(value)); Some(senvcfg.bits[sizeof(xlen) - 1 .. 0]) }, (0x140, _) => { sscratch = value; Some(sscratch) }, (0x141, _) => { Some(set_xret_target(Supervisor, value)) }, - (0x142, _) => { scause->bits() = value; Some(scause.bits()) }, + (0x142, _) => { scause.bits = value; Some(scause.bits) }, (0x143, _) => { stval = value; Some(stval) }, - (0x144, _) => { mip = legalize_sip(mip, mideleg, value); Some(mip.bits()) }, + (0x144, _) => { mip = legalize_sip(mip, mideleg, value); Some(mip.bits) }, (0x180, _) => { satp = legalize_satp(cur_Architecture(), satp, value); Some(satp) }, /* user mode: seed (entropy source). writes are ignored */ @@ -263,9 +238,9 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = { (0x008, _) => { let vstart_length = get_vlen_pow(); vstart = zero_extend(16, value[(vstart_length - 1) .. 0]); Some(zero_extend(vstart)) }, (0x009, _) => { vxsat = value[0 .. 0]; Some(zero_extend(vxsat)) }, (0x00A, _) => { vxrm = value[1 .. 0]; Some(zero_extend(vxrm)) }, - (0x00F, _) => { vcsr->bits() = value[2 ..0]; Some(zero_extend(vcsr.bits())) }, + (0x00F, _) => { vcsr.bits = value[2 ..0]; Some(zero_extend(vcsr.bits)) }, (0xC20, _) => { vl = value; Some(vl) }, - (0xC21, _) => { vtype->bits() = value; Some(vtype.bits()) }, + (0xC21, _) => { vtype.bits = value; Some(vtype.bits) }, (0xC22, _) => { vlenb = value; Some(vlenb) }, _ => ext_write_CSR(csr, value) diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail index 0f36deef5..5224938f0 100644 --- a/model/riscv_mem.sail +++ b/model/riscv_mem.sail @@ -144,7 +144,7 @@ function checked_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType( /* PMP checks if enabled */ function pmp_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), p : Privilege, paddr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool, meta : bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) = - if not(plat_enable_pmp()) + if sys_pmp_count() == 0 then checked_mem_read(t, paddr, width, aq, rl, res, meta) else { match pmpCheck(paddr, width, t, p) { @@ -158,13 +158,13 @@ function pmp_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_ $ifdef RVFI_DII val rvfi_read : forall 'n, 'n > 0. (xlenbits, atom('n), MemoryOpResult((bits(8 * 'n), mem_meta))) -> unit function rvfi_read (addr, width, result) = { - rvfi_mem_data->rvfi_mem_addr() = zero_extend(addr); + rvfi_mem_data[rvfi_mem_addr] = zero_extend(addr); rvfi_mem_data_present = true; match result { /* TODO: report tag bit for capability writes and extend mask by one bit. */ MemValue(v, _) => if width <= 16 - then { rvfi_mem_data->rvfi_mem_rdata() = sail_zero_extend(v, 256); - rvfi_mem_data->rvfi_mem_rmask() = rvfi_encode_width_mask(width) } + then { rvfi_mem_data[rvfi_mem_rdata] = sail_zero_extend(v, 256); + rvfi_mem_data[rvfi_mem_rmask] = rvfi_encode_width_mask(width) } else { internal_error(__FILE__, __LINE__, "Expected at most 16 bytes here!") }, MemException(_) => () }; @@ -232,14 +232,14 @@ function mem_write_ea (addr, width, aq, rl, con) = { $ifdef RVFI_DII val rvfi_write : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bits(8 * 'n), mem_meta, MemoryOpResult(bool)) -> unit function rvfi_write (addr, width, value, meta, result) = { - rvfi_mem_data->rvfi_mem_addr() = zero_extend(addr); + rvfi_mem_data[rvfi_mem_addr] = zero_extend(addr); rvfi_mem_data_present = true; match result { /* Log only the memory address (without the value) if the write fails. */ MemValue(_) => if width <= 16 then { /* TODO: report tag bit for capability writes and extend mask by one bit. */ - rvfi_mem_data->rvfi_mem_wdata() = sail_zero_extend(value,256); - rvfi_mem_data->rvfi_mem_wmask() = rvfi_encode_width_mask(width); + rvfi_mem_data[rvfi_mem_wdata] = sail_zero_extend(value,256); + rvfi_mem_data[rvfi_mem_wmask] = rvfi_encode_width_mask(width); } else { internal_error(__FILE__, __LINE__, "Expected at most 16 bytes here!"); }, @@ -272,7 +272,7 @@ function checked_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk : write_kin /* PMP checks if enabled */ function pmp_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk: write_kind, paddr : xlenbits, width : atom('n), data: bits(8 * 'n), typ: AccessType(ext_access_type), priv: Privilege, meta: mem_meta) -> MemoryOpResult(bool) = - if not(plat_enable_pmp()) + if sys_pmp_count() == 0 then checked_mem_write(wk, paddr, width, data, meta) else { match pmpCheck(paddr, width, typ, priv) { diff --git a/model/riscv_next_control.sail b/model/riscv_next_control.sail index 432fd0d6e..796d9dfd0 100644 --- a/model/riscv_next_control.sail +++ b/model/riscv_next_control.sail @@ -79,24 +79,24 @@ function clause ext_is_CSR_defined(0x042, _) = haveUsrMode() & haveNExt() // uca function clause ext_is_CSR_defined(0x043, _) = haveUsrMode() & haveNExt() // utval function clause ext_is_CSR_defined(0x044, _) = haveUsrMode() & haveNExt() // uip -function clause ext_read_CSR(0x000) = Some(lower_sstatus(lower_mstatus(mstatus)).bits()) -function clause ext_read_CSR(0x004) = Some(lower_sie(lower_mie(mie, mideleg), sideleg).bits()) +function clause ext_read_CSR(0x000) = Some(lower_sstatus(lower_mstatus(mstatus)).bits) +function clause ext_read_CSR(0x004) = Some(lower_sie(lower_mie(mie, mideleg), sideleg).bits) function clause ext_read_CSR(0x005) = Some(get_utvec()) function clause ext_read_CSR(0x040) = Some(uscratch) function clause ext_read_CSR(0x041) = Some(get_xret_target(User) & pc_alignment_mask()) -function clause ext_read_CSR(0x042) = Some(ucause.bits()) +function clause ext_read_CSR(0x042) = Some(ucause.bits) function clause ext_read_CSR(0x043) = Some(utval) -function clause ext_read_CSR(0x044) = Some(lower_sip(lower_mip(mip, mideleg), sideleg).bits()) +function clause ext_read_CSR(0x044) = Some(lower_sip(lower_mip(mip, mideleg), sideleg).bits) -function clause ext_write_CSR(0x000, value) = { mstatus = legalize_ustatus(mstatus, value); Some(mstatus.bits()) } +function clause ext_write_CSR(0x000, value) = { mstatus = legalize_ustatus(mstatus, value); Some(mstatus.bits) } function clause ext_write_CSR(0x004, value) = { let sie = legalize_uie(lower_mie(mie, mideleg), sideleg, value); mie = lift_sie(mie, mideleg, sie); - Some(mie.bits()) } + Some(mie.bits) } function clause ext_write_CSR(0x005, value) = { Some(set_utvec(value)) } function clause ext_write_CSR(0x040, value) = { uscratch = value; Some(uscratch) } function clause ext_write_CSR(0x041, value) = { Some(set_xret_target(User, value)) } -function clause ext_write_CSR(0x042, value) = { ucause->bits() = value; Some(ucause.bits()) } +function clause ext_write_CSR(0x042, value) = { ucause.bits = value; Some(ucause.bits) } function clause ext_write_CSR(0x043, value) = { utval = value; Some(utval) } function clause ext_write_CSR(0x044, value) = { let sip = legalize_uip(lower_mip(mip, mideleg), sideleg, value); mip = lift_sip(mip, mideleg, sip); - Some(mip.bits()) } + Some(mip.bits) } diff --git a/model/riscv_next_regs.sail b/model/riscv_next_regs.sail index b078bf88f..73d4d17eb 100644 --- a/model/riscv_next_regs.sail +++ b/model/riscv_next_regs.sail @@ -79,14 +79,14 @@ bitfield Ustatus : xlenbits = { /* This is a view, so there is no register defined. */ function lower_sstatus(s : Sstatus) -> Ustatus = { let u = Mk_Ustatus(zero_extend(0b0)); - let u = update_UPIE(u, s.UPIE()); - let u = update_UIE(u, s.UIE()); + let u = [u with UPIE = s[UPIE]]; + let u = [u with UIE = s[UIE]]; u } function lift_ustatus(s : Sstatus, u : Ustatus) -> Sstatus = { - let s = update_UPIE(s, u.UPIE()); - let s = update_UIE(s, u.UIE()); + let s = [s with UPIE = u[UPIE]]; + let s = [s with UIE = u[UIE]]; s } @@ -107,25 +107,25 @@ bitfield Uinterrupts : xlenbits = { /* Provides the uip read view of sip (s) as delegated by sideleg (d). */ function lower_sip(s : Sinterrupts, d : Sinterrupts) -> Uinterrupts = { let u : Uinterrupts = Mk_Uinterrupts(zero_extend(0b0)); - let u = update_UEI(u, s.UEI() & d.UEI()); - let u = update_UTI(u, s.UTI() & d.UTI()); - let u = update_USI(u, s.USI() & d.USI()); + let u = [u with UEI = s[UEI] & d[UEI]]; + let u = [u with UTI = s[UTI] & d[UTI]]; + let u = [u with USI = s[USI] & d[USI]]; u } /* Provides the uie read view of sie as delegated by sideleg. */ function lower_sie(s : Sinterrupts, d : Sinterrupts) -> Uinterrupts = { let u : Uinterrupts = Mk_Uinterrupts(zero_extend(0b0)); - let u = update_UEI(u, s.UEI() & d.UEI()); - let u = update_UTI(u, s.UTI() & d.UTI()); - let u = update_USI(u, s.USI() & d.USI()); + let u = [u with UEI = s[UEI] & d[UEI]]; + let u = [u with UTI = s[UTI] & d[UTI]]; + let u = [u with USI = s[USI] & d[USI]]; u } /* Returns the new value of sip from the previous sip (o) and the written uip (u) as delegated by sideleg (d). */ function lift_uip(o : Sinterrupts, d : Sinterrupts, u : Uinterrupts) -> Sinterrupts = { let s : Sinterrupts = o; - let s = if d.USI() == 0b1 then update_USI(s, u.USI()) else s; + let s = if d[USI] == 0b1 then [s with USI = u[USI]] else s; s } @@ -136,9 +136,9 @@ function legalize_uip(s : Sinterrupts, d : Sinterrupts, v : xlenbits) -> Sinterr /* Returns the new value of sie from the previous sie (o) and the written uie (u) as delegated by sideleg (d). */ function lift_uie(o : Sinterrupts, d : Sinterrupts, u : Uinterrupts) -> Sinterrupts = { let s : Sinterrupts = o; - let s = if d.UEI() == 0b1 then update_UEI(s, u.UEI()) else s; - let s = if d.UTI() == 0b1 then update_UTI(s, u.UTI()) else s; - let s = if d.USI() == 0b1 then update_USI(s, u.USI()) else s; + let s = if d[UEI] == 0b1 then [s with UEI = u[UEI]] else s; + let s = if d[UTI] == 0b1 then [s with UTI = u[UTI]] else s; + let s = if d[USI] == 0b1 then [s with USI = u[USI]] else s; s } diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail index 579a118b6..15b0d4c46 100644 --- a/model/riscv_platform.sail +++ b/model/riscv_platform.sail @@ -92,12 +92,6 @@ val elf_entry = { val plat_ram_base = {c: "plat_ram_base", ocaml: "Platform.dram_base", interpreter: "Platform.dram_base", lem: "plat_ram_base"} : unit -> xlenbits val plat_ram_size = {c: "plat_ram_size", ocaml: "Platform.dram_size", interpreter: "Platform.dram_size", lem: "plat_ram_size"} : unit -> xlenbits -/* whether the platform supports PMP configurations */ -val plat_enable_pmp = {ocaml: "Platform.enable_pmp", - interpreter: "Platform.enable_pmp", - c: "plat_enable_pmp", - lem: "plat_enable_pmp"} : unit -> bool - /* whether the MMU should update dirty bits in PTEs */ val plat_enable_dirty_update = {ocaml: "Platform.enable_dirty_update", interpreter: "Platform.enable_dirty_update", @@ -219,8 +213,8 @@ function clint_load(t, addr, width) = { if addr == MSIP_BASE & ('n == 8 | 'n == 4) then { if get_config_print_platform() - then print_platform("clint[" ^ BitStr(addr) ^ "] -> " ^ BitStr(mip.MSI())); - MemValue(sail_zero_extend(mip.MSI(), sizeof(8 * 'n))) + then print_platform("clint[" ^ BitStr(addr) ^ "] -> " ^ BitStr(mip[MSI])); + MemValue(sail_zero_extend(mip[MSI], sizeof(8 * 'n))) } else if addr == MTIMECMP_BASE & ('n == 4) then { @@ -275,11 +269,11 @@ function clint_load(t, addr, width) = { function clint_dispatch() -> unit = { if get_config_print_platform() then print_platform("clint::tick mtime <- " ^ BitStr(mtime)); - mip->MTI() = 0b0; + mip[MTI] = 0b0; if mtimecmp <=_u mtime then { if get_config_print_platform() then print_platform(" clint timer pending at mtime " ^ BitStr(mtime)); - mip->MTI() = 0b1 + mip[MTI] = 0b1 } } @@ -290,7 +284,7 @@ function clint_store(addr, width, data) = { if addr == MSIP_BASE & ('n == 8 | 'n == 4) then { if get_config_print_platform() then print_platform("clint[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data) ^ " (mip.MSI <- " ^ BitStr(data[0]) ^ ")"); - mip->MSI() = [data[0]]; + mip[MSI] = [data[0]]; clint_dispatch(); MemValue(true) } else if addr == MTIMECMP_BASE & 'n == 8 then { @@ -320,7 +314,7 @@ function clint_store(addr, width, data) = { val tick_clock : unit -> unit function tick_clock() = { - if mcountinhibit.CY() == 0b0 + if mcountinhibit[CY] == 0b0 then mcycle = mcycle + 1; mtime = mtime + 1; @@ -416,23 +410,23 @@ function htif_store(paddr, width, data) = { | (unsigned(htif_payload_writes) > 2)) then { let cmd = Mk_htif_cmd(htif_tohost); - match cmd.device() { + match cmd[device] { 0x00 => { /* syscall-proxy */ if get_config_print_platform() - then print_platform("htif-syscall-proxy cmd: " ^ BitStr(cmd.payload())); - if cmd.payload()[0] == bitone + then print_platform("htif-syscall-proxy cmd: " ^ BitStr(cmd[payload])); + if cmd[payload][0] == bitone then { htif_done = true; - htif_exit_code = (sail_zero_extend(cmd.payload(), 64) >> 1) + htif_exit_code = (sail_zero_extend(cmd[payload], 64) >> 1) } else () }, 0x01 => { /* terminal */ if get_config_print_platform() - then print_platform("htif-term cmd: " ^ BitStr(cmd.payload())); - match cmd.cmd() { + then print_platform("htif-term cmd: " ^ BitStr(cmd[payload])); + match cmd[cmd] { 0x00 => /* TODO: terminal input handling */ (), - 0x01 => plat_term_write(cmd.payload()[7..0]), + 0x01 => plat_term_write(cmd[payload][7..0]), c => print("Unknown term cmd: " ^ BitStr(c)) }; /* reset to ack */ diff --git a/model/riscv_pmp_control.sail b/model/riscv_pmp_control.sail index 998fb9228..b2da8d893 100644 --- a/model/riscv_pmp_control.sail +++ b/model/riscv_pmp_control.sail @@ -70,24 +70,30 @@ /* address ranges */ -// TODO: handle PMP grain > 4 (i.e. G > 0). // TODO: handle the 34-bit paddr32 on RV32 /* [min, max) of the matching range. */ type pmp_addr_range = option((xlenbits, xlenbits)) function pmpAddrRange(cfg: Pmpcfg_ent, pmpaddr: xlenbits, prev_pmpaddr: xlenbits) -> pmp_addr_range = { - match pmpAddrMatchType_of_bits(cfg.A()) { + match pmpAddrMatchType_of_bits(cfg[A]) { OFF => None(), TOR => { Some ((prev_pmpaddr << 2, pmpaddr << 2)) }, - NA4 => { // TODO: I find the spec unclear for entries marked NA4 and G = 1. - // (for G >= 2, it is the same as NAPOT). In particular, it affects - // whether pmpaddr[0] is always read as 0. + NA4 => { + // NA4 is not selectable when the PMP grain G >= 1. See pmpWriteCfg(). + assert(sys_pmp_grain() < 1, "NA4 cannot be selected when PMP grain G >= 1."); let lo = pmpaddr << 2; Some((lo, lo + 4)) }, - NAPOT => { let mask = pmpaddr ^ (pmpaddr + 1); // generate 1s in signifying bits + NAPOT => { + // Example pmpaddr: 0b00010101111 + // ^--- last 0 dictates region size & alignment + let mask = pmpaddr ^ (pmpaddr + 1); + // pmpaddr + 1: 0b00010110000 + // mask: 0b00000011111 + // ~mask: 0b11111100000 let lo = pmpaddr & (~ (mask)); + // mask + 1: 0b00000100000 let len = mask + 1; Some((lo << 2, (lo + len) << 2)) } @@ -99,10 +105,10 @@ function pmpAddrRange(cfg: Pmpcfg_ent, pmpaddr: xlenbits, prev_pmpaddr: xlenbits val pmpCheckRWX: (Pmpcfg_ent, AccessType(ext_access_type)) -> bool function pmpCheckRWX(ent, acc) = { match acc { - Read(_) => ent.R() == 0b1, - Write(_) => ent.W() == 0b1, - ReadWrite(_) => ent.R() == 0b1 & ent.W() == 0b1, - Execute() => ent.X() == 0b1 + Read(_) => ent[R] == 0b1, + Write(_) => ent[W] == 0b1, + ReadWrite(_) => ent[R] == 0b1 & ent[W] == 0b1, + Execute() => ent[X] == 0b1 } } @@ -152,104 +158,38 @@ function pmpMatchEntry(addr: xlenbits, width: xlenbits, acc: AccessType(ext_acce /* priority checks */ +function accessToFault(acc : AccessType(ext_access_type)) -> ExceptionType = + match acc { + Read(_) => E_Load_Access_Fault(), + Write(_) => E_SAMO_Access_Fault(), + ReadWrite(_) => E_SAMO_Access_Fault(), + Execute() => E_Fetch_Access_Fault(), + } + function pmpCheck forall 'n, 'n > 0. (addr: xlenbits, width: atom('n), acc: AccessType(ext_access_type), priv: Privilege) -> option(ExceptionType) = { let width : xlenbits = to_bits(sizeof(xlen), width); - let check : bool = - match pmpMatchEntry(addr, width, acc, priv, pmp0cfg, pmpaddr0, zeros()) { - PMP_Success => true, - PMP_Fail => false, - PMP_Continue => - match pmpMatchEntry(addr, width, acc, priv, pmp1cfg, pmpaddr1, pmpaddr0) { - PMP_Success => true, - PMP_Fail => false, - PMP_Continue => - match pmpMatchEntry(addr, width, acc, priv, pmp2cfg, pmpaddr2, pmpaddr1) { - PMP_Success => true, - PMP_Fail => false, - PMP_Continue => - match pmpMatchEntry(addr, width, acc, priv, pmp3cfg, pmpaddr3, pmpaddr2) { - PMP_Success => true, - PMP_Fail => false, - PMP_Continue => - match pmpMatchEntry(addr, width, acc, priv, pmp4cfg, pmpaddr4, pmpaddr3) { - PMP_Success => true, - PMP_Fail => false, - PMP_Continue => - match pmpMatchEntry(addr, width, acc, priv, pmp5cfg, pmpaddr5, pmpaddr4) { - PMP_Success => true, - PMP_Fail => false, - PMP_Continue => - match pmpMatchEntry(addr, width, acc, priv, pmp6cfg, pmpaddr6, pmpaddr5) { - PMP_Success => true, - PMP_Fail => false, - PMP_Continue => - match pmpMatchEntry(addr, width, acc, priv, pmp7cfg, pmpaddr7, pmpaddr6) { - PMP_Success => true, - PMP_Fail => false, - PMP_Continue => - match pmpMatchEntry(addr, width, acc, priv, pmp8cfg, pmpaddr8, pmpaddr7) { - PMP_Success => true, - PMP_Fail => false, - PMP_Continue => - match pmpMatchEntry(addr, width, acc, priv, pmp9cfg, pmpaddr9, pmpaddr8) { - PMP_Success => true, - PMP_Fail => false, - PMP_Continue => - match pmpMatchEntry(addr, width, acc, priv, pmp10cfg, pmpaddr10, pmpaddr9) { - PMP_Success => true, - PMP_Fail => false, - PMP_Continue => - match pmpMatchEntry(addr, width, acc, priv, pmp11cfg, pmpaddr11, pmpaddr10) { - PMP_Success => true, - PMP_Fail => false, - PMP_Continue => - match pmpMatchEntry(addr, width, acc, priv, pmp12cfg, pmpaddr12, pmpaddr11) { - PMP_Success => true, - PMP_Fail => false, - PMP_Continue => - match pmpMatchEntry(addr, width, acc, priv, pmp13cfg, pmpaddr13, pmpaddr12) { - PMP_Success => true, - PMP_Fail => false, - PMP_Continue => - match pmpMatchEntry(addr, width, acc, priv, pmp14cfg, pmpaddr14, pmpaddr13) { - PMP_Success => true, - PMP_Fail => false, - PMP_Continue => - match pmpMatchEntry(addr, width, acc, priv, pmp15cfg, pmpaddr15, pmpaddr14) { - PMP_Success => true, - PMP_Fail => false, - PMP_Continue => match priv { - Machine => true, - _ => false - } - }}}}}}}}}}}}}}}}; - - if check - then None() - else match acc { - Read(_) => Some(E_Load_Access_Fault()), - Write(_) => Some(E_SAMO_Access_Fault()), - ReadWrite(_) => Some(E_SAMO_Access_Fault()), - Execute() => Some(E_Fetch_Access_Fault()) - } + + foreach (i from 0 to 63) { + let prev_pmpaddr = (if i > 0 then pmpReadAddrReg(i - 1) else zeros()); + match pmpMatchEntry(addr, width, acc, priv, pmpcfg_n[i], pmpReadAddrReg(i), prev_pmpaddr) { + PMP_Success => { return None(); }, + PMP_Fail => { return Some(accessToFault(acc)); }, + PMP_Continue => (), + } + }; + if priv == Machine then None() else Some(accessToFault(acc)) } function init_pmp() -> unit = { - pmp0cfg = update_A(pmp0cfg, pmpAddrMatchType_to_bits(OFF)); - pmp1cfg = update_A(pmp1cfg, pmpAddrMatchType_to_bits(OFF)); - pmp2cfg = update_A(pmp2cfg, pmpAddrMatchType_to_bits(OFF)); - pmp3cfg = update_A(pmp3cfg, pmpAddrMatchType_to_bits(OFF)); - pmp4cfg = update_A(pmp4cfg, pmpAddrMatchType_to_bits(OFF)); - pmp5cfg = update_A(pmp5cfg, pmpAddrMatchType_to_bits(OFF)); - pmp6cfg = update_A(pmp6cfg, pmpAddrMatchType_to_bits(OFF)); - pmp7cfg = update_A(pmp7cfg, pmpAddrMatchType_to_bits(OFF)); - pmp8cfg = update_A(pmp8cfg, pmpAddrMatchType_to_bits(OFF)); - pmp9cfg = update_A(pmp9cfg, pmpAddrMatchType_to_bits(OFF)); - pmp10cfg = update_A(pmp10cfg, pmpAddrMatchType_to_bits(OFF)); - pmp11cfg = update_A(pmp11cfg, pmpAddrMatchType_to_bits(OFF)); - pmp12cfg = update_A(pmp12cfg, pmpAddrMatchType_to_bits(OFF)); - pmp13cfg = update_A(pmp13cfg, pmpAddrMatchType_to_bits(OFF)); - pmp14cfg = update_A(pmp14cfg, pmpAddrMatchType_to_bits(OFF)); - pmp15cfg = update_A(pmp15cfg, pmpAddrMatchType_to_bits(OFF)) + assert( + sys_pmp_count() == 0 | sys_pmp_count() == 16 | sys_pmp_count() == 64, + "sys_pmp_count() must be 0, 16, or 64" + ); + + foreach (i from 0 to 63) { + // On reset the PMP register's A and L bits are set to 0 unless the plaform + // mandates a different value. + pmpcfg_n[i] = [pmpcfg_n[i] with A = pmpAddrMatchType_to_bits(OFF), L = 0b0]; + }; } diff --git a/model/riscv_pmp_regs.sail b/model/riscv_pmp_regs.sail index 9b6355ca6..5f931af49 100644 --- a/model/riscv_pmp_regs.sail +++ b/model/riscv_pmp_regs.sail @@ -102,123 +102,109 @@ bitfield Pmpcfg_ent : bits(8) = { R : 0 /* read */ } -register pmp0cfg : Pmpcfg_ent -register pmp1cfg : Pmpcfg_ent -register pmp2cfg : Pmpcfg_ent -register pmp3cfg : Pmpcfg_ent -register pmp4cfg : Pmpcfg_ent -register pmp5cfg : Pmpcfg_ent -register pmp6cfg : Pmpcfg_ent -register pmp7cfg : Pmpcfg_ent -register pmp8cfg : Pmpcfg_ent -register pmp9cfg : Pmpcfg_ent -register pmp10cfg : Pmpcfg_ent -register pmp11cfg : Pmpcfg_ent -register pmp12cfg : Pmpcfg_ent -register pmp13cfg : Pmpcfg_ent -register pmp14cfg : Pmpcfg_ent -register pmp15cfg : Pmpcfg_ent - -/* PMP address configuration */ - -register pmpaddr0 : xlenbits -register pmpaddr1 : xlenbits -register pmpaddr2 : xlenbits -register pmpaddr3 : xlenbits -register pmpaddr4 : xlenbits -register pmpaddr5 : xlenbits -register pmpaddr6 : xlenbits -register pmpaddr7 : xlenbits -register pmpaddr8 : xlenbits -register pmpaddr9 : xlenbits -register pmpaddr10 : xlenbits -register pmpaddr11 : xlenbits -register pmpaddr12 : xlenbits -register pmpaddr13 : xlenbits -register pmpaddr14 : xlenbits -register pmpaddr15 : xlenbits +register pmpcfg_n : vector(64, dec, Pmpcfg_ent) +register pmpaddr_n : vector(64, dec, xlenbits) /* Packing and unpacking pmpcfg regs for xlen-width accesses */ -val pmpReadCfgReg : forall 'n, 0 <= 'n < 4 . (atom('n)) -> xlenbits -function pmpReadCfgReg(n) = { - if sizeof(xlen) == 32 - then match n { - 0 => append(pmp3cfg.bits(), append(pmp2cfg.bits(), append(pmp1cfg.bits(), pmp0cfg.bits()))), - 1 => append(pmp7cfg.bits(), append(pmp6cfg.bits(), append(pmp5cfg.bits(), pmp4cfg.bits()))), - 2 => append(pmp11cfg.bits(), append(pmp10cfg.bits(), append(pmp9cfg.bits(), pmp8cfg.bits()))), - 3 => append(pmp15cfg.bits(), append(pmp14cfg.bits(), append(pmp13cfg.bits(), pmp12cfg.bits()))), - _ => internal_error(__FILE__, __LINE__, "Unexpected pmp config reg read") - } - else match n { // sizeof(xlen) >= 64 - 0 => append(pmp7cfg.bits(), append(pmp6cfg.bits(), append(pmp5cfg.bits(), append(pmp4cfg.bits(), append(pmp3cfg.bits(), append(pmp2cfg.bits(), append(pmp1cfg.bits(), pmp0cfg.bits()))))))), - 2 => append(pmp15cfg.bits(), append(pmp14cfg.bits(), append(pmp13cfg.bits(), append(pmp12cfg.bits(), append(pmp11cfg.bits(), append(pmp10cfg.bits(), append(pmp9cfg.bits(), pmp8cfg.bits()))))))), - _ => internal_error(__FILE__, __LINE__, "Unexpected pmp config reg read") - } +function pmpReadCfgReg(n : range(0, 15)) -> xlenbits = { + if sizeof(xlen) == 32 + then { + pmpcfg_n[n*4 + 3].bits @ + pmpcfg_n[n*4 + 2].bits @ + pmpcfg_n[n*4 + 1].bits @ + pmpcfg_n[n*4 + 0].bits + } + else { + assert(n % 2 == 0, "Unexpected pmp config reg read"); + pmpcfg_n[n*4 + 7].bits @ + pmpcfg_n[n*4 + 6].bits @ + pmpcfg_n[n*4 + 5].bits @ + pmpcfg_n[n*4 + 4].bits @ + pmpcfg_n[n*4 + 3].bits @ + pmpcfg_n[n*4 + 2].bits @ + pmpcfg_n[n*4 + 1].bits @ + pmpcfg_n[n*4 + 0].bits + } +} + +function pmpReadAddrReg(n : range(0, 63)) -> xlenbits = { + let G = sys_pmp_grain(); + let match_type = pmpcfg_n[n].A(); + let addr = pmpaddr_n[n]; + + match match_type[1] { + bitone if G >= 2 => { + // [G-2..0] read as all ones to form mask, therefore we need G-1 bits. + let mask : xlenbits = zero_extend(ones(min(G - 1, sizeof(xlen)))); + addr | mask + }, + + bitzero if G >= 1 => { + // [G-1..0] read as all zeros to form mask, therefore we need G bits. + let mask : xlenbits = zero_extend(ones(min(G , sizeof(xlen)))); + addr & ~(mask) + }, + + _ => addr, + } } /* Helpers to handle locked entries */ function pmpLocked(cfg: Pmpcfg_ent) -> bool = - cfg.L() == 0b1 + cfg[L] == 0b1 function pmpTORLocked(cfg: Pmpcfg_ent) -> bool = - (cfg.L() == 0b1) & (pmpAddrMatchType_of_bits(cfg.A()) == TOR) + (cfg[L] == 0b1) & (pmpAddrMatchType_of_bits(cfg[A]) == TOR) -function pmpWriteCfg(cfg: Pmpcfg_ent, v: bits(8)) -> Pmpcfg_ent = +function pmpWriteCfg(n: range(0, 63), cfg: Pmpcfg_ent, v: bits(8)) -> Pmpcfg_ent = if pmpLocked(cfg) then cfg - else Mk_Pmpcfg_ent(v & 0x9f) // Bits 5 and 6 are zero. + else { + // Bits 5 and 6 are zero. + let cfg = Mk_Pmpcfg_ent(v & 0x9f); + + // "The R, W, and X fields form a collective WARL field for which the combinations with R=0 and W=1 are reserved." + // In this implementation if R=0 and W=1 then R, W and X are all set to 0. + // This is the least risky option from a security perspective. + let cfg = if cfg.W() == 0b1 & cfg.R() == 0b0 then [cfg with X = 0b0, W = 0b0, R = 0b0] else cfg; + + // "When G >= 1, the NA4 mode is not selectable." + // In this implementation we set it to OFF if NA4 is selected. + // This is the least risky option from a security perspective. + let cfg = if sys_pmp_grain() >= 1 & pmpAddrMatchType_of_bits(cfg.A()) == NA4 + then [cfg with A = pmpAddrMatchType_to_bits(OFF)] + else cfg; + + cfg + } -val pmpWriteCfgReg : forall 'n, 0 <= 'n < 4 . (atom('n), xlenbits) -> unit -function pmpWriteCfgReg(n, v) = { - if sizeof(xlen) == 32 - then match n { - 0 => { pmp0cfg = pmpWriteCfg(pmp0cfg, v[7 ..0]); - pmp1cfg = pmpWriteCfg(pmp1cfg, v[15..8]); - pmp2cfg = pmpWriteCfg(pmp2cfg, v[23..16]); - pmp3cfg = pmpWriteCfg(pmp3cfg, v[31..24]); - }, - 1 => { pmp4cfg = pmpWriteCfg(pmp4cfg, v[7 ..0]); - pmp5cfg = pmpWriteCfg(pmp5cfg, v[15..8]); - pmp6cfg = pmpWriteCfg(pmp6cfg, v[23..16]); - pmp7cfg = pmpWriteCfg(pmp7cfg, v[31..24]); - }, - 2 => { pmp8cfg = pmpWriteCfg(pmp8cfg, v[7 ..0]); - pmp9cfg = pmpWriteCfg(pmp9cfg, v[15..8]); - pmp10cfg = pmpWriteCfg(pmp10cfg, v[23..16]); - pmp11cfg = pmpWriteCfg(pmp11cfg, v[31..24]); - }, - 3 => { pmp12cfg = pmpWriteCfg(pmp12cfg, v[7 ..0]); - pmp13cfg = pmpWriteCfg(pmp13cfg, v[15..8]); - pmp14cfg = pmpWriteCfg(pmp14cfg, v[23..16]); - pmp15cfg = pmpWriteCfg(pmp15cfg, v[31..24]); - }, - _ => internal_error(__FILE__, __LINE__, "Unexpected pmp config reg write") - } - else if sizeof(xlen) >= 64 - then match n { - 0 => { pmp0cfg = pmpWriteCfg(pmp0cfg, v[7 ..0]); - pmp1cfg = pmpWriteCfg(pmp1cfg, v[15..8]); - pmp2cfg = pmpWriteCfg(pmp2cfg, v[23..16]); - pmp3cfg = pmpWriteCfg(pmp3cfg, v[31..24]); - pmp4cfg = pmpWriteCfg(pmp4cfg, v[39..32]); - pmp5cfg = pmpWriteCfg(pmp5cfg, v[47..40]); - pmp6cfg = pmpWriteCfg(pmp6cfg, v[55..48]); - pmp7cfg = pmpWriteCfg(pmp7cfg, v[63..56]) - }, - 2 => { pmp8cfg = pmpWriteCfg(pmp8cfg, v[7 ..0]); - pmp9cfg = pmpWriteCfg(pmp9cfg, v[15..8]); - pmp10cfg = pmpWriteCfg(pmp10cfg, v[23..16]); - pmp11cfg = pmpWriteCfg(pmp11cfg, v[31..24]); - pmp12cfg = pmpWriteCfg(pmp12cfg, v[39..32]); - pmp13cfg = pmpWriteCfg(pmp13cfg, v[47..40]); - pmp14cfg = pmpWriteCfg(pmp14cfg, v[55..48]); - pmp15cfg = pmpWriteCfg(pmp15cfg, v[63..56]) - }, - _ => internal_error(__FILE__, __LINE__, "Unexpected pmp config reg write") - } +function pmpWriteCfgReg(n : range(0, 15), v : xlenbits) -> unit = { + if sizeof(xlen) == 32 + then { + foreach (i from 0 to 3) { + let idx = n*4 + i; + pmpcfg_n[idx] = pmpWriteCfg(idx, pmpcfg_n[idx], v[8*i+7 .. 8*i]); + } + } + else { + assert(n % 2 == 0, "Unexpected pmp config reg write"); + foreach (i from 0 to 7) { + let idx = n*4 + i; + pmpcfg_n[idx] = pmpWriteCfg(idx, pmpcfg_n[idx], v[8*i+7 .. 8*i]); + } + } } function pmpWriteAddr(locked: bool, tor_locked: bool, reg: xlenbits, v: xlenbits) -> xlenbits = if sizeof(xlen) == 32 then { if (locked | tor_locked) then reg else v } else { if (locked | tor_locked) then reg else zero_extend(v[53..0]) } + +function pmpWriteAddrReg(n : range(0, 63), v : xlenbits) -> unit = { + pmpaddr_n[n] = pmpWriteAddr( + pmpLocked(pmpcfg_n[n]), + if n + 1 < 64 then pmpTORLocked(pmpcfg_n[n + 1]) else false, + pmpaddr_n[n], + v, + ); +} diff --git a/model/riscv_pte.sail b/model/riscv_pte.sail index 44c8d0c23..eb93e2dd6 100644 --- a/model/riscv_pte.sail +++ b/model/riscv_pte.sail @@ -119,7 +119,7 @@ function ext_isInvalidPTE (p : pteAttribs, std_ext : pteStdExtAttribs) -> Ext_is function isPTEPtr(p : pteAttribs, std_ext : pteStdExtAttribs) -> bool = { let a = Mk_PTE_Bits(p); - a.R() == 0b0 & a.W() == 0b0 & a.X() == 0b0 + a[R] == 0b0 & a[W] == 0b0 & a[X] == 0b0 } function isInvalidPTE(p : pteAttribs, std_ext : pteStdExtAttribs) -> bool = { @@ -129,12 +129,12 @@ function isInvalidPTE(p : pteAttribs, std_ext : pteStdExtAttribs) -> bool = { Ext_PTE_Invalid() => true, Ext_PTE_Valid() => false, Ext_PTE_Std() => { - a.V() == 0b0 | - (a.W() == 0b1 & a.R() == 0b0) | - (e.RSVD() != 0b0000000 | e.PBMT() == 0b11) | - (not(isPTEPtr(p, std_ext)) & (e.N() != 0b0 ) & (not(haveSvnapot()))) | - (not(isPTEPtr(p, std_ext)) & (e.PBMT() != 0b00) & (not(haveSvpbmt()) | menvcfg.PBMTE() == 0b0)) | - (isPTEPtr(p, std_ext) & (a.D() == 0b1 | a.A() == 0b1 | a.U() == 0b1 | e.N() != 0b0 | e.PBMT() != 0b00)) + a[V] == 0b0 | + (a[W] == 0b1 & a[R] == 0b0) | + (e[RSVD] != 0b0000000 | e[PBMT] == 0b11) | + (not(isPTEPtr(p, std_ext)) & (e[N] != 0b0 ) & (not(haveSvnapot()))) | + (not(isPTEPtr(p, std_ext)) & (e[PBMT] != 0b00) & (not(haveSvpbmt()) | menvcfg[PBMTE] == 0b0)) | + (isPTEPtr(p, std_ext) & (a[D] == 0b1 | a[A] == 0b1 | a[U] == 0b1 | e[N] != 0b0 | e[PBMT] != 0b00)) } } } @@ -153,28 +153,29 @@ function to_pte_check(b : bool) -> PTE_Check = */ function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege, mxr : bool, do_sum : bool, p : PTE_Bits, std_ext : pteStdExtAttribs, ext_ptw : ext_ptw) -> PTE_Check = { match (ac, priv) { - (Read(_), User) => to_pte_check(p.U() == 0b1 & (p.R() == 0b1 | (p.X() == 0b1 & mxr))), - (Write(_), User) => to_pte_check(p.U() == 0b1 & p.W() == 0b1), - (ReadWrite(_, _), User) => to_pte_check(p.U() == 0b1 & p.W() == 0b1 & (p.R() == 0b1 | (p.X() == 0b1 & mxr))), - (Execute(), User) => to_pte_check(p.U() == 0b1 & p.X() == 0b1), + (Read(_), User) => to_pte_check(p[U] == 0b1 & (p[R] == 0b1 | (p[X] == 0b1 & mxr))), + (Write(_), User) => to_pte_check(p[U] == 0b1 & p[W] == 0b1), + (ReadWrite(_, _), User) => to_pte_check(p[U] == 0b1 & p[W] == 0b1 & (p[R] == 0b1 | (p[X] == 0b1 & mxr))), + (Execute(), User) => to_pte_check(p[U] == 0b1 & p[X] == 0b1), - (Read(_), Supervisor) => to_pte_check((p.U() == 0b0 | do_sum) & (p.R() == 0b1 | (p.X() == 0b1 & mxr))), - (Write(_), Supervisor) => to_pte_check((p.U() == 0b0 | do_sum) & p.W() == 0b1), - (ReadWrite(_, _), Supervisor) => to_pte_check((p.U() == 0b0 | do_sum) & p.W() == 0b1 & (p.R() == 0b1 | (p.X() == 0b1 & mxr))), - (Execute(), Supervisor) => to_pte_check(p.U() == 0b0 & p.X() == 0b1), + (Read(_), Supervisor) => to_pte_check((p[U] == 0b0 | do_sum) & (p[R] == 0b1 | (p[X] == 0b1 & mxr))), + (Write(_), Supervisor) => to_pte_check((p[U] == 0b0 | do_sum) & p[W] == 0b1), + (ReadWrite(_, _), Supervisor) => to_pte_check((p[U] == 0b0 | do_sum) & p[W] == 0b1 & (p[R] == 0b1 | (p[X] == 0b1 & mxr))), + (Execute(), Supervisor) => to_pte_check(p[U] == 0b0 & p[X] == 0b1), (_, Machine) => internal_error(__FILE__, __LINE__, "m-mode mem perm check") } } -function update_PTE_Bits(p : PTE_Bits, a : AccessType(ext_access_type), std_ext : pteStdExtAttribs) -> option((PTE_Bits, pteStdExtAttribs)) = { let update_d = p.D() == 0b0 & (match a { // dirty-bit +function update_PTE_Bits(p : PTE_Bits, a : AccessType(ext_access_type), std_ext : pteStdExtAttribs) -> option((PTE_Bits, pteStdExtAttribs)) = { + let update_d = p[D] == 0b0 & (match a { // dirty-bit Execute() => false, Read() => false, Write(_) => true, ReadWrite(_,_) => true }); - let update_a = p.A() == 0b0; // accessed-bit + let update_a = p[A] == 0b0; // accessed-bit if update_d | update_a then { let np = update_A(p, 0b1); let np = if update_d then update_D(np, 0b1) else np; diff --git a/model/riscv_regs.sail b/model/riscv_regs.sail index 15e7613f0..aa1d5e635 100644 --- a/model/riscv_regs.sail +++ b/model/riscv_regs.sail @@ -154,8 +154,8 @@ function rX r = { $ifdef RVFI_DII val rvfi_wX : forall 'n, 0 <= 'n < 32. (regno('n), xlenbits) -> unit function rvfi_wX (r,v) = { - rvfi_int_data->rvfi_rd_wdata() = zero_extend(v); - rvfi_int_data->rvfi_rd_addr() = to_bits(8,r); + rvfi_int_data[rvfi_rd_wdata] = zero_extend(v); + rvfi_int_data[rvfi_rd_addr] = to_bits(8,r); rvfi_int_data_present = true; } $else @@ -204,7 +204,7 @@ function wX (r, in_v) = { if (r != 0) then { rvfi_wX(r, in_v); if get_config_print_reg() - then print_reg("x" ^ string_of_int(r) ^ " <- " ^ RegStr(v)); + then print_reg("x" ^ dec_str(r) ^ " <- " ^ RegStr(v)); } } diff --git a/model/riscv_step.sail b/model/riscv_step.sail index 550f11a4a..ec7d58e3a 100644 --- a/model/riscv_step.sail +++ b/model/riscv_step.sail @@ -83,7 +83,7 @@ function step(step_no : int) -> bool = { * written. See the note near the minstret declaration for more * information. */ - minstret_increment = mcountinhibit.IR() == 0b0; + minstret_increment = mcountinhibit[IR] == 0b0; let (retired, stepped) : (Retired, bool) = match dispatchInterrupt(cur_privilege) { @@ -113,7 +113,7 @@ function step(step_no : int) -> bool = { let ast = ext_decode_compressed(h); if get_config_print_instr() then { - print_instr("[" ^ string_of_int(step_no) ^ "] [" ^ to_str(cur_privilege) ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(h) ^ ") " ^ to_str(ast)); + print_instr("[" ^ dec_str(step_no) ^ "] [" ^ to_str(cur_privilege) ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(h) ^ ") " ^ to_str(ast)); }; /* check for RVC once here instead of every RVC execute clause. */ if haveRVC() then { @@ -129,7 +129,7 @@ function step(step_no : int) -> bool = { let ast = ext_decode(w); if get_config_print_instr() then { - print_instr("[" ^ string_of_int(step_no) ^ "] [" ^ to_str(cur_privilege) ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(w) ^ ") " ^ to_str(ast)); + print_instr("[" ^ dec_str(step_no) ^ "] [" ^ to_str(cur_privilege) ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(w) ^ ") " ^ to_str(ast)); }; nextPC = PC + 4; (execute(ast), true) diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 3830725d1..4dfe36539 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -102,29 +102,14 @@ function is_CSR_defined (csr : csreg, p : Privilege) -> bool = 0x343 => p == Machine, // mtval 0x344 => p == Machine, // mip - 0x3A0 => p == Machine, // pmpcfg0 - 0x3A1 => p == Machine & (sizeof(xlen) == 32), // pmpcfg1 - 0x3A2 => p == Machine, // pmpcfg2 - 0x3A3 => p == Machine & (sizeof(xlen) == 32), // pmpcfg3 - - 0x3B0 => p == Machine, // pmpaddr0 - 0x3B1 => p == Machine, // pmpaddr1 - 0x3B2 => p == Machine, // pmpaddr2 - 0x3B3 => p == Machine, // pmpaddr3 - 0x3B4 => p == Machine, // pmpaddr4 - 0x3B5 => p == Machine, // pmpaddr5 - 0x3B6 => p == Machine, // pmpaddr6 - 0x3B7 => p == Machine, // pmpaddr7 - 0x3B8 => p == Machine, // pmpaddr8 - 0x3B9 => p == Machine, // pmpaddr9 - 0x3BA => p == Machine, // pmpaddrA - 0x3BB => p == Machine, // pmpaddrB - 0x3BC => p == Machine, // pmpaddrC - 0x3BD => p == Machine, // pmpaddrD - 0x3BE => p == Machine, // pmpaddrE - 0x3BF => p == Machine, // pmpaddrF - - /* counters */ + // pmpcfgN + 0x3A @ idx : bits(4) => p == Machine & sys_pmp_count() > unsigned(idx) & (idx[0] == bitzero | sizeof(xlen) == 32), + + // pmpaddrN. Unfortunately the PMP index does not nicely align with the CSR index bits. + 0x3B @ idx : bits(4) => p == Machine & sys_pmp_count() > unsigned(0b00 @ idx), + 0x3C @ idx : bits(4) => p == Machine & sys_pmp_count() > unsigned(0b01 @ idx), + 0x3D @ idx : bits(4) => p == Machine & sys_pmp_count() > unsigned(0b10 @ idx), + 0x3E @ idx : bits(4) => p == Machine & sys_pmp_count() > unsigned(0b11 @ idx), 0xB00 => p == Machine, // mcycle 0xB02 => p == Machine, // minstret @@ -175,17 +160,17 @@ function check_CSR_access(csrrw, csrpr, p, isWrite) = & (privLevel_to_bits(p) >=_u csrpr) /* privilege */ function check_TVM_SATP(csr : csreg, p : Privilege) -> bool = - not(csr == 0x180 & p == Supervisor & mstatus.TVM() == 0b1) + not(csr == 0x180 & p == Supervisor & mstatus[TVM] == 0b1) function check_Counteren(csr : csreg, p : Privilege) -> bool = match(csr, p) { - (0xC00, Supervisor) => mcounteren.CY() == 0b1, - (0xC01, Supervisor) => mcounteren.TM() == 0b1, - (0xC02, Supervisor) => mcounteren.IR() == 0b1, + (0xC00, Supervisor) => mcounteren[CY] == 0b1, + (0xC01, Supervisor) => mcounteren[TM] == 0b1, + (0xC02, Supervisor) => mcounteren[IR] == 0b1, - (0xC00, User) => mcounteren.CY() == 0b1 & (not(haveSupMode()) | scounteren.CY() == 0b1), - (0xC01, User) => mcounteren.TM() == 0b1 & (not(haveSupMode()) | scounteren.TM() == 0b1), - (0xC02, User) => mcounteren.IR() == 0b1 & (not(haveSupMode()) | scounteren.IR() == 0b1), + (0xC00, User) => mcounteren[CY] == 0b1 & (not(haveSupMode()) | scounteren[CY] == 0b1), + (0xC01, User) => mcounteren[TM] == 0b1 & (not(haveSupMode()) | scounteren[TM] == 0b1), + (0xC02, User) => mcounteren[IR] == 0b1 & (not(haveSupMode()) | scounteren[IR] == 0b1), (_, _) => /* no HPM counters for now */ if 0xC03 <=_u csr & csr <=_u 0xC1F @@ -242,10 +227,10 @@ val cancel_reservation = {ocaml: "Platform.cancel_reservation", interpreter: "Pl */ function exception_delegatee(e : ExceptionType, p : Privilege) -> Privilege = { let idx = num_of_ExceptionType(e); - let super = bit_to_bool(medeleg.bits()[idx]); + let super = bit_to_bool(medeleg.bits[idx]); /* if S-mode is absent, medeleg delegates to U-mode if 'N' is supported. */ let user = if haveSupMode() - then super & haveNExt() & bit_to_bool(sedeleg.bits()[idx]) + then super & haveNExt() & bit_to_bool(sedeleg.bits[idx]) else super & haveNExt(); let deleg = if haveUsrMode() & user then User else if haveSupMode() & super then Supervisor @@ -260,15 +245,15 @@ function exception_delegatee(e : ExceptionType, p : Privilege) -> Privilege = { */ function findPendingInterrupt(ip : xlenbits) -> option(InterruptType) = { let ip = Mk_Minterrupts(ip); - if ip.MEI() == 0b1 then Some(I_M_External) - else if ip.MSI() == 0b1 then Some(I_M_Software) - else if ip.MTI() == 0b1 then Some(I_M_Timer) - else if ip.SEI() == 0b1 then Some(I_S_External) - else if ip.SSI() == 0b1 then Some(I_S_Software) - else if ip.STI() == 0b1 then Some(I_S_Timer) - else if ip.UEI() == 0b1 then Some(I_U_External) - else if ip.USI() == 0b1 then Some(I_U_Software) - else if ip.UTI() == 0b1 then Some(I_U_Timer) + if ip[MEI] == 0b1 then Some(I_M_External) + else if ip[MSI] == 0b1 then Some(I_M_Software) + else if ip[MTI] == 0b1 then Some(I_M_Timer) + else if ip[SEI] == 0b1 then Some(I_S_External) + else if ip[SSI] == 0b1 then Some(I_S_Software) + else if ip[STI] == 0b1 then Some(I_S_Timer) + else if ip[UEI] == 0b1 then Some(I_U_External) + else if ip[USI] == 0b1 then Some(I_U_Software) + else if ip[UTI] == 0b1 then Some(I_U_Timer) else None() } @@ -285,9 +270,9 @@ union interrupt_set = { function processPending(xip : Minterrupts, xie : Minterrupts, xideleg : xlenbits, priv_enabled : bool) -> interrupt_set = { /* interrupts that are enabled but not delegated are pending */ - let effective_pend = xip.bits() & xie.bits() & (~ (xideleg)); + let effective_pend = xip.bits & xie.bits & (~ (xideleg)); /* the others are delegated */ - let effective_delg = xip.bits() & xideleg; + let effective_delg = xip.bits & xideleg; /* we have pending interrupts if this privilege is enabled */ if priv_enabled & (effective_pend != zero_extend(0b0)) then Ints_Pending(effective_pend) @@ -305,17 +290,17 @@ function processPending(xip : Minterrupts, xie : Minterrupts, xideleg : xlenbits */ function getPendingSet(priv : Privilege) -> option((xlenbits, Privilege)) = { assert(haveUsrMode(), "no user mode: M/U or M/S/U system required"); - let effective_pending = mip.bits() & mie.bits(); + let effective_pending = mip.bits & mie.bits; if effective_pending == zero_extend(0b0) then None() /* fast path */ else { /* Higher privileges than the current one are implicitly enabled, * while lower privileges are blocked. An unsupported privilege is * considered blocked. */ - let mIE = priv != Machine | (priv == Machine & mstatus.MIE() == 0b1); - let sIE = haveSupMode() & (priv == User | (priv == Supervisor & mstatus.SIE() == 0b1)); - let uIE = haveNExt() & (priv == User & mstatus.UIE() == 0b1); - match processPending(mip, mie, mideleg.bits(), mIE) { + let mIE = priv != Machine | (priv == Machine & mstatus[MIE] == 0b1); + let sIE = haveSupMode() & (priv == User | (priv == Supervisor & mstatus[SIE] == 0b1)); + let uIE = haveNExt() & (priv == User & mstatus[UIE] == 0b1); + match processPending(mip, mie, mideleg.bits, mIE) { Ints_Empty() => None(), Ints_Pending(p) => let r = (p, Machine) in Some(r), Ints_Delegated(d) => @@ -324,7 +309,7 @@ function getPendingSet(priv : Privilege) -> option((xlenbits, Privilege)) = { else None() } else { /* the delegated bits are pending for S-mode */ - match processPending(Mk_Minterrupts(d), mie, sideleg.bits(), sIE) { + match processPending(Mk_Minterrupts(d), mie, sideleg.bits, sIE) { Ints_Empty() => None(), Ints_Pending(p) => let r = (p, Supervisor) in Some(r), Ints_Delegated(d) => if uIE @@ -345,7 +330,7 @@ function dispatchInterrupt(priv : Privilege) -> option((InterruptType, Privilege */ if not(haveUsrMode()) | (not(haveSupMode()) & not(haveNExt())) then { assert(priv == Machine, "invalid current privilege"); - let enabled_pending = mip.bits() & mie.bits(); + let enabled_pending = mip.bits & mie.bits; match findPendingInterrupt(enabled_pending) { Some(i) => let r = (i, Machine) in Some(r), None() => None() @@ -383,7 +368,7 @@ $ifdef RVFI_DII val rvfi_trap : unit -> unit // TODO: record rvfi_trap_data function rvfi_trap () = - rvfi_inst_data->rvfi_trap() = 0x01 + rvfi_inst_data[rvfi_trap] = 0x01 $else val rvfi_trap : unit -> unit function rvfi_trap () = () @@ -403,12 +388,12 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen match (del_priv) { Machine => { - mcause->IsInterrupt() = bool_to_bits(intr); - mcause->Cause() = zero_extend(c); + mcause[IsInterrupt] = bool_to_bits(intr); + mcause[Cause] = zero_extend(c); - mstatus->MPIE() = mstatus.MIE(); - mstatus->MIE() = 0b0; - mstatus->MPP() = privLevel_to_bits(cur_privilege); + mstatus[MPIE] = mstatus[MIE]; + mstatus[MIE] = 0b0; + mstatus[MPP] = privLevel_to_bits(cur_privilege); mtval = tval(info); mepc = pc; @@ -417,19 +402,19 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen handle_trap_extension(del_priv, pc, ext); if get_config_print_reg() - then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits())); + then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits)); prepare_trap_vector(del_priv, mcause) }, Supervisor => { assert (haveSupMode(), "no supervisor mode present for delegation"); - scause->IsInterrupt() = bool_to_bits(intr); - scause->Cause() = zero_extend(c); + scause[IsInterrupt] = bool_to_bits(intr); + scause[Cause] = zero_extend(c); - mstatus->SPIE() = mstatus.SIE(); - mstatus->SIE() = 0b0; - mstatus->SPP() = match cur_privilege { + mstatus[SPIE] = mstatus[SIE]; + mstatus[SIE] = 0b0; + mstatus[SPP] = match cur_privilege { User => 0b0, Supervisor => 0b1, Machine => internal_error(__FILE__, __LINE__, "invalid privilege for s-mode trap") @@ -442,18 +427,18 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen handle_trap_extension(del_priv, pc, ext); if get_config_print_reg() - then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits())); + then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits)); prepare_trap_vector(del_priv, scause) }, User => { assert(haveUsrMode(), "no user mode present for delegation"); - ucause->IsInterrupt() = bool_to_bits(intr); - ucause->Cause() = zero_extend(c); + ucause[IsInterrupt] = bool_to_bits(intr); + ucause[Cause] = zero_extend(c); - mstatus->UPIE() = mstatus.UIE(); - mstatus->UIE() = 0b0; + mstatus[UPIE] = mstatus[UIE]; + mstatus[UIE] = 0b0; utval = tval(info); uepc = pc; @@ -462,7 +447,7 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen handle_trap_extension(del_priv, pc, ext); if get_config_print_reg() - then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits())); + then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits)); prepare_trap_vector(del_priv, ucause) } @@ -481,15 +466,15 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result, }, (_, CTL_MRET()) => { let prev_priv = cur_privilege; - mstatus->MIE() = mstatus.MPIE(); - mstatus->MPIE() = 0b1; - cur_privilege = privLevel_of_bits(mstatus.MPP()); - mstatus->MPP() = privLevel_to_bits(if haveUsrMode() then User else Machine); + mstatus[MIE] = mstatus[MPIE]; + mstatus[MPIE] = 0b1; + cur_privilege = privLevel_of_bits(mstatus[MPP]); + mstatus[MPP] = privLevel_to_bits(if haveUsrMode() then User else Machine); if cur_privilege != Machine - then mstatus->MPRV() = 0b0; + then mstatus[MPRV] = 0b0; if get_config_print_reg() - then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits())); + then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits)); if get_config_print_platform() then print_platform("ret-ing from " ^ to_str(prev_priv) ^ " to " ^ to_str(cur_privilege)); @@ -498,15 +483,15 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result, }, (_, CTL_SRET()) => { let prev_priv = cur_privilege; - mstatus->SIE() = mstatus.SPIE(); - mstatus->SPIE() = 0b1; - cur_privilege = if mstatus.SPP() == 0b1 then Supervisor else User; - mstatus->SPP() = 0b0; + mstatus[SIE] = mstatus[SPIE]; + mstatus[SPIE] = 0b1; + cur_privilege = if mstatus[SPP] == 0b1 then Supervisor else User; + mstatus[SPP] = 0b0; if cur_privilege != Machine - then mstatus->MPRV() = 0b0; + then mstatus[MPRV] = 0b0; if get_config_print_reg() - then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits())); + then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits)); if get_config_print_platform() then print_platform("ret-ing from " ^ to_str(prev_priv) ^ " to " ^ to_str(cur_privilege)); @@ -516,12 +501,12 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result, }, (_, CTL_URET()) => { let prev_priv = cur_privilege; - mstatus->UIE() = mstatus.UPIE(); - mstatus->UPIE() = 0b1; + mstatus[UIE] = mstatus[UPIE]; + mstatus[UPIE] = 0b1; cur_privilege = User; if get_config_print_reg() - then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits())); + then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits)); if get_config_print_platform() then print_platform("ret-ing from " ^ to_str(prev_priv) ^ " to " ^ to_str(cur_privilege)); @@ -555,40 +540,40 @@ function init_sys() -> unit = { mhartid = zero_extend(0b0); - misa->MXL() = arch_to_bits(if sizeof(xlen) == 32 then RV32 else RV64); - misa->A() = 0b1; /* atomics */ - misa->C() = bool_to_bits(sys_enable_rvc()); /* RVC */ - misa->I() = 0b1; /* base integer ISA */ - misa->M() = 0b1; /* integer multiply/divide */ - misa->U() = 0b1; /* user-mode */ - misa->S() = 0b1; /* supervisor-mode */ - misa->V() = bool_to_bits(sys_enable_vext()); /* vector extension */ + misa[MXL] = arch_to_bits(if sizeof(xlen) == 32 then RV32 else RV64); + misa[A] = 0b1; /* atomics */ + misa[C] = bool_to_bits(sys_enable_rvc()); /* RVC */ + misa[I] = 0b1; /* base integer ISA */ + misa[M] = 0b1; /* integer multiply/divide */ + misa[U] = 0b1; /* user-mode */ + misa[S] = 0b1; /* supervisor-mode */ + misa[V] = bool_to_bits(sys_enable_vext()); /* vector extension */ if sys_enable_fdext() & sys_enable_zfinx() then internal_error(__FILE__, __LINE__, "F and Zfinx cannot both be enabled!"); /* We currently support both F and D */ - misa->F() = bool_to_bits(sys_enable_fdext()); /* single-precision */ - misa->D() = if sizeof(flen) >= 64 + misa[F] = bool_to_bits(sys_enable_fdext()); /* single-precision */ + misa[D] = if sizeof(flen) >= 64 then bool_to_bits(sys_enable_fdext()) /* double-precision */ else 0b0; - mstatus = set_mstatus_SXL(mstatus, misa.MXL()); - mstatus = set_mstatus_UXL(mstatus, misa.MXL()); - mstatus->SD() = 0b0; + mstatus = set_mstatus_SXL(mstatus, misa[MXL]); + mstatus = set_mstatus_UXL(mstatus, misa[MXL]); + mstatus[SD] = 0b0; /* set to little-endian mode */ if sizeof(xlen) == 64 then { - mstatus = Mk_Mstatus([mstatus.bits() with 37 .. 36 = 0b00]) + mstatus = Mk_Mstatus([mstatus.bits with 37 .. 36 = 0b00]) }; - mstatush->bits() = zero_extend(0b0); - - mip->bits() = zero_extend(0b0); - mie->bits() = zero_extend(0b0); - mideleg->bits() = zero_extend(0b0); - medeleg->bits() = zero_extend(0b0); - mtvec->bits() = zero_extend(0b0); - mcause->bits() = zero_extend(0b0); + mstatush.bits = zero_extend(0b0); + + mip.bits = zero_extend(0b0); + mie.bits = zero_extend(0b0); + mideleg.bits = zero_extend(0b0); + medeleg.bits = zero_extend(0b0); + mtvec.bits = zero_extend(0b0); + mcause.bits = zero_extend(0b0); mepc = zero_extend(0b0); mtval = zero_extend(0b0); mscratch = zero_extend(0b0); @@ -596,13 +581,13 @@ function init_sys() -> unit = { mcycle = zero_extend(0b0); mtime = zero_extend(0b0); - mcounteren->bits() = zero_extend(0b0); + mcounteren.bits = zero_extend(0b0); minstret = zero_extend(0b0); minstret_increment = true; - menvcfg->bits() = zero_extend(0b0); - senvcfg->bits() = zero_extend(0b0); + menvcfg.bits = zero_extend(0b0); + senvcfg.bits = zero_extend(0b0); /* initialize vector csrs */ elen = 0b1; /* ELEN=64 as the common case */ vlen = 0b0100; /* VLEN=512 as a default value */ @@ -613,21 +598,22 @@ function init_sys() -> unit = { vstart = zero_extend(0b0); vxsat = 0b0; vxrm = 0b00; - vcsr->vxrm() = vxrm; - vcsr->vxsat() = vxsat; + vcsr[vxrm] = vxrm; + vcsr[vxsat] = vxsat; vl = zero_extend(0b0); - vtype->vill() = 0b1; - vtype->reserved() = zero_extend(0b0); - vtype->vma() = 0b0; - vtype->vta() = 0b0; - vtype->vsew() = 0b000; - vtype->vlmul() = 0b000; - + vtype[vill] = 0b1; + vtype[reserved] = zero_extend(0b0); + vtype[vma] = 0b0; + vtype[vta] = 0b0; + vtype[vsew] = 0b000; + vtype[vlmul] = 0b000; + + // PMP's L and A fields are set to 0 on reset. init_pmp(); // log compatibility with spike if get_config_print_reg() - then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits()) ^ " (input: " ^ BitStr(zero_extend(0b0) : xlenbits) ^ ")") + then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits) ^ " (input: " ^ BitStr(zero_extend(0b0) : xlenbits) ^ ")") } /* memory access exceptions, defined here for use by the platform model. */ diff --git a/model/riscv_sys_exceptions.sail b/model/riscv_sys_exceptions.sail index 14cc05cfd..4dcdd9ec2 100644 --- a/model/riscv_sys_exceptions.sail +++ b/model/riscv_sys_exceptions.sail @@ -125,25 +125,25 @@ function prepare_xret_target(p) = /* other trap-related CSRs */ function get_mtvec() -> xlenbits = - mtvec.bits() + mtvec.bits function get_stvec() -> xlenbits = - stvec.bits() + stvec.bits function get_utvec() -> xlenbits = - utvec.bits() + utvec.bits function set_mtvec(value : xlenbits) -> xlenbits = { mtvec = legalize_tvec(mtvec, value); - mtvec.bits() + mtvec.bits } function set_stvec(value : xlenbits) -> xlenbits = { stvec = legalize_tvec(stvec, value); - stvec.bits() + stvec.bits } function set_utvec(value : xlenbits) -> xlenbits = { utvec = legalize_tvec(utvec, value); - utvec.bits() + utvec.bits } diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index a07c4fc1c..b05762986 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -153,6 +153,13 @@ val sys_enable_next = {c: "sys_enable_next", ocaml: "Platform.enable_next", _: " /* Whether FIOM bit of menvcfg/senvcfg is enabled. It must be enabled if supervisor mode is implemented and non-bare addressing modes are supported. */ val sys_enable_writable_fiom = {c: "sys_enable_writable_fiom", ocaml: "Platform.enable_writable_fiom", _: "sys_enable_writable_fiom"} : unit -> bool + +/* How many PMP entries are implemented. This must be 0, 16 or 64 (this is checked at runtime). */ +val sys_pmp_count = {c: "sys_pmp_count", ocaml: "Platform.pmp_count", _: "sys_pmp_count"} : unit -> range(0, 64) +/* G parameter that specifies the PMP grain size. The grain size is 2^(G+2), e.g. + G=0 -> 4 bytes, G=10 -> 4096 bytes. */ +val sys_pmp_grain = {c: "sys_pmp_grain", ocaml: "Platform.pmp_grain", _: "sys_pmp_grain"} : unit -> range(0, 63) + /* whether misa.v was enabled at boot */ val sys_enable_vext = {c: "sys_enable_vext", ocaml: "Platform.enable_vext", _: "sys_enable_vext"} : unit -> bool @@ -170,26 +177,26 @@ val ext_veto_disable_C : unit -> bool function legalize_misa(m : Misa, v : xlenbits) -> Misa = { let v = Mk_Misa(v); /* Suppress updates to MISA if MISA is not writable or if by disabling C next PC would become misaligned or an extension vetoes */ - if not(sys_enable_writable_misa()) | (v.C() == 0b0 & (nextPC[1] == bitone | ext_veto_disable_C())) + if not(sys_enable_writable_misa()) | (v[C] == 0b0 & (nextPC[1] == bitone | ext_veto_disable_C())) then m else { /* Suppress enabling C if C was disabled at boot (i.e. not supported) */ - let m = if not(sys_enable_rvc()) then m else update_C(m, v.C()); + let m = if not(sys_enable_rvc()) then m else [m with C = v[C]]; /* Suppress updates to misa.{f,d} if disabled at boot */ if not(sys_enable_fdext()) then m - else update_D(update_F(m, v.F()), v.D() & v.F()) + else [m with F = v[F], D = v[D] & v[F]] } } /* helpers to check support for various extensions. */ /* we currently don't model 'E', so always assume 'I'. */ -function haveAtomics() -> bool = misa.A() == 0b1 -function haveRVC() -> bool = misa.C() == 0b1 -function haveMulDiv() -> bool = misa.M() == 0b1 -function haveSupMode() -> bool = misa.S() == 0b1 -function haveUsrMode() -> bool = misa.U() == 0b1 -function haveNExt() -> bool = misa.N() == 0b1 +function haveAtomics() -> bool = misa[A] == 0b1 +function haveRVC() -> bool = misa[C] == 0b1 +function haveMulDiv() -> bool = misa[M] == 0b1 +function haveSupMode() -> bool = misa[S] == 0b1 +function haveUsrMode() -> bool = misa[U] == 0b1 +function haveNExt() -> bool = misa[N] == 0b1 /* see below for F and D (and Z*inx counterparts) extension tests */ /* BitManip extension support. */ @@ -272,21 +279,21 @@ bitfield Mstatus : xlenbits = { register mstatus : Mstatus function effectivePrivilege(t : AccessType(ext_access_type), m : Mstatus, priv : Privilege) -> Privilege = - if t != Execute() & m.MPRV() == 0b1 - then privLevel_of_bits(m.MPP()) + if t != Execute() & m[MPRV] == 0b1 + then privLevel_of_bits(m[MPP]) else priv function get_mstatus_SXL(m : Mstatus) -> arch_xlen = { if sizeof(xlen) == 32 then arch_to_bits(RV32) - else m.bits()[35 .. 34] + else m.bits[35 .. 34] } function set_mstatus_SXL(m : Mstatus, a : arch_xlen) -> Mstatus = { if sizeof(xlen) == 32 then m else { - let m = vector_update_subrange(m.bits(), 35, 34, a); + let m = vector_update_subrange(m.bits, 35, 34, a); Mk_Mstatus(m) } } @@ -294,14 +301,14 @@ function set_mstatus_SXL(m : Mstatus, a : arch_xlen) -> Mstatus = { function get_mstatus_UXL(m : Mstatus) -> arch_xlen = { if sizeof(xlen) == 32 then arch_to_bits(RV32) - else m.bits()[33 .. 32] + else m.bits[33 .. 32] } function set_mstatus_UXL(m : Mstatus, a : arch_xlen) -> Mstatus = { if sizeof(xlen) == 32 then m else { - let m = vector_update_subrange(m.bits(), 33, 32, a); + let m = vector_update_subrange(m.bits, 33, 32, a); Mk_Mstatus(m) } } @@ -315,17 +322,17 @@ function legalize_mstatus(o : Mstatus, v : xlenbits) -> Mstatus = { let m : Mstatus = Mk_Mstatus(zero_extend(v[22 .. 7] @ 0b0 @ v[5 .. 3] @ 0b0 @ v[1 .. 0])); /* We don't have any extension context yet. */ - let m = update_XS(m, extStatus_to_bits(Off)); + let m = [m with XS = extStatus_to_bits(Off)]; /* FS is WARL, and making FS writable can support the M-mode emulation of an FPU * to support code running in S/U-modes. Spike does this, and for now, we match it, * but only if Zfinx isn't enabled. * FIXME: This should be made a platform parameter. */ - let m = if sys_enable_zfinx() then update_FS(m, extStatus_to_bits(Off)) else m; - let dirty = extStatus_of_bits(m.FS()) == Dirty | extStatus_of_bits(m.XS()) == Dirty | - extStatus_of_bits(m.VS()) == Dirty; - let m = update_SD(m, bool_to_bits(dirty)); + let m = if sys_enable_zfinx() then [m with FS = extStatus_to_bits(Off)] else m; + let dirty = extStatus_of_bits(m[FS]) == Dirty | extStatus_of_bits(m[XS]) == Dirty | + extStatus_of_bits(m[VS]) == Dirty; + let m = [m with SD = bool_to_bits(dirty)]; /* We don't support dynamic changes to SXL and UXL. */ let m = set_mstatus_SXL(m, get_mstatus_SXL(o)); @@ -333,18 +340,18 @@ function legalize_mstatus(o : Mstatus, v : xlenbits) -> Mstatus = { /* We don't currently support changing MBE and SBE. */ let m = if sizeof(xlen) == 64 then { - Mk_Mstatus([m.bits() with 37 .. 36 = 0b00]) + Mk_Mstatus([m.bits with 37 .. 36 = 0b00]) } else m; /* Hardwired to zero in the absence of 'U' or 'N'. */ let m = if not(haveNExt()) then { - let m = update_UPIE(m, 0b0); - let m = update_UIE(m, 0b0); + let m = [m with UPIE = 0b0]; + let m = [m with UIE = 0b0]; m } else m; if not(haveUsrMode()) then { - let m = update_MPRV(m, 0b0); + let m = [m with MPRV = 0b0]; m } else m } @@ -354,7 +361,7 @@ function legalize_mstatus(o : Mstatus, v : xlenbits) -> Mstatus = { function cur_Architecture() -> Architecture = { let a : arch_xlen = match (cur_privilege) { - Machine => misa.MXL(), + Machine => misa[MXL], Supervisor => get_mstatus_SXL(mstatus), User => get_mstatus_UXL(mstatus) }; @@ -369,12 +376,12 @@ function in32BitMode() -> bool = { } /* F and D extensions have to enabled both via misa.{FD} as well as mstatus.FS */ -function haveFExt() -> bool = (misa.F() == 0b1) & (mstatus.FS() != 0b00) -function haveDExt() -> bool = (misa.D() == 0b1) & (mstatus.FS() != 0b00) +function haveFExt() -> bool = (misa[F] == 0b1) & (mstatus[FS] != 0b00) +function haveDExt() -> bool = (misa[D] == 0b1) & (mstatus[FS] != 0b00) /* Zfh (half-precision) extension depends on misa.F and mstatus.FS */ -function haveZfh() -> bool = (misa.F() == 0b1) & (mstatus.FS() != 0b00) +function haveZfh() -> bool = (misa[F] == 0b1) & (mstatus[FS] != 0b00) /* V extension has to enable both via misa.V as well as mstatus.VS */ -function haveVExt() -> bool = (misa.V() == 0b1) & (mstatus.VS() != 0b00) +function haveVExt() -> bool = (misa[V] == 0b1) & (mstatus[VS] != 0b00) /* Zhinx, Zfinx and Zdinx extensions (TODO: gate FCSR access on [mhs]stateen0 bit 1 when implemented) */ function haveZhinx() -> bool = sys_enable_zfinx() @@ -404,42 +411,32 @@ function legalize_mip(o : Minterrupts, v : xlenbits) -> Minterrupts = { /* The only writable bits are the S-mode bits, and with the 'N' * extension, the U-mode bits. */ let v = Mk_Minterrupts(v); - let m = update_SEI(o, v.SEI()); - let m = update_STI(m, v.STI()); - let m = update_SSI(m, v.SSI()); + let m = [o with SEI = v[SEI], STI = v[STI], SSI = v[SSI]]; if haveUsrMode() & haveNExt() then { - let m = update_UEI(m, v.UEI()); - let m = update_UTI(m, v.UTI()); - let m = update_USI(m, v.USI()); - m + [m with UEI = v[UEI], UTI = v[UTI], USI = v[USI]] } else m } function legalize_mie(o : Minterrupts, v : xlenbits) -> Minterrupts = { let v = Mk_Minterrupts(v); - let m = update_MEI(o, v.MEI()); - let m = update_MTI(m, v.MTI()); - let m = update_MSI(m, v.MSI()); - let m = update_SEI(m, v.SEI()); - let m = update_STI(m, v.STI()); - let m = update_SSI(m, v.SSI()); + let m = [o with + MEI = v[MEI], + MTI = v[MTI], + MSI = v[MSI], + SEI = v[SEI], + STI = v[STI], + SSI = v[SSI] + ]; /* The U-mode bits will be modified if we have the 'N' extension. */ if haveUsrMode() & haveNExt() then { - let m = update_UEI(m, v.UEI()); - let m = update_UTI(m, v.UTI()); - let m = update_USI(m, v.USI()); - m + [m with UEI = v[UEI], UTI = v[UTI], USI = v[USI]] } else m } function legalize_mideleg(o : Minterrupts, v : xlenbits) -> Minterrupts = { /* M-mode interrupt delegation bits "should" be hardwired to 0. */ /* FIXME: needs verification against eventual spec language. */ - let m = Mk_Minterrupts(v); - let m = update_MEI(m, 0b0); - let m = update_MTI(m, 0b0); - let m = update_MSI(m, 0b0); - m + [Mk_Minterrupts(v) with MEI = 0b0, MTI = 0b0, MSI = 0b0] } /* exception processing state */ @@ -463,10 +460,8 @@ bitfield Medeleg : xlenbits = { register medeleg : Medeleg /* Delegation to S-mode */ function legalize_medeleg(o : Medeleg, v : xlenbits) -> Medeleg = { - let m = Mk_Medeleg(v); /* M-EnvCalls delegation is not supported */ - let m = update_MEnvCall(m, 0b0); - m + [Mk_Medeleg(v) with MEnvCall = 0b0] } /* registers for trap handling */ @@ -479,10 +474,10 @@ register mtvec : Mtvec /* Trap Vector */ function legalize_tvec(o : Mtvec, v : xlenbits) -> Mtvec = { let v = Mk_Mtvec(v); - match (trapVectorMode_of_bits(v.Mode())) { + match (trapVectorMode_of_bits(v[Mode])) { TV_Direct => v, TV_Vector => v, - _ => update_Mode(v, o.Mode()) + _ => [v with Mode = o[Mode]] } } @@ -494,11 +489,11 @@ register mcause : Mcause /* Interpreting the trap-vector address */ function tvec_addr(m : Mtvec, c : Mcause) -> option(xlenbits) = { - let base : xlenbits = m.Base() @ 0b00; - match (trapVectorMode_of_bits(m.Mode())) { + let base : xlenbits = m[Base] @ 0b00; + match (trapVectorMode_of_bits(m[Mode])) { TV_Direct => Some(base), - TV_Vector => if c.IsInterrupt() == 0b1 - then Some(base + (zero_extend(c.Cause()) << 2)) + TV_Vector => if c[IsInterrupt] == 0b1 + then Some(base + (zero_extend(c[Cause]) << 2)) else Some(base), TV_Reserved => None() } @@ -514,13 +509,13 @@ register mepc : xlenbits function legalize_xepc(v : xlenbits) -> xlenbits = /* allow writing xepc[1] only if misa.C is enabled or could be enabled XXX specification says this legalization should be done on read */ - if (sys_enable_writable_misa() & sys_enable_rvc()) | misa.C() == 0b1 + if (sys_enable_writable_misa() & sys_enable_rvc()) | misa[C] == 0b1 then [v with 0 = bitzero] else v & sign_extend(0b100) /* masking for reads to xepc */ function pc_alignment_mask() -> xlenbits = - ~(zero_extend(if misa.C() == 0b1 then 0b00 else 0b10)) + ~(zero_extend(if misa[C] == 0b1 then 0b00 else 0b10)) /* auxiliary exception registers */ @@ -541,18 +536,12 @@ register scounteren : Counteren function legalize_mcounteren(c : Counteren, v : xlenbits) -> Counteren = { /* no HPM counters yet */ - let c = update_IR(c, [v[2]]); - let c = update_TM(c, [v[1]]); - let c = update_CY(c, [v[0]]); - c + [c with IR = [v[2]], TM = [v[1]], CY = [v[0]]] } function legalize_scounteren(c : Counteren, v : xlenbits) -> Counteren = { /* no HPM counters yet */ - let c = update_IR(c, [v[2]]); - let c = update_TM(c, [v[1]]); - let c = update_CY(c, [v[0]]); - c + [c with IR = [v[2]], TM = [v[1]], CY = [v[0]]] } bitfield Counterin : bits(32) = { @@ -563,9 +552,7 @@ bitfield Counterin : bits(32) = { register mcountinhibit : Counterin function legalize_mcountinhibit(c : Counterin, v : xlenbits) -> Counterin = { - let c = update_IR(c, [v[2]]); - let c = update_CY(c, [v[0]]); - c + [c with IR = [v[2]], CY = [v[0]]] } register mcycle : bits(64) @@ -620,55 +607,55 @@ bitfield Sstatus : xlenbits = { /* sstatus is a view of mstatus, so there is no register defined. */ function get_sstatus_UXL(s : Sstatus) -> arch_xlen = { - let m = Mk_Mstatus(s.bits()); + let m = Mk_Mstatus(s.bits); get_mstatus_UXL(m) } function set_sstatus_UXL(s : Sstatus, a : arch_xlen) -> Sstatus = { - let m = Mk_Mstatus(s.bits()); + let m = Mk_Mstatus(s.bits); let m = set_mstatus_UXL(m, a); - Mk_Sstatus(m.bits()) + Mk_Sstatus(m.bits) } function lower_mstatus(m : Mstatus) -> Sstatus = { let s = Mk_Sstatus(zero_extend(0b0)); - let s = update_SD(s, m.SD()); + let s = [s with SD = m[SD]]; let s = set_sstatus_UXL(s, get_mstatus_UXL(m)); - let s = update_MXR(s, m.MXR()); - let s = update_SUM(s, m.SUM()); - let s = update_XS(s, m.XS()); - let s = update_FS(s, m.FS()); - let s = update_VS(s, m.VS()); - let s = update_SPP(s, m.SPP()); - let s = update_SPIE(s, m.SPIE()); - let s = update_UPIE(s, m.UPIE()); - let s = update_SIE(s, m.SIE()); - let s = update_UIE(s, m.UIE()); + let s = [s with MXR = m[MXR]]; + let s = [s with SUM = m[SUM]]; + let s = [s with XS = m[XS]]; + let s = [s with FS = m[FS]]; + let s = [s with VS = m[VS]]; + let s = [s with SPP = m[SPP]]; + let s = [s with SPIE = m[SPIE]]; + let s = [s with UPIE = m[UPIE]]; + let s = [s with SIE = m[SIE]]; + let s = [s with UIE = m[UIE]]; s } function lift_sstatus(m : Mstatus, s : Sstatus) -> Mstatus = { - let m = update_MXR(m, s.MXR()); - let m = update_SUM(m, s.SUM()); + let m = [m with MXR = s[MXR]]; + let m = [m with SUM = s[SUM]]; - let m = update_XS(m, s.XS()); + let m = [m with XS = s[XS]]; // See comment for mstatus.FS. - let m = update_FS(m, s.FS()); - let m = update_VS(m, s.VS()); - let dirty = extStatus_of_bits(m.FS()) == Dirty | extStatus_of_bits(m.XS()) == Dirty | - extStatus_of_bits(m.VS()) == Dirty; - let m = update_SD(m, bool_to_bits(dirty)); - - let m = update_SPP(m, s.SPP()); - let m = update_SPIE(m, s.SPIE()); - let m = update_UPIE(m, s.UPIE()); - let m = update_SIE(m, s.SIE()); - let m = update_UIE(m, s.UIE()); + let m = [m with FS = s[FS]]; + let m = [m with VS = s[VS]]; + let dirty = extStatus_of_bits(m[FS]) == Dirty | extStatus_of_bits(m[XS]) == Dirty | + extStatus_of_bits(m[VS]) == Dirty; + let m = [m with SD = bool_to_bits(dirty)]; + + let m = [m with SPP = s[SPP]]; + let m = [m with SPIE = s[SPIE]]; + let m = [m with UPIE = s[UPIE]]; + let m = [m with SIE = s[SIE]]; + let m = [m with UIE = s[UIE]]; m } function legalize_sstatus(m : Mstatus, v : xlenbits) -> Mstatus = { - legalize_mstatus(m, lift_sstatus(m, Mk_Sstatus(v)).bits()) + legalize_mstatus(m, lift_sstatus(m, Mk_Sstatus(v)).bits) } bitfield Sedeleg : xlenbits = { @@ -702,35 +689,35 @@ bitfield Sinterrupts : xlenbits = { /* Provides the sip read view of mip (m) as delegated by mideleg (d). */ function lower_mip(m : Minterrupts, d : Minterrupts) -> Sinterrupts = { let s : Sinterrupts = Mk_Sinterrupts(zero_extend(0b0)); - let s = update_SEI(s, m.SEI() & d.SEI()); - let s = update_STI(s, m.STI() & d.STI()); - let s = update_SSI(s, m.SSI() & d.SSI()); + let s = [s with SEI = m[SEI] & d[SEI]]; + let s = [s with STI = m[STI] & d[STI]]; + let s = [s with SSI = m[SSI] & d[SSI]]; - let s = update_UEI(s, m.UEI() & d.UEI()); - let s = update_UTI(s, m.UTI() & d.UTI()); - let s = update_USI(s, m.USI() & d.USI()); + let s = [s with UEI = m[UEI] & d[UEI]]; + let s = [s with UTI = m[UTI] & d[UTI]]; + let s = [s with USI = m[USI] & d[USI]]; s } /* Provides the sie read view of mie (m) as delegated by mideleg (d). */ function lower_mie(m : Minterrupts, d : Minterrupts) -> Sinterrupts = { let s : Sinterrupts = Mk_Sinterrupts(zero_extend(0b0)); - let s = update_SEI(s, m.SEI() & d.SEI()); - let s = update_STI(s, m.STI() & d.STI()); - let s = update_SSI(s, m.SSI() & d.SSI()); - let s = update_UEI(s, m.UEI() & d.UEI()); - let s = update_UTI(s, m.UTI() & d.UTI()); - let s = update_USI(s, m.USI() & d.USI()); + let s = [s with SEI = m[SEI] & d[SEI]]; + let s = [s with STI = m[STI] & d[STI]]; + let s = [s with SSI = m[SSI] & d[SSI]]; + let s = [s with UEI = m[UEI] & d[UEI]]; + let s = [s with UTI = m[UTI] & d[UTI]]; + let s = [s with USI = m[USI] & d[USI]]; s } /* Returns the new value of mip from the previous mip (o) and the written sip (s) as delegated by mideleg (d). */ function lift_sip(o : Minterrupts, d : Minterrupts, s : Sinterrupts) -> Minterrupts = { let m : Minterrupts = o; - let m = if d.SSI() == 0b1 then update_SSI(m, s.SSI()) else m; + let m = if d[SSI] == 0b1 then [m with SSI = s[SSI]] else m; if haveNExt() then { - let m = if d.UEI() == 0b1 then update_UEI(m, s.UEI()) else m; - let m = if d.USI() == 0b1 then update_USI(m, s.USI()) else m; + let m = if d[UEI] == 0b1 then [m with UEI = s[UEI]] else m; + let m = if d[USI] == 0b1 then [m with USI = s[USI]] else m; m } else m } @@ -742,13 +729,13 @@ function legalize_sip(m : Minterrupts, d : Minterrupts, v : xlenbits) -> Minterr /* Returns the new value of mie from the previous mie (o) and the written sie (s) as delegated by mideleg (d). */ function lift_sie(o : Minterrupts, d : Minterrupts, s : Sinterrupts) -> Minterrupts = { let m : Minterrupts = o; - let m = if d.SEI() == 0b1 then update_SEI(m, s.SEI()) else m; - let m = if d.STI() == 0b1 then update_STI(m, s.STI()) else m; - let m = if d.SSI() == 0b1 then update_SSI(m, s.SSI()) else m; + let m = if d[SEI] == 0b1 then [m with SEI = s[SEI]] else m; + let m = if d[STI] == 0b1 then [m with STI = s[STI]] else m; + let m = if d[SSI] == 0b1 then [m with SSI = s[SSI]] else m; if haveNExt() then { - let m = if d.UEI() == 0b1 then update_UEI(m, s.UEI()) else m; - let m = if d.UTI() == 0b1 then update_UTI(m, s.UTI()) else m; - let m = if d.USI() == 0b1 then update_USI(m, s.USI()) else m; + let m = if d[UEI] == 0b1 then [m with UEI = s[UEI]] else m; + let m = if d[UTI] == 0b1 then [m with UTI = s[UTI]] else m; + let m = if d[USI] == 0b1 then [m with USI = s[USI]] else m; m } else m } @@ -779,10 +766,10 @@ bitfield Satp64 : bits(64) = { function legalize_satp64(a : Architecture, o : bits(64), v : bits(64)) -> bits(64) = { let s = Mk_Satp64(v); - match satp64Mode_of_bits(a, s.Mode()) { + match satp64Mode_of_bits(a, s[Mode]) { None() => o, Some(Sv32) => o, /* Sv32 is unsupported for now */ - Some(_) => s.bits() + Some(_) => s.bits } } @@ -879,16 +866,16 @@ register senvcfg : Envcfg function legalize_menvcfg(o : Envcfg, v : bits(64)) -> Envcfg = { let v = Mk_Envcfg(v); - let o = update_FIOM(o, if sys_enable_writable_fiom() then v.FIOM() else 0b0); + let o = [o with FIOM = if sys_enable_writable_fiom() then v[FIOM] else 0b0]; // Svpbmt - PBMTE : PBMT enable - let o = update_PBMTE(o, if haveSvpbmt() then v.PBMTE() else 0b0); + let o = [o with PBMTE = if haveSvpbmt() then v[PBMTE] else 0b0]; // Other extensions are not implemented yet so all other fields are read only zero. o } function legalize_senvcfg(o : Envcfg, v : bits(64)) -> Envcfg = { let v = Mk_Envcfg(v); - let o = update_FIOM(o, if sys_enable_writable_fiom() then v.FIOM() else 0b0); + let o = [o with FIOM = if sys_enable_writable_fiom() then v[FIOM] else 0b0]; // Other extensions are not implemented yet so all other fields are read only zero. o } @@ -899,8 +886,8 @@ function legalize_senvcfg(o : Envcfg, v : bits(64)) -> Envcfg = { function is_fiom_active() -> bool = { match cur_privilege { Machine => false, - Supervisor => menvcfg.FIOM() == 0b1, - User => (menvcfg.FIOM() | senvcfg.FIOM()) == 0b1, + Supervisor => menvcfg[FIOM] == 0b1, + User => (menvcfg[FIOM] | senvcfg[FIOM]) == 0b1, } } /* vector csrs */ @@ -924,7 +911,7 @@ register vtype : Vtype /* this returns the power of 2 for SEW */ val get_sew_pow : unit -> {|3, 4, 5, 6|} function get_sew_pow() = { - let SEW_pow : {|3, 4, 5, 6|} = match vtype.vsew() { + let SEW_pow : {|3, 4, 5, 6|} = match vtype[vsew] { 0b000 => 3, 0b001 => 4, 0b010 => 5, @@ -958,7 +945,7 @@ function get_sew_bytes() = { /* this returns the power of 2 for LMUL */ val get_lmul_pow : unit -> {|-3, -2, -1, 0, 1, 2, 3|} function get_lmul_pow() = { - match vtype.vlmul() { + match vtype[vlmul] { 0b101 => -3, 0b110 => -2, 0b111 => -1, @@ -981,7 +968,7 @@ function decode_agtype(ag) = { } val get_vtype_vma : unit -> agtype -function get_vtype_vma() = decode_agtype(vtype.vma()) +function get_vtype_vma() = decode_agtype(vtype[vma]) val get_vtype_vta : unit -> agtype -function get_vtype_vta() = decode_agtype(vtype.vta()) +function get_vtype_vta() = decode_agtype(vtype[vta]) diff --git a/model/riscv_types.sail b/model/riscv_types.sail index b9402864b..2f46156cf 100644 --- a/model/riscv_types.sail +++ b/model/riscv_types.sail @@ -143,7 +143,7 @@ function not_implemented message = throw(Error_not_implemented(message)) val internal_error : forall ('a : Type). (string, int, string) -> 'a function internal_error(file, line, s) = { - assert (false, file ^ ":" ^ string_of_int(line) ^ ": " ^ s); + assert (false, file ^ ":" ^ dec_str(line) ^ ": " ^ s); throw Error_internal_error() } @@ -419,11 +419,6 @@ enum extop_zbb = {RISCV_SEXTB, RISCV_SEXTH, RISCV_ZEXTH} enum zicondop = {RISCV_CZERO_EQZ, RISCV_CZERO_NEZ} -val sep : unit <-> string -mapping sep : unit <-> string = { - () <-> opt_spc() ^ "," ^ def_spc() -} - mapping bool_bits : bool <-> bits(1) = { true <-> 0b1, false <-> 0b0 @@ -474,9 +469,9 @@ function report_invalid_width(f , l, w, k) -> 'a = { * and remove the rest of the function. */ // internal_error(f, l, "Invalid width, " ^ size_mnemonic(w) ^ ", for " ^ k ^ - // " with xlen=" ^ string_of_int(sizeof(xlen))); - assert (false, f ^ ":" ^ string_of_int(l) ^ ": " ^ "Invalid width, " + // " with xlen=" ^ dec_str(sizeof(xlen))); + assert (false, f ^ ":" ^ dec_str(l) ^ ": " ^ "Invalid width, " ^ size_mnemonic(w) ^ ", for " ^ k ^ " with xlen=" - ^ string_of_int(sizeof(xlen))); + ^ dec_str(sizeof(xlen))); throw Error_internal_error() } diff --git a/model/riscv_vext_control.sail b/model/riscv_vext_control.sail index 0fc1660e9..931b5d7b2 100755 --- a/model/riscv_vext_control.sail +++ b/model/riscv_vext_control.sail @@ -45,14 +45,14 @@ function clause ext_is_CSR_defined (0x009, _) = true function clause ext_is_CSR_defined (0x00A, _) = true function clause ext_is_CSR_defined (0x00F, _) = true -function clause ext_read_CSR (0x009) = Some (zero_extend(vcsr.vxsat())) -function clause ext_read_CSR (0x00A) = Some (zero_extend(vcsr.vxrm())) -function clause ext_read_CSR (0x00F) = Some (zero_extend(vcsr.bits())) +function clause ext_read_CSR (0x009) = Some (zero_extend(vcsr[vxsat])) +function clause ext_read_CSR (0x00A) = Some (zero_extend(vcsr[vxrm])) +function clause ext_read_CSR (0x00F) = Some (zero_extend(vcsr.bits)) -function clause ext_read_CSR (0x009) = Some (zero_extend(vcsr.vxsat())) -function clause ext_read_CSR (0x00A) = Some (zero_extend(vcsr.vxrm())) -function clause ext_read_CSR (0x00F) = Some (zero_extend(vcsr.bits())) +function clause ext_read_CSR (0x009) = Some (zero_extend(vcsr[vxsat])) +function clause ext_read_CSR (0x00A) = Some (zero_extend(vcsr[vxrm])) +function clause ext_read_CSR (0x00F) = Some (zero_extend(vcsr.bits)) -function clause ext_write_CSR (0x009, value) = { ext_write_vcsr (vcsr.vxrm(), value[0 .. 0]); Some(zero_extend(vcsr.vxsat())) } -function clause ext_write_CSR (0x00A, value) = { ext_write_vcsr (value[1 .. 0], vcsr.vxsat()); Some(zero_extend(vcsr.vxrm())) } -function clause ext_write_CSR (0x00F, value) = { ext_write_vcsr (value [2 .. 1], value [0 .. 0]); Some(zero_extend(vcsr.bits())) } +function clause ext_write_CSR (0x009, value) = { ext_write_vcsr (vcsr[vxrm], value[0 .. 0]); Some(zero_extend(vcsr[vxsat])) } +function clause ext_write_CSR (0x00A, value) = { ext_write_vcsr (value[1 .. 0], vcsr[vxsat]); Some(zero_extend(vcsr[vxrm])) } +function clause ext_write_CSR (0x00F, value) = { ext_write_vcsr (value [2 .. 1], value [0 .. 0]); Some(zero_extend(vcsr.bits)) } diff --git a/model/riscv_vext_regs.sail b/model/riscv_vext_regs.sail index 7faa50bc3..9b81e32e9 100644 --- a/model/riscv_vext_regs.sail +++ b/model/riscv_vext_regs.sail @@ -108,8 +108,8 @@ mapping vreg_name = { function dirty_v_context() -> unit = { assert(sys_enable_vext()); - mstatus->VS() = extStatus_to_bits(Dirty); - mstatus->SD() = 0b1 + mstatus[VS] = extStatus_to_bits(Dirty); + mstatus[SD] = 0b1 } function dirty_v_context_if_present() -> unit = { @@ -202,7 +202,7 @@ function wV (r, in_v) = { let VLEN = unsigned(vlenb) * 8; assert(0 < VLEN & VLEN <= sizeof(vlenmax)); if get_config_print_reg() - then print_reg("v" ^ string_of_int(r) ^ " <- " ^ BitStr(v[VLEN - 1 .. 0])); + then print_reg("v" ^ dec_str(r) ^ " <- " ^ BitStr(v[VLEN - 1 .. 0])); } function rV_bits(i: bits(5)) -> vregtype = rV(unsigned(i)) @@ -259,8 +259,8 @@ register vcsr : Vcsr val ext_write_vcsr : (bits(2), bits(1)) -> unit function ext_write_vcsr (vxrm_val, vxsat_val) = { - vcsr->vxrm() = vxrm_val; /* Note: frm can be an illegal value, 101, 110, 111 */ - vcsr->vxsat() = vxsat_val; + vcsr[vxrm] = vxrm_val; /* Note: frm can be an illegal value, 101, 110, 111 */ + vcsr[vxsat] = vxsat_val; dirty_v_context_if_present() } diff --git a/model/riscv_vmem_common.sail b/model/riscv_vmem_common.sail index 46134d2d9..453de86e6 100644 --- a/model/riscv_vmem_common.sail +++ b/model/riscv_vmem_common.sail @@ -91,13 +91,13 @@ type asid32 = bits(9) function curAsid32(satp : bits(32)) -> asid32 = { let s = Mk_Satp32(satp); - s.Asid() + s[Asid] } /* page table base from satp */ function curPTB32(satp : bits(32)) -> paddr32 = { let s : Satp32 = Mk_Satp32(satp); - shiftl(zero_extend(s.PPN()), PAGESIZE_BITS) + shiftl(zero_extend(s[PPN]), PAGESIZE_BITS) } /* Sv32 parameters and bitfield layouts */ @@ -147,13 +147,13 @@ type asid64 = bits(16) function curAsid64(satp : bits(64)) -> asid64 = { let s = Mk_Satp64(satp); - s.Asid() + s[Asid] } /* page table base from satp */ function curPTB64(satp : bits(64)) -> paddr64 = { let s = Mk_Satp64(satp); - shiftl(zero_extend(s.PPN()), PAGESIZE_BITS) + shiftl(zero_extend(s[PPN]), PAGESIZE_BITS) } /* Sv39 parameters and bitfield layouts */ diff --git a/model/riscv_vmem_rv32.sail b/model/riscv_vmem_rv32.sail index 3478be4da..c0e20f87c 100644 --- a/model/riscv_vmem_rv32.sail +++ b/model/riscv_vmem_rv32.sail @@ -87,7 +87,7 @@ function translationMode(priv) = { match arch { Some(RV32) => { let s = Mk_Satp32(satp[31..0]); - if s.Mode() == 0b0 then Sbare else Sv32 + if s[Mode] == 0b0 then Sbare else Sv32 }, _ => internal_error(__FILE__, __LINE__, "unsupported address translation arch") } @@ -98,8 +98,8 @@ function translationMode(priv) = { val translateAddr_priv : (xlenbits, AccessType(ext_access_type), Privilege) -> TR_Result(xlenbits, ExceptionType) function translateAddr_priv(vAddr, ac, effPriv) = { - let mxr : bool = mstatus.MXR() == 0b1; - let do_sum : bool = mstatus.SUM() == 0b1; + let mxr : bool = mstatus[MXR] == 0b1; + let do_sum : bool = mstatus[SUM] == 0b1; let mode : SATPMode = translationMode(effPriv); let asid = curAsid32(satp); diff --git a/model/riscv_vmem_rv64.sail b/model/riscv_vmem_rv64.sail index 18d099192..025a1cbf9 100644 --- a/model/riscv_vmem_rv64.sail +++ b/model/riscv_vmem_rv64.sail @@ -100,7 +100,7 @@ function translationMode(priv) = { let arch = architecture(get_mstatus_SXL(mstatus)); match arch { Some(RV64) => { - let mbits : satp_mode = Mk_Satp64(satp).Mode(); + let mbits : satp_mode = Mk_Satp64(satp)[Mode]; match satp64Mode_of_bits(RV64, mbits) { Some(m) => m, None() => internal_error(__FILE__, __LINE__, "invalid RV64 translation mode in satp") @@ -108,7 +108,7 @@ function translationMode(priv) = { }, Some(RV32) => { let s = Mk_Satp32(satp[31..0]); - if s.Mode() == 0b0 then Sbare else Sv32 + if s[Mode] == 0b0 then Sbare else Sv32 }, _ => internal_error(__FILE__, __LINE__, "unsupported address translation arch") } @@ -119,8 +119,8 @@ function translationMode(priv) = { val translateAddr_priv : (xlenbits, AccessType(ext_access_type), Privilege) -> TR_Result(xlenbits, ExceptionType) function translateAddr_priv(vAddr, ac, effPriv) = { - let mxr : bool = mstatus.MXR() == 0b1; - let do_sum : bool = mstatus.SUM() == 0b1; + let mxr : bool = mstatus[MXR] == 0b1; + let do_sum : bool = mstatus[SUM] == 0b1; let mode : SATPMode = translationMode(effPriv); let asid = curAsid64(satp); diff --git a/model/riscv_vmem_sv32.sail b/model/riscv_vmem_sv32.sail index a6b810b3b..a44c4fd2e 100644 --- a/model/riscv_vmem_sv32.sail +++ b/model/riscv_vmem_sv32.sail @@ -79,12 +79,12 @@ function to_phys_addr(a : paddr32) -> xlenbits = a[31..0] val walk32 : (vaddr32, AccessType(ext_access_type), Privilege, bool, bool, paddr32, nat, bool, ext_ptw) -> PTW_Result(paddr32, SV32_PTE) function walk32(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { let va = Mk_SV32_Vaddr(vaddr); - let pt_ofs : paddr32 = shiftl(zero_extend(shiftr(va.VPNi(), (level * SV32_LEVEL_BITS))[(SV32_LEVEL_BITS - 1) .. 0]), + let pt_ofs : paddr32 = shiftl(zero_extend(shiftr(va[VPNi], (level * SV32_LEVEL_BITS))[(SV32_LEVEL_BITS - 1) .. 0]), PTE32_LOG_SIZE); let pte_addr = ptb + pt_ofs; match (mem_read_priv(Read(Data), Supervisor, to_phys_addr(pte_addr), 4, false, false, false)) { MemException(_) => { -/* print("walk32(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level) +/* print("walk32(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ dec_str(level) ^ " pt_base=" ^ BitStr(to_phys_addr(ptb)) ^ " pt_ofs=" ^ BitStr(to_phys_addr(pt_ofs)) ^ " pte_addr=" ^ BitStr(to_phys_addr(pte_addr)) @@ -93,11 +93,11 @@ function walk32(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { }, MemValue(v) => { let pte = Mk_SV32_PTE(v); - let pbits = pte.BITS(); + let pbits = pte[BITS]; let std_ext : pteStdExtAttribs = default_sv32_pte_std_ext_attribs; let pattr = Mk_PTE_Bits(pbits); - let is_global = global | (pattr.G() == 0b1); -/* print("walk32(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level) + let is_global = global | (pattr[G] == 0b1); +/* print("walk32(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ dec_str(level) ^ " pt_base=" ^ BitStr(to_phys_addr(ptb)) ^ " pt_ofs=" ^ BitStr(to_phys_addr(pt_ofs)) ^ " pte_addr=" ^ BitStr(to_phys_addr(pte_addr)) @@ -109,7 +109,7 @@ function walk32(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { if isPTEPtr(pbits, std_ext) then { if level > 0 then { /* walk down the pointer to the next level */ - walk32(vaddr, ac, priv, mxr, do_sum, shiftl(zero_extend(pte.PPNi()), PAGESIZE_BITS), level - 1, is_global, ext_ptw) + walk32(vaddr, ac, priv, mxr, do_sum, shiftl(zero_extend(pte[PPNi]), PAGESIZE_BITS), level - 1, is_global, ext_ptw) } else { /* last-level PTE contains a pointer instead of a leaf */ /* print("walk32: last-level pte contains a ptr"); */ @@ -124,24 +124,24 @@ function walk32(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { PTE_Check_Success(ext_ptw) => { if level > 0 then { /* superpage */ /* fixme hack: to get a mask of appropriate size */ - let mask = shiftl(pte.PPNi() ^ pte.PPNi() ^ zero_extend(0b1), level * SV32_LEVEL_BITS) - 1; - if (pte.PPNi() & mask) != zero_extend(0b0) then { + let mask = shiftl(pte[PPNi] ^ pte[PPNi] ^ zero_extend(0b1), level * SV32_LEVEL_BITS) - 1; + if (pte[PPNi] & mask) != zero_extend(0b0) then { /* misaligned superpage mapping */ /* print("walk32: misaligned superpage mapping"); */ PTW_Failure(PTW_Misaligned(), ext_ptw) } else { /* add the appropriate bits of the VPN to the superpage PPN */ - let ppn = pte.PPNi() | (zero_extend(va.VPNi()) & mask); -/* let res = append(ppn, va.PgOfs()); - print("walk32: using superpage: pte.ppn=" ^ BitStr(pte.PPNi()) + let ppn = pte[PPNi] | (zero_extend(va[VPNi]) & mask); +/* let res = append(ppn, va[PgOfs]); + print("walk32: using superpage: pte.ppn=" ^ BitStr(pte[PPNi]) ^ " ppn=" ^ BitStr(ppn) ^ " res=" ^ BitStr(res)); */ - PTW_Success(append(ppn, va.PgOfs()), pte, pte_addr, level, is_global, ext_ptw) + PTW_Success(append(ppn, va[PgOfs]), pte, pte_addr, level, is_global, ext_ptw) } } else { /* normal leaf PTE */ -/* let res = append(pte.PPNi(), va.PgOfs()); - print("walk32: pte.ppn=" ^ BitStr(pte.PPNi()) ^ " ppn=" ^ BitStr(pte.PPNi()) ^ " res=" ^ BitStr(res)); */ - PTW_Success(append(pte.PPNi(), va.PgOfs()), pte, pte_addr, level, is_global, ext_ptw) +/* let res = append(pte[PPNi], va[PgOfs]); + print("walk32: pte.ppn=" ^ BitStr(pte[PPNi]) ^ " ppn=" ^ BitStr(pte[PPNi]) ^ " res=" ^ BitStr(res)); */ + PTW_Success(append(pte[PPNi], va[PgOfs]), pte, pte_addr, level, is_global, ext_ptw) } } } @@ -167,7 +167,7 @@ function lookup_TLB32(asid, vaddr) = val add_to_TLB32 : (asid32, vaddr32, paddr32, SV32_PTE, paddr32, nat, bool) -> unit function add_to_TLB32(asid, vAddr, pAddr, pte, pteAddr, level, global) = { - let ent : TLB32_Entry = make_TLB_Entry(asid, global, vAddr, pAddr, pte.bits(), level, pteAddr, SV32_LEVEL_BITS); + let ent : TLB32_Entry = make_TLB_Entry(asid, global, vAddr, pAddr, pte.bits, level, pteAddr, SV32_LEVEL_BITS); tlb32 = Some(ent) } @@ -191,8 +191,8 @@ function translate32(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = Some(idx, ent) => { /* print("translate32: TLB32 hit for " ^ BitStr(vAddr)); */ let pte = Mk_SV32_PTE(ent.pte); - let std_ext : pteStdExtAttribs = default_sv32_pte_std_ext_attribs; - let pteBits = Mk_PTE_Bits(pte.BITS()); + let std_ext : pteStdExtAttribs = zeros(); // no reserved bits for extensions + let pteBits = Mk_PTE_Bits(pte[BITS]); match checkPTEPermission(ac, priv, mxr, do_sum, pteBits, std_ext, ext_ptw) { PTE_Check_Failure(ext_ptw, ext_ptw_fail) => { TR_Failure(ext_get_ptw_error(ext_ptw_fail), ext_ptw) }, PTE_Check_Success(ext_ptw) => { @@ -205,13 +205,13 @@ function translate32(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = TR_Failure(PTW_PTE_Update(), ext_ptw) } else { /* update PTE entry and TLB */ - n_pte = update_BITS(pte, pbits.bits()); + n_pte = update_BITS(pte, pbits.bits); /* ext is unused since there are no reserved bits for extensions */ n_ent : TLB32_Entry = ent; - n_ent.pte = n_pte.bits(); + n_ent.pte = n_pte.bits; write_TLB32(idx, n_ent); /* update page table */ - match mem_write_value_priv(to_phys_addr(zero_extend(ent.pteAddr)), 4, n_pte.bits(), Supervisor, false, false, false) { + match mem_write_value_priv(to_phys_addr(zero_extend(ent.pteAddr)), 4, n_pte.bits, Supervisor, false, false, false) { MemValue(_) => (), MemException(e) => internal_error(__FILE__, __LINE__, "invalid physical address in TLB") }; @@ -226,7 +226,7 @@ function translate32(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = match walk32(vAddr, ac, priv, mxr, do_sum, ptb, level, false, ext_ptw) { PTW_Failure(f, ext_ptw) => TR_Failure(f, ext_ptw), PTW_Success(pAddr, pte, pteAddr, level, global, ext_ptw) => { - match update_PTE_Bits(Mk_PTE_Bits(pte.BITS()), ac, zeros()) { + match update_PTE_Bits(Mk_PTE_Bits(pte[BITS]), ac, zeros()) { None() => { add_to_TLB32(asid, vAddr, pAddr, pte, pteAddr, level, global); TR_Address(pAddr, ext_ptw) @@ -237,9 +237,9 @@ function translate32(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = /* pte needs dirty/accessed update but that is not enabled */ TR_Failure(PTW_PTE_Update(), ext_ptw) } else { - var w_pte : SV32_PTE = update_BITS(pte, pbits.bits()); + var w_pte : SV32_PTE = update_BITS(pte, pbits.bits); /* ext is unused since there are no reserved bits for extensions */ - match mem_write_value_priv(to_phys_addr(pteAddr), 4, w_pte.bits(), Supervisor, false, false, false) { + match mem_write_value_priv(to_phys_addr(pteAddr), 4, w_pte.bits, Supervisor, false, false, false) { MemValue(_) => { add_to_TLB32(asid, vAddr, pAddr, w_pte, pteAddr, level, global); TR_Address(pAddr, ext_ptw) diff --git a/model/riscv_vmem_sv39.sail b/model/riscv_vmem_sv39.sail index 25c814487..84c28b8f6 100644 --- a/model/riscv_vmem_sv39.sail +++ b/model/riscv_vmem_sv39.sail @@ -73,12 +73,12 @@ val walk39 : (vaddr39, AccessType(ext_access_type), Privilege, bool, bool, paddr64, nat, bool, ext_ptw) -> PTW_Result(paddr64, SV39_PTE) function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { let va = Mk_SV39_Vaddr(vaddr); - let pt_ofs : paddr64 = shiftl(zero_extend(shiftr(va.VPNi(), (level * SV39_LEVEL_BITS))[(SV39_LEVEL_BITS - 1) .. 0]), + let pt_ofs : paddr64 = shiftl(zero_extend(shiftr(va[VPNi], (level * SV39_LEVEL_BITS))[(SV39_LEVEL_BITS - 1) .. 0]), PTE39_LOG_SIZE); let pte_addr = ptb + pt_ofs; match (mem_read_priv(Read(Data), Supervisor, zero_extend(pte_addr), 8, false, false, false)) { MemException(_) => { -/* print("walk39(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level) +/* print("walk39(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ dec_str(level) ^ " pt_base=" ^ BitStr(ptb) ^ " pt_ofs=" ^ BitStr(pt_ofs) ^ " pte_addr=" ^ BitStr(pte_addr) @@ -87,11 +87,11 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { }, MemValue(v) => { let pte = Mk_SV39_PTE(v); - let pbits = pte.BITS(); - let std_ext = pte.Ext(); + let pbits = pte[BITS]; + let std_ext = pte[Ext]; let pattr = Mk_PTE_Bits(pbits); let eattr = Mk_PTE_StdExt_Bits(std_ext); - let is_global = global | (pattr.G() == 0b1); + let is_global = global | (pattr[G] == 0b1); /* print("walk39(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level) ^ " pt_base=" ^ BitStr(ptb) ^ " pt_ofs=" ^ BitStr(pt_ofs) @@ -104,7 +104,7 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { if isPTEPtr(pbits, std_ext) then { if level > 0 then { /* walk down the pointer to the next level */ - walk39(vaddr, ac, priv, mxr, do_sum, shiftl(zero_extend(pte.PPNi()), PAGESIZE_BITS), level - 1, is_global, ext_ptw) + walk39(vaddr, ac, priv, mxr, do_sum, shiftl(zero_extend(pte[PPNi]), PAGESIZE_BITS), level - 1, is_global, ext_ptw) } else { /* last-level PTE contains a pointer instead of a leaf */ /* print("walk39: last-level pte contains a ptr"); */ @@ -119,34 +119,34 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { PTE_Check_Success(ext_ptw) => { if level > 0 then { /* superpage */ /* fixme hack: to get a mask of appropriate size */ - let mask = shiftl(pte.PPNi() ^ pte.PPNi() ^ zero_extend(0b1), level * SV39_LEVEL_BITS) - 1; - if haveSvnapot() & eattr.N() == 0b1 then { + let mask = shiftl(pte[PPNi] ^ pte[PPNi] ^ zero_extend(0b1), level * SV39_LEVEL_BITS) - 1; + if haveSvnapot() & eattr[N] == 0b1 then { PTW_Failure(PTW_Invalid_PTE(), ext_ptw) - } else if (pte.PPNi() & mask) != zero_extend(0b0) then { + } else if (pte[PPNi] & mask) != zero_extend(0b0) then { /* misaligned superpage mapping */ /* print("walk39: misaligned superpage mapping"); */ PTW_Failure(PTW_Misaligned(), ext_ptw) } else { /* add the appropriate bits of the VPN to the superpage PPN */ - let ppn = pte.PPNi() | (zero_extend(va.VPNi()) & mask); -/* let res = append(ppn, va.PgOfs()); - print("walk39: using superpage: pte.ppn=" ^ BitStr(pte.PPNi()) + let ppn = pte[PPNi] | (zero_extend(va[VPNi]) & mask); +/* let res = append(ppn, va[PgOfs]); + print("walk39: using superpage: pte.ppn=" ^ BitStr(pte[PPNi]) ^ " ppn=" ^ BitStr(ppn) ^ " res=" ^ BitStr(res)); */ - PTW_Success(append(ppn, va.PgOfs()), pte, pte_addr, level, is_global, ext_ptw) + PTW_Success(append(ppn, va[PgOfs]), pte, pte_addr, level, is_global, ext_ptw) } } else { /* normal leaf PTE */ - if ( haveSvnapot() & eattr.N() == 0b1 & pte.PPNi()[3 .. 0] != 0b1000 ) then { + if ( haveSvnapot() & eattr[N] == 0b1 & pte.PPNi()[3 .. 0] != 0b1000 ) then { PTW_Failure(PTW_Invalid_PTE(), ext_ptw) } else { - let ppn : bits(44) = match (haveSvnapot(), eattr.N()) { - (false, _) => pte.PPNi(), - (true, 0b0) => pte.PPNi(), + let ppn : bits(44) = match (haveSvnapot(), eattr[N]) { + (false, _) => pte[PPNi], + (true, 0b0) => pte[PPNi], (true, 0b1) => append(pte.PPNi()[43 .. 4], va.VPNi()[3 .. 0]) }; -/* let res = append(ppn, va.PgOfs()); - print("walk39: pte.ppn=" ^ BitStr(pte.PPNi()) ^ " ppn=" ^ BitStr(ppn) ^ " res=" ^ BitStr(res)); */ - PTW_Success(append(ppn, va.PgOfs()), pte, pte_addr, level, is_global, ext_ptw) +/* let res = append(ppn, va[PgOfs]); + print("walk39: pte.ppn=" ^ BitStr(pte[PPNi]) ^ " ppn=" ^ BitStr(ppn) ^ " res=" ^ BitStr(res)); */ + PTW_Success(append(ppn, va[PgOfs]), pte, pte_addr, level, is_global, ext_ptw) } } } @@ -173,7 +173,7 @@ function lookup_TLB39(asid, vaddr) = val add_to_TLB39 : (asid64, vaddr39, paddr64, SV39_PTE, paddr64, nat, bool) -> unit function add_to_TLB39(asid, vAddr, pAddr, pte, pteAddr, level, global) = { - let ent : TLB39_Entry = make_TLB_Entry(asid, global, vAddr, pAddr, pte.bits(), level, pteAddr, SV39_LEVEL_BITS); + let ent : TLB39_Entry = make_TLB_Entry(asid, global, vAddr, pAddr, pte.bits, level, pteAddr, SV39_LEVEL_BITS); tlb39 = Some(ent) } @@ -211,13 +211,13 @@ function translate39(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = TR_Failure(PTW_PTE_Update(), ext_ptw) } else { /* update PTE entry and TLB */ - n_pte = update_BITS(pte, pbits.bits()); + n_pte = update_BITS(pte, pbits.bits); n_pte = update_Ext(n_pte, ext); n_ent : TLB39_Entry = ent; - n_ent.pte = n_pte.bits(); + n_ent.pte = n_pte.bits; write_TLB39(idx, n_ent); /* update page table */ - match mem_write_value_priv(zero_extend(ent.pteAddr), 8, n_pte.bits(), Supervisor, false, false, false) { + match mem_write_value_priv(zero_extend(ent.pteAddr), 8, n_pte.bits, Supervisor, false, false, false) { MemValue(_) => (), MemException(e) => internal_error(__FILE__, __LINE__, "invalid physical address in TLB") }; @@ -232,7 +232,7 @@ function translate39(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = match walk39(vAddr, ac, priv, mxr, do_sum, ptb, level, false, ext_ptw) { PTW_Failure(f, ext_ptw) => TR_Failure(f, ext_ptw), PTW_Success(pAddr, pte, pteAddr, level, global, ext_ptw) => { - match update_PTE_Bits(Mk_PTE_Bits(pte.BITS()), ac, pte.Ext()) { + match update_PTE_Bits(Mk_PTE_Bits(pte[BITS]), ac, pte[Ext]) { None() => { add_to_TLB39(asid, vAddr, pAddr, pte, pteAddr, level, global); TR_Address(pAddr, ext_ptw) @@ -243,9 +243,9 @@ function translate39(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = /* pte needs dirty/accessed update but that is not enabled */ TR_Failure(PTW_PTE_Update(), ext_ptw) } else { - var w_pte : SV39_PTE = update_BITS(pte, pbits.bits()); + var w_pte : SV39_PTE = update_BITS(pte, pbits.bits); w_pte = update_Ext(w_pte, ext); - match mem_write_value_priv(zero_extend(pteAddr), 8, w_pte.bits(), Supervisor, false, false, false) { + match mem_write_value_priv(zero_extend(pteAddr), 8, w_pte.bits, Supervisor, false, false, false) { MemValue(_) => { add_to_TLB39(asid, vAddr, pAddr, w_pte, pteAddr, level, global); TR_Address(pAddr, ext_ptw) diff --git a/model/riscv_vmem_sv48.sail b/model/riscv_vmem_sv48.sail index 3d8cc64ce..97630f3f9 100644 --- a/model/riscv_vmem_sv48.sail +++ b/model/riscv_vmem_sv48.sail @@ -73,12 +73,12 @@ val walk48 : (vaddr48, AccessType(ext_access_type), Privilege, bool, bool, paddr64, nat, bool, ext_ptw) -> PTW_Result(paddr64, SV48_PTE) function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { let va = Mk_SV48_Vaddr(vaddr); - let pt_ofs : paddr64 = shiftl(zero_extend(shiftr(va.VPNi(), (level * SV48_LEVEL_BITS))[(SV48_LEVEL_BITS - 1) .. 0]), + let pt_ofs : paddr64 = shiftl(zero_extend(shiftr(va[VPNi], (level * SV48_LEVEL_BITS))[(SV48_LEVEL_BITS - 1) .. 0]), PTE48_LOG_SIZE); let pte_addr = ptb + pt_ofs; match (mem_read_priv(Read(Data), Supervisor, zero_extend(pte_addr), 8, false, false, false)) { MemException(_) => { -/* print("walk48(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level) +/* print("walk48(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ dec_str(level) ^ " pt_base=" ^ BitStr(ptb) ^ " pt_ofs=" ^ BitStr(pt_ofs) ^ " pte_addr=" ^ BitStr(pte_addr) @@ -87,11 +87,11 @@ function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { }, MemValue(v) => { let pte = Mk_SV48_PTE(v); - let pbits = pte.BITS(); - let std_ext = pte.Ext(); + let pbits = pte[BITS]; + let std_ext = pte[Ext]; let pattr = Mk_PTE_Bits(pbits); let eattr = Mk_PTE_StdExt_Bits(std_ext); - let is_global = global | (pattr.G() == 0b1); + let is_global = global | (pattr[G] == 0b1); /* print("walk48(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level) ^ " pt_base=" ^ BitStr(ptb) ^ " pt_ofs=" ^ BitStr(pt_ofs) @@ -104,7 +104,7 @@ function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { if isPTEPtr(pbits, std_ext) then { if level > 0 then { /* walk down the pointer to the next level */ - walk48(vaddr, ac, priv, mxr, do_sum, shiftl(zero_extend(pte.PPNi()), PAGESIZE_BITS), level - 1, is_global, ext_ptw) + walk48(vaddr, ac, priv, mxr, do_sum, shiftl(zero_extend(pte[PPNi]), PAGESIZE_BITS), level - 1, is_global, ext_ptw) } else { /* last-level PTE contains a pointer instead of a leaf */ /* print("walk48: last-level pte contains a ptr"); */ @@ -119,34 +119,34 @@ function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { PTE_Check_Success(ext_ptw) => { if level > 0 then { /* superpage */ /* fixme hack: to get a mask of appropriate size */ - let mask = shiftl(pte.PPNi() ^ pte.PPNi() ^ zero_extend(0b1), level * SV48_LEVEL_BITS) - 1; - if haveSvnapot() & eattr.N() == 0b1 then { + let mask = shiftl(pte[PPNi] ^ pte[PPNi] ^ zero_extend(0b1), level * SV48_LEVEL_BITS) - 1; + if haveSvnapot() & eattr[N] == 0b1 then { PTW_Failure(PTW_Invalid_PTE(), ext_ptw) - } else if (pte.PPNi() & mask) != zero_extend(0b0) then { + } else if (pte[PPNi] & mask) != zero_extend(0b0) then { /* misaligned superpage mapping */ /* print("walk48: misaligned superpage mapping"); */ PTW_Failure(PTW_Misaligned(), ext_ptw) } else { /* add the appropriate bits of the VPN to the superpage PPN */ - let ppn = pte.PPNi() | (zero_extend(va.VPNi()) & mask); -/* let res = append(ppn, va.PgOfs()); - print("walk48: using superpage: pte.ppn=" ^ BitStr(pte.PPNi()) + let ppn = pte[PPNi] | (zero_extend(va[VPNi]) & mask); +/* let res = append(ppn, va[PgOfs]); + print("walk48: using superpage: pte.ppn=" ^ BitStr(pte[PPNi]) ^ " ppn=" ^ BitStr(ppn) ^ " res=" ^ BitStr(res)); */ - PTW_Success(append(ppn, va.PgOfs()), pte, pte_addr, level, is_global, ext_ptw) + PTW_Success(append(ppn, va[PgOfs]), pte, pte_addr, level, is_global, ext_ptw) } } else { /* normal leaf PTE */ - if ( haveSvnapot() & eattr.N() == 0b1 & pte.PPNi()[3 .. 0] != 0b1000 ) then { + if ( haveSvnapot() & eattr[N] == 0b1 & pte.PPNi()[3 .. 0] != 0b1000 ) then { PTW_Failure(PTW_Invalid_PTE(), ext_ptw) } else { - let ppn : bits(44) = match (haveSvnapot(), eattr.N()) { - (false, _) => pte.PPNi(), - (true, 0b0) => pte.PPNi(), + let ppn : bits(44) = match (haveSvnapot(), eattr[N]) { + (false, _) => pte[PPNi], + (true, 0b0) => pte[PPNi], (true, 0b1) => append(pte.PPNi()[43 .. 4], va.VPNi()[3 .. 0]) }; -/* let res = append(ppn, va.PgOfs()); - print("walk48: pte.ppn=" ^ BitStr(pte.PPNi()) ^ " ppn=" ^ BitStr(ppn) ^ " res=" ^ BitStr(res)); */ - PTW_Success(append(ppn, va.PgOfs()), pte, pte_addr, level, is_global, ext_ptw) +/* let res = append(ppn, va[PgOfs]); + print("walk48: pte.ppn=" ^ BitStr(pte[PPNi]) ^ " ppn=" ^ BitStr(ppn) ^ " res=" ^ BitStr(res)); */ + PTW_Success(append(ppn, va[PgOfs]), pte, pte_addr, level, is_global, ext_ptw) } } } @@ -173,7 +173,7 @@ function lookup_TLB48(asid, vaddr) = val add_to_TLB48 : (asid64, vaddr48, paddr64, SV48_PTE, paddr64, nat, bool) -> unit function add_to_TLB48(asid, vAddr, pAddr, pte, pteAddr, level, global) = { - let ent : TLB48_Entry = make_TLB_Entry(asid, global, vAddr, pAddr, pte.bits(), level, pteAddr, SV48_LEVEL_BITS); + let ent : TLB48_Entry = make_TLB_Entry(asid, global, vAddr, pAddr, pte.bits, level, pteAddr, SV48_LEVEL_BITS); tlb48 = Some(ent) } @@ -196,7 +196,7 @@ function translate48(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = match walk48(vAddr, ac, priv, mxr, do_sum, ptb, level, false, ext_ptw) { PTW_Failure(f, ext_ptw) => TR_Failure(f, ext_ptw), PTW_Success(pAddr, pte, pteAddr, level, global, ext_ptw) => { - match update_PTE_Bits(Mk_PTE_Bits(pte.BITS()), ac, pte.Ext()) { + match update_PTE_Bits(Mk_PTE_Bits(pte[BITS]), ac, pte[Ext]) { None() => { add_to_TLB48(asid, vAddr, pAddr, pte, pteAddr, level, global); TR_Address(pAddr, ext_ptw) @@ -207,9 +207,9 @@ function translate48(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = /* pte needs dirty/accessed update but that is not enabled */ TR_Failure(PTW_PTE_Update(), ext_ptw) } else { - var w_pte : SV48_PTE = update_BITS(pte, pbits.bits()); + var w_pte : SV48_PTE = update_BITS(pte, pbits.bits); w_pte = update_Ext(w_pte, ext); - match mem_write_value_priv(zero_extend(pteAddr), 8, w_pte.bits(), Supervisor, false, false, false) { + match mem_write_value_priv(zero_extend(pteAddr), 8, w_pte.bits, Supervisor, false, false, false) { MemValue(_) => { add_to_TLB48(asid, vAddr, pAddr, w_pte, pteAddr, level, global); TR_Address(pAddr, ext_ptw) diff --git a/model/rvfi_dii.sail b/model/rvfi_dii.sail index e1007bb03..121bcf873 100644 --- a/model/rvfi_dii.sail +++ b/model/rvfi_dii.sail @@ -93,18 +93,18 @@ function rvfi_set_instr_packet(p) = val rvfi_get_cmd : unit -> bits(8) -function rvfi_get_cmd () = rvfi_instruction.rvfi_cmd() +function rvfi_get_cmd () = rvfi_instruction[rvfi_cmd] val rvfi_get_insn : unit -> bits(32) -function rvfi_get_insn () = rvfi_instruction.rvfi_insn() +function rvfi_get_insn () = rvfi_instruction[rvfi_insn] val print_instr_packet : bits(64) -> unit function print_instr_packet(bs) = { let p = Mk_RVFI_DII_Instruction_Packet(bs); - print_bits("command ", p.rvfi_cmd()); - print_bits("instruction ", p.rvfi_insn()) + print_bits("command ", p[rvfi_cmd]); + print_bits("instruction ", p[rvfi_insn]) } bitfield RVFI_DII_Execution_Packet_V1 : bits(704) = { @@ -291,36 +291,36 @@ function rvfi_get_v2_support_packet () = { // backwards compatibility with old implementations that do not support // the new trace format. let rvfi_exec = update_rvfi_halt(rvfi_exec, 0x03); - return rvfi_exec.bits(); + return rvfi_exec.bits; } val rvfi_get_exec_packet_v1 : unit -> bits(704) function rvfi_get_exec_packet_v1 () = { let v1_packet = Mk_RVFI_DII_Execution_Packet_V1(zero_extend(0b0)); // Convert the v2 packet to a v1 packet - let v1_packet = update_rvfi_intr(v1_packet, rvfi_inst_data.rvfi_intr()); - let v1_packet = update_rvfi_halt(v1_packet, rvfi_inst_data.rvfi_halt()); - let v1_packet = update_rvfi_trap(v1_packet, rvfi_inst_data.rvfi_trap()); - let v1_packet = update_rvfi_insn(v1_packet, rvfi_inst_data.rvfi_insn()); - let v1_packet = update_rvfi_order(v1_packet, rvfi_inst_data.rvfi_order()); + let v1_packet = update_rvfi_intr(v1_packet, rvfi_inst_data[rvfi_intr]); + let v1_packet = update_rvfi_halt(v1_packet, rvfi_inst_data[rvfi_halt]); + let v1_packet = update_rvfi_trap(v1_packet, rvfi_inst_data[rvfi_trap]); + let v1_packet = update_rvfi_insn(v1_packet, rvfi_inst_data[rvfi_insn]); + let v1_packet = update_rvfi_order(v1_packet, rvfi_inst_data[rvfi_order]); - let v1_packet = update_rvfi_pc_wdata(v1_packet, rvfi_pc_data.rvfi_pc_wdata()); - let v1_packet = update_rvfi_pc_rdata(v1_packet, rvfi_pc_data.rvfi_pc_rdata()); + let v1_packet = update_rvfi_pc_wdata(v1_packet, rvfi_pc_data[rvfi_pc_wdata]); + let v1_packet = update_rvfi_pc_rdata(v1_packet, rvfi_pc_data[rvfi_pc_rdata]); - let v1_packet = update_rvfi_rd_addr(v1_packet, rvfi_int_data.rvfi_rd_addr()); + let v1_packet = update_rvfi_rd_addr(v1_packet, rvfi_int_data[rvfi_rd_addr]); let v1_packet = update_rvfi_rs2_addr(v1_packet, rvfi_int_data.rvfi_rs2_addr()); let v1_packet = update_rvfi_rs1_addr(v1_packet, rvfi_int_data.rvfi_rs1_addr()); - let v1_packet = update_rvfi_rd_wdata(v1_packet, rvfi_int_data.rvfi_rd_wdata()); + let v1_packet = update_rvfi_rd_wdata(v1_packet, rvfi_int_data[rvfi_rd_wdata]); let v1_packet = update_rvfi_rs2_data(v1_packet, rvfi_int_data.rvfi_rs2_rdata()); let v1_packet = update_rvfi_rs1_data(v1_packet, rvfi_int_data.rvfi_rs1_rdata()); - let v1_packet = update_rvfi_mem_wmask(v1_packet, truncate(rvfi_mem_data.rvfi_mem_wmask(), 8)); - let v1_packet = update_rvfi_mem_rmask(v1_packet, truncate(rvfi_mem_data.rvfi_mem_rmask(), 8)); - let v1_packet = update_rvfi_mem_wdata(v1_packet, truncate(rvfi_mem_data.rvfi_mem_wdata(), 64)); - let v1_packet = update_rvfi_mem_rdata(v1_packet, truncate(rvfi_mem_data.rvfi_mem_rdata(), 64)); - let v1_packet = update_rvfi_mem_addr(v1_packet, rvfi_mem_data.rvfi_mem_addr()); + let v1_packet = update_rvfi_mem_wmask(v1_packet, truncate(rvfi_mem_data[rvfi_mem_wmask], 8)); + let v1_packet = update_rvfi_mem_rmask(v1_packet, truncate(rvfi_mem_data[rvfi_mem_rmask], 8)); + let v1_packet = update_rvfi_mem_wdata(v1_packet, truncate(rvfi_mem_data[rvfi_mem_wdata], 64)); + let v1_packet = update_rvfi_mem_rdata(v1_packet, truncate(rvfi_mem_data[rvfi_mem_rdata], 64)); + let v1_packet = update_rvfi_mem_addr(v1_packet, rvfi_mem_data[rvfi_mem_addr]); - return v1_packet.bits(); + return v1_packet.bits; } val rvfi_get_v2_trace_size : unit -> bits(64) @@ -337,27 +337,27 @@ function rvfi_get_exec_packet_v2 () = { // TODO: find a way to return a variable-length bitvector let packet = Mk_RVFI_DII_Execution_PacketV2(zero_extend(0b0)); let packet = update_magic(packet, 0x32762d6563617274); // ASCII "trace-v2" (BE) - let packet = update_basic_data(packet, rvfi_inst_data.bits()); - let packet = update_pc_data(packet, rvfi_pc_data.bits()); + let packet = update_basic_data(packet, rvfi_inst_data.bits); + let packet = update_pc_data(packet, rvfi_pc_data.bits); let packet = update_integer_data_available(packet, bool_to_bits(rvfi_int_data_present)); let packet = update_memory_access_data_available(packet, bool_to_bits(rvfi_mem_data_present)); // To simplify the implementation (so that we can return a fixed-size vector) // we always return a max-size packet from this function, and the C emulator // ensures that only trace_size bits are sent over the socket. let packet = update_trace_size(packet, rvfi_get_v2_trace_size()); - return packet.bits(); + return packet.bits; } val rvfi_get_int_data : unit -> bits(320) function rvfi_get_int_data () = { assert(rvfi_int_data_present, "reading uninitialized data"); - return rvfi_int_data.bits(); + return rvfi_int_data.bits; } val rvfi_get_mem_data : unit -> bits(704) function rvfi_get_mem_data () = { assert(rvfi_mem_data_present, "reading uninitialized data"); - return rvfi_mem_data.bits(); + return rvfi_mem_data.bits; } val rvfi_encode_width_mask : forall 'n, 0 < 'n <= 32. atom('n) -> bits(32) @@ -368,22 +368,22 @@ function rvfi_encode_width_mask(width) = val print_rvfi_exec : unit -> unit function print_rvfi_exec () = { - print_bits("rvfi_intr : ", rvfi_inst_data.rvfi_intr()); - print_bits("rvfi_halt : ", rvfi_inst_data.rvfi_halt()); - print_bits("rvfi_trap : ", rvfi_inst_data.rvfi_trap()); - print_bits("rvfi_rd_addr : ", rvfi_int_data.rvfi_rd_addr()); + print_bits("rvfi_intr : ", rvfi_inst_data[rvfi_intr]); + print_bits("rvfi_halt : ", rvfi_inst_data[rvfi_halt]); + print_bits("rvfi_trap : ", rvfi_inst_data[rvfi_trap]); + print_bits("rvfi_rd_addr : ", rvfi_int_data[rvfi_rd_addr]); print_bits("rvfi_rs2_addr : ", rvfi_int_data.rvfi_rs2_addr()); print_bits("rvfi_rs1_addr : ", rvfi_int_data.rvfi_rs1_addr()); - print_bits("rvfi_mem_wmask: ", rvfi_mem_data.rvfi_mem_wmask()); - print_bits("rvfi_mem_rmask: ", rvfi_mem_data.rvfi_mem_rmask()); - print_bits("rvfi_mem_wdata: ", rvfi_mem_data.rvfi_mem_wdata()); - print_bits("rvfi_mem_rdata: ", rvfi_mem_data.rvfi_mem_rdata()); - print_bits("rvfi_mem_addr : ", rvfi_mem_data.rvfi_mem_addr()); - print_bits("rvfi_rd_wdata : ", rvfi_int_data.rvfi_rd_wdata()); + print_bits("rvfi_mem_wmask: ", rvfi_mem_data[rvfi_mem_wmask]); + print_bits("rvfi_mem_rmask: ", rvfi_mem_data[rvfi_mem_rmask]); + print_bits("rvfi_mem_wdata: ", rvfi_mem_data[rvfi_mem_wdata]); + print_bits("rvfi_mem_rdata: ", rvfi_mem_data[rvfi_mem_rdata]); + print_bits("rvfi_mem_addr : ", rvfi_mem_data[rvfi_mem_addr]); + print_bits("rvfi_rd_wdata : ", rvfi_int_data[rvfi_rd_wdata]); print_bits("rvfi_rs2_data : ", rvfi_int_data.rvfi_rs2_rdata()); print_bits("rvfi_rs1_data : ", rvfi_int_data.rvfi_rs1_rdata()); - print_bits("rvfi_insn : ", rvfi_inst_data.rvfi_insn()); - print_bits("rvfi_pc_wdata : ", rvfi_pc_data.rvfi_pc_wdata()); - print_bits("rvfi_pc_rdata : ", rvfi_pc_data.rvfi_pc_rdata()); - print_bits("rvfi_order : ", rvfi_inst_data.rvfi_order()); + print_bits("rvfi_insn : ", rvfi_inst_data[rvfi_insn]); + print_bits("rvfi_pc_wdata : ", rvfi_pc_data[rvfi_pc_wdata]); + print_bits("rvfi_pc_rdata : ", rvfi_pc_data[rvfi_pc_rdata]); + print_bits("rvfi_order : ", rvfi_inst_data[rvfi_order]); } diff --git a/ocaml_emulator/platform.ml b/ocaml_emulator/platform.ml index db9baad91..e03cb5dd0 100644 --- a/ocaml_emulator/platform.ml +++ b/ocaml_emulator/platform.ml @@ -10,9 +10,14 @@ let config_enable_writable_misa = ref true let config_enable_dirty_update = ref false let config_enable_misaligned_access = ref false let config_mtval_has_illegal_inst_bits = ref false -let config_enable_pmp = ref false let config_enable_writable_fiom = ref true let config_enable_vext = ref true +let config_pmp_count = ref Big_int.zero +let config_pmp_grain = ref Big_int.zero + +let set_config_pmp_count x = config_pmp_count := Big_int.of_int x +let set_config_pmp_grain x = config_pmp_grain := Big_int.of_int x + let config_enable_svnapot = ref false let config_enable_svpbmt = ref false @@ -86,9 +91,10 @@ let enable_vext () = !config_enable_vext let enable_dirty_update () = !config_enable_dirty_update let enable_misaligned_access () = !config_enable_misaligned_access let mtval_has_illegal_inst_bits () = !config_mtval_has_illegal_inst_bits -let enable_pmp () = !config_enable_pmp let enable_zfinx () = false let enable_writable_fiom () = !config_enable_writable_fiom +let pmp_count () = !config_pmp_count +let pmp_grain () = !config_pmp_grain let enable_svnapot () = !config_enable_svnapot let enable_svpbmt () = !config_enable_svpbmt diff --git a/ocaml_emulator/riscv_ocaml_sim.ml b/ocaml_emulator/riscv_ocaml_sim.ml index 37c93eb51..44d3b2c8b 100644 --- a/ocaml_emulator/riscv_ocaml_sim.ml +++ b/ocaml_emulator/riscv_ocaml_sim.ml @@ -41,9 +41,12 @@ let options = Arg.align ([("-dump-dts", ("-enable-misaligned-access", Arg.Set P.config_enable_misaligned_access, " enable misaligned accesses without M-mode traps"); - ("-enable-pmp", - Arg.Set P.config_enable_pmp, - " enable PMP support"); + ("-pmp-count", + Arg.Int P.set_config_pmp_count, + " number of supported PMPs (0, 16, 64)"); + ("-pmp-grain", + Arg.Int P.set_config_pmp_grain, + " exponent of granularity of PMP addresses (G in the spec)"); ("-enable-next", Arg.Set P.config_enable_next, " enable N extension"); diff --git a/sail-riscv.install b/sail-riscv.install index 5a8367388..7a539dfb5 100644 --- a/sail-riscv.install +++ b/sail-riscv.install @@ -1,2 +1,2 @@ bin: ["c_emulator/riscv_sim_RV64" "c_emulator/riscv_sim_RV32"] -share: [ "model/main.sail" {"model/main.sail"} "model/prelude.sail" {"model/prelude.sail"} "model/prelude_mapping.sail" {"model/prelude_mapping.sail"} "model/prelude_mem.sail" {"model/prelude_mem.sail"} "model/prelude_mem_metadata.sail" {"model/prelude_mem_metadata.sail"} "model/riscv_addr_checks.sail" {"model/riscv_addr_checks.sail"} "model/riscv_addr_checks_common.sail" {"model/riscv_addr_checks_common.sail"} "model/riscv_analysis.sail" {"model/riscv_analysis.sail"} "model/riscv_csr_ext.sail" {"model/riscv_csr_ext.sail"} "model/riscv_csr_map.sail" {"model/riscv_csr_map.sail"} "model/riscv_decode_ext.sail" {"model/riscv_decode_ext.sail"} "model/riscv_ext_regs.sail" {"model/riscv_ext_regs.sail"} "model/riscv_fdext_control.sail" {"model/riscv_fdext_control.sail"} "model/riscv_fdext_regs.sail" {"model/riscv_fdext_regs.sail"} "model/riscv_fetch.sail" {"model/riscv_fetch.sail"} "model/riscv_fetch_rvfi.sail" {"model/riscv_fetch_rvfi.sail"} "model/riscv_flen_D.sail" {"model/riscv_flen_D.sail"} "model/riscv_flen_F.sail" {"model/riscv_flen_F.sail"} "model/riscv_freg_type.sail" {"model/riscv_freg_type.sail"} "model/riscv_insts_aext.sail" {"model/riscv_insts_aext.sail"} "model/riscv_insts_base.sail" {"model/riscv_insts_base.sail"} "model/riscv_insts_begin.sail" {"model/riscv_insts_begin.sail"} "model/riscv_insts_cdext.sail" {"model/riscv_insts_cdext.sail"} "model/riscv_insts_cext.sail" {"model/riscv_insts_cext.sail"} "model/riscv_insts_cfext.sail" {"model/riscv_insts_cfext.sail"} "model/riscv_insts_dext.sail" {"model/riscv_insts_dext.sail"} "model/riscv_insts_end.sail" {"model/riscv_insts_end.sail"} "model/riscv_insts_fext.sail" {"model/riscv_insts_fext.sail"} "model/riscv_insts_hints.sail" {"model/riscv_insts_hints.sail"} "model/riscv_insts_mext.sail" {"model/riscv_insts_mext.sail"} "model/riscv_insts_next.sail" {"model/riscv_insts_next.sail"} "model/riscv_insts_rmem.sail" {"model/riscv_insts_rmem.sail"} "model/riscv_insts_zba.sail" {"model/riscv_insts_zba.sail"} "model/riscv_insts_zbb.sail" {"model/riscv_insts_zbb.sail"} "model/riscv_insts_zbc.sail" {"model/riscv_insts_zbc.sail"} "model/riscv_insts_zbkb.sail" {"model/riscv_insts_zbkb.sail"} "model/riscv_insts_zbkx.sail" {"model/riscv_insts_zbkx.sail"} "model/riscv_insts_zbs.sail" {"model/riscv_insts_zbs.sail"} "model/riscv_insts_zfh.sail" {"model/riscv_insts_zfh.sail"} "model/riscv_insts_zicsr.sail" {"model/riscv_insts_zicsr.sail"} "model/riscv_insts_zkn.sail" {"model/riscv_insts_zkn.sail"} "model/riscv_insts_zks.sail" {"model/riscv_insts_zks.sail"} "model/riscv_jalr_rmem.sail" {"model/riscv_jalr_rmem.sail"} "model/riscv_jalr_seq.sail" {"model/riscv_jalr_seq.sail"} "model/riscv_mem.sail" {"model/riscv_mem.sail"} "model/riscv_misa_ext.sail" {"model/riscv_misa_ext.sail"} "model/riscv_next_control.sail" {"model/riscv_next_control.sail"} "model/riscv_next_regs.sail" {"model/riscv_next_regs.sail"} "model/riscv_pc_access.sail" {"model/riscv_pc_access.sail"} "model/riscv_platform.sail" {"model/riscv_platform.sail"} "model/riscv_pmp_control.sail" {"model/riscv_pmp_control.sail"} "model/riscv_pmp_regs.sail" {"model/riscv_pmp_regs.sail"} "model/riscv_pte.sail" {"model/riscv_pte.sail"} "model/riscv_ptw.sail" {"model/riscv_ptw.sail"} "model/riscv_reg_type.sail" {"model/riscv_reg_type.sail"} "model/riscv_regs.sail" {"model/riscv_regs.sail"} "model/riscv_softfloat_interface.sail" {"model/riscv_softfloat_interface.sail"} "model/riscv_step.sail" {"model/riscv_step.sail"} "model/riscv_step_common.sail" {"model/riscv_step_common.sail"} "model/riscv_step_ext.sail" {"model/riscv_step_ext.sail"} "model/riscv_step_rvfi.sail" {"model/riscv_step_rvfi.sail"} "model/riscv_sync_exception.sail" {"model/riscv_sync_exception.sail"} "model/riscv_sys_control.sail" {"model/riscv_sys_control.sail"} "model/riscv_sys_exceptions.sail" {"model/riscv_sys_exceptions.sail"} "model/riscv_sys_regs.sail" {"model/riscv_sys_regs.sail"} "model/riscv_termination_common.sail" {"model/riscv_termination_common.sail"} "model/riscv_termination_rv32.sail" {"model/riscv_termination_rv32.sail"} "model/riscv_termination_rv64.sail" {"model/riscv_termination_rv64.sail"} "model/riscv_types.sail" {"model/riscv_types.sail"} "model/riscv_types_common.sail" {"model/riscv_types_common.sail"} "model/riscv_types_ext.sail" {"model/riscv_types_ext.sail"} "model/riscv_types_kext.sail" {"model/riscv_types_kext.sail"} "model/riscv_vmem_common.sail" {"model/riscv_vmem_common.sail"} "model/riscv_vmem_rv32.sail" {"model/riscv_vmem_rv32.sail"} "model/riscv_vmem_rv64.sail" {"model/riscv_vmem_rv64.sail"} "model/riscv_vmem_sv32.sail" {"model/riscv_vmem_sv32.sail"} "model/riscv_vmem_sv39.sail" {"model/riscv_vmem_sv39.sail"} "model/riscv_vmem_sv48.sail" {"model/riscv_vmem_sv48.sail"} "model/riscv_vmem_tlb.sail" {"model/riscv_vmem_tlb.sail"} "model/riscv_vmem_types.sail" {"model/riscv_vmem_types.sail"} "model/riscv_xlen32.sail" {"model/riscv_xlen32.sail"} "model/riscv_xlen64.sail" {"model/riscv_xlen64.sail"} "model/rvfi_dii.sail" {"model/rvfi_dii.sail"} "c_emulator/riscv_platform.c" {"c_emulator/riscv_platform.c"} "c_emulator/riscv_platform_impl.c" {"c_emulator/riscv_platform_impl.c"} "c_emulator/riscv_prelude.c" {"c_emulator/riscv_prelude.c"} "c_emulator/riscv_sim.c" {"c_emulator/riscv_sim.c"} "c_emulator/riscv_softfloat.c" {"c_emulator/riscv_softfloat.c"} "c_emulator/riscv_config.h" {"c_emulator/riscv_config.h"} "c_emulator/riscv_platform.h" {"c_emulator/riscv_platform.h"} "c_emulator/riscv_platform_impl.h" {"c_emulator/riscv_platform_impl.h"} "c_emulator/riscv_prelude.h" {"c_emulator/riscv_prelude.h"} "c_emulator/riscv_sail.h" {"c_emulator/riscv_sail.h"} "c_emulator/riscv_softfloat.h" {"c_emulator/riscv_softfloat.h"} "handwritten_support/mem_metadata.lem" {"handwritten_support/mem_metadata.lem"} "handwritten_support/riscv_extras.lem" {"handwritten_support/riscv_extras.lem"} "handwritten_support/riscv_extras_fdext.lem" {"handwritten_support/riscv_extras_fdext.lem"} "handwritten_support/riscv_extras_sequential.lem" {"handwritten_support/riscv_extras_sequential.lem"} "handwritten_support/hgen/ast.hgen" {"handwritten_support/hgen/ast.hgen"} "handwritten_support/hgen/fold.hgen" {"handwritten_support/hgen/fold.hgen"} "handwritten_support/hgen/herdtools_ast_to_shallow_ast.hgen" {"handwritten_support/hgen/herdtools_ast_to_shallow_ast.hgen"} "handwritten_support/hgen/herdtools_types_to_shallow_types.hgen" {"handwritten_support/hgen/herdtools_types_to_shallow_types.hgen"} "handwritten_support/hgen/lexer.hgen" {"handwritten_support/hgen/lexer.hgen"} "handwritten_support/hgen/lexer_regexps.hgen" {"handwritten_support/hgen/lexer_regexps.hgen"} "handwritten_support/hgen/map.hgen" {"handwritten_support/hgen/map.hgen"} "handwritten_support/hgen/parser.hgen" {"handwritten_support/hgen/parser.hgen"} "handwritten_support/hgen/pretty.hgen" {"handwritten_support/hgen/pretty.hgen"} "handwritten_support/hgen/pretty_xml.hgen" {"handwritten_support/hgen/pretty_xml.hgen"} "handwritten_support/hgen/sail_trans_out.hgen" {"handwritten_support/hgen/sail_trans_out.hgen"} "handwritten_support/hgen/shallow_ast_to_herdtools_ast.hgen" {"handwritten_support/hgen/shallow_ast_to_herdtools_ast.hgen"} "handwritten_support/hgen/shallow_types_to_herdtools_types.hgen" {"handwritten_support/hgen/shallow_types_to_herdtools_types.hgen"} "handwritten_support/hgen/token_types.hgen" {"handwritten_support/hgen/token_types.hgen"} "handwritten_support/hgen/tokens.hgen" {"handwritten_support/hgen/tokens.hgen"} "handwritten_support/hgen/trans_sail.hgen" {"handwritten_support/hgen/trans_sail.hgen"} "handwritten_support/hgen/types.hgen" {"handwritten_support/hgen/types.hgen"} "handwritten_support/hgen/types_sail_trans_out.hgen" {"handwritten_support/hgen/types_sail_trans_out.hgen"} "handwritten_support/hgen/types_trans_sail.hgen" {"handwritten_support/hgen/types_trans_sail.hgen"} "handwritten_support/0.11/mem_metadata.lem" {"handwritten_support/0.11/mem_metadata.lem"} "handwritten_support/0.11/riscv_extras.lem" {"handwritten_support/0.11/riscv_extras.lem"} "handwritten_support/0.11/riscv_extras_fdext.lem" {"handwritten_support/0.11/riscv_extras_fdext.lem"} "handwritten_support/0.11/riscv_extras_sequential.lem" {"handwritten_support/0.11/riscv_extras_sequential.lem"} "generated_definitions/for-rmem/riscv.lem" {"generated_definitions/for-rmem/riscv.lem"} "generated_definitions/for-rmem/riscv_types.lem" {"generated_definitions/for-rmem/riscv_types.lem"} "generated_definitions/for-rmem/riscv_toFromInterp2.ml" {"generated_definitions/for-rmem/riscv_toFromInterp2.ml"} "generated_definitions/for-rmem/riscv.defs" {"generated_definitions/for-rmem/riscv.defs"} ] +share: [ "model/main.sail" {"model/main.sail"} "model/prelude.sail" {"model/prelude.sail"} "model/prelude_mem.sail" {"model/prelude_mem.sail"} "model/prelude_mem_metadata.sail" {"model/prelude_mem_metadata.sail"} "model/riscv_addr_checks.sail" {"model/riscv_addr_checks.sail"} "model/riscv_addr_checks_common.sail" {"model/riscv_addr_checks_common.sail"} "model/riscv_analysis.sail" {"model/riscv_analysis.sail"} "model/riscv_csr_ext.sail" {"model/riscv_csr_ext.sail"} "model/riscv_csr_map.sail" {"model/riscv_csr_map.sail"} "model/riscv_decode_ext.sail" {"model/riscv_decode_ext.sail"} "model/riscv_ext_regs.sail" {"model/riscv_ext_regs.sail"} "model/riscv_fdext_control.sail" {"model/riscv_fdext_control.sail"} "model/riscv_fdext_regs.sail" {"model/riscv_fdext_regs.sail"} "model/riscv_fetch.sail" {"model/riscv_fetch.sail"} "model/riscv_fetch_rvfi.sail" {"model/riscv_fetch_rvfi.sail"} "model/riscv_flen_D.sail" {"model/riscv_flen_D.sail"} "model/riscv_flen_F.sail" {"model/riscv_flen_F.sail"} "model/riscv_freg_type.sail" {"model/riscv_freg_type.sail"} "model/riscv_insts_aext.sail" {"model/riscv_insts_aext.sail"} "model/riscv_insts_base.sail" {"model/riscv_insts_base.sail"} "model/riscv_insts_begin.sail" {"model/riscv_insts_begin.sail"} "model/riscv_insts_cdext.sail" {"model/riscv_insts_cdext.sail"} "model/riscv_insts_cext.sail" {"model/riscv_insts_cext.sail"} "model/riscv_insts_cfext.sail" {"model/riscv_insts_cfext.sail"} "model/riscv_insts_dext.sail" {"model/riscv_insts_dext.sail"} "model/riscv_insts_end.sail" {"model/riscv_insts_end.sail"} "model/riscv_insts_fext.sail" {"model/riscv_insts_fext.sail"} "model/riscv_insts_hints.sail" {"model/riscv_insts_hints.sail"} "model/riscv_insts_mext.sail" {"model/riscv_insts_mext.sail"} "model/riscv_insts_next.sail" {"model/riscv_insts_next.sail"} "model/riscv_insts_rmem.sail" {"model/riscv_insts_rmem.sail"} "model/riscv_insts_zba.sail" {"model/riscv_insts_zba.sail"} "model/riscv_insts_zbb.sail" {"model/riscv_insts_zbb.sail"} "model/riscv_insts_zbc.sail" {"model/riscv_insts_zbc.sail"} "model/riscv_insts_zbkb.sail" {"model/riscv_insts_zbkb.sail"} "model/riscv_insts_zbkx.sail" {"model/riscv_insts_zbkx.sail"} "model/riscv_insts_zbs.sail" {"model/riscv_insts_zbs.sail"} "model/riscv_insts_zfh.sail" {"model/riscv_insts_zfh.sail"} "model/riscv_insts_zicsr.sail" {"model/riscv_insts_zicsr.sail"} "model/riscv_insts_zkn.sail" {"model/riscv_insts_zkn.sail"} "model/riscv_insts_zks.sail" {"model/riscv_insts_zks.sail"} "model/riscv_jalr_rmem.sail" {"model/riscv_jalr_rmem.sail"} "model/riscv_jalr_seq.sail" {"model/riscv_jalr_seq.sail"} "model/riscv_mem.sail" {"model/riscv_mem.sail"} "model/riscv_misa_ext.sail" {"model/riscv_misa_ext.sail"} "model/riscv_next_control.sail" {"model/riscv_next_control.sail"} "model/riscv_next_regs.sail" {"model/riscv_next_regs.sail"} "model/riscv_pc_access.sail" {"model/riscv_pc_access.sail"} "model/riscv_platform.sail" {"model/riscv_platform.sail"} "model/riscv_pmp_control.sail" {"model/riscv_pmp_control.sail"} "model/riscv_pmp_regs.sail" {"model/riscv_pmp_regs.sail"} "model/riscv_pte.sail" {"model/riscv_pte.sail"} "model/riscv_ptw.sail" {"model/riscv_ptw.sail"} "model/riscv_reg_type.sail" {"model/riscv_reg_type.sail"} "model/riscv_regs.sail" {"model/riscv_regs.sail"} "model/riscv_softfloat_interface.sail" {"model/riscv_softfloat_interface.sail"} "model/riscv_step.sail" {"model/riscv_step.sail"} "model/riscv_step_common.sail" {"model/riscv_step_common.sail"} "model/riscv_step_ext.sail" {"model/riscv_step_ext.sail"} "model/riscv_step_rvfi.sail" {"model/riscv_step_rvfi.sail"} "model/riscv_sync_exception.sail" {"model/riscv_sync_exception.sail"} "model/riscv_sys_control.sail" {"model/riscv_sys_control.sail"} "model/riscv_sys_exceptions.sail" {"model/riscv_sys_exceptions.sail"} "model/riscv_sys_regs.sail" {"model/riscv_sys_regs.sail"} "model/riscv_termination_common.sail" {"model/riscv_termination_common.sail"} "model/riscv_termination_rv32.sail" {"model/riscv_termination_rv32.sail"} "model/riscv_termination_rv64.sail" {"model/riscv_termination_rv64.sail"} "model/riscv_types.sail" {"model/riscv_types.sail"} "model/riscv_types_common.sail" {"model/riscv_types_common.sail"} "model/riscv_types_ext.sail" {"model/riscv_types_ext.sail"} "model/riscv_types_kext.sail" {"model/riscv_types_kext.sail"} "model/riscv_vmem_common.sail" {"model/riscv_vmem_common.sail"} "model/riscv_vmem_rv32.sail" {"model/riscv_vmem_rv32.sail"} "model/riscv_vmem_rv64.sail" {"model/riscv_vmem_rv64.sail"} "model/riscv_vmem_sv32.sail" {"model/riscv_vmem_sv32.sail"} "model/riscv_vmem_sv39.sail" {"model/riscv_vmem_sv39.sail"} "model/riscv_vmem_sv48.sail" {"model/riscv_vmem_sv48.sail"} "model/riscv_vmem_tlb.sail" {"model/riscv_vmem_tlb.sail"} "model/riscv_vmem_types.sail" {"model/riscv_vmem_types.sail"} "model/riscv_xlen32.sail" {"model/riscv_xlen32.sail"} "model/riscv_xlen64.sail" {"model/riscv_xlen64.sail"} "model/rvfi_dii.sail" {"model/rvfi_dii.sail"} "c_emulator/riscv_platform.c" {"c_emulator/riscv_platform.c"} "c_emulator/riscv_platform_impl.c" {"c_emulator/riscv_platform_impl.c"} "c_emulator/riscv_prelude.c" {"c_emulator/riscv_prelude.c"} "c_emulator/riscv_sim.c" {"c_emulator/riscv_sim.c"} "c_emulator/riscv_softfloat.c" {"c_emulator/riscv_softfloat.c"} "c_emulator/riscv_config.h" {"c_emulator/riscv_config.h"} "c_emulator/riscv_platform.h" {"c_emulator/riscv_platform.h"} "c_emulator/riscv_platform_impl.h" {"c_emulator/riscv_platform_impl.h"} "c_emulator/riscv_prelude.h" {"c_emulator/riscv_prelude.h"} "c_emulator/riscv_sail.h" {"c_emulator/riscv_sail.h"} "c_emulator/riscv_softfloat.h" {"c_emulator/riscv_softfloat.h"} "handwritten_support/mem_metadata.lem" {"handwritten_support/mem_metadata.lem"} "handwritten_support/riscv_extras.lem" {"handwritten_support/riscv_extras.lem"} "handwritten_support/riscv_extras_fdext.lem" {"handwritten_support/riscv_extras_fdext.lem"} "handwritten_support/riscv_extras_sequential.lem" {"handwritten_support/riscv_extras_sequential.lem"} "handwritten_support/hgen/ast.hgen" {"handwritten_support/hgen/ast.hgen"} "handwritten_support/hgen/fold.hgen" {"handwritten_support/hgen/fold.hgen"} "handwritten_support/hgen/herdtools_ast_to_shallow_ast.hgen" {"handwritten_support/hgen/herdtools_ast_to_shallow_ast.hgen"} "handwritten_support/hgen/herdtools_types_to_shallow_types.hgen" {"handwritten_support/hgen/herdtools_types_to_shallow_types.hgen"} "handwritten_support/hgen/lexer.hgen" {"handwritten_support/hgen/lexer.hgen"} "handwritten_support/hgen/lexer_regexps.hgen" {"handwritten_support/hgen/lexer_regexps.hgen"} "handwritten_support/hgen/map.hgen" {"handwritten_support/hgen/map.hgen"} "handwritten_support/hgen/parser.hgen" {"handwritten_support/hgen/parser.hgen"} "handwritten_support/hgen/pretty.hgen" {"handwritten_support/hgen/pretty.hgen"} "handwritten_support/hgen/pretty_xml.hgen" {"handwritten_support/hgen/pretty_xml.hgen"} "handwritten_support/hgen/sail_trans_out.hgen" {"handwritten_support/hgen/sail_trans_out.hgen"} "handwritten_support/hgen/shallow_ast_to_herdtools_ast.hgen" {"handwritten_support/hgen/shallow_ast_to_herdtools_ast.hgen"} "handwritten_support/hgen/shallow_types_to_herdtools_types.hgen" {"handwritten_support/hgen/shallow_types_to_herdtools_types.hgen"} "handwritten_support/hgen/token_types.hgen" {"handwritten_support/hgen/token_types.hgen"} "handwritten_support/hgen/tokens.hgen" {"handwritten_support/hgen/tokens.hgen"} "handwritten_support/hgen/trans_sail.hgen" {"handwritten_support/hgen/trans_sail.hgen"} "handwritten_support/hgen/types.hgen" {"handwritten_support/hgen/types.hgen"} "handwritten_support/hgen/types_sail_trans_out.hgen" {"handwritten_support/hgen/types_sail_trans_out.hgen"} "handwritten_support/hgen/types_trans_sail.hgen" {"handwritten_support/hgen/types_trans_sail.hgen"} "handwritten_support/0.11/mem_metadata.lem" {"handwritten_support/0.11/mem_metadata.lem"} "handwritten_support/0.11/riscv_extras.lem" {"handwritten_support/0.11/riscv_extras.lem"} "handwritten_support/0.11/riscv_extras_fdext.lem" {"handwritten_support/0.11/riscv_extras_fdext.lem"} "handwritten_support/0.11/riscv_extras_sequential.lem" {"handwritten_support/0.11/riscv_extras_sequential.lem"} "generated_definitions/for-rmem/riscv.lem" {"generated_definitions/for-rmem/riscv.lem"} "generated_definitions/for-rmem/riscv_types.lem" {"generated_definitions/for-rmem/riscv_types.lem"} "generated_definitions/for-rmem/riscv_toFromInterp2.ml" {"generated_definitions/for-rmem/riscv_toFromInterp2.ml"} "generated_definitions/for-rmem/riscv.defs" {"generated_definitions/for-rmem/riscv.defs"} ]