Error detection/correction and fault detection/recovery – Pulse or data error handling – Digital logic testing
Reexamination Certificate
1998-12-10
2001-09-18
DeCady, Albert (Department: 2133)
Error detection/correction and fault detection/recovery
Pulse or data error handling
Digital logic testing
72
Reexamination Certificate
active
06292916
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). In applications involving combinational circuits, the 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, e.g., 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, for example, those involving complex very-large-scale integration (VLSI) circuits, can require many hours of computation using powerfill 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. Circuits implemented in reconfigurable hardware to facilitate SAT computation are referred to as “satisfiers.” Although existing satisfiers and other conventional techniques and devices have produced reductions in the computational complexity of SAT algorithms, additional improvements are needed to provide further improvements in the efficiency of the many CAD, test and other types of applications that utilize SAT.
SUMMARY OF THE INVENTION
The invention provides methods and apparatus for implementing a satisfiability algorithm on reconfigurable hardware. An illustrative embodiment of the invention is a parallel-backtrace satisfier which includes a controller, e.g., a synchronization unit, which directs the operation of clause logic, literal logic and variable logic for implementing logic functions associated with the processing of clauses, literals and variables, respectively, of a circuit to be analyzed. In the illustrative embodiment, enhanced parallelism is implemented using parallel backtracing of multiple objectives along multiple circuit paths from a primary output of the circuit toward its primary inputs. Further parallelism may be provided by, for example, providing concurrent assignments of several primary inputs. The clause logic, literal logic and variable logic may each be implemented using easily-scalable iterative logic array (ILA) structures which are made up of multiple cells, with each cell representative of a logic function associated with the processing of a corresponding clause, literal or variable of the circuit.
Compared to conventional SAT algorithms implemented in software, a parallel-backtrace satisfier with prioritized objectives and concurrent assignments significantly reduces the amount of search time required to solve the SAT problem, resulting in a computational speedup which may be as much as several orders of magnitude in certain applications. The invention also provides similar advantages relative to previous satisfiers implemented in reconfigurable hardware. Unlike previous satisfiers whose efficiency is limited by incorrect or unnecessary variable assignments, parallel-backtrace satisfiers in accordance with the invention can skip over variables whose assignment is unnecessary in the current state and select only the correct values for variables which become dynamically unate in the current state, i.e., have all their literals either complemented or not complemented in the current state.
REFERENCES:
patent: 4541071 (1985-09-01), Ohmori
patent: 4672307 (1987-06-01), Breuer et al.
patent: 5493239 (1996-02-01), Zlotnick
patent: 5572148 (1996-11-01), Lytle et al.
patent: 5831996 (1998-11-01), Abramovici et al.
patent: 6026222 (2000-02-01), Gupta et al.
patent: 6038392 (2000-03-01), Ashar et al.
patent: 6086626 (2000-06-01), Jain et al.
patent: 6131181 (2000-10-01), Bushnell et al.
patent: 0 759 662 A2 (1997-02-01), None
patent: 2 286 737 A (1995-08-01), None
patent: 2 304 438 A (1997-03-01), None
Abramovici, Miron; “Satisfiability on Reconfigurable Hardware,” Proceedings International Workshop on Field Programmable Logic and Applications, pp. 448-456, Sep. 1997.*
Zhong, Peixin; “Solving Boolean Satisfiability with Dynamic Hardware Configuration”, Proceedings International Workshop on Field Programmable Logic and Applications, pp. 326-335, 1998.*
Platzner, Marco “Acceleration of Satisfiability Algorithms by Reconfigurable Hardware”, Proceedings International Workshop on Field Programmable Logic and Applications, pp. 69-78, Sep. 1998.*
Rashid, Azra; “Dynamic Circuit Generation for Solving Specific problem Instances of Boolean Satisfiability”, Proceedings IEEE Symposium on Field Programmable Custom Computing Machines, pp. 196-203, Apr. 1998.*
Zhong, P.; “Accelerating Boolean Satisfiability with Configurable Hardware”, Proceedings IEEE Symposium on Field Programmable Custom Computing Machines, Apr. 1998.*
Silva, Joao; “GRASP—a new search algorithm for satisfiability”, Proceedigns of the 1996 IEEE/ACM International Conference on Computer-Aided Design, pp. 220-227.*
P. Zhong et al., “Accelerating Boolean Satisfiability with Configurable Hardware,”Proc. IEEE Symp. on Field-Programmable Custom Computing Machines, Apr. 1998.
P. Zhong et al., “Using Reconfigurable Computing Techniques to Accelerate Problems in CAD Domain: A Case Study with Boolean Satisfiability,” Proc. Design Automation Conf., Jun. 1998.
A. Rashid et al., “Dynamic Circuit Generation for Solving Specific Problem Instances of Boolean Satisfiability,” Proc. IEEE Symp. on Field-Programmable Custom Computing Machines, pp. 196-203, Apr. 1998.
H. Fujiwara et al., “On the Acceleration of Test Generation Algorithms,” IEEE Trans. on Computers, vol. C-32, No. 12, pp. 1137-1144, Dec. 1983.
M. Platzner et al., “Acceleration of Satisfiability algorithms by Reconfigurable Hardware, ” Proc. Intn'l. Workshop of Field-Programmable Logic and Applications, pp.69-78, Sep. 1998.
M. Abramovici et al., “Satisfiability on Reconfigurable Hardware,” Proc. Intn'l. Workshop of Field-Programmable Logic and Applications, pp. 448-456, Sep. 1997.
P. Zhong et al., “Solving Boolean Satisfiability with Dynamic Hardware Configurations,” Proc. Intn'l. Workshop on Field-Programmable Logic and Applications, pp. 326-335, 1998.
J.H. Mayer, “Reconfigurable computing redefines design flexibility,” Computer Design, pp. 49-52, Feb. 1997.
J. Rosenberg, “Implementing Cache Logic™ with FPGAs,” Atm
Abramovici Miron
De Sousa Jose T.
Saab Daniel G.
De'cady Albert
Lucent Technologies - Inc.
Ryan & Mason & Lewis, LLP
Torres Joseph D.
LandOfFree
Parallel backtracing for satisfiability on reconfigurable... does not yet have a rating. At this time, there are no reviews or comments for this patent.
If you have personal experience with Parallel backtracing for satisfiability on reconfigurable..., we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Parallel backtracing for satisfiability on reconfigurable... will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-2516536