Liste filtern : Jahre: 2020 |
2019 |
2018 |
2017 |
2016 |
2015 |
2014 |
2013 |
2012 |
2011 |
2010 |
2009 |
2008 |
2007 |
2006 |
2005 |
2004 |
2002 |
2001 |
2000 |
1999 |
1998 |
1997 |
1995 |
1994 |
1993 | alle anzeigen nach oben zur Jahresübersicht Christoph Scholl, Alexander KonradSymbolic Computer Algebra and SAT Based Information Forwarding for Fully Automatic Divider Verification 2020 Design Automation Conf. , Seiten : 1 - 6» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung During the last few years Symbolic Computer Algebra
(SCA) delivered excellent results in the verification of large integer and finite field multipliers at the gate level. In contrast to those encouraging advances, SCA-based divider verification has been still in its infancy and
awaited a major breakthrough. In this paper we analyze the fundamental reasons that prevented the success for SCA-based divider verification so far and present SAT Based Information Forwarding (SBIF). SBIF enhances SCA-based backward rewriting by information propagation in
the opposite direction. We successfully apply the method to the fully automatic formal verification of large non-restoring dividers. Alireza Mahzoon, Daniel Große, Christoph Scholl, Rolf DrechslerTowards Formal Verification of Optimized and Industrial Multipliers 2020 Conference on Design, Automation and Test in Europe (DATE) , Seiten : 544 - 549» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Formal verification methods have made huge progress
over the last decades. However, proving the correctness of arithmetic circuits involving integer multipliers still drives the verification techniques to their limits. Recently, Symbolic Computer Algebra (SCA) methods have shown good results in the verification of both large and non-trivial multipliers. Their success is mainly based on (1) reverse engineering and identifying basic building blocks, (2) finding converging gate cones which start from the
basic building blocks and (3) early removal of redundant terms (vanishing monomials) to avoid the blow-up during backward rewriting.
Despite these important accomplishments, verifying optimized
and technology-mapped multipliers is an almost unexplored area. This creates major barriers for industrial use as most of the designs are area and delay optimized. To overcome the barriers, we propose a novel SCA-method which supports the formal verification of a large variety of optimized multipliers. Our method takes advantage of a dynamic substitution ordering to avoid the monomial explosion during backward rewriting. Experimental results confirm the efficiency of our approach in the verification of a wide range of optimized multipliers including industrial benchmarks. 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 33th AAAI Conference on Artificial Intelligence (AAAI-19) » 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 SigmaP3 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. Katalin Fazekas, Armin Biere, Christoph SchollIncremental Inprocessing in SAT Solving 2019 10th International Conference on Theory and Applications of Satisfiability Testing (SAT) , Springer-Verlag, Nummer : 11628, Seiten : 136 - 154» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Incremental SAT is about solving a sequence of related SAT
problems efficiently. It makes use of already learned information to avoid repeating redundant work. Also preprocessing and inprocessing are considered to be crucial. Our calculus uses the most general redundancy property and extends existing inprocessing rules to incremental SAT solving. It allows to automatically reverse earlier simplification steps, which are inconsistent with literals in new incrementally added clauses. Our approach to incremental SAT solving not only simplifies the use of inprocessing but also substantially improves solving time. Aile Ge-Ernst, Christoph Scholl, Ralf WimmerLocalizing Quantifiers for DQBF 2019 Proceedings of the Conference on Formal Methods in Computer Aided Design (FMCAD) , IEEE Computer Society 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. 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. Aile Ge-Ernst, Christoph Scholl, Ralf WimmerQuantifier Localization for DQBF 2019 Int'l Workshop on Logic and Synthesis » 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 which can be encoded by DQBFs in a natural, compact, and elegant way, research on DQBF solving has emerged in the past few years. However, research focused 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. Aile Ge-Ernst, Christoph Scholl, Ralf WimmerQuantifier Localization for DQBF CoRR , Band : abs/1905.04755, 2019 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. Tobias Seufert, Christoph SchollfbPDR: In-depth Combination of Forward and Backward Analysis in Property Directed Reachability 2019 Conference on Design, Automation and Test in Europe (DATE) » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We describe a thoroughly interweaved forward and backward version of PDR/IC3 called fbPDR. Motivated by the complementary strengths of PDR and Reverse PDR and by related work showing the benefits of collaboration between the two, fbPDR lifts the combination to a new level. We lay the theoretical foundations for sharing information represented by learned lemmas between PDR and Reverse PDR and demonstrate the effectiveness of our approach on benchmarks from the Hardware Model Checking Competition. Tobias Seufert, Christoph SchollfbPDR: In-depth Combination of Forward and Backward Analysis in Property Directed Reachability (extended abstract) 2019 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We describe a thoroughly interweaved forward and backward version of PDR/IC3 called fbPDR. Motivated by the com-
plementary strengths of PDR and Reverse PDR, fbPDR enables beneficial collaboration between the two and lifts the
combination to a new level. We lay the theoretical foundations for sharing information between PDR and Reverse PDR
and demonstrate the effectiveness of our approach on benchmarks from the Hardware Model Checking Competition. 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 International Publishing , André Inácio Reis, Rolf Drechsler, Seiten : 151 - 168, André Inácio Reis, Rolf Drechsler, ISBN : 978-3-319-67294-6» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We consider Dependency Quantified Boolean Formulas (DQBFs), a generalization of Quantified Boolean Formulas (QBFs), and demonstrate that DQBFs are a natural calculus to exactly express the realizability problem of incomplete combinational and sequential circuits with an arbitrary number of (combinational or bounded-memory) black boxes. In contrast to usual approaches for controller synthesis, restrictions to the interfaces of missing circuit parts in distributed architectures are strictly taken into account. We present a solution method for DQBFs together with the extraction of Skolem functions for existential variables, which can directly serve as implementations for the black boxes. First experimental results are provided. Tobias Seufert, Christoph SchollCombining PDR and Reverse PDR for Hardware Model Checking 2018 Conference on Design, Automation and Test in Europe (DATE) » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In the last few years IC3 resp. PDR attracted a lot of
attention as a SAT-based hardware verification approach without needing to unroll the transition relation as in Bounded Model Checking (BMC). Motivated by different strengths of forward and backward traversal already observed in BDD based model checking and by an exponential complexity gap between original PDR and its reverted counterpart ‘Reverse PDR’ (which starts its analysis with the initial states instead of the unsafe states as in the original PDR), we take a closer look at Reverse PDR and we present a combined forward/backward version of PDR that inherits the advantages of both original and Reverse PDR.
Our experimental results on benchmarks from the Hardware
Model Checking Competition demonstrate clear benefits of the
combined approach. Christoph Scholl, Ralf WimmerDependency Quantified Boolean Formulas: An Overview of Solution Methods and Applications 2018 13th International Conference on Theory and Applications of Satisfiability Testing (SAT) , Springer-Verlag, Nummer : 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 International Conference on Theory and Applications of Satisfiability Testing (SAT) , Nummer : 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. Tobias Seufert, Christoph SchollSequential Verification Using Reverse PDR 2017 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In the last few years IC3 resp. PDR made a great stir as a SAT-based hardware verification approach without needing to unroll the transition relation as in Bounded Model Checking (BMC). Motivated by different strengths of forward and backward traversal observed in BDD based model checking, we consider Reverse PDR which starts its analysis with the initial states instead of the unsafe states as in original PDR. We show great benefits of Reverse PDR both by a theoretical and an experimental analysis. Finally, we profit from parallelism offered by modern multi-core processors and use a portfolio approach combining the advantages of Reverse and original PDR. Bernd Becker, Christoph Scholl, Ralf WimmerVerification of Incomplete Designs In : Formal System Verification
State-of the-Art and Future Trends 2017, Springer International Publishing , 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?"). Ernst Althaus, Björn Beber, Werner Damm, Stefan Disch, Willem Hagemann, Astrid Rakow, Christoph Scholl, Uwe Waldmann, Boris WirtzVerification of Linear Hybrid Systems with Large Discrete State Spaces: Exploring the Design Space for Optimization Sci Comput Program , Nummer : 148, Seiten : 123 - 160, 2017 nach oben zur Jahresübersicht Valeriy Balabanov, Jie-Hong Roland Jiang, Christoph Scholl, Alan Mishchenko, Robert K. Brayton2QBF: Challenges and Solutions 2016 International Conference on Theory and Applications of Satisfiability Testing (SAT) , Springer-Verlag, Nummer : 9710, Seiten : 453 - 469» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung 2QBF is a special form \forall x \exists y. \Phi of the quantified Boolean formula (QBF) restricted to only two quantification layers, where \Phi is a quantifier-free formula. Despite its restricted form, it provides a framework for a wide range of applications, such as artificial intelligence, graph theory, synthesis, etc. In this work, we overview two main 2QBF challenges in terms of solving and certification. We contribute several improvements to existing solving approaches and study how the corresponding approaches affect certification. We further conduct an extensive experimental comparison on both competition and application benchmarks to demonstrate strengths of the proposed methodology. Ralf Wimmer, Karina Wimmer, Christoph Scholl, Bernd BeckerAnalysis of Incomplete Circuits using Dependency Quantified Boolean Formulas 2016 Int'l Workshop on Logic and Synthesis » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We consider Dependency Quantified Boolean Formulas (DQBFs), a generalization of Quantified Boolean Formulas (QBFs), and demonstrate that DQBFs are a natural calculus to exactly express the realizability problem of incomplete combinational and sequential circuits with an arbitrary number of (combinational or bounded-memory) black boxes.
In contrast to usual approaches for controller synthesis, restrictions to the interfaces of missing circuit parts in distributed architectures are strictly taken into account. We present a solution method for DQBFs together with the extraction of Skolem functions for existential variables, which can directly serve as implementations for the black boxes. First experimental results are provided. Valeriy Balabanov, Jie-Hong R. Jiang, Alan Mishchenko, Christoph SchollClauses Versus Gates in CEGAR-Based 2QBF Solving 2016 Workshop of the Thirtieth AAAI Conference on Artificial Intelligence Beyond NP » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung 2QBF is a special case of general quantified Boolean formulae (QBF). It is limited to just two quantification levels, i.e., to a form \forall X \exists Y. \Phi.
Despite this limitation it applies to a wide range of applications, e.g., to artificial intelligence, graph theory, synthesis, etc.. Recent research showed that CEGAR-based methods give a performance boost to QBF solving (e.g. compared to QDPLL). Conjunctive normal form (CNF) is a commonly accepted representation for both SAT and QBF problems; however, it does not reflect the circuit structure that might be present in the problem. Existing attempts of extracting this structure from CNF and using it in 2QBF context do not show advantages over CNF based 2QBF solvers. In this work we introduce a new workflow for 2QBF, containing a new *semantic* circuit extraction algorithm and a CEGAR-based 2QBF solver that uses circuit structure and is improved by so-called 'cofactor sharing' heuristics. We evaluate the proposed methodology on a range of benchmarks and show the practicality of the new approach. Ralf Wimmer, Christoph Scholl, Karina Wimmer, Bernd BeckerDependency Schemes for DQBF 2016 International Conference on Theory and Applications of Satisfiability Testing (SAT) , Nummer : 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 counter examples. 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 International Symposium on Automated Technology for Verification and Analysis (ATVA) » 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 Martin Böhnert, Christoph SchollTask Variants with Different Scratchpad Memory Consumption in Multi-Task Environments 2016 International Conference on Architecture of Computing Systems (ARCS) , Nummer : 9637, Seiten : 143 - 156» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We present an approach which schedules task sets using scratchpad memory (SPM) in an embedded multi-task system with real-time constraints. A new task model is introduced, where each task is represented by different pre-compiled
variants which differ in the amount of scratchpad memory used. A higher use of SPM leads to smaller run-times of a task. Moreover, the energy consumption is reduced by replacing memory accesses by SPM accesses.
Our heuristic method assembles a task set of these variants by choosing one variant per task. After selecting candidates from the pre-computed set of task variants,
the task set can be handled by a real-time scheduler like EDF.
Our approach is able to build a new incremental task set and feasible transition in dynamically changing environments.
Furthermore we show an extension of our approach to multicore environments. Christoph Scholl, Florian PigorschThe QBF Solver AIGSolve 2016 International Workshop on Quantified Boolean Formulas » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung AIGSolve is a rewriting-based solver based on And-Inverter Graphs (AIGs). In this approach, quantifiers are eliminated, starting with the inner-most quantifiers.
Intermediate results are represented symbolically using AIGs. The basic method consists of cofactor-based quantifier elimination which is combined with a multitude of optimization approaches including a SAT- and BDD-based compaction of the representations, methods for preprocessing QBF-formulas based on incremental SAT, heuristics that exchange quantifiers of the same level, heuristics that use BDD-based quantifier elimination as an alternative, as well as structure extraction and structure exploitation for the processed instances. Ernst Althaus, Björn Beber, Werner Damm, Stefan Disch, Willem Hagemann, Astrid Rakow, Christoph Scholl, Uwe Waldmann, Boris WirtzVerification of Linear Hybrid Systems with Large Discrete State Spaces: Exploring the Design Space for Optimization SFB/TR 14 AVACS Technical Report , Nummer : 103, 2016 nach oben zur Jahresübersicht Georges Morbé, Christoph SchollFully symbolic TCTL model checking for complete and incomplete real-time systems 2015 Science of Computer Programming » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In this paper we present a fully symbolic TCTL model checking algorithm for real-time systems represented in a formal model called finite state machine with time (FSMT), which works on fully symbolic state sets containing both the clock values and the state variables. Our algorithm is able to verify TCTL properties on complete and incomplete FSMTs containing unknown components. For that purpose over-approximations of state sets fulfilling a TCTL property φ for at least one implementation of the unknown components and under-approximations of state sets fulfilling φ for all possible implementations of the unknown components are computed. We present two different methods to convert timed automata to FSMTs. In addition to FSMTs simulating pure interleaving behaviour of timed automata we can produce FSMTs with a parallelized interleaving behaviour which allows parallelism of conflict-free transitions. This can dramatically reduce the number of steps during verification. Our prototype implementation outperforms the state-of-the-art model checkers UPPAAL and RED on complete systems, and on incomplete systems our tool is able to prove interesting properties when parts of the system are unknown. Ernst Althaus, Björn Beber, Joschka Kupilas, Christoph SchollImproving Interpolants for Linear Arithmetic 2015 13th International Symposium on Automated Technology for Verification and Analysis (ATVA) , Springer-Verlag, Nummer : 9364, Seiten : 48 - 63» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Craig interpolation for satisfiability modulo theory formulas have come more into focus for applications of formal verification. In this paper we, introduce a method to reduce the size of linear constraints used in the description of already computed interpolant in the theory of
linear arithmetic with respect to the number of linear constraints. We successfully improve interpolants by combining satisfiability modulo theory and linear programming in a local search heuristic. Our experimental
results suggest a lower running time and a larger reduction compared to other methods from the literature. Bernd Becker, Matthias Sauer, Christoph Scholl, Ralf WimmerModeling Unknown Values in Test and Verification In : Formal Modeling and Verification of Cyber-Physical Systems, 1st International Summer School on Methods and Tools for the Design of Digital Systems 2015, Springer Vieweg , Seiten : 122 - 150, ISBN : 978-3-658-09993-0» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung With increasing complexities and a component-based design
style the handling of unknown 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 unknowns 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 10th International Conference on Theory and Applications of Satisfiability Testing (SAT) , Springer-Verlag, Nummer : 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. Ralf Wimmer, Karina Gitina, Jennifer Nist, Christoph Scholl, Bernd BeckerPreprocessing for DQBF SFB/TR 14 AVACS Technical Report , Nummer : 110, 2015 Ralf Wimmer, Karina Gitina, Jennifer Nist, Christoph Scholl, Bernd BeckerPreprocessing for DQBF SFB/TR 14 AVACS Technical Report , Nummer : 110, 2015 Valeriy Balabanov, Jie-Hong Roland Jiang Christoph SchollSkolem functions computation for CEGAR based QBF solvers 2015 International Workshop on Quantified Boolean Formulas » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In this work we propose an approach to extract Skolem-functions from CEGAR based QBF solvers (e.g., RareQS [4]) for true QBF formulas containing 2 or 3 quantification levels. We as well propose some optimizations to improve extracted certificates and perform detailed experimental evaluation. Karina Gitina, Ralf Wimmer, Sven Reimer, Matthias Sauer, Christoph Scholl, Bernd BeckerSolving DQBF Through Quantifier Elimination 2015 Proceedings of Design, Automation & Test in Europe Conference (DATE) , Seiten : 1617 - 1622» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We show how to solve dependency quantified Boolean
formulas (DQBF) using a quantifier elimination strategy which yields an equivalent QBF that can be decided using any standard QBF solver. The elimination is accompanied by a number of optimizations which help reduce memory consumption and computation time.
We apply our solver HQS to problems from the domain of
verification of incomplete combinational circuits to demonstrate the effectiveness of the proposed algorithm. The results show enormous improvements both in the number of solved instances and in the computation times compared to existing work on validating DQBF. Karina Gitina, Ralf Wimmer, Sven Reimer, Matthias Sauer, Christoph Scholl, Bernd BeckerSolving DQBF Through Quantifier Elimination SFB/TR 14 AVACS Technical Report , Nummer : 107, 2015 nach oben zur Jahresübersicht Martin Böhnert, Christoph SchollA Dynamic Virtual Memory Management under Real-Time Constraints 2014 RTCSA, Chongqing, IEEE » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In this work we describe a new memory management concept which allows the use of both virtual and dynamic memory management at the same time in the context of real-time systems. For a fixed size of the virtual address space, the operations of memory allocation, de-allocation and access have a constant complexity. Therefore our approach is highly suited for real-time environments with hard deadlines. We employ efficient data-structures to yield runtimes that are close to traditional static memory management concepts,
and -- at the same time -- provide the user with the full flexibility of both virtual and dynamic memory management. Our approach is based on novel operating system components and a novel real-time aware virtual memory management unit (RTMMU) in hardware.
Our experimental results demonstrate the applicability of our concept and compare its performance with a classical approach. The results show that our new approach does not only provide constant-time memory management operations, but is also able to reduce the memory footprint to a large extent. Georges Morbé, Christian Miller, Christoph Scholl, Bernd BeckerCombined Bounded and Symbolic Model Checking for Incomplete Timed Systems 2014 Haifa Haifa Verification Conference (HVC) , Yahav, Eran, Band : 8855, Seiten : 30 - 47» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We present a hybrid model checking algorithm for incomplete timed systems where parts of the system are unspecified (so-called black boxes). Here, we answer the question of unrealisability, i.e., “Is there a path violating a safety property regardless of the implementation of the black boxes?” Existing bounded model checking (BMC) approaches for incomplete timed systems exploit the power of modern SMT solvers, but might be too coarse as an abstraction for certain problem instances. On the other hand, symbolic model checking (SMC) for incomplete timed systems is more accurate, but may fail due to the size of the explored state space. In this work, we propose a tight integration of a backward SMC routine with a forward BMC procedure leveraging the strengths of both worlds. The symbolic model checker is hereby used to compute an enlarged target which we then try to hit using BMC. We use learning strategies to guide the SMT solver’s search into the right direction and manipulate the enlarged target to improve the overall accuracy of the current verification run. Our experimental results show that the hybrid approach is able to verify incomplete timed systems which are out of the scope for BMC and can neither be solved in reasonable time using SMC. Furthermore, our approach compares favourably with UPPAAL-TIGA when considering timed games as a special case of the unrealisability problem. Georges Morbé, Christoph SchollFully Symbolic TCTL Model Checking for Complete and Incomplete Real-Time Systems 2014 AVACS Technical Report, Nummer 104 » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In this paper we introduce a new formal model, called finite state machines with time (FSMT), to represent real-time systems. We present a model checking algorithm for FSMTs, which works on fully symbolic state sets containing both the clock values and the state variables. Besides complete networks of FSMTs our algorithm can verify incomplete real-time systems in form of incomplete FSMTs, and is able to prove that a TCTL property is violated or satisfied regardless of the implementation of unknown components in the system. For that purpose the algorithm
computes over-approximations of sets of states fulfilling a TCTL property Φ for at least one implementation of the unknown components and under-approximations of sets of states fulfilling Φ for all possible implementations of the unknown components. In order to verify timed automata with our model checking algorithm, we present two different methods to convert timed automata to FSMTs. In addition to pure interleaving semantics we can convert timed automata to FSMTs having a parallelized interleaving behaviour which allows parallelism of transitions causing no conflicts. This can dramatically reduce the number of steps during verification. In our experimental results on complete systems our prototype implementation outperforms the state-of-the-art model checkers UPPAAL and RED, and on incomplete systems our tool is able to prove interesting properties at early stages of the design when parts of the overall system
may not yet be finished. Additionally, fading out components of a large system may dramatically reduce the complexity of the system and thus the effort for verification. Christoph Scholl, Florian Pigorsch, Stefan Disch, Ernst AlthausSimple Interpolants for Linear Arithmetic 2014 DATE , EDA Consortium San Jose, CA, USA / ACM DL nach oben zur Jahresübersicht Karina Gitina, Sven Reimer, Matthias Sauer, Ralf Wimmer, Christoph Scholl, Bernd BeckerEquivalence Checking for Partial Implementations Revisited 2013 MBMV , Seiten : 61 - 70 Karina Gitina, Sven Reimer, Matthias Sauer, Ralf Wimmer, Christoph Scholl, Bernd BeckerEquivalence checking of partial designs using dependency quantified Boolean formulae 2013 IEEE 31st International Conference on Computer Design (ICCD) , Seiten : 396 - 403 Georges Morbé, Christoph SchollFully Symbolic Model Checking for Incomplete Systems of Timed Automata 2013 Electronic Communications of the EASST, Proceedings of AVOCS 2013 , Band : 66 Florian Pigorsch, Christoph SchollLemma localization: a practical method for downsizing SMT-interpolants 2013 DATE , EDA Consortium San Jose, CA, USA / ACM DL, Seiten : 1405 - 1410 Christian Miller, Christoph Scholl, Bernd BeckerProving QBF-Hardness in Bounded Model Checking for Incomplete Designs 2013 MTV , IEEE Computer Society Tobias Nopper, Christoph SchollSymbolic Model Checking for Incomplete Designs with Flexible Modeling of Unknowns 2013 IEEE Trans. Computers , Band : 62, Nummer : 6, Seiten : 1234 - 1254 nach oben zur Jahresübersicht Sven Reimer, Florian Pigorsch, Christoph Scholl, Bernd BeckerEnhanced Integration of QBF Solving Techniques 2012 MBMV , Seiten : 133 - 143 Werner Damm, Henning Dierks, Stefan Disch, Willem Hagemann, Florian Pigorsch, Christoph Scholl, Uwe Waldmann, Boris WirtzExact and fully symbolic verification of linear hybrid automata with large discrete state spaces 2012 Sci. Comput. Program. , Band : 77, Nummer : 10-11, Seiten : 1122 - 1150 Georges Morbé, Christoph SchollFully Symbolic Model Checking for Incomplete Systems of Timed Automata 2012 MBMV , Seiten : 97 - 108 Georges Morbé, Christoph SchollGuaranteeing Termination of Fully Symbolic Timed Forward Model Checking 2012 MTV , IEEE Computer Society, Seiten : 35 - 40 nach oben zur Jahresübersicht Georges Morbé, Florian Pigorsch, Christoph SchollFully Symbolic Model Checking for Timed Automata 2011 CAV , Springer, Band : 6806, Seiten : 616 - 632 Georges Morbé, Christoph SchollFully Symbolic Model Checking for Timed Automata 2011 MBMV , Seiten : 9 - 18 Werner Damm, Stefan Disch, Willem Hagemann, Christoph Scholl, Uwe Waldmann, Boris WirtzIntegrating Incremental Flow Pipes into a Symbolic Model Checker for Hybrid Systems SFB/TR 14 AVACS Technical Report , Nummer : 76, 2011 Sven Reimer, Florian Pigorsch, Christoph Scholl, Bernd BeckerIntegration of orthogonal QBF solving techniques 2011 DATE , IEEE, Seiten : 149 - 154 Christian Miller, Christoph Scholl, Bernd BeckerVerifying Incomplete Networks of Timed Automata 2011 MBMV , Seiten : 113 - 122 nach oben zur Jahresübersicht Thorsten Zitterell, Christoph SchollA probabilistic and energy-efficient scheduling approach for online application in real-time systems 2010 DAC , ACM, Seiten : 42 - 47 Florian Pigorsch, Christoph SchollAn AIG-Based QBF-solver using SAT for preprocessing 2010 DAC , ACM, Seiten : 170 - 175 Christian Miller, Karina Gitina, Christoph Scholl, Bernd BeckerBounded Model Checking of Incomplete Networks of Timed Automata 2010 MTV , IEEE, Seiten : 61 - 66 Tobias Nopper, Christian Miller, Matthew Lewis, Bernd Becker, Christoph SchollSAT Modulo BDD – A Combined Verification Approach for Incomplete Designs 2010 MBMV , Fraunhofer Verlag, 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 TACAS , Springer, Band : 5505, Seiten : 383 - 397 Florian Pigorsch, Christoph SchollExploiting structure in an AIG based QBF solver 2009 DATE , IEEE, Seiten : 1596 - 1601 Christian Miller, Tobias Nopper, Christoph SchollSymbolic CTL Model Checking for Incomplete Designs by Selecting Property-Specific Subsets of Local Component Assumptions 2009 MBMV , Seiten : 87 - 96 Florian Pigorsch, Christoph SchollUsing Implications for Optimizing State Set Representations of Linear Hybrid Systems 2009 MBMV , Seiten : 77 - 86 nach oben zur Jahresübersicht Martin Böhnert, Thorsten Zitterell, Christoph SchollDynamische Verwaltung Virtuellen Speichers für Echtzeitsysteme 2008 Echtzeit , Springer, Seiten : 101 - 110 Thorsten Zitterell, Christoph SchollImproving energy-efficient real-time scheduling by exploiting code instrumentation 2008 International Workshop on Real Time Software (RTS’08) , IEEE, Seiten : 763 - 771 Christoph Scholl, Stefan DischMethoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), Freiburg, Germany, March 3-5, 2008 2008 Shaker Matthias Sippel, Axel Rottmann, Thorsten Zitterell, Bastian Steder, Christoph Scholl, Wolfram Burgard, Leonhard ReindlMultisensor-Navigation für autonome Flugroboter 2008 Proceedings 14. GMA/ITG-Fachtagung Sensoren und Messsysteme , Seiten : 667 - 676 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 New York, NY, USA Proceedings of the Joint Workshops of the 6th International Workshop on Satisfiability Modulo Theories and 1st International Workshop on Bit-Precise Reasoning , ACM, Seiten : 18 - 26 nach oben zur Jahresübersicht Stefan Disch, Christoph SchollCombinational Equivalence Checking Using Incremental SAT Solving, Output Ordering, and Resets 2007 ASP Design Automation Conf. » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Combinational equivalence checking is an essential task in circuit design. In this paper we focus on SAT based equivalence checking making use of incremental SAT techniques which are well known from the application inBounded Model Checking. Based on an analysis of shared circuit structures we present heuristics which try to maximize the benefit from incremental SAT solving in this application by looking for good orders in which the equivalence of different circuit outputs is checked. Moreover, we present a reset strategy for situations where the benefit from the incremental SAT approach seems to decrease. Experimental results prove that our novel method outperforms traditional methods significantly. Tobias Nopper, Christoph Scholl, Bernd BeckerComputation of Minimal Counterexamples by Using Black Box Techniques and Symbolic Methods 2007 San Jose International Conference on Computer Aided Design (ICCAD) , IEEE Computer Society Press» 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 behavior — 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. Tobias Nopper, Christoph SchollCounterexample Generation for Incomplete Designs 2007 Erlangen GI/ITG/GMM Workshop“Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” , Shaker Verlag, Aachen, Seiten : 193 - 202» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Counterexample generation is a crucial task for error diagnosis and debugging of sequential circuits.The simpler a counterexample is - i.e. more general and fewer assigned input values - the better it can be understood by humans. We will use the concept of Black Boxes - parts of the design with unknown behavior - to mask out components for counterexample computation. By this, the resulting counterexample will argue about a reduced number of components in the system in order to facilitate the task of understanding and correcting the error effect. Werner Damm, Stefan Disch, Hardi Hungar, Swen Jacobs, Jun Pang, Florian Pigorsch, Christoph Scholl, Uwe Waldmann, Boris WirtzExact State Set Representations in the Verification of Linear Hybrid Systems with Large Discrete State Space 2007 Berlin / Heidelberg Automated Technology for Verification and Analysis , Springer, Band : 4762, Seiten : 425 - 440» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We propose algorithms significantly extending the limits for maintaining exact representations in the verification of linear hybrid systems with large discrete state spaces. We use AND-Inverter Graphs (AIGs) extended with linear constraints (LinAIGs) as symbolic representation of the hybrid state space, and show how methods for maintaining compactness of AIGs can be lifted to support model-checking of linear hybrid systems with large discrete state spaces. This builds on a novel approach for eliminating sets of redundant constraints in such rich hybrid state representations by a suitable exploitation of the capabilities of SMT solvers, which is of independent value beyond the application context studied in this paper. We used a benchmark derived from an Airbus flap control system (containing 220 discrete states) to demonstrate the relevance of the approach.This work was partly supported by the German Research Council (DFG) as part of the Transregional Collaborative Research Center “Automatic Verification and Analysis of Complex Systems” (SFB/TR 14 AVACS, http://www.avacs.org/). Tobias Nopper, Christoph SchollSymbolic Model Checking for Incomplete Designs with Flexible Modeling of Unknowns SFB/TR 14 AVACS Technical Report , Nummer : 31, 2007 Axel Rottmann, Matthias Sippel, Thorsten Zitterell, Wolfram Burgard, Leonhard Reindl, Christoph SchollTowards an Experimental Autonomous Blimp Platform 2007 Proceedings of the 3rd European Conference on Mobile Robots, EMCR 2007 nach oben zur Jahresübersicht Marc Herbstritt, Bernd Becker, Christoph SchollAdvanced SAT-Techniques for Bounded Model Checking of Blackbox Designs 2006 Proc. of Microprocessor Test and Verification Workshop (MTV) , IEEE Computer Society Florian Pigorsch, Christoph Scholl, Stefan DischAdvanced Unbounded CTL Model Checking By Using AIGs, BDD Sweeping, And Quantifier Scheduling 2006 GI/ITG/GMM Workshop“Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In this paper we present a complete method for verifying properties expressed in the temporal logic CTL. In contrast to the majority of verification methods presented in recent years, we support unbounded model checking based on symbolic representations of characteristic functions. Among others, our method is based on an advanced And-Inverter Graph (AIG) implementation, quantifier scheduling, and BDD sweeping. For several examples, our method outperforms BDD based symbolic model checking by orders of magnitude. However, our approach is also able to produce competitive results for cases where BDD are known to perform well. Florian Pigorsch, Christoph Scholl, Stefan DischAdvanced Unbounded Model Checking Based on AIGs, BDD Sweeping, And Quantifier Scheduling 2006 Proceedings of the Conference on Formal Methods in Computer Aided Design (FMCAD) , IEEE Computer Society Press, Seiten : 89 - 96» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In this paper we present a complete method for verifying properties expressed in the temporal logic CTL. In contrast to the majority of verification methods presented in recent years, we support unbounded model checking based on symbolic representations of characteristic functions. Among others, our method is based on an advanced And-Inverter Graph (AIG) implementation, quantifier scheduling, and BDD sweeping. For several examples, our method outperforms BDD based symbolic model checking by orders of magnitude. However, our approach is also able to produce competitive results for cases where BDD are known to perform well. Werner Damm, Stefan Disch, Hardi Hungar, Jun Pang, Florian Pigorsch, Christoph Scholl, Uwe Waldmann, Boris WirtzAutomatic verification of hybrid systems with large discrete state space 2006 Proceedings of the 4th International Symposium on Automated Technology for Verification and Analysis , Springer-Verlag, Band : 4218» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We address the problem of model checking hybrid systems which exhibit nontrivial discrete behavior and thus cannot be treated by considering the discrete states one by one, as most currently available verification tools do. Our procedure relies on a deep integration of several techniques and tools. An extension of And-Inverter-Graphs (AIGs) with first-order constraints serves as a compact representation format for sets of configurations which are composed of continuous regions and discrete states. Boolean reasoning on the AIGs is complemented by first-order reasoning in various forms and on various levels. These include implication checks for simple constraints, test vector generation for fast inequality checks of boolean combinations of constraints, and an exact subsumption check for representations of two configurations. These techniques are integrated within a model checker for universal CTL. Technically, it deals with discrete-time hybrid systems with linear differentials. The paper presents the approach, its prototype implementation, and first experimental data. nach oben zur Jahresübersicht Tobias Nopper, Christoph SchollFlexible Modeling of Unknowns in Model Checking for Incomplete Designs 2005 8. 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 incomplete design (i.e. a design containing so-called Black Boxes) can still be extended to a complete design satisfying a given property or whether the property is satisfied for all possible extensions.In this paper we extend a method based on a series of approximate, yet sound algorithms to prove or disprove CTL properties for incomplete designs. Each algorithm in the previous approach was able to model the effect of the unknown information at the outputs of the Black Boxes at a different level of accuracy (leading to different requirements for computational resources). In this paper we present a novel approach which is able to use different methods for modeling unknowns at the outputs of different Black Boxes within a single model checking run. This permits us to handle less relevant Black Boxes (in terms of the CTL formula) with larger approximation and thus faster, whereas we do not lose important information when the possible effect of more relevant Black Boxes is modeled by more exact methods.Finally we give a series of experimental results demonstrating the effectiveness and feasibility of the new method. nach oben zur Jahresübersicht Tobias Nopper, Christoph SchollApproximate Symbolic Model Checking for Incomplete Designs 2004 Austin, Texas Formal Methods in Computer-Aided Design , Springer Verlag, Band : 3312, Seiten : 290 - 305» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We consider the problem of checking whether an incomplete design can still be extended to a complete design satisfying a given CTL formula and whether the property is satisfied for all possible extensions. Motivated by the fact that well-known model checkers like SMV or VIS produce incorrect results when handling unknowns by using the programs’ non-deterministic signals, we present a series of approximate, yet sound algorithms to process incomplete designs with increasing quality and computational resources. Finally we give a series of experimental results demonstrating the effectiveness and feasibility of the presented methods. Tobias Nopper, Christoph SchollApproximate Symbolic Model Checking of Incomplete Designs 2004 13th Int’l Workshop on Logic Synth. , Band : 13, Seiten : 377 - 384» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We consider the problem of checking whether an incomplete design can still be extended to a complete design satisfying a given CTL formula and whether the property is satisfied for all possible extensions.Motivated by the fact that well-known model checkers like SMV or VIS produce incorrect results when handling unknowns by using the programs’ non-deterministic signals, we present a series of approximate, yet sound algorithms to process incomplete designs with increasing quality and computational resources.Finally we give a series of experimental results demonstrating theeffectiveness and feasibility of the presented methods. Christoph Scholl, Matthias BücheFilter Based Diagnosis for Multiple Design Errors 2004 GI/ITG/GMM-Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” Tobias Nopper, Christoph SchollSymbolic Model Checking of Incomplete Designs Technical Report Albert-Ludwigs-University , Nummer : 201, 2004 nach oben zur Jahresübersicht Christoph Scholl, Bernd BeckerChecking Equivalence for Circuits Containing Incompletely Specified Boxes 2002 Int’l Conf. on Comp. Design » 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 ITG/GI/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. Christoph Scholl, Bernd Becker, Thomas WeisOn WLCDs and the Complexity of Word-Level Decision Diagrams - A Lower Bound for Division 2002 Formal Methods in System Design , Band : 20, Nummer : 3, Seiten : 311 - 326 nach oben zur Jahresübersicht Christoph Scholl, Bernd BeckerChecking Equivalence for Partial Implementations 2001 ITG/GI/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 Design Automation Conf. , Seiten : 238 - 243 Christoph Scholl, Marc Herbstritt, Bernd BeckerDon’t Care Minimization of *BMDs 2001 ITG/GI/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 Int’l Symp. Circ. and Systems Kluwer Academic Publishers Functional Decomposition with Application to FPGA Synthesis Christoph Scholl Christoph Scholl, Bernd Becker, Andreas BrogleThe Multiple Variable Order Problem for Binary Decision Diagrams 2001 ASP Design Automation Conf. » 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 Technical Report Albert-Ludwigs-University , Nummer : 145, 2000 Andreas Hett, Christoph Scholl, Bernd BeckerDistance Driven Finite State Machine Traversal 2000 Design Automation Conf. , 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. Christoph Scholl, Marc Herbstritt, Bernd BeckerExploiting Don’t Cares to Minimize *BMDs Technical Report Albert-Ludwigs-University , Nummer : 141, 2000 Christoph Scholl, Bernd BeckerOn the Generation of Multiplexer Circuits for Pass Transistor Logic 2000 Design, Automation and Test in Europe , Seiten : 372 - 378 Andreas Hett, Christoph Scholl, Bernd BeckerState Traversal guided by Hamming Distance Profiles 2000 ITG/GI/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, Dirk Möller, Paul Molitor, Rolf DrechslerBDD Minimization Using Symmetries 1999 IEEE Trans. on CAD , Band : 18, Nummer : 2, Seiten : 81 - 100 B.G. Teubner Datenstrukturen und effiziente Algorithmen fuer die Logiksynthese kombinatorischer Schaltungen Paul Molitor, Christoph Scholl 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, Andreas 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, Andreas BrogleSolving the Multiple Variable Order Problem for Binary Decision Diagram by Use of Dynamic Reordering Techniques Technical Report Albert-Ludwigs-University , Nummer : 130, 1999 nach oben zur Jahresübersicht Christoph SchollMulti-output Functional Decomposition with Exploitation of Don’t Cares 1998 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, Thomas 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, Dirk Möller, Paul Molitor, Rolf DrechslerBDD Minimization Using Symmetries Technical Report, Institute for Computer Science, University Halle , Band : 97-32, 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 Int’l. Conf. on Computer Aided Design , Seiten : 8 - 12 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 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, Stefan Melchior, Günter Hotz, Paul MolitorMinimizing ROBDD Sizes of Incompletely Specified Boolean Functions by Exploiting Strong Symmetries 1997 European Design & Test Conf. , Seiten : 229 - 234» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We present a method computing a minimum sized partition of the variables of an incompletely specified Boolean function into symmetric groups. The method can be used during minimization of ROBDDs of incompletely specified Boolean functions. We apply it as a preprocessing step of symmetric sifting presented by Panda (1994) and Möller (1994) and of techniques for ROBDD minimization of incompletely specified Boolean functions presented by Chang (1994) and Shiple (1994). The technique is shown to be very effective: it improves ROBDD sizes of symmetric sifting by a factor of 51 percent and by a factor of 70 percent in combination with a slightly modified version of the technique of Chang and Shiple. 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. nach oben zur Jahresübersicht Christoph Scholl, Paul MolitorCommunication Based FPGA Synthesis for Multi-Output Boolean Functions 1995 ASP Design Automation Conf. , Seiten : 279 - 287» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung One of the crucial problems multi-level logic synthesis techniques for multi-output boolean functions f = (f_1, ...,f_m): 0, 1^n to 0,1^m have to deal with is finding sublogic which can be shared by different outputs, i.e., finding boolean functions alpha =( alpha _1, ..., alpha _h): 0, 1^p to 0,1^h which can be used as common sublogic of good realizations of f_1, ...,f_m. In this paper we present an efficient ROBDD based implementation of this Common Decomposition Functions Problem (CDF). Formally, CDF is defined as follows: Given m boolean functions f_1, ...,f_m 0, 1^n to 0,1^m, and two natural numbers p and h, find h boolean functions alpha _1, ..., alpha _h : 0, 1^p to 0,1^h such that for all 1 leq k leq m there is a decomposition of f_k of the form f_k(x_1, ..., x_n) = g^(k)( alpha _1(x_1, ..., x_p), ..., alpha _h(x_1, ..., x_p), alpha ^(k)_h+1(x_1, ..., x_p), ..., alpha ^(k)_r_k(x_1, ..., x_p), x_p+1 , ..., x_n) using a minimal number r_k of single-output boolean decomposition functions. Experimental results applying the method to FPGA synthesis are promising. Christoph Scholl, Paul MolitorEfficient ROBDD based computation of common decomposition functions of multioutput boolean functions In : Novel Approaches in Logic and Architecture Synthesis 1995, Chapman\,&\,Hall , Seiten : 57 - 63, » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung One of the crucial problems multi-level logic synthesis techniques for multi-output boolean functions f = (f_1, ...,f_m): 0, 1^n to 0,1^m have to deal with is finding sublogic which can be shared by different outputs, i.e., finding boolean functions alpha =( alpha _1, ..., alpha _h): 0, 1^p to 0,1^h which can be used as common sublogic of good realizations of f_1, ...,f_m. In this paper we present an efficient ROBDD based implementation of this Common Decomposition Functions Problem (CDF). Formally, CDF is defined as follows: Given m boolean functions f_1, ...,f_m 0, 1^n to 0,1^m, and two natural numbers p and h, find h boolean functions alpha _1, ..., alpha _h : 0, 1^p to 0,1^h such that for all 1 leq k leq m there is a decomposition of f_k of the form f_k(x_1, ..., x_n) = g^(k)( alpha _1(x_1, ..., x_p), ..., alpha _h(x_1, ..., x_p), alpha ^(k)_h+1(x_1, ..., x_p), ..., alpha ^(k)_r_k(x_1, ..., x_p), x_p+1 , ..., x_n) using a minimal number r_k of single-output boolean decomposition functions. nach oben zur Jahresübersicht Paul Molitor, Christoph SchollCommunication Based Multilevel Synthesis for Multi-Output Boolean Functions 1994 Great Lakes Symp. VLSI , Seiten : 101 - 104» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung A multilevel logic synthesis technique for multi-output boolean functions is presented which is based on minimizing the communication complexity. Unlike the approaches known from literature ([Ash59], [Kar63], [HOI90], [HOI92]) which in the final analysis decompose each single-output function f_i of a multi-output function f = f_1, ...,f_m independently of the other single-output functions f_j (j neq i), the approach presented in this paper gives special attention to the fact that there possibly exist some decomposition functions which can be used by different outputs during the decomposition of the single-output functions of f. The benchmarking results (taken from 1989 MCNC multilevel logic benchmarks) which close the paper are promising. Paul Molitor, Christoph SchollCommunication Based Multilevel Synthesis for Multi-Output Boolean Functions Informatik-Berichte Humbold-University , Nummer : 29, 1994 Christoph Scholl, Paul MolitorEfficient ROBDD Based Computation of Common Decomposition Functions of Multi-Output Boolean Functions 1994 IFIP Workshop on Logic and Architecture Synthesis, Grenoble , Seiten : 61 - 70» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung One of the crucial problems multi-level logic synthesis techniques for multi-output boolean functions f = (f_1, ...,f_m): 0, 1^n to 0,1^m have to deal with is finding sublogic which can be shared by different outputs, i.e., finding boolean functions alpha =( alpha _1, ..., alpha _h): 0, 1^p to 0,1^h which can be used as common sublogic of good realizations of f_1, ...,f_m. In this paper we present an efficient ROBDD based implementation of this Common Decomposition Functions Problem (CDF). The key concept of our method is the exploitation of "equivalences" of the functions f_1, ...,f_m which considerably reduces the running time of the tool. Formally, CDF is defined as follows: Given m boolean functions f_1, ...,f_m 0, 1^n to 0,1^m, and two natural numbers p and h, find h boolean functions alpha _1, ..., alpha _h : 0, 1^p to 0,1^h such that for all 1 leq k leq m there is a decomposition of f_k of the form f_k(x_1, ..., x_n) = g^(k)( alpha _1(x_1, ..., x_p), ..., alpha _h(x_1, ..., x_p), alpha ^(k)_h+1(x_1, ..., x_p), ..., alpha ^(k)_r_k(x_1, ..., x_p), x_p+1 , ..., x_n) using a minimal number r_k of single-output boolean decomposition functions. nach oben zur Jahresübersicht