Christoph Scholl
Liste filtern : Jahre: 2019 |
2018 |
2017 |
2016 |
2015 |
2013 |
2012 |
2011 |
2010 |
2009 |
2008 |
2007 |
2006 |
2002 |
2001 |
2000 |
1999 |
1998 |
1997 | alle anzeigen nach oben zur Jahresübersicht Christoph Scholl, Jie-Hong Roland Jiang, Ralf Wimmer, Aile Ge-ErnstA 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 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. This enables a succinct encoding of decision problems in the NEXPTIME complexity class. As solving general DQBFs is NEXPTIME complete, in contrast to the PSPACE completeness of QBF solving, characterizing DQBF subclasses of lower computational complexity allows their effective solving and is of practical importance.
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 WimmerLocalizing 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 BeckerThe (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. nach oben zur Jahresübersicht Ralf Wimmer, Karina Wimmer, Christoph Scholl, Bernd BeckerAnalysis 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 WimmerDependency 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. nach oben zur Jahresübersicht Ralf Wimmer, Andreas Karrenbauer, Ruben Becker, Christoph Scholl, Bernd BeckerFrom 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 WimmerVerification 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?''). nach oben zur Jahresübersicht Ralf Wimmer, Christoph Scholl, Karina Wimmer, Bernd BeckerDependency 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 BeckerSkolem 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 BeckerSkolem Functions for DQBF (Extended Version) , 2016 nach oben zur Jahresübersicht Bernd Becker, Matthias Sauer, Christoph Scholl, Ralf WimmerModeling 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 With increasing complexities and a component-based design style the handling of unkown values (e. g., at the interface of components) becomes more and more important in electronic design automation (EDA) and production processes. Tools are required that allow an accurate modeling of unkowns in combination 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 BeckerPreprocessing 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 BeckerSolving DQBF Through Quantifier Elimination 2015 Conf. on Design, Automation and Test in Europe nach oben zur Jahresübersicht Karina Gitina, Sven Reimer, Matthias Sauer, Ralf Wimmer, Christoph Scholl, Bernd BeckerEquivalence 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 BeckerEquivalence 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 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. nach oben zur Jahresübersicht Sven Reimer, Florian Pigorsch, Christoph Scholl, Bernd BeckerEnhanced 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. nach oben zur Jahresübersicht Christian Miller, Christoph Scholl, Bernd BeckerVerifying 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 BeckerIntegration 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. nach oben zur Jahresübersicht Christian Miller, Karina Gitina, Christoph Scholl, Bernd BeckerBounded 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 SchollSAT 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 nach oben zur Jahresübersicht Christoph Scholl, Stefan Disch, Florian Pigorsch, Stefan KupferschmidComputing 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 SchollSymbolic 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. nach oben zur Jahresübersicht Christoph Scholl, Stefan Disch, Florian Pigorsch, Stefan KupferschmidUsing 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 nach oben zur Jahresübersicht Tobias Nopper, Christoph Scholl, Bernd BeckerComputation 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. nach oben zur Jahresübersicht Marc Herbstritt, Bernd Becker, Christoph SchollAdvanced SAT-Techniques for Bounded Model Checking of Blackbox Designs 2006 Int'l Workshop on Microprocessor Test and Verification , IEEE Computer Society, Seiten : 37 - 44 nach oben zur Jahresübersicht Christoph Scholl, Bernd BeckerChecking 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 BeckerEquivalence 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. nach oben zur Jahresübersicht Christoph Scholl, Bernd BeckerChecking 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 BeckerChecking Equivalence for Partial Implementations 2001 IEEE Design Automation Conference , IEEE Computer Society, Seiten : 238 - 243 Christoph Scholl, Marc Herbstritt, Bernd BeckerDon'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 BeckerExploiting Don't Cares to Minimize *BMDs 2001 IEEE Int'l Symp. on Circuits and Systems , Band : 5, Seiten : 191 - 194 Christoph SchollFunctional Decomposition with Application to FPGA Synthesis Kluwer Academic Publishers, 2001 Christoph Scholl, Bernd Becker, A. BrogleThe 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. nach oben zur Jahresübersicht Christoph Scholl, Bernd BeckerChecking 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 BeckerExploiting 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 BeckerDistance 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 BeckerState 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 nach oben zur Jahresübersicht Christoph Scholl, Bernd Becker, A. BrogleSolving 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 BeckerA.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 DrechslerBDD Minimization Using Symmetries 1999 IEEE Trans. on CAD , Band : 18, Nummer : 2, Seiten : 81 - 100 Paul Molitor, Christoph SchollDatenstrukturen und effiziente Algorithmen fuer die Logiksynthese kombinatorischer Schaltungen B.G. Teubner, 1999 Christoph Scholl, Bernd BeckerOn the Generation of Multiplexer Circuits for Pass Transistor Logic 1999 Int'l Workshop on Logic Synth. » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Pass Transistor Logic has attracted more and more interest during last years, since it has proved to be an attractive alternative to static CMOS designs with respect to area, performance and power consumption. Existing automatic PTL synthesis tools use a direct mapping of (decomposed) BDDs to pass transistors. Thereby, structural properties of BDDs like the ordering restriction and the fact that the select signals of the multiplexers (corresponding to BDD nodes) directly depend on input variables, are imposed on PTL circuits although they are not necessary for PTL synthesis. General Multiplexer Circuits can be 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. BrogleSolving 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. BrogleSolving 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. nach oben zur Jahresübersicht Christoph SchollMulti-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. WeisWord-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. nach oben zur Jahresübersicht Christoph Scholl, D. Möller, Paul Molitor, Rolf DrechslerBDD Minimization Using Symmetries , 1997 Christoph SchollFunctional 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 BeckerFunctional 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 BeckerFunctional 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 SchollMulti-output Functional Decomposition with Exploitation of Don't Cares 1997 Int'l Workshop on Logic Synth. » 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.