US 6,912,700 B1Grant

Method and system for non-linear state based satisfiability

Issue Date:2005-06-28

•10 Claims

•9 Drawing Sheets

Abstract

A computerized method and system for solving non-linear Boolean equations is disclosed comprising at least partially solving a Boolean function; developing at least one inference regarding said Boolean function and saving said inference to a state machine; and accessing said inference from said state machine to develop at least one heuristic for determining whether said Boolean function is satisfiable.

Metadata

Assignees

The United States of America as represented by the National Security Agency
The University of Cincinnati

Inventors

John V. Franco
W. Mark VanFleet
John Schlipf
Michael R. Dransfield

Application Information

Application Number:US 10/164,203

Filing Date:2002-06-06

Priority Date:2001-06-06

Art Unit:2825

Patent Drawings (9 sheets)

Description

Preamble

[0001] This application is based upon, claims priority from, and incorporates by reference the entirety of the provisional application Ser. No. 60/296,380, Franco, et al, filed Jun. 6, 2001.

Field of Invention

[0002] The present invention relates generally to a computerized system for the design and testing of integrated circuits, other complex devices and systems, the evaluation of software systems, solving non-linear systems of Boolean equations, and more particularly to computer program comprising instructions for implementing satisfiability algorithms involving such devices and systems.

Background

[0003] In math and physics, “linear” means “simple” and “non-linear” means “complicated”. The theory for solving linear equations is very well developed because it is simple enough to solve and only one solution exists. Non-linear equations can in general not be solved exactly (they have multiple solutions) and are the subject of much on-going research. Here is a brief description of how to distinguish a linear equation from a non-linear equation: In a linear equation, the variables (and their derivatives) must always appear as a simple first power. Here are some simple examples to illustrate this principle:

[0004] x+5=10 is linear and the equation is satisfied if and only if x takes the value 5. On the other hand, 5+x²=6 is non-linear because x²is not a first power. The solution to this equation entails two values for x, namely −1 and +1 and this solution is harder to find than in the previous case.

[0005] In Boolean logic, equations have an analogous meaning but the operations of or (denoted ) and and (denoted ^) replace the operations of plus (denoted +) and times (denoted x), the connective ≡replaces the connective =, and Boolean variables can only take two values, namely true (also referred to as value 1) and false (also referred to as value 0), instead of any number as in the case of mathematics and physics. Analogously, non-linear Boolean equations are far harder to solve than linear Boolean equations and often, if there is one solution, there are many solutions.

[0006] There are two current competing methods for solving systems of non-linear Boolean equations. The first is via the use of Binary Decision Diagrams (BDDs). The second, is via Conjunctive Normal Form (CNF) Satisfiability checkers, e.g., POSIT, GRASP, zCHAFF, SATO, WALKSAT, etc. A BDD is intended as a compact representation of a Boolean function. A Boolean function has several input variables and one output variable. Every input variable may either be independently assigned value 0 or 1 or may be left unassigned. The output takes either value 0 or 1 or has undetermined value depending on the values assigned to the input variables. The input assignment patterns causing the output to have value 0 or 1 or undetermined may be listed in a table called a truth table. A truth table corresponds uniquely to a particular Boolean function.

[0007] A BDD is a mathematical abstraction which describes a truth table in an alternative and compact form. A BDD consists of a number of nodes, one distinguished as the root, one as the 0 node and one as the 1 node, representing function variable values, and arcs leading away from nodes, except the 0 and 1 nodes, representing values given to input variables. In this formalism 0 represents false and 1 represents true. The 0 and 1 nodes together represent the 0 and 1 values, respectively, which the function may take. A path from root to the 1 node signifies an assignment of values to input variables which causes the function's output variable to have value true and a path to the 0 node signifies an assignment causing an output value of false. Principal attributes of BDDs leading to their wide use are: 1) a BDD can be a compact, efficiently computed representation for a Boolean function and 2) operations for combining BDDs, such as conjunction (the operator), can be fairly efficient provided the number of nodes in the resulting BDD is not great.

[0008] BDDs are typically applied to non-linear equations as follows. A non-linear equation is a Boolean function. Variables named in a non-linear equation are its input variables. Thus, each equation may be represented by a BDD. Solving a system of non-linear equations means finding an assignment of values to all variables named in the system which causes each equation to have value 1. An equation, which has value 1, due to an assignment, is satisfied by that assignment. Since a system of non-linear equations is a Boolean function, a system may be solved if its corresponding BDD can be computed. Starting from the easily computed BDDs for each equation and using the rich set of operations available to BDDs, a BDD solver combines BDDs until one is left: that which represents the entire system. If that point can be reached, the system is solved. Observe that purely BDD techniques involve no guessing and checking of assignments.

[0009] By contrast, Satisfiability checkers, or SAT solvers, solve a restricted class of non-linear Boolean equations referred to as CNF formulas (see below for a description) by guessing, checking, discarding, and guessing again input variable values until either all possible combinations are exhausted or until an assignment is found which satisfies all equations. A SAT solver starts with all variables unassigned and attempts to extend the set of currently assigned input variables, one at a time, until it can be determined that all equations are satisfied or that all possible assignments to remaining unassigned variables will not satisfy all equations. In the former case a satisfying solution to the system is found. In the latter case one or more of the last variables to be assigned are reassigned or unassigned and the search for satisfying extensions is continued. If all possible extensions from the starting case, where all variables are unassigned, fail to satisfy all equations then the SAT solver reports no satisfying solution is possible.

[0010] BDD solvers are limited in the size of problems that they can solve, e.g., hundreds of variables and thousands of equations, depending on the problem domain. The principle problem plaguing BDD solvers is that as BDDs are being combined, they can get extremely large before completion, even if the final BDD is very small.

[0011] SAT solvers can solve problems with tens of thousands of variables and hundreds of thousands of equations, depending again on the problem domain. However, good performance seems to depend heavily on search heuristics, which choose the order in which variables are assigned values. Heuristics pertain to a trial-and-error method of problem solving used when an algorithmic approach is impractical. But the management of highly intelligent heuristics requires a great deal of overhead using conventional data structures and high overhead cancels the potential gains offered by such heuristics.

[0012] BDD and SAT solvers have (separately) been applied to a variety of problems. Many of these are a subclass of a general class of expressions called Layered Boolean Formulas (LBF).

[0013] A formula is one of the LBF class of expressions if it is given as 1) a list F={f₁, f₂, . . . f_m} of m Boolean functions whose inputs are taken from a set V={ν₁, ν₂, . . . , ν_n}of n Boolean variables; and 2) a list O=<o₁, o₂, . . . , o_m> of m Boolean values, one for each function, which specify the values the functions' outputs need to have if the expression is considered satisfied. The problem that needs to be solved, given an LBF Ø, is to determine whether there exists a list of Boolean values <b₁, b₂, . . . , b_n> which the variables of V can be set to (that is, variable ν_itakes value b_ifor all 1≦i≦n) to satisfy the expression Ø (that is, makes all function outputs of F consistent with O) and if such a list exists (called a solution) output one.

[0014] The LBF class of expressions includes Conjunctive Normal Form (CNF) formulas, some Quantified Boolean Formulas (QBF), and Trace formulas. In a CNF formula each Boolean function fi is a disjunction of Boolean variables and complemented Boolean variables (a complemented Boolean variable just has a value opposite that of its variable counterpart) and each oi is 1. For example, f1 might be expressed as v1v3v8 which is a disjunction of two variables and one complemented variable (v3) and has value 0 if v1 and v8 have value 0 and v3 has value 1; has value 1 if v1 or v8 have value 1 or v3 has value 0; and has undetermined value otherwise. Boolean functions in a Trace formula typically use the equivalence operator ≡ and a few other operators such as ite which means if-then-else. For example, f1 of a Trace formula might be expressed as
ν≡ite(ν₁, ν₂, ν₃);
This function has value 0 if either

- [0015] 1) ν₁and ν₃have value 0 and ν has value 1; or
- [0016] 2) ν₁and ν have value 0 and ν₃has value 1; or
- [0017] 3) ν₁and ν₂have value 1 and ν has value 0; or
- [0018] 4) ν₁and ν have value 1 and ν₂has value 0.
  It has value 1 if either
- [0019] 1) ν₁and ν₃have value 0 and ν has value 0; or
- [0020] 2) ν₁has value 0 and ν₃and ν have value 1; or
- [0021] 3) ν₁and ν₂have value 1 and ν has value 1; or
- [0022] 4) ν₁has value 1 and ν₂and ν have value 0.
  It has undetermined value otherwise.

[0023] A QBF expression is more complicated. Instead of asking whether the exists a list of Boolean values that satisfy Ø, the problem is to ask whether, for every possible combination of values that some of the V variables can have, there exists some combination of values that the remaining V variables can have with the result that Ø is satisfied, and if so, what is one such combination of values.

[0024] Before the 1990s, Binary Decision Diagrams (or BDDs) were considered the best way to deal with LBFs arising from some classes of practical problems. Unfortunately, on real LBFs, the number of nodes of “intermediate” BDDs (those that are formed while combining BDDs) can get to be enormous before realizing the final BDD which solves the problem and which can be quite small.

[0025] An alternative is to convert the BDDs to a conjunction of clauses, that is expressions which are conjunctions of terms of the form s₁s₂s₃and solve the conjunction of all conjunctions of clauses using a SAT solver. Before the 1990s this was infeasible because SAT solvers performed a form of tree search, that is SAT solvers did not effectively remember and reuse what had been learned in early parts of the search process. This sharply contrasts with BDDs which reuse portions of paths leading to the 1 node and 0 node, respectively. But the 1990s saw major improvements in the design of SAT solvers including conflict resolution, a form of remembering learned facts which we call lemmas, lookahead for inferences, better search heuristics, and exploitation of problem symmetry to prune away large portions of the search space. With these improvements SAT solvers can now compete with and in some cases significantly exceed the performance of BDD tools.

[0026] Formulas such as these arise in a variety of formal verification problems including microprocessor verification, illegal transition checking, and interconnect synthesis, among others. Consider microprocessor verification first. A circuit for use in a computer or other electronic device is designed from a formal specification of its functionality. This specification is written in some human understandable form such as make a noise at noon on cloudy days only. But an implementation of this statement as a circuit must be in a machine understandable form involving input and output variables. For example, let time represent time-of-day, let weather represent a type of weather condition, let noise represent whether a noise is made. Then the circuit to build may be expressed
noise≡(time=12:00)^(weather=cloudy).

[0027] The output of this circuit has either logic value true or false depending on the values of its input variables, namely noise time and weather. For a example, if input values are sunny for weather, 12:00 for time, and true for noise, then the circuit outputs false. Observe that a formal specification may also have a logic value of true or false depending on some conditions. For example, the specification above has value false if a noise is made on a sunny day. If a circuit is to function as expected, its output logic values must be consistent with the logic values of the associated specification for corresponding input variable/specification conditions, that is, the specification and the circuit design should be functionally equivalent.

[0028] The microprocessor verification problem is to prove, using a computer program, that a given formal specification is logically equivalent to a given circuit expression. This is accomplished by using a special language for writing specifications which can efficiently be transformed into a conjunction of logic expressions. To determine whether the conjunction of expressions, S, is fictionally equivalent to a circuit design, D, the expressions representing D and S are combined as follows:
(D^S)(D^S)

[0029] This equivalence expression always has value false if and only if D and S are functionally equivalent.

[0030] An effective SAT solver (computer program) checks a minimal number of possible combinations of input values that is sufficient to completely determine whether a given equivalence expression always has value false. But all SAT solvers operate on CNF formulas. Thus, equivalence expressions must be translated to CNF before being solved by a SAT solver. Translation has two undesirable side-effects: 1) the length of the equivalence expression in CNF may be much greater; 2) variables which are understood in the context of the equivalence expression may lose that property as they become scattered in the translation. Continuing with the above example, consider attempting to show that
noise≡(time=12:00)^(weather=cloudy)
is equivalent to
noise≡ite(weather=cloudy, time=12:00, weather=cloudy)

[0031] The later expression may have come from the special formal specification language. Current solvers cannot directly deal with the equivalence expression. Rather, a straightforward translation of the equivalence expression to CNF might give
(noise(time=12:00)(weather =cloudy))^
(noise(time=12:00)(weather=cloudy))^
(noise(time=12:00)(weather=cloudy))^
(noise(time=12:00)(weather=cloudy))^
(noise(time=12:00)(weather=cloudy))^
(noise(time=12:00)(weather=cloudy))^
(noise(time=12:00)(weather=cloudy))^
(noise(time=12:00)(weather=cloudy))

[0032] A SAT solver will take this expression as input and attempt to solve it by searching for a solution. Although this example omits some trivial simplifications that could result in a reduced translated expression (and that most SAT solvers perform), it illustrates that the approach used by SAT solvers when inputs are extremely large results in a complexity of the translated expression that is much greater than the original expression, variables tend to get scattered throughout the translated expression, and the relationship between variables becomes blurred.

Summary of the Invention

[0033] In one embodiment the invention comprises a computerized method for solving a non-linear Boolean equations comprising partially solving said non-linear Boolean equation; storing at least one precomputed search inference relating to said Boolean equation in 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; and determining if said Boolean equation is satisfiable using said at least one heuristic.

[0034] In another embodiment, 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.

[0035] In another embodiment, said method includes 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 the desirability of using said associated inference in said determining step.

[0036] In another embodiment, 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.

[0037] In another embodiment, said state machine comprises at least one inference for a user domain relating to said non-linear Boolean equation.

[0038] In another embodiment, said state machine further comprises a computer readable data storage location for storing any linear inferences developed in said partial solving step.

[0039] In another embodiment, said state machine utilizes a technique selected from the 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.

[0040] In another embodiment the invention comprises 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.

[0041] In another embodiment, said searching step does not comprise translating said equation into Conjunctive Normal Format.

[0042] In another embodiment, said invention comprises a computer system for solving a non-linear Boolean equations comprising a pre-processor, a state machine and a search engine wherein said pre-processor is configured to perform the steps of translating said Boolean equation into a set of functions; solving said set of functions for all possible inputs; 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; a search engine configured to search for a solution to said Boolean equation using a set of heuristics developed from said set of inferences.

Brief Description of the Drawings

[0043] While the invention is claimed in the concluding portions hereof, preferred embodiments are provided in the accompanying detailed description which may be best understood in conjunction with the accompanying diagrams where:

[0044] FIG. 1 shows an example of an interconnect synthesis problem.

[0045] FIG. 2 shows sample modules and interconnect fabric for example of FIG. 1.

[0046] FIG. 3 shows a layered Boolean function corresponding to the example of FIG. 2.

[0047] FIG. 4 shows the effect of variable order on branch pruning applied to two functions.

[0048] FIG. 5 shows the result of strengthening applied to the two functions of FIG. 4.

[0049] FIG. 6 shows an example of a State Machine Used to Represent Functions (SMURF).

[0050] FIG. 7 shows an inference queue, which helps manage a collection of SMURFs.

[0051] FIG. 8 shows an example of Chaff lemma management and discovery.

[0052] FIG. 9 shows a block diagram of computational components of one embodiment of the system.

Detailed Description of the Embodiments

[0053] The present invention is a method of solving a system of generalized non-linear Boolean equations called Satisfiability, or proving that no solution exists called Unsatisfiability. This method does not require the translation of the system of equations into CNF as the CNF SAT solvers do, nor does this tool solve for all inputs as BDD solvers do.

[0054] The SBSAT method may use a BDD front end to pre-process the input. The SBSAT method searches for a solution to the system of equations in the user domain, that is, directly using the original equations to determine which variable should be assigned a value next. This is accomplished by building a state machine to represent each of the user domain equations.

[0055] A state machine is a computerized device for storing the current status of the search process so that variable assignment decisions can be made efficiently by table lookup and not by recomputing complex calculations. The concept of the state machine construction is to pre-compute anything that can be pre-computed so that search time computations can be minimized. In one embodiment of the invention, the use of state machines support the precomputing and storing of all possible search futures (or other important information/inferences) before searching commences. In another embodiment, the method performs no computation while searching that is not absolutely required.

[0056] A state of an SBSAT state machine may capture information about all of the variables present in that particular state. It may further associate with each state a pre-computed score that is computed hierarchically at state machine build time. The score may be used at run time to determine what the next variable to assign a value to should be. This method of score pre-computation allows complex scoring functions to be computed that, in CNF branching, are too expensive to compute.

[0057] In another embodiment, each state reports any linear inferences, i.e., inferences of the form v=false, ν=true, ν=w, ν=w, where νand w are input variables, that are implied by the current state. The search mechanism may use these inferences at run time. Thus, the state machines may support highly intelligent search heuristics. The state machines may contain information that is discovered once (expensively) at preprocessing time and reused (inexpensively) repeatedly during search.

[0058] At any point in the search process each state machine is in a particular state, called a current state, and access to any information contained in that state is immediate. When another variable is assigned a value or when a variable must be unassigned the current state becomes one of the other states of the state machine. In that case we say there has been a state transition from one state to another. State transitions may be predicted efficiently in preprocessing and may also carry information that may be used efficiently many times during search. For example, inferences that become valid after the transition may be saved. State machines also allow variables that exist only in that one state machine to be existentially quantified away. They allow complex autarky variable subassignments to be captured and globally applied. An autarky variable assignment or autarky is an assignment of values to some of the input variables such that a solution to any one extension of that assignment implies a solution to all other extensions and no solution to any extension implies no other extensions will lead to a solution. Identifying autarkies can be important during search because failure to extend a partial assignment containing an autarky means the same failure will result for any extension of that assignment so they should not even be tried. Thus, search time may be reduced considerably by identifying autarky subassignments.

[0059] An embodiment of a State Based Satisfiability Solver (SBSAT) solves problems in the user domain through techniques such as existential quantification, generalized co-factoring, branch pruning, lemmas, high order scoring functions, pure literals, and branch time autarky detection. The improved performance of various embodiments of the current invention is needed because many instances of problems are still too difficult to be solved by any existing method including pure BDD and pure SAT solvers. Furthermore, the magnitude of such problems is increasing as the need for more complex and compact circuits continues to grow.

[0060] The invention may solve instances of LBF (Layered Boolean Formulas) including Conjunctive Normal Form (CNF) formulas, some Quantified Boolean Formulas (QBF), and Trace formulas which may arise in a variety of formal verification problems including microprocessor verification, illegal transition checking, and interconnect synthesis, among others.

[0061] An embodiment of the invention solves LBFs by using BDD technology as far as is possible and then switching to search technology to complete a solution. Such an embodiment precomputes everything for the sake of efficient, advanced search heuristics by doing a function-complete lookahead for inferences while staying in the user domain. A preferred embodiment of the system and method does not include translation of the problem into CNF format. Thus, some domain-specific information that may be garbled by translation remains clear and accessible. For instance, dependent and independent variables, which have been known for some time to have tremendous impact on the speed of solvability in microprocessors, may be more successfully identified. Traditional BDD also recognizes these variables by staying in the user domain but the BDDs often get too big when combining to practically solve problems.

[0062] In one embodiment, the purpose of the pre-processing phase is merely to reorganize and reduce input functions, to discover some basic inferences, and to pre-compute information to be memoized, or saved, and used effectively by the search engine, called the brancher. All pre-computed information is saved. This is done using a collection of state machines, one for each function remaining after pre-processing. The state machines enable a new form of search look-ahead: inferences and other information resulting from any possible future computation from the current search state are immediately available for each pre-computed function. This differs from the partial breadth-first look-ahead of Stalmarck across all functions and the partial depth-first look-ahead, commonly called restarts, or Chaff.

[0063] Preferred embodiments of the invention support complete lookaheads on all possible search futures for all equations. Prior art embodies 1) partial breadth-first lookahead—where inferences are generated just a few levels below the current level (like looking ahead two or so moves in chess) and 2) partial depth-first lookahead—where inferences are generated during search then the search is restarted now knowing these newly generated inferences (like stopping the chess game after knowing what the opponent will do after several moves and restarting).

[0064] In various embodiments of the invention, function-complete lookahead admits search heuristics of greater complexity which can be computed efficiently. The net result is to reduce the size of the search space, due to the powerful heuristics, and increase the rate at which search steps are completed, due to the memorization of pre-computed information. Existing search support strategies such as lemma maintenance and lemma replacement heuristics (see below) are incorporated by the invention. However some, particularly autarky variable subassignments are used in a unique way. The invention also incorporates existing and new BDD operations. Among the new ones are branch pruning and strengthening which are described below.

Pre-Processing

[0065] In one embodiment the preprocessor contains four principle components: primitive inferencer, branch pruner, strengthener, and existential quantifier.

[0066] The primitive inferencer also captures some inferences, namely ν=true, ν=false, ν=w or ν=w for some variables v and w, at pre-process time. These differ from those captured by branch pruning or other techniques in that they come from just one BDD.

[0067] The branch pruner eliminates redundancies but it also reveals inferences that may be used to simplify the input set of functions. However, not all inferences are revealed that can be as this outcome is sensitive to the order of variables used for the BDDs. This is illustrated in FIG. 4. The top two BDDs are branch pruned with no change. However, the same two functions under a different variable ordering, as shown by the bottom two BDDs, are branch pruned to reveal the inference ν₃is false.

[0068] The purpose of strengthening is to reveal the inferences not caught by branch pruning. It does so by existentially quantifying away variables in f that do not exist in c and then applying the branch pruner, leaving a reduced f which may reveal new inferences. FIG. 5 shows an example.

[0069] The top two BDDs are strengthened and the resulting two BDDs are conjoined as shown in the bottom of the Figure to reveal ν₃is false.

[0070] Existential quantification is an existing concept among BDD tools: the idea is to eliminate a variable v from a function f_iby substituting the logical or of f_iwith v set true and f_iwith v set false. This can have a major impact on function complexity if v is in only one of the input functions.

[0071] In another embodiment, the method for deriving a satisfying variable assignment for variables of a Boolean formula, compromises a iterative preprocessing phase which includes the steps of building clusters of equations that share common variables (if we view each equation as a Truth Table, this step causes as many zeros as possible to be entered into the Truth Table) and globally applying any inferences that were implied by the local equations (or clusters from above). The process of applying inferences may uncover additional inferences, these additional inferences are also applied globally until such time that no additional inferences are uncovered or the system of equations is solved or the system of equations is proven unsolvable. Variables that exist in only one equation are existentially quantified away (if additional inferences are uncovered return to the step of globally applying such inferences. Using a weakened form of generalized co-factoring, called branch pruning, conditional variable assignments from one equation (or cluster) are applied to other equations (or clusters). If additional inferences are uncovered return to return to the step of globally applying such inferences. A State Machine Used to Represent Functions (SMURF) is created for each equation (or cluster) out put from the pre-processing phase.

[0072] The data may be presented to the pre-processor via an input file. In this input file BDD variables may be created, all Boolean functions, e.g., AND, OR, NOT, IMPLIES, XOR, NOR, NAND, etc., may be used taking as inputs previously computed BDDs producing new BDDs as outputs. These BDDs created may be entered as macros. The macros may be passed parameters to create layered Boolean Functions. macros may be used to create additional macros. Once the user domain equation has been created, it is submitted as an input to the clustering method.

[0073] A sample input file is as follows:

[0074]


P BDD 8 3 ;;; DIMACS Format, BDD representation, 8 variables, 3 user
inputs
#define m1 (1 2 3 4) : and 1 or 2 xor 3 4	;;; macro 1
#define m2 (1 2 3) : imp m1(1 3 2 T) xor 1 3	;;; macro 2
and 6 xor 3 6	;;; equation 1
or eq(1) m2(6 3 8)	;;; equation 2
*imp eq(2) eq(1)	;;; equation 3, User input 1
#define m3 (1 2 3 4 5): or4 and	;;; macro 3
1 2 and 2 3 and 3 4 and 4 5
*m3 (6 8 5 8 T)	;;; equation 4, User input 2
*m3 (m1(−2 3 4) m2(2 −3 −4) 2 4 3)	;;; equation 5, User input 3

[0075] Input from the file continues until the specified number of user inputs has been processed. The user inputs are represented by * at the start of the current equation. Each entry, except macros, is entered as a new equation that can be either entered as a BDD equation awaiting further processing and/or as a user input. Equation entries, results of previous BDD calculations, or macros with parameter substitution, can be used to create new equations or macros. Macros are not entered in as user inputs nor are they entered as BDD equations. The BDD functions that are pre-defined are: AND, OR, NOT, IMP, XOR, EQU, NAND, NOR, NIMP, EXIST, UNIVERSAL, CoFactor, Prune, BDD_PRINT, and BDD_INF. Variables may be negated by use of NOT, or they be negated by simply negating the variable, e.g., 7, −7, 67, −67, NOT(7), NOT(67). Results of previous BDD calculations may be referenced in new equation or macro definitions by use of the EQ function with a parameter referencing the BDD equation as a parameter. This interface makes available to the user all the power and expressive power of BDDs. Computations can be carried out directly in the BDD tool if the equations being represented are simple enough. The BDD interface tool also supports BDD_PRINT, which prints out a BDD. BDD_INF, which computes all linear inferences that are represented by the BDD that was input as a parameter. BDD_INF returns all inferences of the form variable=0, variable=1, variable1=variable2, variable1=NOT(variable2) for any given BDD.

[0076] In addition to supporting DIMACS BDD input files, DIMACS CNF and DIMACS DNF files are also accepted as input. Also Carnegie Mellon Trace input files are also accepted as input files. All input file formats go through the BDD preprocessor. The BDD pre-processor, in all input formats, produces BDD equation outputs for the next step of the SATISFIABILITY solver.

[0077] In another embodiment the pre-processing phase may allow additional zeros to be entered into the truth table that represents each user level constraint. By adding extra zeros into each truth table then additional inferences will be exposed higher in the satisfiability branch tree. This results in backtrack with fewer assumptions. This results in solution times that are potentially orders of magnitudes more efficient.

[0078] In another embodiment the pre-processing phase avoids the building of unnecessary state machines. No state machine will have inferences at the top level. Every variable will occur in at least two state machines. All trivial systems of equations will have been solved before entering the brancher.

[0079] In another embodiment, the preprocessing phase removes all variables that do not exist in at least two equations. If a variable only occurs in one equation, then the satisfiability or non-satisfiability of the system of equations does not depend directly on that variable. If a satisfying assignment of variables is found, then substitution of the satisfying variable assignments into the original equation will yield the satisfying assignment of the variable that was existentially quantified away. If the system of equations was unsatisfiable after the variable was quantified away, then the system would also have been unsatisfiable with the variable that was existentially quantified away. Existentially quantifying away internal variables when using BDDs is a long established procedure for reducing the size and complexity of solving BDD problems. In this case we are using the technique during pre-processing to build optimial conditions for branching over generalized non-linear systems of equations.

[0080] In another embodiment the preprocessing phase seeks to remove as much dependency from the generalized systems of non-linear equations as possible. By making the system of equations independent as possible, then the scoring functions, which have an assumption of independence, will result in near optimal branching decisions. The following C code shows the branch prune algorithm. The highlighted code in the middle is what makes branch prune different from generalized co-factoring. The branch pruning algorithm makes conditional variable assignments.

[0081]


	BDDNode prune (BDDNode f, BDDNode *c) {
	// base case
	if(f == c) return true_ptr;
	if((c == true_ptr) ∥ (f == true_ptr) ∥ (f == false_ptr))
	return f;
	// Optional line if complemented edges are supported
	if(c == ite_not(f)) return false_ptr;
	// The following line is what makes prune different from GCF
	// i.e., variables in c not if f are existentially quantified
	if(f−>variable > c−>variable)
	// existentially quantify away c−>variable
	return prune(f, ite_or(c−>thenCase, c−>elseCase));
	int v = f−>variable;
	// process conditional variable assignment, v==true_ptr
	if(reduce_f(v, c) == false_ptr)
	return prune(reduce_t(v, f), reduce_t(v, c));
	// process conditional variable assignment, v=false_ptr
	if(reduce_t(v, c) == false_ptr)
	return prune(reduce_f(v, f), reduce_f(v, c));
	// recursive case, continue search for conditional assignments
	BDDNode *r = prune(reduce_t(v, f), reduce_t(v, c));
	BDDNode *e = prune(reduce_f(v, f), reduce_f(v, c));
	if(r == e) return r;
	return find_or_add_node(v, r, e);
	}

[0082] In another embodiment, the preprocessing phase is essentially building a Directed Acyclic Graph (DAG) where at each node is represented every variable in the function that is represented by the current function. Stored within each node is a data structure for each variable in the current state. Stored with in each variable data structure is a pointer to a new state that would result from assigning the variable true within the current state, a pointer to a new state that would result from assigning the variable false within the current state, a pointer to a new state that would result if the current variable were to existentially quantified away, a pre-computed score under the assumption that the current variable is to assigned true, a pre-computed score under the assumption that the current variable is to assigned false, a pre-computed score for the variable as a whole. And associated with the current state is a score that is the merger of all individual variable scores. In addition associated with each state is a list of pointers to descendant states that are autarky with the current state.

[0083] In another embodiment the preprocessing phase determines if a parent state and a descendant state are AUTARK or not is accomplished by existentially quantifying away the variables on the path that lead from the parent state to the descendant state, and then comparing the resulting function with the function associated with the descendant state. If the existentially quantified function equals the function that resulted from just following variable assignments, then the parent and descendant states are AUTARK with respect to one another. The AUTARKY in this case means that if the descendant state is satisfiable then the parent state will also be satisfiable, and that if the descendant state is unsatisfiable then the parent state will also be unsatisfiable. In particular, it means that the entire branching path reaching from the parent state to the descendent state can be thought of as a single assumption, even if multiple assumptions were involved in reaching the descendant state. However, in building the state machine we are only searching for AUTARKIES within each individual state machine. Before an AUTRAKY can be applied globally each state in some parent node of the brancher must be AUTRAK with respect to the current state of the brancher that is considering a back track decision. Global AUTARKIES are only searched for at brancher back track time. If an AUTRAKY is found then multiple assumptions get to be popped off the branching stack. The result of AUTARKY backtracking is that significant portions of the branching tree can be eliminated. Global AUTARKY backtracking can be efficiently implemented by storing pre-computed AUTARKY relationships in the state machines at state machine construction time.

[0084] In another embodiment, the preprocessing phase is used to build state machines that will include all of the information necessary to support high order scoring functions, fast state transitions, fast scoring function calculations, fast elimination of variables that exist only in one state machine, AUTARKY detection at branching back track time, early backtracking by branching on generalized non-linear equations directly, reduced number of backtracks, and more back jumping, all of which supports a faster satisfiability solver that is tailored to solving extremely complex systems of non-linear Boolean equations.

State Machines.

[0085] In various embodiments of the invention, the primary vehicle for revealing inferences during the search process is a collection of state machines, one for each function, called SMURFs (State Machine Used to Represent Functions). We illustrate the use of state machines with an example. Suppose one of the functions of a given LBF is
ν₃^((ν₁≡ν₇)ν₉)(ν₁^ν₇^ν₉)

[0086] The truth table for this function is given in FIG. 6. Suppose also that we require this function to have output value true. Now suppose that during the search process, of the four variables input to the function, the first to be assigned a value is v₁and suppose the value it is assigned is true. Then, for any extension to that assignment which does not involve the function's other input variables (namely ν₃, ν₇, and ν₉), this function becomes the reduced function
ν₃^(ν₇ν₉)

- [0087] because the term (ν₁^ν₇^ν₉) can never be made true as long as ν₁is true. The original function is true if and only if the reduced function is true if ν₁is true. But for the reduced function to be true ν₃must be true. Thus the assignment of true to ν₃is forced and we say that ν₃=true is an inference.

[0088] Inferences are extremely important to the search process: generally, the more variables which are forced the better because they relieve the brancher of the burden to test both values of those variables during search. If we knew all inferences that could be made for a given problem right from the start (that is, can do a complete lookahead for inferences), the problem would be solved without the need for any search at all. But the problem of finding all inferences is, not surprisingly, extremely hard. What state machines allow us to do is find all inferences for each of the original functions of a given problem (not the entire input) right at the start. In other words, state machines provide a complete lookahead on all functions. State machines do not supply as much information as a complete lookahead would but do provide some intermediate level of information that can make search much more intelligent: the inference information discovered per function at the start is compiled into and saved in the form of state machine and that information may be used efficiently (because it is computed only once during preprocessing) by a powerful search heuristic.

[0089] Prior attempts at using lookahead information involve either: 1) during search look ahead to the next one or two variable assignments and see what inferences will be made; and 2) continue the search for a while and accumulate inferences that are made, then save those inferences and restart the search process using the knowledge obtained from them. For these methods to use the same heuristics we do, the information we precomputed one time at the start will have to be recomputed over and over again. Below is an example of a heuristic that is easy for us to compute but difficult for other solvers.

[0090] Now we describe the structure of state machine. A state, for a given function, is an assignment of values from the set {false,true,unassigned} to its input variables. Transitions from one state to another occur deterministically when the value of an input variable changes. Each change in state asserts one or more new inferences, that is, propositions implied by the assignment of values corresponding to the target state, which did not hold before the transition. Since the assertion of an inference rules out a contrary transition, some states may be unreachable. Therefore, although a function of k variables has 3^kstates, a SMURF typically consists of far fewer than this number since it does not maintain unreachable states.

[0091] Supervising the SMURFs is a module, called the Village, which creates them, performs the function of brancher (changes states when a variable is assigned a value), and collects inferences asserted by SMURFs so it can make early backtracking decisions and broadcast assertions to all SMURFs. Fundamental to the operation of the Village is an Inference Queue where all inferences are stored.

[0092] Each of a SMURF's states corresponds to a reduced Boolean function reached by forcing the function's input variables to the values specified by the state. A SMURF's initial state (state number 2) corresponds to the entire Boolean function, when all variables are unassigned. One of a SMURF's final states corresponds to a tautology (state number 1). A SMURF in state 1 means that its associated function is satisfied by the variable assignment of the current state. A SMURFs hypothetical trap state (state number 0) corresponds to a contradiction, meaning the current variable assignment cannot possibly extend to an assignment where the SMURFs associated function is satisfied. This state is unnecessary (see FIG. 6, for example) because precomputed inferences saved in association with state transitions force assignments to variables in such a way as to prevent a contradiction from actually being reached.

[0093] When a Boolean function evaluates to false its associated SMURF is built to represent the function's complement instead. A solution to the given collection of Boolean functions and output vector is a consistent total assignment (no unassigned variables) that drives each SMURF to its tautology state.

[0094] A SMURF may be modeled as a directed acyclic graph (DAG) where edges represent transitions and vertices represent states. Each edge in the DAG is labeled by a single variable assignment. When a SMURF receives a variable assignment from the Village, it changes state along the outgoing edge labeled by the assignment. Such an edge may exists because SMURFs may be built to report impending inconsistencies one step before they happen (see below for an explanation). Also associated with each edge may be a (possibly empty) list of other variable assignments that must be honored in order to validate the transition (one form of inference). The transitioning SMURF replies to the Village and gives it the assignments found in the list, called the SMURF's reply list. The Village enqueues them for broadcast to all Smurfs representing functions which depend on at least one of the inferred variables.

[0095] Each state has a unique reference number, and uniquely represents a partial assignment. In other words, there may exist in the DAG many paths from the initial state corresponding to one partial assignment (depending on the order in which the single assignments are presented), but all of these paths lead to the same state.

[0096] An important feature of SMURFs is that implementation of the trap state is avoided by making the tautology state reachable from all other states. This is a consequence of the reply inferences: when a SMURF would otherwise be a single variable assignment away from its trap state, it makes the opposite assignment as a reply inference, avoiding the problem. This is a generalization of the well-known unit clause rule used successfully in Davis-Putnam-Loveland-Logemann algorithms; it may force values on several variables at one time. This is illustrated in the example SMURF shown schematically in FIG. 6. If ν₃is assigned value false for some reason, the arc from state 2 to state 1 in the figure shows that variables ν₁, ν₇, and ν₉have implied values of false, false, and true, respectively, and these are placed in the reply list associated with that arc. Similarly, if ν₁is assigned the value true, then the assignment ν₃=true is inferred from the reply list of the arc between states 2 and 4. Observe there is no arc from state 8 to state 1. This is because state 8 represents a linear function. The topic of linear functions is treated below where it should become clear why state 8 is terminal.

[0097] A SMURF listens to the Village for variable assignments. When a SMURF receives one, it makes the state transition and returns a list of inferences that must now hold. It is the responsibility of the Village to ensure that the inferences in the list become agreed upon by all Smurfs.

[0098] A Village manages a collection of Boolean functions and controls the search. It builds a SMURF for each function, has an inference queue to handle communication of variable assignments between SMURFs, and is a nearly complete brancher, lacking only heuristic guidance. The heuristic component of the solver, which guesses a variable assignment when no inferences are offered, is discussed below.

[0099] The inference queue contains an ordinary queue and a filter (refer to FIG. 7). The queue contains variable assignments. Every variable assignment made during the search is input into the inference queue. If the variable assignment was previously enqueued, the filter prevents it from being enqueued a second time. If the opposite assignment was previously enqueued, the filter reports a contradiction, causing a backtrack. To perform its task, the inference queue must remember every variable assignment that passes through it. Since these are the variable assignments assumed so far in the search, the memory of the filter is enough to determine a search state.

[0100] A Village has a state space in which each state corresponds to a particular partial assignment on the set of input variables. Unlike SMURF state spaces, this space is too large to explore completely; instead, it is the job of the Village brancher to find a state with a consistent total assignment. From a particular Village state, the brancher guesses a variable assignment by calling a heuristic function. If the new state cannot be extended to a solution, then the original state must be restored and the opposite of the guess assumed.

[0101] The following is a description of Village's brancher:

[0102]


Repeat {
	Push the current Village state onto the stack.
	Consult a heuristic for a guess and push it onto the Inference Queue.
	While Inference Queue is not empty {
	Dequeue a variable assignment and broadcast it to dependent Smurfs.
	Enqueue all assignments returned by the Smurfs.
	If Inference Queue reports a contradiction:
	If Village Stack is empty, terminate in failure.
	Otherwise, pop the stack (restore the previous Village state)
	and enqueue an assignment opposite the assumption made
	at that state.
	}
	If all variables have been assigned, report a solution.
}

[0103] Observe the following about SMURFs:

- [0104] 1. A state of a single SMURF may be entered many times during a search even though all search states are entered at most once. Thus, precomputing state and transition information saves on overhead during the search.
- [0105] 2. The pre-computation of SMURF information may be amortised still further in the case that the LBF problem is modified to ask whether solutions exist for the same input formula but different output function values.
- [0106] 3. From any SMURF state, all computation futures are easily accessible.

[0107] Although SMURF size can grow exponentially in the number of input variables we have developed three ways to control size. First, there are some functions which have SMURFs that can be simulated by a few states and a counter. An example of such a function is x≡ab . . . y. Where possible, such simulations are used. Second, a function appearring many times with different inputs may be parameterized so that its SMURF may be constructed once and used many times. Third, if all else fails and a very large SMURF is unavoidable, the action of a SMURF may be simulated by a modified BDD which changes through the search to allow inferences to percolate to the top as would happen when entering a corresponding SMURF state.

Search Heuristics.

[0108] Complex search heuristics may be efficiently computed from precomputed SMURF state and transition information. The objective of a search heuristic is to pick a variable for branching and then to pick the most likely branch to search first.

[0109] In one embodiment, FutureInference, each SMURF state has a precomputed weight to which every inference, that the SMURF may yet broadcast, contributes. The computation is done in a bottom-up fashion: a state's successors' contributions are computed before the state's own contribution If a state s hasp successors {s₁, s₂, . . . , s_p}, then the weight of s is

\sum_{i = 1}^{p} (weightOf (s_{i}) + numberOfInferencesMadeEnrouteTo (s_{i})) / k * p

where k is some predetermined constant The weight of the final (tautology) state is 0, as no inferences are ever reachable from it.

[0110] The constant k controls the balance between quantities of inference and how deep into the future they occur. The original FutureInference heuristic took k equal to 1 so that the score of a state was an arithmetic mean of its successors' scores plus the number of inferences replied in the transition. However, the latest FutureInference heuristic implemented uses a k of 3. It is clear that some problems are more successfully solved by a lower k and some by a higher k but values outside the range 1 to 3 have not shown any special solving power.

[0111] At a choice point each variable is assigned a score equal to the sum of the weights of the SMURFs that still use it in their current states. The variable with the highest score is then chosen for branching.

[0112] In a second embodiment a search heuristic called GloballyBalanced-LocallySkewed (GBLS) attempts both to skew the search within a SMURF toward forcing inferences as soon as possible and balance the expected global search space seen among all SMURFs. In GBLS the states of SMURFs are assigned weights in the manner of the FutureInference heuristic. In addition, every state transition gets a weight derived from the weight of the destination state and the number of reply inferences along the transition. The score of a literal is the sum of the weights of the outgoing transitions from current states on the literal. Each variable is scored as (sν₁+1/4096)*(sν₀+1/4096), where sν₀and sν₁are the scores of its literals. The highest-scoring variable is chosen for branching, and the branching is in the direction of the higher-scoring literal.

Linear Functions.

[0113] A linear function either has value true if and only if an even number of its input variables have value true (even type), or has value true if and only if an odd number of its input variables have value true (odd type). Even if given functions are not linear, they may be reduced to linear subfunctions during the search for a solution, as variables are assigned values. During preprocessing, every linear subfunction of every function in F is tagged to an appropriate SMURF state. When that state is reached during search, the linear subfunction it tags is added to a collection of all currently active (that is, inferred) linear functions. For such a collection we can answer the following questions efficiently:

- [0114] 1. Are there any equivalences between variables?
- [0115] 2. Are any variables forced to a value?
- [0116] 3. Is the collection of functions satisfiable?

[0117] These are answered when the collection of linear functions changes by applying gaussian elimination. Gaussian elimination is a well-known technique for solving a system of linear equations. In this technique like terms of any pair of equations may be added together to form another equation which replaces one of the two that were added. The net effect of the addition is to replace an equation with one having one fewer term.

Lemmas.

[0118] As is the case with all modern SAT solvers, we reuse some of the refutations obtained for subsets of functions after guessing values for a substantial number of input variables. This has the effect of turning a tree search into a search on a DAG (edges directed downward) with the result that fewer nodes of the search space are expanded. A refutation which is saved for future use is a lemma. More precisely, a lemma is a minimal subset of variables and their values which actually causes a refutation at a particular node in the search DAG. There may be several such lemmas for each node of the search DAG but using all of them is too expensive. Thus, heuristics for choosing lemmas as well as replacing lemmas with more current ones have become extremely important and can have a tremendous effect on the number of nodes expanded in the search space. We use the heuristics developed by Chaff. FIG. 8 illustrates this. The white circle is a choice point involving variable ν₆₁at a depth 20 (according to the table) in the search DAG. The black circles are variable choices which are forced by functions, in this case simple disjunctions, shown beside white boxes. After setting ν₆₁to false, ν₁₇is forced to true, then ν₁₈to true, and so on until a contradiction is reached at ν₇₂. At this point the brancher creates the resolvent of the two disjunctions below node ν_72,sshown as a disjunction between square brackets, and checks to see how many of its variables are below the ν₆₁choice point. In this case the number is 2. The brancher backtracks to ν₇₃and repeats until at node ν₃₅it finds the number to be 1. At this point the bracketed disjunction becomes a lemma and the search “backjumps” to the deepest node corresponding to a variable in the new lemma.

Applications

[0119] Our solver can deal directly with the equivalence expression. In this case it is
((noise≡(time=12:00)^(weather=cloudy))^(noise≡ite(weather=cloudy, time=12:00, weather=cloudy)))((noise≡(time=12:00)^(weather=cloudy))^(noise≡ite(weather=cloudy, time=12:00, weather=cloudy)))

- [0120] which, because this is a very simple example, our solver immediately determines is unsatisfiable during pre-processing using typical BDD operations.

[0121] Subexpressions allowed by our solver, such as
time=12:00 and weather=cloudy implies noise
are typically more intuitive than their CNF counterparts such as
time≠12:00weather≠cloudynoise

- [0122] and this allows our solver to use more intuitive and intelligent search heuristics to find a solution.

[0123] The above example as well as all short examples are too simple to appreciate the power of our solver. More typically, a specification of circuit behavior and an implementation are given to a solver as an LBF. If that LBF has no solution then the circuit and its specification match, otherwise there is a bug. LBFs of this kind may be given as several thousand equations similar to some or all of the following:
ν≡ν₁^ν₂^ . . . ^ν_k;
ν≡ν₁;
ν≡ite(ν₁, ν₂, ν₃);
ν≡ν₁ν₂ . . . ν_k;
where ν_ican be an independent or dependent variable.

[0124] As a second example consider the problem of interconnect synthesis which is illustrated and described in FIG. 1. This problem arises when configuring Field Programmable Gate Arrays to behave according to a given circuit specification. A conceptual circuit is partitioned into sections and the question is whether there are switch settings for a given interconnect fabric which allow the FPGAs to be connected in such a way as the circuit specification requires. If there is a set of switch settings that works, show that it is the only one that does.

[0125] An interconnect fabric, as shown in FIG. 2, may be expressed using the following Boolean terms: a term similar to (x=a) is a variable which is interpreted to be true if and only if input point a is connected to output point x; the operator ^denotes Boolean and; the operator≡expresses equivalence between two Boolean variables; the operator is Boolean or; the operator ite(a,b,c) is the value of b if a has value true and is the value of c otherwise (ite stands for if-then-else). An LBF representing the solution to the example is shown in FIG. 3. The variables appearing in the last group of the figure are considered to be output variables. For a particular mapping, set the appropriate output variables to true (e.g. (o₁=a₁), (o₂=a₃), (o₃=a₂), and (o₄=a₄)), the remaining output variables to false, and solve for values of s₁. Doing so in this case gives s₁=false, s₂=false, and s₃=time. Add the expression s₁s₂s₃to those of FIG. 3 and solve to determine uniqueness (unsatisfiability).

[0126] What makes this class of problems interesting is our solver can immediately infer a solution without any search whatsoever. Thus, a solution may be obtained in a very short time. This is typically not the case if BDD tools are used exclusively. The trick is to use a method which we have adapted from other branches of electrical engineering called the impulse method. In this method connections from input to output are forced one at a time. One may develop separate expressions for each forced connection and solve the whole system of expressions as one. Although the resulting expression is huge, variable assignments are forced and a solution is obtained in less than a second, after the input expression is formulated.

[0127] Finally, we discuss the illegal transition checking problem. Consider a system of some number of “chunks” of electronic circuits, the output lines of one chunk feeding into the input lines of another chunk, except that the input lines of one particular chunk are considered the inputs to the system and the output lines of one particular chunk are considered the output of the system, and suppose that each chunk has some “control” lines which switch data entering the chunk on its input lines to the chunks output lines. Each chunk typically has some internal memory that is considered inaccesible to other chunks. Over time, possibly numerous times, the memory is given values by the internal circuitry of the chunk: those values depend on previous memory values and current input and control line values. In a secure system, some values for those memory elements will be restricted and therefore considered “illegal.” The illegal transition checking problem is to determine whether some illegal memory values are possible given some sequence of system input assignments and control assignments. Our solver is well suited to this class of problems because each chunk is a circuit that is handled as a unit by our solver. A SAT solver must translate a chunk to CNF and therefore not necessaily preserve the strong interdependence of variables corresponding to a chunk and independence of elements in different chunks. Thus, our solver is able to use this interdependence/independence information intelligently.

[0128] FIG. 9 shows a block diagram of an embodiment of the system. Inputs are a conjunction of Boolean functions expressed in any common format such as CNF, BDD, or Trace and exist as a computer file of latin symbols and symbols representing logic connectives and parentheses. All inputs enter a pre-processor which converts all functions to BDD and then reduces and simplifies those BDD functions (that is, the number of variables and subexpressions is reduced, redundant portions of an input are eliminated, and functions remaining after pre-processing are made more independent of each other). Optionally, the pre-processor exists on a remote server and inputs may be transmitted over the internet to the server for pre-processing. The location of the server is obtained by means of an internet query to a Registry operating from a published port on a worldwide known computer which is connected to the internet. After preprocessing, the functions may be partitioned into separate components by the Splitter and each component (possibly there is just one component: namely the entire input) is then sent to a SAT solver, a device which searches for a solution. Many different solvers may be recipients of a component. All but SBSAT, which is part of this invention, require translation to CNF or DNF (just a complementary way to express CNF). Shown in FIG. 9 are other popular SAT solvers such as SATO, GRASP, and CHAFF but other solvers could just as easily connect to the splitter. The SAT solver works on the component that it receives and attempts to solve it. Progress is reported to SAT solvers working on other components (the splitter knows which these are) so that all SAT solvers can agree on values to input variables when a solution is reported by the splitter. When ready, the splitter reports the solution (or that none is possible) to the program that originated the request in the first place.

Claims

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.

Patent Citations (21)

Patent	Date	Inventor	Cited By
US4649515(A)	1987-03-01	Thompson et al.	Examiner
US4658370(A)	1987-04-01	Erman et al.	Examiner
US4713775(A)	1987-12-01	Scott et al.	Examiner
US5136686(A)	1992-08-01	Koza	Examiner
US5195172(A)	1993-03-01	Elad et al.	Examiner
US5265222(A)	1993-11-01	Nishiya et al.	Examiner
US5434952(A)	1995-07-01	Yen et al.	Examiner
US5636328(A)	1997-06-01	Kautz et al.	Examiner
US5649165(A)	1997-07-01	Jain et al.	Examiner
US5734798(A)	1998-03-01	Allred	Examiner
US6058385(A)	2000-05-01	Koza et al.	Examiner
US6308299(B1)	2001-10-01	Burch et al.	Examiner
US6343376(B1)	2002-01-01	Saxe et al.	Examiner
US6408262(B1)	2002-06-01	Leerberg et al.	Examiner
US6496961(B2)	2002-12-01	Gupta et al.	Examiner
US6560758(B1)	2003-05-01	Jain	Examiner
US6640231(B1)	2003-10-01	Andersen et al.	Examiner
US6681373(B1)	2004-01-01	Zolotykh et al.	Examiner
US2001/0010091(A1)	2001-07-01	Noy	Examiner
US2002/0178424(A1)	2002-11-01	Gupta et al.	Examiner
US2004/0015799(A1)	2004-01-01	Jain	Examiner

Non-Patent Literature (31)

Mukherjee et al., “VERIFUL: Verification Using Functional Learning”, European Design and Test Conference, Mar. 6, 1995, pp 444-448.Examiner
NN9105435, “State Machine Verification Expert”, IBM Technical Disclosure Bulletin, vol. 33, No. 12, May 1991, pp. 435-436 (4 pages).Examiner
Kunz et al., “Recursive Learning: A New Implication Technique for Efficient Solutions to CAD Problems—Test, Verification, and Optimization”, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 13, No. 9, pp. 1143-115.Examiner
Li et al., “Programming model for concept learning and its solution based on genetic algorithms”, Proceedings of the 3rd World Congress on Intelligent Control and Automation, Jun. 28, 2000, vol. 1, pp. 299-303.Examiner
Kondo et al., “Design and heuristics for BDD-based automated termination verification system for rule-based programs”, IEEE SMC '99 Conference Proceedings, 1999 IEEE International Conference on Systems, Man and Cybernetics, vol. 5, Oct. 12, 1999, pp. 738.Examiner
Kurihara et al., “BDD encoding for partial order constraints and its application to expert systems in software verification domains”, 2000 IEEE International Conference on Systems, Man and Cybernetics, vol. 3, Oct. 8, 2000, pp. 2062-2067.Examiner
Holman, “A framework for determining the satisfiability of general Boolean expressions”, Proceedings of the 37th Midwest Symposium on Circuits and Systems, vol. 1, Aug. 3, 1994, pp. 381-384.Examiner
Chatalic, Philippe, et al., “Multi-Resolution on Compressed Sets of Clauses,” pp. 1-10, no date.Applicant
Baher, R. Iris et al., “Power Optimization of Technology-Dependent Circuits Based on Symbolic Computation of Logic Implications,” pp. 1-24, no date.Applicant
Paruthi, Viresh, et al., “Equivalence Checking Combining a Structural SAT-Solver, BDDs, and Simulation” (pp. 459-464), IEEE, 2000.Applicant
Wilson, Chris, et al., “Reliable Verification Using Symbolic Simulation with Scalar Values,” pp. 1-6, no date.Applicant
Kalla, Priyank, et al., “A BDD-Based Satisfiability Infrastructure Using the Unate Recursive Paradigm,” Technical Report: TR-CSE-99-6, pp. 1-10, no date.Applicant
Gupta, Aarti, et al., “Fast Error Diagnosis for Combinational Verification,” pp. 1-7, no date.Applicant
Prasad, Mukul R., et al., “Why is ATPG easy?”, pp. 1-7, no date.Applicant
Bryant, Randal E., et al., “Microprocessor Verification Using Efficient Decision Procedures for a Logic of Equality with Uninterpreted Functions,” Jun. 1999, pp. 1-13.Applicant
Biere, Armin, et al., “Symbolic Model Checking without BDDs”; Submitted for TACAS (1999), Jan. 4, 1999, pp. 1-17.Applicant
Tragoudas, S. et al., “Functional ATPG for Delay Faults,” pp. 1-4, no date.Applicant
Nam, Gi-Joon, et al., “Satisfiability-Based Layout Revisited: Detailed Routing of Complex FPGAs Via Search-Based Boolean SAT,” (pp. 167-175), ACM, 1999.Applicant
Bollig, et al, “Hierarchy Theorems for κOBDDs and κIBDDs,” pp. 1-18, no date.Applicant
Wood, R. Glenn, et al., “FPGA Routing and Routability of Estimation Via Boolean Satisfiability,” IEEE Transaction on VLSI Systems, vol. 6, No. 2, Jun. 1998, pp. 222-231.Applicant
Gupta, Aarti, et al., “Integrating a Boolean Satisfiability Checker and BDDs for Combinational Equivalence Checking,” (pp. 222 225), IEEE, 1997.Applicant
Cyrluk, David et al., “An Efficient Decision Procedure for the Theory of Fixed-Sized Bit-Vectors,” pp. 1-10, no date.Applicant
Takagi, Kazuyoshi, et al., “Computational Power of Nondeterministic Ordered Binary Decision Diagrams and Their Subclasses,” IEICE Trans. Fundamentals E80:4, pp. 663-669 (Apr. 1997).Applicant
Kawakubo, Kasuo, et al., “Formal Verification of Self-Testing Properties of Combinational Circuits,” Proceedings of ATS '96, pp. 119 122, IEEE, 1996.Applicant
Puri, Ruchir, et al., “A BDD SAT solver for satisfiability testing: An industrial case study,” Annals of Mathematics and Artificial Intelligence 17, pp. 315-337 (1996).Applicant
Groote, Jan F, “Hiding Propositional Constants in BDDs,” pp. 1-6, no date.Applicant
Nakaoka, Toshihiro, et al., “A Verification Algorithm for Logic Circuits with Internal Variables,” pp. 1920-1923, IEEE, 1995.Applicant
Ashar, Pranav, et al., “Boolean Satisfiability and Equivalence Checking Using General Binary Decision Diagrams,” pp. 259 264, no date.Applicant
Burch, J.R., et al., “Symbolic Model Checking: 1020 States and Beyond,” pp. 1-33, no date.Applicant
Bryant, Randal E., et al., “Processor Verification Using Efficient Reductions of the Logic of Uninterpreted Functions to Propositional Logic,” May, 1999, Carnegie Mellon University, pp. 1-45.Applicant
Biere, A., et al., “Symbolic Model Checking using SAT procedures instead of BDDs,” pp. 1-4, no date.Applicant