33 results about "Boolean satisfiability problem" patented technology

A method for generating a test vector for functional verification of circuits includes providing a representation of a circuit, where the representation includes a control logic component and a datapath logic component. The method also includes reading one or more vector generation targets, and performing word-level ATPG justification on the control logic component to obtain a control logic solution. The method further includes extracting one or more arithmetic functions for the datapath logic component based on the control logic solution, and solving the one or more arithmetic functions using a modular constraint solver. The modular constraint solver is based on a modular number system.

Disclosed are representative examples of methods, apparatus, and systems for generating test patterns targeting multiple faults using Boolean Satisfiability (SAT)-based test pattern generation methods. A SAT instance is constructed based on the circuit design information and a set of faults being targeted. A SAT solving engine is applied to the SAT instance to search for a test pattern for detecting the set of faults. The SAT instance or the SAT solving engine may be modified so that the SAT solving engine will search for a test pattern for detecting a maximum number of faults in the set of faults.

A method for generating a test vector for functional verification of circuits includes providing a representation of a circuit, where the representation includes a control logic component and a datapath logic component. The method also includes reading one or more vector generation targets, and performing word-level ATPG justification on the control logic component to obtain a control logic solution. The method further includes extracting one or more arithmetic functions for the datapath logic component based on the control logic solution, and solving the one or more arithmetic functions using a modular constraint solver. The modular constraint solver is based on a modular number system.

A method and system for solving satisfiability problems is disclosed. In one embodiment, clauses in a satisfiability problem are organized as a chronologically ordered stack. In another embodiment, the activity of each variable in the satisfiability problem is monitored. An activity counter is maintained for each variable and is incremented each time the variable appears in a clause used in generating a conflict clause. In an embodiment, a branching variable is selected from among the variables in the top clause of the stack when the top clause is a conflict clause. In a further embodiment, one or more conflict clauses in the stack are removed when the search tree is abandoned. In a still further embodiment, the value assigned to a branching variable is selected for purposes of having a uniform distribution of positive and negative literals.

The invention relates to a satisfiability problem (SAT)-based manufacturable hot spot disconnecting and rerouting method which belongs to the very large scale integration (VLSI) physical design field. The method is characterized in that the topological structure constraint of hot spot and connectivity constraint of line networks are used as directions, SAT constraints are established in all the rerouted line networks in the region, the constraint problem is solved to route a plurality of line networks at the same time, and the generation of a new manufacturable hot spot can be effectively controlled. Meanwhile, as the method adopts the region-based disconnecting and rerouting strategy to ensure the efficiency; and the hot spot elimination ratio in the layout can be greatly increased through the dynamic marginal adjustment and the two-stage disconnecting and rerouting process involving offset. The experimental result proves that the method can fast and effectively eliminate the manufacturable hot spot in the layout; compared with the traditional disconnecting and rerouting algorithm aiming at the hot spot, the method has better convergence, and can more effectively avoid the generation of the new hot spot and ensure to find an existing and feasible rerouting scheme.

Disclosed is a complete SAT solver, Chaff, which is one to two orders of magnitude faster than existing SAT solvers. Using the Davis-Putnam (DP) backtrack search strategy, Chaff employs efficient Boolean Constraint Propagation (BCP), termed two literal watching, and a low overhead decision making strategy, termed Variable State Independent Decaying Sum (VSIDS). During BCP, Chaff watches two literals not assigned to zero. The literals can be specifically ordered or randomly selected. VSIDS ranks variables, the highest-ranking literal having the highest counter value, where counter value is incremented by one for each occurrence of a literal in a clause. Periodically, the counters are divided by a constant to favor literals included in recently created conflict clauses. VSIDS can also be used to select watched literals, the literal least likely to be set (i.e., lowest VSIDS rank, or lowest VSIDS rank combined with last decision level) being selected to watch.

A method is provided to formally verify a property of a circuit design comprising: receiving a description of at least a portion of the circuit; receiving an indication of search accuracy criteria; receiving a description of a relationship between current and voltage (I-V relationship) for one or more of devices of the circuit; converting each I-V relationship to a conservative approximation of such I-V relationship; assigning voltage labels to one or more terminals of one or more identified devices that indicate voltage relationships among the one or more terminals consistent with KVL; defining a respective current relationship among one or more respective sets of currents of the one or more of the identified devices that is consistent with KCL; searching for one or more combinations of current and voltage values that are within at least one region of each conservative approximation and that are consistent with the voltage labels and that are consistent with each respective defined current relationship; converting each region determined to have a searched for combination of current and voltage values to multiple respective smaller regions; and repeating the acts of searching and converting until regions are obtained that meet the received search accuracy criteria.

In one embodiment of the invention, a design verifier is disclosed including a model extractor and a bounded model checker having an arithmetic satisfiability solver. The arithmetic satisfiability solver searches for a solution in the form of a numeric assignment of numbers to variables that satisfies each and every one of the one or more numeric formulas. Conflict in the search, results in the deduction of one or more new numeric formulas that serve to guide the search toward a solution. If the search finds a numeric assignment that satisfies each and every one of the one or more numeric formulas, it indicates that a functional property of the system is violated.

A method for transforming a tautology check of an original logic circuit into a contradiction check of the original logic circuit and vice versa comprises interpreting the original logic circuit in terms of AND, OR, MAJ, MIN, XOR, XNOR, INV original logic operators; transforming the original circuit obtained from the interpreting, into a dual logic circuit enabled for a checking of contradiction in place of tautology and vice versa, by providing a set of switching rules configured to switch each respective one of the original logic operators INV, AND, OR, MAJ, XOR, XNOR, MIN into a respective switched logic operator INV, OR, AND, MAJ, XNOR, XOR, MIN; and complementing outputs of the original circuit by adding an INV at each output wire. The method further provides testing in parallel the satisfiability of the original logic circuit, and the satisfiability of the dual logic circuit with inverted outputs. Responsive to one of the parallel tests finishing, the other parallel test is caused to also stop.

Soft error detection is performed by computation of states based on formal methods and by simulating a synthesized target identification logic together with the design. Soft errors may be simulated in response to detecting that a simulated state of the design is comprised by the states. A BDD representation of the design may be utilized to determine the states. A Boolean satisfiability problem may be defined and solved using an all-SAT solver in order to determine the states.

One embodiment of a method for solving an input satisfiability instance includes searching a database for a stored satisfiability instance that matches the input satisfiability instance and outputting a solution to the input satisfiability instance. One embodiment of method for converting an input satisfiability instance into a standardized representation includes applying a plurality of syntactical simplification rules to the input satisfiability instance until no conditions of any of the plurality of syntactical simplification rules can be met, thereby producing a simplified instance, uniformly replacing each variable in the simplified instance with a unique, consecutively chosen even number, annotating each literal in the simplified instance to indicate whether the each literal is positive or negative, ordering all literals in the simplified instance, and ordering all clauses in the simplified instance to produce the standardized representation.

The invention is a general-purpose sequential machine for solving boolean satisfiability (SAT) problems for functions of n variables and m clauses in linear time with complexity O(m), independent of the number of variables in the function. With current hardware technology, a value of n=32 variables can be achieved. The machine can serve as a basic building block to develop faster SAT solvers.

An apparatus includes a state machine engine. The state machine engine may also include an automaton, whereby the automaton is configured to analyze data from a beginning of an input data stream until a point when an end of data signal is seen. The automaton may further be configured to report an event representative of a satisfaction of a Boolean clause of a conjunctive normal form (CNF) Boolean expression representative of a Boolean Satisfiability problem (SAT) by a portion of the input data stream.

The invention pertains to the technical field of formal verification of an ultra-large-scale integrated circuit, in particular to an orthogonal algorithm for solving the SAT problem. The algorithm firstly defines an orthogonal relationship among the clauses, then utilizes the features of the orthogonal clauses from the point of eliminating the overlapping information in the clauses, combines the effective simplification technology and gradually simplifies the problem into a group of orthogonal clauses which are fully equivalent to the original problem; finally, whether the SAT is met or not is judged according to the coverage situation on the whole assignment space by the group of the orthogonal clauses. The method of the invention is highly efficient and practical, which can accelerate the simplification process of the problem, improve the calculation speed of solving the problem and be applicable to automatic test vector generation, a timing analysis, logic verification and equivalence verification, etc. during the design of the ultra-large-scale integrated circuit.

The invention is a method for solving the satisfiability of grand scale integration test. It is based on depth priority search, adds in reasoning process, and uses the reasoning process to carry on correspondent improvement to tactics of decision. The steps include: decision making process, simplifying process of Boolean restrain, back-track process, studying process and reasoning process. Its data structure uses 2-3 mixed variable monitoring data structure. The invention can decrease the times of decision greatly, and upgrades the operating efficiency.

The invention discloses an improved digital hardware circuit diagnosis mechanism. According to the digital hardware circuit diagnosis mechanism, an equivalence checking method based on satiable increment is applied to error diagnosis, certain candidate areas are excluded by means of similarity of internal structures of candidate areas, and then processing speed of error checking is improved. According to the digital hardware circuit diagnosis mechanism, the stability and reliability of design are systematically improved by means of the combination of various formalized methods such as the increment equivalence checking method, a logic simulation method and a Boolean satisfiability method.

Provided is a processing apparatus that processes a problem for minimizing the sum of weights respectively associated with clauses that each become false, of a plurality of clauses each based on at least one logical variable, the processing apparatus including: a calculation unit for calculating a boundary value of the sum of the weights in a case where it is assumed that a first logical variable and a second logical variable have a predetermined logical relation; and a replacement unit for replacing the first logical variable in each of the plurality of clauses with a logical expression formed by using the second logical variable, in a case where the boundary value satisfies a predetermined condition.

Techniques and systems for solving Boolean satisfiability (SAT) problems are described. Some embodiments solve SAT problems using efficient construction of truth tables. Some embodiments can improve performance of SAT solvers by using truth tables instead of incurring the overhead of Conjunctive Normal Form (CNF) conversion.

The invention discloses a target algorithm prediction method for Boolean satisfiability problems based on a graph, and the method comprises the following steps: designing a graph structure, inputtingthe original definition of each Boolean satisfiability problem in a problem set, outputting related graph structure representation, and constructing a graph structure data set corresponding to an original problem; building a conversion model from a graph structure to a document structure, and building a document data set corresponding to the original Boolean satisfiability problem; building a document vectorization model, and building a group of vectors corresponding to the original Boolean satisfiability problem; and selecting a classification model or a regression model, and training the model to enable the model to learn to predict a target algorithm of the Boolean satisfiability problem. According to the method, the powerful representation capability of the graph is utilized, the original representation of each SAT problem is converted into the logic representation of the graph, effective features are learned from the graph in an unsupervised mode, and finally target algorithm prediction of the problems is learned and applied according to the features.

This invention is a signal input / output design tool for integrated circuit input / output design. The connectivity capacity of at least multiplexer connecting internal signals and external lines is expressed as a first set of Boolean expressions. The desired connectivity between internal signals and external lines is expressed is provided by a designer. A programmed general purpose computer expresses the desired connectivity as a second set of Boolean expressions and determines whether said first set of Boolean expressions and said second set of Boolean expressions are Boolean satisfiable. If satisfiable, the design tool generates control signals to configure the at least one multiplexer to achieve the desired connectivity. If not satisfiable, the design tool generates a report indicating which portions of the desired connectivity are achievable and which are not.

The invention discloses a method for solving a Boolean satisfiability problem based on an extension rule, and the method comprises the steps: firstly designing a CCAER heuristic expression and PAWSERplanning suitable for the extension rule, and inventing a Subscoerer attribute and a CScoreer attribute of variables, wherein the CCAER heuristic expression is a certain overturning opportunity givento variables which exceed a certain threshold but have no change in pattern, and the PAWSER planning is mainly used for updating clause weights. For an example in a phase change interval, the CScoreerattribute of the variables is adopted; for an example which is not in a phase change interval, the Subscoerer attribute of a variable is adopted. Then, during initialization, an IMOM thought is utilized to obtain an initial maximum item, so that an initial solution is closer to an actual solution space, and the number of overturning times is reduced; and finally, the satisfiability of the subspace is judged in the searching process, if the satisfiability is met, a solution is found, and otherwise, we continue to judge the satisfiability of the whole space.

The invention discloses a Boolean satisfiability problem solving method and system, and the method comprises the steps: employing a plurality of parallel solvers to carry out the multi-thread parallelsolving of a CNF instance in a set threshold condition, and enabling each parallel solver to employ different initial variables; each parallel solver stops solving after triggering a threshold condition, and records the activity score of each variable in the solving process; and selecting a variable element with the highest sum of the active fractions obtained by the plurality of parallel solversas an initial variable element of a main solver, and solving the CNF instance. By adopting the technical scheme of the invention, the solving speed of the Boolean satisfiability problem can be improved.