Verification of hardware design for data transformation component

Patent metadata

Field	Value
Publication number	US-11657198-B2
Application number	US-202117384599-A
Country	US
Kind code	B2
Filing date	Jul 23, 2021
Priority date	Oct 8, 2019
Publication date	May 23, 2023
Grant date	May 23, 2023

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) a plurality of leaf data transformation components which do not have children, and (ii) one or more parent data transformation components which each comprise one or more child data transformation components. For each of the plurality of 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 in response to each of a plurality of test input transactions. For each of the one or more parent data transformation components, it is formally verified, using a formal verification tool, that an instantiation of an abstracted hardware design for the parent data transformation component generates an expected output transaction in response to each of a plurality of test input transactions. The abstracted hardware design for the parent data transformation component represents each of the one or more 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 is configured to produce a specific output transaction with a causal deterministic relationship to the specific input transaction.

First claim

What is claimed is:

1. A method of generating an integrated circuit hardware design for a main data transformation component that is configured to perform a data transformation on one on one or more inputs to produce one or more outputs, the method comprising:
(a) generating a high level specification for the main data transformation component in a formal verification language that defines (i) the one or more inputs and the one or more outputs of the main data transformation component, (ii) a set of one or more child data transformation components, and (iii) movement of the one or more inputs through the set of one or more child data transformation components to generate the one or more outputs;
(b) for each child data transformation component:
determining whether the child data transformation component is to be represented by a set of one or more further child data transformation components,
in response to determining that the child data transformation component is not to be represented by a set of one or more further child data transformation components, generating a detailed specification for that child data transformation component in a formal verification language,
in response to determining that the child data transformation component is to be represented by a set of one or more further child data transformation components, generating a high level specification for the child data transformation component in a formal verification language that defines (i) one or more inputs and one or more outputs of the child data transformation component, (ii) the set of one or more further child data transformation components, and (iii) movement of the one or more inputs of the child data transformation component through the set of one or more further child data transformation components to generate the one or more outputs of the child data transformation component, and repeating (b) for the set of one or more further child data transformation components;

(c) generating an integrated circuit hardware design for each detailed specification;
(d) generating an integrated circuit hardware design for the main data transformation component from the integrated circuit hardware designs for the detailed specifications; and
(e) verifying the integrated circuit hardware design for the main data transformation component using the high level specifications and the integrated circuit hardware designs for the detailed specifications.

2. The method of claim 1 , wherein the definition of a child data transformation in a high level specification does not describe the data transformation performed by that child data transformation component.

3. The method of claim 2 , wherein the definition of child data transformation component in a high level specification comprises a definition of a symbolic input transaction to the child data transformation component, a definition of a symbolic output transaction of the child data transformation component, and one or more constraints that establish a deterministic causal relationship between the symbolic input transaction and the symbolic output transaction.

4. The method of claim 3 , wherein the symbolic input transaction to a child data transformation component is a symbolic constant that represents the valid input transactions to that child data transformation component.

5. The method of claim 3 , wherein the symbolic output transaction of a child data transformation component is a symbolic constant that represents the valid output transactions for that child data transformation component.

6. The method of claim 3 , wherein the one or more constraints that establish a deterministic causal relationship between the symbolic input transaction and the symbolic output transaction are implemented by one or more formal assumption statements.

7. The method of claim 3 , wherein the definition of movement of the one or more inputs through the set of one or more child data transformation components to generate the one or more outputs in a high level specification comprises a description of a relationship between the symbolic input and output transactions of the set of one or more child data transformation components.

8. The method of claim 1 , wherein each child data transformation component is configured to perform a data transformation on one or more inputs to generate one or more outputs.

9. The method of claim 1 , wherein verifying the integrated circuit hardware design for the main data transformation component using the high level specifications and the integrated circuit hardware designs for the detailed specifications comprises verifying, for each high level specification and each integrated circuit hardware design for a detailed specification, that an instantiation thereof generates an expected output transaction in response to each of a plurality of test input transactions.

10. The method of claim 9 , wherein verifying that an instantiation of an integrated circuit hardware design for a detailed specification generates an expected output transaction in response to an input transaction comprises verifying that the instantiation of the integrated circuit hardware design generates an output transaction, with a deterministic causal relationship to the input transaction, that is correct with respect to a data transformation set out in the detailed specification.

11. The method of claim 9 , wherein verifying that an instantiation of a high level specification generates an expected output transaction in response to an input transaction comprises verifying that an instantiation of the high level specification generates an output transaction, with a deterministic causal relationship to the input transaction, that has been generated by processing the input transaction through an expected combination of the set of one or more child data transformation components defined in the high level specification.

12. The method of claim 9 , wherein the plurality of test input transactions for an integrated circuit hardware design for a detailed specification comprises all valid input transactions to the child data transformation component corresponding to the detailed specification.

13. The method of claim 9 , wherein the plurality of test input transactions for a high level specification comprises all valid input transactions to the data transformation component corresponding to the high level specification.

14. The method of claim 9 , wherein verifying that an instantiation of the integrated circuit hardware design for a detailed specification generates an expected output transaction in response to each of a plurality of test input transactions comprises formally verifying, using a formal verification tool, that the instantiation of the integrated circuit hardware design generates an expected output transaction in response to each of the plurality of test input transactions.

15. The method of claim 1 , further comprising outputting one or more control signals indicating whether the verification was successful.

16. The method of claim 1 , further comprising, in response to determining that the verification was not successful, modifying the hardware design for the main data transformation component to generate a modified hardware design for the main data transformation component.

17. The method of claim 1 , further comprising, in response to determining that the verification was successful, manufacturing, using an integrated circuit manufacturing system, an integrated circuit embodying the main data transformation component according to the integrated circuit hardware design for the main data tran

Assignees

• Imagination Tech Ltd

Inventors

• Elliott Sam

Classifications

• G06F2119/18

  Manufacturability analysis or optimisation for manufacturability · CPC title

• G06F30/3323 Primary

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

• G06F30/3308

  using simulation · CPC title

• G06F2111/12

  Symbolic schematics · CPC title

• G06F2115/02

  System on chip [SoC] design · CPC title