Deadlock detection in hardware design using assertion based verification

Patent metadata

Field	Value
Publication number	US-9767236-B2
Application number	US-201514674651-A
Country	US
Kind code	B2
Filing date	Mar 31, 2015
Priority date	Mar 31, 2014
Publication date	Sep 19, 2017
Grant date	Sep 19, 2017

Abstract

Methods and systems for detecting deadlock in a hardware design. The method comprises identifying one or more control signals in the hardware design; generating a state machine for each of the one or more control signals to track the state of the control signal; generating one or more assertions for each control signal to detect that the control signal is in a deadlock state from the state machine; and detecting whether any of the one or more control signal are in a deadlock state using the assertions. The method may also comprise generating one or more fairness constraints to impose on a particular assertion and detecting the particular control signal is in the deadlock state using the assertions under the fairness constraints.

First claim

The invention claimed is:

1. A method to detect deadlock in a hardware design, comprising:
identifying, in a processor, one or more key control signals in the hardware design, each key control signal enabling or blocking an action from happening;
generating, in a processor, a state machine for each identified key control signal to track the state of that key control signal;
generating, in a processor, one or more assertions for each identified key control signal to detect whether that key control signal is in a deadlock state based on data from the state machine for that key control signal, each of the one or more assertions for each identified key control signal defined in an assertion language; and
determining, in a processor, whether the hardware design can enter a deadlock state by detecting, through formal verification or simulation based verification of the one or more assertions for each identified key control signal in conjunction with said state machines, whether any of the identified key control signals can enter a deadlock state further comprising, in response to determining the hardware design can enter a deadlock state, outputting an indication of the detected deadlock state and updating the hardware design based on the outputted indication.

2. The method of claim 1 , wherein formal verification of the one or more assertions for each identified key control signal comprises using a formal verification tool to search an entire reachable state space of the hardware design to determine whether there is a state in which any of the one or more assertions for the identified key control signals is not valid.

3. The method of claim 1 , wherein simulation based verification of the one or more assertions for each identified key control signal comprises:
applying stimuli to the hardware design;
tracking, using the state machines, the state of the identified key control signals in response to the stimuli; and
evaluating the one or more assertions for each identified key control signal to determine whether any of the identified key control signals have entered a deadlock state.

4. The method of claim 1 , wherein the one or more assertions for each identified key control signal are verified under one or more fairness constraints, each fairness constraint ensuring certain behavior takes place on one or more inputs of the hardware design to allow a valid sequence of state transformations and interactions to take place during simulation based verification or formal verification of an assertion.

5. The method of claim 1 , wherein identifying the one or more key control signals comprises obtaining a configuration file that comprises a list of the one or more key control signals.

6. The method of claim 1 , wherein identifying the one or more key control signals comprises extracting the one or more key control signals from the hardware design.

7. The method of claim 1 , wherein at least one of the one or more assertions asserts that if a particular control signal is not true then sometime in the future the particular control signal will be true.

8. The method of claim 1 , wherein at least one of the one or more assertions asserts that if a particular control signal falls then sometime in the future the particular control signal will rise.

9. The method of claim 1 , wherein the hardware design is a high level language description of a System on Chip.

10. A system to detect deadlock in a hardware design, the system comprising:
one or more state machines, each state machine configured to track the state of a key control signal in the hardware design, each key control signal enabling or blocking an action from happening;
an assertion verification unit in communication with the one or more state machines, the assertion verification unit configured to use one or more assertions to analyze the one or more state machines to determine whether any of the key control signals is in a deadlock state, each of the one or more assertions defined in an assertion language; and
a test bench configured to determine whether the hardware design can enter a deadlock state by detecting, through formal verification or simulation based verification of the one or more assertions via the assertion verification unit, whether any of the key control signals can enter a deadlock state wherein the test bench is further configured to, in response to determining the hardware design can enter a deadlock state, output an indication of the detected deadlock state whereby the hardware design is updated based on the outputted indication.

11. The system of claim 10 , wherein formal verification of the one or more assertions comprises using a formal verification tool to search an entire reachable state space of the hardware design to determine whether there is a state in which any of the one or more assertions is not valid.

12. The system of claim 10 , wherein simulation based verification of the one or more assertions comprises:
applying stimuli to the hardware design;
tracking, using the state machines, the state of the key control signals in response to the stimuli; and
evaluating the one or more assertions to determine whether any of the key control signals have entered a deadlock state.

13. The system of claim 10 , wherein the assertion verification unit is configured to evaluate the one or more assertions under one or more fairness constraints, each fairness constraint ensuring certain behavior takes place on one or more inputs of the hardware design to allow a valid sequence of state transformations and interactions to take place during simulation based verification or formal verification of an assertion.

14. The system of claim 10 , wherein at least one of the one or more assertions asserts that if a particular control signal is not true then sometime in the future the particular control signal will be true.

15. The system of claim 10 , wherein at least one of the one or more assertions asserts that if a particular control signal falls then sometime in the future the particular control signal will rise.

16. The system of claim 10 , wherein each of the one or more state machines comprises:
a register; and
a logic unit in communication with the register, the logic unit configured to periodically identify the state of the key control signal and store the identified state in the register.

17. The system of claim 10 , wherein the hardware design is a high level language description of a System on Chip.

18. A non-transitory computer readable storage medium having stored thereon computer executable program code that when executed causes at least one processor to:
identify one or more key control signals in a hardware design, each key control signal enabling or blocking an action from happening;
generate a state machine for each identified key control signal to track the state of that key control signal;
generate one or more assertions for each identified key control signal to detect whether that key control signal is in a deadlock state based on data from the state machine for that key control signal, each of the one or more assertions for each identified key control signal defined in an assertion language; and
determine whether the hardware design can enter a deadlock state by detecting, through formal verification or simulation based verification of the one or more assertions for each identified key control signal in conjunction with said state machines, whether any of the identified key control signals can enter a deadlock state; and
in response to determining the hardware design can enter

Assignees

• Imagination Tech Ltd

Inventors

• Darbari Ashish
• Mckellar Colin

Classifications

• G06F30/327

  Logic synthesis; Behaviour synthesis, e.g. mapping logic, HDL to netlist, high-level language to RTL or netlist · CPC title

• G06F30/30

  Circuit design · CPC title

• G06F30/3323 Primary

  using formal methods, e.g. equivalence checking or property checking · CPC title

• G06F9/524

  Deadlock detection or avoidance · CPC title

• G06F30/33

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