diff options
| -rw-r--r-- | riscv/main.sail | 35 | ||||
| -rw-r--r-- | riscv/prelude.sail | 2 |
2 files changed, 18 insertions, 19 deletions
diff --git a/riscv/main.sail b/riscv/main.sail index 994324bd..8c93afdc 100644 --- a/riscv/main.sail +++ b/riscv/main.sail @@ -1,29 +1,26 @@ val fetch_and_execute : unit -> unit effect {barr, eamem, escape, exmem, rmem, rreg, wmv, wreg} -function break () : unit -> unit = () - val elf_tohost = "Elf_loader.elf_tohost" : unit -> int function fetch_and_execute () = let tohost = __GetSlice_int(64, elf_tohost(), 0) in while true do { - print_bits("PC: ", PC); - let instr = __RISCV_read(PC, 4); - nextPC = PC + 4; - let instr_ast = decode(instr); - break (); - match instr_ast { - Some(ast) => execute(ast), - None => {print("Decode failed"); exit (())} - }; - let tohost_val = __RISCV_read(tohost, 4); - if unsigned(tohost_val) != 0 then { - let exit_val = unsigned(tohost_val >> 0b1) in - if exit_val == 0 then - print("SUCCESS") - else - print_int("FAILURE: ", exit_val); - exit (()); + print_bits("PC: ", PC); + let instr = __RISCV_read(PC, 4); + nextPC = PC + 4; + let instr_ast = decode(instr); + match instr_ast { + Some(ast) => execute(ast), + None => {print("Decode failed"); exit (())} + }; + let tohost_val = __RISCV_read(tohost, 4); + if unsigned(tohost_val) != 0 then { + let exit_val = unsigned(tohost_val >> 0b1) in + if exit_val == 0 then + print("SUCCESS") + else + print_int("FAILURE: ", exit_val); + exit (()); }; PC = nextPC } diff --git a/riscv/prelude.sail b/riscv/prelude.sail index 427da759..5d56858c 100644 --- a/riscv/prelude.sail +++ b/riscv/prelude.sail @@ -373,3 +373,5 @@ val operator << = "shift_bits_left" : forall 'n 'm. (bits('n), bits('m)) -> bits val vector64 : int -> bits(64) function vector64 n = __raw_GetSlice_int(64, n, 0) + +function break () : unit -> unit = () |