diff options
| -rw-r--r-- | riscv/main.sail | 17 | ||||
| -rw-r--r-- | riscv/prelude.sail | 1 | ||||
| -rw-r--r-- | src/sail_lib.ml | 3 |
3 files changed, 20 insertions, 1 deletions
diff --git a/riscv/main.sail b/riscv/main.sail index 8c93afdc..cc6bb90c 100644 --- a/riscv/main.sail +++ b/riscv/main.sail @@ -29,7 +29,22 @@ val elf_entry = "Elf_loader.elf_entry" : unit -> int val main : unit -> unit effect {barr, eamem, escape, exmem, rmem, rreg, wmv, wreg} +function dump_state () : unit -> unit = { + print("Dumping state"); + print_bits(" PC: ", PC); + let instr = __RISCV_read(PC, 4); + print_bits(" instr: ", instr) +} + function main () = { PC = __GetSlice_int(64, elf_entry(), 0); - fetch_and_execute() + try { + fetch_and_execute() + } catch { + Error_not_implemented(s) => print_string("Error: Not implemented: ", s), + Error_misaligned_access => print("Error: misaligned_access"), + Error_EBREAK => print("EBREAK"), + Error_internal_error => print("Error: internal error") + }; + dump_state () } diff --git a/riscv/prelude.sail b/riscv/prelude.sail index 6ddd56ab..f77994d6 100644 --- a/riscv/prelude.sail +++ b/riscv/prelude.sail @@ -326,6 +326,7 @@ val pow2 = "pow2" : forall 'n. atom('n) -> atom(2 ^ 'n) 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 union exception = { Error_not_implemented : string, diff --git a/src/sail_lib.ml b/src/sail_lib.ml index f0ea7fb4..7a8dc88c 100644 --- a/src/sail_lib.ml +++ b/src/sail_lib.ml @@ -469,6 +469,9 @@ let print_int (str, x) = let print_bits (str, xs) = print_endline (str ^ string_of_bits xs) +let print_string(str, msg) = + print_endline (str ^ msg) + let reg_deref r = !r let string_of_zbit = function |