Sequential circuit diagnosis based on formal verification techniques