diff options
| author | Robert Norton | 2018-02-05 16:19:54 +0000 |
|---|---|---|
| committer | Robert Norton | 2018-02-05 16:19:54 +0000 |
| commit | 22b723ce7266a3e1333788f9d50b0b3dc9bb9893 (patch) | |
| tree | 1fdaec517a3993f1747f626cffbb014d503d8a3a /riscv | |
| parent | 0fc31bb06b7676d29758a36ab4f120b10f5c6cd1 (diff) | |
riscv: slightly prettier register trace output
Diffstat (limited to 'riscv')
| -rw-r--r-- | riscv/prelude.sail | 2 | ||||
| -rw-r--r-- | riscv/riscv_types.sail | 3 |
2 files changed, 3 insertions, 2 deletions
diff --git a/riscv/prelude.sail b/riscv/prelude.sail index ad74434c..a0d3d3a1 100644 --- a/riscv/prelude.sail +++ b/riscv/prelude.sail @@ -151,6 +151,8 @@ val putchar = "putchar" : forall ('a : Type). 'a -> unit val concat_str = {ocaml: "concat_str", lem: "stringAppend"} : (string, string) -> string +val string_of_int = "string_of_int" : int -> string + val DecStr : int -> string val HexStr : int -> string diff --git a/riscv/riscv_types.sail b/riscv/riscv_types.sail index 78116723..477b4902 100644 --- a/riscv/riscv_types.sail +++ b/riscv/riscv_types.sail @@ -84,8 +84,7 @@ val wGPR : forall 'n, 0 <= 'n < 32. (regno('n), regval) -> unit effect {wreg} function wGPR (r, v) = if (r != 0) then { (*GPRs[r - 1]) = v; - print_int("GPR ", r); - print_bits("<- ", v); + print_string("x", concat_str(string_of_int(r), concat_str(" <- ", BitStr(v)))); } function check_alignment (addr : bits(64), width : atom('n)) -> forall 'n. unit = |