#ifndef _DEVICES_ACLINT_H
#define _DEVICES_ACLINT_H

#include "gen/aclint.h"
#include <stdint.h>

static void set_aclint_mtime(volatile aclint_t* reg, uint64_t value) {
    set_aclint_mtime_hi(reg, (uint32_t)(value >> 32));
    set_aclint_mtime_lo(reg, (uint32_t)value);
}

static uint64_t get_aclint_mtime(volatile aclint_t* reg) {
    // #if ( __riscv_xlen == 64)
    //     volatile uint64_t *mtime = (volatile uint64_t *)(RISCV_MTIME_ADDR);
    //     return *mtime;
    // #else
    uint32_t mtimeh_val;
    uint32_t mtimel_val;
    do {
        mtimeh_val = get_aclint_mtime_hi(reg);
        mtimel_val = get_aclint_mtime_lo(reg);
    } while(mtimeh_val != get_aclint_mtime_hi(reg));
    return (uint64_t)((((uint64_t)mtimeh_val) << 32) | mtimel_val);
    // #endif
}

static void set_aclint_mtimecmp(volatile aclint_t* reg, uint64_t value) {
    set_aclint_mtimecmp0lo(reg, (uint32_t)0xFFFFFFFF);
    set_aclint_mtimecmp0hi(reg, (uint32_t)(value >> 32));
    set_aclint_mtimecmp0lo(reg, (uint32_t)value);
}

static uint64_t get_aclint_mtimecmp(volatile aclint_t* reg) {
    uint64_t value = ((uint64_t)get_aclint_mtimecmp0hi(reg) << 32) | (uint64_t)get_aclint_mtimecmp0lo(reg);
    return value;
}

#endif /* _DEVICES_ACLINT_H */