Verification of Hardware Design for Data Transformation Pipeline with Equivalent Data Transformation Element Output Constraint
First Claim
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 Assignments
0 Petitions
Accused Products
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).
-
Citations
20 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. - View Dependent Claims (2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 20)
-
-
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.
-
Specification