System and Method for Sequential Equivalence Checking for Asynchronous Verification
First Claim
1. A method, in a data processing system, for performing asynchronous verification of an integrated circuit design, comprising:
- receiving a first model of the integrated circuit design;
unfolding paths within the first model that have asynchronous crossings to generate an unfolded integrated circuit design model;
inserting asynchronous crossing logic into the unfolded integrated circuit design model to generate a second model;
correlating outputs of the first model with outputs of the second model;
applying one or more exclusive OR operations to the correlated outputs of the first model and the second model; and
performing sequential equivalence checking on the first model and second model utilizing the applied one or more exclusive OR operations.
3 Assignments
0 Petitions
Accused Products
Abstract
A system and method for performing sequential equivalence checking for asynchronous verification are provided. A first model of the integrated circuit design is provided that has additional logic in it to reflect the possible variance in behavior of the asynchronous crossings. A second model of the integrated circuit design is provided that does not have this asynchronous behavior logic but instead correlates to the simplest synchronous model that is usually used for non-asynchronous functional verification tasks. Sequential equivalence checking is performed to verify that the two models are input/output equivalent. In order to address non-uniform arrival times of bus strands, logic is provided for identifying bus strands that have transitioning bits, determining a representative delay for these strands, comparing the representative delays for all of the bus strands to determine the maximum delay for the entire bus, and applying this maximum delay to one of the models.
-
Citations
24 Claims
-
1. A method, in a data processing system, for performing asynchronous verification of an integrated circuit design, comprising:
-
receiving a first model of the integrated circuit design; unfolding paths within the first model that have asynchronous crossings to generate an unfolded integrated circuit design model; inserting asynchronous crossing logic into the unfolded integrated circuit design model to generate a second model; correlating outputs of the first model with outputs of the second model; applying one or more exclusive OR operations to the correlated outputs of the first model and the second model; and performing sequential equivalence checking on the first model and second model utilizing the applied one or more exclusive OR operations. - View Dependent Claims (2, 3, 4, 5, 6, 7, 8)
-
-
9. An apparatus, comprising:
-
a processor; and a memory coupled to the processor, wherein the memory comprises instructions which, when executed by the processor, cause the processor to; receive a first model of the integrated circuit design; unfold paths within the first model that have asynchronous crossings to generate an unfolded integrated circuit design model; insert asynchronous crossing logic into the unfolded integrated circuit design model to generate a second model; correlate outputs of the first model with outputs of the second model; apply one or more exclusive OR operations to the correlated outputs of the first model and the second model; and perform sequential equivalence checking on the first model and second model utilizing the applied one or more exclusive OR operations. - View Dependent Claims (10, 11, 12, 13, 14, 15, 16)
-
-
17. A computer program product comprising a computer recordable medium having a computer readable program, wherein the computer readable program, when executed on a computing device, causes the computing device to:
-
receive a first model of the integrated circuit design; unfold paths within the first model that have asynchronous crossings to generate an unfolded integrated circuit design model; insert asynchronous crossing logic into the unfolded integrated circuit design model to generate a second model; correlate outputs of the first model with outputs of the second model; apply one or more exclusive OR operations to the correlated outputs of the first model and the second model; and perform sequential equivalence checking on the first model and second model utilizing the applied one or more exclusive OR operations. - View Dependent Claims (18, 19, 20, 21, 22, 23, 24)
-
Specification