Patent ID: 7739635

Claim:
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; storing one or more of said binary decision diagrams in a computer-readable storage device, whereby said one or more binary decision diagrams has a reduced number of peak live nodes; 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.