Method and system for verification of circuits with encoded signals

• US 7,627,842 B1
• Filed: 06/01/2004
• Issued: 12/01/2009
• Est. Priority Date: 06/03/2003
• Status: Active Grant

• Current Assignee: Cadence Design Systems Incorporated (Cadence Group)
• Original Assignee: Cadence Design Systems Incorporated (Cadence Group)
• Inventors: Lin, Chih-Chang, Khoo, Kei-Yong
• Primary Examiner(s): Chiang; Jack
• Assistant Examiner(s): Tat; Binh C
• Application Number:
  US10/859,465
• Time in Patent Office: 2,009 Days
• Field of Search: 716/1, 716 3- 6
• US Class Current: 716/106
• CPC Class Codes: G06F 30/33 Design verification, e.g. functional simulation or model checking

Abstract

Disclosed are techniques for performing the verification of circuits where corresponding signals in the circuits or specifications are encoded differently and/or redundancy occurs in the signals. Verification, such as logic equivalence checking of circuits, can be performed where the corresponding signals in the two circuits are encoded differently, and/or redundancy occurs in the signals.

Claims

1. A computer implemented method for verifying a circuit design, the circuit design having a portion corresponds to an encoded carry-save signal, comprising:

decoding by a decoder the encoded carry-save signal to produce a decoded carry-save signal;

determining a correspondence between the decoded carry-save signal of the circuit design and a second signal of a second circuit design;

comparing by a processor the decoded carry-save signal to the second signal to perform verification upon the circuit design, in which decoding logic and encoding logic are inserted into one or more paths of the carry-save signal, in which the decoding logic and the encoding logic are explicitly inserted by an actual modification to a circuit representation of the circuit design or are implicitly inserted without actual modification to the circuit representation of the circuit design but causing realization of the encoding and the decoding logics; and

storing the decoded carry-save signal in a volatile or non-volatile computer readable medium or displaying the decoded carry-save signal on a display device.

2. The method of claim 1 in which two vectors are used to represent one arithmetic value for the encoded carry-save signal.

3. The method of claim 1 in which the act of decoding the encoded carry-save signal is performed using a logic function, addition function or look-up table from an encoding table.

4. The method of claim 1 in which the decoded carry-save signal is re-encoded.

5. The method of claim 4 in which one or more pseudo inputs are employed to perform the action of re-encoding the decoded carry-save signal.

6. The method of claim 4 in which the re-encoded signal is represented by two vectors.

7. The method of claim 6, further comprising:

generating carry-save vectors as (X-P, P) where P is an N-bit pseudo input, where X-P and P are the two vectors, and X is the decoded carry-save signal.

8. The method of claim 5 in which the one or more pseudo inputs are unmapped.

9. The method of claim 8 in which the method is performed in the framework of formal equivalence checking.

10. The method of claim 9 in which circuits are shown to be formally shown to be equivalent when key-points in the circuits can be proven to be equivalent when the one or more pseudo-inputs are redundant.

11. The method of claim 1 further comprising:

identifying the encoded carry-save signal either automatically or manually by a user.

12. The method of claim 1 in which correspondence is identified between the decoded signal of the circuit design to be verified.

13. The method of claim 12 in which correspondences found between key-points in the circuit design.

14. The method of claim 13 in which the key-points comprise boundary points.

15. The method of claim 1 in which pseudo signals produced by decoding logic is left as free-variables to formal checking algorithms.

16. The method of claim 1 in which the second signal is another encoded signal that is decoded before performing the act of comparing.

17. A computer implemented method for verifying a circuit design, the circuit design having a portion corresponds to an encoded signal, comprising:

decoding by a decoder the encoded signal to produce a decoded signal;

determining by a processor a correspondence between the decoded signal of the circuit design and a second signal of a second circuit design;

comparing the decoded signal to the second signal to perform verification upon the circuit design, in which decoding logic and encoding logic are inserted into one or more paths of the carry-save signal, in which the decoding logic and the encoding logic are explicitly inserted by an actual modification to a circuit representation of the circuit design or are implicitly inserted without actual modification to the circuit representation of the circuit design but causing realization of the encoding and the decoding logics; and

storing the decoded signal in a volatile or non-volatile computer readable medium or displaying the decoded signal on a display device.

18. The method of claim 17 in which the act of decoding the encoded signal is performed using a logic function, addition function or a look-up table from an encoding table.

19. The method of claim 17 in which the act of decoding realizes a mapping from an encoded signal pattern to a decoded signal pattern.

20. The method of claim 17 in which a determination is made whether the encoded signal is in error.

21. The method of claim 20 in which a completed encoding function indicates no error.

22. The method of claim 17 in which the decoded signal is re-encoded.

23. The method of claim 22 in which one or more pseudo inputs are employed to perform the action of re-encoding the decoded signal.

24. The method of claim 23 in which the one or more pseudo inputs are unmapped.

25. The method of claim 24 in which the method is performed in the framework of formal equivalence checking.

26. The method of claim 25 in which circuits are shown to be formally shown to be equivalent when key-points in the circuits can be proven to be equivalent when the one or more pseudo-inputs are redundant.

27. The method of claim 22 in which encoding logic is employed to realizes a mapping from a decoded signal pattern to an encoded signal pattern.

28. The method of claim 27 in which, if an encoding function ƒ

is redundant, a single input pattern to the encoding logic is mapped to multiple patterns at an output of the encoding logic.

29. The method of claim 27 in which the encoding logic has one or more pseudo inputs that are used to select possible output patterns.

30. The method of claim 29 in which all possible patterns are applied to the one or more pseudo inputs.

31. The method of claim 17 in which verification is performed of the circuit design against a specification.

32. The method of claim 20 in which the modification is performed as either a permanent or temporary modification.

33. The method of claim 17 in which correspondence is identified between the decoded signal of the circuit design to be verified.

34. The method of claim 33 in which correspondences found between key-points in the circuit design.

35. The method of claim 34 in which the key-points comprise boundary points.

36. The method of claim 17 in which pseudo signals produced by decoding logic is left as free-variables to formal checking algorithms.

37. The method of claim 17 in which the second signal is another encoded signal that is decoded before performing the act of comparing.

38. The method of claim 17 in which multiple nested levels of encoding and decoding are performed to verify the circuit design.

39. The method of claim 17 in which a comparison is performed between one or more Boolean functions of the encoded signal and the decoded signal.

40. The method of claim 17 in which a comparison is performed between one or more Boolean functions of two encoded signals using the same encoding function.

41. The method of claim 17 in which a comparison is performed between one or more Boolean functions of two encoded signals using different encoding functions.

42. A volatile or non-volatile computer usable medium comprising instructions for performing a process by a processor for verifying a circuit design, the circuit design having a portion corresponds to an encoded carry-save signal, the process comprising the acts of:

decoding by a decoder the encoded carry-save signal to produce a decoded carry-save signal;

determining a correspondence between the decoded carry-save signal of the circuit design and a second signal of a second circuit design;

comparing the decoded carry-save signal to the second signal to perform verification upon the circuit design, in which decoding logic and encoding logic are inserted into one or more paths of the carry-save signal, in which the decoding logic and the encoding logic are explicitly inserted by an actual modification to a circuit representation of the circuit design or are implicitly inserted without actual modification to the circuit representation of the circuit design but causing realization of the encoding and the decoding logics; and

storing the decoded carry-save signal or displaying the decoded carry-save signal on a display device.

46. The method of claim 42 in which two vectors are used to represent one arithmetic value for the encoded carry-save signal.

43. A system for verifying a circuit design, the circuit design having a portion corresponds to an encoded carry-save signal, the system comprising:

a decoder for decoding the encoded carry-save signal to produce a decoded carry-save signal;

means for determining a correspondence between the decoded carry-save signal of the circuit design and a second signal of the second circuit design;

a processor for comparing the decoded carry-save signal to the second signal to perform verification upon the circuit design, in which decoding logic and encoding logic are inserted into one or more paths of the carry-save signal, in which the decoding logic and the encoding logic are explicitly inserted by an actual modification to a circuit representation of the circuit design or are implicitly inserted without actual modification to the circuit representation of the circuit design but causing realization of the encoding and the decoding logics; and

a volatile or non-volatile computer readable medium for storing the decoded carry-save signal or a display device for displaying the decoded carry-save signal.

47. The system of claim 43 in which two vectors are used to represent one arithmetic value for the encoded carry-save signal.

44. A volatile or non-volatile computer usable medium comprising instructions for performing a process by a processor for verifying a circuit design, the circuit design having a portion corresponds to an encoded signal, the process comprising the acts of:

decoding by a decoder the encoded signal to produce a decoded signal;

determining a correspondence between the decoded signal of the circuit design and a second signal of the second circuit design;

comparing the decoded signal to the second signal to perform verification upon the circuit design, in which decoding logic and encoding logic are inserted into one or more paths of the carry-save signal, in which the decoding logic and the encoding logic are explicitly inserted by an actual modification to a circuit representation of the circuit design or are implicitly inserted without actual modification to the circuit representation of the circuit design but causing realization of the encoding and the decoding logics, and

storing the decoding signal or displaying the decoder signal on a display device.

48. The method of claim 44, further comprising employing one or more pseudo inputs to re-encode the decoded signal, in which the one or more pseudo inputs are unmapped.

45. A system for verifying a circuit design, the circuit design having a portion corresponds to an encoded signal, the system comprising:

a decoder for decoding the encoded signal to produce a decoded signal;

a processor for determining correspondence between the decoded signal of the circuit design and a second signal of the second circuit design;

means for comparing the decoded signal to the second signal to perform verification upon the circuit design, in which decoding logic and encoding logic are inserted into one or more paths of the carry-save signal, in which the decoding logic and the encoding logic are explicitly inserted by an actual modification to a circuit representation of the circuit design or are implicitly inserted without actual modification to the circuit representation of the circuit design but causing realization of the encoding and the decoding logics; and

a volatile or non-volatile computer readable medium for storing the decoded carry-save signal or a display device for displaying the decoded carry-save signal.

49. The system of claim 45, further comprising logic for employing one or more pseudo inputs to re-encode the decoded signal, in which the one or more pseudo inputs are unmapped.