Livelock Detection in a Hardware Design Using Formal Evaluation Logic

A method of detecting livelock in a hardware design for an integrated circuit, the method comprising:

• (a) receiving the hardware design and a hardware monitor, the hardware monitor comprising:
• monitor and detection logic configured to detect when a particular state has occurred in an instantiation of the hardware design;
• and
• assertion evaluation logic configured to periodically evaluate one or more assertions that assert a formal property related to reoccurrence of the particular state in the instantiation of the hardware design to determine whether the instantiation of the hardware design is in a livelock comprising the predetermined state;
• (b) formally verifying, by a formal verification tool, the one or more formal assertions are true for the hardware design;
• and
• (c) outputting an indication of whether or not each of the one or more formal assertions was successfully verified to identify whether the instantiation of the hardware design can enter a livelock that includes the particular state.

A system configured to detect livelock in a hardware design for an integrated circuit, the system comprising:

• a memory configured to store:
• the hardware design;
• a formal verification tool;
• and
• a hardware monitor comprising:
• monitor and detection logic configured to detect when a particular state has occurred in an instantiation of the hardware design;
• and
• assertion evaluation logic configured to periodically evaluate one or more assertions that assert a formal property related to reoccurrence of the particular state in the instantiation of the hardware design to determine whether the instantiation of the hardware design is in a livelock comprising the predetermined state;
• and
• one or more processors configured to:
• formally verify, by the formal verification tool, that the one or more formal assertions are true for the hardware design;
• and
• output an indication of whether or not each of the one or more formal assertions was successfully verified to identify whether the instantiation of the hardware design can enter a livelock that includes the particular state.