/* Sets the timer match value for a 64-bit timer. */
void TimerMatchSet64(unsigned long ulBase, unsigned long long ullValue)
/* Sets the timer match value for a 64-bit timer. */
void TimerMatchSet64(unsigned long ulBase, unsigned long long ullValue)
{
    ASSERT(TimerBaseValid(ulBase));
    HWREG(ulBase + TIMER_O_TBMATCHR) = ullValue >> 32;
    HWREG(ulBase + TIMER_O_TAMATCHR) = ullValue & 0xffffffff;
}