2012

 back to the year overview

• Bernd Becker, Ruediger Ehlers, Matthew Lewis, Paolo Marin
  ALLQBF Solving by Computational Learning
  2012 Automated Technology for Verification and Analysis, Springer, volume: 7561, pages: 370 - 384
  » show abstract« hide abstract
  Abstract

  In the last years, search-based QBF solvers have become essential formany applications in the formal methods domain. The exploitation oftheir reasoning efficiency has however been restricted to applicationsin which a ``satisfiable/unsatisfiable'' answer or one model of anopen quantified Boolean formula suffices as an outcome, whereasapplications in which a compact representation of all models isrequired could not be tackled with QBF solvers so far. In this paper,we describe how computational learning provides a remedy to thisproblem. Our algorithms employ a search-based QBF solver and learn theset of all models of a given open QBF problem in a CNF (conjunctivenormal form), DNF (disjunctive normal form), or CDNF (conjunction ofDNFs) representation. We evaluate our approach experimentally usingbenchmarks from synthesis of finite-state systems from temporal logicand monitor computation.
• Paolo Marin, Christian Miller, Matthew Lewis, Bernd Becker
  Verification of Partial Designs Using Incremental QBF Solving
  2012 Conf. on Design, Automation and Test in Europe, pages: 623 - 628
  » show abstract« hide abstract
  Abstract

  SAT solving is an indispensable core component of numerous formal verification tools and has found widespread use in industry, in particular when using it in an incremental fashion, e.g. in Bounded Model Checking (BMC). On the other hand, there are applications, in particular in the area of partial design verification, where SAT formulas are not expressive enough and a description via Quantified Boolean Formulas (QBF) is much more adequate.In this paper we introduce incremental QBF solving and thereby make it usable as a core component of BMC. To do so, we realized an incremental version of the state-of-the-art QBF solver QuBE, allowing for the reuse of learnt information e.g. in the form of conflict clauses and solution cubes. As an application we consider BMC for partial designs (i.e. designs containing so-called blackboxes) and thereby disprove realizability, that is, we prove that an unsafe state is reachable no matter how the blackboxes are implemented. In our experimental analysis, we compare different incremental approaches implemented in our BMC tool. BMC with incremental QBF turns out to be feasible for designs with more than 21,000 gates and 2,700 latches. Significant performance gains over non incremental QBF based BMC can be obtained on many benchmark circuits, in particular when using the so-called backward-incremental approach combined with incremental preprocessing.

2011

 back to the year overview

• Matthias Sauer, Victor Tomashevich, Jörg Müller, Matthew Lewis, Ilia Polian, Bernd Becker, Wolfram Burgard
  An FPGA-Based Framework for Run-time Injection and Analysis of Soft Errors in Microprocessors
  2011 IEEE Int'l Online Testing Symp., pages: 182 - 185
  » show abstract« hide abstract
  Abstract

  State-of-the-art cyber-physical systems are increasingly deployed in harsh environments with non-negligible soft error rates, such as aviation or search-and-rescue missions. State-of-the-art nanoscale manufacturing technologies are more vulnerable to soft errors. In this paper, we present an FPGA-based framework for injecting soft errors into user-specified memory elements of an entire microprocessor (MIPS32) running application software. While the framework is applicable to arbitrary software, we demonstrate its usage by characterizing soft errors effects on several software filters used in aviation for probabilistic sensor data fusion.
• Stefan Kupferschmid, Matthew Lewis, Tobias Schubert, Bernd Becker
  Incremental preprocessing methods for use in BMC
  2011 Formal Methods in System Design, volume: 39, pages: 185 - 204
  » show abstract« hide abstract
  Abstract

  . Unfortunately, many preprocessing techniques such as variable and (blocked) clause elimination cannot be directly used in an incremental manner. This work focuses on extending these techniques and Craig interpolation so that they can be used effectively together in incremental SAT solving (in the context of BMC). The techniques introduced here doubled the performance of our BMC solver on both SAT and UNSAT problems. For UNSAT problems, preprocessing had the added advantage that Craig interpolation was able to find the fixed point sooner, reducing the number of incremental SAT iterations. Furthermore, our ideas seem to perform better as the benchmarks become larger, and/or deeper, which is exactly when they are needed. Lastly, our methods can be integrated into other SAT based BMC tools to achieve similar speedups.
• Matthew Lewis, Paolo Marin, Tobias Schubert, Massimo Narizzano, Bernd Becker, Enrico Giunchiglia
  Parallel QBF Solving with Advanced Knowledge Sharing
  2011 Fundamenta Informaticae, volume: 107, issue: 2-3, pages: 139 - 166
  » show abstract« hide abstract
  Abstract

  In this paper we present the parallel QBF Solver PaQuBE. This new solver leverages the additional computational power that can be exploited from modern computer architectures, from pervasive multi-core boxes to clusters and grids, to solve more relevant instances faster than previous generation solvers. Furthermore, PaQuBE's progressive MPI based parallel framework is the first to support advanced knowledge sharing in which solution cubes as well as conflict clauses can be exchanged between solvers. Knowledge sharing plays a critical role in the performance of PaQuBE. However, due to the overhead associated with sending and receiving MPI messages, and the restricted communication/network bandwidth available between solvers, it is essential to optimize not only what information is shared, but the way in which it is shared. In this context, we compare multiple conflict clause and solution cube sharing strategies, and finally show that an adaptive method provides the best overall results.
• Matthew Lewis
  SAT, QBF, and Multicore Processors
  Der Andere Verlag, 2011

2010

 back to the year overview

• Stefan Kupferschmid, Matthew Lewis, Tobias Schubert, Bernd Becker
  Incremental Preprocessing Methods for use in BMC
  2010 Int'l Workshop on Hardware Verification
  » show abstract« hide abstract
  Abstract

  Traditional incremental SAT solvers have achieved great success in the domain of Bounded Model Checking (BMC). However, modern solvers depend on advanced preprocessing procedures to obtain high levels of performance. Unfortunately,many preprocessing techniques such as a variable and (blocked) clauseelimination cannot be directly used in an incremental manner. This work focuses on extending these techniques and Craig interpolation so that they can be used effectively together in incremental SAT solving (in the context of BMC). The techniques introduced here doubled the performance of our BMC solver onboth SAT and UNSAT problems. For UNSAT problems, preprocessing had the added advantagethat Craig interpolation was able to find the fixed point sooner,reducing the number of incremental SAT iterations. Furthermore, our ideas seem to perform better as the benchmarks become larger, and/or deeper, which is exactly when they are needed. Lastly, our methods can be extended to other SAT based BMC tools to achieve similar speedups.
• Tobias Nopper, Christian Miller, Matthew Lewis, Bernd Becker, Christoph Scholl
  SAT modulo BDD - A Combined Verification Approach for Incomplete Designs
  2010 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, volume: 13, pages: 107 - 116
• Christian Miller, Stefan Kupferschmid, Matthew Lewis, Bernd Becker
  Encoding Techniques, Craig Interpolants and Bounded Model Checking for Incomplete Designs
  2010 Theory and Applications of Satisfiability Testing, Springer, pages: 194 - 208
  » show abstract« hide abstract
  Abstract

  This paper focuses on bounded invariant checking for partially specified circuits – designs containing so-called blackboxes – using the well known 01X- and QBF-encoding techniques. For detecting counterexamples, modeling the behavior of a blackbox using 01X-encoding is fast, but rather coarse as it limits what problems can be verified. We introduce the idea of 01X-hardness, mainly the classification of problems for which this encoding technique does not provide any useful information about the existence of a counterexample. Furthermore, we provide a proof for 01X-hardness based on Craig interpolation, and show how the information contained within the Craig interpolant or unsat-core can be used to determine heuristically which blackbox outputs to model in a more precise way. We then compare 01X, QBF and multiple hybrid modeling methods. Finally, our total workflow along with multiple state-of-the-art QBF-solvers are shown to perform well on a range of industrial blackbox circuit problems.
• Alexander Czutro, Ilia Polian, Matthew Lewis, Piet Engelke, Sudhakar M. Reddy, Bernd Becker
  Thread-Parallel Integrated Test Pattern Generator Utilizing Satisfiability Analysis
  2010 International Journal of Parallel Programming, volume: 38, issue: 3-4, pages: 185 - 202
  » show abstract« hide abstract
  Abstract

  Efficient utilization of the inherent parallelism of multi-core architectures is a grand challenge in the field of electronic design automation (EDA). One EDA algorithm associated with a high computational cost is automatic test pattern generation (ATPG). We present the ATPG tool TIGUAN based on a thread-parallel SAT solver. Due to a tight integration of the SAT engine into the ATPG algorithm and a carefully chosen mix of various optimization techniques, multi-million-gate industrial circuits are handled without aborts. TIGUAN supports both conventional single-stuck-at faults and sophisticated conditional multiple stuck-at faults which allows to generate patterns for non-standard fault models. We demonstrate how TIGUAN can be combined with conventional structural ATPG to extract full benefit of the intrinsic strengths of both approaches.

2009

 back to the year overview

• Alejandro Czutro, Ilia Polian, Matthew Lewis, Piet Engelke, Sudhakar M. Reddy, Bernd Becker
  TIGUAN: Thread-parallel Integrated test pattern Generator Utilizing satisfiability ANalysis
  2009 Int'l Conf. on VLSI Design, pages: 227 - 232
• Paolo Marin, Matthew Lewis, Massimo Narizzano, Tobias Schubert, Enrico Giunchiglia, Bernd Becker
  Comparison of Knowledge Sharing Strategies in a Parallel QBF Solver
  2009 High-Performance Computing and Simulation Conference, pages: 161 - 167
• Matthew Lewis, Tobias Schubert, Bernd Becker
  DPLL-based Reasoning in a Multi-Core Environment
  2009 Int'l Workshop on Microprocessor Test and Verification
• Paolo Marin, Matthew Lewis, Tobias Schubert, Massimo Narizzano, Bernd Becker, Enrico Giunchiglia
  Evaluation of Knowledge Sharing Strategies in a Parallel QBF Solver
  2009 RCRA International Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion
• Tobias Schubert, Matthew Lewis, Bernd Becker
  PaMiraXT: Parallel SAT Solving with Threads and Message Passing
  2009 Journal on Satisfiability, Boolean Modeling, and Computation, volume: 6, pages: 203 - 222
• Matthew Lewis, Paolo Marin, Tobias Schubert, Massimo Narizzano, Bernd Becker, Enrico Giunchiglia
  PaQuBE: Distributed QBF Solving with Advanced Knowledge Sharing
  2009 Int'l Conf. on Theory and Applications of Satisfiability Testing, volume: 5584, pages: 509 - 523
• Matthew Lewis, Tobias Schubert, Bernd Becker
  QMiraXT - A Multithreaded QBF Solver
  2009 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”

2008

 back to the year overview

• Alejandro Czutro, Ilia Polian, Matthew Lewis, Piet Engelke, Sudhakar M. Reddy, Bernd Becker
  TIGUAN: Thread-parallel Integrated test pattern Generator Utilizing satisfiability ANalysis
  2008 edaWorkshop
• Bernd Becker, Marc Herbstritt, Natalia Kalinnik, Matthew Lewis, Juri Lichtner, Tobias Nopper, Ralf Wimmer
  Propositional Approximations for Bounded Model Checking of Partial Circuit Designs
  2008 IEEE Int'l Conf. on Computer Design, IEEE Computer Society Press, pages: 52 - 59
  » show abstract« hide abstract
  Abstract

  Bounded model checking of partial circuit designs enables the detection of errors even when the implementation of the design is not finished. The behavior of the missing parts can be modeled by a conservative extension of propositional logic, called 01X-logic. Then the transitions of the underlying (incomplete) sequential circuit under verification have to be represented adequately. In this work, we investigate the difference between a relation-oriented and a function-oriented approach for this issue. Experimental results on a large set of examples show that the function-oriented representation is most often superior w.\,r.\,t. (1) CPU runtime and (2) accuracy regarding the ability to find a counterexample, such that by using the function-oriented approach an increase of accuracy up to 210\% and a speed-up of the CPU runtime up to 390\% compared to the relation-oriented approach are achieved. But there are also relevant examples, e.\,g. a VLIW-ALU, for which the relation-oriented approach outperforms the function-oriented one by 300\% in terms of CPU-time, showing that both approaches are efficient for different scenarios.

2007

 back to the year overview

• Matthew Lewis, Tobias Schubert, Bernd Becker
  Multithreaded SAT Solving
  2007 ASP Design Automation Conf., pages: 926 - 921

2005

 back to the year overview

• Matthew Lewis, Tobias Schubert, Bernd Becker
  Speedup Techniques Utilized in Modern SAT Solvers - An Analysis in the MIRA Environment
  2005 Theory and Applications of Satisfiability Testing, Springer, volume: 3569, pages: 437 - 443
  » show abstract« hide abstract
  Abstract

  s 28.
• Sandip Kundu, Matthew Lewis, Ilia Polian, Bernd Becker
  A Soft Error Emulation System for Logic Circuits
  2005 GI/ITG Workshop “Testmethoden und Zuverlässigkeit von Schaltungen und Systemen”, pages: 10 - 14
  » show abstract« hide abstract
  Abstract

  In nanometer technologies, soft errors in logic circuits are increasingly important. Since the failure in time (FIT) rates for these circuits are very low, millions of test vectors are required for a realistic analysis of soft errors. This exceeds the capabilities of software simulation tools. We propose an FPGA emulation architecture that can apply millions of vectors within seconds. Comprehensive soft error profiling was done for ISCAS 89 circuits. Soft errors were assigned to four different classes, and their latency and recovery time were obtained. This information is useful for understanding the vulnerability of the system to soft errors and hardening it against such errors.
• Sandip Kundu, Matthew Lewis, Ilia Polian, Bernd Becker
  A Soft Error Emulation System for Logic Circuits
  2005 Conf. on Design of Circuits and Integrated Systems, page: 137
  » show abstract« hide abstract
  Abstract

  In nanometer technologies, soft errors in logic circuits are increasingly important. Since the failure in time (FIT) rates for these circuits are very low, millions of test vectors are required for a realistic analysis of soft errors. This exceeds the capabilities of software simulation tools. We propose an FPGA emulation architecture that can apply millions of vectors within seconds. Comprehensive soft error profiling was done for ISCAS 89 circuits. Soft errors were assigned to four different classes, and their latency and recovery time were obtained. This information is useful for understanding the vulnerability of the system to soft errors and hardening it against such errors.
• Tobias Schubert, Bernd Becker, Matthew Lewis
  PaMira - A Parallel SAT Solver with Knowledge Sharing
  2005 Int'l Workshop on Microprocessor Test and Verification, IEEE Computer Society, volume: 00, pages: 29 - 36
  » show abstract« hide abstract
  Abstract

  In this paper we describe PaMira, a powerful distributed SAT solver. PaMira is based on the highly optimized, sequential SAT engine Mira, incorporating all essential optimization techniques modern algorithms utilize to maximize performance. For the distributed execution an efficient work stealing method has been implemented. PaMira also employs the exchange of conflict clauses between the processes to guide the search more efficiently. We provide experimental results showing linear speedup on a multiprocessor environment with four AMD Opteron processors.

2004

 back to the year overview

• Matthew Lewis, Tobias Schubert, Bernd Becker
  Early Conflict Detection Based BCP for SAT Solving
  2004 Int'l Conf. on Theory and Applications of Satisfiability Testing, pages: 29 - 36
  » show abstract« hide abstract
  Abstract

  Abstract. This paper describes a new BCP algorithm that improves the performance of Chaff class solvers by reducing the total number of clauses the BCP procedure must evaluate. This is done by: detecting conflicts earlier; evaluating clauses better; and by increasing the controllability of the conflicts which the BCP procedure finds. Solvers like Limmat [10] include a simple Early Conflict Detection BCP (ECDB), however we introduce a new aggressive ECDB procedure and the MIRA solver that efficiently incorporates it while easily facilitating comparisons between ECDB modes. With the full ECDB procedure enabled, MIRA was able to reduce the number of evaluated clauses by 59% on average compared to the disabled ECDB version. This new procedure and other speedup techniques discussed here allow MIRA to solve problems 3.7 times faster on average than zChaff. Lastly, this paper shows how significant speedup can be attained relatively easily by incorporating a certain level of ECDB into other solvers.
• Matthew Lewis, Tobias Schubert, Bernd Becker
  Early Conflict Detection Based SAT Solving
  2004 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”

2003

 back to the year overview

• Matthew Lewis, S. Simmons
  A VLSI Implementation of a Cryptographic Processor
  2003 CCECE, volume: 2, pages: 821 - 826