Sequential equivalence checking for asynchronous verification

• US 7,882,473 B2
• Filed: 11/27/2007
• Issued: 02/01/2011
• Est. Priority Date: 11/27/2007
• Status: Active Grant

• Current Assignee: Siemens Industry Software Inc. (Siemens AG)
• Original Assignee: International Business Machines Corporation
• Inventors: Ramanandray, Barinjato, Ja, Yee, Paruthi, Viresh, Mony, Hari, Baumgartner, Jason R.
• Primary Examiner(s): Doan; Nghia M
• Application Number:
  US11/945,465
• Publication Number:
  US 20090138837A1
• Time in Patent Office: 1,162 Days
• Field of Search: 716 4- 6, 326 93- 96, 327 1- 3, 327 40- 41, 703 13- 16, 703/19
• US Class Current: 716/106
• CPC Class Codes: G06F 30/3323 using formal methods, e.g. equivalence checking or property checking

Abstract

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

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, by the data processing system, sequential equivalence checking on the first model and second model utilizing the applied one or more exclusive OR operations, wherein the asynchronous crossing logic comprises skewing logic for selecting a phase difference between clocks of asynchronous domains of asynchronous crossings in the unfolded integrated circuit design.

2. The method of claim 1, further comprising:

determining, based on outputs of the one or more exclusive OR operations due to the sequential equivalence checking, whether the asynchronous crossings of the integrated circuit design are verified or not verified; and

generating an output indicative of whether the asynchronous crossings of the integrated circuit design are verified or not verified based on results of the determination.

3. The method of claim 1, wherein the asynchronous crossing logic further comprises, for an asynchronous bus in the unfolded integrated circuit design, transitioning bit detection logic for detecting transitioning bits of strands of the asynchronous bus, and maximum delay logic for determining a maximum delay of strands having transitioning bits in the asynchronous bus.

4. The method of claim 3, wherein inserting the asynchronous crossing logic further comprises:

replicating the second model to generate a third model; and

coupling, for the asynchronous bus in the second model, the maximum delay logic of the second model to random select inputs of the skewing logic associated with a corresponding asynchronous bus in the third model to thereby bypass the random select inputs.

5. 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;

performing sequential equivalence checking on the first model and second model utilizing the applied one or more exclusive OR operations;

determining, based on outputs of the one or more exclusive OR operations due to the sequential equivalence checking, whether the asynchronous crossings of the integrated circuit design are verified or not verified;

generating an output indicative of whether the asynchronous crossings of the integrated circuit design are verified or not verified based on results of the determination; and

performing, by the data processing system, a failure analysis to determine if a failure of the asynchronous crossings is a real failure or a false failure in response to determining that the asynchronous crossings of the integrated circuit design are not verified.

6. The method of claim 5, further comprising:

determining if results of the failure analysis indicate a false failure of the asynchronous crossings; and

generating an output indicating a real failure of the integrated circuit design and a need to modify the integrated circuit design if results of the failure analysis indicate a real failure occurred with the asynchronous crossings of the integrated circuit design.

7. The method of claim 5, further comprising:

determining if results of the failure analysis indicate a false failure of the asynchronous crossings; and

generating an output indicating a false failure of the integrated circuit design and a need to modify the sequential equivalence checking of the first model and second model if results of the failure analysis indicate a false failure occurred with the asynchronous crossings of the integrated circuit design.

8. 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, wherein the asynchronous crossing logic comprises skewing logic for selecting a phase difference between clocks of asynchronous domains of asynchronous crossings in the unfolded integrated circuit design.

9. The apparatus of claim 8, wherein the instructions further cause the processor to:

determine, based on outputs of the one or more exclusive OR operations due to the sequential equivalence checking, whether the asynchronous crossings of the integrated circuit design are verified or not verified; and

generate an output indicative of whether the asynchronous crossings of the integrated circuit design are verified or not verified based on results of the determination.

10. The apparatus of claim 8, wherein the asynchronous crossing logic further comprises, for an asynchronous bus in the unfolded integrated circuit design, transitioning bit detection logic for detecting transitioning bits of strands of the asynchronous bus, and maximum delay logic for determining a maximum delay of strands having transitioning bits in the asynchronous bus.

11. The apparatus of claim 10, wherein inserting the asynchronous crossing logic further comprises:

replicating the second model to generate a third model; and

coupling, for the asynchronous bus in the second model, the maximum delay logic of the second model to random select inputs of the skewing logic associated with a corresponding asynchronous bus in the third model to thereby bypass the random select inputs.

12. 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;

perform sequential equivalence checking on the first model and second model utilizing the applied one or more exclusive OR operations;

determine, based on outputs of the one or more exclusive OR operations due to the sequential equivalence checking, whether the asynchronous crossings of the integrated circuit design are verified or not verified;

generate an output indicative of whether the asynchronous crossings of the integrated circuit design are verified or not verified based on results of the determination; and

perform a failure analysis to determine if a failure of the asynchronous crossings is a real failure or a false failure in response to determining that the asynchronous crossings of the integrated circuit design are not verified.

13. The apparatus of claim 12, wherein the instructions further cause the processor to:

determine if results of the failure analysis indicate a false failure of the asynchronous crossings; and

generate an output indicating a real failure of the integrated circuit design and a need to modify the integrated circuit design if results of the failure analysis indicate a real failure occurred with the asynchronous crossings of the integrated circuit design.

14. The apparatus of claim 12, wherein the instructions further cause the processor to:

determine if results of the failure analysis indicate a false failure of the asynchronous crossings; and

generate an output indicating a false failure of the integrated circuit design and a need to modify the sequential equivalence checking of the first model and second model if results of the failure analysis indicate a false failure occurred with the asynchronous crossings of the integrated circuit design.

15. A computer program product comprising a computer recordable storage device 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, wherein the asynchronous crossing logic comprises skewing logic for selecting a phase difference between clocks of asynchronous domains of asynchronous crossings in the unfolded integrated circuit design.

16. The computer program product of claim 15, wherein the computer readable program further causes the computing device to:

determine, based on outputs of the one or more exclusive OR operations due to the sequential equivalence checking, whether the asynchronous crossings of the integrated circuit design are verified or not verified; and

generate an output indicative of whether the asynchronous crossings of the integrated circuit design are verified or not verified based on results of the determination.

17. The computer program product of claim 15, wherein the asynchronous crossing logic further comprises, for an asynchronous bus in the unfolded integrated circuit design, transitioning bit detection logic for detecting transitioning bits of strands of the asynchronous bus, and maximum delay logic for determining a maximum delay of strands having transitioning bits in the asynchronous bus.

18. The computer program product of claim 17, wherein inserting the asynchronous crossing logic further comprises:

replicating the second model to generate a third model; and

coupling, for the asynchronous bus in the second model, the maximum delay logic of the second model to random select inputs of the skewing logic associated with a corresponding asynchronous bus in the third model to thereby bypass the random select inputs.

19. A computer program product comprising a computer recordable storage device 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;

perform sequential equivalence checking on the first model and second model utilizing the applied one or more exclusive OR operations

determine, based on outputs of the one or more exclusive OR operations due to the sequential equivalence checking, whether the asynchronous crossings of the integrated circuit design are verified or not verified;

generate an output indicative of whether the asynchronous crossings of the integrated circuit design are verified or not verified based on results of the determination; and

perform a failure analysis to determine if a failure of the asynchronous crossings is a real failure or a false failure in response to determining that the asynchronous crossings of the integrated circuit design are not verified.

20. The computer program product of claim 19, wherein the computer readable program further causes the computing device to:

determine if results of the failure analysis indicate a false failure of the asynchronous crossings; and

generate an output indicating a real failure of the integrated circuit design and a need to modify the integrated circuit design if results of the failure analysis indicate a real failure occurred with the asynchronous crossings of the integrated circuit design.

21. The computer program product of claim 19, wherein the computer readable program further causes the computing device to:

determine if results of the failure analysis indicate a false failure of the asynchronous crossings; and

generate an output indicating a false failure of the integrated circuit design and a need to modify the sequential equivalence checking of the first model and second model if results of the failure analysis indicate a false failure occurred with the asynchronous crossings of the integrated circuit design.