/* Write to the Timer Configuration Register. 
This writes the specified value to the Timer Configuration Register of Timer #0. */
static void hpet_timer_conf_set(uint32_t val)
/* Write to the Timer Configuration Register. 
This writes the specified value to the Timer Configuration Register of Timer #0. */
static void hpet_timer_conf_set(uint32_t val)
{
	sys_write32(val, TIMER0_CONF_REG);
}