AVACS: Automatic Verification and Analysis of Complex Systems

Start/End of project

2016

 back to the year overview

• Karsten Scheibler, Dominik Erb, Bernd Becker
  Accurate CEGAR-based ATPG in Presence of Unknown Values for Large Industrial Designs
  2016 Conf. on Design, Automation and Test in Europe
  » show abstract« hide abstract
  Abstract

  Unknown values emerge during the design and test generation process as well as during later test application and system operation. They adversely affect the test quality by reducing the controllability and observability of internal circuit structures -- resulting in a loss of fault coverage. To handle unknown values, conventional test generation algorithms as used in state-of-the-art commercial tools, rely on n-valued algebras. However, n-valued algebras introduce pessimism as soon as X-values reconverge. Consequently, these algorithms fail to compute the accurate result. Therefore, this paper focuses on a new highly incremental CEGAR-based algorithm that overcomes these limitations and hence is completely accurate in presence of unknown values. It relies on a modified SAT-solver tailored to this specific problem. The experimental results for circuits with up to 2.400.000 gates show that this combination allows high accuracy and high scalability at the same time. Compared to a state-of-the-art commercial tool, the fault coverage could be increased significantly. Furthermore, the runtime is reduced remarkably compared to a QBF-based encoding of the problem.
• Karsten Scheibler, Dominik Erb, Bernd Becker
  Applying Tailored Formal Methods to X-ATPG
  2016 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”
  » show abstract« hide abstract
  Abstract

  When producing integrated circuits (ICs) one wants to know whether a manufactured IC works as expected and is free of physical defects. Basically, for combinational circuits, this is done by applying patterns to the circuit inputs and checking if the circuit outputs show the expected result. In case of sequential circuits, one concentrates on the combinational core of the circuit and treats the signal lines driven by flip-flops as additional (secondary) inputs. The job of automatic test pattern generation (ATPG) is to find such input patterns. Usually, these patterns are generated with respect to a fault-model. E.g. the stuck-at fault model assumes that a physical defect causes signal lines in a circuit to stay on a fixed logical value (logic-0 or logic-1). The aim is to find patterns for all possible fault locations. In SAT-based ATPG the circuit is transformed into two Boolean formulas F1 and F2. One formula describes the fault-free circuit and the second formula contains the fault-affected circuit (we consider one fault at a time). If (F1 XOR F2) is satisfiable a test pattern for the current fault under consideration is found. This is the basic principle of two-valued SAT-based ATPG and a very similar approach is used for combinational equivalence checking. However, usually, one can not assume full control of all sequential elements and primary inputs. Therefore, uninitialized flip-flops may occur in the design -- leading to binary but unknown values (X-values). Classically, these X-values are handled by three-valued logic (01X). But this introduces pessimism when X-values reconverge in the circuit. On the other hand, the expressiveness of QBF allows to encode the unknown values accurately -- but comes at the cost of much higher runtimes. Therefore, we presented in [1] an accurate SAT-based CEGAR approach for automatic test pattern generation (ATPG) in presence of X-values. This approach is tailored to and optimized for this specific problem class and could also be used for closely related topics such as equivalence checking in presence of X-values. Although the approach is similar to an existing CEGAR-based 2-QBF solving algorithm, we show that our method has up to 50x lower runtimes. This underlines that an efficient CNF-encoding of a problem together with the fastest available standard solver does not guarantee optimal performance. Tailoring the underlying formal methods to the target problem class may give remarkable speedups on top.
• Dominik Erb, Karsten Scheibler, Michael A. Kochte, Matthias Sauer, Hans-Joachim Wunderlich, Bernd Becker
  Mixed 01X-RSL-Encoding for Fast and Accurate ATPG with Unknowns
  2016 21st Asia and South Pacific Design Automation Conference
  » show abstract« hide abstract
  Abstract

  Unknown (X) values in a design introduce pessimism in conventional test generation algorithms, which results in a loss of fault coverage. This pessimism is reduced by a more accurate modeling and analysis. Unfortunately, accurate analysis techniques highly increase runtime and limit scalability. One promising technique to prevent high runtimes while still providing high accuracy is the use of restricted symbolic logic (RSL). However, also pure RSL-based algorithms reach their limits as soon as millon gate circuits need to be processed. In this paper, we propose new ATPG techniques to overcome such limitations. An efficient hybrid encoding combines the accuracy of RSL-based modeling with the compactness of conventional three-valued encoding. A low-cost two-valued SAT-based untestability check is able to classify most untestable faults with low runtime. An incremental and event-based accurate fault simulator is introduced to reduce fault simulation effort. The experiments demonstrate the effectiveness of the proposed techniques. On average, over 99.3% of the faults are accurately classified. Both the number of aborts and the total runtime are significantly reduced compared to the state-of-the-art pure RSL-based algorithm. For circuits up to a million gates, the fault coverage could be increased considerably compared to a state-of-the-art commercial tool with very competitive runtimes.

2015

 back to the year overview

• Karsten Scheibler, Dominik Erb, Bernd Becker
  Improving Test Pattern Generation in Presence of Unknown Values beyond Restricted Symbolic Logic
  2015 to be published at European Test Symposium (ETS)
  » show abstract« hide abstract
  Abstract

  Test generation algorithms considering unknown (X) values are pessimistic if standard n-valued logic algebras are used. This results on an overestimation of the number of signals with X-values and an underestimation of the fault coverage. In contrast, algorithms based on quantified Boolean formula (QBF), are accurate in presence of X-values but have limits with respect to runtime, scalability and robustness. Recently, an algorithm based on restricted symbolic logic (RSL) has been presented which is more accurate than classical three-valued logic and faster than QBF. Nonetheless, this RSL-based approach is still pessimistic and is unable to detect all testable faults. Additionally, it does not allow the accurate identification of untestable faults. In this paper, we improve test generation based on RSL in two directions in order to reduce the gap to QBF further. First, we present techniques to go beyond the accuracy of RSL when generating test patterns. Second, we include a check which is able to accurately identify untestable faults. Experimental results show the high efficiency of the proposed method classifying almost all faults as testable or proving untestability.
• Dominik Erb, Karsten Scheibler, Matthias Sauer, Sudhakar M. Reddy, Bernd Becker
  Multi-Cycle Circuit Parameter Independent ATPG for Interconnect Open Defects
  2015 33rd VLSI Test Symposium (VTS)
  » show abstract« hide abstract
  Abstract

  Interconnect opens are known to be one of the predominant defects in nanoscale technologies. Generating tests to detect such defects is challenging due to the need to accurately determine the coupling capacitances between the open net and its aggressors and fix the state of these aggressors during test. Process variations cause deviations from assumed values of circuit parameters thus potentially invalidating tests generated with assumed circuit parameters. Additionally, recent investigation using test chips showed that the steady state voltage on open nets may drift slowly with the application of circuit inputs and can be different at different nets. Recently we proposed a class of tests called Circuit Parameter Independent (CPI) tests to detect interconnect opens and reported on an implementation of a test generator for them. CPI tests detect opens independent of the values of coupling capacitances and the initial trapped charge on the open net and hence are robust against process variations affecting these parameters. Yet, this work did not address the effects of leakage currents on open nets. In this work we extend the validity of CPI tests by introducing so-called multi-cycle CPI tests and single-value CPI tests. By doing so, we significantly improve the coverage of open defects and ensure their detection whilst including the additional effect of leakage currents on opens. Experimental results for circuits with over 500k non-equivalent faults and several thousand aggressors %deriving the new classes of CPI tests show the effectiveness of the newly proposed CPI tests as well as the high efficiency of a new ATPG algorithm to generate these new classes of CPI tests.
• Karina Gitina, Ralf Wimmer, Sven Reimer, Matthias Sauer, Christoph Scholl, Bernd Becker
  Solving DQBF Through Quantifier Elimination
  2015 Conf. on Design, Automation and Test in Europe
• Karsten Scheibler, Leonore Winterer, Ralf Wimmer, Bernd Becker
  Towards Verification of Artificial Neural Networks
  2015 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”
  » show abstract« hide abstract
  Abstract

  We consider the safety verification of controllers obtained via machine learning. This is an important problem as the employed machine learning techniques work well in practice, but cannot guarantee safety of the produced controller, which is typically represented as an artificial neural network. Nevertheless, such methods are used in safety-critical environments. In this paper we take a typical control problem, namely the Cart Pole System (a.k.a. inverted pendulum), and a model of its physical environment and study safety verification of this system. To do so, we use bounded model checking (BMC). The created formulas are solved with the SMT-solver iSAT3. We examine the problems that occur during solving these formulas and show that extending the solver by special deduction routines can reduce both memory consumption and computation time on such instances significantly. This constitutes a first step towards verification of machine-learned controllers, but a lot of challenges remain.

2014

 back to the year overview

• Dominik Erb, Karsten Scheibler, Matthias Sauer, Sudhakar M. Reddy, Bernd Becker
  Circuit Parameter Independent Test Pattern Generation for Interconnect Open Defects
  2014 23nd IEEE Asian Test Symposium (ATS)
  » show abstract« hide abstract
  Abstract

  Open defects such as interconnect opens are known to be one of the predominant defects in nanoscale technologies. Yet, test pattern generation for open defects is challenging because of the high number of parameters which need to be considered. Additionally, the assumed values of these parameters may vary due to process variations reducing fault coverage of a test set generated under this assumption. This paper presents a new ATPG approach for circuit parameter independent (CPI) tests. In addition a definition of oscillation free CPI tests is given. The generated tests are robust against process variations affecting the influence of neighboring interconnects as well as trapped charge and prohibit oscillating behavior. Experimental results show the high efficiency of the new approach, generating CPI tests for circuits with over 500k nonequivalent faults and several thousand aggressors.
• Sven Reimer, Matthias Sauer, Tobias Schubert, Bernd Becker
  Incremental Encoding and Solving of Cardinality Constraints
  2014 International Symposium on Automated Technology for Verification and Analysis, Springer International Publishing, volume: 8837, pages: 297 - 313
  » show abstract« hide abstract
  Abstract

  Traditional SAT-based MaxSAT solvers encode cardinality constraints directly as part of the CNF and solve the entire optimization problem by a sequence of iterative calls of the underlying SAT solver. The main drawback of such approaches is their dependence on the number of soft clauses: The more soft clauses the MaxSAT instance contains, the larger is the CNF part encoding the cardinality constraints. To counter this drawback, we introduce an innovative encoding of cardinality constraints: Instead of translating the entire and probably bloated constraint network into CNF, a divide-and-conquer approach is used to encode partial constraint networks successively. The resulting subproblems are solved and merged incrementally, reusing not only intermediate local optima, but also additional constraints which are derived from solving the individual subproblems by the back-end SAT solver. Extensive experimental results for the last MaxSAT evaluation benchmark suitew demonstrate that our encoding is in general smaller compared to existing methods using a monolithic encoding of the constraints and converges faster to the global optimum.
• Sven Reimer, Matthias Sauer, Paolo Marin, Bernd Becker
  QBF with Soft Variables
  2014 International Workshop on Automated Verification of Critical Systems (AVOCS)
• Matthias Sauer, Sven Reimer, Sudhakar M. Reddy, Bernd Becker
  Efficient SAT-based Circuit Initialization for Large Designs
  2014 Int'l Conf. on VLSI Design
  » show abstract« hide abstract
  Abstract

  We present a procedure to determine initialization sequences for a sequential circuit optimizing sequence length and unknown values (Xes) in the flip-flops. Specifically, we consider the following two problems: (1) Determine a sequence that initializes a maximal set of flip-flops starting in a completely unknown state. (2) Determine a minimal subset of flip-flops that need to be controllable such that the circuit can be completely initialized in a limited number of time frames. The underlying principle of our methods is a maximization formalism using formal optimization techniques based on satisfiability solvers (MaxSAT). We introduce several heuristics which increase the scalability of our approach significantly. Experimental results demonstrate the applicability of the method for large academic and industrial benchmark circuits with up to a few hundred thousand gates.
• Dominik Erb, Karsten Scheibler, Matthias Sauer, Bernd Becker
  Efficient SMT-based ATPG for Interconnect Open Defects
  2014 Conf. on Design, Automation and Test in Europe
  » show abstract« hide abstract
  Abstract

  Interconnect opens are known to be one of the predominant defects in nanoscale technologies. However, automatic test pattern generation for open faults is challenging, because of their rather unstable behaviour and the numerous electric parameters which need to be considered. Thus, most approaches try to avoid accurate modeling of all constraints and use simplified fault models in order to detect as many faults as possible or make assumptions which decrease both complexity and accuracy. This paper presents a new SMT-based approach which for the first time supports the Robust Enhanced Aggressor Victim model without restrictions and handles oscillations. It is combined with the first open fault simulator fully supporting the Robust Enhanced Aggressor Victim model and thereby accurately considering unknown values. Experimental results show the high efficiency of the new method outperforming previous approaches by up to two orders of magnitude.
• Karsten Scheibler, Bernd Becker
  Implication Graph Compression inside the SMT Solver iSAT3
  2014 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”
  » show abstract« hide abstract
  Abstract

  The iSAT algorithm aims at solving boolean combinations of linear and non-linear arithmetic constraint formulas (including transcendental functions), and thus is suitable to verify safety properties of systems consisting of both, linear and non-linear behaviour. The iSAT algorithm tightly integrates interval constraint propagation into the conflict-driven clause-learning framework. During the solving process, this may result in a huge implication graph. This paper presents a method to compress the implication graph on-the-fly. Experiments demonstrate that this method is able to reduce the overall memory footprint up to an order of magnitude.
• Dominik Erb, Karsten Scheibler, Michael Kochte, Matthias Sauer, Hans-Joachim Wunderlich, Bernd Becker
  Test Pattern Generation in Presence of Unknown Values Based on Restricted Symbolic Logic
  2014 Int'l Test Conf.
  » show abstract« hide abstract
  Abstract

  Test generation algorithms based on standard n- valued logic algebras are pessimistic in presence of unknown values, overestimate the number of signals with X-values and underestimate fault coverage. Recently, an ATPG algorithm based on quantified Boolean formula (QBF) has been presented, which is accurate in presence of X-values but has limits with respect to runtime, scalability and robustness. In this paper, we consider ATPG based on restricted symbolic logic (RSL) and demonstrate its potential. We introduce a complete RSL ATPG exploiting the full potential of RSL in ATPG. Experimental results demonstrate that RSL ATPG significantly increases fault coverage over classical algorithms and provides results very close to the accurate QBF-based algorithm. An optimized version of RSL ATPG (together with accurate fault simulation) is up to 618x faster than the QBF-based solution, more scalable and more robust.
• Karsten Scheibler, Bernd Becker
  Using Interval Constraint Propagation for Pseudo-Boolean Constraint Solving
  2014 Formal Methods in Computer-Aided Design
  » show abstract« hide abstract
  Abstract

  This work is motivated by (1) a practical application which automatically generates test patterns for integrated circuits and (2) the observation that off-the-shelf state-of-the-art pseudo-Boolean solvers have difficulties in solving instances with huge pseudo-Boolean constraints as created by our application. Derived from the SMT solver iSAT3 we present the solver iSAT3p that on the one hand allows the efficient handling of huge pseudo-Boolean constraints with several thousand summands and large integer coefficients. On the other hand, experimental results demonstrate that at the same time iSAT3p is competitive or even superior to other solvers on standard pseudo-Boolean benchmark families.
• Sven Reimer, Matthias Sauer, Tobias Schubert, Bernd Becker
  Using MaxBMC for Pareto-Optimal Circuit Initialization
  2014 Conf. on Design, Automation and Test in Europe
  » show abstract« hide abstract
  Abstract

  In this paper we present MaxBMC, a novel formalism for solving optimization problems in sequential systems. Our approach combines techniques from symbolic SAT-based Bounded Model Checking (BMC) and incremental MaxSAT, leading to the first MaxBMC solver. In traditional BMC safety and liveness properties are validated. We extend this formalism: in case the required property is satisfied, an optimization problem is defined to maximize the quality of the reached witnesses. Further, we compare its qualities in different depths of the system, leading to Pareto-optimal solutions. We state a sound and complete algorithm that not only tackles the optimization problem but moreover verifies whether a global optimum has been identified by using a complete BMC solver as back-end. As a first reference application we present the problem of circuit initialization. Additionally, we give pointers to other tasks which can be covered by our formalism quite naturally and further demonstrate the efficiency and effectiveness of our approach.

2013

 back to the year overview

• Ulrich Loup, Karsten Scheibler, Florian Corzilius, Erika Ábrahám, Bernd Becker
  A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition
  2013 CADE, Springer, volume: 7898, pages: 193 - 207
  » show abstract« hide abstract
  Abstract

  We present a novel decision procedure for non-linear real arithmetic: a combination of iSAT, an incomplete SMT solver based on interval constraint propagation (ICP), and an implementation of the complete cylindrical algebraic decomposition (CAD) method in the library GiNaCRA. While iSAT is efficient in finding unsatisfiability, on satisfiable instances it often terminates with an interval box whose satisfiability status is unknown to iSAT. The CAD method, in turn, always terminates with a satisfiability result. However, it has to traverse a double-exponentially large search space. A symbiosis of iSAT and CAD combines the advantages of both methods resulting in a fast and complete solver. In particular, the interval box determined by iSAT provides precious extra information to guide the CAD-method search routine: We use the interval box to prune the CAD search space in both phases, the projection and the construction phase, forming a search `tube' rather than a search tree. This proves to be particularly beneficial for a CAD implementation designed to search a satisfying assignment pointedly, as opposed to search and exclude conflicting regions.
• Matthias Sauer, Sven Reimer, Stefan Kupferschmid, Tobias Schubert, Paolo Marin, Bernd Becker
  Applying BMC, Craig Interpolation and MAX-SAT to Functional Justification in Sequential Circuits
  2013 RCRA International Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion
  » show abstract« hide abstract
  Abstract

  We present an approach to identify functional input sequences in sequential circuits. The properties required are inserted as target of a bounded model checking (BMC) problem, by using Craig interpolants it can be stated whether sequences justifying the properties exist or not. The initial state is either completely or partially unknown, and for the latter we engage a MAX-SAT formulation to retrieve the shortest sequence if a maximal subset of the initial state bits are unknown. We apply this method to problems arising from digital circuit testing domain, in which usually an arbitrary initial state is assumed, i.e., that the circuit’s sequential elements (flip-flops) are assumed to be fully con- trollable. However, since some of these states may be unreachable during normal operation, this results in undesired secondary test conditions. In this paper BMC is used to (1) test timing faults in a digital circuit, thereby the test requirements are encoded as target properties. Our method yields the shortest functional test-sequences that justify the target properties or it proves that such a sequence does not exist. Furthermore, (2) the initialization of circuits is considered. We analyze the length of such sequences depending on the number of controllable flip-flops.
• Karsten Scheibler, Matthias Sauer, Kohei Miyase, Bernd Becker
  Controlling Small-Delay Test Power Consumption using Satisfibility Modulo Theory Solving
  2013 GI/ITG Workshop “Testmethoden und Zuverlässigkeit von Schaltungen und Systemen”
  » show abstract« hide abstract
  Abstract

  Exaggerated power consumption during test mode is a major issue in today's nanoscale circuits and can lead to a significant amount of overtesting and hence yield loss. We present a method that yields two-pattern tests sensitizing long paths while at the same time minimizing weighted switching activity. Experimental results on standard benchmark circuits demonstrate the applicability of the method.
• Matthias Sauer, Sven Reimer, Tobias Schubert, Ilia Polian, Bernd Becker
  Efficient SAT-Based Dynamic Compaction and Relaxation for Longest Sensitizable Paths
  2013 Conf. on Design, Automation and Test in Europe, pages: 448 - 453
  » show abstract« hide abstract
  Abstract

  Comprehensive coverage of small-delay faults under massive process variations is achieved when multiple paths through the fault locations are sensitized by the test pair set. Using one test pair per path may lead to impractical test set sizes and test application times due to the large number of near-critical paths in state-of-the-art circuits.
• Karina Gitina, Sven Reimer, Matthias Sauer, Ralf Wimmer, Christoph Scholl, Bernd Becker
  Equivalence Checking for Partial Implementations Revisited
  2013 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, Universität Rostock ITMZ, pages: 61 - 70
  » show abstract« hide abstract
  Abstract

  In this paper we consider the problem of checking whether a partial implementation can (still) be extended to a complete design which is equivalent to a given full specification. In particular, we investigate the relationship between the equivalence checking problem for partial implementations (PEC) and the validity problem for quantified boolean formulae (QBF) with so-called Henkin quantifiers. Our analysis leads us to a sound and complete algorithmic solution to the PEC problem as well as to an exact complexity theoretical classification of the problem.
• Karina Gitina, Sven Reimer, Matthias Sauer, Ralf Wimmer, Christoph Scholl, Bernd Becker
  Equivalence Checking of Partial Designs using Dependency Quantified Boolean Formulae
  2013 Int'l Conf. on Computer Design, IEEE Computer Society, pages: 396 - 403
  » show abstract« hide abstract
  Abstract

  We consider the partial equivalence checking problem (PEC), i.e., checking whether a given partial implementation of a combinational circuit can (still) be extended to a complete design that is equivalent to a given full specification. To solve PEC, we give a linear transformation from PEC to the question whether a dependency quantified Boolean formula (DQBF) is satisfied. Our novel algorithm to solve DQBF based on quantifier elimination can therefore be applied to solve PEC. We also present first experimental results showing the feasibility of our approach and the inaccuracy of QBF approximations, which are usually used for deciding the PEC so far.
• Matthias Sauer, Sven Reimer, Ilia Polian, Tobias Schubert, Bernd Becker
  Provably Optimal Test Cube Generation Using Quantified Boolean Formula Solving
  2013 ASP Design Automation Conf.
  » show abstract« hide abstract
  Abstract

  Circuits that employ test pattern compression rely on test cubes to achieve high compression ratios. The less inputs of a test pattern are specified, the better it can be compacted and hence the lower the test application time. Although there exist previous approaches to generate such test cubes, none of them are optimal. We present for the first time a framework that yields provably optimal test cubes by using the theory of quantified Boolean formulas (QBF). Extensive comparisons with previous methods demonstrate the quality gain of the proposed method.
• Karsten Scheibler, Stefan Kupferschmid, Bernd Becker
  Recent Improvements in the SMT Solver iSAT
  2013 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”
  » show abstract« hide abstract
  Abstract

  Over the past decades embedded systems have become more and more complex. Furthermore, besides digital components they now often contain additional analog parts -- making them to embedded hybrid systems. If such systems are used in safety critical environments, a formal correctness proof is highly desirable. The SMT solver iSAT aims at solving boolean combinations of linear and non-linear constraint formulas (including transcendental functions), and thus is suitable to verify safety properties of systems consisting of both, linear and non-linear behaviour. To keep up with the ever increasing complexity of these systems we present recent improvements in various parts of iSAT. Experiments demonstrate that iSAT with all the presented improvements integrated typically gains a speedup between one and two orders of magnitude.
• Der Andere Verlag, page: 266
  Über Craigsche Interpolation und deren Anwendung in der formalen Modellprüfung
  ISBN: 978-3-86247-411-0
  Stefan Kupferschmid

2012

 back to the year overview

• Sven Reimer, Florian Pigorsch, Christoph Scholl, Bernd Becker
  Enhanced Integration of QBF Solving Techniques
  2012 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, pages: 133 - 143
  » show abstract« hide abstract
  Abstract

  In this paper we present a novel QBF solving technique which is based on the integration of a search based (DPLL) and a rewriting based approach: While traversing the search space in a DPLL manner, we iteratively generate many sub-problems, which are handed over to the rewriting method one by one. Instead of just communicating back satisfiability results of the individual sub-problems, we collect as many constraints derived by the rewriting based solver as possible, and transfer them back to the search based solver. This allows not only to prune the current branch, but also to avoid the unnecessary traversal of search paths in different regions of the search tree. We also discuss heuristics to determine suitable switching points between these two methods. We present first promising results that underline the potential of our approach.
• Matthias Sauer, Stefan Kupferschmid, Alexander Czutro, Sudhakar M. Reddy, Bernd Becker
  Analysis of Reachable Sensitisable Paths in Sequential Circuits with SAT and Craig Interpolation
  2012 Int'l Conf. on VLSI Design
  » show abstract« hide abstract
  Abstract

  Test pattern generation for sequential circuits benefits from scanning strategies as these allow the justification of arbitrary circuit states. However, some of these states may be unreachable during normal operation. This results in non-functional operation which may lead to abnormal circuit behaviour and result in over-testing. In this work, we present a versatile approach that combines a highly adaptable SAT-based path-enumeration algorithm with a model-checking solver for invariant properties that relies on the theory of Craig interpolants to prove the unreachability of circuit states. The method enumerates a set of longest sensitisable paths and yields test sequences of minimal length able to sensitise the found paths starting from a given circuit state. We present detailed experimental results on the reach ability of sensitisable paths in ITC 99 circuits.
• Matthias Sauer, Stefan Kupferschmid, Alexander Czutro, Ilia Polian, Sudhakar M. Reddy, Bernd Becker
  Functional Justification in Sequential Circuits using SAT and Craig Interpolation
  2012 GI/ITG Workshop “Testmethoden und Zuverlässigkeit von Schaltungen und Systemen”
• Matthias Sauer, Stefan Kupferschmid, Alexander Czutro, Ilia Polian, Sudhakar M. Reddy, Bernd Becker
  Functional Test of Small-Delay Faults using SAT and Craig Interpolation
  2012 Int'l Test Conf., pages: 1 - 8
  » show abstract« hide abstract
  Abstract

  We present SATSEQ, a timing-aware ATPG system for small-delay faults in non-scan circuits. The tool identifies the longest paths suitable for functional fault propagation and generates the shortest possible sub-sequences per fault. Based on advanced model-checking techniques, SATSEQ provides detection of small-delay faults through the longest functional paths. All test sequences start at the circuit's initial state; therefore, overtesting is avoided. Moreover, potential invalidation of the fault detection is taken into account. Experimental results show high detection and better performance than scan testing in terms of test application time and overtesting-avoidance.

2011

 back to the year overview

• Stefan Kupferschmid, Bernd Becker
  Craig interpolation in the presence of non-linear constraints
  2011 Formal Modeling and Analysis of Timed Systems, Springer, pages: 240 - 255
  » show abstract« hide abstract
  Abstract

  An increasing number of applications in particular in the verification area leverages Craig interpolation. Craig interpolants (CIs) can be computed for many different theories such as: propositional logic, linear inequalities over the reals, and the combination of the preceding theories with uninterpreted function symbols. To the best of our knowledge all previous tools that provide CIs are addressing decidable theories. With this paper we make Craig interpolation available for an in general undecidable theory that contains Boolean combinations of linear and non-linear constraints including transcendental functions like $\sin(\cdot)$ and $\cos(\cdot)$. Such formulae arise e.g.~during the verification of hybrid systems. We show how the construction rules for CIs can be extended to handle non-linear constraints. To do so, an existing SMT solver based on a close integration of SAT and Interval Constraint Propagation is enhanced to construct CIs on the basis of proof trees. We provide first experimental results demonstrating the usefulness of our approach: With the help of Craig interpolation we succeed in proving safety in cases where the basic solver could not provide a complete answer. Furthermore, we point out the (heuristic) decisions we made to obtain suitable CIs and discuss further possibilities to increase the flexibility of the CI construction.
• Stefan Kupferschmid, Bernd Becker
  Craigsche Interpolation für Boolesche Kombinationen linearer und nichtlinearer Ungleichungen
  2011 OFFIS-Institut für Informatik, pages: 279 - 288
  » show abstract« hide abstract
  Abstract

  Die vorliegende Arbeit behandelt die Berechnung Craigscher Interpolanten für beliebige boolesche Kombinationen linearer und nichtlinearer Gleichungen, einschließlich transzendenter Funktionen wie sin(x) und cos(x). Craigsche Interpolanten sind in der computergestützten Verifikation weit verbreitet und können für viele verschiedene Theorien berechnet werden, zum Beispiel: Aussagenlogik, lineare Arithmetik über rationale Zahlen sowie die Theorie mit uninterpretierten Funktionsymbolen. Nach bestem Wissen berechnen alle uns bekannten Interpolationsprogramme Craigsche Interpolanten für entscheidbare Theorien. In dieser Arbeit stellen wir einen Ansatz vor, der für eine im Allgemeinem nicht entscheidbare Theorie Craigsche Interpolanten berechnen kann. Wir erlauben neben linearen und nichtlinearen Gleichungen auch transzendente Funktionen. Solche Formeln entstehen bei der Analyse und Verifikation hybrider Systeme. Der in dieser Arbeit vorgestellte Ansatz wurde mithilfe des Sat-Modulo-Theorie Solvers iSAT implementiert. Erste Ergebnisse zeigen, dass Craigsche Interpolanten bei der Verifikation solcher Systeme erfolgreich eingesetzt werden können.
• 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

  Traditional incremental SAT solvers have achieved great success in the domain of Bounded Model Checking (BMC). Recently, modern solvers have introduced advanced preprocessing procedures that have allowed them to obtain high levels of performance. 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.
• Sven Reimer, Florian Pigorsch, Christoph Scholl, Bernd Becker
  Integration of Orthogonal QBF Solving Techniques
  2011 Conf. on Design, Automation and Test in Europe, pages: 149 - 154
  » show abstract« hide abstract
  Abstract

  In this paper we present a method for integrating two complementary solving techniques for QBF formulas, i. e. variable elimination based on an AIG-framework and search with DPLL based solving. We develop a sophisticated mechanism for coupling these techniques, enabling the transfer of partial results from the variable elimination part to the search part. This includes the definition of heuristics to (1) determine appropriate points in time to snapshot the current partial result during variable elimination (by estimating its quality) and (2) switch from variable elimination to search-based methods (applied to the best known snapshot) when the progress of variable elimination is supposed to be too slow or when representation sizes grow too fast. We will show in the experimental section that our combined approach is clearly superior to both individual methods run in a stand-alone manner. Moreover, our combined approach significantly outperforms all other state-of-the-art solvers.
• Ernst Althaus, Bernd Becker, Daniel Dumitriu, Stefan Kupferschmid
  Integration of an LP solver into interval constraint propagation
  2011 Int'l Conf. on Combinatorial optimization and applications, Springer, pages: 343 - 356
  » show abstract« hide abstract
  Abstract

  This paper describes the integration of an LP solver into iSAT, a Satisfiability Modulo Theories solver that can solve Boolean combinations of linear and nonlinear constraints. iSAT is a tight integration of the well-known DPLL algorithm and interval constraint propagation allowing it to reason about linear and nonlinear constraints. As interval arithmetic is known to be less efficient on solving linear programs, we will demonstrate how the integration of an LP solver can improve the overall solving performance of iSAT.
• Stefan Kupferschmid, Bernd Becker, Tino Teige, Martin Fränzle
  Proof Certificates and Non-linear Arithmetic Constraints
  2011 IEEE Design and Diagnostics of Electronic Circuits and Systems, pages: 429 - 434
  » show abstract« hide abstract
  Abstract

  Symbolic methods in computer-aided verification rely heavily on constraint solvers. The correctness and reliability of these solvers are of vital importance in the analysis of safety-critical systems, e.g., in the automotive context. Satisfiabilityresults of a solver can usually be checked by probing the computed solution. This isin general not the case for unsatisfiability results. In this paper, we propose a certification method for unsatisfiability results for mixed Boolean and non-lineararithmetic constraint formulae. Such formulae arise in the analysis of hybrid discrete/continuous systems. Furthermore, we test our approach by enhancing the iSATconstraint solver to generate unsatisfiability proofs, and implemented a tool that can efficiently validate such proofs. Finally, some experimental results showing theeffectiveness of our techniques are given.
• Andreas Eggers, Evgeny Kruglov, Stefan Kupferschmid, Karsten Scheibler, Tino Teige, Christoph Weidenbach
  Superposition modulo non-linear arithmetic
  2011 Int'l Symp. on Frontiers of Combining Systems, Springer, pages: 119 - 134
  » show abstract« hide abstract
  Abstract

  The first-order theory over non-linear arithmetic including transcendental functions (NLA) is undecidable.Nevertheless, in this paper we show that a particular combination with superposition leads to a sound and complete calculus that is useful in practice. We follow basically the ideas of the SUP(LA) combination, but have to take care of undecidability, resulting in ``unknown'' answers by the NLA reasoning procedure. A pipeline of NLA constraint simplification techniques related to the SUP(NLA) framework significantly decreases the number of ``unknown'' answers.The resulting approach is implemented as SUP(NLA) by a system combination of SPASS\ and iSAT. Applied to various scenarios of traffic collision avoidance protocols, we show by experiments that SPASS(iSAT) can fully automatically proof and disproof safety properties of such protocols using the very same formalization.

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.
• Christian Miller, Stefan Kupferschmid, Bernd Becker
  Exploiting Craig Interpolants in Bounded Model Checking for Incomplete Designs
  2010 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, volume: 13, pages: 77 - 86
• 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.
• Natalia Kalinnik, Erika Ábrahám, Tobias Schubert, Ralf Wimmer, Bernd Becker
  Exploiting Different Strategies for the Parallelization of an SMT Solver
  2010 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, Fraunhofer Verlag, pages: 97 - 106
  » show abstract« hide abstract
  Abstract

  In this paper we present two different parallelization schemes for the SMT solver iSAT, based on (1) the distribution of work by dividing the search space into disjoint parts and exploring them in parallel, thereby exchanging learnt information, and (2) a portfolio approach, where the entire benchmark instance isexplored in parallel by several copies of the same solver but usingdifferent heuristics to guide the search. We also combine bothapproaches such that solvers examine disjoint parts of the searchspace using different heuristics. The main contribution of the paper is to study the performances of different techniques for parallelizing iSAT.

2009

 back to the year overview

• Natalia Kalinnik, Tobias Schubert, Erika Ábrahám, Ralf Wimmer, Bernd Becker
  Picoso - A Parallel Interval Constraint Solver
  2009 Int'l Conf. on Parallel and Distributed Processing Techniques and Applications, CSREA Press, pages: 473 - 479
  » show abstract« hide abstract
  Abstract

  This paper describes the parallel interval constraint solver Picoso, which can decide (a subclass of) boolean combinations of linear and non-linear constraints. Picoso follows a master/client model based on message passing, making it suitable for any kind of workstation cluster as well as for multi-processor machines. To run several clients in parallel, an efficient work stealing mechanism has been integrated, dividing the overall search space into disjoint parts. Additionally, to prevent the clients from running into identical conflicts, information about conflicts in form of conflict clauses is exchanged among the clients. Performance measurements, using four clients to solve a number of benchmark problems, show that Picoso yields linear speedup compared to the sequential interval constraint solver iSAT, on which the clients of Picoso are based.
• Christoph Scholl, Stefan Disch, Florian Pigorsch, Stefan Kupferschmid
  Computing Optimized Representations for Non-convex Polyhedra by Detection and Removal of Redundant Linear Constraints
  2009 Tools and Algorithms for the Construction and Analysis of Systems, Springer, volume: 5505, pages: 383 - 397
  » show abstract« hide abstract
  Abstract

  We present a method which computes optimized representationsfor non-convex polyhedra. Our method detects so-called redundantlinear constraints in these representations by using an incremental SMT(Satisfiability Modulo Theories) solver and then removes the redundantconstraints based on Craig interpolation. The approach is motivated byapplications in the context of model checking for Linear Hybrid Automata.Basically, it can be seen as an optimization method for formulasincluding arbitrary boolean combinations of linear constraints andboolean variables. We show that our method provides an essential stepmaking quantifier elimination for linear arithmetic much more efficient.Experimental results clearly show the advantages of our approach incomparison to state-of-the-art solvers.
• Andreas Eggers, Natalia Kalinnik, Stefan Kupferschmid, Tino Teige
  Challenges in Constraint-Based Analysis of Hybrid Systems
  2009 Recent Advances in Constraints, Springer, volume: 5655, pages: 51 - 65
  » show abstract« hide abstract
  Abstract

  In the analysis of hybrid discrete-continuous systems, rich arithmeticconstraint formulae with complex Boolean structure arise naturally. The iSATalgorithm, a solver for such formulae, is aimed at bounded model checking ofhybrid systems. In this paper, we identify challenges emerging from planned and ongoing work to enhancethe iSAT algorithm. First, we propose an extension of iSAT to directly handleordinary differential equations as constraints. Second, we outline the recentlyintroduced generalization of the iSAT algorithm to deal with probabilistichybrid systems and some open research issues in that context. Third, wepresent ideas on how to move from bounded to unbounded model checking by usingthe concept of interpolation. Finally, we discuss the adaption of someparallelization techniques to the iSAT case, which will hopefully lead toperformance gains in the future.By presenting these open research questions, this paper aims at fosteringdiscussions on these extensions of constraint solving.
• Stefan Kupferschmid, Tino Teige, Bernd Becker, Martin Fränzle
  Proofs of Unsatisfiability for mixed Boolean and Non-linear Arithmetic Constraint Formulae
  2009 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, pages: 27 - 36
  » show abstract« hide abstract
  Abstract

  Symbolic methods in computer-aidedverification rely on appropriate constraint solvers. Correctness and reliabilityof solvers are a vital requirement in the analysis of safety-critical systems,e.g., in the automotive context. Satisfiability results of a solver can usuallybe checked by probing the computed solution. However, efficient validation of anuncertified unsatisfiability result for some constraint formula is nearlyimpossible. In this paper, we propose a certification method for unsatisfiability resultsfor mixed Boolean and non-linear arithmetic constraint formulae. Such formulaearise in the analysis of hybrid discrete-continuous systems.

2008

 back to the year overview

• Christoph Scholl, Stefan Disch, Florian Pigorsch, Stefan Kupferschmid
  Using an SMT Solver and Craig Interpolation to Detect and Remove Redundant Linear Constraints in Representations of Non-Convex Polyhedra
  2008 Int'l Workshop on Satisfiability Modulo Theories, pages: 18 - 26
• Andreas Eggers, Natalia Kalinnik, Stefan Kupferschmid, Tino Teige
  Challenges in Constraint-based Analysis of Hybrid Systems
  2008 ERCIM Workshop on Constraint Solving and Constraint Logic Programming
  » show abstract« hide abstract
  Abstract

  In the analysis of hybrid discrete-continuous systems, rich arithmeticconstraint formulae with complex Boolean structure arise naturally. The iSATalgorithm, a solver for such formulae, is aimed at bounded model checking ofhybrid systems. In this paper, we identify challenges emerging from planned and ongoing work to enhance the iSAT algorithm. First, we propose anextension of iSAT to directly handleordinary differential equations as constraints. Second, we outline the recentlyintroduced generalization of the iSAT algorithm to deal with probabilistichybrid systems and some open research issues in that context. Third, wepresent ideas on how to move from bounded to unbounded model checking by usingthe concept of interpolation. Finally, we discuss the adaption of someparallelization techniques to the iSAT case, which will hopefully lead toperformance gains in the future.By presenting these open research questions, this paper aims at fosteringdiscussions on these extensions of constraint solving.
• Jochen Eisinger
  Upper Bounds on the Automata Size for Integer and Mixed Real and Integer Linear Arithmetic
  2008 EACSL Annual Conf. on Computer Science Logic, Springer-Verlag, pages: 430 - 444

2007

 back to the year overview

• Bernd Becker, Jochen Eisinger, Felix Klaedtke
  Parallelization of Decision Procedures for Automatic Structures
  2007 Workshop on Omega-Automata