Abstraction-based livelock/deadlock checking for hardware verification

A non-transitory computer-readable storage medium storing instructions that when executed by a computer cause the computer to perform 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 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.

An apparatus 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, comprising:

• a processor;
• a memory;
• an identification mechanism configured to identify 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;
• a construction mechanism configured to construct 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;
• a search mechanism configured to search for one or more livelocks in the abstract machine;
• and
• a verification mechanism, wherein if a livelock is found in the abstract machine, the verification mechanism is configured to verify 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.