/* i8254 reload value for countdown */ /* XXX put in header file */