Computer-aided design and analysis of circuits and semiconductor – Nanotechnology related integrated circuit design
Reexamination Certificate
2001-06-15
2002-12-17
Wong, Don (Department: 2825)
Computer-aided design and analysis of circuits and semiconductor
Nanotechnology related integrated circuit design
C716S030000
Reexamination Certificate
active
06496961
ABSTRACT:
FIELD
This disclosure teaches a technique for dynamically removing inactive clauses in a Boolean satisfiability checking (SAT) problem. While, specific example circuit types might be discussed to better understand the disclosed technique, the technique itself is applicable to any circuit analysis problem that uses SAT. The precise scope of the disclosed technique should be self-evident from the claims.
BACKGROUND
1. References
The following papers provide useful background information, for which they are incorporated herein by reference in their entirety, and are selectively referred to in the remainder of this disclosure by their accompanying reference numbers in square brackets (i.e., [2] for the second numbered paper by A. Biere et al.):
[1] M. Abramovici, M. A. Bruer, and A. D. Friedman. Digital Systems Testing and testable Design. Electrical Engineering, Communications and Signal Processing. Computer Science Press, New York, N.Y., 1990.
[2] A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Tools and Algorithms for the Analysis and Construction of Systems (TACAS), volume 1579 of Lecture Notes in Computer Science, 1999.
[3] R. K. Brayton et al. VIS: A system for verification and synthesis. In R. Alur and T. Henzinger, editors, Proceedings of the Internation Conference on Computer-Aided Verification, volume 1102 of Lecture Notes in Computer Science, pages 428-432, June 1996.
[4] R. E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C-35(8):677-691, August 1986.
[5]. Burch and V. Singhal. Tight integration of combinational verification methods. In Proceedings of the International Conference on Computer-Aided Design, pages 570-576, 1998.
[6]. R. Burch, E. M. Clarke, D. E. Long, K. L. McMillan, and D. L. Dill. Symbolic model checking for sequential circuit verification. IEEE Transactions on Computer-Aided Design, 13(4):401-424, April 1994.
[7] S. T. Chakradhar, V. D. Agrawal, and S. G. Rothweiler. A transitive closure algorithm for test generation. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 12(1): 1015-1028, July 1993.
[8] Coudert, J. C. Madre, and C. Berthet. Verifying temporal properties of sequential machines without building their state diagrams. In Proceedings of the International Conference on Computer-Aided Verification (CAV 90), volume 3 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, 1991.
[9] A. Gupta and P. Ashar. Integrating a Boolean satisfiability checker and BDDs for combinational verification. In Proceedings of the VLSI Design Conference, January 1998.
[10] A. Gupta, Z. Yang, A. Gupta, and P. Ashar. Sat-based image computation with application in reachability analysis. In Formal Methods in Computer-Aided Design, 2000.
[11] W. Kunz and D. Pradhan. Recursive learning: A new implication technique for efficient solutions to cad problems—test, verification and optimization. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 13(9):1143-1158, September 1994.
[12] T. Larrabee. Test pattern generation using Boolean satisfiability. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1l(l):4-15, January 1992.
[13] J. P. Marques-Silva and A. L. Oliveira. Improving satisfiability algorithms with dominance and partitioning. In IEEE/ACM International Workshop on Logic Synthesis, May 1997.
[14] J. P. Marques-Silva and K. A. Sakallah. Grasp: A new search algorithm for satisfiability. In Proceedings of the International Conference on Computer-Aided Design, pages 220-227, November 1996.
[15] J. P. Marquez-Silva. Grasp package. http://algos.inesc.pt/~jpms/software.html.
[16] I.-H. Moon, G. Hachtel, and F. Somenzi. Border-clock triangular form and conjunction schedule in image computation. In Proceedings of the Conference on Formal Methods in Computer-Aided Design, 2000.
[17] I.-H. Moon, J. Kukula, K. Ravi, and F Somenzi. To split or to conjoin: The question in image computation. In Proceedings of the Design Automation Conference, pages 23-28, June 2000.
[18] M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik. Engineering a (super?) efficient SAT solver. In Proceedings of the Design Automation Conference, 2001.
[19] M. Sheeran and G. Stalmark. A tutorial on Stalmark's method of propositional proof. Formal Methods in System Design, 16(1), 2000.
[20] O. Shtrichman. Tuning SAT checkers for bounded model checking. In proceedings of the International Conference on Computer-Aided Verification, 2000.
[21] F. Somenzi et al. CUDD: University of Colorado Decision Diagram Package. http://visi.colorado.edu/~fabio/CUDD/.
[22] H. Zhang. SATO: an efficient propositional prover. In International Conference on Automated Deduction, number 1249 in LNAI, pages 272-275, 1997.
2. Related Work
Checking Boolean Satisfiability (SAT) is required for a number of applications in VLSI CAD including combinational verification, Automatic Test Pattern Generation (ATPG), timing analysis, synthesis and, recently, reachability analysis and model checking. Acceleration of SAT can have significant impact in terms of improving the quality of these applications. SAT has received considerable attention in the recent past, focusing both on basic improvements in the SAT algorithms [7, 11, 14, 19], and on various applications like Automatic Test Pattern Generation (ATPG) [12], equivalence checking [5, 9], bounded model checking (BMC) [2]. Recently, combining SAT techniques with BDDs has been shown to be effective for image computation with application in state reachability analysis of sequential circuits [10].
Typical SAT solvers are based on a Davis-Putnam style branch-and-bound algorithm, and include considerable sophistication in heuristics for decision making, implication gathering, and backtracking [15, 18, 22]. However, missing from these efforts is exploitation of the fact that most SAT problems arising in VLSI CAD are derived from logic gate netlists. Logic gate netlists have some special properties related to how gates are connected together to realize circuit functionality. These include properties like the input-to-output flow of information, limitation on the fanout and fanin of each gate, and the connectivity and signal value dependence dynamically changing the controllability and observability of a gate. Such properties have not been exploited in conventional SAT packages.
On the other hand, circuit structure has been effectively utilized in many SAT applications, e.g., ATPG [1], BMC [20]. However, this utilization has been mostly application-specific. For example, justification/propagation frontiers in ATPG, and unrolled transition relations in BMC, are used for more effective decision heuristics in the associated SAT procedures.
While the technique disclosed herein provide a clear benefit to SAT algorithms, it is also important to put the disclosed ideas in the context of the large body of work in conventional combinational ATPG [1]. Unlike traditional SAT, conventional ATPG algorithms operate on data structures at the level of the circuit structure itself. As a result, all circuit information, including gate connectivity, is directly available to these algorithms. In-deed, dynamic detection of inactive circuit regions is performed by the justification-propagation operations, which are at the core of ATPG algorithms. However, there is no explicit removal of these inactive regions. In particular, the overhead of propagating values through inactive regions is not avoided.
In terms of detecting redundant clauses in a SAT formula, a recent effort [13] proposed the use of clause dominance in the inner loop of the SAT algorithm. Unfortunately, the effort required for de
Ashar Pranav
Gupta Aarti
Gupta Anubhav
Yang Zijiang
Lee Wilson
NEC USA Inc.
Sughrue & Mion, PLLC
Wong Don
LandOfFree
Dynamic detection and removal of inactive clauses in SAT... does not yet have a rating. At this time, there are no reviews or comments for this patent.
If you have personal experience with Dynamic detection and removal of inactive clauses in SAT..., we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Dynamic detection and removal of inactive clauses in SAT... will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-2989454