Sponsored By:
9C: Satisfiability and Applications
9C-1
| Title | Multithreaded SAT Solving |
| Author | *Matthew Lewis, Tobias Schubert, Bernd Becker (Albert-Ludwigs-University of Freiburg, Germany) |
| Abstract | This paper describes the multithreaded MiraXT SAT Solver which was designed to take advantage of current and future shared memory multiprocessor systems. The paper highlights design and implementation details that allow the multiple threads to run and cooperate efficiently. Results show that in single threaded mode, MiraXT compares well to other state of the art solvers on Industrial problems. In threaded mode, it provides cutting edge performance, as speedup is obtained on both SAT and UNSAT instances. |
| Slides (pdf file) | 9C-1 |
9C-2
| Title | Trace Compaction using SAT-based Reachability Analysis |
| Author | *Sean Safarpour, Andreas Veneris, Hratch Mangassarian (University of Toronto, Canada) |
| Abstract | In today's designs, when functional verification fails, engineers perform debugging using the provided error traces. Reducing the length of error traces can help the debugging task by decreasing the number of variables and clock cycles that must be considered. We propose a novel trace length compaction approach based on SAT-based reachability analysis. We develop procedures and algorithms using pre-image computation to efficiently traverse the state space and reduce the trace lengths. We further introduce a data structure used to store the visited states which is critical to the performance of the proposed approach. Experiments demonstrate the effectiveness of the reachability approach as approximately 75\% of the traces are reduced by one or two orders of magnitudes. |
| Slides (pdf file) | 9C-2 |
9C-3
| Title | Combinational Equivalence Checking Using Incremental SAT Solving, Output Ordering, and Resets |
| Author | *Stefan Disch, Christoph Scholl (University of Freiburg, Germany) |
| Abstract | Combinational equivalence checking is an essential task in circuit design. In this paper we focus on SAT based equivalence checking making use of incremental SAT techniques which are well known from their application in Bounded Model Checking. Based on an analysis of shared circuit structures we present heuristics which try to maximize the benefit from incremental SAT solving in this application by looking for good orders in which the equivalence of different circuit outputs is checked. Moreover, we present a reset strategy for situations where the benefit from the incremental SAT approach seems to decrease. Experimental results demonstrate that our novel method outperforms traditional methods significantly. |
| Slides (pdf file) | 9C-3 |
9C-4
| Title | Fixing Design Errors with Counterexamples and Resynthesis |
| Author | *Kai-hui Chang, Igor L. Markov, Valeria Bertacco (University of Michigan at Ann Arbor, United States) |
| Abstract | In this work we propose a new error-correction framework, called CoRe, which uses counterexamples, or bug traces, generated in verification to automatically correct errors in digital designs. CoRe is powered by two innovative resynthesis techniques, Goal-Directed Search (GDS) and Entropy-Guided Search (EGS), which modify the functionality of internal circuit's nodes to match the desired specification. We evaluate our solution to designs and errors arising during combinational equivalence checking, as well as simulation-based verification of digital systems. Compared with previously proposed techniques, CoRe is more powerful in that: (1) it can fix a broader range of error types because it does not rely on specific error models; (2) it derives the correct functionality from simulation vectors, hence not requiring golden netlists; and (3) it can be applied to a range of verification flows, including formal and simulation-based. |
| Slides (pdf file) | 9C-4 |