From dd75592f98f991cfdda21f9d63e7c808369f0295 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Fri, 31 May 2019 16:33:35 +0100 Subject: Install sail and C sources in share directory of opam package. --- Makefile | 7 +++++++ sail-riscv.install | 3 ++- 2 files changed, 9 insertions(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 64b1471..c075d53 100644 --- a/Makefile +++ b/Makefile @@ -327,6 +327,13 @@ generated_definitions/for-rmem/riscv.defs: $(SAIL_RMEM_SRCS) #LOC_FILES:=$(SAIL_SRCS) main.sail #include $(SAIL_DIR)/etc/loc.mk +FORCE: + +SHARE_FILES:=$(wildcard model/*.sail) $(wildcard c_emulator/*.c) $(wildcard c_emulator/*.h) +sail-riscv.install: FORCE + echo 'bin: ["c_emulator/riscv_sim_RV64" "c_emulator/riscv_sim_RV32"]' > sail-riscv.install + echo 'share: [ $(foreach f,$(SHARE_FILES),"$f" {"$f"}) ]' >> sail-riscv.install + opam-build: $(MAKE) ARCH=64 c_emulator/riscv_sim_RV64 $(MAKE) ARCH=32 c_emulator/riscv_sim_RV32 diff --git a/sail-riscv.install b/sail-riscv.install index 63d985a..ce50f55 100644 --- a/sail-riscv.install +++ b/sail-riscv.install @@ -1 +1,2 @@ -bin: ["c_emulator/riscv_sim_RV32" "c_emulator/riscv_sim_RV64"] +bin: ["c_emulator/riscv_sim_RV64" "c_emulator/riscv_sim_RV32"] +share: [ "model/riscv_insts_mext.sail" {"model/riscv_insts_mext.sail"} "model/riscv_insts_cext.sail" {"model/riscv_insts_cext.sail"} "model/riscv_csr_map.sail" {"model/riscv_csr_map.sail"} "model/riscv_addr_checks.sail" {"model/riscv_addr_checks.sail"} "model/riscv_sys_exceptions.sail" {"model/riscv_sys_exceptions.sail"} "model/riscv_vmem_sv32.sail" {"model/riscv_vmem_sv32.sail"} "model/riscv_types.sail" {"model/riscv_types.sail"} "model/riscv_addr_checks_common.sail" {"model/riscv_addr_checks_common.sail"} "model/riscv_step.sail" {"model/riscv_step.sail"} "model/riscv_step_rvfi.sail" {"model/riscv_step_rvfi.sail"} "model/riscv_step_common.sail" {"model/riscv_step_common.sail"} "model/riscv_platform.sail" {"model/riscv_platform.sail"} "model/riscv_insts_next.sail" {"model/riscv_insts_next.sail"} "model/riscv_sys_control.sail" {"model/riscv_sys_control.sail"} "model/riscv_insts_begin.sail" {"model/riscv_insts_begin.sail"} "model/riscv_vmem_sv48.sail" {"model/riscv_vmem_sv48.sail"} "model/riscv_csr_ext.sail" {"model/riscv_csr_ext.sail"} "model/riscv_regs.sail" {"model/riscv_regs.sail"} "model/riscv_fetch.sail" {"model/riscv_fetch.sail"} "model/riscv_step_ext.sail" {"model/riscv_step_ext.sail"} "model/riscv_fetch_rvfi.sail" {"model/riscv_fetch_rvfi.sail"} "model/riscv_termination_rv32.sail" {"model/riscv_termination_rv32.sail"} "model/riscv_jalr_rmem.sail" {"model/riscv_jalr_rmem.sail"} "model/riscv_vmem_common.sail" {"model/riscv_vmem_common.sail"} "model/riscv_decode_ext.sail" {"model/riscv_decode_ext.sail"} "model/riscv_next_regs.sail" {"model/riscv_next_regs.sail"} "model/riscv_xlen64.sail" {"model/riscv_xlen64.sail"} "model/riscv_insts_zicsr.sail" {"model/riscv_insts_zicsr.sail"} "model/riscv_pc_access.sail" {"model/riscv_pc_access.sail"} "model/riscv_insts_rmem.sail" {"model/riscv_insts_rmem.sail"} "model/prelude_mapping.sail" {"model/prelude_mapping.sail"} "model/riscv_vmem_rv32.sail" {"model/riscv_vmem_rv32.sail"} "model/riscv_insts_end.sail" {"model/riscv_insts_end.sail"} "model/riscv_ext_regs.sail" {"model/riscv_ext_regs.sail"} "model/rvfi_dii.sail" {"model/rvfi_dii.sail"} "model/prelude_mem.sail" {"model/prelude_mem.sail"} "model/riscv_duopod.sail" {"model/riscv_duopod.sail"} "model/riscv_sync_exception.sail" {"model/riscv_sync_exception.sail"} "model/riscv_vmem_sv39.sail" {"model/riscv_vmem_sv39.sail"} "model/riscv_next_control.sail" {"model/riscv_next_control.sail"} "model/riscv_vmem_rv64.sail" {"model/riscv_vmem_rv64.sail"} "model/riscv_analysis.sail" {"model/riscv_analysis.sail"} "model/main.sail" {"model/main.sail"} "model/riscv_vmem_tlb.sail" {"model/riscv_vmem_tlb.sail"} "model/riscv_sys_regs.sail" {"model/riscv_sys_regs.sail"} "model/riscv_termination_rv64.sail" {"model/riscv_termination_rv64.sail"} "model/prelude_mem_metadata.sail" {"model/prelude_mem_metadata.sail"} "model/prelude.sail" {"model/prelude.sail"} "model/riscv_xlen32.sail" {"model/riscv_xlen32.sail"} "model/riscv_termination_common.sail" {"model/riscv_termination_common.sail"} "model/riscv_insts_base.sail" {"model/riscv_insts_base.sail"} "model/riscv_jalr_seq.sail" {"model/riscv_jalr_seq.sail"} "model/riscv_reg_type.sail" {"model/riscv_reg_type.sail"} "model/riscv_mem.sail" {"model/riscv_mem.sail"} "model/riscv_insts_aext.sail" {"model/riscv_insts_aext.sail"} "c_emulator/riscv_platform.c" {"c_emulator/riscv_platform.c"} "c_emulator/riscv_sim.c" {"c_emulator/riscv_sim.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_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_platform.h" {"c_emulator/riscv_platform.h"} "c_emulator/riscv_config.h" {"c_emulator/riscv_config.h"} ] -- cgit v1.1 From 79508e4c6d5d7eaf865897d77dd69f9169c37db4 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Mon, 3 Jun 2019 11:53:29 +0100 Subject: Add a suppress_warnings directive in prelude_mapping.sail. Would be nice to fix the warnings properly but I don't understand mappings will enough to know how. --- model/prelude_mapping.sail | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/model/prelude_mapping.sail b/model/prelude_mapping.sail index e40edbf..070c4cb 100644 --- a/model/prelude_mapping.sail +++ b/model/prelude_mapping.sail @@ -1,5 +1,11 @@ /* 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 -- cgit v1.1 From 69b805540e868a7d097a28d6a7e84bcc30d628bc Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Mon, 3 Jun 2019 13:03:13 +0100 Subject: Bump opam version for release with installed model code. --- opam | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/opam b/opam index e3b2f91..fb65f9a 100644 --- a/opam +++ b/opam @@ -1,6 +1,6 @@ opam-version: "1.2" name: "sail-riscv" -version: "0.2" +version: "0.3" maintainer: "Sail Devs " authors: [ "Alasdair Armstrong" -- cgit v1.1 From 36f5da6a169afaba86d2c7191df477ae1837d5d1 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Fri, 14 Jun 2019 16:40:49 +0100 Subject: Use sail's built-in ones functions for compatibility with smt backend. --- model/prelude.sail | 14 ++++---------- 1 file changed, 4 insertions(+), 10 deletions(-) diff --git a/model/prelude.sail b/model/prelude.sail index 31d5668..51ed984 100644 --- a/model/prelude.sail +++ b/model/prelude.sail @@ -111,13 +111,10 @@ val zeros_implicit : forall 'n, 'n >= 0 . unit -> bits('n) function zeros_implicit () = sail_zeros('n) overload zeros = {zeros_implicit, sail_zeros} -val ones_n : forall 'n, 'n >= 0 . int('n) -> bits('n) -function ones_n n = replicate_bits (0b1, n) - val ones_implicit : forall 'n, 'n >= 0 . unit -> bits('n) -function ones_implicit () = ones_n ('n) +function ones_implicit () = sail_ones ('n) -overload ones = {ones_implicit, ones_n} +overload ones = {ones_implicit, sail_ones} $else val EXTS : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m) @@ -130,13 +127,10 @@ val zeros_implicit : forall 'n, 'n >= 0 . implicit('n) -> bits('n) function zeros_implicit (n) = sail_zeros(n) overload zeros = {zeros_implicit, sail_zeros} -val ones_n : forall 'n, 'n >= 0 . int('n) -> bits('n) -function ones_n n = replicate_bits (0b1, n) - val ones_implicit : forall 'n, 'n >= 0 . implicit('n) -> bits('n) -function ones_implicit (n) = ones_n (n) +function ones_implicit (n) = sail_ones (n) -overload ones = {ones_implicit, ones_n} +overload ones = {ones_implicit, sail_ones} $endif -- cgit v1.1 From c4260c12c978866d8701156695140cfaf7c6dc68 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Thu, 20 Jun 2019 13:21:04 +0100 Subject: Add interpreter builtin for min_nat. Should min/max be in standard library? --- model/prelude.sail | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/model/prelude.sail b/model/prelude.sail index 51ed984..54f7d03 100644 --- a/model/prelude.sail +++ b/model/prelude.sail @@ -79,7 +79,7 @@ val rem_round_zero = {ocaml: "rem_round_zero", interpreter: "rem_round_zero", le /* The following should get us euclidean modulus, and is compatible with pre and post 0.9 versions of sail */ overload operator % = {emod_int, mod} -val min_nat = {ocaml: "min_int", lem: "min", coq: "min_nat", c: "min_int"} : (nat, nat) -> nat +val min_nat = {ocaml: "min_int", interpreter: "min_int", lem: "min", coq: "min_nat", c: "min_int"} : (nat, nat) -> nat val min_int = {ocaml: "min_int", interpreter: "min_int", lem: "min", coq: "Z.min", c: "min_int"} : (int, int) -> int -- cgit v1.1 From 57694dc5a53d84a0d9299b59c45676eacf121bc7 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Wed, 26 Jun 2019 17:33:16 +0100 Subject: Add command line option in c_emulator for disabling tracing. Add builtins for getting values of config_print_xxx variables to speed up emulation when not tracing. --- c_emulator/riscv_prelude.c | 20 ++++++++++++++++++++ c_emulator/riscv_prelude.h | 5 +++++ c_emulator/riscv_sim.c | 40 +++++++++++++++++++++++++++++++++++----- model/prelude.sail | 12 ++++++++++++ model/riscv_step.sail | 8 ++++++-- ocaml_emulator/platform.ml | 5 +++++ 6 files changed, 83 insertions(+), 7 deletions(-) diff --git a/c_emulator/riscv_prelude.c b/c_emulator/riscv_prelude.c index 1621913..92f8415 100644 --- a/c_emulator/riscv_prelude.c +++ b/c_emulator/riscv_prelude.c @@ -30,3 +30,23 @@ unit print_platform(sail_string s) if (config_print_platform) printf("%s\n", s); return UNIT; } + +bool get_config_print_instr(unit u) +{ + return (config_print_instr) ? true : false; +} + +bool get_config_print_reg(unit u) +{ + return (config_print_reg) ? true : false; +} + +bool get_config_print_mem(unit u) +{ + return (config_print_mem_access) ? true : false; +} + +bool get_config_print_platform(unit u) +{ + return (config_print_platform) ? true : false; +} diff --git a/c_emulator/riscv_prelude.h b/c_emulator/riscv_prelude.h index a296c7e..da292fe 100644 --- a/c_emulator/riscv_prelude.h +++ b/c_emulator/riscv_prelude.h @@ -8,3 +8,8 @@ unit print_instr(sail_string s); unit print_reg(sail_string s); unit print_mem_access(sail_string s); unit print_platform(sail_string s); + +bool get_config_print_instr(unit u); +bool get_config_print_reg(unit u); +bool get_config_print_mem(unit u); +bool get_config_print_platform(unit u); diff --git a/c_emulator/riscv_sim.c b/c_emulator/riscv_sim.c index 864e2b7..c9cf011 100644 --- a/c_emulator/riscv_sim.c +++ b/c_emulator/riscv_sim.c @@ -69,6 +69,26 @@ bool config_print_reg = true; bool config_print_mem_access = true; bool config_print_platform = true; +void set_config_print(char *var, bool val) { + if (strcmp("instr", optarg) == 0) { + config_print_instr = val; + } else if (strcmp("reg", optarg) == 0) { + config_print_reg = val; + } else if (strcmp("mem", optarg) == 0) { + config_print_mem_access = val; + } else if (strcmp("platform", optarg) == 0) { + config_print_platform = val; + } else if (strcmp("all", optarg) == 0) { + config_print_instr = val; + config_print_mem_access = val; + config_print_reg = val; + config_print_platform = val; + } else { + fprintf(stderr, "Unknown trace category: %s (should be instr|reg|mem|platform|all)\n", var); + exit(1); + } +} + struct timeval init_start, init_end, run_end; int total_insns = 0; @@ -88,6 +108,8 @@ static struct option options[] = { {"rvfi-dii", required_argument, 0, 'r'}, #endif {"help", no_argument, 0, 'h'}, + {"trace", required_argument, 0, 'v'}, + {"no-trace", required_argument, 0, 'V'}, {0, 0, 0, 0} }; @@ -171,7 +193,7 @@ char *process_args(int argc, char **argv) int c, idx = 1; uint64_t ram_size = 0; while(true) { - c = getopt_long(argc, argv, "admCIispz:b:t:v:hr:T:", options, &idx); + c = getopt_long(argc, argv, "admCIispz:b:t:v:hr:T:V:v:", options, &idx); if (c == -1) break; switch (c) { case 'a': @@ -236,6 +258,12 @@ char *process_args(int argc, char **argv) fprintf(stderr, "using %d as RVFI port.\n", rvfi_dii_port); break; #endif + case 'V': + set_config_print(optarg, false); + break; + case 'v': + set_config_print(optarg, true); + break; } } if (do_dump_dts) dump_dts(); @@ -574,10 +602,12 @@ int compare_states(struct tv_spike_t *s) void flush_logs(void) { - fprintf(stderr, "\n"); - fflush(stderr); - fprintf(stdout, "\n"); - fflush(stdout); + if(config_print_instr) { + fprintf(stderr, "\n"); + fflush(stderr); + fprintf(stdout, "\n"); + fflush(stdout); + } } #ifdef RVFI_DII diff --git a/model/prelude.sail b/model/prelude.sail index 54f7d03..9f8ad37 100644 --- a/model/prelude.sail +++ b/model/prelude.sail @@ -101,6 +101,18 @@ val print_reg = {ocaml: "Platform.print_reg", interpreter: "print_endline", val print_mem = {ocaml: "Platform.print_mem_access", interpreter: "print_endline", c: "print_mem_access", lem: "print_dbg", _: "print_endline"} : string -> unit val print_platform = {ocaml: "Platform.print_platform", interpreter: "print_endline", c: "print_platform", lem: "print_dbg", _: "print_endline"} : string -> unit +val get_config_print_instr = {ocaml: "Platform.get_config_print_instr", c:"get_config_print_instr"} : unit -> bool +function get_config_print_instr () -> bool = false + +val get_config_print_reg = {ocaml: "Platform.get_config_print_reg", c:"get_config_print_reg"} : unit -> bool +function get_config_print_reg () -> bool = false + +val get_config_print_mem = {ocaml: "Platform.get_config_print_mem", c:"get_config_print_mem"} : unit -> bool +function get_config_print_mem () -> bool = false + +val get_config_print_platform = {ocaml: "Platform.get_config_print_platform", c:"get_config_print_platform"} : unit -> bool +function get_config_print_platform () -> bool = false + $ifndef FEATURE_IMPLICITS val EXTS : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m) val EXTZ : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m) diff --git a/model/riscv_step.sail b/model/riscv_step.sail index 4b5c1c5..12c8522 100644 --- a/model/riscv_step.sail +++ b/model/riscv_step.sail @@ -31,7 +31,9 @@ function step(step_no) = { /* non-error cases: */ F_RVC(h) => { let ast = decodeCompressed(h); - print_instr("[" ^ string_of_int(step_no) ^ "] [" ^ cur_privilege ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(h) ^ ") " ^ ast); + if get_config_print_instr() then { + print_instr("[" ^ string_of_int(step_no) ^ "] [" ^ cur_privilege ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(h) ^ ") " ^ ast); + }; /* check for RVC once here instead of every RVC execute clause. */ if haveRVC() then { nextPC = PC + 2; @@ -43,7 +45,9 @@ function step(step_no) = { }, F_Base(w) => { let ast = decode(w); - print_instr("[" ^ string_of_int(step_no) ^ "] [" ^ cur_privilege ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(w) ^ ") " ^ ast); + if get_config_print_instr() then { + print_instr("[" ^ string_of_int(step_no) ^ "] [" ^ cur_privilege ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(w) ^ ") " ^ ast); + }; nextPC = PC + 4; (execute(ext_post_decode_hook(ast)), true) } diff --git a/ocaml_emulator/platform.ml b/ocaml_emulator/platform.ml index 11abaf1..a5c01ba 100644 --- a/ocaml_emulator/platform.ml +++ b/ocaml_emulator/platform.ml @@ -39,6 +39,11 @@ let print_platform s = then print_endline s else () +let get_config_print_instr () = !config_print_instr +let get_config_print_reg () = !config_print_reg +let get_config_print_mem () = !config_print_mem_access +let get_config_print_platform () = !config_print_platform + (* Mapping to Sail externs *) let cur_arch_bitwidth () = match !platform_arch with -- cgit v1.1