Patent ID: 6026222
Filing Date: 2000-02-15
Classification: G06F

Abstract:
A method for determining non-equivalence between two combinational circuits comprising:combining the two combinational circuits into a miter circuit;partitioning the miter circuit along a boundary which separates each of the two combinational circuits into a respective fanin partition and a respective fanout partition, the two combinational circuits having variables including a set of cutset variables defined by the boundary;defining a binary decision diagram for the respective fanout partitions, the binary decision diagram having a respective binary decision diagram onset;defining a set of Boolean satisfiability clauses for the respective fanin partitions, the Boolean satisfiability clauses having the cutset variables as an output, the binary decision diagram having the cutset variables as an input;performing Boolean satisfiability checking to find satisfiability solutions for the set of Boolean satisfiability clauses, including bounding values to the variables included in the set of Boolean satisfiability clauses to define currently bound variables;whenever one of the variables bound to a value is one of the set of cutset variables, checking the values of the currently bound ones of the set of cutset variables to make a determination as to whether the values of the currently bound ones of the set of cutset variables have a non-null intersection with the binary decision diagram onset;proceeding forward in the performing of the Boolean satisfiability checking when the determination indicates the non-null intersection; andbacktracking in the performing of the Boolean satisfiability checking when the determination indicates the null intersection.