Use riscv platform insns_per_tick to tick the clock.

1 files changed, 4 insertions, 0 deletions

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`