Ordering binary decision diagrams used in the formal equivalence verification of digital designs
AssigneeIntel Corporation
InventorSreenath Kurupati
Life of this patent
Estimating the term…
Abstract
A method for ordering input variables in binary decision diagrams is described. Once a plurality of disjoint sets of input variables can be found from the sub-equations of a Boolean function, an initial top-level order can be used to form a significantly smaller diagram. The diagram can by reduced further by application of the method recursively on the sub-equations and successive sub-equations until primary inputs are reached.
Claims24
A method of ordering input variables in a binary decision diagram (BDD) representing a Boolean function, comprising:
- performing a search within said Boolean function for first and second sub-equations with first and second disjoint sets of said input variables;
- performing a search for common input variables from said first and second disjoint sets of input variables;
- removing found common input variables from said first and second disjoint sets of input variables;
- and
- building an order of said input variables based on said disjoint sets and said found common input variables.
A method of ordering input variables in a binary decision diagram (BDD) representing a Boolean function, comprising:
- performing a search within said Boolean function for first and second sub-equations with first and second sets of said input variables;
- creating a set of common input variables from said first and second sub-equations;
- removing said common inputs from said first and second sets of input variables to form first and second disjoint sets;
- and
- building an order of said input variables based on said common input variables set and said first and second disjoint sets.
A set of instructions residing in a storage medium, said set of instructions capable of being executed by a processor to implement a method to order input variables in a binary decision diagram (BDD) representing a Boolean function, the method comprising:
- performing a search within said Boolean function for first and second sub-equations with first and second disjoint sets of said input variables;
- performing a search for common input variables from said first and second disjoint sets of input variables;
- removing found common input variables from said first and second disjoint sets of input variables;
- and
- building an order of said input variables based on said disjoint sets and said found common input variables.
A set of instructions residing in a storage medium, said set of instructions capable of being executed by a processor to implement a method to order input variables in a binary decision diagram (BDD) representing a Boolean function, the method comprising:
- performing a search within said Boolean function for first and second sub-equations with first and second sets of said input variables;
- creating a set of common input variables from said first and second sub-equations;
- removing said common inputs from said first and second sets of input variables to form first and second disjoint sets;
- and
- building an order of said input variables based on said common input variables set and said first and second disjoint sets.
Dependencies are inferred from the claim text.