2021

 nach oben zur Jahresübersicht

• Karsten Scheibler, Felix Winterer, Tobias Seufert, Tino Teige, Christoph Scholl, Bernd Becker
  ICP and IC3
  2021 Conference on Design, Automation and Test in Europe Conference (DATE)
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  If embedded systems are used in safety-critical environments, they need to meet several standards. For example, in the automotive domain the ISO 26262 standard requires that the software running on such systems does not contain unreachable code. Software model checking is one effective approach to automatically detect such dead code. Being used in a commercial product, iSAT3 already performs very well in this context. In this paper we integrate IC3 into iSAT3 in order to improve its dead code detection capabilities even further.
• Felix Winterer, Tobias Seufert, Karsten Scheibler, Tino Teige, Christoph Scholl, Bernd Becker
  ICP and IC3 with Stronger Generalization
  2021 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Most recently, IC3 was integrated into the SMT solver iSAT3. Thus, iSAT3+IC3 introduces the first IC3 variant based on interval abstraction and Interval Constraint Propagation (ICP). As strong generalization is one of the key aspects for the IC3 algorithm to be successful, we integrate two additional generalization schemes from literature into iSAT3+IC3: Inductive Generalization and Counterexamples To Generalization (CTG). Furthermore, we evaluate the benefits and the drawbacks of different variants of these methods in the context of interval abstraction and ICP.

2019

 nach oben zur Jahresübersicht

• Christoph Scholl, Jie-Hong Roland Jiang, Ralf Wimmer, Aile Ge-Ernst
  A PSPACE Subclass of Dependency Quantified Boolean Formulas and Its Effective Solving
  2019 Honolulu, HI, USA Proceedings of the 33rd AAAI Conference on Artificial Intelligence (AAAI), AAAI Press
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Recently a DQBF proof calculus based on a notion of fork extension, in addition to resolution and universal reduction, was proposed by Rabe in 2017. We show that this calculus is in fact incomplete for general DQBFs, but complete for a subclass of DQBFs, where any two existential variables have either identical or disjoint dependency sets over the universal variables. We further characterize this DQBF subclass to be Sigma_3^P complete in the polynomial time hierarchy. Essentially using fork extension, a DQBF in this subclass can be converted to an equisatisfiable 3QBF with only a linear increase in formula size. We exploit this conversion for effective solving of this DQBF subclass and point out its potential as a general strategy for DQBF quantifier localization. Experimental results show that the method outperforms state-of-the-art DQBF solvers on a number of benchmarks, including the 2018 DQBF evaluation benchmarks.
• Aile Ge-Ernst, Christoph Scholl, Ralf Wimmer
  Localizing Quantifiers for DQBF
  2019 Proceedings of the 2019 Conference on Formal Methods in Computer Aided Design (FMCAD), Clark W. Barrett, Jin Yang
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Dependency quantified Boolean formulas (DQBFs) are a powerful formalism, which subsumes quantified Boolean formulas (QBFs) and allows an explicit specification of dependencies of existential variables on universal variables. Driven by the needs of various applications that can be encoded by DQBFs in a natural, compact, and elegant way, research on DQBF solving has emerged in the past few years. However, most works focus on closed DQBFs in prenex form (where all quantifiers are placed in front of a propositional formula), and non-prenex DQBFs have almost not been studied in the literature. In this paper we provide a formal definition for syntax and semantics of non-closed non-prenex DQBFs and prove useful properties enabling quantifier localization. Moreover, we make use of our theory by integrating quantifier localization into a state-of-the- art DQBF solver. Experiments with prenex DQBF benchmarks, including those from the QBFEVAL'18 competition, clearly show that quantifier localization pays off in this context.
• Ralf Wimmer, Christoph Scholl, Bernd Becker
  The (D)QBF Preprocessor HQSpre – Underlying Theory and Its Implementation
  2019 Journal on Satisfiability, Boolean Modeling and Computation, Band: 11, Nummer: 1, Seiten: 3 - 52
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Preprocessing turned out to be an essential step for SAT, QBF, and DQBF solvers to reduce/modify the number of variables and clauses of the formula, before the formula is passed to the actual solving algorithm. These preprocessing techniques often reduce the computation time of the solver by orders of magnitude. In this paper, we present the preprocessor HQSpre that was developed for Dependency Quantified Boolean Formulas (DQBFs) and that generalizes different preprocessing techniques for SAT and QBF problems to DQBF. We give a presentation of the underlying theory together with detailed proofs as well as implementation details contributing to the efficiency of the preprocessor. HQSpre has been used with obvious success by the winners of the DQBF track, and, even more interestingly, the QBF tracks of QBFEVAL’18.

2018

 nach oben zur Jahresübersicht

• Ralf Wimmer, Karina Wimmer, Christoph Scholl, Bernd Becker
  Analysis of Incomplete Circuits using Dependency Quantified Boolean Formulas
  In: Advanced Logic Synthesis
  2018, Springer, André Ignacio Reis and Rolf Drechsler, Seiten: 151 - 168, André Ignacio Reis and Rolf Drechsler, ISBN: 978-3-319-67294-6
• Christoph Scholl, Ralf Wimmer
  Dependency Quantified Boolean Formulas: An Overview of Solution Methods and Applications
  2018 Oxford, UK Proceedings of the 21st Int'l Conf. on Theory and Applications of Satisfiability Testing (SAT), Olaf Beyersdorff, Christoph M. Wintersteiger, Band: 10929, Seiten: 3 - 16
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Dependency quantified Boolean formulas (DQBFs) as a generalization of quantified Boolean formulas (QBFs) have received considerable attention in research during the last years. Here we give an overview of the solution methods developed for DQBF so far. The exposition is complemented with the discussion of various applications that can be handled with DQBF solving.

2017

 nach oben zur Jahresübersicht

• Ralf Wimmer, Andreas Karrenbauer, Ruben Becker, Christoph Scholl, Bernd Becker
  From DQBF to QBF by Dependency Elimination
  2017 Melbourne, VIC, Australia Int'l Conf. on Theory and Applications of Satisfiability Checking, Serge Gaspers and Toby Walsh, Band: 10491, Seiten: 326 - 343
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  In this paper, we propose the elimination of dependencies to convert a given dependency quantified Boolean formula (DQBF) to an equisatisfiable QBF. We show how to select a set of dependencies to eliminate such that we arrive at a smallest equisatisfiable QBF in terms of existential variables that is achievable using dependency elimination. This approach is improved by taking so-called don't-care dependencies into account, which result from the application of dependency schemes to the formula and can be added to or removed from the formula at no cost. We have implemented this new method in the state-of-the-art DQBF solver HQS. Experiments show that dependency elimination is clearly superior to the previous method using variable elimination.
• Bernd Becker, Christoph Scholl, Ralf Wimmer
  Verification of Incomplete Designs
  In: Formal System Verification - State of the Art and Future Trends
  2017, Springer, Rolf Drechsler, Seiten: 37 - 72, Rolf Drechsler, ISBN: 978-3-319-57683-1
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  We consider the verification of digital systems which are incomplete in the sense that for some modules only their interfaces (i.e., the signals entering and leaving the module) are known, but not their implementations. For such designs, we study realizability (``Is it possible to implement the missing modules such that the complete design has certain properties?'') and validity (``Does a property hold no matter how the missing parts are implemented?'').

2016

 nach oben zur Jahresübersicht

• Ralf Wimmer, Christoph Scholl, Karina Wimmer, Bernd Becker
  Dependency Schemes for DQBF
  2016 Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing (SAT), Springer, Band: 9710, Seiten: 473 - 489
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Dependency schemes allow to identify variable independencies in QBFs or DQBFs. For QBF, several dependency schemes have been proposed, which differ in the number of independencies they are able to identify. In this paper, we analyze the spectrum of dependency schemes that were proposed for QBF. It turns out that only some of them are sound for DQBF. For the sound ones, we provide a correctness proof, for the others counterexamples. Experiments show that a significant number of dependencies can either be added to or removed from a formula without changing its truth value, but with significantly increasing the flexibility for modifying the representation.
• Karina Wimmer, Ralf Wimmer, Christoph Scholl, Bernd Becker
  Skolem Functions for DQBF
  2016 Int'l Symposium on Automated Technology for Verification and Analysis (ATVA) Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA), Springer, Band: 9938, Seiten: 395 - 411
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  We consider the problem of computing Skolem functions for satisfied dependency quantified Boolean formulas (DQBFs). We show how Skolem functions can be obtained from an elimination-based DQBF solver and how to take preprocessing steps into account. The size of the Skolem functions is optimized by don't-care minimization using Craig interpolants and rewriting techniques. Experiments with our DQBF solver HQS show that we are able to effectively compute Skolem functions with very little overhead compared to the mere solution of the formula.
• Karina Wimmer, Ralf Wimmer, Christoph Scholl, Bernd Becker
  Skolem Functions for DQBF (Extended Version)
  , 2016

2015

 nach oben zur Jahresübersicht

• Bernd Becker, Matthias Sauer, Christoph Scholl, Ralf Wimmer
  Modeling Unknown Values in Test and Verification
  In: Formal Modeling and Verification of Cyber-Physical Systems (Proceedings of the 1st International Summer School on Methods and Tools for the Design of Digital Systems)
  2015, Springer, Rolf Drechsler, Ulrich Kühne, Seiten: 122 - 150, Rolf Drechsler, Ulrich Kühne, ISBN: 978-3-658-09993-0
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  mbination with algorithms balancing exactness of representation and efficiency of calculation. In the following, state-of-the-art approaches are described that enable an efficient and successful handling of unknown values using formal techniques in the areas of Test and Verification.
• Ralf Wimmer, Karina Gitina, Jennifer Nist, Christoph Scholl, Bernd Becker
  Preprocessing for DQBF
  2015 Proceedings of the 18th International Conference on Theory and Applications of Satisfiability Testing (SAT), Springer, Band: 9340, Seiten: 173 - 190
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  For SAT and QBF formulas many techniques are applied in order to reduce/modify the number of variables and clauses of the formula, before the formula is passed to the actual solving algorithm. It is well known that these preprocessing techniques often reduce the computation time of the solver by orders of magnitude. In this paper we generalize different preprocessing techniques for SAT and QBF problems to dependency quantified Boolean formulas (DQBF) and describe how they need to be adapted to work with a DQBF solver core. We demonstrate their effectiveness both for CNF- and non-CNF-based DQBF algorithms.
• 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

2013

 nach oben zur Jahresübersicht

• 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, Seiten: 61 - 70
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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, Seiten: 396 - 403
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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.

2012

 nach oben zur Jahresübersicht

• 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”, Seiten: 133 - 143
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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.

2011

 nach oben zur Jahresübersicht

• Christian Miller, Christoph Scholl, Bernd Becker
  Verifying Incomplete Networks of Timed Automata
  2011 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, Band: 14
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Verification of real-time systems - e.g. communication protocols or embedded controllers - is an important task. One method to detect errors is called bounded model checking (BMC). In BMC a system is iteratively unfolded and then transformed into a satisfiability problem. If an appropriate solver finds the k-th instance to be satisfiable, a counterexample for a given safety property has been found. In this paper, we present a novel approach to apply BMC to networks of timed automata (i.e. a system of several interacting subautomata) where parts of the network are unspecified (so-called blackboxes). Here, we would like to answer the question of unrealizability, that is, is there a path of a certain length violating a safety property regardless of the implementation of the blackboxes. Focusing on two prevalent communication models for networks of interacting timed automata, we introduce two methods to solve these types of BMC problems. The first is based on fixed transitions, which in some cases is too coarse of an abstraction. In the second approach we prove unrealizability by introducing universal quantification, yielding more advanced quantified SAT-Modulo-Theory formulas.
• Sven Reimer, Florian Pigorsch, Christoph Scholl, Bernd Becker
  Integration of Orthogonal QBF Solving Techniques
  2011 Conf. on Design, Automation and Test in Europe, Seiten: 149 - 154
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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.

2010

 nach oben zur Jahresübersicht

• Christian Miller, Karina Gitina, Christoph Scholl, Bernd Becker
  Bounded Model Checking of Incomplete Networks of Timed Automata
  2010 Int'l Workshop on Microprocessor Test and Verification, IEEE Computer Society, Band: 11, Seiten: 61 - 66
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Verification of real-time systems - e.g. communication protocols or embedded controllers - is an important task. One method to detect errors is called bounded model checking (BMC). In BMC the system is iteratively unfolded and then transformed into a satisfiability problem. If an appropriate solver finds the k-th instance to be satisfiable a counterexample for a given safety property has been found. In this paper we present a first approach to apply BMC to networks of timed automata (that is a system of several interacting subautomata) where parts of the network are unspecified (so called blackboxes). Here, we would like to answer the question of unrealizability, that is, is there a path of a certain length violating a safety property regardless of the implementation of the blackboxes. We provide solutions to this problem for two timed automata communication models. For the simple synchronization model, a BMC approach based on fixed transitions is introduced resulting in a SAT-Modulo-Theory formula. With respect to the use of bounded integer variables for communication, we prove unrealizability by introducing universal quantification, yielding more advanced quantified SAT-Modulo-Theory formulas.
• 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”, Band: 13, Seiten: 107 - 116

2009

 nach oben zur Jahresübersicht

• 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, Band: 5505, Seiten: 383 - 397
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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.
• Christian Miller, Tobias Nopper, Christoph Scholl
  Symbolic CTL Model Checking for Incomplete Designs by Selecting Property-Specific Subsets of Local Component Assumptions
  2009 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Black Box symbolic model checking is a method to check whether an incompletely specified circuit,in which some parts of the design have been replaced by ‘Black Boxes’, satisfies a CTL propertyregardless of the actual replacement of the Black Boxes. One possible application is model checkingwith abstraction where complex parts of the design (which are not really relevant for the propertyat hand) are put into Black Boxes in order to speed up the model checking run. However, due toits approximative nature, symbolic model checking for incomplete designs may be unable to provideproofs when the approximations are to coarse.In this paper we show how Black Box model checking can profit from information about the Black-Boxed parts given in form of so-called local component assumptions. The assumptions we use in thiscontext are safety properties arguing about fixed time windows. Furthermore we will present a setof heuristic-based approaches to automatically select a subset of local component assumptions that issufficient to prove or disprove a given CTL property.

2008

 nach oben zur Jahresübersicht

• 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, Seiten: 18 - 26

2007

 nach oben zur Jahresübersicht

• Tobias Nopper, Christoph Scholl, Bernd Becker
  Computation of Minimal Counterexamples by Using Black Box Techniques and Symbolic Methods
  2007 IEEE Int'l Conf. on Computer-Aided Design, IEEE Computer Society Press, Seiten: 273 - 280
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Computing counterexamples is a crucial task for error diagnosis and debugging of sequential systems. If an implementation does not fulfill its specification, counterexamples are used to explain the error effect to the designer. In order to be understood by the designer, counterexamples should be simple, i.e. they should be as general as possible and assign values to a minimal number of input signals. Here we use the concept of Black Boxes (parts of the design with unknown behaviour) to mask out components for counterexample computation. By doing so, the resulting counterexample will argue about a reduced number of components in the system to facilitate the task of understanding and correcting the error. We introduce the notion of "uniform counterexamples" to provide an exact formalization of simplified counterexamples arguing only about components which were not masked out. Our computation of counterexamples is based on symbolic methods using AIGs (And-Inverter-Graphs). Experimental results using a VLIW processor as a case study clearly demonstrate our capability of providing simplified counterexamples.

2006

 nach oben zur Jahresübersicht

• Marc Herbstritt, Bernd Becker, Christoph Scholl
  Advanced SAT-Techniques for Bounded Model Checking of Blackbox Designs
  2006 Int'l Workshop on Microprocessor Test and Verification, IEEE Computer Society, Seiten: 37 - 44

2002

 nach oben zur Jahresübersicht

• Christoph Scholl, Bernd Becker
  Checking Equivalence for Circuits Containing Incompletely Specified Boxes
  2002 Int'l Conf. on Computer Design, Seite: 56
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  We consider the problem of checking whether an implementation which contains parts with incomplete information is equivalent to a given full specification. We study implementations which are not completely specified, but contain boxes which are associated with incompletely specified functions (called Incompletely Specified Boxes or IS--Boxes). After motivating the use of implementations with Incompletely Specified Boxes we define our notion of equivalence for this kind of implementations and present a method to solve the problem. A series of experimental results demonstrates the effectiveness and feasibility of the methods presented.
• Christoph Scholl, Bernd Becker
  Equivalence Checking in the Presence of Incompletely Specified Boxes
  2002 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  We consider the problem of checking whether an implementation which contains parts with incomplete information is equivalent to a given full specification. We study implementations which are not completely specified, but contain boxes which are associated with incompletely specified functions (called Incompletely Specified Boxes or IS--Boxes). After motivating the use of implementations with Incompletely Specified Boxes we define our notion of equivalence for this kind of implementations and present a method to solve the problem. A series of experimental results demonstrates the effectiveness and feasibility of the methods presented.

2001

 nach oben zur Jahresübersicht

• Christoph Scholl, Bernd Becker
  Checking Equivalence for Partial Implementations
  2001 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, Seiten: 31 - 43
• Christoph Scholl, Bernd Becker
  Checking Equivalence for Partial Implementations
  2001 IEEE Design Automation Conference, IEEE Computer Society, Seiten: 238 - 243
• Christoph Scholl, Marc Herbstritt, Bernd Becker
  Don't Care Minimization of *BMDs: Complexity and Algorithms
  2001 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, Seiten: 45 - 57
• Christoph Scholl, Marc Herbstritt, Bernd Becker
  Exploiting Don't Cares to Minimize *BMDs
  2001 IEEE Int'l Symp. on Circuits and Systems, Band: 5, Seiten: 191 - 194
• Christoph Scholl
  Functional Decomposition with Application to FPGA Synthesis
  Kluwer Academic Publishers, 2001
• Christoph Scholl, Bernd Becker, A. Brogle
  The Multiple Variable Order Problem for Binary Decision Diagrams: Theory and Practical Application
  2001 ASP Design Automation Conf., Seiten: 85 - 90
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Reduced Ordered Binary Decision Diagrams (ROBDDs) gained widespread use in logic design verification, test generation, fault simulation, and logic synthesis [MWBS:88,Bry:92]. Since the size of an ROBDD heavily depends on the variable order used, there is a strong need to find variable orders that minimize the number of nodes in an ROBDD. In certain applications we have to cope with ROBDDs with different variable orders, whereas further manipulations of these ROBDDs require common variable orders. In this paper we give a theoretical background for this "Multiple Variable Order problem". Moreover, we solve the problem to transform ROBDDs with different variable orders into a good common variable order using dynamic variable ordering techniques.

2000

 nach oben zur Jahresübersicht

• Christoph Scholl, Bernd Becker
  Checking Equivalence for Partial Implementations
  , Nummer: 145, 2000
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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. Several algorithms trading off accuracy and computational resources are presented: Starting with a simple 0,1,X-based simulation, which allows approximate solutions, but is not able to find all errors in the partial implementation, we consider more and more exact methods finally covering all errors detectable in the partial implementation. The exact algorithm reports no error if and only if the current partial implementation conforms to the specification, i.e. it can be extended to a full implementation which is equivalent to the specification. We give a series of experimental results demonstrating the effectiveness and feasibility of the methods presented.
• Christoph Scholl, Marc Herbstritt, Bernd Becker
  Exploiting Don't Cares to Minimize *BMDs
  , Nummer: 141, 2000
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  We present for the first time methods to minimize *BMDs exploiting don't care conditions. These minimization methods can be used during the verification of circuits by *BMDs. By changing function values for input vectors, which are in the don't care set, smaller *BMDs can be computed to keep peak memory consumption during *BMD construction as low as possible. We determine the complexity of the problem of don't care minimization for *BMDs and thus justify the use of heuristics to approximate the solution. Preliminary experimental results prove our heuristcs to be very effective in minimizing *BMD sizes.
• Andreas Hett, Christoph Scholl, Bernd Becker
  Distance Driven Finite State Machine Traversal
  2000 IEEE Design Automation Conference, Seiten: 39 - 42
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Symbolic techniques have revolutionized reachability analysis in the last years. Extending their applicability to handle large, industrial designs is a key issue, involving the need to focus on memory consumption for BDD representation as well as time consumption to perform symbolic traversals of Finite State Machines (FSMs). We address the problem of reachability analysis for large FSMs, introducing a novel technique that performs reachability analysis using a sequence of "distance driven" partial traversals based on dynamically chosen prunings of the transition relation. Experiments are given to demonstrate the efficiency and robustness of our approach: We succeed in completing reachability problems with significantly smaller memory requirements and improved time performance.
• Andreas Hett, Christoph Scholl, Bernd Becker
  State Traversal guided by Hamming Distance Profiles
  2000 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, VDE Verlag, Seiten: 57 - 66

1999

 nach oben zur Jahresübersicht

• Christoph Scholl, Bernd Becker, A. Brogle
  Solving the Multiple Variable Order Problem for Binary Decision Diagrams by Use of Dynamic Reordering Techniques
  , Nummer: 130, 1999
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Reduced Ordered Binary Decision Diagrams (ROBDDs) gained widespread use in logic design verification, test generation, fault simulation, and logic synthesis [MWBS:88,Bry:92]. Since the size of an ROBDD heavily depends on the variable order used, there is a strong need to find variable orders that minimize the number of nodes in an ROBDD. In certain applications we have to cope with ROBDDs with different variable orders, whereas further manipulations of these ROBDDs require common variable orders. In this paper we solve the problem to transform ROBDDs with different variable orders into a good common variable order. To do so, we make use of dynamic variable ordering techniques.
• Andreas Hett, Christoph Scholl, Bernd Becker
  A.MORE - A Multi-Operand BDD Package
  University of Freiburg, 1999
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Decision Diagrams (DDs) are often used in CAD systems for the efficient representation and manipulation of Boolean functions. The most popular data structure in this context are Ordered Binary Decision Diagrams (OBDDs) that are used in many applications. This package provides a novel approach for synthesizing BDDs using operator nodes instead of procedure calls. Thus, transformations on this data structure are possible as well as the flexibility to adapt the synthesis process in order to execute the 'most primising paths' first, resulting in less superfluous calculations and lower memory usage due to the skipping of unneeded branches.
• Christoph Scholl, D. Möller, Paul Molitor, Rolf Drechsler
  BDD Minimization Using Symmetries
  1999 IEEE Trans. on CAD, Band: 18, Nummer: 2, Seiten: 81 - 100
• Paul Molitor, Christoph Scholl
  Datenstrukturen und effiziente Algorithmen fuer die Logiksynthese kombinatorischer Schaltungen
  B.G. Teubner, 1999
• Christoph Scholl, Bernd Becker
  On the Generation of Multiplexer Circuits for Pass Transistor Logic
  1999 Int'l Workshop on Logic Synth.
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  used instead and should provide a much higher potential for optimization compared to a pure BDD approach. Nevertheless - to the best of our knowledge - an optimization of general Multiplexer Circuits (MCs) for PTL synthesis was not tried so far due to a lack of suitable optimization approaches. In this paper we present such an algorithm which is based on efficient BDD optimization techniques. Our experiments prove that there is indeed a high optimization potential by the use of general MCs - both concerning area and depth of the resulting PTL networks.
• Christoph Scholl, Bernd Becker, A. Brogle
  Solving the Multiple Variable Order Problem for Binary Decision Diagram by Use of Dynamic Reordering Techniques
  1999 Int'l Workshop on Logic Synth.
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Reduced Ordered Binary Decision Diagrams (ROBDDs) gained widespread use in logic design verification, test generation, fault simulation, and logic synthesis [MWBS:88,Bry:92]. Since the size of an ROBDD heavily depends on the variable order used, there is a strong need to find variable orders that minimize the number of nodes in an ROBDD. In certain applications we have to cope with ROBDDs with different variable orders, whereas further manipulations of these ROBDDs require common variable orders. In this paper we solve the problem to transform ROBDDs with different variable orders into a good common variable order. To do so, we make use of dynamic variable ordering techniques.
• Christoph Scholl, Bernd Becker, A. Brogle
  Solving the Multiple Variable Order Problem for Binary Decision Diagram by Use of Dynamic Reordering Techniques
  , Nummer: 130, 1999
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Reduced Ordered Binary Decision Diagrams (ROBDDs) gained widespread use in logic design verification, test generation, fault simulation, and logic synthesis [MWBS:88,Bry:92]. Since the size of an ROBDD heavily depends on the variable order used, there is a strong need to find variable orders that minimize the number of nodes in an ROBDD. In certain applications we have to cope with ROBDDs with different variable orders, whereas further manipulations of these ROBDDs require common variable orders. In this paper we solve the problem to transform ROBDDs with different variable orders into a good common variable order. To do so, we make use of dynamic variable ordering techniques.

1998

 nach oben zur Jahresübersicht

• Christoph Scholl
  Multi-output Functional Decomposition with Exploitation of Don't Cares
  1998 Conf. on Design, Automation and Test in Europe, Seiten: 743 - 748
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Functional decomposition is an important technique in logic synthesis, especially for the design of lookup table based FPGA architectures. We present a method for functional decomposition with a novel concept for the exploitation of don't cares thereby combining two essential goals: the minimization of the numbers of decomposition functions in the current decomposition step and the extraction of common subfunctions for multi-output Boolean functions. The exploitation of symmetries of Boolean functions plays an important role in our algorithm as a means to minimize the number of decomposition functions not only for the current decomposition step but also for the (recursive) decomposition algorithm as a whole. Experimental results prove the effectiveness of our approach.
• Christoph Scholl, Bernd Becker, T. M. Weis
  Word-Level Decision Diagrams, WLCDs and Division
  1998 Int'l Conf. on CAD, Seiten: 672 - 677
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Several types of Decision Diagrams (DDs) have been proposed for the verification of Integrated Circuits. Recently, word-level DDs like BMDs, *BMDs, HDDs, K*BMDs and *PHDDs have been attracting more and more interest, e.g., by using *BMDs and *PHDDs it was for the first time possible to formally verify integer multipliers and floating point multipliers of "significant" bitlengths, respectively. On the other hand, it has been unknown, whether division, the operation inverse to multiplication, can be efficiently represented by some type of word-level DDs. In this paper we show that the representational power of any word-level DD is too weak to efficiently represent integer division. Thus, neither a clever choice of the variable ordering, the decomposition type or the edge weights, can lead to a polynomial DD size for division. For the proof we introduce Word-Level Linear Combination Diagrams (WLCDs), a DD, which may be viewed as a "generic" word-level DD. We derive an exponential lower bound on the WLCD representation size for integer dividers and show how this bound transfers to all other word-level DDs.

1997

 nach oben zur Jahresübersicht

• Christoph Scholl, D. Möller, Paul Molitor, Rolf Drechsler
  BDD Minimization Using Symmetries
  , 1997
• Christoph Scholl
  Functional Decomposition with Integrated Test Generation
  1997 GI/ITG Workshop “Testmethoden und Zuverlässigkeit von Schaltungen und Systemen”
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Functional decomposition is an important technique in logic synthesis, especially for the design of lookup table based FPGA architectures. We present an approach how to compute test information, e.g. a complete test set (according to the stuck-at-fault model or the cellular fault model), for functionally decomposed circuits. We are able to compute this test information in parallel with logic synthesis by (recursive) functional decomposition.
• Christoph Scholl, Rolf Drechsler, Bernd Becker
  Functional Simulation using Binary Decision Diagrams
  1997 GI/ITG/GME Workshop “Methoden des Entwurfs und der Verifikation digitaler Systeme”
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  In many verification techniques fast functional evaluation of a Boolean network is needed. We investigate the idea of using Binary Decision Diagrams (BDDs) for functional simulation. The area-time trade-off that results from different minimization techniques of the BDD is discussed. We propose new minimization methods based on dynamic reordering that allow smaller representations with (nearly) no runtime penalty.
• Christoph Scholl, Rolf Drechsler, Bernd Becker
  Functional Simulation using Binary Decision Diagrams
  1997 Int'l Workshop on Logic Synth.
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  In many verification techniques fast functional evaluation of a Boolean network is needed. We investigate the idea of using Binary Decision Diagrams (BDDs) for functional simulation. The area-time trade-off that results from different minimization techniques of the BDD is discussed. We propose new minimization methods based on dynamic reordering that allow smaller representations with (nearly) no runtime penalty.
• Christoph Scholl
  Multi-output Functional Decomposition with Exploitation of Don't Cares
  1997 Int'l Workshop on Logic Synth.
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  ults prove the effectiveness of our approach.