#ifndef _DEVICES_ACLINT_H
#define _DEVICES_ACLINT_H

#include <stdint.h>
#include "gen/aclint.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){
    uint64_t value = ((uint64_t)get_aclint_mtime_hi(reg) << 32) | (uint64_t)get_aclint_mtime_lo(reg);
    return value;
}

static void set_aclint_mtimecmp(volatile aclint_t* reg, uint64_t value){
    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 */