Use riscv platform insns_per_tick to tick the clock.

5 files changed, 29 insertions, 14 deletions

diff --git a/riscv/platform.ml b/riscv/platform.ml
index 81d2c90a..10c79faf 100644
--- a/riscv/platform.ml
+++ b/riscv/platform.ml
@@ -80,6 +80,8 @@ let htif_tohost () =
 let clint_base () = bits_of_int64 P.clint_base
 let clint_size () = bits_of_int64 P.clint_size
 
+let insns_per_tick () = Big_int.of_int P.insns_per_tick
+
 (* terminal I/O *)
 let term_write char_bits =
   let big_char = Big_int.bitwise_and (uint char_bits) (Big_int.of_int 255) in
diff --git a/riscv/riscv_extras.lem b/riscv/riscv_extras.lem
index fc72ca2b..989ee1cb 100644
--- a/riscv/riscv_extras.lem
+++ b/riscv/riscv_extras.lem
@@ -68,6 +68,10 @@ val plat_clint_size : forall 'a. Size 'a => unit -> bitvector 'a
 let plat_clint_size () = wordFromInteger 0
 declare ocaml target_rep function plat_clint_size = `Platform.clint_size`
 
+val plat_insns_per_tick : unit -> integer
+let plat_insns_per_tick () = 1
+declare ocaml target_rep function plat_insns_per_tick = `Platform.insns_per_tick`
+
 val plat_htif_tohost : forall 'a. Size 'a => unit -> bitvector 'a
 let plat_htif_tohost () = wordFromInteger 0
 declare ocaml target_rep function plat_htif_tohost = `Platform.htif_tohost`
diff --git a/riscv/riscv_platform.sail b/riscv/riscv_platform.sail
index 4dc976ea..1e17b0f2 100644
--- a/riscv/riscv_platform.sail
+++ b/riscv/riscv_platform.sail
@@ -53,7 +53,7 @@ function within_htif_readable(addr : xlenbits, width : atom('n)) -> forall 'n. b
 
 /* CLINT (Core Local Interruptor), based on Spike. */
 
-val plat_insns_per_tick = {ocaml: "Platform.insns_per_tick"} : unit -> int
+val plat_insns_per_tick = {ocaml: "Platform.insns_per_tick", lem: "plat_insns_per_tick"} : unit -> int
 
 // assumes a single hart, since this typically is a vector of per-hart registers.
 register mtimecmp : xlenbits  // memory-mapped internal clint register.
@@ -112,6 +112,14 @@ function clint_store(addr, width, data) = {
   } else MemException(E_SAMO_Access_Fault)
 }
 
+val tick_clock : unit -> unit effect {rreg, wreg}
+function tick_clock() = {
+  mcycle = mcycle + 1;
+  mtime  = mtime  + 1;
+  if mtime >=_u mtimecmp
+  then mip->MTI() = true
+}
+
 /* Basic terminal character I/O. */
 
 val plat_term_write = {ocaml: "Platform.term_write", lem: "plat_term_write"} : bits(8) -> unit
diff --git a/riscv/riscv_step.sail b/riscv/riscv_step.sail
index 36f633ef..73343029 100644
--- a/riscv/riscv_step.sail
+++ b/riscv/riscv_step.sail
@@ -41,9 +41,10 @@ function fetch() -> FetchResult = {
   }
 }
 
-/* returns whether an instruction was executed */
-val step : int -> bool effect {barr, eamem, escape, exmem, rmem, rreg, wmv, wreg}
-function step(step_no) = {
+/* returns whether an instruction was retired */
+val step : unit -> bool effect {barr, eamem, escape, exmem, rmem, rreg, wmv, wreg}
+function step() = {
+  let step_no = unsigned(minstret);
   match curInterrupt(mip, mie, mideleg) {
     Some(intr, priv) => {
       print_bits("Handling interrupt: ", intr);
@@ -91,17 +92,14 @@ function step(step_no) = {
 
 val loop : int -> unit effect {barr, eamem, escape, exmem, rmem, rreg, wmv, wreg}
 function loop (tohost_addr) = {
-  let tohost = __GetSlice_int(64, tohost_addr, 0);
+  let insns_per_tick = plat_insns_per_tick();
   i : int = 0;
   while true do {
     tick_clock();
     minstret_written = false;     /* see note for minstret */
-    let retired = step(i);
+    let retired = step();
     PC = nextPC;
-    if retired then {
-      i = i + 1;
-      retire_instruction()
-    };
+    if retired then retire_instruction();
 
     /* check htif exit */
     if htif_done then {
@@ -109,6 +107,13 @@ function loop (tohost_addr) = {
       if exit_val == 0 then print("SUCCESS")
       else print_int("FAILURE: ", exit_val);
       exit(());
+    };
+
+    /* update time */
+    i = i + 1;
+    if i == insns_per_tick then {
+      tick_clock();
+      i = 0;
     }
   }
 }
diff --git a/riscv/riscv_sys.sail b/riscv/riscv_sys.sail
index 9373701c..c42ee806 100644
--- a/riscv/riscv_sys.sail
+++ b/riscv/riscv_sys.sail
@@ -869,10 +869,6 @@ function init_sys() -> unit = {
   minstret_written = false;
 }
 
-function tick_clock() -> unit = {
-  mcycle = mcycle + 1
-}
-
 /* memory access exceptions, defined here for use by the platform model. */
 
 union MemoryOpResult ('a : Type) = {