Computer-aided design and analysis of circuits and semiconductor – Nanotechnology related integrated circuit design
Reexamination Certificate
1997-08-28
2001-06-12
Smith, Matthew (Department: 2825)
Computer-aided design and analysis of circuits and semiconductor
Nanotechnology related integrated circuit design
C716S030000
Reexamination Certificate
active
06247164
ABSTRACT:
BACKGROUND OP THE INVENTION
1. Field of the Invention
The present invention relates to a configurable hardware system implementing Boolean satisfiability (SAT) and method therefor. More specifically, the present invention relates to a field-programmable gate array (FPGA) system operable to obtain a solution set for a SAT problem, and method for using the FPGA system to derive the solution set.
2. Description of the Related Art
The Boolean satisfiability problem lies at the core of many synthesis and verification applications. Therefore, software approaches for accelerating the solution process have been studied extensively. Often, however, particular SAT problems pose computational difficulties for even the most aggressive software approaches. Accordingly, it is desirable to discover new systems and methods for solving complex SAT problems efficiently and rapidly.
Software implementations of SAT have been used to accelerate the solutions of a wide range of problems in synthesis, verification, automatic test pattern generation (ATPG), cryptology, and other fields. Some examples are discussed in S. Chakradhar, V. Agrawal, and S. Rothweiler,
A Transitive Closure Algorithm for Test Generation
, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 12(7):1015-1028, July 1993; T. Larrabee,
Efficient Generation of Test Patterns Using Boolean Satisfiability
, PhD thesis, Stanford University, February 1990; and T. Larrabee,
Test Pattern Generation Using Boolean Satisfiability
, IEEE Transactions on Computer-Aided Design, volume 11, pages 4-15, January 1992. Such software implementations of SAT rely on a backtracking algorithm and other search-space-reducing techniques to explore different possible variable settings, and to determine the implications of these variable settings on the rest of the problem. These methods expand the set of problems for which solutions can be generated in acceptable runtimes. However, for many cases, the prior art software methods are still too slow and at times may have to be aborted before a solution has been obtained.
In order to fully appreciate the present invention, one must have an understanding of SAT and, therefore, it is assumed that the reader is familiar with SAT and with prior art software methods for its implementations. Nevertheless, a short review of SAT and software implementations is provided herein. Additionally, throughout the specification, references are made to various publications describing SAT and prior art software implementations.
Boolean satisfiability (SAT) is a method for finding variable values that satisfy a Boolean formula typically provided in a conjunctive normal form (CNF), i.e., a product of sums. That is, the formula is expressed as an AND of m clauses, each of which is the disjunction (i.e., OR) of one or more literals. Hereinafter, variables (or their complements) taking on an assigned value (1 or 0) are referred to as literals, while a disjunctive expression of literals is referred to as a clause. An x-clause is a clause having x variables. Thus, a set of m clauses defines the SAT in CNF, such as, for example, the set of the two 3-clauses (a+b+d) ({overscore (a)}+{overscore (b)}+{overscore (d)}). Here {overscore (b)} is the complement of b.
As discussed in Larrabee cited above, any Boolean satisfiability problems for Boolean formula or circuit can be converted to one for the conjunctive normal form. Those well versed in the art will recognize this as one of several equivalent ways of doing this conversion. Thus, our methods apply to Boolean formulas or circuits in any original form.
According to the prior art methods, the SAT-solver uses a systematic backtracking procedure to obtain a variable assignment for which the CNF formula evaluates to 1. The efficiency of this approach derives from the fact that dependencies between variables can be extracted readily by the nature of the CNF representation. For example, the requirement that the set (b+d) ({overscore (b)}+{overscore (d)}) evaluate to 1 creates a dependency between the variables b and d, so that d equals to the complement of b. Derivation of such local dependencies allows rapid derivation of non-local dependencies between variables.
The ability to capture non-local implications efficiently, in turn, allows contradictions in variable assignments during the backtracking procedure to be determined rapidly and early. That is, if during variable assignment it is noted that one dependency implies that a=1 and another dependency implies that a=0, then we have a contradiction, i.e., our variable assignment will not lead to a solution and we need to change the assignment.
A number of efficient algorithms have been proposed for SAT in the recent past. For example T. Larrabee, cited above, emphasized the advantage of SAT-based algorithms for automatic test pattern generation (ATPG). Significant enhancements to the basic SAT algorithm are described in S. Chakradhar et al., cited above, and in J. Silva and K. Sakallah,
GRASP-A New Search Algorithm for Satisfiability
, IEEE ACM International Conference on CAD-96, pages 220-227, November 1996 and P. Stephan, R. Brayton, and A. Sangiovanni-Vincentelli,
Combinational Test Generation Using Satisfiability
, IEEE Transactions on CAD, Vol. 15, No. 9, Pg 1167-1176, September 1996. In particular, Chakradhar et al. proposed techniques for efficiently deriving and using non-local implications, equivalences and contrapositives. On the other hand, Silva et al. proposed one key advance: a technique for realizing nonlinear backtracking in the SAT solver.
The means of expressing a problem in a conjunctive normal form differ depending on the problem domain. Once the problem has been mapped into the CNF formula, the SAT solver searches for a satisfying assignment for the variables of the CNF. Overall, the solution approach is to assign values to variables one by one, and determine whether their implications on the rest of the clauses in the formula leads to a contradiction. When variables have been assigned to all the variables and the CNF evaluates to one, the SAT has been solved.
However, if an assignment of a particular variable leads to a contradiction, the assignment needs to be changed, or the algorithm needs to backtrack and change a previous assignment(s). More specifically, if a contradiction occurs before the procedure is begun, it indicates that the CNF is unsolvable. If a contradiction occurs after some partial assignments, it indicates that the search can be stopped at that point for these partial assignments. That is, we know that some of the values assigned to variables are leading to a nonsensical solution.
Each step of the backtracking procedure involves two sub-parts. First, a variable to branch on is chosen and is assigned a value. Then the CNF formula is repeatedly updated based on the implications of this variable value until a stopping point is reached, i.e., all the implications have been satisfied or a contradiction occurred. If the second step leads to a contradiction, the search can be stopped at this point and the algorithm can backtrack.
In choosing a value for a variable, there are three possibilities: (a) it may have no value assigned to it at the point the choice is made, (b) the algorithm may be backtracking on the first assignment to the variable, or (c) the algorithm may be backtracking on the second assignment to the variable. In case (a) the algorithm can choose to assign either value (1 or 0) to the variable. In case (b), the algorithm must assign a value that is the opposite of the previous assignment. In case (c) the algorithm must backtrack to the previous variable in the search tree. The algorithm completes when either all the clauses are satisfied or when the search space is exhausted.
Various heuristics can be used to pick the next variable and value to branch on. A common strategy is to pick the literal that occurs in the largest number of clauses.
Consider the example in
FIG. 1
for which we need to determine a vector of sa
Ashar Pranav
Malik Sharad
Martonosi Margaret
Zhong Peixin
Do Thuan
NEC USA Inc.
Smith Matthew
Sughrue Mion Zinn Macpeak & Seas, PLLC
LandOfFree
Configurable hardware system implementing Boolean... does not yet have a rating. At this time, there are no reviews or comments for this patent.
If you have personal experience with Configurable hardware system implementing Boolean..., we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Configurable hardware system implementing Boolean... will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-2543952