Livelock detection in a hardware design using formal evaluation logic

Patent metadata

Field	Value
Publication number	US-12050849-B2
Application number	US-202217749054-A
Country	US
Kind code	B2
Filing date	May 19, 2022
Priority date	Jun 20, 2016
Publication date	Jul 30, 2024
Grant date	Jul 30, 2024

Abstract

A hardware monitor arranged to detect livelock in a hardware design for an integrated circuit. The hardware monitor includes 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 detect whether the instantiation of the hardware design is in a livelock comprising the predetermined state. The hardware monitor may be used by a formal verification tool to exhaustively verify that the instantiation of the hardware design cannot enter a livelock comprising the predetermined state.

First claim

What is claimed is:

1. A method of detecting whether a hardware design for an integrated circuit that forms a processor can enter livelock, the method comprising:
configuring a hardware monitor to detect when a particular state has occurred in an instantiation of the hardware design;
configuring the hardware monitor to periodically evaluate one or more assertions to determine whether the instantiation of the hardware design is in a livelock comprising the particular state, the one or more assertions comprising an assertion that asserts that a number of occurrences of the particular state in the instantiation of the hardware design between a start event and a stop event is less than a predetermined number; and
formally verifying, by a formal verification tool, that the one or more assertions of the hardware monitor are true for the instantiation of the hardware design to determine whether the instantiation of the hardware design can enter a livelock that includes the particular state;
wherein the start event is when the processor is in an idle state and the stop event is when the processor is in an idle state.

2. The method of claim 1 , further comprising configuring the hardware monitor to:
monitor one or more control signals and/or data signals of the instantiation of the hardware design to detect the start event and in response to detecting the start event set a seen start register;
monitor one or more controls signals and/or data signals of the instantiation of the hardware design to detect the stop event, and in response to detecting the stop event when the seen start register is set, set a seen stop register;
in response to detecting the particular state has occurred in the instantiation of the hardware design, set a state register; and
increment a counter that represents the number of occurrences of the particular state between the start event and the stop event when the seen register is set, the state register is set, and the seen stop register is not set.

3. The method of claim 2 , wherein the one or more assertions comprises an assertion that asserts that when the seen start register is set and the seen stop register is not set that the counter is less than the predetermined number.

4. The method of claim 1 , wherein the particular state is based on a symbolic variable, and when the one or more assertions are verified by the formal verification tool, the formal verification tool formally verifies the one or more assertions are true for the instantiation of the hardware design for each valid value of the symbolic variable.

5. The method of claim 1 , further comprising outputting an indication of whether or not each of the one or more assertions was successfully verified to identify whether the instantiation of the hardware design can enter livelock that includes the particular state.

6. The method of claim 1 , further comprising, when one of the one or more assertions is not successfully verified, outputting an indication of a sequence of states of the instantiation of the hardware design for which the assertion is not true.

7. The method of claim 6 , further comprising, using the indication of the sequence of states of the instantiation of the hardware design for which the assertion is not true to modify the hardware design to avoid the livelock that includes the particular state.

8. The method of claim 1 , wherein when the hardware design is processed in an integrated circuit manufacturing system, the hardware design configures the integrated circuit manufacturing system to manufacture the integrated circuit.

9. The method of claim 1 , further comprising, in response to each of the one or more assertions being successfully verified, generating a hardware manifestation of the integrated circuit based on the hardware design.

Assignees

• Imagination Tech Ltd

Inventors

• Darbari Ashish
• Singleton Iain

Classifications

• G06F9/3802

  Instruction prefetching · CPC title

• G06F9/30145

  Instruction analysis, e.g. decoding, instruction word fields · CPC title

• G06F30/333

  Design for testability [DFT], e.g. scan chain or built-in self-test [BIST] · CPC title

• G06F30/33

  Design verification, e.g. functional simulation or model checking · CPC title

• G06F11/3055

  Monitoring arrangements for monitoring the status of the computing system or of the computing system component, e.g. monitoring if the computing system is on, off, available, not available (error or fault processing without redundancy G06F11/0703; error detection or correction by redundancy in data representation G06F11/08; error detection or correction of the data by redundancy in operations G06F11/14; error detection or correction by redundancy in hardware G06F11/16) · CPC title