Assessing performance of a hardware design using formal evaluation logic

Patent metadata

Field	Value
Publication number	US-12175179-B2
Application number	US-202218076231-A
Country	US
Kind code	B2
Filing date	Dec 6, 2022
Priority date	May 25, 2016
Publication date	Dec 24, 2024
Grant date	Dec 24, 2024

Abstract

A hardware monitor arranged to assess performance of a hardware design for an integrated circuit to complete a task. The hardware monitor includes monitoring and counting logic configured to count a number of cycles between start and completion of the symbolic task in the hardware design; and property evaluation logic configured to evaluate one or more formal properties related to the counted number of cycles to assess the performance of the hardware design in completing the symbolic task. The hardware monitor may be used by a formal verification tool to exhaustively verify that the hardware design meets a desired performance goal and/or to exhaustively identify a performance metric (e.g. best case and/or worst case performance) with respect to completion of the task.

First claim

What is claimed is:

1. A method of assessing the performance of a hardware design for an integrated circuit to complete a set of tasks, the method comprising:
monitoring one or more control signals and/or data signals of an instantiation of the hardware design to identify start and completion of a symbolic task by the instantiation of the hardware design, the symbolic task representing the set of tasks using one or more symbolic variables;
counting a number of cycles between the start and the completion of the symbolic task;
formally verifying, using a formal verification tool, that one or more formal properties related to the counted number of cycles are true for the hardware design to assess the performance of the instantiation of the hardware design in completing the symbolic task; and
outputting an indication of whether or not each of the one or more formal properties was successfully verified, the indication providing an exhaustive assessment of the performance of the instantiation of the hardware design in completing the set of tasks.

2. The method of claim 1 , wherein formally verifying that the one or more formal properties are true for the hardware design comprises formally verifying that the one or more properties are true for the hardware design for each task of the set of tasks.

3. The method of claim 1 , wherein the one or more formal properties related to the counted number of cycles are configured such that verification of the one or more formal properties determines whether the instantiation of the hardware design completes the symbolic task within a predetermined number of cycles.

4. The method of claim 1 , wherein the one or more formal properties related to the counted number of cycles are configured such that verification of the one or more formal properties identifies one or more performance metrics of the instantiation of the hardware design in completing the symbolic task.

5. The method of claim 4 , wherein the one or more formal properties comprises one or more covered properties that state that the counted number of cycles is equal to a particular number of cycles.

6. The method of claim 4 , wherein the one or more formal properties comprises a plurality of covered properties that each state that the counted number of cycles is equal to a different number of cycles.

7. The method of claim 1 , wherein the one or more formal properties comprises one or more asserted properties that state that the counted number of cycles is less than a predetermined number.

8. The method of claim 7 , wherein the one or more formal properties comprises an asserted property for each task of the set of tasks that states that if the symbolic task is that task, the counted number of cycles is less than a predetermined number.

9. The method of claim 1 , wherein:
monitoring the one or more control signals and/or data signals of the instantiation of the hardware design to identify the start and completion of the symbolic task by the instantiation of the hardware design comprises:
monitoring the one or more control signals and/or data signals of the instantiation of the hardware design to detect the start of the symbolic task, and in response to detecting the start of the symbolic task setting a sampled IN register, and
monitoring the one or more control signals and/or data signals of the instantiation of the hardware design to detect the completion of the symbolic task, and in response to detecting the completion of the symbolic task when the sampled IN register is set, set a sampled OUT register; and

counting the number of cycles between the start and the completion of the symbolic task comprises incrementing a counter that represents the counted number of cycles when the sampled IN register is set and the sampled OUT register is not set.

10. The method of claim 1 , wherein the integrated circuit forms a processor.

11. The method of claim 10 , wherein monitoring the one or more control signals and/or data signals of the instantiation of the hardware design to identify the start and completion of the symbolic task by the instantiation of the hardware design comprises detecting the start of the symbolic task when it is detected from the one or more control signals and/or data signals of the instantiation of the hardware design that a symbolic instruction has been fetched or decoded and detecting the completion of the symbolic task when it is detected from the one or more control signals and/or data signals of the instantiation of the hardware design that the symbolic instruction has been executed.

12. 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.

13. A non-transitory computer readable storage medium having stored thereon computer readable code adapted to perform the steps of the method as set forth in claim 1 when the code is run on a computer.

14. A system configured to assess the performance of a hardware design for an integrated circuit to complete a set of tasks, the system comprising one or more processors configured to:
monitor one or more control signals and/or data signals of an instantiation of the hardware design to identify start and completion of a symbolic task by the instantiation of the hardware design, the symbolic task representing the set of tasks using one or more symbolic variables;
count a number of cycles between the start and the completion of the symbolic task;
formally verify, using a formal verification tool, that one or more formal properties related to the counted number of cycles are true for the hardware design to assess the performance of the instantiation of the hardware design in completing the symbolic task; and
output an indication of whether or not each of the one or more formal properties was successfully verified, the indication providing an exhaustive assessment of the performance of the instantiation of the hardware design in completing the set of tasks.

15. The system of claim 14 , wherein the one or more processors are further configured to, when the one or more formal properties comprises an asserted property and the asserted property is not successfully verified, output an indication of a state of the instantiation of the hardware design in which the asserted property is not true.

16. The system of claim 14 , wherein the one or more processors are further configured to, when the one or more formal properties comprises a covered property and the covered property is successfully verified, output an indication of a state of the instantiation of the hardware design in which the covered property is true.

17. The system of claim 14 , wherein formally verifying that the one or more formal properties are true for the hardware design comprises formally verifying that the one or more formal properties are true for the hardware design for each task of the set of tasks.

18. The system of claim 14 , further comprising an integrated circuit manufacturing system configured to process the hardware design so as to manufacture the integrated circuit.

19. The system of claim 18 , wherein the integrated circuit manufacturing system comprises:
a non-transitory computer readable storage medium having stored thereon the hardware design;
a layout processing system configured to process the hardware design so as to generate a circuit layout description of the integrated circuit; and
an integrated circuit generation system configured t

Assignees

• Imagination Tech Ltd

Inventors

• Darbari Ashish
• Singleton Iain

Classifications

• G06F11/3409

  for performance assessment · CPC title

• G06F11/3652

  in-circuit-emulation [ICE] arrangements · CPC title

• G06F11/3648

  using additional hardware · CPC title

• G06F11/3636

  by tracing the execution of the program · CPC title

• G06F11/3608

  using formal methods, e.g. model checking, abstract interpretation (theorem proving G06N5/013) · CPC title