Computer-aided design and analysis of circuits and semiconductor – Nanotechnology related integrated circuit design
Reexamination Certificate
2001-11-01
2003-11-18
Siek, Vuthe (Department: 2825)
Computer-aided design and analysis of circuits and semiconductor
Nanotechnology related integrated circuit design
C716S030000, C716S030000
Reexamination Certificate
active
06651234
ABSTRACT:
FIELD
This disclosure teaches novel techniques related to image computation. Specifically, techniques for decision heuristics for image computation using boolean satisfiability tests (SATs) and binary decision diagrams (BDDs) that are based on partitions are taught. The disclosed teachings are embodied in methods for image computation.
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., [3] for the third numbered paper by A Biere et al.):
[1] P. A. Abdulla, P. Bjesse, and N. Een. Symbolic reachability analysis based on SAT-solvers. In
Tools and Algorithms for the Analysis and Construction of Systems
(TACAS), 2000.
[2] E. Amir and S. McIlraith. Partition-based logical reasoning. In
Proc.
7
th International Conference on Principles of Knowledge Representation and Reasoning,
2000.
[3] 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 LNCS, 1999.
[4] R. K. Brayton et al. VIS: A system for verification and synthesis. In R. Alur and T. Henzinger, editors,
Proc. mt. Conf. on Comput.
-
Aided Verification
, volume 1102 of LNCS, pages 428-432, June 1996.
[5] R. E. Bryant. Graph-based algorithms for Boolean function manipulation.
IEEE Tran. on Comp
., C-35(8):677-691, August 1986.
[6] J. Burch and V. Singhal. Tight integration of combinational verification methods. In
Proc. Int. Conf. on Comput.
-
Aided Design
, pages 570-576, 1998.
[7] J. R. Burch, E. M. Clarke, D. E. Long, K. L. McMillan, and D. L. Dill. Symbolic model checking for sequential circuit verification.
IEEE Tran. on CAD of Integrated Circ. and Sys.,
13(4):401-424, Aprial 1994.
[8] G. Cabodi, P. Camurati, and S. Quer. Biasing symbolic search by means of dynamic activity profiles. In
Proc. Conference on Design Automation and Test Europe
(
DATE
), March 2001.
[9] P. Chauhan, E. M. Clarke, S. Jha, J. Kukula, T. Shiple, H. Veith, and D. Wang. Non-linear quantification scheduling in image computation. In
Proc. Int. Conf. on Comput.
-
Aided Design
, November 2001.
[10] E. M. Clarke, O. Grumberg, and D. Peled.
Model Checking
. MIT Press, 1999.
[11] O. Coudert, C. Berthet, and J. C. Madre. Verification of synchronous sequential machines using symbolic execution. In
Proc. Int. Workshop on Automatic Verification Methods for Finite State Systems
, volume 407 of LNCS, pages 365-373. Springer-Verlag, June 1989.
[12] A. Gupta and P. Ashar. Integrating a Boolean satisfiability checker and BDDs for combinational verification. In
Proc. VLSI Design Conference
, January 1998.
[13] A. Gupta, Z. Yang, A. Gupta, and P. Ashar. SAT-based image computation with application in reachability analysis. In
Proc. Conference on Formal Methods in Computer
-
Aided Design
, November 2000.
[14] G. Karypis et al. hMETIS: Serial hypergraph and circuit partitioning.
http://www-users.cs.umn.edu/
~
karypis/metis/hmetis.
[15] J. Kukula. When is SAT hard? Presented at Dagstuhl Seminar
Design and Test on BDDs versus SAT
, Schloss Dagstuhl, Germany, January 2001.
[16] T. Lengauer.
Combinatorial Algorithms for Integrated Circuit Layout
. John Wiley & Sons, England, 1990.
[17] J. P. Marques-Silva.
Search Algorithms for Satisfiability Problems in Combinational Switching Circuits
. PhD thesis, EEOS Department, University of Michigan, May 1995.
[18] 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.
[19] J. P. Marquez-Silva. Grasp package.
http://algos.inesc.pt/
~
jpms/software.html.
[20] I.-H. Moon, G. Haclitel, and F. Somenzi. Border-block triangular form and conjunction schedule in image computation. In
Proc. Conference on Formal Methods in Computer
-
Aided Design
, November 2000.
[21] I.-H. Moon, J. Kukula, K. Ravi, and F. Somenzi. To split or to conjoin: The question in image computation. In
Proc. Design Automation Conf
., pages 23-28, June 2000.
[22] M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an efficient SAT solver. In
Proc. Design Automation Conf
., June 2001.
[23] V. Paruthi and A. Kuehlmann. Equivalence checking combining a structural SAT-Solver, BDDs and simulation. In
Proc. Int. Conf on Comput. Design
, October 2000.
[24] M. R. Prasad, P. Chong, and K. Keutzer. Why is ATPG easy? In
Proc. Design Automation Conf
., pages 22-28, 1999.
[25] R. K. Ranjan, A. Aziz, R. K. Brayton, B. F. Plessier, and C. Pixley. Efficient BDD algorithms for FSM synthesis and verification. In
International Workshop for Logic Synthesis
, May 1995. Lake Tahoe, Calif.
[26] M. Sheeran, S. Singh, and G. Stalmarck. Checking safety properties using induction and a SAT-Solver. In
Proc. Conference on Formal Methods in Computer
-
Aided Design,
November 2000.
[27] F. Somenzi et al. CUDD: University of Colorado Decision Diagram Package.
mhttp://visi.colorado.eduefabio/CUDD/.
[28] H. Zhang. SATO: an efficient propositional prover. In
International Conference on Automated Deduction
, number 1249 in LNAI, pages 272-275, 1997.
2. Related Work
The Boolean satisfiability problem (SAT) has conventionally been used in many verification applications, such as equivalence checking [6, 12, 23], as well as model checking [1, 3, 26]. Combining SAT techniques with BDDs has also been conventionally shown to be effective for image computation with application in state reachability analysis of sequential circuits [13].
A typical implementation for solving SAT uses a branch-and-bound search over the values of all variables, with considerable sophistication in the software engineering of techniques for decision making, implication gathering, and back-tracking [19, 22, 28]. Since the SAT problem itself is NP-complete, the effectiveness of any algorithm for solving SAT depends upon the amount of pruning of the search space enabled by the SAT. In solving the SAT problem, decision heuristics are used to decide on the choice of which SAT variable to branch on at a given point in the solution. Such decision heuristics and their values, directly affect the amount of pruning.
Many SAT implementations use a Conjunctive Normal Form (CNF) representation of the Boolean formula associated with the SAT. This has led to the development of many decision heuristics based on the frequency of appearance of variables in unsatisfied (or all) clauses. In these decision heuristics, sometimes preference is given to smaller clauses in order to facilitate implications [17].
The present disclosure focuses on decision heuristics targeted at decomposing the overall problem into smaller, unrelated, partitions.
There have been some efforts in exploring the benefits of partitioning for generic SAT applications in CAD [18]. But, such efforts were restricted to the detection of partitions as they arise dynamically within the search, and no effort was made to actually derive such partitions. There has been some recent independent work on use of partitioning methods, including the use of separator-based partitioning, to improve the efficiency of the SAT solver [2]. However, this effort is not directly targeted at deriving good decision heuristics. In that work [2], the SAT problem is recursively partitioned into a tree of SAT subproblems using vertex separators as we do, but the manner in which they use the separators is completely different. Rather than deriving good decision heuristics based on the partitions, they find all solut
Ashar Pranav
Gupta Aarti
Malik Sharad
Yang Zijiang
Levin Naum
Siek Vuthe
LandOfFree
Partition-based decision heuristics for SAT and image... does not yet have a rating. At this time, there are no reviews or comments for this patent.
If you have personal experience with Partition-based decision heuristics for SAT and image..., we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Partition-based decision heuristics for SAT and image... will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-3179246