diff options
| author | Robert Norton <rmn30@cam.ac.uk> | 2019-06-26 17:33:16 +0100 |
|---|---|---|
| committer | Robert Norton <rmn30@cam.ac.uk> | 2019-06-26 17:33:16 +0100 |
| commit | 57694dc5a53d84a0d9299b59c45676eacf121bc7 (patch) | |
| tree | 60aec2beba1e0e5f03e483e60afca4349bcb1d02 /model | |
| parent | c4260c12c978866d8701156695140cfaf7c6dc68 (diff) | |
| download | sail-riscv-57694dc5a53d84a0d9299b59c45676eacf121bc7.zip sail-riscv-57694dc5a53d84a0d9299b59c45676eacf121bc7.tar.gz sail-riscv-57694dc5a53d84a0d9299b59c45676eacf121bc7.tar.bz2 | |
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.
Diffstat (limited to 'model')
| -rw-r--r-- | model/prelude.sail | 12 | ||||
| -rw-r--r-- | model/riscv_step.sail | 8 |
2 files changed, 18 insertions, 2 deletions
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) } |