diff --git a/sw/device/examples/hello_world.c b/sw/device/examples/hello_world.c
index 9ca5ce04..06eed4df 100644
--- a/sw/device/examples/hello_world.c
+++ b/sw/device/examples/hello_world.c
@@ -22,14 +22,13 @@ int main(void)
     uart_init(uart);
     timer_init(timer);
 
-    timer_set_prescale_step(timer, (SYSCLK_FREQ / 1000000) - 1, 1); // 1 tick/us
     timer_enable(timer);
 
     uprintf(uart, "Hello CHERI Mocha!\n");
 
     // Print every 100us
     for (int i = 0; i < 4; ++i) {
-        timer_busy_sleep(timer, 100);
+        timer_busy_sleep_us(timer, 100u);
 
         uprintf(uart, "timer 100us\n");
         gpio_write_pin(gpio, i, 1); // turn on LEDs in sequence
diff --git a/sw/device/examples/i2c.c b/sw/device/examples/i2c.c
index 9d284c9e..65b5c0a0 100644
--- a/sw/device/examples/i2c.c
+++ b/sw/device/examples/i2c.c
@@ -18,14 +18,12 @@ int main(void)
     i2c_init(i2c);
     uart_init(uart);
     timer_init(timer);
-
-    timer_set_prescale_step(timer, (SYSCLK_FREQ / 1000000) - 1, 1); // 1 tick/us
     timer_enable(timer);
 
     uprintf(uart, "Hello i2c Mocha!\n");
 
     while (true) {
-        timer_busy_sleep(timer, 1000);
+        timer_busy_sleep_ms(timer, 1u);
 
         // Read current temperature from an AS6212 I^2C-bus sensor and print the value
         if (i2c_write_byte(i2c, 0x48u, 0u)) { // select TVAL reg; also a presence check
diff --git a/sw/device/lib/hal/mocha.c b/sw/device/lib/hal/mocha.c
index 55e6670a..938314c9 100644
--- a/sw/device/lib/hal/mocha.c
+++ b/sw/device/lib/hal/mocha.c
@@ -108,7 +108,7 @@ spi_device_t mocha_system_spi_device(void)
 timer_t mocha_system_timer(void)
 {
 #if defined(__riscv_zcherihybrid)
-    return (timer_t)create_mmio_capability(timer_base, 0x120u);
+    return (timer_t)create_mmio_capability(timer_base, sizeof(struct timer_memory_layout));
 #else /* !defined(__riscv_zcherihybrid) */
     return (timer_t)timer_base;
 #endif /* defined(__riscv_zcherihybrid) */
@@ -140,3 +140,13 @@ void *mocha_system_dv_test_status(void)
     return (void *)dv_test_status_base;
 #endif /* defined(__riscv_zcherihybrid) */
 }
+
+inline uint64_t us_to_cycles(uint64_t us)
+{
+    return us * (SYSCLK_FREQ / 1000000u);
+};
+
+inline uint64_t cycles_to_us(uint64_t cycles)
+{
+    return cycles / (SYSCLK_FREQ / 1000000u);
+};
diff --git a/sw/device/lib/hal/mocha.h b/sw/device/lib/hal/mocha.h
index d1b9a522..ac118259 100644
--- a/sw/device/lib/hal/mocha.h
+++ b/sw/device/lib/hal/mocha.h
@@ -17,7 +17,7 @@
 #include "hal/uart.h"
 
 /* System clock frequency (50 MHz) */
-#define SYSCLK_FREQ (50000000)
+#define SYSCLK_FREQ (50000000u)
 /* System clock period in nanoseconds (20 ns) */
 #define SYSCLK_NS (20)
 
@@ -36,3 +36,6 @@ plic_t mocha_system_plic(void);
 void *mocha_system_dram(void);
 
 void *mocha_system_dv_test_status(void);
+
+uint64_t us_to_cycles(uint64_t us);
+uint64_t cycles_to_us(uint64_t cycles);
diff --git a/sw/device/lib/hal/timer.c b/sw/device/lib/hal/timer.c
index f8034546..8dce5a02 100644
--- a/sw/device/lib/hal/timer.c
+++ b/sw/device/lib/hal/timer.c
@@ -4,152 +4,119 @@
 
 #include "hal/timer.h"
 #include "hal/mmio.h"
+#include "hal/mocha.h"
 #include <stdbool.h>
 #include <stddef.h>
 #include <stdint.h>
 
-void timer_disable(timer_t timer)
-{
-    DEV_WRITE(timer + TIMER_CTRL_REG, 0x0);
-}
-
-void timer_enable(timer_t timer)
-{
-    DEV_WRITE(timer + TIMER_CTRL_REG, 0x1);
-}
-
-bool timer_get_enable(timer_t timer)
-{
-    return ((DEV_READ(timer + TIMER_CTRL_REG) & 0x1) == 0x1);
-}
-
-void timer_set_prescale_step(timer_t timer, uint16_t prescale, uint8_t step)
-{
-    DEV_WRITE(timer + TIMER_CFG0_REG,
-              (step << TIMER_STEP) | ((prescale & TIMER_PRESCALE_MASK) << TIMER_PRESCALE));
-}
-
-uint16_t timer_get_prescale(timer_t timer)
-{
-    return (uint16_t)(DEV_READ(timer + TIMER_CFG0_REG) & TIMER_PRESCALE_MASK);
-}
-
-uint8_t timer_get_step(timer_t timer)
-{
-    return (uint8_t)(DEV_READ(timer + TIMER_CFG0_REG) >> TIMER_STEP);
-}
-
-void timer_set_compare_lower(timer_t timer, uint32_t compare_lower)
-{
-    DEV_WRITE(timer + TIMER_COMPARE_LOWER0_0_REG, compare_lower);
-}
+static void timer_compare_write(timer_t timer, uint64_t compare);
 
-void timer_set_compare_upper(timer_t timer, uint32_t compare_upper)
-{
-    DEV_WRITE(timer + TIMER_COMPARE_UPPER0_0_REG, compare_upper);
-}
-
-void timer_set_compare(timer_t timer, uint64_t compare)
-{
-    timer_set_compare_lower(timer, (uint32_t)(compare & 0xFFFFFFFF));
-    timer_set_compare_upper(timer, (uint32_t)(compare >> 32));
-}
-
-uint32_t timer_get_compare_lower(timer_t timer)
-{
-    return DEV_READ(timer + TIMER_COMPARE_LOWER0_0_REG);
-}
-
-uint32_t timer_get_compare_upper(timer_t timer)
-{
-    return DEV_READ(timer + TIMER_COMPARE_UPPER0_0_REG);
-}
-
-uint64_t timer_get_compare(timer_t timer)
+void timer_init(timer_t timer)
 {
-    return (((uint64_t)timer_get_compare_upper(timer)) << 32) |
-           ((uint64_t)timer_get_compare_lower(timer));
+    timer_disable(timer);
+    timer_interrupt_enable_write(timer, false);
+    timer_interrupt_clear(timer);
+    uint64_t cycles = us_to_cycles(1u);
+    /* configure the timer to tick by one every us */
+    timer_cfg0 cfg = {
+        .prescale = cycles - 1u,
+        .step = 1u,
+    };
+    VOLATILE_WRITE(timer->cfg0, cfg);
 }
 
-void timer_set_value_lower(timer_t timer, uint32_t value_lower)
+bool timer_interrupt_enable_read(timer_t timer)
 {
-    DEV_WRITE(timer + TIMER_V_LOWER0_REG, value_lower);
+    timer_intr_enable0 intr_enable = VOLATILE_READ(timer->intr_enable0);
+    return intr_enable.ie;
 }
 
-void timer_set_value_upper(timer_t timer, uint32_t value_upper)
+void timer_interrupt_enable_write(timer_t timer, bool enable)
 {
-    DEV_WRITE(timer + TIMER_V_UPPER0_REG, value_upper);
+    timer_intr_enable0 intr_enable = { .ie = enable };
+    VOLATILE_WRITE(timer->intr_enable0, intr_enable);
 }
 
-void timer_set_value(timer_t timer, uint64_t value)
+void timer_interrupt_force(timer_t timer)
 {
-    timer_set_value_lower(timer, (uint32_t)(value & 0xFFFFFFFF));
-    timer_set_value_upper(timer, (uint32_t)(value >> 32));
+    timer_intr_test0 intr_test = { .t = true };
+    VOLATILE_WRITE(timer->intr_test0, intr_test);
 }
 
-uint32_t timer_get_value_lower(timer_t timer)
+void timer_interrupt_clear(timer_t timer)
 {
-    return DEV_READ(timer + TIMER_V_LOWER0_REG);
+    /* the rv_timer is effectively a level-triggered interrupt, so to
+     * clear it we can schedule an interrupt infinitely far away... */
+    timer_compare_write(timer, UINT64_MAX);
+    /* ...then clear the latched interrupt bit */
+    timer_intr_state0 intr_state = { .is = true };
+    VOLATILE_WRITE(timer->intr_state0, intr_state);
 }
 
-uint32_t timer_get_value_upper(timer_t timer)
+bool timer_interrupt_pending(timer_t timer)
 {
-    return DEV_READ(timer + TIMER_V_UPPER0_REG);
+    timer_intr_state0 intr_state = VOLATILE_READ(timer->intr_state0);
+    return intr_state.is;
 }
 
-uint64_t timer_get_value(timer_t timer)
+void timer_enable(timer_t timer)
 {
-    return (((uint64_t)timer_get_value_upper(timer)) << 32) |
-           ((uint64_t)timer_get_value_lower(timer));
+    timer_ctrl ctrl = { .active = true };
+    VOLATILE_WRITE(timer->ctrl, ctrl);
 }
 
-void timer_disable_interrupt(timer_t timer)
+void timer_disable(timer_t timer)
 {
-    DEV_WRITE(timer + TIMER_INTR_ENABLE0_REG, 0x0);
+    timer_ctrl ctrl = { .active = false };
+    VOLATILE_WRITE(timer->ctrl, ctrl);
 }
 
-void timer_enable_interrupt(timer_t timer)
+uint64_t timer_value_read_us(timer_t timer)
 {
-    DEV_WRITE(timer + TIMER_INTR_ENABLE0_REG, 0x1);
-}
+    uint32_t timer_lower, timer_upper, timer_upper_again;
+    do {
+        /* make sure the lower half of the timer value does
+         * not overflow while reading the two halves, see
+         * Unprivileged Spec Chapter 7.1 */
+        timer_upper = VOLATILE_READ(timer->timer_v_upper0);
+        timer_lower = VOLATILE_READ(timer->timer_v_lower0);
+        timer_upper_again = VOLATILE_READ(timer->timer_v_upper0);
+    } while (timer_upper != timer_upper_again);
 
-bool timer_get_interrupt_enable(timer_t timer)
-{
-    return ((DEV_READ(timer + TIMER_INTR_ENABLE0_REG) & 0x1) == 0x1);
+    return (((uint64_t)timer_upper) << 32u) | timer_lower;
 }
 
-bool timer_has_interrupt(timer_t timer)
+static void timer_compare_write(timer_t timer, uint64_t compare)
 {
-    return ((DEV_READ(timer + TIMER_INTR_STATE0_REG) & 0x1) == 0x1);
-}
+    uint32_t compare_lower = (uint32_t)compare;
+    uint32_t compare_upper = (uint32_t)(compare >> 32u);
 
-void timer_clear_interrupt(timer_t timer)
-{
-    DEV_WRITE(timer + TIMER_INTR_STATE0_REG, 0x1);
+    /* write all 1s to the bottom half first, then the top and
+     * bottom to not cause a spurious interrupt from writing an
+     * intermediate value, see Privileged Spec Chapter 3.2.1 */
+    VOLATILE_WRITE(timer->compare_lower0_0, UINT32_MAX);
+    VOLATILE_WRITE(timer->compare_upper0_0, compare_upper);
+    VOLATILE_WRITE(timer->compare_lower0_0, compare_lower);
 }
 
-void timer_trigger_alert(timer_t timer)
+void timer_schedule_in_us(timer_t timer, uint64_t us)
 {
-    DEV_WRITE(timer + TIMER_ALERT_TEST_REG, 0x1);
+    timer_compare_write(timer, timer_value_read_us(timer) + us);
 }
 
-void timer_trigger_interrupt(timer_t timer)
+void timer_schedule_in_ms(timer_t timer, uint64_t ms)
 {
-    DEV_WRITE(timer + TIMER_INTR_TEST0_REG, 0x1);
+    timer_schedule_in_us(timer, ms * 1000u);
 }
 
-void timer_init(timer_t timer)
+void timer_busy_sleep_us(timer_t timer, uint64_t us)
 {
-    timer_disable(timer);
-    timer_disable_interrupt(timer);
+    timer_schedule_in_us(timer, us);
+    while (!timer_interrupt_pending(timer)) {
+    }
 }
 
-void timer_busy_sleep(timer_t timer, uint64_t duration_steps)
+void timer_busy_sleep_ms(timer_t timer, uint64_t ms)
 {
-    timer_set_compare(timer, timer_get_value(timer) + duration_steps);
-    timer_clear_interrupt(timer);
-
-    // Poll for interrupt
-    while (!timer_has_interrupt(timer)) {
-    }
+    timer_busy_sleep_us(timer, ms * 1000u);
 }
diff --git a/sw/device/lib/hal/timer.h b/sw/device/lib/hal/timer.h
index ec3e8d24..5d2f248c 100644
--- a/sw/device/lib/hal/timer.h
+++ b/sw/device/lib/hal/timer.h
@@ -4,55 +4,25 @@
 
 #pragma once
 
+#include "autogen/timer.h"
 #include <stdbool.h>
 #include <stddef.h>
 #include <stdint.h>
 
-#define TIMER_ALERT_TEST_REG (0x0)
-
-#define TIMER_CTRL_REG (0x4)
-
-#define TIMER_INTR_ENABLE0_REG (0x100)
-#define TIMER_INTR_STATE0_REG  (0x104)
-#define TIMER_INTR_TEST0_REG   (0x108)
-
-#define TIMER_CFG0_REG      (0x10c)
-#define TIMER_PRESCALE      (0)
-#define TIMER_PRESCALE_MASK (0xFFF)
-#define TIMER_STEP          (16)
-
-#define TIMER_V_LOWER0_REG         (0x110)
-#define TIMER_V_UPPER0_REG         (0x114)
-#define TIMER_COMPARE_LOWER0_0_REG (0x118)
-#define TIMER_COMPARE_UPPER0_0_REG (0x11c)
+/* initialisation */
+void timer_init(timer_t timer);
 
-typedef void *timer_t;
+/* interrupts */
+bool timer_interrupt_enable_read(timer_t timer);
+void timer_interrupt_enable_write(timer_t timer, bool enable);
+void timer_interrupt_force(timer_t timer);
+void timer_interrupt_clear(timer_t timer);
+bool timer_interrupt_pending(timer_t timer);
 
-void timer_disable(timer_t timer);
 void timer_enable(timer_t timer);
-bool timer_get_enable(timer_t timer);
-void timer_set_prescale_step(timer_t timer, uint16_t prescale, uint8_t step);
-uint16_t timer_get_prescale(timer_t timer);
-uint8_t timer_get_step(timer_t timer);
-void timer_set_compare_lower(timer_t timer, uint32_t compare_lower);
-void timer_set_compare_upper(timer_t timer, uint32_t compare_upper);
-void timer_set_compare(timer_t timer, uint64_t compare);
-uint32_t timer_get_compare_lower(timer_t timer);
-uint32_t timer_get_compare_upper(timer_t timer);
-uint64_t timer_get_compare(timer_t timer);
-void timer_set_value_lower(timer_t timer, uint32_t value_lower);
-void timer_set_value_upper(timer_t timer, uint32_t value_upper);
-void timer_set_value(timer_t timer, uint64_t value);
-uint32_t timer_get_value_lower(timer_t timer);
-uint32_t timer_get_value_upper(timer_t timer);
-uint64_t timer_get_value(timer_t timer);
-void timer_disable_interrupt(timer_t timer);
-void timer_enable_interrupt(timer_t timer);
-bool timer_get_interrupt_enable(timer_t timer);
-bool timer_has_interrupt(timer_t timer);
-void timer_clear_interrupt(timer_t timer);
-void timer_trigger_alert(timer_t timer);
-void timer_trigger_interrupt(timer_t timer);
-
-void timer_init(timer_t timer);
-void timer_busy_sleep(timer_t timer, uint64_t duration_steps);
+void timer_disable(timer_t timer);
+uint64_t timer_value_read_us(timer_t timer);
+void timer_schedule_in_us(timer_t timer, uint64_t us);
+void timer_schedule_in_ms(timer_t timer, uint64_t ms);
+void timer_busy_sleep_us(timer_t timer, uint64_t us);
+void timer_busy_sleep_ms(timer_t timer, uint64_t ms);
diff --git a/sw/device/tests/timer/interrupt.c b/sw/device/tests/timer/interrupt.c
index 04e29d6f..699558c1 100644
--- a/sw/device/tests/timer/interrupt.c
+++ b/sw/device/tests/timer/interrupt.c
@@ -5,33 +5,34 @@
 #include "hal/hart.h"
 #include "hal/mocha.h"
 #include "hal/timer.h"
-#include "hal/uart.h"
 #include <stdbool.h>
 
-timer_t timer = NULL;
+volatile timer_t timer = NULL;
 volatile bool interrupt_handled = false;
 
 bool test_main(uart_t console)
 {
     (void)console;
 
+    /* initialise the timer */
+    timer = mocha_system_timer();
+    timer_init(timer);
+
     /* globally disable all interrupts at the hart */
     hart_global_interrupt_enable_set(false);
 
     /* enable timer interrupt at the hart */
     hart_interrupt_enable_write(interrupt_machine_timer);
 
-    /* initialise the timer */
-    timer = mocha_system_timer();
-    timer_init(timer);
-    timer_set_prescale_step(timer, (SYSCLK_FREQ / 1000000) - 1, 1); /* 1 tick/us */
-    timer_enable_interrupt(timer);
+    /* enable timer interrupt */
+    timer_interrupt_enable_write(timer, true);
+
     timer_enable(timer);
 
     for (size_t i = 0; i < 10; i++) {
         /* schedule an interrupt 100us from now */
         interrupt_handled = false;
-        timer_set_compare(timer, timer_get_value(timer) + 100);
+        timer_schedule_in_us(timer, 100u);
         WAIT_FOR_CONDITION_PREEMPTABLE(interrupt_handled);
     }
 
@@ -41,11 +42,9 @@ bool test_main(uart_t console)
 bool test_interrupt_handler(enum interrupt interrupt)
 {
     if (interrupt == interrupt_machine_timer) {
-        /* machine mode timer interrupt */
-        /* set next timer interrupt to be infinitely far into the future */
-        timer_set_compare(timer, UINT64_MAX);
-        /* clear the timer interrupt */
-        timer_clear_interrupt(timer);
+        /* machine mode timer interrupt, clear the interrupt by scheduling
+         * an interrupt infinitely far into the future */
+        timer_interrupt_clear(timer);
         interrupt_handled = true;
         return true;
     }
diff --git a/sw/device/tests/timer/smoketest.c b/sw/device/tests/timer/smoketest.c
index cd052cf8..32b1a0c0 100644
--- a/sw/device/tests/timer/smoketest.c
+++ b/sw/device/tests/timer/smoketest.c
@@ -16,16 +16,15 @@ bool accuracy_test(timer_t timer)
     bool has_intr_before_expire;
     bool has_intr_after_expire;
 
-    const uint64_t duration_steps = 100;
-    const uint64_t tolerance_steps = 10;
+    const uint64_t duration_us = 100;
+    const uint64_t tolerance_us = 10;
 
-    const uint64_t min_cycle_diff = (duration_steps - tolerance_steps) * (SYSCLK_FREQ / 1000000);
-    const uint64_t max_cycle_diff = (duration_steps + tolerance_steps) * (SYSCLK_FREQ / 1000000);
+    const uint64_t min_cycle_diff = us_to_cycles(duration_us - tolerance_us);
+    const uint64_t max_cycle_diff = us_to_cycles(duration_us + tolerance_us);
 
     timer_init(timer);
-    timer_set_prescale_step(timer, (SYSCLK_FREQ / 1000000) - 1, 1); // 1 tick/us
-    timer_set_compare(timer, timer_get_value(timer) + duration_steps);
-    timer_clear_interrupt(timer);
+    timer_schedule_in_us(timer, duration_us);
+    timer_interrupt_enable_write(timer, true);
 
     start_cycle = hart_cycle_get();
 
@@ -37,12 +36,12 @@ bool accuracy_test(timer_t timer)
     while (hart_cycle_get() <= min_cycle) {
     }
 
-    has_intr_before_expire = timer_has_interrupt(timer);
+    has_intr_before_expire = timer_interrupt_pending(timer);
 
     while (hart_cycle_get() <= max_cycle) {
     }
 
-    has_intr_after_expire = timer_has_interrupt(timer);
+    has_intr_after_expire = timer_interrupt_pending(timer);
 
     return (!has_intr_before_expire && has_intr_after_expire);
 }
@@ -52,19 +51,16 @@ bool timer_irq_test(timer_t timer)
     bool has_mtip_before_expire;
     bool has_mtip_after_expire;
 
-    const uint64_t duration_steps = 5;
+    const uint64_t duration_us = 5;
 
     timer_init(timer);
-    timer_set_prescale_step(timer, (SYSCLK_FREQ / 1000000) - 1, 1); // 1 tick/us
-    timer_set_compare(timer, timer_get_value(timer) + duration_steps);
-    timer_clear_interrupt(timer);
-    timer_enable_interrupt(timer);
-
+    timer_schedule_in_us(timer, duration_us);
+    timer_interrupt_enable_write(timer, true);
     timer_enable(timer);
 
     has_mtip_before_expire = hart_interrupt_any_pending(interrupt_machine_timer);
 
-    while (!timer_has_interrupt(timer)) {
+    while (!timer_interrupt_pending(timer)) {
     }
 
     has_mtip_after_expire = hart_interrupt_any_pending(interrupt_machine_timer);
