diff options
| author | Prashanth Mundkur | 2018-11-28 15:56:08 -0800 |
|---|---|---|
| committer | Prashanth Mundkur | 2018-11-29 09:52:36 -0800 |
| commit | 35eff0805dffe8d006d390bdaebac1b8d4b0a61d (patch) | |
| tree | 500ed7eec04c75b885ca2cccafd1c7484bbb298f /riscv/prelude.sail | |
| parent | d4ace417655622268e5af471d8d13dd2422054f7 (diff) | |
RISC-V: factor the execution trace.
This is now split into instructions, regs, memory and platform, each
controlled individually. Currently all are enabled and not connected to
any command-line options, so a recompile is needed for trace tuning.
Diffstat (limited to 'riscv/prelude.sail')
| -rw-r--r-- | riscv/prelude.sail | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/riscv/prelude.sail b/riscv/prelude.sail index 24913719..a2117bec 100644 --- a/riscv/prelude.sail +++ b/riscv/prelude.sail @@ -845,8 +845,6 @@ function cast_unit_vec b = match b { bitone => 0b1 } -val print = "print_endline" : string -> unit - val putchar = "putchar" : forall ('a : Type). 'a -> unit val concat_str = {c: "concat_str", ocaml: "concat_str", lem: "stringAppend", coq: "String.append"} : (string, string) -> string @@ -1057,10 +1055,16 @@ val slice = "slice" : forall ('n : Int) ('m : Int), 'm >= 0 & 'n >= 0. val pow2 = "pow2" : forall 'n. atom('n) -> atom(2 ^ 'n) +val print = "print_endline" : string -> unit val print_int = "print_int" : (string, int) -> unit val print_bits = "print_bits" : forall 'n. (string, bits('n)) -> unit val print_string = "print_string" : (string, string) -> unit +val print_instr = {ocaml: "Platform.print_instr", c: "print_instr", _: "print_endline"} : string -> unit +val print_reg = {ocaml: "Platform.print_reg", c: "print_reg", _: "print_endline"} : string -> unit +val print_mem = {ocaml: "Platform.print_mem_access", c: "print_mem_access", _: "print_endline"} : string -> unit +val print_platform = {ocaml: "Platform.print_platform", c: "print_platform", _: "print_endline"} : string -> unit + val "sign_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m) val "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m) |