Professur für Betriebssysteme - Universität Freiburg

Publikationen

Jahre: 2024 | 2023 | 2022 | 2021 | 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

2024

nach oben zur Jahresübersicht

Alexander Konrad, Christoph Scholl, Alireza Mahzoon, Daniel Große, Rolf Drechsler
Divider Verification Using Symbolic Computer Algebra and Delayed Don't Care Optimization: Theory and Practical Implementation
2024 Formal Methods in System Design
KurzfassungRecent methods based on Symbolic Computer Algebra (SCA) have shown great success in formal verification of multipliers and - more recently - of dividers as well. In this paper we enhance known approaches by the computation of satisfiability don't cares for so-called Extended Atomic Blocks (EABs) and by Delayed Don't Care Optimization (DDCO) for optimizing polynomials during backward rewriting. Using those novel methods we are able to extend the applicability of SCA-based methods to further divider architectures which could not be handled by previous approaches. We succesfully apply the approach to the fully automatic formal verification of large dividers (with bit widths up to 512).
Christoph Scholl, Tobias Seufert, Fabian Siegwolf
Hierarchical Stochastic SAT and Quality Assessment of Logic Locking
2024 SAT
KurzfassungMotivated by the application of quality assessment of logic locking we introduce Hierarchical Stochastic SAT (HSSAT) which generalizes Stochastic SAT (SSAT). We look into the complexity of HSSAT and for solving HSSAT formulas we provide a prototype solver which computes exact evaluation results (i.e., without any approximation and without any imprecision caused by numerical rounding errors). Finally, we perform an intensive experimental evaluation of our HSSAT solver in the context of quality assessment of logic locking.
Alexander Konrad, Christoph Scholl
Symbolic Computer Algebra for Multipliers Revisited - Its All About Orders and Phases
2024 Proceedings of the 24th Conference on Formal Methods in Computer-Adied Design - FMCAD 2024, TU Wien Academic Press
KurzfassungUsing Symbolic Computer Algebra (SCA) enabled a huge progress in formal verification of arithmetic circuits in recent years. Several different approaches have been proposed showing great success especially for the verification of multipliers. Some of them are based on precomputing and simplifying polynomials for specific circuit structures like converging cones while others take advantage of known or detected hierarchy information to replace and simplify particular sub-circuits of the design. In this paper we propose a new method that avoids the use of such methods and applies only two dynamic approaches: (1) choosing a good substitution order for the backward rewriting process and (2) adjusting the phases of signals occuring in the intermediate polynomials during the verification process. Both methods are simply based on a greedy local search taking the the sizes of intermediate polynomials into account. Our experimental results show that this method is very competitive with already existing tools and it improves their robustness, e.g. against optimizations of the verified circuits using logic synthesis.

2023

nach oben zur Jahresübersicht

Alexander Konrad, Christoph Scholl, Alireza Mahzoon, Daniel Große, Rolf Drechsler
Divider Verification Using Symbolic Computer Algebra and Delayed Don’t Care Optimization (extended abstract)
2023 MBMV
KurzfassungRecent methods based on Symbolic Computer Algebra (SCA) have shown great success in formal verification of multipliers and -- more recently -- of dividers as well. Here we give an overview of our work published in [1-3] which enhances SCA-based verification by the computation of satisfiability don't cares for so-called (Extended) Atomic Blocks (EABs) and by Delayed Don't Care Optimization (DDCO) for optimizing polynomials during backward rewriting. The optimization is reduced to Integer Linear Programming (ILP). Whereas the basic methods using SCA failed for divider verification, using those novel methods we are able to verify (formally and fully automatically) large gate level implementations of several divider architectures (with bit widths up to 512).
Tobias Seufert, Felix Winterer, Christoph Scholl, Karsten Scheibler, Tobias Paxian, Bernd Becker
Everything You Always Wanted to Know About Generalization of Proof Obligations in PDR
2023 IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Band: 42, Nummer: 4, Seiten: 1351 - 1364
KurzfassungIn this article we revisit the topic of generalizing proof obligations in bit-level Property Directed Reachability (PDR). We provide a comprehensive study which (1) determines the complexity of the problem, (2) thoroughly analyzes limitations of existing methods, (3) introduces approaches to proof obligation generalization that have never been used in the context of PDR, (4) compares the strengths of different methods from a theoretical point of view, and (5) intensively evaluates the methods on various benchmarks from Hardware Model Checking as well as from AI Planning.
Tobias Seufert
On Safety Verification using PDR and Reverse PDR
2023 Dissertation

2022

nach oben zur Jahresübersicht

Tobias Seufert, Christoph Scholl, Arun Chandrasekharan, Sven Reimer, Tobias Welp
Making PROGRESS in Property Directed Reachability
2022 23rd International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2022)
KurzfassungWith Proof-Guided Restriction Skipping (PROGRESS) we present a fully automatic and complete approach for Hardware Model Checking under restrictions. We use the PROGRESS approach in the context of PDR/IC3 [9, 18]. Our implementation of PDR/IC3 restricts input signals as well as state bits of a circuit to constants in order to quickly explore long execution paths of the design. We are able to identify spurious proofs of safety along the way and exploit information from these proofs to guide the relaxation of the restrictions. Hence, we greatly improve the capability of PDR to find counterexamples, especially with long error paths. In experiments with HWMCC benchmarks our approach is able to double the amount of detected deep counterexamples in comparison to Bounded Model Checking as well as in comparison to PDR.
Alexander Konrad, Christoph Scholl, Alireza Mahzoon, Daniel Große, Rolf Drechsler
Divider Verification Using Symbolic Computer Algebra and Delayed Don't Care Optimization
2022 Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design (FMCAD), TU Wien Academic Press
KurzfassungRecent methods based on Symbolic Computer Algebra (SCA) have shown great success in formal verification of multipliers and - more recently - of dividers as well. In this paper we enhance known approaches by the computation of satisfiability don't cares of so-called Extended Atomic Blocks (EABs) and by Delayed Don't Care Optimization (DDCO) for optimizing polynomials during backward rewriting. Using those novel methods we are able to extend the applicability of SCA-based methods to further divider architectures which could not be handled by previous approaches. We successfully apply the approach to the fully automatic formal verification of large dividers (with bit widths up to 512).

2021

nach oben zur Jahresübersicht

Tobias Seufert, Felix Winterer, Christoph Scholl, Karsten Scheibler, Tobias Paxian, Bernd Becker
Everything You Always Wanted to Know About Generalization of Proof Obligations in PDR
CoRR, Band: 2105.09169, 2021
KurzfassungIn this paper we revisit the topic of generalizing proof obligations in bit-level Property Directed Reachability (PDR). We provide a comprehensive study which (1) determines the complexity of the problem, (2) thoroughly analyzes limitations of existing methods, (3) introduces approaches to proof obligation generalization that have never been used in the context of PDR, (4) compares the strengths of different methods from a theoretical point of view, and (5) intensively evaluates the methods on various benchmarks from Hardware Model Checking as well as from AI Planning.
Karsten Scheibler, Felix Winterer, Tobias Seufert, Tino Teige, Christoph Scholl, Bernd Becker
ICP and IC3
2021 DATE, IEEE
KurzfassungIf embedded systems are used in safety-critical environments,they need to meet several standards. For example, in the automotive domain the ISO 26262 standard requires that the software running on such systems does not contain unreachable code. Software model checking is one effective approach to automatically detect such dead code. Being used in a commercial product, iSAT3 already performs very well in this context. In this paper we integrate IC3 into iSAT3 in order to improve its dead code detection capabilities even further.
Felix Winterer, Tobias Seufert, Karsten Scheibler, Tino Teige, Christoph Scholl, Bernd Becker
ICP and IC3 with Stronger Generalization
2021 MBMV
Kurzfassungon interval abstraction and Interval Constraint Propagation (ICP). As strong generalization is one of the key aspects for the IC3 algorithm to be successful, we integrate two additional generalization schemes from literature into iSAT3+IC3: Inductive Generalization and Counterexamples To Generalization (CTG). Furthermore, we evaluate the benefits and the drawbacks of different variants of these methods in the context of interval abstraction and ICP.
Aile Ge-Ernst, Christoph Scholl, Ralf Wimmer
Solving Dependency Quantified Boolean Formulas Using Quantifier Localization
CoRR, Band: 1905.04755, 2021
Christoph Scholl, Alexander Konrad, Alireza Mahzoon, Daniel Große, Rolf Drechsler
Verifying Dividers Using Symbolic Computer Algebra and Don’t Care Optimization
2021 DATE, IEEE
KurzfassungOur experimental results show that this method is the key for enabling the verification of large and optimized non-restoring dividers (with bit widths up to 512).

2020

nach oben zur Jahresübersicht

Christoph Scholl, Alexander Konrad
Symbolic Computer Algebra and SAT Based Information Forwarding for Fully Automatic Divider Verification
2020 Design Automation Conf., Seiten: 1 - 6
Kurzfassungthe 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 Drechsler
Towards Formal Verification of Optimized and Industrial Multipliers
2020 Conference on Design, Automation and Test in Europe (DATE), Seiten: 544 - 549
Kurzfassungand 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.

2019

nach oben zur Jahresübersicht

Christoph Scholl, Jie-Hong Roland Jiang, Ralf Wimmer, Aile Ge-Ernst
A PSPACE Subclass of Dependency Quantified Boolean Formulas and Its Effective Solving
2019 33th AAAI Conference on Artificial Intelligence (AAAI-19)
KurzfassungRecently 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 Scholl
Incremental Inprocessing in SAT Solving
2019 10th International Conference on Theory and Applications of Satisfiability Testing (SAT), Springer-Verlag, Nummer: 11628, Seiten: 136 - 154
Kurzfassungproblems 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 Wimmer
Localizing Quantifiers for DQBF
2019 Proceedings of the Conference on Formal Methods in Computer Aided Design (FMCAD), IEEE Computer Society Press
KurzfassungDependency 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 Wimmer
Quantifier Localization for DQBF
2019 Int'l Workshop on Logic and Synthesis
Kurzfassungthat quantifier localization pays off in this context.
Ralf Wimmer, Christoph Scholl, Bernd Becker
The (D)QBF Preprocessor HQSpre – Underlying Theory and Its Implementation
2019 Journal on Satisfiability, Boolean Modeling and Computation, Band: 11, Nummer: 1, Seiten: 3 - 52
KurzfassungPreprocessing 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 Scholl
fbPDR: In-depth Combination of Forward and Backward Analysis in Property Directed Reachability
2019 Conference on Design, Automation and Test in Europe (DATE)
KurzfassungWe 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 Scholl
fbPDR: 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”
Kurzfassungand demonstrate the effectiveness of our approach on benchmarks from the Hardware Model Checking Competition.

2018

nach oben zur Jahresübersicht

Ralf Wimmer, Karina Wimmer, Christoph Scholl, Bernd Becker
Analysis of Incomplete Circuits Using Dependency Quantified Boolean Formulas
In: Advanced Logic Synthesis
2018, Springer International Publishing, André Inácio Reis, Rolf Drechsler, Seiten: 151 - 168, André Inácio Reis, Rolf Drechsler, ISBN: 978-3-319-67294-6
KurzfassungWe 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 Scholl
Combining PDR and Reverse PDR for Hardware Model Checking
2018 Conference on Design, Automation and Test in Europe (DATE)
Kurzfassungcombined approach.
Christoph Scholl, Ralf Wimmer
Dependency 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
KurzfassungDependency quantified Boolean formulas (DQBFs) as a generalization of quantified Boolean formulas (QBFs) have received considerable attention in research during the last years. Here we give an overview of the solution methods developed for DQBF so far. The exposition is complemented with the discussion of various applications that can be handled with DQBF solving.

2017

nach oben zur Jahresübersicht

Ralf Wimmer, Andreas Karrenbauer, Ruben Becker, Christoph Scholl, Bernd Becker
From DQBF to QBF by Dependency Elimination
2017 International Conference on Theory and Applications of Satisfiability Testing (SAT), Nummer: 10491, Seiten: 326 - 343
Kurzfassungclearly superior to the previous method using variable elimination.
Tobias Seufert, Christoph Scholl
Sequential Verification Using Reverse PDR
2017 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”
KurzfassungIn 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 Wimmer
Verification of Incomplete Designs
In: State-of the-Art and Future Trends
2017, Springer International Publishing, Rolf Drechsler, Seiten: 37 - 72, Rolf Drechsler, ISBN: 978-3-319-57683-1
KurzfassungWe 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 Wirtz
Verification of Linear Hybrid Systems with Large Discrete State Spaces: Exploring the Design Space for Optimization
Sci Comput Program, Nummer: 148, Seiten: 123 - 160, 2017

2016

nach oben zur Jahresübersicht

Valeriy Balabanov, Jie-Hong Roland Jiang, Christoph Scholl, Alan Mishchenko, Robert K. Brayton
2QBF: Challenges and Solutions
2016 International Conference on Theory and Applications of Satisfiability Testing (SAT), Springer-Verlag, Nummer: 9710, Seiten: 453 - 469
Kurzfassung2QBF 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 Becker
Analysis of Incomplete Circuits using Dependency Quantified Boolean Formulas
2016 Int'l Workshop on Logic and Synthesis
KurzfassungIn 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 Scholl
Clauses Versus Gates in CEGAR-Based 2QBF Solving
2016 Workshop of the Thirtieth AAAI Conference on Artificial Intelligence Beyond NP
KurzfassungDespite 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 Becker
Dependency Schemes for DQBF
2016 International Conference on Theory and Applications of Satisfiability Testing (SAT), Nummer: 9710, Seiten: 473 - 489
Kurzfassungbeen 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 Becker
Skolem Functions for DQBF
2016 International Symposium on Automated Technology for Verification and Analysis (ATVA)
Kurzfassungto effectively compute Skolem functions with very little overhead compared to the mere solution of the formula.
Karina Wimmer, Ralf Wimmer, Christoph Scholl, Bernd Becker
Skolem Functions for DQBF, Extended Version
, 2016
Martin Böhnert, Christoph Scholl
Task Variants with Different Scratchpad Memory Consumption in Multi-Task Environments
2016 International Conference on Architecture of Computing Systems (ARCS), Nummer: 9637, Seiten: 143 - 156
KurzfassungFurthermore we show an extension of our approach to multicore environments.
Christoph Scholl, Florian Pigorsch
The QBF Solver AIGSolve
2016 International Workshop on Quantified Boolean Formulas
KurzfassungIntermediate 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 Wirtz
Verification of Linear Hybrid Systems with Large Discrete State Spaces: Exploring the Design Space for Optimization
SFB/TR 14 AVACS Technical Report, Nummer: 103, 2016

2015

nach oben zur Jahresübersicht

Georges Morbé, Christoph Scholl
Fully symbolic TCTL model checking for complete and incomplete real-time systems
2015 Science of Computer Programming
KurzfassungIn 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 Scholl
Improving Interpolants for Linear Arithmetic
2015 13th International Symposium on Automated Technology for Verification and Analysis (ATVA), Springer-Verlag, Nummer: 9364, Seiten: 48 - 63
Kurzfassungresults suggest a lower running time and a larger reduction compared to other methods from the literature.
Bernd Becker, Matthias Sauer, Christoph Scholl, Ralf Wimmer
Modeling 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
Kurzfassunghandling of unknown values using formal techniques in the areas of Test and Verification.
Ralf Wimmer, Karina Gitina, Jennifer Nist, Christoph Scholl, Bernd Becker
Preprocessing for DQBF
2015 10th International Conference on Theory and Applications of Satisfiability Testing (SAT), Springer-Verlag, Nummer: 9340, Seiten: 173 - 190
Kurzfassungtime 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 Becker
Preprocessing for DQBF
SFB/TR 14 AVACS Technical Report, Nummer: 110, 2015
Ralf Wimmer, Karina Gitina, Jennifer Nist, Christoph Scholl, Bernd Becker
Preprocessing for DQBF
SFB/TR 14 AVACS Technical Report, Nummer: 110, 2015
Valeriy Balabanov, Jie-Hong Roland Jiang Christoph Scholl
Skolem functions computation for CEGAR based QBF solvers
2015 International Workshop on Quantified Boolean Formulas
KurzfassungIn 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 Becker
Solving DQBF Through Quantifier Elimination
2015 Test in Europe Conference (DATE), Seiten: 1617 - 1622
Kurzfassungverification 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 Becker
Solving DQBF Through Quantifier Elimination
SFB/TR 14 AVACS Technical Report, Nummer: 107, 2015

2014

nach oben zur Jahresübersicht

Martin Böhnert, Christoph Scholl
A Dynamic Virtual Memory Management under Real-Time Constraints
2014 RTCSA, Chongqing, IEEE
KurzfassungOur 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 Becker
Combined Bounded and Symbolic Model Checking for Incomplete Timed Systems
2014 Haifa Haifa Verification Conference (HVC), Yahav, Eran, Band: 8855, Seiten: 30 - 47
KurzfassungWe 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 Scholl
Fully Symbolic TCTL Model Checking for Complete and Incomplete Real-Time Systems
2014 AVACS Technical Report, Nummer 104
Kurzfassungmay 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 Althaus
Simple Interpolants for Linear Arithmetic
2014 DATE, EDA Consortium San Jose, CA, USA / ACM DL

2013

nach oben zur Jahresübersicht

Karina Gitina, Sven Reimer, Matthias Sauer, Ralf Wimmer, Christoph Scholl, Bernd Becker
Equivalence Checking for Partial Implementations Revisited
2013 MBMV, Seiten: 61 - 70
Karina Gitina, Sven Reimer, Matthias Sauer, Ralf Wimmer, Christoph Scholl, Bernd Becker
Equivalence checking of partial designs using dependency quantified Boolean formulae
2013 IEEE 31st International Conference on Computer Design (ICCD) , Seiten: 396 - 403
Georges Morbé, Christoph Scholl
Fully Symbolic Model Checking for Incomplete Systems of Timed Automata
2013 Electronic Communications of the EASST, Proceedings of AVOCS 2013, Band: 66
Florian Pigorsch, Christoph Scholl
Lemma 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 Becker
Proving QBF-Hardness in Bounded Model Checking for Incomplete Designs
2013 MTV, IEEE Computer Society
Tobias Nopper, Christoph Scholl
Symbolic Model Checking for Incomplete Designs with Flexible Modeling of Unknowns
2013 IEEE Trans. Computers, Band: 62, Nummer: 6, Seiten: 1234 - 1254

2012

nach oben zur Jahresübersicht

Sven Reimer, Florian Pigorsch, Christoph Scholl, Bernd Becker
Enhanced 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 Wirtz
Exact 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 Scholl
Fully Symbolic Model Checking for Incomplete Systems of Timed Automata
2012 MBMV, Seiten: 97 - 108
Georges Morbé, Christoph Scholl
Guaranteeing Termination of Fully Symbolic Timed Forward Model Checking
2012 MTV, IEEE Computer Society, Seiten: 35 - 40

2011

nach oben zur Jahresübersicht

Georges Morbé, Florian Pigorsch, Christoph Scholl
Fully Symbolic Model Checking for Timed Automata
2011 CAV, Springer, Band: 6806, Seiten: 616 - 632
Georges Morbé, Christoph Scholl
Fully Symbolic Model Checking for Timed Automata
2011 MBMV, Seiten: 9 - 18
Werner Damm, Stefan Disch, Willem Hagemann, Christoph Scholl, Uwe Waldmann, Boris Wirtz
Integrating 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 Becker
Integration of orthogonal QBF solving techniques
2011 DATE, IEEE, Seiten: 149 - 154
Christian Miller, Christoph Scholl, Bernd Becker
Verifying Incomplete Networks of Timed Automata
2011 MBMV, Seiten: 113 - 122

2010

nach oben zur Jahresübersicht

Thorsten Zitterell, Christoph Scholl
A probabilistic and energy-efficient scheduling approach for online application in real-time systems
2010 DAC, ACM, Seiten: 42 - 47
Florian Pigorsch, Christoph Scholl
An AIG-Based QBF-solver using SAT for preprocessing
2010 DAC, ACM, Seiten: 170 - 175
Christian Miller, Karina Gitina, Christoph Scholl, Bernd Becker
Bounded Model Checking of Incomplete Networks of Timed Automata
2010 MTV, IEEE, Seiten: 61 - 66
Tobias Nopper, Christian Miller, Matthew Lewis, Bernd Becker, Christoph Scholl
SAT Modulo BDD – A Combined Verification Approach for Incomplete Designs
2010 MBMV, Fraunhofer Verlag, Seiten: 107 - 116

2009

nach oben zur Jahresübersicht

Christoph Scholl, Stefan Disch, Florian Pigorsch, Stefan Kupferschmid
Computing Optimized Representations for Non-convex Polyhedra by Detection and Removal of Redundant Linear Constraints
2009 TACAS, Springer, Band: 5505, Seiten: 383 - 397
Florian Pigorsch, Christoph Scholl
Exploiting structure in an AIG based QBF solver
2009 DATE, IEEE, Seiten: 1596 - 1601
Christian Miller, Tobias Nopper, Christoph Scholl
Symbolic CTL Model Checking for Incomplete Designs by Selecting Property-Specific Subsets of Local Component Assumptions
2009 MBMV, Seiten: 87 - 96
Florian Pigorsch, Christoph Scholl
Using Implications for Optimizing State Set Representations of Linear Hybrid Systems
2009 MBMV, Seiten: 77 - 86

2008

nach oben zur Jahresübersicht

Martin Böhnert, Thorsten Zitterell, Christoph Scholl
Dynamische Verwaltung Virtuellen Speichers für Echtzeitsysteme
2008 Echtzeit, Springer, Seiten: 101 - 110
Thorsten Zitterell, Christoph Scholl
Improving 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 Disch
Methoden 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 Reindl
Multisensor-Navigation für autonome Flugroboter
2008 Proceedings 14. GMA/ITG-Fachtagung Sensoren und Messsysteme, Seiten: 667 - 676
Bernd Becker, Marc Herbstritt, Natalia Kalinnik, Matthew Lewis, Juri Lichtner, Tobias Nopper, Ralf Wimmer
Propositional approximations for bounded model checking of partial circuit designs
2008 ICCD, IEEE, Seiten: 52 - 59
Christoph Scholl, Stefan Disch, Florian Pigorsch, Stefan Kupferschmid
Using an SMT Solver and Craig Interpolation to Detect and Remove Redundant Linear Constraints in Representations of Non-convex Polyhedra
2008 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

2007

nach oben zur Jahresübersicht

Stefan Disch, Christoph Scholl
Combinational Equivalence Checking Using Incremental SAT Solving, Output Ordering, and Resets
2007 ASP Design Automation Conf.
KurzfassungCombinational 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 Becker
Computation 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
Kurzfassungto 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.
Werner Damm, Stefan Disch, Hardi Hungar, Swen Jacobs, Jun Pang, Florian Pigorsch, Christoph Scholl, Uwe Waldmann, Boris Wirtz
Exact 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(SFB/TR 14 AVACS, http://www.avacs.org/).
Tobias Nopper, Christoph Scholl
Symbolic 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 Scholl
Towards an Experimental Autonomous Blimp Platform
2007 Proceedings of the 3rd European Conference on Mobile Robots, EMCR 2007
Tobias Nopper, Christoph Scholl
tion 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
KurzfassungCounterexample 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.

2006

nach oben zur Jahresübersicht

Marc Herbstritt, Bernd Becker, Christoph Scholl
Advanced 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 Disch
Advanced 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”
KurzfassungIn 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 Disch
Advanced 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
KurzfassungIn 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 Wirtz
Automatic 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
KurzfassungWe 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.

2005

nach oben zur Jahresübersicht

Tobias Nopper, Christoph Scholl
Flexible 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”
KurzfassungWe 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.
Jochen Eisinger, Peter Winterer, Bernd Becker
Securing Wireless Networks in a University Environment
2005 IEEE Int'l Conf. on Pervasive Computing and Communications Workshops, IEEE Computer Society, Seiten: 312 - 316
KurzfassungMany applications in e-learning utilize wireless networks (WLAN) as a carrier for data and communication. These networks in their basic form are unsecured, protecting the communication is a pre-condition for using a WLAN for confidential contents. Many existing solutions either do not provide the necessary security or fail when employed with large user bases. The IPSec based solution developed at the Faculty of Applied Science of the University of Freiburg provides a high level of security, and by using digital X.509 certificates the problem of administrating a large user base is solved as well.

2004

nach oben zur Jahresübersicht

Tobias Nopper, Christoph Scholl
Approximate Symbolic Model Checking for Incomplete Designs
2004 Austin, Texas Formal Methods in Computer-Aided Design, Springer Verlag, Band: 3312, Seiten: 290 - 305
KurzfassungWe 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 Scholl
Approximate Symbolic Model Checking of Incomplete Designs
2004 13th Int’l Workshop on Logic Synth., Band: 13, Seiten: 377 - 384
KurzfassungWe 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üche
Filter 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 Scholl
Symbolic Model Checking of Incomplete Designs
Technical Report Albert-Ludwigs-University, Nummer: 201, 2004

2002

nach oben zur Jahresübersicht

Christoph Scholl, Bernd Becker
Checking Equivalence for Circuits Containing Incompletely Specified Boxes
2002 Int’l Conf. on Comp. Design
KurzfassungWe consider the problem of checking whether an implementation which contains parts with incomplete information is equivalent to a given full specification. We study implementations which are not completely specified, but contain boxes which are associated with incompletely specified functions (called Incompletely Specified Boxes or IS–Boxes). After motivating the use of implementations with Incompletely Specified Boxes we define our notion of equivalence for this kind of implementations and present a method to solve the problem. A series of experimental results demonstrates the effectiveness and feasibility of the methods presented.
Christoph Scholl, Bernd Becker
Equivalence Checking in the Presence of Incompletely Specified Boxes
2002 ITG/GI/GMM-Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”
KurzfassungWe 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 Weis
On 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

2001

nach oben zur Jahresübersicht

Christoph Scholl, Bernd Becker
Checking 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 Becker
Checking Equivalence for Partial Implementations
2001 Design Automation Conf., Seiten: 238 - 243
Christoph Scholl, Marc Herbstritt, Bernd Becker
Don’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 Becker
Exploiting 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 Brogle
The Multiple Variable Order Problem for Binary Decision Diagrams
2001 ASP Design Automation Conf.
KurzfassungReduced Ordered Binary Decision Diagrams (ROBDDs) gained widespread use in logic design verification, test generation, fault simulation, and logic synthesis [MWBS:88,Bry:92]. Since the size of an ROBDD heavily depends on the variable order used, there is a strong need to find variable orders that minimize the number of nodes in an ROBDD. In certain applications we have to cope with ROBDDs with different variable orders, whereas further manipulations of these ROBDDs require common variable orders. In this paper we give a theoretical background for this “Multiple Variable Order problem”. Moreover, we solve the problem to transform ROBDDs with different variable orders into a good common variable order using dynamic variable ordering techniques.

2000

nach oben zur Jahresübersicht

Christoph Scholl, Bernd Becker
Checking Equivalence for Partial Implementations
Technical Report Albert-Ludwigs-University, Nummer: 145, 2000
Andreas Hett, Christoph Scholl, Bernd Becker
Distance Driven Finite State Machine Traversal
2000 Design Automation Conf., Seiten: 39 - 42
KurzfassungSymbolic 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 Becker
Exploiting Don’t Cares to Minimize *BMDs
Technical Report Albert-Ludwigs-University, Nummer: 141, 2000
Christoph Scholl, Bernd Becker
On the Generation of Multiplexer Circuits for Pass Transistor Logic
2000 Design, Automation and Test in Europe, Seiten: 372 - 378
Andreas Hett, Christoph Scholl, Bernd Becker
State 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

1999

nach oben zur Jahresübersicht

Christoph Scholl, Dirk Möller, Paul Molitor, Rolf Drechsler
BDD 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 Becker
On the Generation of Multiplexer Circuits for Pass Transistor Logic
1999 Int’l Workshop on Logic Synth.
KurzfassungPass 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 Brogle
Solving the Multiple Variable Order Problem for Binary Decision Diagram by Use of Dynamic Reordering Techniques
1999 Int’l Workshop on Logic Synth.
KurzfassungReduced 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 Brogle
Solving the Multiple Variable Order Problem for Binary Decision Diagram by Use of Dynamic Reordering Techniques
Technical Report Albert-Ludwigs-University, Nummer: 130, 1999

1998

nach oben zur Jahresübersicht

Christoph Scholl
Multi-output Functional Decomposition with Exploitation of Don’t Cares
1998 Design, Automation and Test in Europe, Seiten: 743 - 748
KurzfassungFunctional 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 Weis
Word-Level Decision Diagrams, WLCDs and Division
1998 Int’l Conf. on CAD, Seiten: 672 - 677
KurzfassungSeveral types of Decision Diagrams (DDs) have been proposed for the verification of Integrated Circuits. Recently, word-level DDs like BMDs, *BMDs, HDDs, K*BMDs and *PHDDs have been attracting more and more interest, e.g., by using *BMDs and *PHDDs it was for the first time possible to formally verify integer multipliers and floating point multipliers of “significant” bitlengths, respectively. On the other hand, it has been unknown, whether division, the operation inverse to multiplication, can be efficiently represented by some type of word-level DDs. In this paper we show that the representational power of any word-level DD is too weak to efficiently represent integer division. Thus, neither a clever choice of the variable ordering, the decomposition type or the edge weights, can lead to a polynomial DD size for division. For the proof we introduce Word-Level Linear Combination Diagrams (WLCDs), a DD, which may be viewed as a “generic” word-level DD. We derive an exponential lower bound on the WLCD representation size for integer dividers and show how this bound transfers to all other word-level DDs.

1997

nach oben zur Jahresübersicht

Christoph Scholl, Dirk Möller, Paul Molitor, Rolf Drechsler
BDD Minimization Using Symmetries
Technical Report, Institute for Computer Science, University Halle, Band: 97-32, 1997
Christoph Scholl
Functional Decomposition with Integrated Test Generation
1997 GI/ITG Workshop “Testmethoden und Zuverlässigkeit von Schaltungen und Systemen”
KurzfassungFunctional decomposition is an important technique in logic synthesis, especially for the design of lookup table based FPGA architectures. We present an approach how to compute test information, e.g. a complete test set (according to the stuck-at-fault model or the cellular fault model), for functionally decomposed circuits. We are able to compute this test information in parallel with logic synthesis by (recursive) functional decomposition.
Christoph Scholl, Rolf Drechsler, Bernd Becker
Functional Simulation Using Binary Decision Diagrams
1997 Int’l. Conf. on Computer Aided Design, Seiten: 8 - 12
Christoph Scholl, Rolf Drechsler, Bernd Becker
Functional Simulation using Binary Decision Diagrams
1997 GI/ITG/GME Workshop “Methoden des Entwurfs und der Verifikation digitaler Systeme”
KurzfassungIn many verification techniques fast functional evaluation of a Boolean network is needed. We investigate the idea of using Binary Decision Diagrams (BDDs) for functional simulation. The area-time trade-off that results from different minimization techniques of the BDD is discussed. We propose new minimization methods based on dynamic reordering that allow smaller representations with (nearly) no runtime penalty.
Christoph Scholl, Rolf Drechsler, Bernd Becker
Functional Simulation using Binary Decision Diagrams
1997 Int’l Workshop on Logic Synth.
KurzfassungIn 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 Molitor
Minimizing ROBDD Sizes of Incompletely Specified Boolean Functions by Exploiting Strong Symmetries
1997 Test Conf., Seiten: 229 - 234
KurzfassungWe 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 Scholl
Multi-output Functional Decomposition with Exploitation of Don’t Cares
1997 Int’l Workshop on Logic Synth.
KurzfassungFunctional 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.

1995

nach oben zur Jahresübersicht

Christoph Scholl, Paul Molitor
Communication Based FPGA Synthesis for Multi-Output Boolean Functions
1995 ASP Design Automation Conf., Seiten: 279 - 287
KurzfassungOne 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 Molitor
Efficient ROBDD based computation of common decomposition functions of multioutput boolean functions
In: Novel Approaches in Logic and Architecture Synthesis
1995, \,Hall, Seiten: 57 - 63,
KurzfassungOne 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.

1994

nach oben zur Jahresübersicht

Paul Molitor, Christoph Scholl
Communication Based Multilevel Synthesis for Multi-Output Boolean Functions
1994 Great Lakes Symp. VLSI, Seiten: 101 - 104
KurzfassungA 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 Scholl
Communication Based Multilevel Synthesis for Multi-Output Boolean Functions
Informatik-Berichte Humbold-University, Nummer: 29, 1994
Christoph Scholl, Paul Molitor
Efficient ROBDD Based Computation of Common Decomposition Functions of Multi-Output Boolean Functions
1994 IFIP Workshop on Logic and Architecture Synthesis, Grenoble, Seiten: 61 - 70
KurzfassungOne 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.

1993

nach oben zur Jahresübersicht

Christoph Scholl, Paul Molitor
Mehrstufige Logiksynthese unter Ausnutzung von Symmetrien und nichttrivialen Zerlegungen
Sonderforschungsbereich 124, TP B6, Nummer: 02/93, 1993