Patent ID: 7356747

Claim:
A method for identifying all states of an electronic circuit from which a given target state of the electronic circuit may be reached, the circuit having a plurality of gates and having a plurality of primary inputs, the target state representing an objective, wherein the objective is a given state of at least one of the gates, comprising backtracing from the objective to the primary inputs, comprising a) setting a connectivity value, for each of the gates, to an initial value; b) generating and storing a branch-and-bound decision for reaching the objective from a cut-set; c) generating a new branch-and-bound decision, the generating based on a heuristic selecting gates having higher connectivity with the previously generated and stored branch-and-bound decisions; d) computing a new search subspace corresponding to the new branch-and-bound decision, e) performing a success-driven learning, comprising determining whether or not the new search subspace is equivalent to a previously computed search subspace, the determining including comparing the new cut-set with previously stored cut-sets, and if the determining identifies the new cut-set as being the equivalent of a previously stored cut-set, linking the new search subspace with the previously computed search subspace corresponding to the same previously stored cut-set, f) computing an estimate of a probability of the new cut-set occurring in a subsequent iteration, wherein the estimating includes calculating the product of signal probabilities of specified gates in the cut-set; g) if the computed estimate for the probability meets a given probability threshold, storing the new cut-set, else not storing the new cut-set; h) dynamically updating the connectivity for each gate, by computing the number of paths that connect the gate to the cut-set, if any, formed by the previously generated and stored branch-and-bound decisions, i) repeating steps (b) through (h) until the search is completed; and constructing the decision graph based on the stored cut-sets, the constructed decision graph representing all the solutions computed for the target objective.