Verification of hardware design for data transformation component

Patent metadata

Field	Value
Publication number	US-11995386-B2
Application number	US-202318201070-A
Country	US
Kind code	B2
Filing date	May 23, 2023
Priority date	Oct 8, 2019
Publication date	May 28, 2024
Grant date	May 28, 2024

Abstract

A hardware design for a main data transformation component is verified. The main data transformation component is representable as a hierarchical set of data transformation components which includes (i) leaf data transformation components which do not have children, and (ii) parent data transformation components which comprise one or more child data transformation components. For each of the leaf data transformation components, it is verified that an instantiation of the hardware design for the leaf data transformation component generates an expected output transaction. For each of the parent data transformation components, it is formally verified that an instantiation of an abstracted hardware design generates an expected output transaction in response to each of test input transactions. The abstracted hardware design for the parent data transformation component represents each of the child data transformation components of the parent data transformation component with a corresponding abstracted component that for a specific input transaction to the child data transformation component produces a specific output transaction with a causal deterministic relationship to the specific input transaction.

First claim

What is claimed is:

1. A computer-implemented method of verifying a hardware design for a main component, the main component being representable as a hierarchical set of components, each component of the hierarchical set of components, other than a component at a lowest level in the hierarchy, comprises at least one component at a next lowest level in the hierarchy, the method comprising:
verifying each component of the hierarchical set of components by formally verifying, at one or more processors using a formal verification tool, that an instantiation of a version of a portion of the hardware design corresponding to that component generates an expected output transaction in response to each of a plurality of test input transactions; and
wherein, in the version of the portion of the hardware design corresponding to a component, logic for driving an output of each of the at least one component at the next lowest level has been replaced with a corresponding abstracted component that is configured to, for a specific input transaction to the next lowest level component, produce a specific output transaction with a deterministic causal relationship to the specific input transaction, and during formal verification the formal verification tool is configured to select the specific input transaction and the specific output transaction pair to be each possible valid input transaction and valid output transaction pair for the next lowest level component.

2. The method of claim 1 , wherein the corresponding abstracted component for a next lowest level component is defined in a formal verification language by (i) a definition of a symbolic input transaction to the next lowest level component which specifies the specific input transaction, (ii) a definition of a symbolic output transaction of the next lowest level component which specifies the specific output transaction, and (iii) one or more constraints that establish a deterministic causal relationship between the symbolic input transaction and the symbolic output transaction.

3. The method of claim 2 , wherein the symbolic input transaction to the next lowest level component is a symbolic constant that represents the valid input transactions to the next lowest level component.

4. The method of claim 2 , wherein the symbolic output transaction of the next lowest level component is a symbolic constant that represents the valid output transactions for the next lowest level component.

5. The method of claim 2 , wherein the one or more constraints are implemented by one or more formal assumption statements.

6. The method of claim 2 , wherein, when a component comprises a plurality of next lowest level components, the version of the portion of the hardware design corresponding to that component comprises a description of a relationship between the symbolic input and output transactions of the plurality of next lowest level components.

7. The method of claim 1 , wherein each component of the hierarchical set of components is a data transformation component configured to receive one or more data inputs, perform a data transformation on the one or more data inputs, and output a result of the data transformation.

8. The method of claim 1 , wherein verifying that an instantiation of the version of the portion of the hardware design corresponding to a component at the lowest level of the hierarchy generates an expected output transaction in response to a test input transaction comprises verifying that the instantiation of the version of the portion of the hardware design corresponding to that component generates an output transaction, with a deterministic causal relationship to the test input transaction, that is correct with respect to a function implemented by that component.

9. The method of claim 1 , wherein verifying that an instantiation of the version of the portion of the hardware design corresponding to a component that comprises one or more next lowest level components generates an expected output transaction in response to a test input transaction comprises verifying that an instantiation of the version of the portion of the hardware design corresponding to that component generates an output transaction, with a deterministic causal relationship to the input transaction, that has been generated by processing the test input transaction through an expected combination of the one or more next lowest level components of that component.

10. The method of claim 1 , wherein the plurality of test input transactions for a component comprises all valid input transactions to the component.

11. The method of claim 1 , further comprising outputting one or more control signals indicating whether the verification of each component of the hierarchical set of components was successful.

12. The method of claim 1 , further comprising, in response to determining that the verification of a component of the hierarchical set of components was not successful, determining whether the verification of the component was inconclusive; and in response to determining that the verification of the component was inconclusive, representing the main component using a different hierarchical set of components, and verifying at least a portion of the components of the different hierarchical set of components.

13. The method of claim 12 , further comprising, when the verification of a component at the lowest level of the hierarchy is inconclusive, converting that component into a component that comprises a plurality of next lowest level components to form the different hierarchical set of components, verifying each next lowest level component, and verifying the component after each next lowest level component has be replaced, in the version of the portion of the hardware design corresponding to the component, with a corresponding abstracted component.

14. The method of claim 12 , further comprising, in response to determining that the verification of the component was not inconclusive, modifying the hardware design for the main component to generate a modified hardware design for the main component.

15. The method of claim 1 , further comprising, in response to determining that the verification of each component of the set of hierarchical components was successful, manufacturing, using an integrated circuit manufacturing system, an integrated circuit embodying the main component according to the hardware design.

16. The method of claim 1 , wherein, when processed at an integrated circuit manufacturing system, the hardware design for the main component configures the integrated circuit manufacturing system to manufacture an integrated circuit embodying the main component.

17. The method of claim 1 , wherein, in the version of the portion of the hardware design corresponding to a component, each abstracted component replaces all of the corresponding next lowest level component.

18. The method of claim 1 , wherein an instantiation of the version of the portion of the hardware design corresponding to a component comprises a mathematical model of the version of the portion of the hardware design generated by the formal verification tool.

19. A system for verifying a hardware design for a main component, the main component being representable as a hierarchical set of components, each component of the hierarchical set of components, other than a component at a lowest level in the hierarchy, comprises at least one component at a next lowest level in the hierarchy, the system comprising:
memory configured to store:
one or more formal verification tools; and

one o

Assignees

• Imagination Tech Ltd

Inventors

• Elliott Sam

Classifications

• G06F30/33 Primary

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

• G01R31/318314

  Tools, e.g. program interfaces, test suite, test bench, simulation hardware, test compiler, test program languages (simulation software G01R31/318357; emulators G06F11/261) · CPC title

• G06F30/3323 Primary

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

• G06F30/337

  Design optimisation · CPC title

• G06F30/3308

  using simulation · CPC title