diff options
Diffstat (limited to 'riscv/riscv_platform.sail')
| -rw-r--r-- | riscv/riscv_platform.sail | 10 |
1 files changed, 9 insertions, 1 deletions
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 |