Verification of hardware design for data transformation pipeline with equivalent data transformation element output constraint

Patent metadata

Field	Value
Publication number	US-10719646-B2
Application number	US-201916373774-A
Country	US
Kind code	B2
Filing date	Apr 3, 2019
Priority date	Apr 5, 2018
Publication date	Jul 21, 2020
Grant date	Jul 21, 2020

Abstract

Methods and systems for verifying, via formal verification, a hardware design for a data transformation pipeline comprising one or more data transformation elements that perform a data transformation on one or more inputs, wherein the formal verification is performed under conditions that simplify the data transformations calculations that the formal verification tool has to perform. In one embodiment the hardware design for the data transformation pipeline is verified by formally verifying that the output of an instantiation of the hardware design produces the same output as an instantiation of a hardware design for another data transformation pipeline for a predetermined set of transactions under a constraint that substantially equivalent data transformation elements between the data transformation pipelines produce the same output(s) in response to the same input(s).

First claim

What is claimed is:

1. A computer-implemented method of verifying a hardware design for a first data transformation pipeline, the first data transformation pipeline comprising one or more data transformation elements that perform a data transformation on one or more inputs, the method comprising, at one or more processors:
formally verifying that a set of one or more outputs of an instantiation of the hardware design for the first data transformation pipeline matches a set of one or more outputs of an instantiation of a hardware design for a second data transformation pipeline for a predetermined set of transactions, wherein the second data transformation pipeline comprises one or more data transformation elements that perform a data transformation on one or more inputs, a data transformation element of the second data transformation pipeline being substantially equivalent to a data transformation element of the first data transformation pipeline;
wherein the formal verification is performed under a constraint that the substantially equivalent data transformation elements of the first and second data transformation pipelines produce the same outputs in response to the same inputs.

2. The method of claim 1 , wherein the first data transformation pipeline and the second data transformation pipeline are different.

3. The method of claim 2 , wherein the constraint is that when the substantially equivalent data transformation elements of instantiations of the hardware designs for the first and second data transformation pipelines receive the same inputs at the same time that they produce a same set of one or more outputs in response to the inputs.

4. The method of claim 2 , wherein the constraint is that when the substantially equivalent data transformation elements of instantiations of the hardware designs for the first and second data transformation pipelines receive the same inputs at different, but related, points in time that they produce a same set of one or more outputs in response to the inputs.

5. The method of claim 2 , wherein the substantially equivalent data transformation elements of the first and second data transformation pipelines are identical.

6. The method of claim 2 , wherein the substantially equivalent data transformation elements of the first and second data transformation pipelines are not identical, and the method further comprises formally verifying that the substantially equivalent data transformation elements of the first and second data transformations pipelines are functionally equivalent.

7. The method of claim 1 , wherein the first and second data transformation pipelines are the same.

8. The method of claim 7 , further comprising, prior to the formal verification, linking the hardware design for the second data transformation pipeline to a hardware design for a capture module, the capture module configured to record a set of one or more inputs to and a set of one or more outputs from the second data transformation pipeline and record a set of one or more inputs to and a set of one or more outputs from the substantially equivalent data transformation element of the second data transformation pipeline when an instantiation of the hardware design for the second data transformation pipeline executes a transaction from a predetermined state of the second data transformation pipeline.

9. The method of claim 8 , wherein the constraint is that when the substantially equivalent data transformation element of an instantiation of the hardware design for the first data transformation pipeline receives the recorded set of one or more inputs for the data transformation element that the substantially equivalent data transformation element of the instantiation of the hardware design for the first data transformation pipeline produces the corresponding recorded set of one or more outputs for the data transformation element.

10. The method of claim 8 , wherein formally verifying that the set of one or more outputs of the instantiation of the hardware design for the first data transformation pipeline matches the set of one or more outputs of the instantiation of the hardware design for the second data transformation pipeline for a predetermined set of transactions comprises formally verifying that if an instantiation of the hardware design for the first data transformation pipeline receives the recorded set of one or more pipeline inputs that the set of one or more outputs of the instantiation of the hardware design for the first data transformation pipeline matches the recorded set of one or more pipeline outputs.

11. The method of claim 8 , wherein the capture module is configured to record the set of one or more inputs to and the set of one or more outputs from the substantially equivalent data transformation element of an instantiation of the hardware design for the second data transformation pipeline for a predetermined number of cycles following a reset of the instantiation of the hardware design for the second data transformation pipeline.

12. The method of claim 8 , further comprising formally verifying that an instantiation of the hardware design for the second data transformation pipeline generates a correct output to a transformation performed on any set of inputs from the predetermined state of the second data transformation pipeline.

13. The method of claim 1 , further comprising, prior to the formal verification, replacing the substantially equivalent data transformation element of the first data transformation pipeline with a black box element and/or replacing the substantially equivalent data transformation element of the second data transformation pipeline with a black box element; and wherein when the substantially equivalent data transformation element of the first data transformation pipeline is replaced with a black box element the constraint constrains the behaviour of that black box element.

14. The method of claim 13 , wherein the formal verification is performed under a second constraint or set of constraints that ensure that at least one black box element does not generate outputs that cannot be generated validly by the corresponding data transformation element.

15. The method of claim 1 , wherein:
a second data transformation element of the second data transformation pipeline is substantially equivalent to another data transformation element of the first data transformation pipeline; and
the method further comprises, prior to the formal verification, replacing each of the second data transformation element of the second data transformation pipeline and the other data transformation element of the first data transformation pipeline with a function element, the function element being treated as an unevaluated function of its inputs by a formal verification tool such that during formal verification the function element produces a same set of one or more outputs in response to a same set of one or more inputs.

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

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

18. The method of claim 1 , wherein, when processed at an integrated circu

Assignees

• Imagination Tech Ltd

Inventors

• Elliott Sam

Classifications

• G06F2119/12

  Timing analysis or timing optimisation · CPC title

• G06F30/3323 Primary

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

• G06F30/3308

  using simulation · CPC title

• G06F30/323

  Translation or migration, e.g. logic to logic, hardware description language [HDL] translation or netlist translation · CPC title

• G06F30/367

  Design verification, e.g. using simulation, simulation program with integrated circuit emphasis [SPICE], direct methods or relaxation methods · CPC title