Method and system for non-linear state based satisfiability

1. A computerized method for utilizing at least one state machine to solve a non-linear Boolean equation comprising:

partially solving said non-linear Boolean equation to determine at least one pre-computed search inference relating to said non-linear Boolean equation;

storing at least one precomputed search inference relating to said Boolean equation in said at least one state machine;

accessing said at least one search inference from said state machine to develop at least one heuristic for solving said non-linear Boolean equation;

iteratively searching for a solution to said equation by utilizing at least one heuristic developed from said at least one inference stored in said state machine.

2. A method as claimed in claim 1 wherein said non-linear Boolean equation is translated into a set of functions and wherein said functions are represented in a Binary Decision Diagram and further wherein said partial solving step comprises solving each function in said set of functions for all possible inputs.

3. A method as claimed in claim 1 further including the steps of computing a score for each of said at least one inference wherein said score is stored and associated with said at least one inference and wherein said score indicates a desirability of using said associated inference in said determining step.

4. A method as claimed in claim 3 wherein a set of heuristics is developed from said at least one inference in an order according to said score associated with said at least one inference.

5. A method as claimed in claim 1 wherein said state machine comprises at least one inference for a user domain relating to said non-linear Boolean equation.

6. A method as claimed in claim 5 wherein said state machine further comprises a computer readable data storage location for storing any linear inferences developed in said partial solving step.

7. A method as claimed in claim 1 wherein said state machine utilizes a technique selected from a group of autarkies, lemmas, and/or pruning to reduce a set of inferences associated with a user domain associated with said non-linear Boolean function.

8. A computerized method for verifying that a circuit expression for a microprocessor matches a specification associated with said microprocessor comprising:

transforming said specification into a conjunction of logical expressions;

combining said conjunction with said circuit expression to produce a verification equation;

analyzing said verification equation via a Binary Decision Diagram;

partitioning said verification equation into a set of functions representing said verification equation;

processing each function in said set of functions for all possible inputs;

storing at least one inference developed from said processing step in a state machine;

iteratively searching for a solution to said equation by utilizing at least one heuristic developed from said at least one inference stored in said state machine.

9. A method as claimed in 8 wherein said searching step does not comprise translating said equation into Conjunctive Normal Format.

10. A computer system for solving a non-linear Boolean equation comprising a pre-processor, a state machine and a search engine wherein

A. said pre-processor is configured to perform the steps of

1. translating said Boolean equation into a set of functions;

2. solving said set of functions for all possible inputs;

B. said state machine is configured to store a set of at least one inferences developed from said solving step wherein said inferences are associated with a respective function in said set of functions;

C. a search engine configured to search for a solution to said Boolean equation using a set of heuristics developed from said set of inferences.