/* Return the value of the General Configuration Register.  */
static uint32_t hpet_gconf_get(void)
/* Return the value of the General Configuration Register.  */
static uint32_t hpet_gconf_get(void)
{
	return sys_read32(GCONF_REG);
}