#include <stdio.h>

#include "basic.h"
#include "config.h"
#include "errnum.h"
#include "eventq.h"

// NOTE: watchdog timer should be clocked by ACLK (32 KHz) for 1 sec intervals

void watchdogInit(void) 
{
  return;
}

// Watchdog Timer interrupt service routine
void watchdog_timer(void)
{
  eventqFireEvent(EVENTQ_EVENT_RTCTICK);
  eventqFireEvent(EVENTQ_EVENT_TIMERTICK);
}