diff options
| -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 = |