A computer-implemented method of detecting livelock in a hardware design (102, 502) of an integrated circuit for an electronic system (104, 504), the method comprising: (a) receiving the hardware design (102, 502); (b) receiving a design for a hardware monitor (106, 300, 500) for monitoring the electronic system (104, 504), the hardware monitor (106, 300, 500) comprising: monitor and detection logic (108, 308, 508) configured to detect when a particular state has occurred in the electronic system (104, 504); and assertion evaluation logic (110, 310, 510) configured to periodically evaluate one or more formal assertions that assert a formal property related to reoccurrence of the particular state in the electronic system (104, 504) as detected by the monitor and detection logic (108, 308, 508) to determine whether the electronic system (104, 504) is in a livelock comprising the particular state; (c) binding the hardware design (102, 502) to the design for the hardware monitor (106, 300, 500); (d) loading the hardware design (102, 502), bindings, and the design for the hardware monitor (106, 300, 500) into a formal verification tool; (e) formally verifying, using the formal verification tool, that the one or more formal assertions evaluated by the assertion evaluation logic (110, 310, 510) are true for the hardware design (102, 502) bound to the design for the hardware monitor so that the monitor and detection logic (110, 310, 510) detects when the particular state has occurred, wherein formally verifying the one or more formal assertions comprises transforming the hardware design into a state-transition system and searching the state-transition system for a state in which the one or more asserted formal properties are not true; and (f) in response to an indication being output that each of the one or more formal assertions was successfully verified, encoding on a computer readable storage medium the verified hardware design which, when processed in an integrated circuit manufacturing system, configures the integrated circuit manufacturing system to manufacture an integrated circuit embodying the electronic system; wherein the assertion evaluation logic (110, 310, 510) is configured to evaluate one or more formal assertions that assert that if the particular state has occurred in the electronic system (104, 504) that the particular state does not reoccur in the electronic system (104, 504) within a predetermined number of clock cycles. (a) receiving the hardware design (102, 502); (b) receiving a design for a hardware monitor (106, 300, 500) for monitoring the electronic system (104, 504), the hardware monitor (106, 300, 500) comprising: monitor and detection logic (108, 308, 508) configured to detect when a particular state has occurred in the electronic system (104, 504); and assertion evaluation logic (110, 310, 510) configured to periodically evaluate one or more formal assertions that assert a formal property related to reoccurrence of the particular state in the electronic system (104, 504) as detected by the monitor and detection logic (108, 308, 508) to determine whether the electronic system (104, 504) is in a livelock comprising the particular state; monitor and detection logic (108, 308, 508) configured to detect when a particular state has occurred in the electronic system (104, 504); and assertion evaluation logic (110, 310, 510) configured to periodically evaluate one or more formal assertions that assert a formal property related to reoccurrence of the particular state in the electronic system (104, 504) as detected by the monitor and detection logic (108, 308, 508) to determine whether the electronic system (104, 504) is in a livelock comprising the particular state; (c) binding the hardware design (102, 502) to the design for the hardware monitor (106, 300, 500); (d) loading the hardware design (102, 502), bindings, and the design for the hardware monitor (106, 300, 500) into a formal verification tool; (e) formally verifying, using the formal verification tool, that the one or more formal assertions evaluated by the assertion evaluation logic (110, 310, 510) are true for the hardware design (102, 502) bound to the design for the hardware monitor so that the monitor and detection logic (110, 310, 510) detects when the particular state has occurred, wherein formally verifying the one or more formal assertions comprises transforming the hardware design into a state-transition system and searching the state-transition system for a state in which the one or more asserted formal properties are not true; and (f) in response to an indication being output that each of the one or more formal assertions was successfully verified, encoding on a computer readable storage medium the verified hardware design which, when processed in an integrated circuit manufacturing system, configures the integrated circuit manufacturing system to manufacture an integrated circuit embodying the electronic system; wherein the assertion evaluation logic (110, 310, 510) is configured to evaluate one or more formal assertions that assert that if the particular state has occurred in the electronic system (104, 504) that the particular state does not reoccur in the electronic system (104, 504) within a predetermined number of clock cycles.