The patent badge is an abbreviated version of the USPTO patent document. The patent badge does contain a link to the full patent document.
The patent badge is an abbreviated version of the USPTO patent document. The patent badge covers the following: Patent number, Date patent was issued, Date patent was filed, Title of the patent, Applicant, Inventor, Assignee, Attorney firm, Primary examiner, Assistant examiner, CPCs, and Abstract. The patent badge does contain a link to the full patent document (in Adobe Acrobat format, aka pdf). To download or print any patent click here.
Patent No.:
Date of Patent:
Jun. 15, 2010
Filed:
May. 10, 2007
Jason R. Baumgartner, Austin, TX (US);
Christian Jacobi, Boblingen, DE;
Viresh Paruthi, Austin, TX (US);
Jiazhao Xu, Mount Kisco, NY (US);
Jason R. Baumgartner, Austin, TX (US);
Christian Jacobi, Boblingen, DE;
Viresh Paruthi, Austin, TX (US);
Jiazhao Xu, Mount Kisco, NY (US);
International Business Machines Corporation, Armonk, NY (US);
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.