Abstract
The developments of efficient SAT solvers have attracted tremendous research interest in recent years. The merits of these solvers are often compared in terms of their performance based upon a wide spread of benchmarks. In this paper, we extend an earlier-proposed solver design concept called (SCGL) Signal Correlation Guided Learning that is ATPG-based into a family of heuristics. Along with this SCGL family of heuristics, we classify benchmark examples according to their performance using the SCGL heuristics. With this study, we identify the class of problems that are uniquely suitable to be solved by using the SCGL approach. In particular, for solving difficult circuit-based problems at INTEL, our SCGL-based ATPG solver is able to achieve at least an order of magnitude speedup over the state-of-the-art SAT solvers. Our conclusion is that SCGL is an unique solver design concept that can complement heuristics proposed by others for solving circuit-oriented difficult problems.
| Original language | English |
|---|---|
| Pages (from-to) | 436-441 |
| Number of pages | 6 |
| Journal | Proceedings - Design Automation Conference |
| DOIs | |
| Publication status | Published - 2003 |
| Externally published | Yes |
| Event | Proceedings of the 40th Design Automation Conference - Anaheim, CA, United States Duration: 2 Jun 2003 → 6 Jun 2003 |
Keywords
- ATPG
- Boolean Equivalence Checking
- Boolean Satisfiability