Computer-aided design and analysis of circuits and semiconductor – Nanotechnology related integrated circuit design
Reexamination Certificate
1999-04-21
2002-08-27
Smith, Matthew (Department: 2825)
Computer-aided design and analysis of circuits and semiconductor
Nanotechnology related integrated circuit design
C716S030000
Reexamination Certificate
active
06442732
ABSTRACT:
FIELD OF THE INVENTION
The present invention relates generally to computational aspects of the design and testing of integrated circuits and other complex devices and systems, and more particularly to techniques for implementing so-called satisfiability algorithms involving such devices and systems.
BACKGROUND OF THE INVENTION
Satisfiability (SAT) is a computationally-difficult problem which is central to many computer-aided design (CAD) and test applications. The SAT problem may be characterized as follows: given a boolean function F(x
1
, x
2
, . . . x
n
), find an assignment of binary values to the variables x
1
, x
2
, . . . x
n
, such that F is set to 1, or prove that no such assignment exists. Typically, F is expressed as a product-of-sums, which is also called conjunctive normal form (CNF). An example of a formula F in CNF is as follows:
F
=(
A+{overscore (B)}
){circumflex over ( )}(
{overscore (A)}+B
){circumflex over ( )}(
A+{overscore (B)}
).
In this example, the formula F includes two variables (A and B) and three clauses, each with two literals. The literals in the third clause are A+{overscore (B)}, where {overscore (B )} is an inverting literal and A is a non-inverting literal. The assignment (A=1, B=1) is a so-called “satisfying assignment,” i.e., it sets all the clauses and F to 1. Hence, the formula F given above is satisfiable. An example of an unsatisfiable formula F′ is given by:
F′=F
{circumflex over ( )}(
{overscore (A)}+{overscore (B)}
)
In applications involving combinational circuits, the above-noted variables x
j
may represent primary inputs (PIs) of a given circuit, while F represents the primary output (PO) of that circuit. CAD and test applications that can be characterized as a SAT problem include, for example, timing verification, routing and routability analysis, fault diagnosis, logic synthesis and logic verification. SAT is also related to automatic test pattern generation (ATPG) algorithms, as it can be viewed as the problem of generating a test for a stuck-at-0 fault on a PO. An important component in ATPG is the so-called line justification problem, which deals with setting an internal signal to a given value, and corresponds to SAT on a subcircuit. Many other computationally-difficult problems, such as graph coloring, scheduling, theorem proving and constraint satisfaction problems, have also been mapped to SAT problems.
A significant drawback often associated with SAT problems is the amount of computation time required for their solution. Even with the most advanced SAT algorithms, difficult problems, such as those involving complex very-large-scale integration (VLSI) circuits, can require many hours of computation using powerful computers. A number of recently-developed techniques have attempted to simplify the SAT computation process through the use of reconfigurable hardware. Reconfigurable hardware is used in adaptive computing and other applications to implement logic circuit functions. A given set of reconfigurable hardware, which may be based on field programmable gate arrays (FPGAs) or other similar programmable logic devices, can be reconfigured so as to provide different logic functions at different times, thereby in effect providing the functionality of a complex circuit which would otherwise require substantially more hardware. Reconfigurable hardware platforms designed to facilitate SAT computation are referred to as “satisfiers.”
Another drawback associated with solving SAT problems using the above-noted reconfigurable hardware is the capacity and the cost of the reconfigurable hardware platform. Existing satisfiers are generally limited in the size of the problems they can handle by their available hardware capacity. As a result, any problem that does not fit within the available capacity of a given satisfier is automatically classified as “out-of-bounds” for that satisfier. Although conventional logic emulators can have a large capacity (up to several million gates), they are generally quite expensive (about $0.50 per emulated gate) and hence not easily affordable. However, most other hardware platforms that are reasonably priced do not provide sufficient capacity. A need therefore exists for improved techniques for solving satisfiability problems on reconfigurable hardware.
SUMMARY OF THE INVENTION
The invention provides a virtual logic system for solving satisfiability problems on reconfigurable hardware, which allows the reconfigurable hardware to solve problems much larger than its available capacity. In an illustrative embodiment, a set of reconfigurable hardware including a number of field programmable gate arrays (FPGAs) is configured to solve a satisfiability problem. The satisfiability problem is decomposed into a number of independent and disjoint subproblems, e.g., using a simple decomposition in conjunction with disjoint partitioning, such that each of the subproblems is implementable within a given one of the FPGAs without the need for any inter-FPGA communication. Each FPGA then independently determines a satisfiability indication for one of the subproblems. At least a subset of the FPGAs may each be used to process more than one of the subproblems.
In accordance with one aspect of the invention, a simple decomposition technique is provided for decomposing the satisfiability problem into a number of independent subproblems such that each of the subproblems is solvable by a single hardware element, e.g., a single FPGA, of a reconfigurable hardware platform. In one possible implementation, the simple decomposition technique utilizes a formula splitting process that is repeated recursively for k variables. If this decomposition process is represented by a binary OR tree with k levels, the subproblems to be solved are obtained at the terminal nodes of the tree. The OR relation between the two branches of a node means that solving one of the two subproblems is sufficient to solve the original problem. The more variables assigned, the smaller the subproblems become, although k should be limited since the number of subproblems is 2
k
. The resulting subproblems share all the variables that are not assigned, so the subproblems are not disjoint. Nevertheless, the subproblems are independent since the values of the shared variables do not have to be correlated, as different subproblems may obtain different satisfying vectors for the original problem.
In accordance with another aspect of the invention, a disjoint partitioning decomposition technique is provided which utilizes the above-noted simple decomposition technique in conjunction with disjoint partitioning to decompose a satisfiability problem into a number of independent and disjoint subproblems. One possible implementation of this disjoint partitioning decomposition utilizes a clause bipartitioning algorithm, which starts by creating a one-component cluster from each clause of a satisfiability formula in conjunctive normal form (CNF), and then repeatedly merges clusters based on a measure reflecting the number of common variables, until two final clause clusters are obtained such that their number of common variables is minimized. To separate these two clusters, at least some of their common variables are assigned. The algorithm tries tentative formula simplifications for both 0 and 1 assignments to each common variable, and evaluates the simplifications based on the reduction obtained in the set of common variables. If there are no common variables, the process continues recursively with the two disjoint sub formulas, both of which need to be satisfied. The recursion terminates when the current sub formulas fit into a target reconfigurable hardware platform. The disjoint partitioning decomposition technique generally results in a significantly smaller number of subproblems than the previously-described simple decomposition technique.
The decomposition techniques of the invention can effectively divide a satisfiability formula into independent subproblems that can be concurrently run by, e.g., m
Abramovici Miron
De Sousa Jose T.
Dinh Paul
Lucent Technologies - Inc.
Ryan & Mason & Lewis, LLP
Smith Matthew
LandOfFree
Virtual logic system for solving satisfiability problems... does not yet have a rating. At this time, there are no reviews or comments for this patent.
If you have personal experience with Virtual logic system for solving satisfiability problems..., we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Virtual logic system for solving satisfiability problems... will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-2926099