Computer-aided design and analysis of circuits and semiconductor – Nanotechnology related integrated circuit design
Reexamination Certificate
1999-12-08
2002-07-02
Smith, Matthew S (Department: 2825)
Computer-aided design and analysis of circuits and semiconductor
Nanotechnology related integrated circuit design
C716S030000, C716S030000, C703S015000
Reexamination Certificate
active
06415430
ABSTRACT:
TECHNICAL FIELD OF THE INVENTION
This invention is related to determining if conflicting signals exist in a Boolean algorithm that represents a group of signals. More specifically, the invention is a method and apparatus for performing Boolean satisfiability testing on a Boolean algorithm using an apparatus that incorporates reconfigurable hardware in a pipelined architecture. The clauses of the Boolean algorithm are input into the reconfigurable hardware and implication and conflict analysis is performed of the variables constituting the Boolean algorithm. The invention also performs non-chronological backtracking on the variables if conflicts are uncovered. The invention is embodied in various methods, apparatuses, a hardware architecture, a computer system, and a computer program product that performs satisfiability testing on a Boolean algorithm.
BACKGROUND
The following references provide useful background information on the indicated topics, all of which relate to the invention, and are incorporated herein by reference.
Challenge Benchmarks:
DIMACS,
DIMACS Challenge Benchmarks and UCSC Benchmarks
, available at ftp://dimacs.rutgers.edu/pub/challenge/sat/benchmarks/cnf.
Use of reconfigurable hardware for satisfiability testing:
M. Abramovici and D. Saab,
Satisfiability on Reconfigurable Hardware
, Seventh International Workshop on Field Programmable Logic and Applications (1997).
Systolic processing systems:
J. Arnold, D. Buell and E. Davis,
Splash
2 (
Attached Processor Board
), Fourth Annual ACM Symposium on Parallel Algorithms and Architectures, pp. 316-322 (1992).
Virtual wiring between FPGAs:
J. Baab, R. Tessier and A. Agarwal,
Overcoming Pin Limitations In FPGA
-
Based Logic Emulators
, IEEE Workshop on FPGA-based Custom Computing Machines, pp. 142-151 (1993).
Combinational verification for equivalence checking:
J. Burch and V. Singhal,
Tight Integration Of Combinational Verification Methods
, Proceedings of ICCAD, pp. 570-576 (1998).
Test generation algorithm using transitive closure computation and decision making:
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, Vol. 12, No. 7, pp. 1015-28 (July 1993).
Uniform proof procedure for quantification theory:
M. Davis and H. Putnam,
A Computing Procedure for Quantification Theory
, Journal of the ACM, Vol. 7, pp. 201-215 (1960).
Path-Oriented Decision Making (PODEM) for combinational logic circuits:
P. Goel,
An Implicit Enumeration Algorithm To Generate Tests For Combinational Logic Circuits
, IEEE Transactions on Computers, Vol. C30, No. 3, pp. 337-343 (March 1981).
Reduction of problem size and backtrack requirements using binary decision diagrams coupled with a Boolean satisfiability checker:
A. Gupta and P. Ashar,
Integrating A Boolean Satisfiability Checker And BDDs For Combinational Verification
, Proceedings of VLSI Design 98, pp. 222-225 (1998).
Using the Boolean satisfiability method for generating test patterns for single stack-at faults in combinational circuits:
T. Larrabee,
Test Pattern Generation Using Boolean Satisfiability
, IEEE Transactions on Computer-Aided Design, Vol. 11, No. 1, pp. 4-15, (January 1992).
Augmentation of basic backtracking with conflict analysis:
J. Silva and K. Sakallah,
GRASP
-
A New Search Algorithm For Satisfiability
, Proceedings of ICCAD, pp. 220-227 (1996).
Using reduction to satisfiability for combinational logic test generation:
P. Stephan, R. Brayton and A. Sangiovanni-Vincentelli,
Combinational Test Generation Using Satisfiability
, IEEE Transactions on Integrated Circuits and Systems, Vol. 15, No. 9, pp. 1167-76 (September 1996).
Solving satisfiability problems using a specialized circuit to solve each problem instance on a FPGA:
T. Suyama, M. Yokoo and H. Sawada,
Solving Satisfiability Problems on FPGAs
, Sixth International Workshop on Field Programmable Logic and Applications (1996).
There will now be provided a discussion of various topics to provide a proper foundation for understanding the invention.
As illustrated by the literature, Boolean Satisfiability Checking (SAT) is at the core of many applications in computer-aided design (CAD) of very large scale integrated (VLSI) circuits. A number of techniques for accelerating SAT using FPGA-based (Field Programmable Gate Arrays) instance-specific reconfigurable hardware have been proposed in the literature. While significant speedups have been reported over software implementations of SAT for a number of examples, fundamental hurdles remain before this technology can be applied widely.
The first fundamental hurdle is the time overhead for compiling the hardware implementation of the algorithm on to FPGAs. This includes the times for mapping the logic netlist onto the Combinational Logic Blocks (CLB) of the FPGA and the time for place-and-route. In most cases, this combined time can actually be comparable to or greater than the time to actually solve the formula, even in software.
The second fundamental hurdle is that the level of sophistication in the hardware algorithm is not equal to the level of the best software algorithm. The hardware algorithm basically relies on raw parallelism to achieve the speedup. As a result, it is possible to find a number of examples for which the software implementation is faster or comparable because the software heuristics work very well. In previous hardware acceleration efforts for SAT, non-chronological backtracking has been incorporated into the hardware SAT algorithm. Another major feature that often speeds up the SAT solver considerably is the addition of clauses corresponding to solution subspaces that do not need to be explored. This feature is practically impossible to implement in previous architectures.
Another fundamental drawback is that previous architectures have led to much slower clock speeds than what is potentially achievable in FPGAs. The slow clock speeds are a result of the hardwired implementation of connections between literals leading to irregular layout, long wires and wires crossing FPGA boundaries.
The Boolean satisfiability problem is a well-known constraint satisfaction problem with many applications in computer-aided design, such as test generation, logic verification and timing analysis. Given a Boolean formula, the objective is either to find an assignment of 0-1 values to the variables so that the formula evaluates to true, or to establish that such an assignment does not exist.
The Boolean formula is typically expressed in conjunctive normal form (CNF), also called product-of-sums form. Each sum term (clause) in the CNF is a sum of single literals, where a literal is a variable or its negation. An n-clause is a clause with n literals. For example, v
i
+v′
j
+v
k
is referred to as a 3-clause. In order for the entire formula to evaluate to 1, each clause must be satisfied, i.e., evaluate to 1.
Most current SAT solvers are based on the Davis-Putnam algorithm. Referring to
FIG. 1
, pseudo code for the basic Davis-Putnam algorithm is shown. Referring to
FIG. 2
, the process flow for the basic Davis-Putnam algorithm is illustrated.
The basic algorithm begins from an empty partial assignment, as shown in Step S
100
. At Step S
110
, the algorithm determines if there are any free variables available. The algorithm proceeds by assigning a 0 or 1 value to one free variable at a time. After each assignment, at Step S
120
, the algorithm determines the direct and transitive implications of that assignment on other variables. In Step S
130
, the algorithm checks contradictions. At Step S
140
, if no contradictions are detected during the implication procedure, the algorithm picks the next free variable at Step S
150
, and repeats the procedure. Otherwise, the algorithm attempts a new partial assignment by complementing the most recently assigned variable for which only one value has been tried so far, as shown in Steps S
160
-S
180
. This step is called backtracking. The algorithm terminates when no free
Ashar Pranav
Martonosi Margaret
Zhong Peixin
Kik Phallaka
NEC USA Inc.
Smith Matthew S
LandOfFree
Method and apparatus for SAT solver architecture with very... does not yet have a rating. At this time, there are no reviews or comments for this patent.
If you have personal experience with Method and apparatus for SAT solver architecture with very..., we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Method and apparatus for SAT solver architecture with very... will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-2886441