Method and System for Conjunctive BDD Building and Variable Quantification Using Case-Splitting

• US 20080282207A1
• Filed: 05/10/2007
• Published: 11/13/2008
• Est. Priority Date: 05/10/2007
• Status: Active Grant

• Current Assignee: International Business Machines Corporation
• Original Assignee: International Business Machines Corporation
• Inventors: Paruthi, Viresh, Jacobi, Christian, Baumgartner, Jason R., Xu, Jiazhao
• Granted Patent: US 7,739,635 B2
• Time in Patent Office: Days
• US Class Current: 716/4
• CPC Class Codes: G06F 30/3323 using formal methods, e.g. equivalence checking or property checking

Abstract

A method, apparatus and computer-readable medium for conjunctive binary decision diagram building and variable quantification using case-splitting are presented. A BDD building program builds a BDD for at least one node in a netlist graph representation of a circuit design. One or more variables are selected for case-splitting. The variable is set to a constant logical value and then the other. A BDD is built for each case. The program determines whether the variable is scheduled to be quantified out. If so, the program combines the BDDs for each case according to whether the quantification is existential or universal. If the variable is not scheduled to be quantified, the program combines the BDDs for each case so that the variable is introduced back into the resulting BDD, which has a reduced number of peak live nodes.

Claims

1. A method in a computer system for building binary decision diagrams of a circuit design comprising:

building a binary decision diagram for at least one node in a netlist graph representation of a circuit design;

selecting at least one variable for case-splitting from a plurality of variables in said netlist graph representation of a circuit design;

building a first binary decision diagram for the case of said at least one variable having a constant logical value of zero;

building a second binary decision diagram for the case of said at least one variable having a constant logical value of one;

determining whether said at least one variable is scheduled to be existentially quantified, universally quantified, or not quantified at all;

in response to determining that said at least one variable is scheduled to be existentially quantified, building a third binary decision diagram equal to the logical disjunction of said first binary decision diagram and said second binary decision diagram;

in response to determining that said at least one variable is scheduled to be universally quantified, building a third binary decision diagram equal to the logical conjunction of said first binary decision diagram and said second binary decision diagram;

in response to determining that said at least one variable is not scheduled to be quantified, building a third binary decision diagram by logically combining said first binary decision diagram with said second binary decision diagram, whereby said variable is introduced into said third binary decision diagram;

generating said binary decision diagrams in said computer system; and

storing one or more of said binary decision diagrams in a computer-readable medium, whereby said one or more binary decision diagrams has a reduced number of peak live nodes.

2. The method according to claim 1, wherein at least one variable is selected for case-splitting when the step of building a binary decision diagram for at least one node in a netlist graph representation of a circuit design exceeds a predefined resource limit of said computer system.

3. The method according to claim 1, farther comprising:

in response to selecting more than one variable for case-splitting,

storing a state of all live binary decision diagrams for each case-split on a stack in a system memory of said computer system; and

reading said state of all live binary decision diagrams for each case-split from said memory stack in said computer system.

4. The method according to claim 3, wherein the storing and reading steps are performed in a first-in first-out (FIFO) manner.

5. The method according to claim 1, farther comprising:

selecting a variable for a comparison with a reduction threshold, wherein said variable is included in the greatest number of nodes among all live binary decision diagrams;

comparing the reduction of nodes obtained by setting said variable to a constant value with said reduction threshold;

in response to determining that said reduction is greater than said reduction threshold, selecting said variable for case-splitting; and

in response to determining that said reduction is less than said reduction threshold, selecting a different variable for a comparison with said reduction threshold.

6. The method according to claim 5, wherein the step of selecting a variable for case-splitting is biased toward selecting a variable that is scheduled to be quantified out.

7. The method according to claim 1, wherein the step of selecting a variable for case-splitting is biased toward selecting a variable that, when assigned a constant value, results in the reduction of the greatest number of nodes among all live binary decision diagrams.

8. A system for building binary decision diagrams of a circuit design comprising:

a processor;

a data bus coupled to the processor; and

a computer-usable medium embodying computer program code, the computer-usable medium being coupled to the data bus, the computer program code comprising instructions executable by the processor and configured for;

building a binary decision diagram for at least one node in a netlist graph representation of a circuit design;

selecting at least one variable for case-splitting from a plurality of variables in said netlist graph representation of a circuit design;

building a first binary decision diagram for the case of said at least one variable having a constant logical value of zero;

building a second binary decision diagram for the case of said at least one variable having a constant logical value of one;

determining whether said at least one variable is scheduled to be existentially quantified, universally quantified, or not quantified at all;

in response to determining that said at least one variable is scheduled to be existentially quantified, building a third binary decision diagram equal to the logical disjunction of said first binary decision diagram and said second binary decision diagram;

in response to determining that said at least one variable is scheduled to be universally quantified, building a third binary decision diagram equal to the logical conjunction of said first binary decision diagram and said second binary decision diagram;

in response to determining that said at least one variable is not scheduled to be quantified, building a third binary decision diagram by logically combining said first binary decision diagram with said second binary decision diagram, whereby said variable is introduced into said third binary decision diagram; and

storing one or more of said binary decision diagrams in a computer-readable medium, whereby said one or more binary decision diagrams has a reduced number of peak live nodes.

9. The system according to claim 8, wherein at least one variable is selected for case-splitting when the step of building a binary decision diagram for at least one node in a netlist graph representation of a circuit design exceeds a predefined resource limit of said computer system.

10. The system according to claim 8, further comprising:

in response to selecting more than one variable for case-splitting;

storing a state of all live binary decision diagrams for each case-split on a stack in a system memory of said computer system; and

reading said state of all live binary decision diagrams for each case-split from said memory stack in said computer system.

11. The system according to claim 10, wherein the storing and reading steps are preformed in a first-in first-out (FIFO) manner.

12. The system according to claim 8, further comprising:

selecting a variable for a comparison with a reduction threshold, wherein said variable is included in the greatest number of nodes among all live binary decision diagrams;

comparing the reduction of nodes obtained by setting said variable to a constant value with said reduction threshold;

in response to determining that said reduction is greater than said reduction threshold, selecting said variable for case-splitting; and

in response to determining that said reduction is less than said reduction threshold, selecting a different variable for a comparison with said reduction threshold.

13. The system according to claim 12, wherein the step of selecting a variable for case-splitting is biased toward selecting a variable that is scheduled to be quantified out.

14. The system according to claim 8, wherein the step of selecting a variable for case-splitting is biased toward selecting a variable that, when assigned a constant value, results in the reduction of the greatest number of nodes among all live binary decision diagrams.

15. A computer-readable medium encoded with a computer program that, when executed, performs the steps of:

building a binary decision diagram for at least one node in a netlist graph representation of a circuit design;

selecting at least one variable for case-splitting from a plurality of variables in said netlist graph representation of a circuit design;

building a first binary decision diagram for the case of said at least one variable having a constant logical value of zero;

building a second binary decision diagram for the case of said at least one variable having a constant logical value of one;

determining whether said at least one variable is scheduled to be existentially quantified, universally quantified, or not quantified at all;

in response to determining that said at least one variable is scheduled to be existentially quantified, building a third binary decision diagram equal to the logical disjunction of said first binary decision diagram and said second binary decision diagram;

in response to determining that said at least one variable is scheduled to be universally quantified, building a third binary decision diagram equal to the logical conjunction of said first binary decision diagram and said second binary decision diagram;

in response to determining that said at least one variable is not scheduled to be quantified, building a third binary decision diagram by logically combining said first binary decision diagram with said second binary decision diagram, whereby said variable is introduced into said third binary decision diagram;

generating said binary decision diagrams in said computer system; and

storing one or more of said binary decision diagrams in a computer-readable medium, whereby said one or more binary decision diagrams has a reduced number of peak live nodes.

16. The computer-readable medium according to claim 15, wherein at least one variable is selected for case-splitting when the step of building a binary decision diagram for at least one node in a netlist graph representation of a circuit design exceeds a predefined resource limit of said computer system.

17. The computer-readable medium according to claim 15, further comprising:

in response to selecting more than one variable for case-splitting,

storing a state of all live binary decision diagrams for each case-split on a stack in a system memory of said computer system; and

reading said state of all live binary decision diagrams for each case-split from said memory stack in said computer system.

18. The computer-readable medium according to claim 17, wherein the storing and reading steps are performed in a first-in first-out (FIFO) manner.

19. The computer-readable medium according to claim 15, further comprising:

selecting a variable for a comparison with a reduction threshold, wherein said variable is included in the greatest number of nodes among all live binary decision diagrams;

comparing the reduction of nodes obtained by setting said variable to a constant value with said reduction threshold;

in response to determining that said reduction is greater than said reduction threshold, selecting said variable for case-splitting; and

in response to determining that said reduction is less than said reduction threshold, selecting a different variable for a comparison with said reduction threshold.

20. The computer-readable medium according to claim 19, wherein the step of selecting a variable for case-splitting is biased toward selecting a variable that is scheduled to be quantified out.