Patent Document ID: 20080282207
Application ID: 11746836
Patent Flag: 0

Claim One:
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.