1. A method for checking a livelock in a circuit design, wherein a livelock is a set of states in the circuit design that does not have any paths to a state outside the set of states that is reachable from an initial state of the circuit design, the method comprising: identifying a finite state machine (FSM) in the circuit design, wherein the FSM comprises a first set of state variables corresponding to a first set of sequential elements; constructing an abstract machine of the circuit design, wherein the abstract machine includes the FSM and a second set of state variables corresponding to a second set of sequential elements, wherein the second set of sequential elements drive the first set of sequential elements; searching, by computer, for one or more livelocks in the abstract machine; and if a livelock is found in the abstract machine, verifying that the livelock is also present in a concrete machine of the circuit design, wherein the concrete machine includes the FSM and a third set of state variables corresponding to a third set of sequential elements, wherein the second set of state variables is a subset of the third set of state variables.