The use of model checking in ATPG for sequential circuits