Solving constraint satisfiability problem for circuit designs

• US 7,073,143 B1
• Filed: 10/24/2001
• Issued: 07/04/2006
• Est. Priority Date: 11/06/2000
• Status: Active Grant

• Current Assignee: Cadence Design Systems Incorporated (Cadence Group)
• Original Assignee: Cadence Design Systems Incorporated (Cadence Group)
• Inventors: Huang, Chung-Yang
• Primary Examiner(s): THOMPSON, ANNETTE M
• Application Number:
  US10/029,596
• Time in Patent Office: 1,714 Days
• Field of Search: 716/5, 716/6, 716/12, 716/4, 703/14, 703/15
• US Class Current: 716/106
• CPC Class Codes: G06F 30/3323 using formal methods, e.g. equivalence checking or property checking

Abstract

A method for generating a test vector for functional verification of circuits includes providing a representation of a circuit, where the representation includes a control logic component and a datapath logic component. The method also includes reading one or more vector generation targets, and performing word-level ATPG justification on the control logic component to obtain a control logic solution. The method further includes extracting one or more arithmetic functions for the datapath logic component based on the control logic solution, and solving the one or more arithmetic functions using a modular constraint solver. The modular constraint solver is based on a modular number system.

Claims

1. A method for performing assertion checking for functional verification of circuits comprising:

providing a representation of a circuit, the representation comprising a control logic component and a datapath logic component;

reading one or more vector generation targets;

performing word-level ATPG justification on the control logic component to obtain a control logic solution;

extracting one or more arithmetic functions for the datapath logic component based on the control logic solution; and

solving the one or more arithmetic functions using a modular constraint solver, the modular constraint solver being based on a modular number system.

2. The method of claim 1, wherein the word-level ATPG justification comprises performing word-level implication on circuit components related to the one or more vector generation targets.

3. The method of claim 1, wherein solving the one or more arithmetic functions comprises:

determining possible solutions for one or more nonlinear equations; and

solving one or more linear equations using one possible solution for the one or more nonlinear equations as boundary conditions.

4. The method of claim 1 further comprising:

dependent on the outcome of solving the one or more arithmetic functions, backtracking to perform word-level ATPG justification on the control logic component to obtain a second control logic solution;

extracting one or more arithmetic functions for the datapath logic component based on the second control logic solution; and

solving the one or more arithmetic functions using the modular constraint solver.

5. The method of claim 1, wherein at least one vector generation target comprises a signal value.

6. The method of claim 1, wherein at least one vector generation target comprises a relation among a set of signals.

7. The method of claim 1, wherein at least one vector generation target comprises a sequence of relations among a set of signals.

8. A computer-readable storage medium having stored thereon computer instructions that, when executed by a computer, cause the computer to:

provide a representation of a circuit, the representation comprising a control logic component and a datapath logic component;

read one or more vector generation targets;

perform word-level ATPG justification on the control logic component to obtain a control logic solution;

extract one or more arithmetic functions for the datapath logic component based on the control logic solution; and

solve the one or more arithmetic functions using a modular constraint solver, the modular constraint solver being based on a modular number system.

9. The computer-readable storage medium of claim 8, wherein the computer instructions that perform word-level ATPG justification further comprise computer instructions that, when executed by a computer, cause the computer to perform word-level implication on circuit components related to the one or more vector generation targets.

10. The computer-readable storage medium of claim 8, wherein the computer instructions that solve the one or more arithmetic functions further comprise computer instructions that, when executed by a computer, cause the computer to:

determine possible solutions for one or more nonlinear equations; and

solve one or more linear equations using one possible solution for the one or more nonlinear equations as boundary conditions.

11. The computer-readable storage medium of claim 8, wherein the computer instructions that solve the one or more arithmetic functions further comprise computer instructions that, when executed by a computer, cause the computer to:

dependent on the outcome of solving the one or more arithmetic functions, backtrack to perform word-level ATPG justification on the control logic component to obtain a second control logic solution;

extract one or more arithmetic functions for the datapath logic component based on the second control logic solution; and

solve the one or more arithmetic functions using the modular constraint solver.

12. The computer-readable storage medium of claim 8, wherein at least one vector generation target comprises a signal value.

13. The computer-readable storage medium of claim 8, wherein at least one vector generation target comprises a relation among a set of signals.

14. The computer-readable storage medium of claim 8, wherein at least one vector generation target comprises a sequence of relations among a set of signals.

15. The computer-readable storage medium of claim 8, wherein the word-level ATPG justification is performed by performing a word-level implication, the word-level implication comprising a decision on at least one control signal.

16. The computer-readable storage medium of claim 15, wherein the word-level implication is performed on the at least one control signal.

17. The computer-readable storage medium of claim 8, further comprising computer instructions that, when executed by a computer, cause the computer to:

extract one or more arithmetic functions based on the ATPG justification; and

solve the one or more arithmetic functions using the modular constraint solver.

18. A system for performing assertion checking for functional verification of circuits comprising:

means for providing a representation of a circuit, the representation comprising a control logic component and a datapath logic component;

means for reading one or more vector generation targets;

means for performing word-level ATPG justification on the control logic component to obtain a control logic solution;

means for extracting one or more arithmetic functions for the datapath logic component based on the control logic solution; and

means for solving the one or more arithmetic functions using a modular constraint solver, the modular constraint solver being based on a modular number system.

19. The system of claim 18, wherein the means for performing the word-level ATPG justification comprises means for performing word-level implication on circuit components related to the one or more targets.

20. The system of claim 18, wherein the means for solving the one or more arithmetic functions comprises:

means for determining possible solutions for one or more nonlinear equations; and

means for solving one or more linear equations using one possible solution for the one or more nonlinear equations as boundary conditions.

21. The system of claim 18, further comprising:

dependent on the outcome of solving the one or more arithmetic functions, means for backtracking to perform word-level ATPG justification on the control logic component to obtain a second control logic solution;

means for extracting one or more arithmetic functions for the datapath logic component based on the second control logic solution; and

means for solving the one or more arithmetic functions using the modular constraint solver.

22. The method of claim 18, wherein at least one vector generation target comprises a signal value.

23. The method of claim 18, wherein at least one vector generation target comprises a relation among a set of signals.

24. The method of claim 18, wherein at least one vector generation target comprises a sequence of relations among a set of signals.