Verification of Hardware Design for Data Transformation Pipeline with Equivalent Data Transformation Element Output Constraint

• US 20190311075A1
• Filed: 04/03/2019
• Published: 10/10/2019
• Est. Priority Date: 04/05/2018
• Status: Active Grant

• Current Assignee: Imagination Technologies Limited (Imagination Technologies Group Ltd.)
• Original Assignee: Imagination Technologies Limited (Imagination Technologies Group Ltd.)
• Inventors: Elliott, Sam
• Granted Patent: US 10,719,646 B2
• Time in Patent Office: Days
• CPC Class Codes: G01R 31/318357 Simulation computer simulation of digital circuits G06F30/3308
• CPC Class Codes: G06F 2119/12 Timing analysis or timing optimisation
• CPC Class Codes: G06F 30/323 Translation or migration, e.g. logic to logic, hardware description language [HDL] translation or netlist translation
• CPC Class Codes: G06F 30/3308 using simulation
• CPC Class Codes: G06F 30/3323 using formal methods, e.g. equivalence checking or property checking
• CPC Class Codes: G06F 30/367 Design verification, e.g. using simulation, simulation program with integrated circuit emphasis [SPICE], direct methods or relaxation methods
• CPC Class Codes: G06F 30/398 Design verification or optimisation, e.g. using design rule check [DRC], layout versus schematics [LVS] or finite element methods [FEM] optical proximity correction [OPC] design processes G03F1/36

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

Claims

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 circuit manufacturing system, the hardware design for the first data transformation pipeline configures the integrated circuit manufacturing system to manufacture an integrated circuit embodying the first data transformation pipeline.

20. A non-transitory computer readable storage medium having stored thereon computer readable instructions that, when executed at a computer system, cause the computer system to perform the method as set forth in claim 1.

19. A system for 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 system comprising:

memory configured to store;

the hardware design for the first data transformation pipeline;

a hardware design for a second data transformation pipeline, 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; and

a formal verification tool; and

one or more processors configured to;

formally verify, using the formal verification tool, 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 the second data transformation pipeline for a predetermined set of transactions;

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.