Start platform execution at the reset-vector in the rom.

2 files changed, 14 insertions, 18 deletions

diff --git a/riscv/platform_impl.ml b/riscv/platform_impl.ml
index 342eab35..a1a1f699 100644
--- a/riscv/platform_impl.ml
+++ b/riscv/platform_impl.ml
@@ -27,7 +27,7 @@ let uint64_to_bytes u = let open Int64 in
 let reset_vec_size = 8l;;
 
 let reset_vec_int start_pc = [
-  0x267l;                                                 (* auipc  t0, 0x0      *)
+  0x297l;                                                 (* auipc  t0, 0x0      *)
   (let open Int32 in
    add 0x28593l (shift_left (mul reset_vec_size 4l) 20)); (* addi   a1, t0, ofs(dtb) *)
   0xf1402573l;                                            (* csrr   a0, mhartid  *)
diff --git a/riscv/platform_main.ml b/riscv/platform_main.ml
index 73497aa5..b4a468f9 100644
--- a/riscv/platform_main.ml
+++ b/riscv/platform_main.ml
@@ -50,7 +50,7 @@
 
 open Elf_loader
 open Sail_lib
-open Riscv;;
+open Riscv
 
 (* OCaml driver for generated RISC-V model. *)
 
@@ -61,8 +61,7 @@ let options = Arg.align []
 let usage_msg = "RISC-V platform options:"
 
 let elf_arg =
-  Arg.parse options (fun s ->
-                     opt_file_arguments := !opt_file_arguments @ [s])
+  Arg.parse options (fun s -> opt_file_arguments := !opt_file_arguments @ [s])
             usage_msg;
   ( match !opt_file_arguments with
       | f :: _ -> print_endline ("Loading ELF file " ^ f); f
@@ -72,20 +71,17 @@ let elf_arg =
 let () =
   Random.self_init ();
 
-  zPC := Platform.init elf_arg;
+  let pc = Platform.init elf_arg in
 
   sail_call
     (fun r ->
-     begin
-       zPC := (z__GetSlice_int ((Big_int.of_string "64"), (Elf_loader.elf_entry ()), (Big_int.of_string "0")));
-       begin
-         try ( zinit_sys ();
-               zloop (Elf_loader.elf_tohost ())
-             )
-         with
-           | ZError_not_implemented (zs) ->
-                 print_string ("Error: Not implemented: ", zs)
-           | ZError_internal_error (_) ->
-                 prerr_endline "Error: internal error"
-       end
-     end)
+      try ( zinit_sys ();
+            zPC := pc;
+            zloop (Elf_loader.elf_tohost ())
+          )
+      with
+        | ZError_not_implemented (zs) ->
+              print_string ("Error: Not implemented: ", zs)
+        | ZError_internal_error (_) ->
+              prerr_endline "Error: internal error"
+    )