Bernd Becker
Liste filtern : Jahre: 2021 |
2020 |
2019 |
2018 |
2017 |
2016 |
2015 |
2014 |
2013 |
2012 |
2011 |
2010 |
2009 |
2008 |
2007 |
2006 |
2005 |
2004 |
2003 |
2002 |
2001 |
2000 |
1999 |
1998 |
1997 |
1996 |
1995 |
1994 |
1993 |
1992 |
1991 |
1988 |
1987 |
1986 |
1983 | alle anzeigen nach oben zur Jahresübersicht Karsten Scheibler, Felix Winterer, Tobias Seufert, Tino Teige, Christoph Scholl, Bernd BeckerICP and IC3 2021 Conference on Design, Automation and Test in Europe Conference (DATE) » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung If embedded systems are used in safety-critical environments, they need to meet several standards. For example, in the automotive domain the ISO 26262 standard requires that the software running on such systems does not contain unreachable code. Software model checking is one effective approach to automatically detect such dead code. Being used in a commercial product, iSAT3 already performs very well in this context. In this paper we integrate IC3 into iSAT3 in order to improve its dead code detection capabilities even further. nach oben zur Jahresübersicht Benjamin Völker, Marc Pfeifer, Philipp M Scholl, Bernd BeckerAnnoticity: A Smart Annotation Tool and Data Browser for Electricity Datasets 2020 5th International Workshop on Non-Intrusive Load Monitoring ACM» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung The growing request for eco-feedback and smart living concepts accelerated the development of Non-Intrusive Load Monitoring (NILM) algorithms during the last decade. Comparing and evaluating these algorithms still remains challenging due to the absence of a common benchmark datasets, and missing best practises for their application. Despite the fact that multiple datasets were recorded for the purpose of comparing NILM algorithms, many researchers still have to record their own dataset in order to meet the requirements of their specific application. Adding ground truth labels to these datasets is a cumbersome and time consuming process as it requires an expert to visually inspect all the data manually. Therefore, we propose the Annoticity inspection and labeling tool which simplifies the process of visualizing and labeling of electricity data. We use an event detector based on the log likelihood ratio test which achieved an F1 score of 90.07% in our experiments. Preliminary results indicate that the effort of generating event labels is reduced by 80.35% using our tool. Benjamin Völker, Marc Pfeifer, Philipp M Scholl, Bernd BeckerFIRED: A Fully-labeled hIgh-fRequency Electricity Disaggregation Dataset 2020 The 7th ACM International Conference on Systems for Energy-Efficient Buildings, Cities, and Transportation Virtual Event Japan November, 2020 ACM» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung As more and more homes are equipped with smart electricity meters, home owners gain the ability to monitor their total electricity consumption on a daily or hourly basis. Techniques such as load forecasting, load disaggregation, and activity recognition try to provide even better insights into our electricity consumption, highlight saving potential or improve our daily living. To develop and evaluate these techniques, publicly available datasets are used. We identified a lack of high frequency fully labeled electricity datasets in the residential domain and present the FIRED dataset. It contains 52 of 8kHz aggregated current and voltage readings of the 3-phase supply of a typical residential apartment in Germany. The dataset also contains synchronized ground truth data as 2kHz readings of 21 individual appliances, as well as room temperature readings and fully labeled state changes of the lighting system, resulting in a complete and versatile residential electricity dataset. Pascal Raiola, Tobias Paxian, Bernd BeckerMinimal Witnesses for Security Weaknesses in Reconﬁgurable Scan Networks 2020 IEEE European Test Symposium Leonore Winterer, Sebastian Junges, Ralf Wimmer, Nils Jansen, Ufuk Topcu, Joost-Pieter Katoen, Bernd BeckerStrategy Synthesis for POMDPs in Robot Planning using Game-Based Abstractions 2020 IEEE T Automat Contr » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We study synthesis problems with constraints in partially observable Markov decision processes (POMDPs), where the objective is to compute a strategy for an agent that is guaranteed to satisfy certain safety and performance specifications. Verification and strategy synthesis for POMDPs are, however, computationally intractable in general. We alleviate this difficulty by focusing on planning applications and exploiting typical structural properties of such scenarios; for instance, we assume that the agent has the ability to observe its own position inside an environment. We propose an abstraction refinement framework which turns such a POMDP model into a (fully observable) probabilistic two-player game (PG). For the obtained PGs, efficient verification and synthesis tools allow to determine strategies with optimal safety and performance measures, which approximate optimal schedulers on the POMDP. If the approximation is too coarse to satisfy the given specifications, an refinement scheme improves the computed strategies. As a running example, we use planning problems where an agent moves inside an environment with randomly moving obstacles and restricted observability. We demonstrate that the proposed method advances the state of the art by solving problems several orders-of-magnitude larger than those that can be handled by existing POMDP solvers. Furthermore, this method gives guarantees on safety constraints, which is not supported by the majority of the existing solvers. Leonore Winterer, Ralf Wimmer, Nils Jansen, Bernd BeckerStrengthening Determinstic Policies for POMPDs 2020 Proceedings of the 12th NASA Formal Methods Symposium (NFM) » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung The synthesis problem for partially observable Markov decision processes (POMDPs) is to compute a policy that satisfies a given specification. Such policies have to take the full execution history of a POMDP into account, rendering the problem undecidable in general. A common approach is to use a limited amount of memory and randomize over potential choices. Yet, this problem is still NP-hard and often computationally intractable in practice. A restricted problem is to use neither history nor randomization, yielding policies that are called stationary and deterministic. Previous approaches to compute such policies employ mixed-integer linear programming (MILP). We provide a novel MILP encoding that supports sophisticated specifications in the form of temporal logic constraints. It is able to handle an arbitrary number of such specifications. Yet, randomization and memory are often mandatory to achieve satisfactory policies. First, we extend our encoding to deliver a restricted class of randomized policies. Second, based on the results of the original MILP, we employ a preprocessing of the POMDP to encompass memory-based decisions. The advantages of our approach over state-of-the-art POMDP solvers lie (1) in the flexibility to strengthen simple deterministic policies without losing computational tractability and (2) in the ability to enforce the provable satisfaction of arbitrarily many specifications. The latter point allows to take trade-offs between performance and safety aspects of typical POMDP examples into account. We show the effectiveness of our method on a broad range of benchmarks. nach oben zur Jahresübersicht Benjamin Völker, Marc Pfeifer, Philipp M Scholl, Bernd BeckerA Versatile High Frequency Electricity Monitoring Framework for Our Future Connected Home 2019 EAI International Conference on Sustainable Energy for Smart Cities, Braga Portugal Springer, Seiten : 221 - 231» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In our homes a lot of devices are powered by electricity with- out us knowing the specific amount. As electricity production has a large, negative environmental impact, we should be more aware about how de- vices consume power and how we can adapt our daily routine to decrease our electricity requirements. Methods such as Non-Intrusive Load Mon- itoring (NILM) can provide the user with precise device level electricity data by measuring at a single point in a houses’ electricity network. However, the time resolution of most off-the-shelf power meters is not sufficient for NILM or the meters are locked down for security reasons. Therefore, we have developed our own versatile energy metering frame- work which consists of a high frequency electricity metering device, a versatile backend for data processing and a webapp for data visualiza- tion. The developed hardware is capable of sampling up to 32 kHz, while the software framework allows to extract other power related metrics such as harmonic content. The system’s application ranges from pro- viding transparent electricity usage to the user up to generating load forecasts with fine granularity. Benjamin Völker, Philipp M Scholl, Bernd BeckerSemi-Automatic Generation and Labeling of Training Data for Non-intrusive Load Monitoring 2019 e-Energy '19 Proceedings of the Tenth ACM International Conference on Future Energy Systems ACM New York, NY, USA ©2019, Band : 10, Seiten : 17 - 23» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung User awareness is one of the main drivers to reduce unnecessary energy consumption in our homes. This awareness, however, requires individual energy data of the devices we own. A retrofittable way to get this data is to use Non-Intrusive Load Monitoring methods. Most of these methods are supervised and require to collect labeled ground truth data in advance. Labeling on-phases of devices is already a tedious process, but if further information about internal device states are required (e.g. intensity of an HVAC), manual labeling methods are infeasible. We propose a novel data collection and labeling method for Non-Intrusive Load Monitoring. This method uses intrusive sensors directly connected to the monitored devices. A post-processing step classifies the connected devices into four categories and exposes internal state sequences in a semi-automatic way. We evaluated our labeling method with a sample dataset comparing the amount of recognized events, states and classified device category. The event detector achieved a total F1 score of 86.52 % for devices which show distinct states in its power signal. Using our framework, the overall labeling effort is cut by more than half (42%). Leonie Feldbusch, Felix Winterer, Johannes Gramsch, Linus Feiten, Bernd BeckerSMILE goes Gaming:
Gamification in a Classroom Response System for Academic Teaching
2019 11th International Conference on Computer Supported Education (CSEDU) » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung The classroom response system SMILE (SMartphones In LEctures) is regularly used in academic lectures.
Among others, it enables lecturers to start quizzes that can be answered anonymously by students on their
smartphones. This aims at both activating the students and giving them feedback about their understanding of
the current content of the lecture. But even though many students use SMILE in the beginning of a course, the
number of active participants tends to decrease as the term progresses. This paper reports the results of a study
looking at incorporating gamification into SMILE to increase the students’ motivation and involvement. Game
elements such as scores, badges and a leaderboard have been integrated paired with a post-processing feature
enabling students to repeat SMILE quizzes outside of the lectures. The evaluations show that the gamification
approach increased the participation in SMILE quizzes significantly. Marc Pfeifer, Philipp M. Scholl, Rainer Voigt, Bernd BeckerActive Stereo Vision with High Resolution on an FPGA 2019 27th IEEE Annual International Symposium on Field-Programmable Custom Computing Machines Proceedings of the 27th IEEE Annual International Symposium on Field-Programmable Custom Computing Machines , Seiten : 118 - 126» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We present a novel FPGA based active stereo vision system, tailored for the use in a mobile 3D stereo camera. For the generation of a single 3D map the matching algorithm is based on a correlation approach, where multiple stereo image pairs instead of a single one are processed to guarantee an improved depth resolution. To efficiently handle the large amounts of incoming image data we adapt the algorithm to the underlying FPGA structures, e.g. by making use of pipelining and parallelization. Experiments demonstrate that our approach provides high-quality 3D maps at least three times more energy-efficient (5.5 fps/W) than comparable approaches executed on CPU and GPU platforms. Implemented on a Xilinx Zynq-7030 SoC our system provides a computation speed of 12.2 fps, at a resolution of 1.3 megapixel and a 128 pixel disparity search space. As such it outperforms the currently best passive stereo systems of the Middlebury Stereo Evaluation in terms of speed and accuracy. The presented approach is therefore well suited for mobile applications, that require a highly accurate and energy-efficient active stereo vision system. Phillip M Scholl, Benjamin Völker, Bernd Becker, Kristof Van LaerhovenA multi-media exchange format for time-series dataset curation In : Human Activity Sensing: Corpus and Applications 2019, Springer International Publishing , Seiten : 111 - 119, ISBN : 9783030130015» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Exchanging data as character-separated values (CSV) is slow, cumbersome and error-prone. Especially for time-series data, which is common in Activity Recognition, synchronizing several independently recorded sensors is challenging. Adding second level evidence, like video recordings from multiple angles and time-coded annotations, further complicates the matter of curating such data. A possible alternative is to make use of standardized multi-media formats. Sensor data can be encoded in audio format, and time-coded information, like annotations, as subtitles. Video data can be added easily. All this media can be merged into a single container file, which makes the issue of synchronization explicit. The incurred performance overhead by this encoding is shown to be negligible and compression can be applied to optimize storage and transmission overhead. Uwe Wagschal, Thomas Waldvogel, Thomas Metz, Samuel Weishaupt, Linus Feiten, Bernd Becker, Kamal SinghAlle gegen Alle? Die Mehrpersonendebatte der kleinen Parteien in der Analyse In : Die Bundestagswahl 2017: Analysen der Wahl-, Parteien-, Kommunikations- und Regierungsforschung 2019, Springer Fachmedien Wiesbaden , Seiten : 461 - 482, ISBN : 978-3-658-25050-8» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Der Beitrag analysiert eine TV-Debatte zur Bundestagswahl 2017 mit einem Mehrpersonenpodium unter Beteiligung der "kleinen" Parteien. Auf Basis von Echtzeit- und Umfragedaten formuliert der Beitrag nach eingehender Analyse fünf zentrale Befunde: 1) Je weiter politisch die Debattenteilnehmer auseinanderliegen, desto polarisierter und konfliktiver ist die Debatte. 2) Anhänger, die sich politisch einem Lager zurechnen bewerten auch den bzw. die Repräsentanten dieses Lagers deutlich besser. 3) Debattenteilnehmer anderer politischer Lager werden systematisch schlechter bewertet. 4) Ein besonderer Bias durch die Moderation liegt für die untersuchte Debatte nicht vor. 5) Die direkte Bedeutung von TV-Debatten für die Wahlentscheidung ist begrenzt. Steven Carr, Nils Jansen, Ralf Wimmer, Alexandru Constantin Serban, Bernd Becker, Ufuk TopcuCounterexample-Guided Strategy Improvement for POMDPs using Recurrent Neural Networks 2019 Macao, China Proceedings of the 28th International Joint Conference on Artificial Intelligence (IJCAI) » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We study strategy synthesis for POMDPs. The particular problem is to determine strategies that provably adhere to (probabilistic) temporal logic constraints. This problem is computationally intractable and theoretically hard. We propose a novel method that combines techniques from machine learning and formal verification. First, we train an RNN to encode POMDP strategies. The RNN accounts for memory-based decisions without the need to expand the full belief space of a POMDP. Secondly, we restrict the RNN-based strategy to represent a finite-memory strategy and implement it on a specific POMDP. For the resulting finite Markov chain, efficient formal verification techniques provide provable guarantees against temporal logic specifications. If the specification is not satisfied, counterexamples supply diagnostic information. We use this information to improve the strategy by iteratively training the RNN. Numerical experiments show that the proposed method elevates the state of the art in POMDP solving by up to three orders of magnitude in terms of solving times and model sizes. Benjamin Thiemann, Linus Feiten, Pascal Raiola, Bernd Becker, Matthias SauerOn Integrating Lightweight Encryption in Reconfigurable Scan Networks 2019 IEEE European Test Symposium » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Reconfigurable Scan Networks (RSNs) are a powerful tool for testing and maintenance of embedded systems, since they allow for flexible access to on-chip instrumentation such as built-in self-test and debug modules. The deployment of RSNs, however, can be exploited by malicious users as a side-channel in order to gain information about sensitive data or intellectual property and to recover secret keys. Hence, implementing appropriate countermeasures to secure the access to and data integrity of embedded instrumentation is of high importance.
In this paper we present a novel hardware and software combined approach to ensure data privacy in IEEE Std 1687 (IJTAG) RSNs. To do so, both a secure IJTAG compliant plug-and-play instrument wrapper and a versatile software toolchain are introduced. The wrapper demonstrates the necessary architectural adaptations required when using a lightweight stream cipher, whereas the software toolchain provides a seamless integration of the testing workflow with stream cipher.
The applicability of the method is demonstrated by an FPGA-based implementation. We report on the performance of the developed instrument wrapper, which is empirically shown to have only a small impact on the workflow in terms of hardware overhead, operational costs and test time overhead. Pascal Raiola, Benjamin Thiemann, Jan Burchard, Ahmed Atteya, Natalia Kapstova, Hans-Joachim Wunderlich, Bernd Becker, Matthias SauerOn Secure Data Flow in Reconfigurable Scan Networks 2019 Conf. on Design, Automation and Test in Europe Ralf Wimmer, Christoph Scholl, Bernd BeckerThe (D)QBF Preprocessor HQSpre – Underlying Theory and Its Implementation 2019 Journal on Satisfiability, Boolean Modeling and Computation , Band : 11, Nummer : 1, Seiten : 3 - 52» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Preprocessing turned out to be an essential step for SAT, QBF, and DQBF solvers to reduce/modify the number of variables and clauses of the formula, before the formula is passed to the actual solving algorithm. These preprocessing techniques often reduce the computation time of the solver by orders of magnitude. In this paper, we present the preprocessor HQSpre that was developed for Dependency Quantified Boolean Formulas (DQBFs) and that generalizes different preprocessing techniques for SAT and QBF problems to DQBF. We give a presentation of the underlying theory together with detailed proofs as well as implementation details contributing to the efficiency of the preprocessor. HQSpre has been used with obvious success by the winners of the DQBF track, and, even more interestingly, the QBF tracks of QBFEVAL’18. nach oben zur Jahresübersicht Pascal Raiola, Michael A. Kochte, Ahmed Atteya, Laura Rodríguez Gómez, Hans-Joachim Wunderlich, Bernd Becker, Matthias SauerDetecting and Resolving Security Violations in Reconfigurable Scan Networks 2018 IEEE International Symposium on On-Line Testing and Robust System Design Benjamin Völker, Philipp M Scholl, Bernd BeckerTowards the Fusion of Intrusive and Non-intrusive Load
Monitoring - A Hybrid Approach 2018 e-Energy '18 Proceedings of the Ninth International Conference on Future Energy Systems/Karlsruhe, Germany , Seiten : 436 - 438 » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung With Electricity as a fundamental part of our life, its production has
still large, negative environmental impact. Therefore, one strain of
research is to optimize electricity usage by avoiding its unnecessary
consumption or time its consumption when green energy is available. The shift towards an Advanced Metering Infrastructure (AMI)
allows to optimize energy distribution based on the current load
at residence level. However, applications such as Demand Management and Advanced Load Forecasting require information further
down at device level, which cannot be provided by standard electricity meters nor existing AMIs. Hence, different approaches for
appliance monitoring emerged over the past 30 years which are
categorized into Intrusive systems requiring multiple distributed
sensors and Non-Intrusive systems requiring a single unobtrusive
sensor. Although each category has been individually explored,
hybrid approaches have received little attention. Our experiments
highlight that variable consumer devices (e.g. PCs) are detrimental
to the detection performance of non-intrusive systems. We further
show that their influence can be inhibited by using sensor data from
additional intrusive sensors. Even fairly straightforward sensor fusion techniques lead to a classification performance (F1) gain from
84.88 % to 93.41 % in our test setup. As this highlights the potential
to contribute to the global goal of saving energy, we define further
research directions for hybrid load monitoring systems Ahmed Atteya, Michael Kochte, Matthias Sauer, Pascal Raiola, Bernd Becker, Hans-Joachim WunderlichOnline Prevention of Security Violations in Reconfigurable Scan Networks 2018 IEEE European Test Symposium Johanna Sepulveda, Damian Aboul-Hassan, Georg Sigl, Bernd Becker, Matthias SauerTowards the Formal Verification of Security Properties of a Network-on-Chip Router 2018 IEEE European Test Symposium Felix Neubauer, Jan Burchard, Pascal Raiola, Jochen Rivoir, Bernd Becker, Matthias SauerEfficient Generation of Parametric Test Conditions for AMS Chips with an Interval Constraint Solver 2018 IEEE VLSI Test Symposium (VTS'18) » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung The characterization of analog-mixed signal (AMS) silicon requires a suitable pattern set able to exercise the parametric operational space to - among other tasks -
validate the correct (specified) working behaviour of the device under test. As experience shows, most of the unexpected problems occur for very specific value combinations of a few test condition variables that were not expected to have an influence. Additionally, restrictions on the operational conditions have to be taken into account.
We present a method to efficiently create a set of test conditions to cover such a constrained search space with a user-defined density. First, an initial test condition set is generated using quasirandom Sobol sequences. Secondly, we analyse the test conditions to identify and fill uncovered areas in the parameter space using the in-house interval constraint solver iSAT3.
The applicability of the method is demonstrated by experimental results on a 19-dimensional search space using a realistic set of constraints. Linus Feiten, Karsten Scheibler, Bernd Becker, Matthias SauerUsing different LUT paths to increase area efficiency of RO-PUFs on Altera FPGAs 2018 TRUDEVICE Workshop, Dresden » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Delay-based PUFs are well suited to be implemented on FPGA chips. A delay line is commonly achieved by
routing the signal through a number of adjacent lookup tables (LUTs). This however uses only one of all possible routings per LUT. We suggest to implement RO-PUFs using all possible routings that can be configured at runtime, which allows to gather much more device-specific information per chip area.
Furthermore, the number of PUF response bits can be increased even further without extra hardware or software if a certain degree of correlations among the response bits is accepted. The degree of correlations is proportional to the growth of response bits, so a design decision can be made. To make this decision, a metric to quantify the degree of correlations is needed, which has so far been mostly neglected in the analyses of PUF implementations. Felix Neubauer, Jan Burchard, Pascal Raiola, Jochen Rivoir, Bernd Becker, Matthias SauerHigh-Coverage AMS Test Space Optimization by Efficient Parametric Test Condition Generation 2018 GI/ITG Workshop “Testmethoden und Zuverlässigkeit von Schaltungen und Systemen” Uwe Wagschal, Thomas Metz, Thomas Waldvogel, Bernd Becker, Linus Feiten, Samuel WeishauptOnline real-time-response measurement in real life settings: the Debat-O-Meter 2018 Cologne 20th General Online Research Conference (GOR) » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Political debates have attracted substantial public and academic attention due to their prominent role in election campaigns. Reaching a tremendous number of potential voters, TV debates concentrate the electoral contest into a one-evening format that covers all major topics and main contenders. As "miniature campaigns" they reach many undecided and serve as (often the only) source of direct campaign information for voters less sophisticated or attentive to politics. In recent years Real Time Response Measurement gained international importance in political communication research. Ralf Wimmer, Karina Wimmer, Christoph Scholl, Bernd BeckerAnalysis of Incomplete Circuits using Dependency Quantified Boolean Formulas In : Advanced Logic Synthesis 2018, Springer , André Ignacio Reis and Rolf Drechsler, Seiten : 151 - 168, André Ignacio Reis and Rolf Drechsler, ISBN : 978-3-319-67294-6 Pascal Raiola, Michael A. Kochte, Ahmed Atteya, Laura Rodríguez Gómez, Hans-Joachim Wunderlich, Bernd Becker, Matthias SauerDesign of Reconfigurable Scan Networks for Secure Data Transmission 2018 GI/ITG Workshop “Testmethoden und Zuverlässigkeit von Schaltungen und Systemen” Tobias Paxian, Sven Reimer, Bernd BeckerDynamic Polynomial Watchdog Encoding for Solving Weighted MaxSAT 2018 International Conference on Theory and Applications of Satisfiability Testing , Springer, Band : 10929, Seiten : 37 - 53» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In this paper we present a novel pseudo-Boolean (PB) constraint encoding for solving the weighted MaxSAT problem with iterative SAT-based methods based on the Polynomial Watchdog (PW) CNF encoding. The watchdog of the PW encoding indicates whether the bound of the PB constraint holds. In our approach, we lift this static watchdog concept to a dynamic one allowing an incremental convergence to the optimal result. Consequently, we formulate and implement a SAT-based algorithm for our new Dynamic Polynomial Watchdog (DPW) encoding which can be applied for solving the MaxSAT problem. Furthermore, we introduce three fundamental optimizations of the PW encoding also suited for the original version leading to significantly less encoding size.
Our experimental results show that our encoding and algorithm is competitive with state-of-the-art encodings as utilized in QMaxSAT (2nd place in last MaxSAT Evaluation 2017). Our encoding dominates two of the QMaxSAT encodings, and at the same time is able to solve unique instances. We integrated our new encoding into QMaxSAT and adapt the heuristic to choose between the only remaining encoding of QMaxSAT and our approach. This combined version solves 19 (4%) more instances in overall 30\% less run time on the benchmark set of the MaxSAT Evaluation 2017. Compared to each encoding of QMaxSAT used in the evaluation, our encoding leads to an algorithm that is on average at least 2X faster. Sebastian Junges, Nils Jansen, Ralf Wimmer, Tim Quatmann, Leonore Winterer, Joost-Pieter Katoen, Bernd BeckerFinite-State Controllers of POMDPs via Parameter Synthesis 2018 Proceedings of the 34th Conference on Uncertainty in Artificial Intelligence (UAI) , AUAI Press, Seiten : 519 - 529» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung e study finite-state controllers (FSCs) for partially observable Markov decision processes (POMDPs) that are provably correct with respect to given specifications. The key insight is that computing (randomised) FSCs on POMDPs is equivalent to (and computationally as hard as) synthesis for parametric Markov chains (pMCs). This correspondence enables using black-box techniques to compute correct-by-construction FSCs for POMDPs for a wide range of properties. Our experimental evaluation on typical POMDP problems shows that we are competitive to state-of-the-art POMDP solvers. nach oben zur Jahresübersicht Jan Horáček, Jan Burchard, Bernd Becker, Martin KreuzerIntegrating Algebraic and SAT Solvers 2017 International Conference on Mathematical Aspects of Computer and Information Sciences (MACIS) 2017 Jan Horáček, Maël Gay, Bernd Becker, Martin KreuzerIntegrating Algebraic and SAT Solvers 2017 International Conference on Mathematical Aspects of Computer and Information Sciences (MACIS) 2017 Jan Burchard, Maël Gay, Ange-Salomé Messeng Ekossono, Jan Horáček, Bernd Becker, Tobias Schubert, Martin Kreuzer, Ilia PolianAutoFault: Towards Automatic Construction of Algebraic Fault
Attacks 2017 Fault Diagnosis and Tolerance in Cryptography (FDTC) 2017 » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung A prototype of the framework AutoFault, which automatically constructs fault-injection attacks for hardware realizations of ciphers, is presented. AutoFault can be used to quickly evaluate the resistance of security-critical hardware blocks to fault attacks and the adequacy of implemented countermeasures. The framework takes as inputs solely the circuit description of the cipher and the fault(s) and produces an algebraic formula that can be handed over to an external solver. In contrast to previous work, attacks constructed by AutoFault do not incorporate any cipher-specific cryptoanalytic derivations, making the framework accessible to users without cryptographic background. We report successful application of AutoFault in combination with a state-of-the-art SAT solver to LED-64 and to small-scale AES. To the best of our knowledge, this is the first time that a state-of-the-art cipher (LED-64) was broken by a fault attack with no prior manual cryptanalysis whatsoever. Michael A. Kochte, Matthias Sauer, Laura Rodríguez Gómez, Pascal Raiola, Bernd Becker, Hans-Joachim WunderlichSpecification and verification of security in reconfigurable scan networks 2017 IEEE European Test Symposium Jan Burchard, Dominik Erb, Sudhakar M. Reddy, Adit D. Singh, Bernd BeckerEfficient SAT-Based Generation of Hazard-Activated
TSO Tests 2017 IEEE VLSI Test Symposium (VTS'17) Uwe Wagschal, Bernd Becker, Thomas Metz, Thomas Waldvogel, Linus FeitenReal-time evaluation of political debates at home and abroad with the Debat-O-Meter 2017 Berlin 19th General Online Research Conference (GOR) » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Due to their role in election campaigns, televised debates between political candidates (“TV-Duelle”) have attracted substantial scholarly attention. A large body of work has used physical feedback devices to measure viewers’ reactions to a debate in real-time. However, this approach is limited to lab-based settings with potential negative ramifications for e.g. external validity. Therefore, a method freeing researchers from the need to use physical devices is called for. Jan Burchard, Felix Neubauer, Pascal Raiola, Dominik Erb, Bernd BeckerEvaluating the Effectiveness of D-Chains in SAT based ATPG 2017 IEEE Latin American Test Symposium (LATS'17) Matthias Sauer, Pascal Raiola, Linus Feiten, Bernd Becker, Ulrich Rührmair, Ilia PolianSensitized Path PUF: A Lightweight Embedded Physical Unclonable Function 2017 Conf. on Design, Automation and Test in Europe Felix Neubauer, Karsten Scheibler, Bernd Becker, Ahmed Mahdi, Martin Fränzle, Tino Teige, Tom Bienmüller, Detlef FehrerAccurate Dead Code Detection in Embedded C
Code by Arithmetic Constraint Solving 2017 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Unreachable code fragments in software, despite not having a negative impact on the functional behavior, can have a bad effect in other areas, such as code optimization or coverage-based code validation and certification. Especially the latter is important in industrial, safety critical environments, where detecting such dead code is a major goal to adjust the coverage of software tests.
In the context of embedded systems we focus on C programs which are reactive, control-oriented, and floating-point dominated. Such programs are either automatically generated
from Simulink-plus-Stateflow models or hand-written according to coding guidelines. While there are various techniques – e.g. abstract interpretation or Counterexample guided abstraction refinement (CEGAR) – to deal with individual issues of this domain, there is none which can cover all of them. The AVACS transfer project T1 aims at the combination of these techniques in order to provide an accurate and efficient dead code detection.
In this paper we present the ideas and goals of the project as well as the current status (including very promising experimental results) and future challenges. Pascal Raiola, Dominik Erb, Sudhakar Reddy, Bernd BeckerAccurate Diagnosis of Interconnect Open Defects based on the Robust Enhanced Aggressor Victim Model 2017 30th International Conference on VLSI Design » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Interconnect opens are known to be one of the predominant defects in nanoscale technologies. Automatic test pattern generation for open faults is challenging, because of their rather unstable behavior and the numerous electrical parameters which need to be considered. Thus, most approaches try to avoid accurate modeling of all constraints like the influence of the aggressors on the open net and use simplified fault models in order to detect as many faults as possible or make assumptions which decrease both complexity and accuracy. Yet, this leads to the problem that not only generated tests may be invalidated but also the localization of a specific fault may fail -- in case such a model is used as basis for diagnosis. Furthermore, most of the models do not consider the problem of oscillating behavior, caused by feedback introduced by coupling capacitances, which occurs in almost all designs.
The Robust Enhanced Aggressor Victim Model (REAV) does not only consider the influence of all aggressors accurately but also guarantees robustness against oscillating behavior as well as process variations affecting the thresholds of gates driven by an open interconnect.
In this work we present the first diagnostic classification algorithm for this model. This algorithm considers all constraints enforced by the REAV model accurately - and hence handles unknown values as well as oscillating behavior.
In addition, it allows to distinguish faults at the same interconnect and thus reducing the area that has to be considered for physical failure analysis. Experimental results show the high efficiency of the new method handling circuits with up to 500,000 non-equivalent faults and considerably increasing the diagnostic resolution. Hassan Hatefi, Ralf Wimmer, Bettina Braitling, Luis Maria Ferrer Fioriti, Bernd Becker, Holger HermannsCost vs. Time in Stochastic Games and Markov Automata 2017 Form Asp Comput , Band : 29, Nummer : 4, Seiten : 629 - 649» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Costs and rewards are important tools for analysing quantitative aspects of models like energy consumption and costs of maintenance and repair. Under the assumption of transient costs, this paper considers the computation of expected cost-bounded rewards and cost-bounded reachability for Markov automata and Markov games. We provide a fixed point characterization of this class of properties under early schedulers. Additionally, we give a transformation to expected time-bounded rewards and time-bounded reachability, which can be computed by available algorithms. We prove the correctness of the transformation and show its effectiveness on a number of Markov automata case studies. Uwe Wagschal, Thomas Waldvogel, Thomas Metz, Bernd Becker, Linus Feiten, Samuel Weishaupt, Kamaljeet SinghDas TV-Duell und die Landtagswahl in Schleswig-Holstein: Das Debat-O-Meter als neues Instrument der politischen Kommunikationsforschung 2017 Zeitschrift für Parlamentsfragen (ZParl) , Band : 48. Jg., Nummer : 3, Seiten : 594 - 613» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Politische TV-Debatten sind das Großereignis in modernen Wahlkämpfen und verstärkt Gegenstand von politik- und kommunikationswissenschaftlichen Untersuchungen. Die bisherige Forschung verwendete physische Eingabegeräte, die die Forscher auf Laborsettings mit kleinen Fallzahlen und negativen Effekten auf die externe Validität der Messung festlegte. Der Beitrag präsentiert eine Studie zur Landtagswahl in Schleswig-Holstein 2017 mit dem Debat-O-Meter, eine neue internetbasierte Anwendung für Smartphones, Tablets und PCs, die die Analyse von Wahrnehmungen und Wirkungen von politischen TV-Debatten mit einer großen Anzahl an Teilnehmenden in natürlichen Rezeptionssituationen erlaubt. Es wird gezeigt, dass „Real-Time Response“-Messungen (RTR) mit einer großen Teilnehmerzahl von mehr als 850 durch neue Wege der Rekrutierung mithilfe von Medienpartnern außerhalb des Labors möglich sind. Die Analyse belegt, dass Herausforderer Daniel Günther (CDU) die Debatte für sich entscheiden konnte und identifiziert die Parteineigung, die RTR-Bewertung und die Kandidateneinschätzung in der Vorbefragung als erklärungskräftigste Variablen für den Debattensieg. Pascal Raiola, Jan Burchard, Felix Neubauer, Dominik Erb, Bernd BeckerEvaluating the Effectiveness of D-chains in SAT-based ATPG and Diagnostic TPG 2017 J Electron Test , Band : 33, Nummer : 6, Seiten : 751 - 767» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung The ever increasing size and complexity of today's Very-Large-Scale-Integration (VLSI) designs requires a thorough investigation of new approaches for the generation of test patterns for both test and diagnosis of faults. SAT-based automatic test pattern generation (ATPG) is one of the most popular methods, where, in contrast to classical structural ATPG methods, first a mathematical representation of the problem in form of a Boolean formula is generated, which is then evaluated by a specialized solver. If the considered fault is testable, the solver will return a satisfying assignment, from which a test pattern can be extracted; otherwise no such assignment can exist.
In order to speed up test pattern generation, the concept of D-chains was introduced by Larrabee (1992). Hereby supplementary clauses are added to the Boolean formula, reducing the search space and guiding the solver towards the solution.
In the past, different variants of D-chains have been developed, such as the backward D-chain or the indirect D-chain. In this work we perform a thorough analysis and evaluation of the D-chain variants for test pattern generation and also analyze the impact of different D-chain encodings on diagnostic test pattern generation.
Our experimental results show that depending on the incorporated D-chain the runtime can be reduced tremendously. Jan Burchard, Dominik Erb, Adit D. Singh, Sudhakar M. Reddy, Bernd BeckerFast and Waveform-Accurate Hazard-Aware SAT-Based TSOF ATPG 2017 Conference on Design, Automation and Test in Europe » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Opens are known to be one of the predominant defects in nanoscale technologies. Especially with an increasing number of complex cells in today’s VLSI designs intra-gate opens are becoming a major problem. The generation of tests for these faults is hard, as the timing of the circuit needs to be considered accurately to prevent the invalidation of the generated tests through hazards. Current test generation methods, including new cell aware tests that explicitly target open defects, ignore the possibility of hazard caused test invalidation. Such tests can fail to detect a significant fraction of the targeted opens.
In this work we present a waveform-accurate hazard-aware test generation approach to target intra-gate opens. Our methodology is based on a SAT-based encoding and allows the generation of tests guaranteed to be robust against hazards. Experimental results for large benchmarks mapped to the state-of-the-art NanGate 45nm cell library including complex cells show the test generation efficiency of the proposed method. Large circuits were efficiently handled – even without the use of fault simulation. Our experiments show that on average, about 10.92 % of conventional hazard-
unaware tests will fail to detect the targeted opens because of test invalidation – these are reliably detected by our new test generation methodology. Importantly, our approach can also be applied to improve the effectiveness of commercial cell aware tests. Ralf Wimmer, Andreas Karrenbauer, Ruben Becker, Christoph Scholl, Bernd BeckerFrom DQBF to QBF by Dependency Elimination 2017 Melbourne, VIC, Australia Int'l Conf. on Theory and Applications of Satisfiability Checking , Serge Gaspers and Toby Walsh, Band : 10491, Seiten : 326 - 343» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In this paper, we propose the elimination of dependencies to convert a given dependency quantified Boolean formula (DQBF) to an equisatisfiable QBF. We show how to select a set of dependencies to eliminate such that we arrive at a smallest equisatisfiable QBF in terms of existential variables that is achievable using dependency elimination. This approach is improved by taking so-called don't-care dependencies into account, which result from the application of dependency schemes to the formula and can be added to or removed from the formula at no cost. We have implemented this new method in the state-of-the-art DQBF solver HQS. Experiments show that dependency elimination is clearly superior to the previous method using variable elimination. Ralf Wimmer, Sven Reimer, Paolo Marin, Bernd BeckerHQSpre - An Effective Preprocessor for QBF and DQBF 2017 Uppsala, Sweden International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Part I , Axel Legay and Tiziana Margaria, Band : 10205, Seiten : 373 - 390» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We present our new preprocessor \textsc{HQSpre}, a state-of-the-art tool for simplifying quantified Boolean formulas (QBFs) and the first available preprocessor for dependency quantified Boolean formulas (DQBFs). The latter are a generalization of QBFs, resulting from adding so-called Henkin-quantifiers to QBFs. HQSpre applies most of the preprocessing techniques that have been proposed in the literature. It can be used both as a standalone tool and as a library. It is possible to tailor it towards different solver back-ends, e. g., to preserve the circuit structure of the formula when a non-CNF solver back-end is used. Extensive experiments show that HQSpre allows QBF solvers to solve more benchmark instances and is able to decide more instances on its own than state-of-the-art tools. The same impact can be observed in the DQBF domain as well. Linus Feiten, Matthias Sauer, Bernd BeckerImplementation of Delay-Based PUFs on Altera FPGAs In : Hardware Security and Trust: Design and Deployment of Integrated Circuits in a Threatened Environment 2017, Springer International Publishing , Seiten : 211 - 235, ISBN : 978-3-319-44318-8» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung This chapter focuses on the implementation of delay-based PUFs on Altera FPGAs. While there has been a manifold of publications on how to evaluate and refine PUFs, a thorough description of the required "handicrafts" enabling a novice to enter this exciting research field has so far been missing. The methods shared in this chapter are not just easily extractable from available standard documentation, but have been compiled by the authors over a long period of trials and consultations with the Altera user community. Designing a delay-based PUF on FPGAs requires fine-tuning which is often like diverting the automated design tools from their intended use. For example, the device-specific delays for the PUF response generation are generally gathered from circuitry looking redundant to the bitstream compiler. Therefore, the automatic reduction of such seemingly redundant circuitry must be prevented. The way the circuitry is placed and routed also has a major impact on delay characteristics, so it is necessary to customise this instead of letting the compiler do it automatically. The reader will be walked through all necessary steps by means of a running example enabling them to embark on further experiments on their own. Along the way, the architecture of Altera Cyclone FPGAs is explained and results from the authors' own experimental studies are shared. Sebastian Junges, Nils Jansen, Ralf Wimmer, Tim Quatmann, Leonore Winterer, Joost-Pieter Katoen, Bernd BeckerPermissive Finite-State Controllers of POMDPs using Parameter Synthesis 2017 » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We study finite-state controllers (FSCs) for partially observable Markov decision processes (POMDPs) that are provably correct with respect to given specifications. The key insight is that computing (randomised) FSCs on POMDPs is equivalent to - and computationally as hard as - synthesis for parametric Markov chains (pMCs). This correspondence allows to use tools for parameter synthesis in pMCs to compute correct-by-construction FSCs on POMDPs for a variety of specifications. Our experimental evaluation shows comparable performance to well-known POMDP solvers. Tobias Schubert, Benjamin Völker, Marc Pfeifer, Bernd BeckerThe Smart MiniFab: An Industrial IoT Demonstrator Anywhere at Any Time 2017 Smart Education and e-Learning 2017, Vilamoura/Portugal, KES International Springer International Publishing, Seiten : 253 - 262 Jan Burchard, Ange-Salomé Messeng Ekossono, Jan Horáček, Maël Gay, Bernd Becker, Tobias Schubert, Martin Kreuzer, Ilia PolianTowards Mixed Structural-Functional Models for
Algebraic Fault Attacks on Ciphers 2017 RESCUE Workshop on Reliability, Security and Quality at ETS 2017 Jan Burchard, Ange-Salomé Messeng Ekossono, Jan Horáček, Maël Gay, Bernd Becker, Tobias Schubert, Martin Kreuzer, Ilia PolianTowards Mixed Structural-Functional Models for
Algebraic Fault Attacks on Ciphers 2017 International Verification and Security Workshop (IVSW) 2017 Bernd Becker, Christoph Scholl, Ralf WimmerVerification of Incomplete Designs In : Formal System Verification - State of the Art and Future Trends 2017, Springer , Rolf Drechsler, Seiten : 37 - 72, Rolf Drechsler, ISBN : 978-3-319-57683-1» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We consider the verification of digital systems which are incomplete in the sense that for some modules only their interfaces (i.e., the signals entering and leaving the module) are known, but not their implementations. For such designs, we study realizability (``Is it possible to implement the missing modules such that the complete design has certain properties?'') and validity (``Does a property hold no matter how the missing parts are implemented?''). nach oben zur Jahresübersicht Marc Pfeifer, Tobias Schubert, Bernd BeckerPackSens: A Condition and Transport Monitoring System Based on an Embedded Sensor Platform 2016 7th EAI International Conference on Sensor Systems and Software Proceedings of the 7th EAI International Conference on Sensor Systems and Software , Seiten : 81 - 92» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung As a consequence of the growing globalization, transports which need a safe handling are increasing. Therefore, this paper introduces an innovative transport and condition monitoring system based on a mobile embedded sensor platform. The platform is equipped with a variety of sensors needed to extensively monitor a transport and can be attached directly to the transported good. The included microcontroller processes all relevant data served by the sensors in a very power efficient manner. Furthermore, it provides possible violations of previously given thresholds through a standardized Near Field Communication (NFC) interface to the user. Since falls are one major cause of damages while transportation, the presented system is the first one that not only detects every fall but also analyses the fall height and other parameters related to the fall event in real-time on the platform. The whole system was tested in different experiments where all critical situations and in particular all fall situations have been detected correctly. Benjamin Völker, Tobias Schubert, Bernd BeckeriHouse: A Voice-Controlled, Centralized, Retrospective Smart Home 2016 7th EAI International Conference on Sensor Systems and Software » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Speech recognition in smart home systems has become pop- ular in both, research and consumer areas. This paper introduces an in- novative concept for a modular, customizable, and voice-controlled smart home system. The system combines the advantages of distributed and centralized processing to enable a secure as well as highly modular plat- form and allows to add existing non-smart components retrospectively into the smart environment. To interact with the system in the most com- fortable way - and in particular without additional devices like smart- phones - voice-controlling was added as the means of choice. The task of speech recognition is partitioned into decentral Wake-Up-Word (WUW) recognition and central continuous speech recognition to enable flexibil- ity while maintaining security. This is achieved utilizing a novel WUW algorithm suitable to be executed on small microcontrollers which uses Mel Frequency Cepstral Coefficients as well as Dynamic Time Warping. A high rejection rate up to 99.93% was achieved, justifying the use of the algorithm as a voice trigger in the developed smart home system. Matthias Sauer, Jie Jiang, Sven Reimer, Kohei Miyase, Xiaoqing Wen, Bernd Becker, Ilia PolianOn Optimal Power-aware Path Sensitization 2016 2016 25nd IEEE Asian Test Symposium (ATS) Mathias Soeken, Pascal Raiola, Baruch Sterin, Bernd Becker, Giovanni De Micheli, Matthias SauerSAT-based Combinational and Sequential Dependency Computation 2016 Haifa Verification Conference (HVC) Sebastian Volkmann, Linus Feiten, Christian Zimmermann, Sebastian Sester, Laura Wehle, Bernd BeckerDigitale Tarnkappe: Anonymisierung in Videoaufnahmen 2016 INFORMATIK 2016 Gesellschaft für Informatik (GI) , Heinrich C. Mayr, Martin Pinzger, Band : P-252, Seiten : 413 - 426» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Videoüberwachung ist heute allgegenwärtig. Sie dient dazu, Delikte im Nachhinein aufzuklären, zur Echtzeit-Überwachung oder zur Abschreckung. Darüber hinaus gibt es aber auch wirtschaftliche Interessen für eine Videoüberwachung und automatische Erfassung von Personen - z.B. zur Erstellung von Kundenprofilen und somit zur Analyse von Kaufverhalten. Dem gegenüber stehen Rechtsansprüche sowie ethische und gesellschaftliche Grundnormen, etwa dass Menschen nicht unter Generalverdacht gestellt oder ohne Zustimmung aufgezeichnet werden dürfen. In dieser Arbeit wird ein technischer Lösungsansatz behandelt, der eine flexible Handhabung der Videoüberwachung erlaubt. Es werden in diesem Zusammenhang neben der technischen Umsetzung auch ökonomische, ethische und juristische Fragen betrachtet. Der Lösungsansatz besteht darin, Personen auf Videoaufnahmen durch ein kryptographisches Verfahren unkenntlich zu machen, noch bevor die Aufnahmen die Kamera-Elektronik verlassen. Nur mittels eines geheimen kryptographischen Schlüssels können einzelne Zeit- und Bildbereiche einer Aufnahme wieder deanonymisiert werden, wodurch rechtlichen wie ethischen Bedenken Rechnung getragen werden kann. In kommerziellen Szenarien erlaubt es diese digitale Tarnkappe, dass Kunden z.B. im Rahmen eines Prämien-Programms freiwillig auf Anonymisierung verzichten. Während in der Literatur der Informatik bereits seit längerem Technologien für solche System beschrieben werden, werden in dieser Arbeit Wege gezeigt, wie dessen Einbettung in die Gesellschaft wirklich realisiert werden könnte. Jan Burchard, Tobias Schubert, Bernd BeckerDistributed Parallel #SAT Solving 2016 IEEE Cluster 2016 » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung The #SAT problem, that is counting the number
of solutions of a propositional formula, extends the well-
known SAT problem into the realm of probabilistic reasoning.
However, the higher computational complexity and lack of fast
solvers still limits its applicability for real world problems.
In this work we present our distributed parallel #SAT solver
dCountAntom which utilizes both local, shared-memory paral-
lelism as well as distributed (cluster computing) parallelism.
Although highly parallel solvers are known in SAT solving,
such techniques have never been applied to the #SAT problem.
Furthermore we introduce a solve progress indicator which
helps the user to assess whether the presented problem is likely
solvable within a reasonable time. Our analysis shows a high
accuracy of the estimated progress.
Our experiments with up to 256 CPU cores working in
parallel yield large speedups across different benchmarks
derived from real world problems: With the maximum number
of available cores dCountAntom solved problems on average 141 times faster than a single core implementation. Michael Kochte, Rafal Baranowski, Matthias Sauer, Bernd Becker, Hans-Joachim WunderlichFormal Verification of Secure Reconfigurable Scan Network Infrastructure 2016 IEEE European Test Symposium Michael Kochte, Matthias Sauer, Pascal Raiola, Bernd Becker, Hans-Joachim WunderlichSHIVA: Sichere Hardware in der Informationsverarbeitung
Formaler Nachweis komplexer Sicherheitseigenschaften in rekonfigurierbarer Infrastruktur
2016 eda Workshop Andreas Riefert, Riccardo Cantoro, Matthias Sauer, Matteo Sonza Reorda, Bernd BeckerEffective Generation and Evaluation of Diagnostic SBST Programs
2016 IEEE VLSI Test Symposium Linus Feiten, Matthias Sauer, Bernd BeckerOn Metrics to Quantify the Inter-Device Uniqueness of PUFs 2016 TRUDEVICE Workshop, Dresden » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Physically Unclonable Functions (PUFs) have been an emerging topic in hardware security and trust in recent years, and many different kinds of PUFs have been presented in the literature. An important criterion is always the diversity of PUF responses for different devices, called inter-device uniqueness. A very popular uniqueness metric consists of calculating the pairwise hamming distance between the response bit-strings of all devices, assuming that all response bits are uncorrelated. Such correlations, however, should be regarded when a statement about inter-device uniqueness is made. We therefore propose a novel correlation metric to fulfil this requirement. Furthermore, we show that the hamming distance metric is actually redundant when at the same time the also popular bit-aliasing metric is applied. Matthias Sauer, Sven Reimer, Daniel Tille, Karsten Scheibler, Dominik Erb, Ulrike Pfannkuchen, Bernd BeckerClock Cycle Aware Encoding for SAT-based Circuit Initialization 2016 GI/ITG Workshop “Testmethoden und Zuverlässigkeit von Schaltungen und Systemen” Andreas Riefert, Riccardo Cantoro, Matthias Sauer, Matteo Sonza Reorda, Bernd BeckerA Flexible Framework for the Automatic Generation of SBST Programs 2016 IEEE Transactions on Very Large Scale Integration (VLSI) Systems , Band : 24, Nummer : 10, Seiten : 3055 - 3066 Karsten Scheibler, Dominik Erb, Bernd BeckerAccurate CEGAR-based ATPG in Presence of Unknown Values for Large Industrial Designs 2016 Conf. on Design, Automation and Test in Europe » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Unknown values emerge during the design and test generation process as well as during later test application and system operation. They adversely affect the test quality by reducing the controllability and observability of internal circuit structures -- resulting in a loss of fault coverage. To handle unknown values, conventional test generation algorithms as used in state-of-the-art commercial tools, rely on n-valued algebras. However, n-valued algebras introduce pessimism as soon as X-values reconverge. Consequently, these algorithms fail to compute the accurate result.
Therefore, this paper focuses on a new highly incremental CEGAR-based algorithm that overcomes these limitations and hence is completely accurate in presence of unknown values. It relies on a modified SAT-solver tailored to this specific problem. The experimental results for circuits with up to 2.400.000 gates show that this combination allows high accuracy and high scalability at the same time. Compared to a state-of-the-art commercial tool, the fault coverage could be increased significantly. Furthermore, the runtime is reduced remarkably compared to a QBF-based encoding of the problem. Felix Neubauer, Karsten Scheibler, Bernd Becker, Ahmed Mahdi, Martin Fränzle, Tino Teige, Tom Bienmüller, Detlef FehrerAccurate Dead Code Detection in Embedded C
Code by Arithmetic Constraint Solving 2016 First International Workshop on Satisfiability Checking and Symbolic Computation - FETOPEN-CSA SC2 Workshop - Affiliated with SYNASC 2016 » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Unreachable code fragments in software, despite not having a negative impact on the functional behavior, can have a bad effect in other areas, such as code optimization or coverage-based code validation and certification. Especially the latter is important in industrial, safety critical environments, where detecting such dead code is a major goal to adjust the coverage of software tests.
In the context of embedded systems we focus on C programs which are reactive, control-oriented, and floating-point dominated. Such programs are either automatically generated
from Simulink-plus-Stateflow models or hand-written according to coding guidelines. While there are various techniques – e.g. abstract interpretation or Counterexample guided abstraction refinement (CEGAR) – to deal with individual issues of this domain, there is none which can cover all of them. The AVACS transfer project T1 aims at the combination of these techniques in order to provide an accurate and efficient dead code detection.
In this paper we present the ideas and goals of the project as well as the current status (including very promising experimental results) and future challenges. Karsten Scheibler, Felix Neubauer, Ahmed Mahdi, Martin Fränzle, Tino Teige, Tom Bienmüller, Detlef Fehrer, Bernd BeckerAccurate ICP-based Floating-Point Reasoning 2016 Formal Methods in Computer-Aided Design , Seiten : 177 - 184» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In scientific and technical software, floating-point arithmetic is often used to approximate arithmetic on physical quantities natively modeled as reals. Checking properties for such programs (e.g. proving unreachability of code fragments) requires accurate reasoning over floating-point arithmetic.
Currently, most of the SMT-solvers addressing this problem class rely on bit-blasting. Recently, methods based on reasoning in interval lattices have been lifted from the reals (where they traditionally have been successful) to the floating-point numbers. The approach presented in this paper follows the latter line of interval-based reasoning, but extends it by including bitwise integer operations and
cast operations between integer and floating-point arithmetic. Such operations have hitherto been omitted, as they tend to define sets not concisely representable in interval lattices, and were consequently considered the domain of bit-blasting approaches. By adding them
to interval-based reasoning, the full range of basic data types and operations of C programs is supported. Furthermore, we propose techniques in order to mitigate the problem of aliasing during interval reasoning.
The experimental results confirm the efficacy of the proposed techniques. Our approach outperforms solvers relying on bit-blasting as well as the existing interval-based SMT-solver. Ahmed Mahdi, Karsten Scheibler, Felix Neubauer, Martin Fränzle, Bernd BeckerAdvancing software model checking beyond linear arithmetic theories 2016 12th International Haifa Verification Conference, HVC 2016, Haifa, Israel, November 14-17, 2016 Twelfth Haifa Verification Conference 2016 , Bloem, Roderick, Arbel, Eli (Eds.), Band : 10028, Seiten : 186 - 201» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Motivated by the practical need for verifying embedded control programs involving linear, polynomial, and transcendental arithmetics, we demonstrate in this paper a CEGAR technique addressing reachability checking over that rich fragment of arithmetics. In contrast to previous approaches, it is neither based on bit-blasting of floating-
point implementations nor confined to decidable fragments of real arithmetic, namely linear or polynomial arithmetic. Its CEGAR loop is based on Craig interpolation within the iSAT3 SMT solver, which employs (abstract) conflict-driven clause learning (CDCL) over interval domains together with interval constraint propagation. As usual, the interpolants
thus obtained on spurious counterexamples are used to subsequently refine the abstraction, yet in contrast to manipulating and refining the state set of a discrete-state abstraction, we propose a novel technique for refining the abstraction, where we annotate the abstract model’s transitions with side-conditions summarizing their effect. We exploit this for implementing case-based reasoning based on assumption-commitment predicates extracted from the stepwise interpolants in a lazy abstraction mechanism. We implemented our approach within iSAT3 and demonstrate its effectiveness by verifying several benchmarks. Karsten Scheibler, Dominik Erb, Bernd BeckerApplying Tailored Formal Methods to X-ATPG 2016 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung When producing integrated circuits (ICs) one wants to know whether a manufactured IC works as expected and is free of physical defects. Basically, for combinational circuits, this is done by applying patterns to the circuit inputs and checking if the circuit outputs show the expected result. In case of sequential circuits, one concentrates on the combinational core of the circuit and treats the signal lines driven by flip-flops as additional (secondary) inputs. The job of automatic test pattern generation (ATPG) is to find such input patterns. Usually, these patterns are generated with respect to a fault-model. E.g. the stuck-at fault model assumes that a physical defect causes signal lines in a circuit to stay on a fixed logical value (logic-0 or logic-1). The aim is to find patterns for all possible fault locations. In SAT-based ATPG the circuit is transformed into two Boolean formulas F1 and F2. One formula describes the fault-free circuit and the second formula contains the fault-affected circuit (we consider one fault at a time). If (F1 XOR F2) is satisfiable a test pattern for the current fault under consideration is found. This is the basic principle of two-valued SAT-based ATPG and a very similar approach is used for combinational equivalence checking.
However, usually, one can not assume full control of all sequential elements and primary inputs. Therefore, uninitialized flip-flops may occur in the design -- leading to binary but unknown values (X-values). Classically, these X-values are handled by three-valued logic (01X). But this introduces pessimism when X-values reconverge in the circuit. On the other hand, the expressiveness of QBF allows to encode the unknown values accurately -- but comes at the cost of much higher runtimes. Therefore, we presented in [1] an accurate SAT-based CEGAR approach for automatic test pattern generation (ATPG) in presence of X-values. This approach is tailored to and optimized for this specific problem class and could also be used for closely related topics such as equivalence checking in presence of X-values. Although the approach is similar to an existing CEGAR-based 2-QBF solving algorithm, we show that our method has up to 50x lower runtimes. This underlines that an efficient CNF-encoding of a problem together with the fastest available standard solver does not guarantee optimal performance. Tailoring the underlying formal methods to the target problem class may give remarkable speedups on top. Thomas Metz, Uwe Wagschal, Thomas Waldvogel, Marko Bachl, Linus Feiten, Bernd BeckerDas Debat-O-Meter: ein neues Instrument zur Analyse von TV-Duellen 2016 ZSE Zeitschrift für Staats- und Europawissenschaften , Band : 14, Nummer : 1, Seiten : 124 - 149 Ralf Wimmer, Christoph Scholl, Karina Wimmer, Bernd BeckerDependency Schemes for DQBF 2016 Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing (SAT) , Springer, Band : 9710, Seiten : 473 - 489» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Dependency schemes allow to identify variable independencies in QBFs or DQBFs. For QBF, several dependency schemes have been proposed, which differ in the number of independencies they are able to identify. In this paper, we analyze the spectrum of dependency schemes that were proposed for QBF. It turns out that only some of them are sound for DQBF. For the sound ones, we provide a correctness proof, for the others counterexamples. Experiments show that a significant number of dependencies can either be added to or removed from a formula without changing its truth value, but with significantly increasing the flexibility for modifying the representation. Karsten Scheibler, Felix Neubauer, Ahmed Mahdi, Martin Fränzle, Tino Teige, Tom Bienmüller, Detlef Fehrer, Bernd BeckerExtending iSAT3 with ICP-Contractors for Bitwise Integer
Operations AVACS Technical Report, SFB/TR 14 AVACS, Subproject T1 , Band : 116, 2016 Dominik Erb, Karsten Scheibler, Michael A. Kochte, Matthias Sauer, Hans-Joachim Wunderlich, Bernd BeckerMixed 01X-RSL-Encoding for Fast and Accurate ATPG with Unknowns 2016 21st Asia and South Pacific Design Automation Conference » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Unknown (X) values in a design introduce pessimism
in conventional test generation algorithms, which results in a loss of fault coverage. This pessimism is reduced by a more accurate modeling and analysis. Unfortunately, accurate analysis techniques highly increase runtime and limit scalability. One promising technique to prevent high runtimes while still providing high accuracy is the use
of restricted symbolic logic (RSL). However, also pure RSL-based algorithms reach their limits as soon as millon gate circuits need to be processed.
In this paper, we propose new ATPG techniques to overcome such limitations. An efficient hybrid encoding combines the accuracy of RSL-based modeling with the compactness of conventional three-valued encoding. A low-cost two-valued SAT-based untestability check is able to classify most untestable faults with low runtime. An incremental and event-based accurate fault simulator is introduced to reduce fault simulation effort. The experiments demonstrate the effectiveness of the proposed techniques. On average, over 99.3% of the faults are accurately classified. Both the number of aborts and the total runtime are significantly reduced compared to the state-of-the-art pure RSL-based algorithm. For circuits up to a million gates, the fault coverage could be increased considerably compared to a state-of-the-art commercial tool with very competitive runtimes. Linus Feiten, Sebastian Sester, Christian Zimmermann, Sebastian Volkmann, Laura Wehle, Bernd BeckerRevocable Anonymisation in Video Surveillance: A "Digital Cloak of Invisibility" In : Technology and Intimacy: Choice or Coercion 2016, Springer International Publishing , Seiten : 314 - 327, ISBN : 978-3-319-44804-6» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Video surveillance is an omnipresent phenomenon in today's metropolitan life. Mainly intended to solve crimes, to prevent them by realtime-monitoring or simply as a deterrent, video surveillance has also become interesting in economical contexts; e.g. to create customer profiles and analyse patterns of their shopping behaviour. The extensive use of video surveillance is challenged by legal claims and societal norms like not putting everybody under generalised suspicion or not recording people without their consent. In this work we propose a technological solution to balance the positive and negative effects of video surveillance. With automatic image recognition algorithms on the rise, we suggest to use that technology to not just automatically identify people but blacken their images. This blackening is done with a cryptographic procedure allowing to revoke it with an appropriate key. Many of the legal and ethical objections to video surveillance could thereby be accommodated. In commercial scenarios, the operator of a customer profiling program could offer enticements for voluntarily renouncing one's anonymity. Customers could e.g. wear a small infrared LED to signal their agreement to being tracked. After explaining the implementation details, this work outlines a multidisciplinary discussion incorporating an economic, ethical and legal viewpoint. Bernd Becker, Katrin Weber, Linus FeitenSMartphones In der LEhre (SMILE) In : Kreativ, Innovativ, Motivierend - Lehrkonzepte in der Praxis: Der Instructional Development Award (IDA) der Universität Freiburg 2016, Universitäts Verlag Webler (UVW) , Seiten : 117 - 133, ISBN : 3-946017-01-0 Karina Wimmer, Ralf Wimmer, Christoph Scholl, Bernd BeckerSkolem Functions for DQBF 2016 Int'l Symposium on Automated Technology for Verification and Analysis (ATVA) Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA) , Springer, Band : 9938, Seiten : 395 - 411» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We consider the problem of computing Skolem functions for satisfied dependency quantified Boolean formulas (DQBFs). We show how Skolem functions can be obtained from an elimination-based DQBF solver and how to take preprocessing steps into account. The size of the Skolem functions is optimized by don't-care minimization using Craig interpolants and rewriting techniques. Experiments with our DQBF solver HQS show that we are able to effectively compute Skolem functions with very little overhead compared to the mere solution of the formula. Karina Wimmer, Ralf Wimmer, Christoph Scholl, Bernd BeckerSkolem Functions for DQBF (Extended Version) , 2016 Maël Gay, Jan Burchard, Jan Horáček, Ange-Salomé Messeng Ekossono, Tobias Schubert, Bernd Becker, Ilia Polian, Martin KreuzerSmall Scale AES Toolbox: Algebraic and Propositional
Formulas, Circuit-Implementations and Fault Equations 2016 FCTRU'16 Linus Feiten, Jonathan Oesterle, Tobias Martin, Matthias Sauer, Bernd BeckerSystematic Frequency Biases in Ring Oscillator PUFs on FPGAs
2016 IEEE Transactions on Multi-Scale Computing Systems (TMSCS) , Band : PP, Nummer : 99» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Physically unclonable functions (PUFs) are an emerging primitive in hardware security, enabling the identification of computer-chips. A promising type particularly for FPGA implementations is the Ring Oscillator (RO) PUF, where signal delays – stemming from uncontrollable variations in the manufacturing process – are used as device-specific characteristics. Based on experimental results gathered with 38 identical Altera FPGAs, we show the existence of nondevice- specific i.e. systemic RO frequency biases, traced back to (1) the internal routing within the RO’s look-up tables, (2) the RO locations on the FPGAs, or (3) the non-PUF payload activity. As these biases are the same for all devices, the result is poor inter-device uniqueness and unreliable signatures under changing payloads. After characterising these biases with a newly developed set of metrics, we suggest a method to overcome them: Using only a small sample of devices, the average bias over all devices for each RO is predicted and the relative differences caused by systemic biases are nullified. We demonstrate the viability of this method by determining the sufficient random sample sizes and showing that the inter-device uniqueness is drastically increased and the PUF signatures become reliable even under changing payload activities. Matthias Sauer, Linus Feiten, Bernd Becker, Ulrich Rührmair, Ilia PolianUtilizing Intrinsic Delay Variability in Complex Digital Circuits for Defining PUF Behavior 2016 TRUDEVICE Workshop, Dresden nach oben zur Jahresübersicht Jan Burchard, Tobias Schubert, Bernd BeckerLaissez-Faire Caching for Parallel #SAT Solving 2015 International Conference on Theory and Applications of Satisfiability Testing , Band : 9340, Seiten : 46 - 61» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung The problem of counting the number of satisfying assignments
of a propositional formula (#SAT) can be considered to be the big brother
of the well known SAT problem. However, the higher computational
complexity and a lack of fast solvers currently limit its usability for real
world problems.
Similar to SAT, utilizing the parallel computation power of modern
CPUs could greatly increase the solving speed in the realm of #SAT.
However, in comparison to SAT there is an additional obstacle for the
parallelization of #SAT that is caused by the usage of conflict learning
together with the #SAT specific techniques of component caching and
sub-formula decomposition. The combination can result in an incorrect
final result being computed due to incorrect values in the formula cache.
This problem is easily resolvable in a sequential solver with a depth-first
node order but requires additional care and handling in a parallel one. In
this paper we introduce laissez-faire caching which allows for an arbitrary
node computation order in both a sequential and parallel solver while
ensuring a correct final result. Additionally, we apply this new caching
approach to build countAntom, the world’s first parallel #SAT-solver.
Our experimental results clearly show that countAntom achieves con-
siderable speedups through the parallel computation while maintaining
correct results on a large variety of benchmarks coming from different
real-world applications. Moreover, our analysis indicates that laissez-faire
caching only adds a small computational overhead. Linus Feiten, Tobias Martin, Matthias Sauer, Bernd BeckerImproving RO-PUF Quality on FPGAs by Incorporating Design-Dependent Frequency Biases 2015 IEEE European Test Symposium » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Physically unclonable functions (PUFs) based on ring oscillators (ROs) are a popular primitive in hardware security, meant to enable the unambiguous and tamper-proof identification of computer chips. This is achieved by exploiting different signal delays on each chip stemming from uncontrollable variations during the manufacturing process. Thus, the relation between RO frequencies on an individual chip can be used as the chip's unique PUF signature. In this work, we show how ROs implemented on a larger number of Altera Cyclone IV FPGAs are biased towards slower or faster frequencies in non-uniform ways depending on the FPGA's programming with different design; even though the ROs are placed and routed equally. Without considering these biases, inter-device uniqueness of the PUF signatures is degraded. We demonstrate that subtracting
the mean frequency of each RO - derived using only a small training set of devices - from the sampled frequencies overcomes this disadvantage; i.e. the uniqueness is increased drastically while maintaining reliability. Kohei Miyase, Matthias Sauer, Bernd Becker, Xiaoqing Wen, Seiji KajiharaIdentification of High Power Consuming Areas with Gate Type and Logic Level Information 2015 IEEE European Test Symposium Andreas Riefert, Riccardo Cantoro, Matthias Sauer, Matteo Sonza Reorda, Bernd BeckerOn the Automatic Generation of SBST Test Programs for In-Field Test 2015 GI/ITG Workshop “Testmethoden und Zuverlässigkeit von Schaltungen und Systemen” Bettina Braitling, Luis María Ferrer Fioriti, Hassan Hatefi, Ralf Wimmer, Bernd Becker, Holger HermannsAbstraction-based Computation of Reward Measures for Markov Automata 2015 Mumbai, India Int'l Conf. Verification, Model Checking, and Abstract Interpretation (VMCAI) , Band : 8931, Seiten : 172 - 189 Dominik Erb, Michael A. Kochte, Sven Reimer, Matthias Sauer, Hans-Joachim Wunderlich, Bernd BeckerAccurate QBF-based Test Pattern Generation in Presence of Unknown Values 2015 Computer-Aided Design of Integrated Circuits and Systems (TCAD) » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Unknown (X) values emerge during the design process as well as during system operation and test application. X-sources are for instance black boxes in design models, clockdomain boundaries, analog-to-digital converters, or uncontrolled or uninitialized sequential elements.
To compute a test pattern for a given fault, well-defined logic values are required both for fault activation and Propagation to observing outputs. In presence of X-values, conventional test generation algorithms, based on structural algorithms, Boolean satisfiability (SAT), or BDD-based reasoning may fail to generate test patterns or to prove faults untestable.
This work proposes the first efficient stuck-at and transition-delay fault test generation algorithm able to prove testability or untestability of faults in presence of X-values. It overcomes the principal pessimism of conventional algorithms when X-values are considered by mapping the test generation problem to the satisfiability of Quantified Boolean Formulae (QBF).
Experiments on ISCAS benchmarks and larger industrial
circuits investigate the increase in fault coverage for conventional deterministic and potential detection requirements for both randomized and clustered X-sources. Linus Feiten, Tobias Martin, Matthias Sauer, Bernd BeckerAnalysis and utilisation of deviations in RO-PUFs under altered FPGA designs 2015 TRUDEVICE Workshop, Grenoble » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Physically unclonable functions (PUFs) based on ring oscillators (ROs) are a popular primitive in hardware security, enabling the unambiguous and tamper-proof identification of computer chips. This is achieved by exploiting uncontrollable variations in the chip manufacturing process, leading to different signal delays of each chip. Thus, if all ROs on a chip are affected uniformly by ageing and temperature effects, the relation between their frequencies can be used as the chip's unique finger print. A problem arises when the RO frequencies change in a non-uniform way.
Here, we are sharing our experiences from analyses on 70 FPGAs about how ROs implemented on Altera Cyclone IV FPGAs are affected in non-uniform ways depending on the non-PUF circuitry of the design. As specific ROs are affected towards faster or slower frequencies on all devices, this leads to bad inter-device uniqueness. We suggest that subtracting the mean frequency - derived with a training set of devices - from the sampled frequencies per RO on all devices will overcome this disadvantage. Hassan Hatefi, Bettina Braitling, Ralf Wimmer, Luis Maria Ferrer Fioriti, Holger Hermanns, Bernd BeckerCost vs. Time in Stochastic Games and Markov Automata 2015 International Symposium on Dependable Software Engineering: Theory, Tools and Applications (SETTA) Proc. of SETTA , Springer-Verlag, Band : 9409, Seiten : 19 - 34» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Costs and rewards are important tools for analysing quantitative aspects of models like energy consumption and costs of maintenance and repair. Under the assumption of transient costs, this paper considers the computation of expected cost-bounded rewards and cost-bounded reachability for Markov automata and stochastic games. We give a transformation of this class of properties to expected time-bounded rewards and time-bounded reachability, which can be computed by available algorithms. We prove the correctness of the transformation and show its effectiveness on a number of case studies. Linus Feiten, Matthias Sauer, Tobias Schubert, Victor Tomashevich, Ilia Polian, Bernd BeckerFormal Vulnerability Analysis of Security Components 2015 IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD) , Band : 34, Nummer : 8, Seiten : 1358 - 1369» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Vulnerability to malicious fault attacks is an emerging concern for hardware circuits that are employed in mobile and embedded systems and process sensitive data. We describe a new methodology to assess the vulnerability of a circuit to such attacks, taking into account built-in protection mechanisms. Our method is based on accurate modeling of fault effects and detection status expressed by Boolean satisfiability (SAT) formulas. Vulnerability is quantified based on the number of solutions of these formulas, which are determined by an efficient #SAT solver. We demonstrate the applicability of this method for design space exploration of a pseudo random number generator and for calculating the attack success rate in a multiplier circuit protected by robust error-detecting codes. Andreas Riefert, Matthias Sauer, Sudhakar Reddy, Bernd BeckerImproving Diagnosis Resolution of a Fault Detection Test Set 2015 VLSI Test Symposium » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Manufactured VLSI circuits using a new technology typically suffer from systematic defects that are process-dependent and at sub-nanometer feature sizes such defects may be even design-dependent. The root causes for systematic defects must be determined to ramp up yields. Volume diagnosis is becoming popular to identify root causes for systematic defects. Volume diagnosis uses logic diagnosis based on failing circuit responses to production tests of a large number of failing devices, followed by statistical analysis methods to determine the root cause(s) for yield limiters. Typically production tests use fault detection tests and hence may have limited diagnosis resolution. To improve diagnosis resolution diagnostic ATPGs can be used to generate test sets to distinguish all pairs of distinguishable faults in one or more fault models. The sizes of such tests tend to be considerably higher than fault detection test sets used as production tests. For this reason, generation of test sets that detect faults and also possess a high diagnosis resolution is important.
In this work we present a method to improve the diagnosis resolution of a compact fault detection test set without increasing pattern count or decreasing fault coverage. The basic idea of the approach is to generate a SAT formula which enforces diagnosis and is solved by a MAX-SAT solver which is a SAT-based maximization tool. We believe this is the first time a method to improve diagnosis resolution of a test set of given size has been reported. Experimental results on ISCAS 89 circuits demonstrate the effectiveness of the proposed method. Karsten Scheibler, Dominik Erb, Bernd BeckerImproving Test Pattern Generation in Presence of Unknown Values beyond Restricted Symbolic Logic 2015 to be published at European Test Symposium (ETS) » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Test generation algorithms considering unknown (X) values are pessimistic if standard n-valued logic algebras are used. This results on an overestimation of the number of signals with X-values and an underestimation of the fault coverage. In contrast, algorithms based on quantified Boolean formula (QBF), are accurate in presence of X-values but have limits with respect to runtime, scalability and robustness.
Recently, an algorithm based on restricted symbolic logic (RSL) has been presented which is more accurate than classical three-valued logic and faster than QBF. Nonetheless, this RSL-based approach is still pessimistic and is unable to detect all testable faults. Additionally, it does not allow the accurate identification of untestable faults.
In this paper, we improve test generation based on RSL in two directions in order to reduce the gap to QBF further. First, we present techniques to go beyond the accuracy of RSL when generating test patterns. Second, we include a check which is able to accurately identify untestable faults. Experimental results show the high efficiency of the proposed method classifying almost all faults as testable or proving untestability. Bernd Becker, Matthias Sauer, Christoph Scholl, Ralf WimmerModeling Unknown Values in Test and Verification In : Formal Modeling and Verification of Cyber-Physical Systems (Proceedings of the 1st International Summer School on Methods and Tools for the Design of Digital Systems) 2015, Springer , Rolf Drechsler, Ulrich Kühne, Seiten : 122 - 150, Rolf Drechsler, Ulrich Kühne, ISBN : 978-3-658-09993-0» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung With increasing complexities and a component-based design style the handling of unkown values (e. g., at the interface of components) becomes more and more important in electronic design automation (EDA) and production processes. Tools are required that allow an accurate modeling of unkowns in combination with algorithms balancing exactness of representation and efficiency of calculation. In the following, state-of-the-art approaches are described that enable an efficient and successful handling of unknown values using formal techniques in the areas of Test and Verification. Dominik Erb, Karsten Scheibler, Matthias Sauer, Sudhakar M. Reddy, Bernd BeckerMulti-Cycle Circuit Parameter Independent ATPG for Interconnect Open Defects 2015 33rd VLSI Test Symposium (VTS) » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Interconnect opens are known to be one of the predominant defects in nanoscale technologies. Generating tests to detect such defects is challenging due to the need to accurately determine the coupling capacitances between the open net and its aggressors and fix the state of these aggressors during test. Process variations cause deviations from assumed values of circuit parameters thus potentially invalidating tests generated with assumed circuit parameters. Additionally, recent investigation using test chips showed that the steady state voltage on open nets may drift slowly with the application of circuit inputs and can be different at different nets.
Recently we proposed a class of tests called Circuit Parameter Independent (CPI) tests to detect interconnect opens and reported on an implementation of a test generator for them. CPI tests detect opens independent of the values of coupling capacitances and the initial trapped charge on the open net and hence are robust against process variations affecting these parameters. Yet, this work did not address the effects of leakage currents on open nets.
In this work we extend the validity of CPI tests by introducing so-called multi-cycle CPI tests and single-value CPI tests. By doing so, we significantly improve the coverage of open defects and ensure their detection whilst including the additional effect of leakage currents on opens. Experimental results for circuits with over 500k non-equivalent faults and several thousand aggressors %deriving the new classes of CPI tests show the effectiveness of the newly proposed CPI tests as well as the high efficiency of a new ATPG algorithm to generate these new classes of CPI tests. Andreas Riefert, Riccardo Cantoro, Matthias Sauer, Matteo Sonza Reorda, Bernd BeckerOn the Automatic Generation of SBST Test Programs for In-Field Test 2015 Conf. on Design, Automation and Test in Europe Matthias Sauer, Bernd Becker, Ilia PolianPHAETON: A SAT-based Framework for Timing-aware Path Sensitization 2015 Ieee T Comput , Band : PP, Nummer : 99» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung nowledge about sensitizable paths through combinational logic is essential for numerous design tasks. We present the framework PHAETON which identifies sensitizable paths and generates test pairs to exercise these paths using Boolean satisfiability (SAT). PHAETON supports a large number of models and sensitization conditions and provides a generic interface that can be used by applications. It incorporates a novel application-specific unary representation of integer numbers to integrate timing information with logical conditions within the same monolithic SAT formula. Due to a number of further elaborate speedup techniques, PHAETON scales to industrial circuits. Experimental results show the performance of PHAETON in classical K longest path generation tasks and in new post-silicon validation and characterization scenarios. Ralf Wimmer, Karina Gitina, Jennifer Nist, Christoph Scholl, Bernd BeckerPreprocessing for DQBF 2015 Proceedings of the 18th International Conference on Theory and Applications of Satisfiability Testing (SAT) , Springer, Band : 9340, Seiten : 173 - 190» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung For SAT and QBF formulas many techniques are applied in order to reduce/modify the number of variables and clauses of the formula, before the formula is passed to the actual solving algorithm. It is well known that these preprocessing techniques often reduce the computation time of the solver by orders of magnitude. In this paper we generalize different preprocessing techniques for SAT and QBF problems to dependency quantified Boolean formulas (DQBF) and describe how they need to be adapted to work with a DQBF solver core. We demonstrate their effectiveness both for CNF- and non-CNF-based DQBF algorithms. Karina Gitina, Ralf Wimmer, Sven Reimer, Matthias Sauer, Christoph Scholl, Bernd BeckerSolving DQBF Through Quantifier Elimination 2015 Conf. on Design, Automation and Test in Europe Karsten Scheibler, Leonore Winterer, Ralf Wimmer, Bernd BeckerTowards Verification of Artificial Neural Networks 2015 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We consider the safety verification of controllers obtained via machine learning. This is an important problem as the employed machine learning techniques work well in practice, but cannot guarantee safety of the produced controller, which is typically represented as an artificial neural network. Nevertheless, such methods are used in safety-critical environments.
In this paper we take a typical control problem, namely the Cart Pole System (a.k.a. inverted pendulum), and a model of its physical environment and study safety verification of this system. To do so, we use bounded model checking (BMC). The created formulas are solved with the SMT-solver iSAT3. We examine the problems that occur during solving these formulas and show that extending the solver by special deduction routines can reduce both memory consumption and computation time on such instances significantly. This constitutes a first step towards verification of machine-learned controllers, but a lot of challenges remain. Ernst Moritz Hahn, Holger Hermanns, Ralf Wimmer, Bernd BeckerTransient Reward Approximation for Continuous-Time Markov Chains 2015 Ieee T Reliab , Band : 64, Nummer : 4» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We are interested in the analysis of very large continuous-time Markov chains (CTMCs) with many distinct rates. Such models arise naturally in the context of the reliability analysis, e.g., of computer networks performability analysis, of power grids, of computer virus vulnerability, and in the study of crowd dynamics. We use abstraction techniques together with novel algorithms for the computation of bounds on the expected final and accumulated rewards in continuous-time Markov decision processes (CTMDPs). These ingredients are combined in a partly symbolic and partly explicit (symblicit) analysis approach. In particular, we circumvent the use of multi-terminal decision diagrams, because the latter do not work well if facing a large number of different rates. We demonstrate the practical applicability and efficiency of the approach on two case studies. Christian Miller, Paolo Marin, Bernd BeckerVerification of Partial Designs Using Incremental QBF 2015 Ai Commun , Band : 28, Nummer : 2, Seiten : 283 - 307» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung SAT solving is an indispensable core component of numerous formal verification tools and has found widespread use in industry, in particular when using it in an incremental fashion, e.g. in Bounded Model Checking (BMC). On the other hand, for some applications SAT formulas are not expressive enough, whereas a description via Quantified Boolean Formulas (QBF) is much more adequate, for instance when dealing with partial designs. Motivated by the success of incremental SAT, in this paper we explore various approaches to solve QBF problems in an incremental fashion and thereby make this technology usable as a core component of BMC. Firstly, we realized an incremental QBF solver based on the state-of-the-art QBF solver QuBE: Taking profit from the reuse of some information from previous iterations, the search space can be pruned, in some cases, to even less than a quarter. However, the need for preprocessing QBF formulas prior to the solving phase, that in general cannot be paired with incremental solving because of the non-predictable elimination of variables in the future incremental steps, posed the question of incremental QBF preprocessing. In this context we present an approach for retaining the QBF formula being preprocessed while extending its clauses and prefix incrementally. This procedure results in a significant size reduction of the QBF formulas, hence leading to a reduced solving time. As this may come together with a high preprocessing time, we analyze various heuristics to dynamically disable incremental preprocessing when its overhead raises over a certain threshold and is not compensated by the reduced solving time anymore. For proving the efficacy of our methods experimentally, as an application we consider BMC for partial designs (i.e. designs containing so-called blackboxes which represent unknown parts). Here, we disprove realizability, that is, we prove that an unsafe state is reachable no matter how the blackboxes are implemented. We examine all these incremental approaches from both the point of view of the effectiveness of the single procedure and the benefits that a range of QBF solvers can take from it. On a domain of partial design benchmarks, engaging incremental QBF methods significant performance gains over non incremental BMC can be achieved. nach oben zur Jahresübersicht Dominik Erb, Karsten Scheibler, Matthias Sauer, Sudhakar M. Reddy, Bernd BeckerCircuit Parameter Independent Test Pattern Generation
for Interconnect Open Defects 2014 23nd IEEE Asian Test Symposium (ATS) » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Open defects such as interconnect opens are known
to be one of the predominant defects in nanoscale technologies.
Yet, test pattern generation for open defects is challenging because
of the high number of parameters which need to be considered.
Additionally, the assumed values of these parameters may vary due
to process variations reducing fault coverage of a test set generated
under this assumption.
This paper presents a new ATPG approach for circuit parameter
independent (CPI) tests. In addition a definition of oscillation free
CPI tests is given. The generated tests are robust against process
variations affecting the influence of neighboring interconnects as
well as trapped charge and prohibit oscillating behavior.
Experimental results show the high efficiency of the new approach,
generating CPI tests for circuits with over 500k nonequivalent
faults and several thousand aggressors. Sven Reimer, Matthias Sauer, Tobias Schubert, Bernd BeckerIncremental Encoding and Solving of Cardinality Constraints 2014 International Symposium on Automated Technology for Verification and Analysis , Springer International Publishing, Band : 8837, Seiten : 297 - 313» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Traditional SAT-based MaxSAT solvers encode cardinality constraints directly as part of the CNF and solve the entire optimization problem by a sequence of iterative calls of the underlying SAT solver. The main drawback of such approaches is their dependence on the number of soft clauses: The more soft clauses the MaxSAT instance contains, the larger is the CNF part encoding the cardinality constraints. To counter this drawback, we introduce an innovative encoding of cardinality constraints: Instead of translating the entire and probably bloated constraint network into CNF, a divide-and-conquer approach is used to encode partial constraint networks successively. The resulting subproblems are solved and merged incrementally, reusing not only intermediate local optima, but also additional constraints which are derived from solving the individual subproblems by the back-end SAT solver. Extensive experimental results for the last MaxSAT evaluation benchmark suitew demonstrate that our encoding is in general smaller compared to existing methods using a monolithic encoding of the constraints and converges faster to the global optimum. Sven Reimer, Matthias Sauer, Paolo Marin, Bernd BeckerQBF with Soft Variables 2014 International Workshop on Automated Verification of Critical Systems (AVOCS) Bernd Becker, Rolf Drechsler, Stephan Eggersglüß, Matthias SauerRecent advances in SAT-based ATPG: Non-standard fault models, multi constraints and optimization 2014 International Conference on Design Technology of Integrated Systems In Nanoscale Era (DTIS) Matthias Sauer, Ilia Polian, Michael E. Imhof, Abdullah Mumtaz, Eric Schneider, Alexander Czutro, Hans-Joachim Wunderlich, Bernd BeckerVariation-Aware Deterministic ATPG 2014 IEEE European Test Symposium , Seiten : 1 - 6» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In technologies affected by variability, the detection status of a small-delay fault may vary among manufactured circuit instances. The same fault may be detected, missed or provably undetectable in different circuit instances. We introduce the first complete flow to accurately evaluate and systematically maximize the test quality under variability. As the number of possible circuit instances is infinite, we employ statistical analysis to obtain a test set that achieves a fault-efficiency target with an user-defined confidence level. The algorithm combines a classical path-oriented test-generation procedure with a novel waveformaccurate engine that can formally prove that a small-delay fault is not detectable and does not count towards fault efficiency. Extensive simulation results demonstrate the performance of the generated test sets for industrial circuits affected by uncorrelated and correlated variations. Matthias Sauer, Sven Reimer, Sudhakar M. Reddy, Bernd BeckerEfficient SAT-based Circuit Initialization for Large Designs 2014 Int'l Conf. on VLSI Design » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We present a procedure to determine initialization sequences for a sequential circuit optimizing sequence length and unknown values (Xes) in the flip-flops. Specifically, we consider the following two problems: (1) Determine a sequence that initializes a maximal set of flip-flops starting in a completely unknown state. (2) Determine a minimal subset of flip-flops that need to be controllable such that the circuit can be completely initialized in a limited number of time frames. The underlying principle of our methods is a maximization formalism using formal optimization techniques based on satisfiability solvers (MaxSAT). We introduce several heuristics which increase the scalability of our approach significantly. Experimental results demonstrate the applicability of the method for large academic and industrial benchmark circuits with up to a few hundred thousand gates. Nils Jansen, Florian Corzilius, Matthias Volk, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen, Bernd BeckerAccelerating Parametric Probabilistic Verification 2014 Int'l Conf. on Quantitative Evaluation of Systems (QEST) , Springer-Verlag, Band : 8657, Seite : 404-420» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We present a novel method for computing reachability probabilities of parametric discrete-time Markov chains whose transition probabilities are fractions of polynomials over a set of parameters. Our algorithm is based on two key ingredients: a graph decomposition into strongly connected subgraphs combined with a novel factorization strategy for polynomials. Experimental evaluations show that these approaches can lead to a speed-up of up to several orders of magnitude in comparison to existing approaches. Tobias Schubert, Marc Pfeifer, Bernd BeckerAccurate Controlling of Velocity on a Mobile Robot 2014 29th International Conference on Computers and Their Applications Andreas Riefert, Lyl Ciganda, Matthias Sauer, Paolo Bernadi, Matteo Sonza Reorda, Bernd BeckerAn Effective Approach to Automatic Functional Processor Test Generation for Small-Delay Faults 2014 Conf. on Design, Automation and Test in Europe » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Functional microprocessor test methods provide several advantages compared to DFT approaches, like reduced chip cost and at-speed execution. However, the automatic generation of functional test patterns is an open issue. In this work we present an approach for the automatic generation of functional microprocessor test sequences for small-delay faults based on Bounded Model Checking. We utilize an ATPG framework for small-delay faults in sequential, non-scan circuits and propose a method for constraining the input space for generating functional test sequences (i.e., test programs). We verify our approach by evaluating the miniMIPS microprocessor. In our experiments we were able to reach over 97 % fault efficiency. To the best of our knowledge, this is the first fully automated approach to functional microprocessor test for small-delay faults. Sreedhar Saseendran Kumar, Jan Wülfing, Joschka Boedecker, Ralf Wimmer, Martin Riedmiller, Bernd Becker, Ulrich EgertAutonomous Control of Network Activity 2014 9th International Meeting on Substrate-Integrated Microelectrode Arrays (MEA) » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Electrical stimulation of the brain is used to treat neurological disorders. Yet it is unknown how to find stimulation patterns that produce desired results with the least interference. Towards this goal, we tested a generic closed-loop paradigm that autonomously optimizes stimulation settings. We used neuronal networks coupled to a reinforcement learning based controller to maximize response lengths. Erika Ábrahám, Bernd Becker, Christian Dehnert, Nils Jansen, Joost-Pieter Katoen, Ralf WimmerCounterexample Generation for Discrete-Time Markov Models: An Introductory Survey In : International School on Formal Methods for the Design of Computer, Communication, and Software Systems (SFM), Advanced Lectures 2014, Springer-Verlag , Seiten : 65 - 121, » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung This paper is an introductory survey of available methods for the computation and representation of probabilistic counterexamples for discrete-time Markov chains and probabilistic automata. In contrast to traditional model checking, probabilistic counterexamples are sets of finite paths with a critical probability mass. Such counterexamples are not obtained as a by-product of model checking, but by dedicated algorithms. We define what probabilistic counterexamples are and present approaches how they can be generated. We discuss methods based on path enumeration, the computation of critical subsystems, and the generation of critical command sets, both, using explicit and symbolic techniques. Dominik Erb, Karsten Scheibler, Matthias Sauer, Bernd BeckerEfficient SMT-based ATPG for Interconnect Open Defects 2014 Conf. on Design, Automation and Test in Europe » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Interconnect opens are known to be one of the predominant
defects in nanoscale technologies. However, automatic test
pattern generation for open faults is challenging, because of their
rather unstable behaviour and the numerous electric parameters
which need to be considered. Thus, most approaches try to avoid
accurate modeling of all constraints and use simplified fault models
in order to detect as many faults as possible or make assumptions
which decrease both complexity and accuracy.
This paper presents a new SMT-based approach which for the
first time supports the Robust Enhanced Aggressor Victim model
without restrictions and handles oscillations. It is combined with the
first open fault simulator fully supporting the Robust Enhanced Aggressor
Victim model and thereby accurately considering unknown
values. Experimental results show the high efficiency of the new
method outperforming previous approaches by up to two orders of
magnitude. Dominik Erb, Michael Koche, Matthias Sauer, Stefan Hillebrecht, Tobias Schubert, Hans-Joachim Wunderlich, Bernd BeckerExact Logic and Fault Simulation in Presence of Unknowns 2014 ACM Transactions on Design Automation of Electronic Systems (TODAES) , Band : 19, Seiten : 28:1 - 28:17» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Logic and fault simulation are essential tools in electronic design automation. The accuracy of standard
simulation algorithms is compromised by unknown or X-values. This results in a pessimistic overestimation
of X-valued signals in the circuit, and a pessimistic underestimation of fault coverage.
This work proposes efficient algorithms for combinational and sequential logic as well as for stuck-at and
transition-delay fault simulation which are free of any simulation pessimism in presence of unknowns. The
SAT-based algorithms exactly classifiy all signal states. During fault simulation, each fault is accurately
classified as either undetected, definitely detected or possibly detected.
The pessimism w. r. t. unknowns present in classic algorithms is thoroughly investigated in the experimental
results on benchmark circuits. The applicability of the proposed algorithms is demonstrated on
larger industrial circuits. The results show, that by accurate analysis the number of detected faults can be
significantly increased without increasing the test set size. Linus Feiten, Andreas Spilla, Matthias Sauer, Tobias Schubert, Bernd BeckerImplementation and Analysis of Ring Oscillator PUFs on 60 nm Altera Cyclone FPGAs 2014 Information Security Journal: A Global Perspective , Band : 22, Nummer : 5-6, Seiten : 265 - 273» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Ring Oscillator (RO) physically unclonable functions (PUFs) on field programmable gate arrays (FPGAs) have drawn much attention in recent years. Making each FPGA uniquely identifiable, they allow for protection of intellectual property (IP) or generation of secret encryption keys. Their implementation has been widely discussed, but most experiments have been conducted on Xilinx platforms. In this paper, we report the statistical results from an analysis spanning 20 Cyclone IV FPGAs with 60 nm technology. We parameterize the RO length, placement, ambient temperature, and non-PUF switching activity and discuss the observed effects on PUF quality. Karsten Scheibler, Bernd BeckerImplication Graph Compression inside the SMT Solver iSAT3 2014 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung The iSAT algorithm aims at solving boolean combinations of linear and non-linear arithmetic constraint formulas (including transcendental functions), and thus is suitable to verify safety properties of systems consisting of both, linear and non-linear behaviour. The iSAT algorithm tightly integrates interval constraint propagation into the conflict-driven clause-learning framework. During the solving process, this may result in a huge implication graph. This paper presents a method to compress the implication graph on-the-fly. Experiments demonstrate that this method is able to reduce the overall memory footprint up to an order of magnitude. Bettina Braitling, Luis María Ferrer Fioriti, Hassan Hatefi, Ralf Wimmer, Bernd Becker, Holger HermannsMeGARA: Menu-based Game Abstraction and Abstraction Refinement of Markov Automata
2014 International Workshop on Quantitative Aspects of Programming Languages and Systems , Band : EPTCS» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Markov automata combine continuous time, probabilistic transitions, and nondeterminism in a single model. They represent an important and powerful way to model a wide range of complex real-life systems. However, such models tend to be large and difficult to handle, making abstraction and abstraction refinement necessary. In this paper we present an abstraction and abstraction refinement technique for Markov automata, based on the game-based and menu-based abstraction of Markov decision processes. First experiments show that a significant reduction in size is possible using
abstraction. Ralf Wimmer, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen, Bernd BeckerMinimal Counterexamples for Linear-Time Probabilistic Verification 2014 Theor Comput Sci » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Counterexamples for property violations have a number of important applications like supporting the debugging of erroneous systems and verifying large systems via counterexample-guided abstraction refinement. In this paper, we propose the usage of minimal critical subsystems of discrete-time Markov chains and Markov decision processes as counterexamples for violated omega-regular properties. Minimality can thereby be defined in terms of the number of states or transitions. This problem is known to be NP-complete for Markov decision processes. We show how to compute such subsystems using mixed integer linear programming and evaluate the practical applicability in a number of experiments. They show that our method yields substantially smaller counterexample than using existing techniques. Nils Jansen, Ralf Wimmer, Erika Ábrahám, Barna Zajzon, Joost-Pieter Katoen, Bernd Becker, Johann SchusterSymbolic Counterexample Generation for Large Discrete-Time Markov Chains 2014 Sci Comput Program , Band : 91, Nummer : A, Seiten : 90 - 114» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung This paper presents several symbolic counterexample generation algorithms for discrete-time Markov chains (DTMCs) violating a PCTL formula. A counterexample is (a symbolic representation of) a sub-DTMC that is incrementally generated. The crux to this incremental approach is the symbolic generation of paths that belong to the counterexample. We consider two approaches. First, we extend bounded model checking and develop a simple heuristic to generate highly probable paths first. We then complement the SAT-based approach by a fully (multi-terminal) BDD-based technique. All symbolic approaches are implemented, and our experimental results show a substantially better scalability than existing explicit techniques. In particular, our BDD-based approach using a method called fragment search allows for counterexample generation for DTMCs with billions of states (up to 10^{15}). Dominik Erb, Karsten Scheibler, Michael Kochte, Matthias Sauer, Hans-Joachim Wunderlich, Bernd BeckerTest Pattern Generation in Presence of Unknown Values
Based on Restricted Symbolic Logic 2014 Int'l Test Conf. » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Test generation algorithms based on standard n-
valued logic algebras are pessimistic in presence of unknown
values, overestimate the number of signals with X-values and
underestimate fault coverage.
Recently, an ATPG algorithm based on quantified Boolean
formula (QBF) has been presented, which is accurate in presence
of X-values but has limits with respect to runtime, scalability and
robustness.
In this paper, we consider ATPG based on restricted symbolic
logic (RSL) and demonstrate its potential. We introduce a
complete RSL ATPG exploiting the full potential of RSL in ATPG.
Experimental results demonstrate that RSL ATPG significantly
increases fault coverage over classical algorithms and provides
results very close to the accurate QBF-based algorithm. An
optimized version of RSL ATPG (together with accurate fault
simulation) is up to 618x faster than the QBF-based solution,
more scalable and more robust. Karsten Scheibler, Bernd BeckerUsing Interval Constraint Propagation for Pseudo-Boolean Constraint Solving 2014 Formal Methods in Computer-Aided Design » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung This work is motivated by (1) a practical application which automatically generates test patterns for integrated circuits and (2) the observation that off-the-shelf state-of-the-art pseudo-Boolean solvers have difficulties in solving instances with huge pseudo-Boolean constraints as created by our application.
Derived from the SMT solver iSAT3 we present the solver iSAT3p that on the one hand allows the efficient handling of huge pseudo-Boolean constraints with several thousand summands and large integer coefficients. On the other hand, experimental results demonstrate that at the same time iSAT3p is competitive or even superior to other solvers on standard pseudo-Boolean benchmark families. Sven Reimer, Matthias Sauer, Tobias Schubert, Bernd BeckerUsing MaxBMC for Pareto-Optimal Circuit Initialization
2014 Conf. on Design, Automation and Test in Europe » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In this paper we present MaxBMC, a novel formalism for solving optimization problems in sequential systems. Our approach combines techniques from symbolic SAT-based Bounded Model Checking (BMC) and incremental MaxSAT, leading to the first MaxBMC solver. In traditional BMC safety and liveness properties are validated. We extend this formalism: in case the required property is satisfied, an optimization problem is defined to maximize the quality of the reached witnesses. Further, we compare its qualities in different depths of the system, leading to Pareto-optimal solutions. We state a sound and complete algorithm that not only tackles the optimization problem but moreover verifies whether a global optimum has been identified by using a complete BMC solver as back-end. As a first reference application we present the problem of circuit initialization. Additionally, we give pointers to other tasks which can be covered by our formalism quite naturally and further demonstrate the efficiency and effectiveness of our approach. nach oben zur Jahresübersicht Linus Feiten, Katrin Weber, Bernd BeckerSMILE: Smartphones in der Lehre – ein Rück- und Überblick 2013 INFORMATIK 2013 Gesellschaft für Informatik (GI) , Matthias Horbach, Band : P-220, Seiten : 255 - 269» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Bei SMILE handelt es sich um ein Projekt, das im Wintersemester 2010 gestartet wurde. Sein fortlaufendes Ziel ist die Erforschung von Möglichkeiten, die universitäre Lehre - insbesondere Vorlesungen mit über hundert Studierenden - durch den Einsatz von IT zu bereichern. Hierfür wurden Apps für Studierende und Dozierenden entwickelt, die auf allen gängigen Geräten laufen. Die konzeptionelle Planung liegt bei einem interdisziplinären Team aus Informatikern und Instructional Designern; für die Implementierung wird eng mit einem studentischen Entwicklerteam zusammen gearbeitet. Zwei Preisauszeichnungen zeigen die positive Resonanz, die SMILE bisher hervor gerufen hat. Im Sommersemester 2013 wird SMILE zum vierten Mal in einer größeren Vorlesung eingesetzt. In diesem Workshop-Paper beschreiben wir den bisherigen Verlauf des Projekts und die Kernfunktionalitäten der Software. Tobias Schubert, Jan Burchard, Matthias Sauer, Bernd BeckerS-Trike: A Mobile Robot Platform for Higher Education 2013 International Conference on Computer Applications in Industry and Engineering , Seiten : 243 - 248 Linus Feiten, Andreas Spilla, Matthias Sauer, Tobias Schubert, Bernd BeckerAnalysis of Ring Oscillator PUFs on 60nm FPGAs 2013 TRUDEVICE Workshop, Avignon » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In hardware security and trusted computing it is often desired to uniquely and unambiguously identify a device among several others of the same brand. Physically unclonable functions (PUFs) take advantage of subtle variations in the devices' production process to achieve this. A ring oscillator (RO) PUF exploits differing time delays of circuits to yield a unique response from each device.
The implementation of RO PUFs on FPGAs has been widely discussed but most experiments have been conducted on Xilinx FPGAs. In this paper we are reporting statistical results from an analysis spanning 20 equivalent Altera FPGAs. The presented results include the PUF quality's dependency on different parameters like RO length and placement on the FPGA. We identify the optimal RO length of 16 Logic Elements (LE) and show some specific placement cases for which the otherwise very good PUF quality decreases drastically. Linus Feiten, Matthias Sauer, Tobias Schubert, Alexander Czutro, Victor Tomashevich, Eberhard Böhl, Ilia Polian, Bernd Becker#SAT for Vulnerability Analysis of Security Components 2013 (Workshop-Paper, Informal Proceedings) IEEE European Test Symposium » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Vulnerability to malicious fault attacks is an emerging concern for hardware circuits that process sensitive data.We describe a new methodology to assess the vulnerability to such attacks, taking into account built-in protection mechanisms. Our method is based on accurate modeling of fault effects and their detection status expressed as Boolean satisfiability (SAT) formulae. Vulnerability is quantified based on the number of solutions of such formulae, which are computed by an eficient #SAT solver. We demonstrate the applicability of this method by analyzing a sequential pseudo random number generator and a combinatorial multiplier circuit both protected by robust error-detecting codes. Ulrich Loup, Karsten Scheibler, Florian Corzilius, Erika Ábrahám, Bernd BeckerA Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition 2013 CADE , Springer, Band : 7898, Seiten : 193 - 207» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We present a novel decision procedure for non-linear real arithmetic: a combination of iSAT, an incomplete SMT solver based on interval constraint propagation (ICP), and an implementation of the complete cylindrical algebraic decomposition (CAD) method in the library GiNaCRA. While iSAT is efficient in finding unsatisfiability, on satisfiable instances it often terminates with an interval box whose satisfiability status is unknown to iSAT. The CAD method, in turn, always terminates with a satisfiability result. However, it has to traverse a double-exponentially large search space.
A symbiosis of iSAT and CAD combines the advantages of both methods resulting in a fast and complete solver. In particular, the interval box determined by iSAT provides precious extra information to guide the CAD-method search routine: We use the interval box to prune the CAD search space in both phases, the projection and the construction phase, forming a search `tube' rather than a search tree. This proves to be particularly beneficial for a CAD implementation designed to search a satisfying assignment pointedly, as opposed to search and exclude conflicting regions. Benjamin Andres, Matthias Sauer, Martin Gebser, Tobias Schubert, Bernd Becker, Torsten SchaubAccurate Computation of Sensitizable Paths using Answer Set Programming 2013 Int. Conf. on Logic Programming and Nonmonotonic Reasoning , Seiten : 92 - 101» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Precise knowledge of the longest sensitizable paths in a circuit is crucial for various tasks in computer-aided design, including timing analysis, performance optimization, delay testing, and speed binning. As delays in today’s nanoscale technologies are increasingly affected by statistical parameter variations, there is significant interest in obtaining sets of paths that are within a length range. For instance, such path sets can be used in the emerging areas of Post-silicon validation and characterization and Adaptive Test. We present an ASP-based method for computing well-defined sets of sensitizable paths within a length range. Unlike previous approaches, the method is accurate and does not rely on a priori relaxations. Experimental results demonstrate the applicability and scalability of our method. Dominik Erb, Michael A Kochte, Matthias Sauer, Hans-Joachim Wunderlich, Bernd BeckerAccurate Multi-Cycle ATPG in Presence of X-Values 2013 22nd IEEE Asian Test Symposium (ATS) » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Unknown (X) values in a circuit impair test quality and increase test costs. Classical n-valued algorithms for fault simulation and ATPG, which typically use a three- or four-valued logic for the good and faulty circuit, are in principle pessimistic in presence of X-values and cannot accurately compute the achievable fault coverage. In partial scan or pipelined circuits, X-values originate in non-scan flip-flops. These circuits are tested using multi-cycle tests. Here we present multi-cycle test generation techniques for circuits with X-values due to partial scan or other X-sources. The proposed techniques have been integrated into a multi-cycle ATPG framework which employs formal Boolean and quantified Boolean (QBF) satisfiability techniques to compute the possible signal states in the circuit accurately. Efficient encoding of the problem instance ensures reasonable runtimes. We show that in presence of X-values, the detection of stuck-at faults requires not only exact formal reasoning in a single cycle, but especially the consideration of multiple cycles for excitation of the fault site as well as propagation and controlled reconvergence of fault effects. For the first time, accurate deterministic ATPG for multi-cycle test application is supported for stuck-at faults. Experiments on ISCAS'89 and industrial circuits with X-sources show that this new approach increases the fault coverage considerably. Stefan Hillebrecht, Michael A. Kochte, Dominik Erb, Hans-Joachim Wunderlich, Bernd BeckerAccurate QBF-based test pattern generation in presence of unknown values 2013 Conf. on Design, Automation and Test in Europe » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Unknown (X) values may emerge during the design
process as well as during system operation and test application.
Sources of X-values are for example black boxes, clockdomain
boundaries, analog-to-digital converters, or uncontrolled
or uninitialized sequential elements.
To compute a detecting pattern for a given stuck-at fault,
well defined logic values are required both for fault activation
as well as for fault effect propagation to observing outputs. In
presence of X-values, classical test generation algorithms, based
on topological algorithms or formal Boolean satisfiability (SAT)
or BDD-based reasoning, may fail to generate testing patterns
or to prove faults untestable.
This work proposes the first efficient stuck-at fault ATPG
algorithm able to prove testability or untestability of faults in
presence of X-values. It overcomes the principal inaccuracy and
pessimism of classical algorithms when X-values are considered.
This accuracy is achieved by mapping the test generation problem
to an instance of quantified Boolean formula (QBF) satisfiability.
The resulting improvement of fault coverage is shown on experimental
results based on ISCAS benchmark and larger industrial
circuits. Matthias Sauer, Sven Reimer, Stefan Kupferschmid, Tobias Schubert, Paolo Marin, Bernd BeckerApplying BMC, Craig Interpolation and MAX-SAT to Functional Justification in Sequential Circuits 2013 RCRA International Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We present an approach to identify functional input sequences
in sequential circuits. The properties required are inserted as target of
a bounded model checking (BMC) problem, by using Craig interpolants
it can be stated whether sequences justifying the properties exist or
not. The initial state is either completely or partially unknown, and for
the latter we engage a MAX-SAT formulation to retrieve the shortest
sequence if a maximal subset of the initial state bits are unknown.
We apply this method to problems arising from digital circuit testing
domain, in which usually an arbitrary initial state is assumed, i.e., that
the circuit’s sequential elements (ﬂip-ﬂops) are assumed to be fully con-
trollable. However, since some of these states may be unreachable during
normal operation, this results in undesired secondary test conditions.
In this paper BMC is used to (1) test timing faults in a digital circuit,
thereby the test requirements are encoded as target properties. Our
method yields the shortest functional test-sequences that justify the target
properties or it proves that such a sequence does not exist. Furthermore,
(2) the initialization of circuits is considered. We analyze the length of
such sequences depending on the number of controllable ﬂip-ﬂops. Karsten Scheibler, Matthias Sauer, Kohei Miyase, Bernd BeckerControlling Small-Delay Test Power Consumption using Satisfibility Modulo Theory Solving 2013 GI/ITG Workshop “Testmethoden und Zuverlässigkeit von Schaltungen und Systemen” » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Exaggerated power consumption during test mode is a major issue in today's nanoscale circuits and can lead to a significant amount of overtesting and hence yield loss. We present a method that yields two-pattern tests sensitizing long paths while at the same time minimizing weighted switching activity. Experimental results on standard benchmark circuits demonstrate the applicability of the method. Young Moon Kim, Jun Seomun, Hyung-Ock Kim, Kyung Tae Do, Jung Yun Choi, Kee Sup Kim, Matthias Sauer, Bernd Becker, Subhasish MitraDetection of early-life failures in high-K metal-gate transistors and ultra low-K inter-metal dielectrics 2013 Custom Integrated Circuits Conference , Seiten : 1 - 4» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Using 28nm test chips, we derive signatures for
early-life failures (ELF) in both high-K/metal-gate transistors
and ultra low-K inter-metal dielectrics. We also demonstrate
that the derived ELF signatures can be successfully detected
using a clock control technique. Our results can be utilized to
overcome scaled-CMOS reliability challenges in several ways: 1.
Low-cost ELF detection during on-line operation of robust
systems without requiring expensive redundancy-based error
detection techniques; 2. Effective ELF screening during
production test while reducing stress time and/or stress levels
associated with stress tests such as burn-in. Matthias Sauer, Young Moon Kim, Jun Seomun, Hyung-Ock Kim, Kyung-Tae Do, Jung Yun Choi, Kee Sup Kim, Subhasish Mitra, Bernd BeckerEarly-Life-Failure Detection using SAT-based ATPG 2013 Int'l Test Conf. , Seiten : 1 - 10» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Early-life failures (ELF) result from weak chips that may pass manufacturing tests but fail early in the field, much earlier than expected product lifetime. Recent experimental studies over a range of technologies have demonstrated that ELF defects result in changes in delays over time inside internal nodes of a logic circuit before functional failure occurs. Such changes in delays are distinct from delay degradation caused by circuit aging mechanisms such as Bias Temperature Instability. Traditional transition fault or robust path delay fault test patterns are inadequate for detecting such ELF-induced changes in delays because they do not model the demanding detection conditions precisely. In this paper, we present an automatic test pattern generation (ATPG) technique based on Boolean Satisfiability (SAT) for detecting ELF-induced delay changes at all gates in a given circuit. Our simulation results, using various circuit blocks from the industrial OpenSPARC T2 design as well as standard benchmarks, demonstrate the effectiveness and practicality of our approach in achieving high coverage of ELF-induced delay change detection. We also demonstrate the robustness of our approach to manufacturing process variations. Matthias Sauer, Sven Reimer, Tobias Schubert, Ilia Polian, Bernd BeckerEfficient SAT-Based Dynamic Compaction and Relaxation for Longest Sensitizable Paths 2013 Conf. on Design, Automation and Test in Europe , Seiten : 448 - 453» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Comprehensive coverage of small-delay faults under massive process variations is achieved when multiple paths through the fault locations are sensitized by the test pair set. Using one test pair per path may lead to impractical test set sizes and test application times due to the large number of near-critical paths in state-of-the-art circuits. Karina Gitina, Sven Reimer, Matthias Sauer, Ralf Wimmer, Christoph Scholl, Bernd BeckerEquivalence Checking for Partial Implementations Revisited 2013 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” , Universität Rostock ITMZ, Seiten : 61 - 70» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In this paper we consider the problem of checking whether a partial implementation can (still) be extended to a complete design which is equivalent to a given full specification. In particular, we investigate the relationship between the equivalence checking problem for partial implementations (PEC) and the validity problem for quantified boolean formulae (QBF) with so-called Henkin quantifiers. Our analysis leads us to a sound and complete algorithmic solution to the PEC problem as well as to an exact complexity theoretical classification of the problem. Karina Gitina, Sven Reimer, Matthias Sauer, Ralf Wimmer, Christoph Scholl, Bernd BeckerEquivalence Checking of Partial Designs using Dependency Quantified Boolean Formulae 2013 Int'l Conf. on Computer Design , IEEE Computer Society, Seiten : 396 - 403» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We consider the partial equivalence checking problem (PEC), i.e., checking whether a given partial implementation of a combinational circuit can (still) be extended to a complete design that is equivalent to a given full specification. To solve PEC, we give a linear transformation from PEC to the question whether a dependency quantified Boolean formula (DQBF) is satisfied.
Our novel algorithm to solve DQBF based on quantifier elimination can therefore be applied to solve PEC. We also present first experimental results showing the feasibility of our approach and the inaccuracy of QBF approximations, which are usually used for deciding the PEC so far. Katrin Weber, Bernd BeckerFormative Evaluation des mobilen Classroom-Response-Systems SMILE 2013 GMW 2013 eLearing , Seiten : 277 - 289» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Bezug nehmend auf das Hauptziel von Classroom-Response-Systems (CRS) – der Förderung der Interaktion in Massenlehrveranstaltungen – wird im vorliegenden Beitrag die Evaluation eines mobilen CRS namens SMILE dargestellt und diskutiert. Die Ergebnisse zeigen, dass die Funktionalitäten der SMILE-App – Live-Feedback, Quiz-Fragen und Question&Answer – von den Studierenden der Pilotvorlesung unterschiedlich häufig genutzt wurden. Darüber hinaus wurden die Akzeptanz der Studierenden gegenüber dem Einsatz des Tools und die Wirkung der Quiz-Fragen untersucht. Es zeigt sich, dass Schwächen der technischen Ausstattung im Hörsaal und die technische Zuverlässigkeit der SMILE-App wesentliche Einflussfaktoren auf die Nutzungshäufigkeit sein könnten. Im Sinne einer formativen Evaluation konnten nicht nur technische Problembereiche identifiziert werden, sondern auch Ableitungen für das didaktische Konzept der SMILE-unterstützten Vorlesungen gemacht werden. Ralf Wimmer, Nils Jansen, Andreas Vorpahl, Erika Ábrahám, Joost-Pieter Katoen, Bernd BeckerHigh-Level Counterexamples for Probabilistic Automata 2013 Springer-Verlag, Band : 8054, Seiten : 18 - 33» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Providing compact and understandable counterexamples for violated
system properties is an essential task in model checking. Existing
works on counterexamples for probabilistic systems so far computed
either a large set of system runs or a subset of the system's
states, both of which are of limited use in manual debugging. Many
probabilistic systems are described in a guarded command language
like the one used by the popular model checker \texttt{PRISM}. In this
paper we describe how a minimal subset of the commands can be
identified which together already make the system erroneous. We
additionally show how the selected commands can be further
simplified to obtain a well-understandable counterexample. Ralf Wimmer, Nils Jansen, Andreas Vorpahl, Erika Ábrahám, Joost-Pieter Katoen, Bernd BeckerHigh-Level Counterexamples for Probabilistic Automata , Band : arxiv:1305.5055, 2013 Andreas Riefert, Joerg Mueller, Matthias Sauer, Wolfram Burgard, Bernd BeckerIdentification of Critical Variables using an FPGA-based Fault Injection Framework 2013 GI/ITG Workshop “Testmethoden und Zuverlässigkeit von Schaltungen und Systemen” Andreas Riefert, Joerg Mueller, Matthias Sauer, Wolfram Burgard, Bernd BeckerIdentification of Critical Variables using an FPGA-based Fault Injection Framework 2013 VLSI Test Symp. , Seiten : 1 - 6» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung The shrinking nanometer technologies of modern microprocessors and the aggressive supply voltage down-scaling drastically increase the risk of soft errors. In order to cope with this risk efficiently, selective hardware and software protection schemes are applied. In this paper, we propose an FPGA-based fault injection framework which is able to identify the most critical registers of an entire microprocessor. Further-more, our framework identifies critical variables in the source code of an arbitrary application running in its native environment. We verify the feasibility and relevance of our approach by implementing a lightweight and efficient error correction mechanism protecting only the most critical parts of the system. Experimental results with state estimation applications demonstrate a significantly reduced number of critical calculation errors caused by faults injected into the processor. Matthias Sauer, Sven Reimer, Ilia Polian, Tobias Schubert, Bernd BeckerProvably Optimal Test Cube Generation Using Quantified Boolean Formula Solving 2013 ASP Design Automation Conf. » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Circuits that employ test pattern compression rely on test cubes to achieve high compression ratios. The less inputs of a test pattern are specified, the better it can be compacted and hence the lower the test application time. Although there exist previous approaches to generate such test cubes, none of them are optimal. We present for the first time a framework that yields provably optimal test cubes by using the theory of quantified Boolean formulas (QBF). Extensive comparisons with previous methods demonstrate the quality gain of the proposed method. Karsten Scheibler, Stefan Kupferschmid, Bernd BeckerRecent Improvements in the SMT Solver iSAT 2013 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Over the past decades embedded systems have become more and more complex. Furthermore, besides digital components they now often contain additional analog parts -- making them to embedded hybrid systems. If such systems are used in safety critical environments, a formal correctness proof is highly desirable. The SMT solver iSAT aims at solving boolean combinations of linear and non-linear constraint formulas (including transcendental functions), and thus is suitable to verify safety properties of systems consisting of both, linear and non-linear behaviour. To keep up with the ever increasing complexity of these systems we present recent improvements in various parts of iSAT. Experiments demonstrate that iSAT with all the presented improvements integrated typically gains a speedup between one and two orders of magnitude. Matthias Sauer, Alexander Czutro, Tobias Schubert, Stefan Hillebrecht, Ilia Polian, Bernd BeckerSAT-based Analysis of Sensitisable Paths 2013 IEEE Design & Test of Computers , Band : 30, Nummer : 4, Seiten : 81 - 88» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung A common trend in the past has been to detect delay defects in nanoscale technologies through the longest sensitisable paths. This approach does not hold up for non-trivial defects due to modeling inaccuracies. This article supports tests through all paths of customized length, using current SAT-solving advances. Kohei Miyase, Matthias Sauer, Bernd Becker, Xiaoqing Wen, Seiji KajiharaSearch Space Reduction for Low-Power Test Generation 2013 22nd IEEE Asian Test Symposium (ATS) » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Ongoing research to shrink feature sizes of LSI circuits leads to an always increasing number of logic gates in a circuit. In general, the complexity of test generation depends on the size of a circuit. Furthermore, modern test generation methods have to consider power reduction in addition to fault detection, since excessive power caused by testing may result in over testing. In this work, we propose a method to reduce the computation time of low-power test generation. The proposed method specifies gates which will cause power issues, consequently reducing the search space for X-filling technique. The reduction of search space for Xfilling also further minimizes the amount of switching activity. Experimental results for circuits of Open Cores provided by IWLS2005 benchmarks show that the proposed method achieves both a reduced computation time and at the same time increased power reduction compared to previous methods. Bettina Braitling, Ralf Wimmer, Bernd Becker, Erika ÁbrahámStochastic Bounded Model Checking: Bounded Rewards and Compositionality 2013 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” , Seiten : 243 - 254» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We extend the available SAT/SMT-based methods for generating
counterexamples of probabilistic systems in two ways: First, we
propose bounded rewards, which are appropriate, e. g., to model the
energy consumption of autonomous embedded systems, and show how to
extend the SMT-based counterexample generation to handle such
models. Second, we describe a compositional SAT encoding of the transition
relation of Markov models, which exploits the system structure to
obtain a more compact formula, which in turn can be solved more
efficiently. Preliminary experiments show promising results in both
cases. Matthias Sauer, Jan Burchard, Tobias Schubert, Ilia Polian, Bernd BeckerWaveform-Guided Fault Injection by Clock Manipulation 2013 TRUDEVICE Workshop nach oben zur Jahresübersicht Alexander Czutro, Michael Imhof, Jie Jiang, Abdullah Mumtaz, Matthias Sauer, Bernd Becker, Ilia Polian, Hans-Joachim WunderlichVariation-Aware Fault Grading 2012 IEEE Asian Test Symp. , Seiten : 344 - 349 Christian Miller, Paolo Marin, Bernd BeckerA Dynamic QBF Preprocessing Approach for the Verification of Incomplete Designs
2012 Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion , Band : 19» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Bounded Model Checking (BMC) is a major verification technique for finding errors in sequential circuits by unfolding the design iteratively and converting the BMC instances into Boolean satisfiability (SAT) formulas. When considering incomplete designs (i.e. those containing so-called blackboxes), we need the logic of Quantified Boolean Formulas (QBF) to obtain a precise modeling of the unknown behavior of the blackbox. The incremental nature of the BMC problem can be exploited by means of incremental preprocessing of the QBF formulas. It was shown that applying incremental preprocessing produces smaller QBF formulas, but with the price of moving computation time from the solver to the preprocessor, which can rise significantly. In this paper we show how we can take advantage of incremental preprocessing limiting this inconvenient overhead. We start applying incremental preprocessing, and switch to conventional BMC when the
preprocessing effectiveness does not compensate for the time spent. We present multiple switching heuristics, and evaluate the overall performance by running several state-of-the-art QBF solvers as back-end. Comparing these results to those obtained by standard and incremental BMC procedures it turns out that dynamic preprocessing leads to the best overall performance of the whole verification process. Sven Reimer, Florian Pigorsch, Christoph Scholl, Bernd BeckerEnhanced Integration of QBF Solving Techniques 2012 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” , Seiten : 133 - 143» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In this paper we present a novel QBF solving technique which is based on the integration of a search based (DPLL) and a rewriting based approach: While traversing the search space in a DPLL manner, we iteratively generate many sub-problems, which are handed over to the rewriting method one by one. Instead of just communicating back satisfiability results of the individual sub-problems, we collect as many constraints derived by the rewriting based solver as possible, and transfer them back to the search based solver. This allows not only to prune the current branch, but also to avoid the unnecessary traversal of search paths in different regions of the search tree. We also discuss heuristics to determine suitable switching points between these two methods. We present first promising results that underline the potential of our approach. Linus Feiten, Matthias Sauer, Tobias Schubert, Alexander Czutro, Eberhard Böhl, Ilia Polian, Bernd Becker#SAT-Based Vulnerability Analysis of Security Components -- A Case Study 2012 IEEE International Symposium on Defect and Fault Tolerance (DFT) , Seiten : 49 - 54» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In this paper we describe a new approach to assess a circuit's vulnerability to fault attacks. This is achieved through analysis of the circuit's design specification, making use of modern SAT solving techniques. For each injectable fault, a corresponding SAT instance is generated. Every satisfying solution for such an instance is equivalent to a circuit state and an input assignment for which the fault affcts the circuit's outputs such that the error is not detected by the embedded fault detection. The number of solutions is precisely calculated by a #SAT solver and can be translated into an exact vulnerability measure. We demonstrate the applicability of this method for design space exploration by giving detailed results for various implementations of a deterministic random bit generator. Bernd Becker, Ruediger Ehlers, Matthew Lewis, Paolo MarinALLQBF Solving by Computational Learning 2012 Automated Technology for Verification and Analysis , Springer, Band : 7561, Seiten : 370 - 384» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In the last years, search-based QBF solvers have become essential formany applications in the formal methods domain. The exploitation oftheir reasoning efficiency has however been restricted to applicationsin which a ``satisfiable/unsatisfiable'' answer or one model of anopen quantified Boolean formula suffices as an outcome, whereasapplications in which a compact representation of all models isrequired could not be tackled with QBF solvers so far. In this paper,we describe how computational learning provides a remedy to thisproblem. Our algorithms employ a search-based QBF solver and learn theset of all models of a given open QBF problem in a CNF (conjunctivenormal form), DNF (disjunctive normal form), or CDNF (conjunction ofDNFs) representation. We evaluate our approach experimentally usingbenchmarks from synthesis of finite-state systems from temporal logicand monitor computation. Benjamin Andres, Matthias Sauer, Martin Gebser, Tobias Schubert, Bernd Becker, Torsten SchaubAccurate Computation of Longest Sensitizable Paths using Answer Set Programming 2012 GMM/ITG-Fachtagung “Zuverlässigkeit und Entwurf” Matthias Sauer, Stefan Kupferschmid, Alexander Czutro, Sudhakar M. Reddy, Bernd BeckerAnalysis of Reachable Sensitisable Paths in Sequential Circuits with SAT and Craig Interpolation 2012 Int'l Conf. on VLSI Design » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Test pattern generation for sequential circuits benefits from scanning strategies as these allow the justification of arbitrary circuit states. However, some of these states may be unreachable during normal operation. This results in non-functional operation which may lead to abnormal circuit behaviour and result in over-testing. In this work, we present a versatile approach that combines a highly adaptable SAT-based path-enumeration algorithm with a model-checking solver for invariant properties that relies on the theory of Craig interpolants to prove the unreachability of circuit states. The method enumerates a set of longest sensitisable paths and yields test sequences of minimal length able to sensitise the found paths starting from a given circuit state. We present detailed experimental results on the reach ability of sensitisable paths in ITC 99 circuits. Stefan Hillebrecht, Michael Kochte, Hans-Joachim Wunderlich, Bernd BeckerExact Stuck-at Fault Classification in Presence of Unknowns 2012 IEEE European Test Symp. » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Fault simulation is an essential tool in electronic design automation. The accuracy of the computation of fault coverage in classic n-valued simulation algorithms is compromised by unknown (X) values. This results in a pessimistic underestimation of the coverage, and overestimation of unknown (X) values at the primary and pseudo-primary outputs. This work proposes the first stuck-at fault simulation algorithm free of any simulation pessimism in presence of unknowns. The SAT-based algorithm exactly classifies any fault and distinguishes between definite and possible detects. The pessimism w.r.t. unknowns present in classic algorithms is discussed in the experimental results on ISCAS benchmark and industrial circuits. The applicability of our algorithm to large industrial circuits is demonstrated
Fault simulation is an essential tool in electronic design automation. The accuracy of the computation of fault coverage in classic n-valued simulation algorithms is compromised by unknown (X) values. This results in a pessimistic underestimation of the coverage, and overestimation of unknown (X) values at the primary and pseudo-primary outputs. This work proposes the first stuck-at fault simulation algorithm free of any simulation pessimism in presence of unknowns. The SAT-based algorithm exactly classifies any fault and distinguishes between definite and possible detects. The pessimism w.r.t. unknowns present in classic algorithms is discussed in the experimental results on ISCAS benchmark and industrial circuits. The applicability of our algorithm to large industrial circuits is demonstrated. Matthias Sauer, Stefan Kupferschmid, Alexander Czutro, Ilia Polian, Sudhakar M. Reddy, Bernd BeckerFunctional Justification in Sequential Circuits using SAT and Craig Interpolation 2012 GI/ITG Workshop “Testmethoden und Zuverlässigkeit von Schaltungen und Systemen” Matthias Sauer, Stefan Kupferschmid, Alexander Czutro, Ilia Polian, Sudhakar M. Reddy, Bernd BeckerFunctional Test of Small-Delay Faults using SAT and Craig Interpolation 2012 Int'l Test Conf. , Seiten : 1 - 8» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We present SATSEQ, a timing-aware ATPG system for small-delay faults in non-scan circuits. The tool identifies the longest paths suitable for functional fault propagation and generates the shortest possible sub-sequences per fault. Based on advanced model-checking techniques, SATSEQ provides detection of small-delay faults through the longest functional paths. All test sequences start at the circuit's initial state; therefore, overtesting is avoided. Moreover, potential invalidation of the fault detection is taken into account. Experimental results show high detection and better performance than scan testing in terms of test application time and overtesting-avoidance. Paolo Marin, Christian Miller, Bernd BeckerIncremental QBF Preprocessing for Partial Design Verification - (Poster Presentation) 2012 Int'l Conf. on Theory and Applications of Satisfiability Testing , Springer, Band : 7317, Seiten : 473 - 474» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Bounded Model Checking (BMC) is a major verification method for finding errors in sequential circuits. BMC accomplishes this by iteratively unfolding a circuit k times, adding the negated property, and finally converting the BMC instance into a sequence of satisfiability (SAT) problems. When considering incomplete designs (i.e. those containing so-called blackboxes), we rather need the logic of Quantified Boolean Formulas (QBF) to obtain a more precise modeling of the unknown behavior of the blackbox. Here, we answer the question of unrealizability of a property, where finding a path of length k proves that the property is violated regardless of the implementation of the blackbox. To boost this task, solving blackbox BMC problems incrementally has been shown to be feasible [3], although the restrictions required in the preprocessing phase reduce its effectiveness. In this paper we enhance the verification procedure when using an off-the-shelf QBF solver, through a stronger preprocessing of the QBF formulas applied in an incremental fashion. Ralf Wimmer, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen, Bernd BeckerMinimal Counterexamples for Refuting omega-Regular Properties of Markov Decision Processes AVACS Technical Report , Nummer : 88, 2012 Ralf Wimmer, Bernd Becker, Nils Jansen, Erika Ábrahám, Joost-Pieter KatoenMinimal Critical Subsystems as Counterexamples for omega-Regular DTMC Properties 2012 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” , Verlag Dr. Kovac, Seiten : 169 - 180 Ralf Wimmer, Bernd Becker, Nils Jansen, Erika Ábrahám, Joost-Pieter KatoenMinimal Critical Subsystems for Discrete-Time Markov Models 2012 Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems , Springer-Verlag, Band : 7214, Seiten : 299 - 314» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We propose a new approach to compute counterexamples for violated ω-regular properties of discrete-time Markov chains and Markov decision processes. Whereas most approaches compute a set of system paths as a counterexample, we determine a critical subsystem that already violates the given property. In earlier work we introduced methods to compute such subsystems based on a search for shortest paths. In this paper we use SMT solvers and mixed integer linear programming to determine minimal critical subsystems. Alexander Czutro, Matthias Sauer, Ilia Polian, Bernd BeckerMulti-Conditional ATPG using SAT with Preferences 2012 GI/ITG Workshop “Testmethoden und Zuverlässigkeit von Schaltungen und Systemen” Alexander Czutro, Matthias Sauer, Ilia Polian, Bernd BeckerMulti-Conditional SAT-ATPG for Power-Droop Testing 2012 IEEE European Test Symp. » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Power droop is a non-trivial signal-integrity-related effect triggered by specific power-supply conditions. High-frequency and low-frequency power droop may lead to failure of an IC during application time, but they usually remain undetected by state-of-the-art manufacturing test methods, as the fault excitation imposes particular conditions on global switching activity over several time frames. Hence, ATPG for power-droop test (PD-ATPG) is an extremely hard problem that has not yet been solved optimally. In this paper, we use a SAT-based ATPG engine that employs a mechanism known as SAT-solving with qualitative preferences to generate a solution guaranteed to be optimal for a given set of optimisation criteria, however at the expense of high SAT-solving times. Therefore, a well-balanced set of criteria has to be chosen for the SAT-formulation in order to get as good solutions as possible without rendering the SAT-instances impracticably hard. We explore several strategies and evaluate them experimentally. Jie Jiang, Matthias Sauer, Alexander Czutro, Bernd Becker, Ilia PolianOn the Optimality of K Longest Path Generation Algorithm Under Memory Constraints 2012 Conf. on Design, Automation and Test in Europe , Seiten : 418 - 423» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Adequate coverage of small-delay defects in circuits affected by statistical process variations requires identification and sensitization of multiple paths through potential defect sites. Existing K longest path generation (KLPG) algorithms use a data structure called path store to prune the search space by restricting the number of sub-paths considered at the same time. While this restriction speeds up the KLPG process, the algorithms lose their optimality and do not guarantee that the K longest sensitizable paths are indeed found. We investigate, for the first time, the effects of missing some of the longest paths on the defect coverage. We systematically quantify how setting different limits on the path-store size affects the numbers and relative lengths of identified paths, as well as the run-times of the algorithm. We also introduce a new optimal KLPG algorithm that works iteratively and pinpointedly addresses defect locations for which the path-store size limit has been exceeded in previous iterations. We compare this algorithm with a naïve KLPG approach that achieves optimality by setting the path-store size limit to a very large value. Extensive experiments are reported for 45nm-technology data. Matthias Sauer, Alexander Czutro, Bernd Becker, Ilia PolianOn the Quality of Test Vectors for Post-Silicon Characterization 2012 IEEE European Test Symp. » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Post-silicon validation, i.e., physical characterization of a small number of fabricated circuit instances before start of high-volume manufacturing, has become an essential step in integrated circuit production. Post-silicon validation is required to identify intricate logic or electrical bugs which could not be found during pre-silicon verification. In addition, physical characterization is useful to determine the performance distribution of the manufactured circuit instances and to derive performance yield. Test vectors used for this step are subject to different requirements compared to vectors for simulation-based verification or for manufacturing test. In particular, they must sensitize a very comprehensive set of paths in the circuit, assuming massive variations and possible modeling deficiencies. An inadequate test vector set may result in overly optimistic yield estimates and wrong manufacturing decisions. On the other hand, the size of the test vector set is less important than in verification or manufacturing test. In this paper, we systematically investigate the relationship between the quality of the employed test vectors and the accuracy of yield-performance predictions. We use a highly efficient SAT-based algorithm to generate comprehensive test vector sets based on simple model assumptions and validate these test sets using simulated circuit instances which incorporate effects of process variations. The obtained vector sets can also serve as a basis for adaptive manufacturing test. Alexander Czutro, Matthias Sauer, Tobias Schubert, Ilia Polian, Bernd BeckerSAT-ATPG Using Preferences for Improved Detection of Complex Defect Mechanisms 2012 VLSI Test Symp. » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Failures caused by phenomena such as crosstalk or power-supply noise are gaining in importance in advanced nanoscale technologies. The detection of such complex defects benefits from the satisfaction of certain constraints, for instance justifying specific transitions on neighbouring lines of the defect location. We present a SAT-based ATPG-tool that supports the enhanced conditional multiple-stuck-at fault model (ECMS@). This model can specify multiple fault locations along with a set of hard conditions imposed on arbitrary lines; hard conditions must hold in order for the fault effect to become active. Additionally, optimisation constraints that may be required for best coverage can be specified via a set of soft conditions. The introduced tool justifies as many of these conditions as possible, using a mechanism known as SAT with preferences. Several applications are discussed and evaluated by extensive experimental data. Furthermore, a novel fault-clustering technique is introduced, thanks to which the time required to classify all stuck-at faults in a suite of industrial benchmarks was reduced by up to 65%. Linus Feiten, Manuel Bührer, Sebastian Sester, Bernd BeckerSMILE - SMARTPHONES IN LECTURES - Initiating a Smartphone-based Audience Response System as a Student Project 2012 4th International Conference on Computer Supported Education (CSEDU) , Seiten : 288 - 293» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In this position paper we are presenting the recent progress in developing our audience response system,SMILE, whose aim is to bring more interactivity into academic lectures. Development started in December2010 with a programming task force of undergraduate Computing Science students. The constant integrationof students as developers is a main concept of SMILE. A first prototype included a multiple-choice quizmodule and a slider-based real-time feedback module. The client runs as a native Android-smartphone/tabletapp or as a JavaScript web-browser application on any platform. In the winter semester 2011/2012 we havebeen applying the prototype permanently in a first year Computing Science lecture with approx. 90 attendingstudents. This has been accompanied by a formative evaluation in cooperation with learning psychologists.Final results of the evaluation will be subject to a later publication later. Here we are sharing first tendenciesalready observable and details of the conception and the ongoing development phases. Celia Kändler, Linus Feiten, Katrin Weber, Michael Wiedmann, Manuel Bührer, Sebastian Sester, Bernd BeckerSMILE - smartphones in a university learning environment: a classroom response system 2012 International Conference of the Learning Sciences (ICLS) , International Society of the Learning Sciences, Band : 2, Seiten : 515 - 516» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We describe and evaluate a tool using smartphones in a university learning environment. Mass lectures often lack in interactivity. Due to missing feedback, the lecture’s content may not be adapted to the students' understanding. The tool consists of two modules, a comprehension level visualization and multiple choice questions, that are hypothesized to increase interactivity and adaptation to students' understanding. We report data from a formative evaluation of the tool's first implementation in a university lecture. Matthias Sauer, Alexander Czutro, Ilia Polian, Bernd BeckerSmall-Delay-Fault ATPG with Waveform Accuracy 2012 Int'l Conf. on CAD , Seiten : 30 - 36» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung The detection of small-delay faults is traditionally performed by sensitizing transitions on a path of sufficient length from an input to an output of the circuit going through the fault site. While this approach allows efficient test generation algorithms, it may result in false positives and false negatives as well, i.e. undetected faults are classified as detected or detectable faults are classified as undetectable. We present an automatic test pattern generation algorithm which considers waveforms and their propagation on each relevant line of the circuit. The model incorporates individual delays for each gate and filtering of small glitches. The algorithm is based on an optimized encoding of the test generation problem by a Boolean satisfiability (SAT) instance and is implemented in the tool WaveSAT. Experimental results for ISCAS-85, ITC-99 and industrial circuits show that no known definition of path sensitization can eliminate false positives and false negatives at the same time, thus resulting in inadequate small-delay fault detection. WaveSAT generates a test if the fault is testable and is also capable of automatically generating a formal redundancy proof for undetectable small-delay faults; to the best of our knowledge this is the first such algorithm that is both scalable and complete. Nils Jansen, Erika Ábrahám, Barna Zajzon, Ralf Wimmer, Johann Schuster, Joost-Pieter Katoen, Bernd BeckerSymbolic Counterexample Generation for Discrete-time Markov Chains 2012 Int'l Symp. on Formal Aspects of Component Software , Springer-Verlag, Band : 7684, Seiten : 134 - 151» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In this paper we investigate the generation of counterexamples for discrete-time Markov chains (DTMCs) and PCTL properties. Whereas most available methods use explicit representations for at least some intermediate results, our aim is to develop fully symbolic algorithms. As in most related work, our counterexample computations are based on path search. We first adapt bounded model checking as a path search algorithm and extend it with a novel SAT-solvingheuristics to prefer paths with higher probabilities. As a second approach, we use symbolic graph algorithms to find counterexamples. Experiments show that our approaches, in contrast to other existing techniques, are applicable to very large systems with millions of states. Nils Jansen, Erika Ábrahám, Matthias Volk, Ralf Wimmer, Joost-Pieter Katoen, Bernd BeckerThe COMICS Tool - Computing Minimal Counterexamples for DTMCs 2012 Automated Technology for Verification and Analysis , Springer-Verlag, Band : 7561, Seiten : 349 - 353» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung This paper presents the tool COMICS 1.0, which performs model checking and generates counterexamples for DTMCs. For an input DTMC, COMICS computes an abstract system that carries the model checking information and uses this result to compute a critical subsystem, which induces a counterexample. This abstract subsystem can be refined and concretized hierarchically. The tool comes with a command line version as well as a graphical user interface that allows the user to interactively influence the refinement process of the counterexample. Nils Jansen, Erika Ábrahám, Maik Scheffler, Matthias Volk, Andreas Vorpahl, Ralf Wimmer, Joost-Pieter Katoen, Bernd BeckerThe COMICS Tool - Computing Minimal Counterexamples for DTMCs , Band : arxiv:1206.0603, 2012 Ernst Moritz Hahn, Holger Hermanns, Ralf Wimmer, Bernd BeckerTransient Reward Approximation for Grids, Crowds, and Viruses arXiv , Band : arxiv:1212.1251, 2012 Paolo Marin, Christian Miller, Matthew Lewis, Bernd BeckerVerification of Partial Designs Using Incremental QBF Solving 2012 Conf. on Design, Automation and Test in Europe , Seiten : 623 - 628» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung SAT solving is an indispensable core component of numerous formal verification tools and has found widespread use in industry, in particular when using it in an incremental fashion, e.g. in Bounded Model Checking (BMC). On the other hand, there are applications, in particular in the area of partial design verification, where SAT formulas are not expressive enough and a description via Quantified Boolean Formulas (QBF) is much more adequate.In this paper we introduce incremental QBF solving and thereby make it usable as a core component of BMC. To do so, we realized an incremental version of the state-of-the-art QBF solver QuBE, allowing for the reuse of learnt information e.g. in the form of conflict clauses and solution cubes. As an application we consider BMC for partial designs (i.e. designs containing so-called blackboxes) and thereby disprove realizability, that is, we prove that an unsafe state is reachable no matter how the blackboxes are implemented. In our experimental analysis, we compare different incremental approaches implemented in our BMC tool. BMC with incremental QBF turns out to be feasible for designs with more than 21,000 gates and 2,700 latches. Significant performance gains over non incremental QBF based BMC can be obtained on many benchmark circuits, in particular when using the so-called backward-incremental approach combined with incremental preprocessing. nach oben zur Jahresübersicht Jie Jiang, Matthias Sauer, Alexander Czutro, Bernd Becker, Ilia PolianOn the Optimality of K Longest Path Generation 2011 Workshop on RTL and High Level Testing Matthias Sauer, Alexander Czutro, Ilia Polian, Bernd BeckerEstimation of Component Criticality in Early Design Steps 2011 IEEE Int'l Online Testing Symp. , Seiten : 104 - 110 Christian Miller, Christoph Scholl, Bernd BeckerVerifying Incomplete Networks of Timed Automata 2011 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” , Band : 14» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Verification of real-time systems - e.g. communication protocols or embedded controllers - is an important task. One method to detect errors is called bounded model checking (BMC). In BMC a system is iteratively unfolded and then transformed into a satisfiability problem. If an appropriate solver finds the k-th instance to be satisfiable, a counterexample for a given safety property has been found. In this paper, we present a novel approach to apply BMC to networks of timed automata (i.e. a system of several interacting subautomata) where parts of the network are unspecified (so-called blackboxes). Here, we would like to answer the question of unrealizability, that is, is there a path of a certain length violating a safety property regardless of the implementation of the blackboxes. Focusing on two prevalent communication models for networks of interacting timed automata, we introduce two methods to solve these types of BMC problems. The first is based on fixed transitions, which in some cases is too coarse of an abstraction. In the second approach we prove unrealizability by introducing universal quantification, yielding more advanced quantified SAT-Modulo-Theory formulas. Matthias Sauer, Victor Tomashevich, Jörg Müller, Matthew Lewis, Ilia Polian, Bernd Becker, Wolfram BurgardAn FPGA-Based Framework for Run-time Injection and Analysis of Soft Errors in Microprocessors 2011 IEEE Int'l Online Testing Symp. , Seiten : 182 - 185» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung State-of-the-art cyber-physical systems are increasingly deployed in harsh environments with non-negligible soft error rates, such as aviation or search-and-rescue missions. State-of-the-art nanoscale manufacturing technologies are more vulnerable to soft errors. In this paper, we present an FPGA-based framework for injecting soft errors into user-specified memory elements of an entire microprocessor (MIPS32) running application software. While the framework is applicable to arbitrary software, we demonstrate its usage by characterizing soft errors effects on several software filters used in aviation for probabilistic sensor data fusion. Pepijn Crouzen, Ernst Moritz Hahn, Holger Hermanns, Abhishek Dhama, Oliver Theel, Ralf Wimmer, Bettina Braitling, Bernd BeckerBounded Fairness for Probabilistic Distributed Algorithms 2011 Int'l Conf. on Application of Concurrency to System Design , IEEE Computer Society, Seiten : 89 - 97» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung This paper investigates quantitative dependability metrics for distributed algorithms operating in the presence of sporadic or frequently occurring faults. In particular, we investigate necessary revisions of traditional fairness assumptions in order to arrive at useful metrics, without adding hidden assumptions that may obfuscate their validity. We formulate faulty distributed algorithms as Markov decision processes to incorporate both probabilistic faults and non-determinism arising from concurrent execution. We lift the notion of bounded fairness to the setting of Markov decision processes. Bounded fairness is particularly suited for distributed algorithms running on nearly symmetric infrastructure, as it is common for sensor network applications. Finally, we apply this fairness notion in the quantitative model-checking of several case studies. Christian Miller, Karina Gitina, Bernd BeckerBounded Model Checking of Incomplete Real-time Systems Using Quantified SMT Formulas 2011 Int'l Workshop on Microprocessor Test and Verification , Seiten : 22 - 27» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Verification of real-time systems - e.g. communication protocols or embedded controllers - is an important task. One method to detect errors is bounded model checking (BMC) where the system is iteratively unfolded and transformed into a satisfiability problem. In this paper, we apply BMC to incomplete networks of timed automata, i.e. systems containing so-called black boxes. In this context, we answer the question of unrealizability, that is, is a safety property violated regardless of the implementation of the black boxes. We focus on problems where the error path depends on the behavior of the black boxes such that an encoding using universal quantification is needed. This yields more advanced quantified SMT formulas, which can no longer be solved by conventional SMT solvers. Taking several prevalent communication models into account, we show how to encode the unrealizability problem and present several procedures to solve the resulting quantified SMT formulas efficiently using And-Inverter-Graphs extended by linear constraints over reals. Finally, we give experimental results to show the applicability of our verification methods. Bettina Braitling, Ralf Wimmer, Bernd Becker, Nils Jansen, Erika ÁbrahámCounterexample Generation for Markov Chains using SMT-based Bounded Model Checking 2011 IFIP Int'l Conf. on Formal Methods for Open Object-based Distributed Systems , Springer-Verlag, Band : 6722, Seiten : 75 - 89» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Generation of counterexamples is a highly important task in the model checking process. In contrast to, e.\,g., digital circuits where counterexamples typically consist of a single path leading to a critical state of the system, in the probabilistic setting counterexamples may consist of a large number of paths. In order to be able to handle large systems and to use the capabilities of modern SAT-solvers, bounded model checking (BMC) for discrete-time Markov chains was established.\par In this paper we introduce the usage of SMT-solving over linear real arithmetic for the BMC procedure. SMT-solving, extending SAT with theories in this context on the one hand leads to a convenient way to express conditions on the probability of certain paths and on the other hand allows to handle Markov reward models. We use the former to find paths with high probability first. This leads to more compact counterexamples. We report on some experiments, which show promising results. Stefan Kupferschmid, Bernd BeckerCraig interpolation in the presence of non-linear constraints 2011 Formal Modeling and Analysis of Timed Systems , Springer, Seiten : 240 - 255» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung An increasing number of applications in particular in the verification area leverages Craig interpolation. Craig interpolants (CIs) can be computed for many different theories such as: propositional logic, linear inequalities over the reals, and the combination of the preceding theories with uninterpreted function symbols. To the best of our knowledge all previous tools that provide CIs are addressing decidable theories. With this paper we make Craig interpolation available for an in general undecidable theory that contains Boolean combinations of linear and non-linear constraints including transcendental functions like $\sin(\cdot)$ and $\cos(\cdot)$. Such formulae arise e.g.~during the verification of hybrid systems. We show how the construction rules for CIs can be extended to handle non-linear constraints. To do so, an existing SMT solver based on a close integration of SAT and Interval Constraint Propagation is enhanced to construct CIs on the basis of proof trees. We provide first experimental results demonstrating the usefulness of our approach: With the help of Craig interpolation we succeed in proving safety in cases where the basic solver could not provide a complete answer. Furthermore, we point out the (heuristic) decisions we made to obtain suitable CIs and discuss further possibilities to increase the flexibility of the CI construction. Stefan Kupferschmid, Bernd BeckerCraigsche Interpolation für Boolesche Kombinationen linearer und nichtlinearer Ungleichungen 2011 OFFIS-Institut für Informatik, Seiten : 279 - 288» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Die vorliegende Arbeit behandelt die Berechnung Craigscher Interpolanten für beliebige boolesche Kombinationen linearer und nichtlinearer Gleichungen, einschließlich transzendenter Funktionen wie sin(x) und cos(x). Craigsche Interpolanten sind in der computergestützten Verifikation weit verbreitet und können für viele verschiedene Theorien berechnet werden, zum Beispiel: Aussagenlogik, lineare Arithmetik über rationale Zahlen sowie die Theorie mit uninterpretierten Funktionsymbolen. Nach bestem Wissen berechnen alle uns bekannten Interpolationsprogramme Craigsche Interpolanten für entscheidbare Theorien. In dieser Arbeit stellen wir einen Ansatz vor, der für eine im Allgemeinem nicht entscheidbare Theorie Craigsche Interpolanten berechnen kann. Wir erlauben neben linearen und nichtlinearen Gleichungen auch transzendente Funktionen. Solche Formeln entstehen bei der Analyse und Verifikation hybrider Systeme. Der in dieser Arbeit vorgestellte Ansatz wurde mithilfe des Sat-Modulo-Theorie Solvers iSAT implementiert. Erste Ergebnisse zeigen, dass Craigsche Interpolanten bei der Verifikation solcher Systeme erfolgreich eingesetzt werden können. Matthias Sauer, Jie Jiang, Alexander Czutro, Ilia Polian, Bernd BeckerEfficient SAT-Based Search for Longest Sensitisable Paths 2011 Test Symposium (ATS), 2011 20th Asian , Seiten : 108 - 113» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We present a versatile method that enumerates all or a user-specified number of longest sensitisable paths in the whole circuit or through specific components. The path information can be used for design and test of circuits affected by statistical process variations. The algorithm encodes all aspects of the path search as an instance of the Boolean Satisfiability Problem (SAT), which allows the method not only to benefit from recent advances in SAT-solving technology, but also to avoid some of the drawbacks of previous structural approaches. Experimental results for academic and industrial benchmark circuits demonstrate the method's accuracy and scalability. Nils Jansen, Erika Ábrahám, Jens Katelaan, Ralf Wimmer, Joost-Pieter Katoen, Bernd BeckerHierarchical Counterexamples for Discrete-Time Markov Chains 2011 Int'l Symp. on Automated Technology for Verification and Analysis , Springer-Verlag, Band : 6996, Seiten : 443 - 452» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung This paper introduces a novel counterexample generation approach for the verification of discrete-time Markov chains (DTMCs) with two main advantages: (1) We generate abstract counterexamples which can be refined in a hierarchical manner. (2) We aim at minimizing the number of states involved in the counterexamples, and compute a critical subsystem of the DTMC whose paths form a counterexample. Experiments show that with our approach we can reduce the size of counterexamples and the number of computation steps by several orders of magnitude. Nils Jansen, Erika Ábrahám, Jens Katelaan, Ralf Wimmer, Joost-Pieter Katoen, Bernd BeckerHierarchical Counterexamples for Discrete-Time Markov Chains , Band : AIB-2011-11, 2011 Stefan Kupferschmid, Matthew Lewis, Tobias Schubert, Bernd BeckerIncremental preprocessing methods for use in BMC 2011 Formal Methods in System Design , Band : 39, Seiten : 185 - 204» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Traditional incremental SAT solvers have achieved great success in the domain of Bounded Model Checking (BMC). Recently, modern solvers have introduced advanced preprocessing procedures that have allowed them to obtain high levels of performance. Unfortunately, many preprocessing techniques such as variable and (blocked) clause elimination cannot be directly used in an incremental manner. This work focuses on extending these techniques and Craig interpolation so that they can be used effectively together in incremental SAT solving (in the context of BMC). The techniques introduced here doubled the performance of our BMC solver on both SAT and UNSAT problems. For UNSAT problems, preprocessing had the added advantage that Craig interpolation was able to find the fixed point sooner, reducing the number of incremental SAT iterations. Furthermore, our ideas seem to perform better as the benchmarks become larger, and/or deeper, which is exactly when they are needed. Lastly, our methods can be integrated into other SAT based BMC tools to achieve similar speedups. Sven Reimer, Florian Pigorsch, Christoph Scholl, Bernd BeckerIntegration of Orthogonal QBF Solving Techniques 2011 Conf. on Design, Automation and Test in Europe , Seiten : 149 - 154» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In this paper we present a method for integrating two complementary solving techniques for QBF formulas, i. e. variable elimination based on an AIG-framework and search with DPLL based solving. We develop a sophisticated mechanism for coupling these techniques, enabling the transfer of partial results from the variable elimination part to the search part. This includes the definition of heuristics to (1) determine appropriate points in time to snapshot the current partial result during variable elimination (by estimating its quality) and (2) switch from variable elimination to search-based methods (applied to the best known snapshot) when the progress of variable elimination is supposed to be too slow or when representation sizes grow too fast. We will show in the experimental section that our combined approach is clearly superior to both individual methods run in a stand-alone manner. Moreover, our combined approach significantly outperforms all other state-of-the-art solvers. Ernst Althaus, Bernd Becker, Daniel Dumitriu, Stefan KupferschmidIntegration of an LP solver into interval constraint propagation 2011 Int'l Conf. on Combinatorial optimization and applications , Springer, Seiten : 343 - 356» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung This paper describes the integration of an LP solver into iSAT, a Satisfiability Modulo Theories solver that can solve Boolean combinations of linear and nonlinear constraints. iSAT is a tight integration of the well-known DPLL algorithm and interval constraint propagation allowing it to reason about linear and nonlinear constraints. As interval arithmetic is known to be less efficient on solving linear programs, we will demonstrate how the integration of an LP solver can improve the overall solving performance of iSAT. Matthew Lewis, Paolo Marin, Tobias Schubert, Massimo Narizzano, Bernd Becker, Enrico GiunchigliaParallel QBF Solving with Advanced Knowledge Sharing 2011 Fundamenta Informaticae , Band : 107, Nummer : 2-3, Seiten : 139 - 166» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In this paper we present the parallel QBF Solver PaQuBE. This new solver leverages the additional computational power that can be exploited from modern computer architectures, from pervasive multi-core boxes to clusters and grids, to solve more relevant instances faster than previous generation solvers. Furthermore, PaQuBE's progressive MPI based parallel framework is the first to support advanced knowledge sharing in which solution cubes as well as conflict clauses can be exchanged between solvers. Knowledge sharing plays a critical role in the performance of PaQuBE. However, due to the overhead associated with sending and receiving MPI messages, and the restricted communication/network bandwidth available between solvers, it is essential to optimize not only what information is shared, but the way in which it is shared. In this context, we compare multiple conflict clause and solution cube sharing strategies, and finally show that an adaptive method provides the best overall results. Erika Ábrahám, Tobias Schubert, Bernd Becker, Martin Fränzle, Christian HerdeParallel SAT Solving in Bounded Model Checking 2011 Journal of Logic and Computation , Band : 21, Nummer : 1, Seiten : 5 - 21» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Bounded model checking (BMC) is an incremental refutation technique to search for counterexamples of increasing length. The existence of a counterexample of a fixed length is expressed by a first-order logic formula that is checked for satisfiability using a suitable solver. We apply communicating parallel solvers to check satisfiability of the BMC formulae. In contrast to other parallel solving techniques, our method does not parallelize the satisfiability check of a single formula, but the parallel solvers work on formulae for different counterexample lengths. We adapt the method of constraint sharing and replication of Shtrichman, originally developed for sequential BMC, to the parallel setting. Since the learning mechanism is now parallelized, it is not obvious whether there is a benefit from the concepts of Shtrichman in the parallel setting. We demonstrate on a number of benchmarks that adequate communication between the parallel solvers yields the desired results. Stefan Kupferschmid, Bernd Becker, Tino Teige, Martin FränzleProof Certificates and Non-linear Arithmetic Constraints 2011 IEEE Design and Diagnostics of Electronic Circuits and Systems , Seiten : 429 - 434» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Symbolic methods in computer-aided verification rely heavily on constraint solvers. The correctness and reliability of these solvers are of vital importance in the analysis of safety-critical systems, e.g., in the automotive context. Satisfiabilityresults of a solver can usually be checked by probing the computed solution. This isin general not the case for unsatisfiability results. In this paper, we propose a certification method for unsatisfiability results for mixed Boolean and non-lineararithmetic constraint formulae. Such formulae arise in the analysis of hybrid discrete/continuous systems. Furthermore, we test our approach by enhancing the iSATconstraint solver to generate unsatisfiability proofs, and implemented a tool that can efficiently validate such proofs. Finally, some experimental results showing theeffectiveness of our techniques are given. Ralf Wimmer, Ernst Moritz Hahn, Holger Hermanns, Bernd BeckerReachability Analysis for Incomplete Networks of Markov Decision Processes 2011 Int'l Conf. on Formal Methods and Models for Co-Design , IEEE Computer Society Press, Seiten : 151 - 160» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Assume we have a network of discrete-time Markov decision processes (MDPs) which synchronize via common actions. We investigate how to compute probability measures in case the structure of some of the component MDPs (so-called blackbox MDPs) is not known. We then extend this computation to work on networks of MDPs that share integer data variables of finite domain. We use a protocol which spreads information within a network as a case study to show the feasibility and effectiveness of our approach. Matthias Sauer, Alexander Czutro, Tobias Schubert, Stefan Hillebrecht, Ilia Polian, Bernd BeckerSAT-Based Analysis of Sensitisable Paths 2011 IEEE Design and Diagnostics of Electronic Circuits and Systems , Seiten : 93 - 98» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Manufacturing defects in nanoscale technologies have highly complex timing behaviour that is also affected by process variations. While conventional wisdom suggests that it is optimal to detect a delay defect through the longest sensitisable path, non-trivial defect behaviour along with modelling inaccuracies necessitate consideration of paths of well-controlled length during test generation. We present a generic methodology that yields tests through all sensitisable paths of user-specified length. The resulting tests can be employed within the framework of adaptive testing. The methodology is based on encoding the problem as a Boolean-satisfiability (SAT) instance and thereby leverages recent advances in SAT-solving technology. Bettina Braitling, Ralf Wimmer, Bernd Becker, Nils Jansen, Erika ÁbrahámSMT-based Counterexample Generation for Markov Chains 2011 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” , Offis Oldenburg, Band : 14, Seiten : 19 - 28» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Counterexamples are a highly important feature of the model checking process. In contrast to, e.\,g., digital circuits where counterexamples typically consist of a single path leading to a critical state of the system, in the probabilistic setting, counterexamples may consist of a large number of paths. In order to be able to handle large systems and to use the capabilities of modern SAT-solvers, bounded model checking (BMC) for discrete-time Markov chains was established.In this paper we introduce the usage of SMT-solving over the reals for the BMC procedure. SMT-solving, extending SAT with theories, leads in this context on the one hand to a convenient way to express conditions on the probability of certain paths and on the other hand to handle Markov Reward models. The former can be used to find paths with high probability first. This leads to more compact counterexamples.We report on some experiments, which show promising results. nach oben zur Jahresübersicht Christian Miller, Karina Gitina, Christoph Scholl, Bernd BeckerBounded Model Checking of Incomplete Networks of Timed Automata 2010 Int'l Workshop on Microprocessor Test and Verification , IEEE Computer Society, Band : 11, Seiten : 61 - 66» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Verification of real-time systems - e.g. communication protocols or embedded controllers - is an important task. One method to detect errors is called bounded model checking (BMC). In BMC the system is iteratively unfolded and then transformed into a satisfiability problem. If an appropriate solver finds the k-th instance to be satisfiable a counterexample for a given safety property has been found. In this paper we present a first approach to apply BMC to networks of timed automata (that is a system of several interacting subautomata) where parts of the network are unspecified (so called blackboxes). Here, we would like to answer the question of unrealizability, that is, is there a path of a certain length violating a safety property regardless of the implementation of the blackboxes. We provide solutions to this problem for two timed automata communication models. For the simple synchronization model, a BMC approach based on fixed transitions is introduced resulting in a SAT-Modulo-Theory formula. With respect to the use of bounded integer variables for communication, we prove unrealizability by introducing universal quantification, yielding more advanced quantified SAT-Modulo-Theory formulas. Stefan Kupferschmid, Matthew Lewis, Tobias Schubert, Bernd BeckerIncremental Preprocessing Methods for use in BMC 2010 Int'l Workshop on Hardware Verification » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Traditional incremental SAT solvers have achieved great success in the domain of Bounded Model Checking (BMC). However, modern solvers depend on advanced preprocessing procedures to obtain high levels of performance. Unfortunately,many preprocessing techniques such as a variable and (blocked) clauseelimination cannot be directly used in an incremental manner. This work focuses on extending these techniques and Craig interpolation so that they can be used effectively together in incremental SAT solving (in the context of BMC). The techniques introduced here doubled the performance of our BMC solver onboth SAT and UNSAT problems. For UNSAT problems, preprocessing had the added advantagethat Craig interpolation was able to find the fixed point sooner,reducing the number of incremental SAT iterations. Furthermore, our ideas seem to perform better as the benchmarks become larger, and/or deeper, which is exactly when they are needed. Lastly, our methods can be extended to other SAT based BMC tools to achieve similar speedups. Christian Miller, Stefan Kupferschmid, Bernd BeckerExploiting Craig Interpolants in Bounded Model Checking for Incomplete Designs 2010 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” , Band : 13, Seiten : 77 - 86 Tobias Nopper, Christian Miller, Matthew Lewis, Bernd Becker, Christoph SchollSAT modulo BDD - A Combined Verification Approach for Incomplete Designs 2010 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” , Band : 13, Seiten : 107 - 116 Pepijn Crouzen, Ernst Moritz Hahn, Holger Hermanns, Abhishek Dhama, Oliver Theel, Ralf Wimmer, Bettina Braitling, Bernd BeckerBounded Fairness for Probabilistic Distributed Algorithms AVACS Technical Report , Band : 57, 2010 Ralf Wimmer, Bernd BeckerCorrectness Issues of Symbolic Bisimulation Computation for Markov Chains 2010 Int'l GI/ITG Conference on “Measurement, Modelling and Evaluation of Computing Systems” , Springer-Verlag, Band : 5987, Seiten : 287 - 301» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Bisimulation reduction is a classical means tofight the infamous state space explosion problem, which limits theapplicability of automated methods for verification like modelchecking. A signature-based method, originally developed by Blom andOrzan for labeled transition systems and adapted for Markov chains byDerisavi, has proved to be very efficient. It is possible to implement itsymbolically using binary decision diagrams such that it is able tohandle very large state spaces efficiently. We will show, however,that for Markov chains this algorithm suffers from numericalinstabilities, which often result in too large quotient systems. Wewill present and experimentally evaluate two different approaches toavoid these problems: first the usage of rational arithmetic, andsecond an approach not only to represent the system structure but alsothe transition rates symbolically. In addition, this allows us tomodify their actual values after the quotient computation. Erika Ábrahám, Nils Jansen, Ralf Wimmer, Joost-Pieter Katoen, Bernd BeckerDTMC Model Checking by SCC Reduction 2010 Int'l Conf. on Quantitative Evaluation of Systems , IEEE Computer Society, Seiten : 37 - 46» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Discrete-Time Markov Chains (DTMCs) are a widely-usedformalism to model probabilistic systems. On the one hand, availabletools like \textsc{Prism} or \textsc{Mrmc} offer efficient \emph{modelchecking} algorithms and thus support the verification of DTMCs.However, these algorithms do not provide any diagnostic informationin the form of \emph{counterexamples}, which arehighly important for the correction of erroneous systems. On the otherhand, there exist several approaches to generate counterexamples forDTMCs, but all these approaches require the model checking result forcompleteness.In this paper we introduce a model checking algorithm for DTMCs thatalso supports the generation of counterexamples. Our algorithm,based on the detection and abstraction of strongly connectedcomponents, offers \emph{abstract} counterexamples, which can beinteractively refined by the user. Christian Miller, Stefan Kupferschmid, Matthew Lewis, Bernd BeckerEncoding Techniques, Craig Interpolants and Bounded Model Checking for Incomplete Designs 2010 Theory and Applications of Satisfiability Testing , Springer, Seiten : 194 - 208» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung This paper focuses on bounded invariant checking for partially specified circuits – designs containing so-called blackboxes – using the well known 01X- and QBF-encoding techniques. For detecting counterexamples, modeling the behavior of a blackbox using 01X-encoding is fast, but rather coarse as it limits what problems can be verified. We introduce the idea of 01X-hardness, mainly the classification of problems for which this encoding technique does not provide any useful information about the existence of a counterexample. Furthermore, we provide a proof for 01X-hardness based on Craig interpolation, and show how the information contained within the Craig interpolant or unsat-core can be used to determine heuristically which blackbox outputs to model in a more precise way. We then compare 01X, QBF and multiple hybrid modeling methods. Finally, our total workflow along with multiple state-of-the-art QBF-solvers are shown to perform well on a range of industrial blackbox circuit problems. Natalia Kalinnik, Erika Ábrahám, Tobias Schubert, Ralf Wimmer, Bernd BeckerExploiting Different Strategies for the Parallelization of an SMT Solver 2010 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” , Fraunhofer Verlag, Seiten : 97 - 106» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In this paper we present two different parallelization schemes for the SMT solver iSAT, based on (1) the distribution of work by dividing the search space into disjoint parts and exploring them in parallel, thereby exchanging learnt information, and (2) a portfolio approach, where the entire benchmark instance isexplored in parallel by several copies of the same solver but usingdifferent heuristics to guide the search. We also combine bothapproaches such that solvers examine disjoint parts of the searchspace using different heuristics. The main contribution of the paper is to study the performances of different techniques for parallelizing iSAT. Ilia Polian, Bernd BeckerFault Models and Test Algorithms for Nanoscale Technologies 2010 it - Information Technology , Band : 52, Nummer : 4, Seiten : 189 - 194» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In the age of Nanoscale Integration (NSI), state-of-the-art integrated circuits with gate length under 100 nm consist of hundreds of millions of transistors. This implies new challenges for their reliability. Novel NSI defect mechanisms require special test methods to sort out faulty chips. We present modeling approaches and efficient test algorithms for fundamental NSI defect mechanisms enabling the handling of industrial multi-million-gate circuits. Ralf Wimmer, Bettina Braitling, Bernd Becker, Ernst Moritz Hahn, Pepijn Crouzen, Holger Hermanns, Abhishek Dhama, Oliver TheelSymblicit Calculation of Long-Run Averages for Concurrent Probabilistic Systems 2010 Int'l Conf. on Quantitative Evaluation of Systems , IEEE Computer Society, Seiten : 27 - 36» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Model checkers for concurrent probabilistic systems havebecome very popular within the last decade. The study of long-runaverage behavior has however received only scant attention in thisarea, at least from the implementation perspective. This paperstudies the problem of how to efficiently realize an algorithm forcomputing optimal long-run average reward values for concurrentprobabilistic systems. At its core is a variation of Howard andVeinott's algorithm for Markov decision processes, where symbolicand non-symbolic representations are intertwined in an effectivemanner: the state space is represented using binary decisiondiagrams, while the linear equation systems which have to be solvedfor the induced Markov chains to improve the current scheduler aresolved using an explicit state representation. In order to keep thelatter small, we apply a symbolic bisimulation minimizationalgorithm to the induced Markov chain. The scheduler improvement step itself is again performed on symbolic data structures. Practical evidence shows that the implementation is effective, andsometimes uses considerably less memory than a fully explicitimplementation. Alexander Czutro, Ilia Polian, Matthew Lewis, Piet Engelke, Sudhakar M. Reddy, Bernd BeckerThread-Parallel Integrated Test Pattern Generator Utilizing Satisfiability Analysis 2010 International Journal of Parallel Programming , Band : 38, Nummer : 3-4, Seiten : 185 - 202» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Efficient utilization of the inherent parallelism of multi-core architectures is a grand challenge in the field of electronic design automation (EDA). One EDA algorithm associated with a high computational cost is automatic test pattern generation (ATPG). We present the ATPG tool TIGUAN based on a thread-parallel SAT solver. Due to a tight integration of the SAT engine into the ATPG algorithm and a carefully chosen mix of various optimization techniques, multi-million-gate industrial circuits are handled without aborts. TIGUAN supports both conventional single-stuck-at faults and sophisticated conditional multiple stuck-at faults which allows to generate patterns for non-standard fault models. We demonstrate how TIGUAN can be combined with conventional structural ATPG to extract full benefit of the intrinsic strengths of both approaches. Fabian Hopsch, Bernd Becker, Sybille Hellebrand, Ilia Polian, Bernd Straube, Wolfgang Vermeiren, Hans-Joachim WunderlichVariation-Aware Fault Modeling 2010 IEEE Asian Test Symp. , Seiten : 87 - 93» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung To achieve a high product quality for nano-scale systems both realistic defect mechanisms and process variations must be taken into account. While existing approaches for variation-aware digital testing either restrict themselves to special classes of defects or assume given probability distributions to model variabilities, the proposed approach combines defect-oriented testing with statistical library characterization. It uses Monte Carlo simu-lations at electrical level to extract delay distributions of cells in the presence of defects and for the defect-free case. This allows distinguishing the effects of process variations on the cell delay from defect-induced cell delays under process variations. To provide a suitable interface for test algorithms at higher levels of abstraction the distributions are represented as histograms and stored in a histogram data base (HDB). Thus, the computationally expensive defect analysis needs to be performed only once as a preprocessing step for library characterization, and statistical test algorithms do not require any low level information beyond the HDB. The generation of the HDB is demonstrated for primitive cells in 45nm technology. nach oben zur Jahresübersicht Alexander Czutro, Ilia Polian, Piet Engelke, Sudhakar M. Reddy, Bernd BeckerDynamic Compaction in SAT-Based ATPG 2009 IEEE Asian Test Symp. Alexander Czutro, Bernd Becker, Ilia PolianPerformance Evaluation of SAT-Based ATPG on Multi-Core Architectures 2009 IEEE East-West Design & Test Symposium Marc Hunger, Sybille Hellebrand, Alexander Czutro, Ilia Polian, Bernd BeckerRobustheitsanalyse stark fehlersicherer Schaltungen mit SAT-basierter Testmustererzeugung 2009 GMM/ITG-Fachtagung “Zuverlässigkeit und Entwurf” Piet Engelke, Bernd Becker, Michel Renovell, Jürgen Schlöffel, Bettina Braitling, Ilia PolianSUPERB: Simulator Utilizing Parallel Evaluation of Resistive Bridges 2009 ACM Trans. on Design Automation of Electronic Systems , Band : 14, Nummer : 4, Seiten : 56:1 - 56:21 Natalia Kalinnik, Tobias Schubert, Erika Ábrahám, Ralf Wimmer, Bernd BeckerPicoso - A Parallel Interval Constraint Solver 2009 Int'l Conf. on Parallel and Distributed Processing Techniques and Applications , CSREA Press, Seiten : 473 - 479» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung This paper describes the parallel interval constraint solver Picoso, which can decide (a subclass of) boolean combinations of linear and non-linear constraints. Picoso follows a master/client model based on message passing, making it suitable for any kind of workstation cluster as well as for multi-processor machines. To run several clients in parallel, an efficient work stealing mechanism has been integrated, dividing the overall search space into disjoint parts. Additionally, to prevent the clients from running into identical conflicts, information about conflicts in form of conflict clauses is exchanged among the clients. Performance measurements, using four clients to solve a number of benchmark problems, show that Picoso yields linear speedup compared to the sequential interval constraint solver iSAT, on which the clients of Picoso are based. Marc Hunger, Sybille Hellebrand, Alejandro Czutro, Ilia Polian, Bernd BeckerATPG-Based Grading of Strong Fault-Secureness 2009 IEEE Int'l Online Testing Symp. Nicolas Houarche, Alejandro Czutro, Mariane Comte, Piet Engelke, Ilia Polian, Bernd Becker, Michel RenovellAn Electrical Model for the Fault Simulation of Small-Delay Faults Caused by Crosstalk Aggravated Resistive Short Defects 2009 VLSI Test Symp. Nicolas Houarche, Alejandro Czutro, Mariane Comte, Piet Engelke, Ilia Polian, Bernd Becker, Michel RenovellDeriving an Electrical Model for Delay Faults Caused by Crosstalk Aggravated Resistive Short Defects 2009 Latin-American Test Workshop Alejandro Czutro, Bernd Becker, Ilia PolianPerformance Evaluation of SAT-Based Automatic Test Pattern Generation on Multi-Core Architectures 2009 GI/ITG Int'l Conf. on Architecture of Computing Systems, Many-Cores Workshop Alejandro Czutro, Bernd Becker, Ilia PolianPerformance Evaluation of SAT-Based ATPG on Multi-Core Architectures 2009 GI/ITG Workshop “Testmethoden und Zuverlässigkeit von Schaltungen und Systemen” Alejandro Czutro, Ilia Polian, Matthew Lewis, Piet Engelke, Sudhakar M. Reddy, Bernd BeckerTIGUAN: Thread-parallel Integrated test pattern Generator Utilizing satisfiability ANalysis 2009 Int'l Conf. on VLSI Design , Seiten : 227 - 232 Paolo Marin, Matthew Lewis, Massimo Narizzano, Tobias Schubert, Enrico Giunchiglia, Bernd BeckerComparison of Knowledge Sharing Strategies in a Parallel QBF Solver 2009 High-Performance Computing and Simulation Conference , Seiten : 161 - 167 Eckard Böde, Marc Herbstritt, Holger Hermanns, Sven Johr, Thomas Peikenkamp, Reza Pulungan, Jan Rakow, Ralf Wimmer, Bernd BeckerCompositional Dependability Evaluation for Statemate 2009 IEEE Trans. on Software Engineering , Band : 35, Nummer : 2, Seiten : 274 - 292» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Software and system dependability is getting ever more important inembedded system design. Current industrial practice of model-basedanalysis is supported by state-transition diagrammatic notationssuch as Statecharts. State-of-the-art modelling tools like\textsc{Statemate} support safety and failure-effect analysis atdesign time, but restricted to qualitative properties. This paperreports on a (plug-in) extension of \textsc{Statemate} enabling theevaluation of quantitative dependability properties at design time.The extension is compositional in the way the model is augmentedwith probabilistic timing information. This fact is exploited in theconstruction of the underlying mathematical model, a uniformcontinuous-time Markov decision process, on which we are able tocheck requirements of the form: \emph{``The probability to hit asafety-critical system configuration within a mission time of 3hours is at most 0.01.''} We give a detailed explanation of theconstruction and evaluation steps making this possible, and reporton a nontrivial case study of a high-speed train signalling systemwhere the tool has been applied successfully. Ralf Wimmer, Bettina Braitling, Bernd BeckerCounterexample Generation for Discrete-time Markov Chains using Bounded Model Checking 2009 Int'l Conf. on Verification, Model Checking and Abstract Interpretation , Springer-Verlag, Band : 5403, Seiten : 366 - 380 Matthew Lewis, Tobias Schubert, Bernd BeckerDPLL-based Reasoning in a Multi-Core Environment 2009 Int'l Workshop on Microprocessor Test and Verification Abhishek Dhama, Oliver Theel, Pepijn Crouzen, Holger Hermanns, Ralf Wimmer, Bernd BeckerDependability Engineering of Silent Self-Stabilizing Systems 2009 Int'l Symp. on Stabilization, Safety, and Security of Distributed Systems , Springer-Verlag, Band : 5873, Seiten : 238 - 253» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Self-stabilization is an elegant way of realizing non-masking fault-tolerant systems. Sustained research over last decades has produced multiple self-stabilizing algorithms for many problems in distributed computing. In this paper, we present a framework to evaluate multiple self-stabilizing solutions under a fault model that allows intermittent transient faults. To that end, metrics to quantify the dependability of self-stabilizing systems are defined. It is also shown how to derive models that are suitable for probabilistic model checking in order to determine those dependability metrics. A heuristics-based method is presented to analyze counterexamples returned by a probabilistic model checker in case the system under investigation does not exhibit the desired degree of dependability. Based on the analysis, the self-stabilizing algorithm is subsequently refined. Paolo Marin, Matthew Lewis, Tobias Schubert, Massimo Narizzano, Bernd Becker, Enrico GiunchigliaEvaluation of Knowledge Sharing Strategies in a Parallel QBF Solver 2009 RCRA International Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion Tobias Schubert, Matthew Lewis, Bernd BeckerPaMiraXT: Parallel SAT Solving with Threads and Message Passing 2009 Journal on Satisfiability, Boolean Modeling, and Computation , Band : 6, Seiten : 203 - 222 Matthew Lewis, Paolo Marin, Tobias Schubert, Massimo Narizzano, Bernd Becker, Enrico GiunchigliaPaQuBE: Distributed QBF Solving with Advanced Knowledge Sharing 2009 Int'l Conf. on Theory and Applications of Satisfiability Testing , Band : 5584, Seiten : 509 - 523 Stefan Kupferschmid, Tino Teige, Bernd Becker, Martin FränzleProofs of Unsatisfiability for mixed Boolean and Non-linear Arithmetic Constraint Formulae 2009 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” , Seiten : 27 - 36» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Symbolic methods in computer-aidedverification rely on appropriate constraint solvers. Correctness and reliabilityof solvers are a vital requirement in the analysis of safety-critical systems,e.g., in the automotive context. Satisfiability results of a solver can usuallybe checked by probing the computed solution. However, efficient validation of anuncertified unsatisfiability result for some constraint formula is nearlyimpossible. In this paper, we propose a certification method for unsatisfiability resultsfor mixed Boolean and non-linear arithmetic constraint formulae. Such formulaearise in the analysis of hybrid discrete-continuous systems. Matthew Lewis, Tobias Schubert, Bernd BeckerQMiraXT - A Multithreaded QBF Solver 2009 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” Stefan Hillebrecht, Ilia Polian, P. Ruther, S. Herwik, Bernd Becker, Oliver PaulReliability Characterization of Interconnects in CMOS Integrated Circuits Under Mechanical Stress 2009 Int'l Reliability Physics Symp. nach oben zur Jahresübersicht Alejandro Czutro, Nicolas Houarche, Piet Engelke, Ilia Polian, Mariane Comte, Michel Renovell, Bernd BeckerA Simulator of Small-Delay Faults Caused by Resistive-Open Defects 2008 IEEE European Test Symp. , Seiten : 113 - 118 Alejandro Czutro, Ilia Polian, Matthew Lewis, Piet Engelke, Sudhakar M. Reddy, Bernd BeckerTIGUAN: Thread-parallel Integrated test pattern Generator Utilizing satisfiability ANalysis 2008 edaWorkshop Piet Engelke, Ilia Polian, Michel Renovell, Sandip Kundu, Bharath Seshadri, Bernd BeckerOn Detection of Resistive Bridging Defects by Low-Temperature and Low-Voltage Testing 2008 IEEE Trans. on CAD , Band : 27, Nummer : 2, Seiten : 327 - 338» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Test application at reduced power supply voltage (low-voltage testing) or reduced temperature (low-temperature testing) can improve the defect coverage of a test set, in particular of resistive short defects. Using a probabilistic model of these defects, we quantify the coverage impact of low-voltage and low-temperature testing for different voltages and temperatures. When considering the coverage increase, we differentiate between defects missed by the test set at nominal conditions and undetectable defects (flaws) detected at non-nominal conditions. In our analysis, the performance degradation of the device caused by lower power supply voltage is accounted for. Furthermore, we describe a situation in which defects detected by conventional testing are missed by low-voltage testing and quantify the resulting coverage loss. Experimental results suggest that test quality is improved even if no cost increase is allowed. If multiple test applications are acceptable, a combination of low-voltage and low-temperature turns out to provide the best coverage of both hard defects and flaws. Damian Nowroth, Ilia Polian, Bernd BeckerA Study of Cognitive Resilience in a JPEG Compressor 2008 Int'l Conf. on Dependable Systems and Networks , Seiten : 32 - 41» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Many classes of applications are inherently tolerant to errors. One such class are applications designed for a human end user, where the capabilities of the human cognitive system (cognitive resilience) may compensate some of the errors produced by the application. We present a methodology to automatically distinguish between tolerable errors in imaging applications which can be handled by the human cognitive system and severe errors which are perceptible to a human end user. We also introduce an approach to identify non-critical spots in a hardware circuit which should not be hardened against soft errors because errors that occur on these spots are tolerable. We demonstrate that over 50% of flip-flops in a JPEG compressor chip are non-critical and require no hardening. Stefan Spinner, Ilia Polian, Piet Engelke, Bernd Becker, Martin Keim, Wu-Tung ChengAutomatic Test Pattern Generation for Interconnect Open Defects 2008 VLSI Test Symp. , Seiten : 181 - 186 Stefan Spinner, Ilia Polian, Piet Engelke, Bernd Becker, Martin Keim, Wu-Tung ChengAutomatic Test Pattern Generation for Interconnect Open Defects 2008 GI/ITG Workshop “Testmethoden und Zuverlässigkeit von Schaltungen und Systemen” Ilia Polian, Yusuke Nakamura, Piet Engelke, Stefan Hillebrecht, Kohei Miyase, Seiji Kajihara, Bernd Becker, Xiaoqing WenDiagnose realistischer Defekte mit Hilfe des X-Fehlermodells 2008 GMM/GI/ITG Reliability and Design Conf. , Seiten : 155 - 156 Ilia Polian, Yusuke Nakamura, Piet Engelke, Stefan Spinner, Kohei Miyase, Seiji Kajihara, Bernd Becker, Xiaoqing WenDiagnosis of Realistic Defects Based on the X-Fault Model 2008 IEEE Design and Diagnostics of Electronic Circuits and Systems , Seiten : 263 - 268 Stefan Hillebrecht, Ilia Polian, Piet Engelke, Bernd Becker, Martin Keim, Wu-Tung ChengExtraction, Simulation and Test Generation for Interconnect Open Defects Based on Enhanced Aggressor-Victim Model 2008 Int'l Test Conf. , Seiten : 1 - 10 Thomas Eschbach, Bernd BeckerInteractive Circuit Diagram Visualization 2008 Computer Graphics and Imaging , ACTA Press, Seiten : 218 - 223 Ilia Polian, Sudhakar M. Reddy, Irith Pomeranz, X. Tang, Bernd BeckerNo Free Lunch in Error Protection? 2008 Workshop on Dependable and Secure Nanocomputing Ilia Polian, Sudhakar M. Reddy, Irith Pomeranz, X. Tang, Bernd BeckerOn Reducing Circuit Malfunctions Caused by Soft Errors 2008 Int'l Symp. on Defect and Fault Tolerance , Seiten : 245 - 253 Ralf Wimmer, Alexander Kortus, Marc Herbstritt, Bernd BeckerProbabilistic Model Checking and Reliability of Results 2008 IEEE Design and Diagnostics of Electronic Circuits and Systems , IEEE Computer Science Press, Seiten : 207 - 212» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In formal verification, reliable results are of utmost importance. In model checking of digital systems, mainly incorrect implementations of the model checking algorithms due to logical errors are the source of wrong results. In probabilistic model checking, however, numerical instabilities are an additional source for inconsistent results.\par We motivate our investigations with an example, for which several state-of-the-art probabilistic model checking tools give completely wrong results due to inexact computations. We then analyze, at which points inaccuracies are introduced during the model checking process. We discuss first ideas how, in spite of these inaccuracies, reliable results can be obtained or at least the user be warned about potential correctness problems: (1) usage of exact (rational) arithmetic, (2) usage of interval arithmetic to obtain safe approximations of the actual probabilities, (3) provision of certificates which testify that the result is correct, and (4) integration of a ``degree of belief'' for each sub-formula into existing model checking tools. Bernd Becker, Marc Herbstritt, Natalia Kalinnik, Matthew Lewis, Juri Lichtner, Tobias Nopper, Ralf WimmerPropositional Approximations for Bounded Model Checking of Partial Circuit Designs 2008 IEEE Int'l Conf. on Computer Design , IEEE Computer Society Press, Seiten : 52 - 59» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Bounded model checking of partial circuit designs enables the detection of errors even when the implementation of the design is not finished. The behavior of the missing parts can be modeled by a conservative extension of propositional logic, called 01X-logic. Then the transitions of the underlying (incomplete) sequential circuit under verification have to be represented adequately. In this work, we investigate the difference between a relation-oriented and a function-oriented approach for this issue. Experimental results on a large set of examples show that the function-oriented representation is most often superior w.\,r.\,t. (1) CPU runtime and (2) accuracy regarding the ability to find a counterexample, such that by using the function-oriented approach an increase of accuracy up to 210\% and a speed-up of the CPU runtime up to 390\% compared to the relation-oriented approach are achieved. But there are also relevant examples, e.\,g. a VLIW-ALU, for which the relation-oriented approach outperforms the function-oriented one by 300\% in terms of CPU-time, showing that both approaches are efficient for different scenarios. Piet Engelke, Ilia Polian, Jürgen Schlöffel, Bernd BeckerResistive Bridging Fault Simulation of Industrial Circuits 2008 Conf. on Design, Automation and Test in Europe , Seiten : 628 - 633» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We report the successful application of a resistive bridging fault (RBF) simulator to industrial benchmark circuits. Despite the slowdown due to the consideration of the sophisticated RBF model, the run times of the simulator were within an order of magnitude of the run times for pattern-parallel complete-circuit stuck-at fault simulation. Industrial-size circuits, including a multi-million-gates design, could be simulated in reasonable time despite a significantly higher number of faults to be simulated compared with stuck-at fault simulation. Piet Engelke, Ilia Polian, Jürgen Schlöffel, Bernd BeckerResistive Bridging Fault Simulation of Industrial Circuits 2008 GI/ITG Workshop “Testmethoden und Zuverlässigkeit von Schaltungen und Systemen” Ilia Polian, Sudhakar M. Reddy, Bernd BeckerScalable Calculation of Logical Masking Effects for Selective Hardening Against Soft Errors 2008 IEEE Int'l Symp. on VLSI , Seiten : 257 - 262 Christian G. Zoellin, Hans-Joachim Wunderlich, Ilia Polian, Bernd BeckerSelective Hardening in Early Design Steps 2008 IEEE European Test Symp. , Seiten : 185 - 190 Bernd Becker, Paul MolitorTechnische Informatik: Eine einführende Darstellung Oldenbourg Wissenschaftsverlag, 2008 Ralf Wimmer, Alexander Kortus, Marc Herbstritt, Bernd BeckerThe Demand for Reliability in Probabilistic Verification 2008 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” , Shaker Verlag, Seiten : 99 - 108» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung For formal verification, reliable results are of utmost importance. In model checking of digital systems, mainly incorrect implementations due to logical errors are the source of wrong results. In probabilistic model checking, however, numerical instabilities are an additional source for inconsistent results.\par First we present an example, for which several state-of-the-art probabilistic model checking tools give completely wrong results due to inexact computations. This motivates the investigation at which points inaccuracies are introduced during the model checking process. We then give ideas how, in spite of these inaccuracies, reliable results can be obtained or at least the user be warned about potential problems: (1) to introduce a ``degree of belief'' for each sub-formula, (2) to use exact (rational) arithmetic, (3) to use interval arithmetic to obtain safe approximations of the actual probabilities, and (4) to provide certificates which testify that the result is correct. nach oben zur Jahresübersicht Ilia Polian, Alejandro Czutro, Sandip Kundu, Bernd BeckerPower Droop Testing 2007 IEEE Design & Test of Computers , Band : 24, Nummer : 3, Seiten : 276 - 284 Marc Herbstritt, Bernd Becker, Erika Ábrahám, Christian HerdeOn Variable Selection in SAT-LP-based Bounded Model Checking of Linear Hybrid Automata 2007 IEEE Design and Diagnostics of Electronic Circuits and Systems , IEEE Computer Society, Seiten : 391 - 396» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung One approach for the verification of embedded systems, where discrete control is embedded in a continuous environment, is bounded model checking of linear hybrid automata. As a decision procedure within this context, a combination of a propositional SAT-solver and an LP-solver can be used. For such combined SAT-LP solvers, it is, among others, an open question how a robust, i.e., reliable, variable selection heuristics should be designed.In this work we investigate the design of such heuristics taking into account (1) the algorithmic structure of the combined SAT-LP-solver, and (2) efficiency issues in form of a counter-based design that adapts the popular concept of the VSIDS heuristics of Chaff. An empirical analysis ofour framework shows (1) the importance of guard variables related to real-valued constraints and (2) reveals an ambiguity between the number of calls of the LP-solver and the time used by the LP-solver. As a result, we propose a simple, but efficient, variable selection heuristics that takes our observations into account and experimentally overcomes the limitations of existing ones. Matthew Lewis, Tobias Schubert, Bernd BeckerMultithreaded SAT Solving 2007 ASP Design Automation Conf. , Seiten : 926 - 921 Bernd Becker, Andreas Podelski, Werner Damm, Martin Fränzle, Ernst-Rüdiger Olderog, Reinhard WilhelmSFB/TR 14 AVACS – Automatic Verification and Analysis of Complex Systems (Der Sonderforschungsbereich/Transregio 14 AVACS – Automatische Verifikation und Analyse komplexer Systeme) 2007 it - Information Technology , Oldenbourg Wissenschaftsverlag GmbH, Band : 49, Nummer : 2, Seiten : 118 - 126 Stefan Spinner, Ilia Polian, Bernd Becker, P. Ruther, Oliver PaulA System for the Calibration and Reliability Testing of MEMS Devices Under Mechanical Stress 2007 VDE Microsystem Technology Congress , Seiten : 861 - 864 John P. Hayes, Ilia Polian, Bernd BeckerAn Analysis Framework for Transient-Error Tolerance 2007 VLSI Test Symp. , Seiten : 249 - 255 Marc Herbstritt, Vanessa Struve, Bernd BeckerApplication of Lifting in Partial Design Analysis 2007 Int'l Workshop on Microprocessor Test and Verification , IEEE Computer Society, Seiten : 33 - 38» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In the past, we have investigated satisfiability-based combinational equivalence checking and bounded model checking of partial circuit designs, i.e., circuit designs where one or more components of the design are not implemented yet. Especially for satisfiability-based bounded model checking, typically a counterexampleis generated in case that the specification property is violated. Minimizing the number of assigned variables in the satisfying assignment that corresponds to such a counterexample is the objective of lifting.In this work we show that lifting is also feasible and profitable for counterexamples obtained via satisfiability-based bounded model checking of partial designs. We provide first experimental results on this issue that show its feasibility.Furthermore, we present a novel application scenario for lifting in the context of automated blackbox synthesis. This is a useful concept that can be applied during combinational equivalence checking of partial circuit designs, where realizability of the missing componentswas already proven, but the functionality of the missing components is still unknown. As a summary, this work provides first experimental results as well as a novel concept regarding the application of lifting for the analysis of partial designs. Tobias Nopper, Christoph Scholl, Bernd BeckerComputation of Minimal Counterexamples by Using Black Box Techniques and Symbolic Methods 2007 IEEE Int'l Conf. on Computer-Aided Design , IEEE Computer Society Press, Seiten : 273 - 280» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Computing counterexamples is a crucial task for error diagnosis and debugging of sequential systems. If an implementation does not fulfill its specification, counterexamples are used to explain the error effect to the designer. In order to be understood by the designer, counterexamples should be simple, i.e. they should be as general as possible and assign values to a minimal number of input signals. Here we use the concept of Black Boxes (parts of the design with unknown behaviour) to mask out components for counterexample computation. By doing so, the resulting counterexample will argue about a reduced number of components in the system to facilitate the task of understanding and correcting the error. We introduce the notion of "uniform counterexamples" to provide an exact formalization of simplified counterexamples arguing only about components which were not masked out. Our computation of counterexamples is based on symbolic methods using AIGs (And-Inverter-Graphs). Experimental results using a VLIW processor as a case study clearly demonstrate our capability of providing simplified counterexamples. Ilia Polian, John P. Hayes, Bernd BeckerCost-Efficient Circuit Hardening Based on Critical Soft Error Rate 2007 IEEE Workshop on RTL ATPG and DfT Ilia Polian, John P. Hayes, Damian Nowroth, Bernd BeckerEin kostenbegrenzter Ansatz zur Reduktion der transienten Fehlerrate 2007 GMM/GI/ITG Reliability and Design Conf. , Seiten : 183 - 184 Ralf Wimmer, Marc Herbstritt, Bernd BeckerForwarding, Splitting, and Block Ordering to Optimize BDD-based Bisimulation Computation 2007 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” , Shaker Verlag, Seiten : 203 - 212» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In this paper we present optimizations for a BDD-based algorithm for the computation of several types of bisimulations which play an important role for minimisation of large systems thus enabling their verification. The basic principle of the algorithm is partition refinement. Our proposed optimizations take this refinement-structure as well as the usage of BDDs for the representation of the system into account: (1) \emph{block forwarding} updates in-situ newly refined blocks of the partition, (2) \emph{split-driven refinement} approximates the blocks that may be refined, and (3) \emph{block ordering} heuristically suggests a good order in which the blocks will be refined.\par We provide substantial experimental results on examples from different applications and compare them to alternative approaches. The experiments clearly show that the proposed optimization techniques result in a significant performance speed-up compared to the basic algorithm as well as to alternative approaches. Ilia Polian, Damian Nowroth, Bernd BeckerIdentification of Critical Errors in Imaging Applications 2007 Int'l On-Line Test Symp. , Seiten : 201 - 202 Bernd Becker, Christian Dax, Jochen Eisinger, Felix KlaedtkeLIRA: Handling Constraints of Linear Arithmetics over the Integers and the Reals 2007 Int'l Conf. on CAV , Springer-Verlag, Seiten : 312 - 315 Marc Herbstritt, Bernd BeckerOn Combining 01X-Logic and QBF 2007 Int'l Conf. on Computer Aided Systems Theory , Springer Verlag, Seiten : 531 - 538» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We discuss how to combine 01X-logic and quantified booleanformulas (QBF) within a homogeneous SAT/QBF-framework in the context of bounded model checking of blackbox designs. The proposed combination allows a flexible handling of blackboxes w.r.t. computational resources. Preliminary results show the scalability of the approach. Ralf Wimmer, Marc Herbstritt, Bernd BeckerOptimization Techniques for BDD-based Bisimulation Minimization 2007 Great Lakes Symp. on VLSI , ACM Press, Seiten : 405 - 410» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In this paper we report on optimizations for a BDD-based algorithm for the computation of bisimulations. The underlying algorithmic principle is an iterative refinement of a partition of the state space. The proposed optimizations demonstrate that both, taking into account the algorithmic structure of the problem and the exploitation of the BDD-based representation, are essential to finally obtain an efficient symbolic algorithm for real-world problems. The contributions of this paper are (1) block forwarding to update block refinement as soon as possible, (2) split-driven refinement that over-approximates the set of blocks that must definitely be refined, and (3) block ordering to fix the order of the blocks for the refinement in a clever way. We provide substantial experimental results on examples from different applications and compare them to alternative approaches when possible. The experiments clearly show that the proposed optimization techniques result in a significant performance speed-up compared to the basic algorithm as well as to alternative approaches. Bernd Becker, Jochen Eisinger, Felix KlaedtkeParallelization of Decision Procedures for Automatic Structures 2007 Workshop on Omega-Automata Piet Engelke, Bettina Braitling, Ilia Polian, Michel Renovell, Bernd BeckerSUPERB: Simulator Utilizing Parallel Evaluation of Resistive Bridges 2007 IEEE Asian Test Symp. , Seiten : 433 - 438» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung A high-performance resistive bridging fault simulator SUPERB (Simulator Utilizing Parallel Evaluation of Resistive Bridges) is proposed. It is based on fault sectioning in combination with parallel-pattern or parallel-fault multiple-stuck-at simulation. It outperforms a conventional interval-based resistive bridging fault simulator by 60X to 120X while delivering identical results. Further competing tools are outperformed by several orders of magnitude. Stefan Spinner, Jie Jiang, Ilia Polian, Piet Engelke, Bernd BeckerSimulating Open-Via Defects 2007 IEEE Asian Test Symp. , Seiten : 265 - 270» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Open-via defects are a major systematic failure mechanism in nanoscale manufacturing processes. We present a flow for simulating open-via defects. Electrical parameters are extracted from the layout and technology data and represented in a way which allows efficient simulation on gate level. The simulator takes oscillation caused by open-via defects into account and quantifies its impact on defect coverage. The flow can be employed for manufacturing test as well as for defect diagnosis. Ralf Wimmer, Alexander Kortus, Marc Herbstritt, Bernd BeckerSymbolic Model Checking for DTMCs with Exact and Inexact Arithmetic AVACS Technical Report , Nummer : 30, 2007 Bernd Becker, Ilia Polian, Sybille Hellebrand, Bernd Straube, Hans-Joachim WunderlichTest und Zuverlässigkeit Nanoelektronischer Systeme 2007 GMM/GI/ITG Reliability and Design Conf. , Seiten : 139 - 140 Ralf Wimmer, Holger Hermanns, Marc Herbstritt, Bernd BeckerTowards Symbolic Stochastic Aggregation AVACS Technical Report , Nummer : 16, 2007 nach oben zur Jahresübersicht Ralf Wimmer, Tobias Nopper, Marc Herbstritt, Christoph Löffler, Bernd BeckerCollaborative Exercise Management 2006 World Conf. on E-Learning in Corporate, Government, Healthcare, and Higher Education , Association for the Advancement of Computing in Education (AACE), Seiten : 3127 - 3134» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In this work, we report on a novel tool for managing exercises used in a collaborative course organization environment at university. Our approach focuses on the separation of the content of the exercises and its layout. The latter is based on the typesetting system LaTeX. Content management of the exercises is established by a web-based interface. As a whole, our tool provides a time-saving and unambiguous workflow for collaborative, time- and place-independent exercise organization. Ilia Polian, Alejandro Czutro, Sandip Kundu, Bernd BeckerPower Droop Testing 2006 Int'l Conf. on Computer Design , Seiten : 243 - 250 Piet Engelke, Ilia Polian, Michel Renovell, Bernd BeckerSimulating Resistive Bridging and Stuck-At Faults 2006 IEEE Trans. on CAD , Band : 25, Nummer : 10, Seiten : 2181 - 2192» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We present a simulator for resistive bridging and stuck-at faults. In contrast to earlier work, it is based on electrical equations rather than table look-up, thus exposing more flexibility. For the first time, simulation of sequential circuits is dealt with; interaction of fault effects in current time frame and earlier timeframes is elaborated on for different bridge resistances. Experimental results are given for resistive bridging and stuck-at faults in combinational and sequential circuits. Different definitions of fault coverage are listed and quantitative results with respect to all these definitions are given for the first time. Michel Renovell, Mariane Comte, Ilia Polian, Piet Engelke, Bernd BeckerAnalyzing the memory effect of resistive open in CMOS random logic 2006 Int'l Conf. on Design and Test of Integrated Systems in Nanoscale Technology , Seiten : 251 - 256» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung This paper analyzes the electrical behaviour of resistive opens as a function of its unpredictable resistance. It is demonstrated that the electrical behaviour depends on the value of the open resistance. It is also shown that, due to the memory effect detection of the open by a given vector Ti depends on all the vectors that have been applied to the circuit before Ti. An electrical analysis of this memory effect is presented. Piet Engelke, Ilia Polian, Michel Renovell, Bernd BeckerAutomatic Test Pattern Generation for Resistive Bridging Faults 2006 Jour. Electronic Testing , Band : 22, Nummer : 1, Seiten : 61 - 69» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung An ATPG for resistive bridging faults in combinational or full-scan circuits is proposed. It combines the advantages of section-based generation and interval-based simulation. In contrast to the solutions introduced so far, it can handle static effects of arbitrary non-feedback bridges between two nodes, including ones detectable at higher bridge resistance and undetectable at lower resistance, and faults requiring more than one vector for detection. The developed tool is applied to ISCAS circuits, and a higher efficiency compared with other resistive bridging fault as well as stuck-at ATPG is reported. Information required for accurate resistive bridging fault simulation is obtained as a by-product. Erika Ábrahám, Marc Herbstritt, Bernd Becker, Martin SteffenMemory-aware Bounded Model Checking for Linear Hybrid Systems 2006 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” , Fraunhofer IIS/EAS, Seiten : 153 - 162» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Bounded Model Checking (BMC) is a successful method for refuting properties of erroneous systems. Initially applied to discrete systems only, BMC could be extended to more complex domains like linear hybrid automata. The increasing complexity coming along with these complex models, but alsorecent optimizations of SAT-based BMC, like excessive conflict learning, reveal a memory explosion problem especially for deep counterexamples. In this paper we introduce parametric data types for the internal solverstructure that, taking advantage of the symmetry of BMC problems, remarkably reduce the memory requirements of the solver. Yuyi Tang, Hans-Joachim Wunderlich, Piet Engelke, Ilia Polian, Bernd Becker, Jürgen Schlöffel, Friedrich Hapke, Michael WittkeX-Masking During Logic BIST and Its Impact on Defect Coverage 2006 IEEE Trans. on VLSI Systems , Band : 14, Nummer : 2, Seiten : 193 - 202» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We present a technique for making a circuit ready for Logic BIST by masking unknown values at its outputs. In order to keep the silicon area cost low, some known bits in output responses are also allowed to be masked. These bits are selected based on a stuck-at n-detection based metric, such that the impact of masking on the defect coverage is minimal. An analysis based on a probabilistic model for resistive short defects indicates that the coverage loss for unmodeled defects is negligible for relatively low values of n. Jan Reineke, Björn Wachter, Stephan Thesing, Reinhard Wilhelm, Jochen Eisinger, Ilia Polian, Bernd BeckerA Definition and Classification of Timing Anomalies 2006 Int'l Workshop on Worst-Case Execution Time John P. Hayes, Ilia Polian, Bernd BeckerA Model for Transient Faults in Logic Circuits 2006 Int'l Design and Test Workshop Michel Renovell, Mariane Comte, Ilia Polian, Piet Engelke, Bernd BeckerA Specific ATPG technique for Resistive Open with Sequence Recursive Dependency 2006 IEEE Asian Test Symp. , Seiten : 273 - 278» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung This paper analyzes the electrical behavior of resistive opens as a function of their unpredictable resistance. It is demonstrated that the electrical behavior depends on the value of the open resistance. It is also shown that detection of the open by a given vector Ti recursively depends on all the vectors that have been applied to the circuit before Ti. An electrical analysis of this recursive effect is presented and a specific ATPG strategy is proposed. Stefan Spinner, M. Doelle, P. Ruther, Ilia Polian, Oliver Paul, Bernd BeckerA System for Electro-Mechanical Reliability Testing of MEMS Devices 2006 Int'l Symp. for Testing and Failure Analysis , Seiten : 147 - 152 Marc Herbstritt, Bernd Becker, Christoph SchollAdvanced SAT-Techniques for Bounded Model Checking of Blackbox Designs 2006 Int'l Workshop on Microprocessor Test and Verification , IEEE Computer Society, Seiten : 37 - 44 Marc Herbstritt, Ralf Wimmer, Thomas Peikenkamp, Eckard Böde, Michael Adelaide, Sven Johr, Holger Hermanns, Bernd BeckerAnalysis of Large Safety-Critical Systems: A quantitative Approach AVACS Technical Report , Band : 8, 2006 Jochen Eisinger, Ilia Polian, Bernd Becker, Alexander Metzner, Stephan Thesing, Reinhard WilhelmAutomatic Identification of Timing Anomalies for Cycle-Accurate Worst-Case Execution Time Analysis 2006 IEEE Design and Diagnostics of Electronic Circuits and Systems , IEEE Computer Society, Seiten : 15 - 20 Erika Ábrahám, Marc Herbstritt, Bernd Becker, Martin SteffenBounded Model Checking with Parametric Data Structures 2006 BMC , Band : 174, Nummer : 3, Seiten : 3 - 16 Eckard Böde, Marc Herbstritt, Holger Hermanns, Sven Johr, Thomas Peikenkamp, Reza Pulungan, Ralf Wimmer, Bernd BeckerCompositional Performability Evaluation for STATEMATE 2006 Int'l Conf. on Quantitative Evaluation of Systems , IEEE Computer Society, Seiten : 167 - 178» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung This paper reports on our efforts to link an industrial state-of-the-art modelling tool to academic state-of-the-art analysis algorithms. In a nutshell, we enable timed reachability analysis of uniform continuous-time Markov decision processes, which are generated from Statemate models. We give a detailed explanation of several construction, transformation, reduction, and analysis steps required to make this possible. The entire tool flow has been implemented, and it is applied to a nontrivial example. Bernd Becker, Ilia Polian, Sybille Hellebrand, Bernd Straube, Hans-Joachim WunderlichDFG-Projekt RealTest - Test und Zuverlässigkeit nanoelektronischer Systeme (DFG-Project - Test and Reliability of Nano-Electronic Systems) 2006 it - Information Technology , Band : 48, Nummer : 5, Seite : 304 Piet Engelke, Ilia Polian, Hans Manhaeve, Michel Renovell, Bernd BeckerDelta-IddQ Testing of Resistive Short Defects 2006 IEEE Asian Test Symp. , Seiten : 63 - 68» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung This paper addresses the efficiency of IDDQ and more in particular Delta-IDDQ testing when using a realistic short defect model that properly considers the relation between the resistance of the short and its detectability. The results clearly show that the Delta-IDDQ approach covers a large number of resistive shorts missed by conventional logic testing, requiring only a relative small vector set. In addition a significant number of defects which are proven to be undetectable by logic testing but may deteriorate and result in reliability failures are detected. The Delta-IDDQ threshold and thus the equipment sensitivity is shown to be critical for the test quality. Furthermore, the validity of the traditional IDDQ fault models when considering resistive short defects is found to be limited. For instance, the use of the fault-free next-state function for sequential IDDQ fault simulation is shown to result in a wrong classification of some resistive short defects. This is the first systematic study of IDDQ testing of resistive short defects. The impact of the threshold on the defect coverage is quantified for the first time. Although the simulation results are based upon an older technology, the results and methodology are as well valid for state-of-the-art and NanoTechnologies. Stefan Spinner, J. Bartholomeyczik, Bernd Becker, M. Doelle, Oliver Paul, Ilia Polian, P. Roth, K. Seitz, P. RutherElectromechanical Reliability Testing of Three-Axial Force Sensors 2006 Design, Test, Integration and Packaging of MEMS/MOEMS , Seiten : 77 - 82 Piet Engelke, Ilia Polian, Hans Manhaeve, Bernd BeckerIddQ Testing of Resistive Bridging Defects 2006 GI/ITG Workshop “Testmethoden und Zuverlässigkeit von Schaltungen und Systemen” , Seiten : 123 - 124 Ilia Polian, Bernd Becker, M. Nakasato, S. Ohtake, Hideo FujiwaraLow-Cost Hardening of Image Processing Applications Against Soft Errors 2006 Int'l Symp. on Defect and Fault Tolerance , Seiten : 274 - 279» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Image processing systems are increasingly used in safetycritical applications, and their hardening against soft errors becomes an issue. We propose a methodology to identify soft errors as uncritical based on their impact on the system’s functionality. We call a soft error uncritical if its impact is provably limited to image perturbations during a very short period of time (number of cycles) and the system is guaranteed to recover thereafter. Uncritical errors do not require hardening as their effects are imperceivable for the human user of the system. We focus on soft errors in the motion estimation subsystem of MPEG-2 and introduce different definitions of uncritical soft errors in that subsystem. We propose a method to automatically determine uncritical errors and provide experimental results for various parameters. The concept can be adapted to further systems and enhance existing methods. Ralf Wimmer, Marc Herbstritt, Bernd BeckerMinimization of Large State Spaces using Symbolic Branching Bisimulation 2006 IEEE Design and Diagnostics of Electronic Circuits and Systems , IEEE Computer Society Press, Seiten : 9 - 14» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Bisimulations in general are a powerful concept to minimize large finite state systems regarding some well-defined observational behavior. In contrast to strong bisimulation, for branching bisimulation there are only tools available that work on an explicit state space representation. In this work we present for the first time a symbolic approach for branching bisimulation that uses BDDs as basic data structure and that is based on the concept of signature refinement. First experimental results for problem instances derived from process algebraic system descriptions show the feasibility and the robustness of our approach. Thomas Eschbach, Wolfgang Günther, Bernd BeckerOrthogonal Hypergraph Drawing for Improved Visibility 2006 Journal of Graph Algorithms and Applications , Band : 10, Nummer : 2, Seiten : 141 - 157» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Visualization of circuits is an important research area in electronic design automation. One commonly accepted method to visualize a circuit aligns the gates to layers and uses orthogonal lines to connect the gates. In our model we assume that between two consecutive layers every net is allowed to occupy only one track. This avoids unnecessary bends in the wires and helps to improve the clarity of the drawing. Then a crossing reduction step is applied to further improve the readability of the circuit schematics.First we assume that the nodes have already been fixed on alayered hypergraph structure. We consider the problem of assigning the hyperedges between two layers to tracks. The idea is to minimize the total number of hyperedge crossings. We prove that finding the best solution is NP-hard. Then, in contrast to many other approaches which route all the wiring after placing all nodes we focus on a new approach which dynamically reorders the nodes within the layers to further reduce the number of hyperedge crossings.An efficient algorithm is presented that minimizes the hyperedge crossings. Experimental results are provided which show that the drawings can be improved significantly while the run time remains moderate. Erika Ábrahám, Tobias Schubert, Bernd Becker, Martin Fränzle, Christian HerdeParallel SAT-Solving in Bounded Model Checking 2006 Int'l Workshop on Parallel and Distributed Methods in Verification , Springer-Verlag, Band : 4346, Seiten : 301 - 315» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Bounded Model Checking (BMC) is an incremental refutation technique to search for counterexamples of increasing length. The existence of a counterexample of a fixed length is expressed by a first-order logic formula that is checked for satisfiability using a suitable solver.We apply communicating parallel solvers to check satisfiability of the BMC formulae. In contrast to other parallel solving techniques, our method does not parallelize the satisfiability check of a single formula, but the parallel solvers work on formulae for different counterexample lengths. We adapt the method of constraint sharing and replication of Shtrichman, originally developed for sequential BMC, to the parallel setting. Since the learning mechanism is now parallelized, it is not obvious whether there is a benefit from the concepts of Shtrichman in the parallel setting. We demonstrate on a number of benchmarks that adequate communication between the parallel solvers yields the desired results. Ilia Polian, Bernd Becker, M. Nakasato, S. Ohtake, Hideo FujiwaraPeriod of Grace: A New Paradigm for Efficient Soft Error Hardening 2006 GI/ITG Workshop “Testmethoden und Zuverlässigkeit von Schaltungen und Systemen” Stefan Spinner, J. Bartholomeyczik, Bernd Becker, M. Doelle, Oliver Paul, Ilia Polian, R. Roth, K. Seitz, P. RutherReliability Testing of Three-Dimensional Silicon Force Sensors 2006 GI/ITG Workshop “Testmethoden und Zuverlässigkeit von Schaltungen und Systemen” Ralf Wimmer, Marc Herbstritt, Holger Hermanns, Kelley Strampp, Bernd BeckerSigref - A Symbolic Bisimulation Tool Box 2006 Int'l Symp. on Automated Technology for Verification and Analysis , Springer-Verlag, Band : 4218, Seiten : 477 - 492» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We present a uniform signature-based approach to compute the most popular bisimulations. Our approach is implemented symbolically using BDDs, which enables the handling of very large transition systems. Signatures for the bisimulations are built up from a few generic building blocks, which naturally correspond to efficient BDD operations. Thus, the definition of an appropriate signature is the key for a rapid development of algorithms for other types of bisimulation. We provide experimental evidence of the viability of this approach by presenting computational results for many bisimulations on real-world instances. The experiments show cases where our framework can handle state spaces efficiently that are far too large to handle for any tool that requires an explicit state space description. nach oben zur Jahresübersicht Marc Herbstritt, Bernd BeckerOn SAT-based Bounded Invariant Checking of Blackbox Designs 2005 Int'l Workshop on Microprocessor Test and Verification , IEEE Computer Society, Seiten : 23 - 28» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Design verification by property checking is a mandatory taskduring circuit design. In this context, Bounded Model Checking (BMC) has become popular for falsifying erroneous designs. Additionally, the analysis of partial designs, i.e., circuits that are not fully specified, has recently gained attraction. In this work we analyze how BMC can be applied to such partial designs. Our experiments show that even with the most simple modelling scheme, namely 01X-simulation, a relevant number of errors can be detected. Additionally, we propose a SAT-solver that directly can handle 01X-logic. Martina Welte, Thomas Eschbach, Bernd BeckerAutomated Text Extraction And Indexing Of Video Presentation Recordings For Keyword Search Via A Web Interface 2005 Workshop eLectures - Einsatzmöglichkeiten, Herausforderungen und Forschungsperspektiven , Logos Verlag Berlin Matthew Lewis, Tobias Schubert, Bernd BeckerSpeedup Techniques Utilized in Modern SAT Solvers - An Analysis in the MIRA Environment 2005 Theory and Applications of Satisfiability Testing , Springer, Band : 3569, Seiten : 437 - 443» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung This paper describes and compares features and techniques modern SAT solvers utilize to maximize performance. Here we focus on: Implication Queue Sorting (IQS) combined with Early Conflict Detection Based BCP (ECDB); and a modified decision heuristic based on the combination of Variable State Independent Decaying Sum (VSIDS), Berkmin, and Siege’s Variable Move to Front (VMTF). These features were implemented and compared within the framework of the MIRA SAT solver. The efficient implementation and analysis of these features are presented and the speedup and robustness each feature provides is demonstrated. Finally, with everything enabled (ECDB with IQS and advanced decision heuristics), MIRA was able to consistently outperform zChaff and even Forklift on the benchmarks provided, solving 37 out of 111 industrial benchmarks compared to zChaff’s 21 and Forklift’s 28. Ilia Polian, Alejandro Czutro, Bernd BeckerEvolutionary Optimization in Code-Based Test Compression 2005 Conf. on Design, Automation and Test in Europe , Seiten : 1124 - 1129 Ilia Polian, Piet Engelke, Michel Renovell, Bernd BeckerModeling feedback bridging faults with non-zero resistance. 2005 Jour. Electronic Testing , Band : 21, Nummer : 1, Seiten : 57 - 69» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We study the behavior of feedback bridging faults with non-zero bridge resistance in both combinational and sequential circuits. We demonstrate that a test vector may detect the fault, not detect the fault or lead to oscillation, depending on bridge resistance. Moreover, the resistance intervals in which a particular behavior is observed are not necessarily contiguous. Even loops going through a gate with controlling values on its side inputs (which we call disabled loops) expose non-trivial behavior. We outline the multiple strengths problem which arises due to the fact that a critical bridge resistance depends on the strengths of the signals driving the bridge, which in turn are functions of the number of the on-transistors, these again depending on the bridge resistance, making such a fault very hard to resolve. For sequential circuits, we describe additional difficulties caused by the need to account for implications on bridge behavior, which have originated in the previous time frames. We conclude that the complexity of resistive feedback bridging fault simulation accurate enough to resolve such situations will probably be prohibitively high and propose possible simplifying assumptions. We present simulation results for ISCAS benchmarks using these assumptions with and without taking oscillation into account. John P. Hayes, Ilia Polian, Thomas Fiehn, Bernd BeckerA Family of Logical Fault Models for Reversible Circuits 2005 IEEE European Test Symp. , Seiten : 65 - 70» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Reversibility is of interest in achieving extremely low power dissipation; it is also an inherent design requirement of quantum computation. Logical fault models for conventional circuits such as stuck-at models are not well-suited to quantum circuits. We derive a family of logical fault models for reversible circuits composed of k-CNOT (k-input controlled-NOT) gates and implementable by many technologies. The models are extensions of the previously proposed single missing-gate fault (MGF) model, and include multiple and partial MGFs. We study the basic detection requirements of the new fault types and derive bounds on the size of their test sets. We also present optimal test sets computed via integer linear programming for various benchmark circuits. These results indicate that, although the test sets are generally very small, partial MGFs may need significantly larger test sets than single MGFs. Ilia Polian, John P. Hayes, Thomas Fiehn, Bernd BeckerA Family of Logical Fault Models for Reversible Circuits 2005 IEEE Asian Test Symp. , Seiten : 422 - 427» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Reversibility is of interest in achieving extremely low power dissipation; it is also an inherent design requirement of quantum computation. Logical fault models for conventional circuits such as stuck-at models are not well-suited to quantum circuits. We derive a family of logical fault models for reversible circuits composed of k-CNOT (k-input controlled-NOT) gates and implementable by many technologies. The models are extensions of the previously proposed single missing-gate fault (MGF) model, and include multiple and partial MGFs. We study the basic detection requirements of the new fault types and derive bounds on the size of their test sets. We also present optimal test sets computed via integer linear programming for various benchmark circuits. These results indicate that, although the test sets are generally very small, partial MGFs may need significantly larger test sets than single MGFs. Tobias Schubert, Bernd BeckerA Hardware Lab Anywhere at Any Time 2005 Journal of Systemics, Cybernetics, and Informatics: JSCI , Band : 2, Nummer : 6 Sandip Kundu, Matthew Lewis, Ilia Polian, Bernd BeckerA Soft Error Emulation System for Logic Circuits 2005 GI/ITG Workshop “Testmethoden und Zuverlässigkeit von Schaltungen und Systemen” , Seiten : 10 - 14» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In nanometer technologies, soft errors in logic circuits are increasingly important. Since the failure in time (FIT) rates for these circuits are very low, millions of test vectors are required for a realistic analysis of soft errors. This exceeds the capabilities of software simulation tools. We propose an FPGA emulation architecture that can apply millions of vectors within seconds. Comprehensive soft error profiling was done for ISCAS 89 circuits. Soft errors were assigned to four different classes, and their latency and recovery time were obtained. This information is useful for understanding the vulnerability of the system to soft errors and hardening it against such errors. Sandip Kundu, Matthew Lewis, Ilia Polian, Bernd BeckerA Soft Error Emulation System for Logic Circuits 2005 Conf. on Design of Circuits and Integrated Systems , Seite : 137» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In nanometer technologies, soft errors in logic circuits are increasingly important. Since the failure in time (FIT) rates for these circuits are very low, millions of test vectors are required for a realistic analysis of soft errors. This exceeds the capabilities of software simulation tools. We propose an FPGA emulation architecture that can apply millions of vectors within seconds. Comprehensive soft error profiling was done for ISCAS 89 circuits. Soft errors were assigned to four different classes, and their latency and recovery time were obtained. This information is useful for understanding the vulnerability of the system to soft errors and hardening it against such errors. M. Doelle, Stefan Spinner, P. Ruther, Ilia Polian, Oliver Paul, Bernd BeckerA System for Determining the Impact of Mechanical Stress on the Reliability of MEMS 2005 IEEE European Test Symp. , Seiten : 57 - 61» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung This paper reports on an experimental test system which enables the automated analysis of mechanical stress impact on the reliability of microelectromechanical systems (MEMS). With this system, in-situ electrical characterization and optical inspection are performed while subjecting MEMS devices to defined mechanical loads. Impact objects of various geometries, e.g., contact probes or wafer prober needles, can be applied which are aligned relative to the MEMS device using an xyz-nanopositioning stage with an accuracy of 25 nm. This positioning stage enables programmable static forces up to 5 N and dynamic loads at frequencies up to 800 Hz. With this highly flexible system reliability tests, postmanufacturing tests and stress screens can be performed on single chips as well as on whole wafers with diameters up to 6 inch. Preliminary results on long-term reliability tests using CMOS-based stress sensors exploiting the piezoresistive effect in field effect transistors are presented. M. Doelle, Stefan Spinner, P. Ruther, Ilia Polian, Oliver Paul, Bernd BeckerA System for Determining the Impact of Mechanical Stress on the Reliability of MEMS 2005 GI/ITG Workshop “Testmethoden und Zuverlässigkeit von Schaltungen und Systemen” , Seiten : 88 - 89» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung This paper reports on an experimental test system which enables the automated analysis of mechanical stress impact on the reliability of microelectromechanical systems (MEMS). With this system, in-situ electrical characterization and optical inspection are performed while subjecting MEMS devices to defined mechanical loads. Impact objects of various geometries, e.g., contact probes or wafer prober needles, can be applied which are aligned relative to the MEMS device using an xyz-nanopositioning stage with an accuracy of 25 nm. This positioning stage enables programmable static forces up to 5 N and dynamic loads at frequencies up to 800 Hz. With this highly flexible system reliability tests, postmanufacturing tests and stress screens can be performed on single chips as well as on whole wafers with diameters up to 6 inch. Preliminary results on long-term reliability tests using CMOS-based stress sensors exploiting the piezoresistive effect in field effect transistors are presented. Tobias Schubert, Bernd BeckerAccelerating Boolean SAT Engines Using Hyper-Threading Technology 2005 Asian Applied Computing Conf. Gang Chen, Sudhakar M. Reddy, Irith Pomeranz, Janusz Rajski, Piet Engelke, Bernd BeckerAn Unified Fault Model and Test Generation Procedure for Interconnect Opens and Bridges 2005 IEEE European Test Symp. , Seiten : 22 - 27 Martina Welte, Thomas Eschbach, Bernd BeckerAutomated Text Extraction And Indexing Of Video Presentation Recordings For Keyword Search Via A Web Interface 2005 AACE World Conf. on E-Learning in Corporate, Government, Healthcare, and Higher Education , AACE Press, Seiten : 3200 - 3205 Bernd Becker, Markus Behle, Friedrich Eisenbrand, Ralf WimmerBDDs in a Branch & Cut Framework 2005 Int'l Workshop on Efficient and Experimental Algorithms , Springer Verlag, Band : 3503, Seiten : 452 - 463» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Branch & Cut is today's state-of-the-art method to solve 0/1-integer linear programs. Important for the success of this method is the generation of strong valid inequalities, which tighten the linear programming relaxation of 0/1-IPs and thus allow for early pruning of parts of the search tree.\par In this paper we present a novel approach to generate valid inequalities for 0/1-IPs which is based on Binary Decision Diagrams (BDDs). BDDs are a datastructure which represents 0/1-vectors as paths of a certain acyclic graph. They have been successfully applied in computational logic, hardware verification and synthesis.\par We implemented our BDD cutting plane generator in a branch-and-cut framework and tested it on several instances of the MAX-ONES problem and randomly generated 0/1-IPs. Our computational results show that we have developed competitive code for these problems, on which state-of-the-art MIP-solvers fall short. Tobias Schubert, Bernd BeckerKnowledge Sharing in a Microcontroller based Parallel SAT Solver 2005 Int'l Conf. on Parallel and Distributed Processing Techniques and Applications Tobias Schubert, Bernd BeckerLemma Exchange in a Microcontroller based Parallel SAT Solver 2005 IEEE Int'l Symp. on VLSI Ilia Polian, Piet Engelke, Michel Renovell, Bernd BeckerModeling feedback bridging faults with non-zero resistance 2005 Jour. Electronic Testing , Band : 21, Nummer : 1, Seiten : 57 - 69» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We study the behavior of feedback bridging faults with non-zero bridge resistance in both combinational and sequential circuits. We demonstrate that a test vector may detect the fault, not detect the fault or lead to oscillation, depending on bridge resistance. Moreover, the resistance intervals in which a particular behavior is observed are not necessarily contiguous. Even loops going through a gate with controlling values on its side inputs (which we call disabled loops) expose non-trivial behavior. We outline the multiple strengths problem which arises due to the fact that a critical bridge resistance depends on the strengths of the signals driving the bridge, which in turn are functions of the number of the on-transistors, these again depending on the bridge resistance, making such a fault very hard to resolve. For sequential circuits, we describe additional difficulties caused by the need to account for implications on bridge behavior, which have originated in the previous time frames. We conclude that the complexity of resistive feedback bridging fault simulation accurate enough to resolve such situations will probably be prohibitively high and propose possible simplifying assumptions. We present simulation results for ISCAS benchmarks using these assumptions with and without taking oscillation into account. Sandip Kundu, Piet Engelke, Ilia Polian, Bernd BeckerOn Detection of Resistive Bridging Defects by Low-Temperature and Low-Voltage Testing 2005 IEEE Asian Test Symp. , Seiten : 266 - 269» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Resistive defects are gaining importance in very-deep-submicron technologies, but their detection conditions are not trivial. Test application can be performed under reduced temperature and/or voltage in order to improve detection of these defects. This is the first analytical study of resistive bridge defect coverage of CMOS ICs under low-temperature and mixed low-temperature, low-voltage conditions. We extend a resistive bridging fault model in order to account for temperature-induced changes in detection conditions. We account for changes in both the parameters of transistors involved in the bridge and the resistance of the short defect itself. Using a resistive bridging fault simulator, we determine fault coverage for low-temperature testing and compare it to the numbers obtained at nominal conditions. We also quantify the coverage of flaws,i.e. defects that are redundant at nominal conditions but could deteriorate and become early-life failures. Finally, we compare our results to the case of low-voltage testing and comment on combination of these two techniques. Erika Ábrahám, Bernd Becker, Felix Klaedtke, Martin SteffenOptimizing bounded model checking for linear hybrid systems 2005 Int'l Conf. on Verification, Model Checking and Abstract Interpretation , Springer-Verlag, Band : 3385, Seiten : 396 - 412» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Bounded model checking (BMC) is an automatic verification method that is based on finitely unfolding the system's transition relation. BMC has been successfully applied, in particular, for discovering bugs in digital system design. Its success is based on the effectiveness of satisfiability solvers that are used to check for a finite unfolding whether a violating state is reachable. In this paper we improve the BMC approach for linear hybrid systems. Our improvements are tailored to lazy satisfiability solving and follow two complementary directions. First, we optimize the formula representation of the finite unfoldings of the transition relations of linear hybrid systems, and second, we accelerate the satisfiability checks by accumulating and generalizing data that is generated during earlier satisfiability checks. Experimental results show that the presented techniques accelerate the satisfiability checks significantly. Thomas Eschbach, Wolfgang Günther, Bernd BeckerOrthogonal Circuit Visualization Improved by Merging the Placement and Routing Phases 2005 Int'l Conf. on VLSI Design , Seiten : 433 - 438 Tobias Schubert, Bernd Becker, Matthew LewisPaMira - A Parallel SAT Solver with Knowledge Sharing 2005 Int'l Workshop on Microprocessor Test and Verification , IEEE Computer Society, Band : 00, Seiten : 29 - 36» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In this paper we describe PaMira, a powerful distributed SAT solver. PaMira is based on the highly optimized, sequential SAT engine Mira, incorporating all essential optimization techniques modern algorithms utilize to maximize performance. For the distributed execution an efficient work stealing method has been implemented. PaMira also employs the exchange of conflict clauses between the processes to guide the search more efficiently. We provide experimental results showing linear speedup on a multiprocessor environment with four AMD Opteron processors. Ilia Polian, Sandip Kundu, Jean-Marc Galliere, Piet Engelke, Michel Renovell, Bernd BeckerResistive Bridge Fault Model Evolution From Conventional to Ultra Deep Submicron Technologies 2005 VLSI Test Symp. , Seiten : 343 - 348» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We present three resistive bridging fault models valid for different CMOS technologies. The models are partitioned into a general framework (which is shared by all three models) and a technology-specific part. The first model is based on Shockley equations and is valid for conventional but not deep submicron CMOS. The second model is obtained by fitting SPICE data. The third resistive bridging fault model uses Berkeley Predictive Technology Model and BSIM4; it is valid for CMOS technologies with feature sizes of 90nm and below, accurately describing non-trivial electrical behavior in that technologies. Experimental results for ISCAS circuits show that the test patterns obtained for the Shockley model are still valid for the Fitted model, but lead to coverage loss under the Predictive model. Jochen Eisinger, Peter Winterer, Bernd BeckerSecuring Wireless Networks in a University Environment 2005 IEEE Int'l Conf. on Pervasive Computing and Communications Workshops , IEEE Computer Society, Seiten : 312 - 316 Piet Engelke, Valentin Gherman, Ilia Polian, Yuyi Tang, Hans-Joachim Wunderlich, Bernd BeckerSequence Length, Area Cost and Non-Target Defect Coverage Tradeoffs in Deterministic Logic BIST 2005 IEEE Design and Diagnostics of Electronic Circuits and Systems , Seiten : 43 - 48 Piet Engelke, Valentin Gherman, Ilia Polian, Yuyi Tang, Hans-Joachim Wunderlich, Bernd BeckerSequence Length, Area Cost and Non-Target Defect Coverage Tradeoffs in Deterministic Logic BIST 2005 GI/ITG Workshop “Testmethoden und Zuverlässigkeit von Schaltungen und Systemen” , Seiten : 16 - 20 Piet Engelke, Valentin Gherman, Ilia Polian, Yuyi Tang, Hans-Joachim Wunderlich, Bernd BeckerSequence Length, Area Cost and Non-Target Defect Coverage Tradeoffs in Deterministic Logic BIST 2005 IEEE Int'l Workshop on Current and Defect-Based Testing , Seiten : 43 - 48 Ilia Polian, John P. Hayes, Sandip Kundu, Bernd BeckerTransient Fault Characterization in Dynamic Noisy Environments 2005 Int'l Test Conf. , Seiten : 10 pp. - 1048 nach oben zur Jahresübersicht Erika Ábrahám, Bernd Becker, Felix Klaedtke, Martin SteffenOptimizing Bounded Model Checking for Linear Hybrid Systems , Nummer : 214, 2004» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Bounded model checking (BMC) is an automatic verification method that is based on finitely unfolding the system's transition relation. BMC has been successfully applied, in particular, for discovering bugs in digital system design. Its success is based on the effectiveness of satisfiability solvers that are used to check for a finite unfolding whether a violating state is reachable. In this report we improve the BMC approach for linear hybrid systems. Our improvements are tailored to lazy satisfiability solving and follow two complementary directions. First, we optimize the formula representation of the finite unfoldings of the transition relations of linear hybrid systems, and second, we accelerate the satisfiability checks by accumulating and generalizing data that is generated during earlier satisfiability checks. Experimental results show that the presented techniques accelerate the satisfiability checks significantly. Marc Herbstritt, Thomas Kmieciak, Bernd BeckerOn the Impact of Structural Circuit Partitioning on SAT-based Combinational Circuit Verification 2004 Int'l Workshop on Microprocessor Test and Verification , IEEE Computer Society, Seiten : 50 - 55» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In this work we present an approach for SAT-based combinational circuit verification using partitionings of the set of primary outputs. We formally analyze the applied partitioning heuristics for the first time and present a closed verification framework incorporating traditional techniques. We report on experiments using our partitioning-based verification procedure that result in speedups of 276% on the average compared to traditional techniques. Marc Herbstritt, Thomas Kmieciak, Bernd BeckerCircuit Partitioning for SAT-based Combinational Circuit Verification -- A Case Study , Nummer : 206, 2004» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Hardware verification is nowadays one of the most time-consuming tasks during chip design. In the last few years SAT-based methods have become a core technology in hardware design, especially for the verification of combinational parts of the circuits. Verifying the equivalence of some specification and a corresponding implementation is typically done by building a so-called miter. In practice this miter is often build for each pair of primary outputs or for all primary outputs at once. In this work we have a closer look on partitioning the primary outpouts of the circuit and how structural partitionings can speed-up the verification process when SAT-based methods are used. Ilia Polian, Bernd Becker, Alejandro CzutroCompression Methods for Path Delay Fault Test Pair Sets: A Comparative Study 2004 IEEE European Test Symp. , Seiten : 263 - 264 Matthew Lewis, Tobias Schubert, Bernd BeckerEarly Conflict Detection Based BCP for SAT Solving 2004 Int'l Conf. on Theory and Applications of Satisfiability Testing , Seiten : 29 - 36» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Abstract. This paper describes a new BCP algorithm that improves the performance of Chaff class solvers by reducing the total number of clauses the BCP procedure must evaluate. This is done by: detecting conflicts earlier; evaluating clauses better; and by increasing the controllability of the conflicts which the BCP procedure finds. Solvers like Limmat [10] include a simple Early Conflict Detection BCP (ECDB), however we introduce a new aggressive ECDB procedure and the MIRA solver that efficiently incorporates it while easily facilitating comparisons between ECDB modes. With the full ECDB procedure enabled, MIRA was able to reduce the number of evaluated clauses by 59% on average compared to the disabled ECDB version. This new procedure and other speedup techniques discussed here allow MIRA to solve problems 3.7 times faster on average than zChaff. Lastly, this paper shows how significant speedup can be attained relatively easily by incorporating a certain level of ECDB into other solvers. Ilia Polian, Irith Pomeranz, Sudhakar M. Reddy, Bernd BeckerOn the use of maximally dominating faults in n-detection test generation 2004 IEE Proceedings Computers and Digital Techniques , Band : 151, Nummer : 3, Seiten : 235 - 244» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung The size of an n-detection test set increases approximately linearly with n. This increase in size may be too fast when an upper bound on test set size must be satisfied. We propose a test generation method for obtaining a more gradual increase in the sizes of n-detection test sets, while still ensuring that every additional test would be useful in improving the test set quality. The method is based on the use of fault dominance relations to identify a small subset of faults (called maximally dominating faults) whose numbers of detections are likely to have a high impact on the defect coverage of the test set. We use structural analysis to obtain a superset of the maximally dominating fault set. We also propose a method for determining exact sets of maximally dominating faults. We define new types of n-detection test sets based on the approximate and exact sets of maximally dominating faults. The test sets are called (n,n2)-detection test sets and (n,n2,n3)-detection test sets. We present experimental results to demonstrate the usefulness of these test sets in producing high-quality n-detection test sets for the combinational logic of ISCAS-89 benchmark circuits. Ilia Polian, Bernd BeckerScalable Delay Fault BIST For Use With Low-Cost ATE 2004 Jour. Electronic Testing , Band : 20, Nummer : 2, Seiten : 181 - 197» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We present a BIST architecture based on Multi-Input Signature Register (MISR) expanding single input vectors into sequences, which are used for testing of delay faults. Input vectors can be stored on-chip or in the ATE; in the latter case, a low speed tester can be employed though the sequences are applied at-speed to block-under-test. The number of input vectors (and thus the area demand on-chip or ATE memory requirements) can be traded for the test application time. The block-under-test can be switched off for some amount of time between application of consecutive input vectors. We provide arguments why this approach may be the only way to meet thermal and power constraints. Furthermore, we demonstrate how the BIST scheme can use these cool-down breaks for re-configuration. We propose two methods for generating input vectors, a straight-forward one and one using BDDs and symbolic state traversals. As both require only a two-pattern test as input, IP cores can be handled by these methods. Yuyi Tang, Hans-Joachim Wunderlich, Harald Vranken, Friedrich Hapke, Michael Wittke, Piet Engelke, Ilia Polian, Bernd BeckerX-masking during logic BIST and its impact on defect coverage 2004 IEEE Int'l Workshop on Test Resource Partitioning , Seiten : 442 - 451 Tobias Schubert, Bernd BeckerA Distributed SAT Solver for Microchip Microcontroller 2004 Workshop on Parallel Systems and Algorithms Piet Engelke, Ilia Polian, Michel Renovell, Bernd BeckerAutomatic test pattern generation for resistive bridging faults 2004 IEEE European Test Symp. , Seiten : 160 - 165 Piet Engelke, Ilia Polian, Michel Renovell, Bernd BeckerAutomatic test pattern generation for resistive bridging faults 2004 IEEE Int'l Workshop on Current and Defect-Based Testing , Seiten : 89 - 94 Bernd Becker, Markus Behle, Friedrich Eisenbrand, Martin Fränzle, Marc Herbstritt, Christian Herde, Jörg Hoffmann, Daniel Kröning, Bernhard Nebel, Ilia Polian, Ralf WimmerBounded Model Checking and Inductive Verification of Hybrid Discrete-continuous Systems 2004 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” , Shaker Verlag, Seiten : 65 - 75» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We present a concept to significantly advance the state of the art for bounded model checking (BMC) and inductive verification (IV) of hybrid discrete-continuous systems. Our approach combines the expertise of partners coming from different domains, like hybrid systems modeling and digital circuit verification, bounded planning and heuristic search, combinatorial optimization and integer programming. After sketching the overall verification flow we present first results indicating that the combination and tight integration of different verification engines is a first step to pave the way to fully automated BMC and IV of medium to large-scale networks of hybrid automata. Matthew Lewis, Tobias Schubert, Bernd BeckerEarly Conflict Detection Based SAT Solving 2004 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” Thomas Eschbach, Wolfgang Günther, Bernd BeckerOrthogonal Hypergraph Routing for Improved Visibility 2004 Great Lakes Symp. on VLSI , Seiten : 385 - 388 Tobias Schubert, Bernd BeckerPICHAFF2 - A Hierarchical Parallel SAT Solver 2004 Int'l Workshop on Microprocessor Test and Verification Tobias Schubert, Bernd BeckerParallel SAT Solving with Microcontrollers 2004 Asian Applied Computing Conf. Thomas Eschbach, Rolf Drechsler, Bernd BeckerPlacement and Routing Optimization for Circuits Derived from BDDs 2004 IEEE Int'l Symp. on Circuits and Systems , Seiten : V229 - V232 John P. Hayes, Ilia Polian, Bernd BeckerTesting for Missing-Gate Faults in Reversible Circuits 2004 IEEE Asian Test Symp. , Seiten : 100 - 105» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Logical reversibility occurs in low-power applications and is an essential feature of quantum circuits. Of special interest are reversible circuits constructed from a class of reversible elements called k-CNOT (controllable NOT) gates. We review the characteristics of k-CNOT circuits and observe that traditional fault models like the stuck-at model may not accurately represent their faulty behavior or test requirements. A new fault model, the missing gate fault (MGF) model, is proposed to better represent the physical failure modes of quantum technologies. It is shown that MGFs are highly testable, and that all MGFs in an N-gate k-CNOT circuit can be detected with from one to | N / 2 | test vectors. A design-for-test (DFT) method to make an arbitrary circuit fully testable for MGFs using a single test vector is described. Finally, we present simulation results to determine (near) optimal test sets and DFT configurations for some benchmark circuits. Piet Engelke, Ilia Polian, Michel Renovell, Bharath Seshadri, Bernd BeckerThe Pros and Cons of Very-Low-Voltage Testing: An Analysis Based on Resistive Short Defects 2004 VLSI Test Symp. , Seiten : 171 - 178 Piet Engelke, Ilia Polian, Michel Renovell, Bharath Seshadri, Bernd BeckerThe Pros and Cons of Very-Low-Voltage Testing: An Analytical View 2004 GI/ITG Workshop “Testmethoden und Zuverlässigkeit von Schaltungen und Systemen” , Seiten : 149 - 153 Yuyi Tang, Hans-Joachim Wunderlich, Harald Vranken, Friedrich Hapke, Michael Wittke, Piet Engelke, Ilia Polian, Bernd BeckerX-masking during logic BIST and its impact on defect coverage 2004 Int'l Test Conf. , Seiten : 442 - 451» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We present a technique for making a circuit ready for Logic BIST by masking unknown values at its outputs. In order to keep the silicon area cost low, some known bits in output responses are also allowed to be masked. These bits are selected based on a stuck-at n-detection based metric, such that the impact of masking on the defect coverage is minimal. An analysis based on a probabilistic model for resistive short defects indicates that the coverage loss for unmodeled defects is negligible for relatively low values of n. nach oben zur Jahresübersicht Tobias Schubert, Bernd BeckerPICHAFF: A Distributed SAT Solver for Microcontrollers 2003 Euromicro Conf. Thomas Eschbach, Wolfgang Günther, Bernd BeckerCrossing Reduction for Orthogonal Circuit Visualization 2003 Int'l Conf. on VLSI , CSREA Press, Seiten : 107 - 113 Marc Herbstritt, Bernd BeckerConflict-based Selection of Branching Rules 2003 Int'l Conf. on Theory and Applications of Satisfiability Testing , Springer, Band : 2919, Seiten : 441 - 451 Marc Herbstritt, Bernd BeckerConflict-based Selection of Branching Rules in SAT-Algorithms 2003 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” , Seiten : 189 - 198 Tobias Schubert, Bernd BeckerA Hardware Lab Anywhere At Anytime 2003 Int'l Conf. on Education and Information Systems: Technologies and Applications , Seiten : 130 - 135 Ilia Polian, Bernd BeckerConfiguring MISR-Based Two-Pattern BIST Using Boolean Satisfiability 2003 IEEE Design and Diagnostics of Electronic Circuits and Systems , Seiten : 73 - 80» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Most known two-pattern BIST architectures require prohibitive test application times in order to obtain high delay fault coverage. In an earlier work, a BIST TPG block based on a MISR expanding input vectors into test sequences of length 2^n has been refined such that shorter sequences could be used. By doing so, spectacular reductions of test application time were achieved. However, the procedures for computing input vectors were based on BDD-backed state traversal or extensive simulation, and their run-time requirements were tremendous. In this work, we propose a SAT-based input vector generation method, which leads to test application times that are similar to the earlier method, but with significantly reduced computational effort. For the first time, we present experimental results for larger ISCAS benchmarks, which previous methods could not treat. Furthermore, we discuss the application of our method when the requirement to apply the complete test pair set is relaxed. Tobias Schubert, Bernd BeckerDas Mobile Hardware-Praktikum 2003 European Conf. on Media in Higher Education Ilia Polian, Bernd Becker, Sudhakar M. ReddyEvolutionary Optimization of Markov Sources for Pseudo Random Scan BIST 2003 Conf. on Design, Automation and Test in Europe , Seiten : 1184 - 1185 Frank Schmiedle, Rolf Drechsler, Bernd BeckerExact Routing with Search Space Reduction 2003 IEEE Trans. on Computers , Band : 52, Nummer : 6, Seiten : 815 - 825 Ilia Polian, Piet Engelke, Michel Renovell, Bernd BeckerModelling Feedback Bridging Faults With Non-Zero Resistance 2003 European Test Workshop , Seiten : 91 - 96» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We study the behavior of feedback bridging faults with non-zero bridge resistance in both combinational and sequential circuits. We demonstrate that a test vector may detect the fault, not detect the fault or lead to oscillation, depending on bridge resistance. Moreover, the resistance intervals in which a particular behavior is observed are not necessarily contiguous. Even loops going through a gate with controlling values on its side inputs (which we call disabled loops) expose non-trivial behavior. We outline the multiple strengths problem which arises due to the fact that a critical bridge resistance depends on the strengths of the signals driving the bridge, which in turn are functions of the number of the on-transistors, these again depending on the bridge resistance, making such a fault very hard to resolve. For sequential circuits, we describe additional difficulties caused by the need to account for implications on bridge behavior, which have originated in the previous time frames. We conclude that the complexity of resistive feedback bridging fault simulation accurate enough to resolve such situations will probably be prohibitively high and propose possible simplifying assumptions. We present simulation results for ISCAS benchmarks using these assumptions with and without taking oscillation into account. Ilia Polian, Bernd BeckerMultiple Scan Chain Design for Two-Pattern Testing 2003 Jour. Electronic Testing , Band : 19, Nummer : 1, Seiten : 37 - 48» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Non-standard fault models often require the application of two-pattern testing. A fully-automated approach for generating a multiple scan chain-based architecture is presented so that two-pattern test sets generated for the combinational core can be applied to the sequential circuit. Test time and area overhead constraints are considered. Ilia Polian, Wolfgang Günther, Bernd BeckerPattern-Based Verification of Connections to Intellectual Property Cores 2003 INTEGRATION, the VLSI Jour. , Band : 35, Nummer : 1, Seiten : 25 - 44» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Verification of designs containing pre-designed cores is a challenging topic in modern IC design, since traditional approaches generally do not use the information that parts of the design (like IP cores) are already verified. The Port Order Fault Model (POF) has recently been introduced for detecting design errors occurring during integration of a core into a System-on-Chip or during test logic insertion. In this work, we generate verification patterns with 100 percent coverage of a sub-class of POF, called 2-POF. We provide theoretical arguments and experimental results backing the efficiency of these patterns also for detecting higher-order POFs. Moreover, verification pattern sets generated by our approach are more compact compared to the results published before. Martin Keim, M. Martin, Bernd Becker, Rolf Drechsler, Paul MolitorPolynomial Formal Verification of Multipliers 2003 Formal Methods in System Design , Band : 22, Nummer : 1, Seiten : 39 - 58 Ilia Polian, Bernd BeckerReducing ATE Cost in System-on-Chip 2003 IFIP VLSI-SoC , Seiten : 337 - 342 Ilia Polian, Bernd BeckerReducing ATE Cost in System-on-Chip Test 2003 GI/ITG Workshop “Testmethoden und Zuverlässigkeit von Schaltungen und Systemen” , Seiten : 34 - 37 Ilia Polian, Bernd BeckerReducing ATE Cost in System-on-Chip Test 2003 IEEE Int'l Workshop on Test Resource Partitioning » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Traditional SoC test scheduling approaches minimize test time under additional constraints. We argue that test costs are not determined by test time alone. Indeed, the speed of used ATE channels influences both cost and test time. We present a case for using a mixture of high-speed and low-cost ATE channels. Two heuristics and an exact algorithm are used. Experimental results show that such a mixture scenario can reduce the cost with no impact on test time. J. Bradford, H. Delong, Ilia Polian, Bernd BeckerSimulating Realistic Bridging and Crosstalk Faults in an Industrial Setting 2003 Jour. Electronic Testing , Band : 19, Nummer : 4, Seiten : 387 - 395» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Three different techniques for simulating realistic faults generated from IC layout are discussed. Two of them deal with bridging faults, and the third one handles crosstalk faults. The simulation is performed on top of a commercial simulator and thus is very well applicable in an industrial environment. No change of the design database and only minimal changes of the test shell are required. Experimental results are reported for a library cell and a block from a full-custom design. Piet Engelke, Ilia Polian, Michel Renovell, Bernd BeckerSimulating Resistive Bridging Faults 2003 GI/ITG Workshop “Testmethoden und Zuverlässigkeit von Schaltungen und Systemen” , Seiten : 92 - 97» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We present a simulator for resistive bridging and stuck-at faults. In contrast to earlier work, it is based on electrical equations rather than table look-up, thus exposing more flexibility. For the first time, simulation of sequential circuits is dealt with; reciprocal action of fault effects in current time frame and earlier time frames is elaborated on for different bridge resistances. Experimental results are given for resistive bridging and stuck-at faults in combinational and sequential circuits. Different definitions of fault coverage are listed and quantitative results with respect to all these definitions are given for the first time. Piet Engelke, Ilia Polian, Michel Renovell, Bernd BeckerSimulating Resistive Bridging and Stuck-At Faults 2003 Int'l Test Conf. , Seiten : 1051 - 1059 Piet Engelke, Ilia Polian, Michel Renovell, Bernd BeckerSimulating Resistive Bridging and Stuck-at Faults 2003 IEEE Int'l Workshop on Current and Defect-Based Testing , Seiten : 49 - 56» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We present a simulator for resistive bridging and stuck-at faults. In contrast to earlier work, it is based on electrical equations rather than table look-up, thus exposing more flexibility. For the first time, simulation of sequential circuits is dealt with; reciprocal action of fault effects in current time frame and earlier time frames is elaborated on for different bridge resistances. Experimental results are given for resistive bridging and stuck-at faults in combinational and sequential circuits. Different definitions of fault coverage are listed and quantitative results with respect to all these definitions are given for the first time. Ilia Polian, Wolfgang Günther, Bernd BeckerThe Case For 2-POF 2003 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” , Seiten : 164 - 173» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung The Port Order Fault Model (POF) has recently been introduced for detecting design errors occuring during integration of a core into a System-on-Chip or during test logic insertion. In an earlier work, we generated verification vectors with 100 percent coverage of a sub-class of POF, called 2-POF. Demonstrating empirically that these sets of verification vectors also cover an other sub-class of POF, 3-POF, almost completely, we concluded their efficiency also for higher-order POFs. In this paper, we provide theoretical arguments and more empirical results supporting the claim that verification vectors with high coverage of lower-order POFs are very likely to be also efficient in detecting higher-order POFs. Ilia Polian, Wolfgang Günther, Bernd BeckerThe Case For 2-POF 2003 IEEE Design and Diagnostics of Electronic Circuits and Systems , Seiten : 291 - 292 nach oben zur Jahresübersicht Christoph Scholl, Bernd BeckerChecking Equivalence for Circuits Containing Incompletely Specified Boxes 2002 Int'l Conf. on Computer Design , Seite : 56» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We consider the problem of checking whether an implementation which contains parts with incomplete information is equivalent to a given full specification. We study implementations which are not completely specified, but contain boxes which are associated with incompletely specified functions (called Incompletely Specified Boxes or IS--Boxes). After motivating the use of implementations with Incompletely Specified Boxes we define our notion of equivalence for this kind of implementations and present a method to solve the problem. A series of experimental results demonstrates the effectiveness and feasibility of the methods presented. Thomas Eschbach, Wolfgang Günther, Rolf Drechsler, Bernd BeckerCrossing Reduction by Windows Optimization 2002 Int'l Symp. on Graph Drawing , Band : 2528, Seiten : 285 - 294 Ilia Polian, Piet Engelke, Bernd BeckerEfficient Bridging Fault Simulation of Sequential Circuits Based on Multi-Valued Logics 2002 Int'l Symp. on Multi-Valued Logic , Seiten : 216 - 222» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We present the concept of a multi-valued logic simulator for bridging faults in sequential circuits. Different models for the handling of intermediate values in flip-flops on the digital design level can be integrated and result in an Expected realistic behavior area for bridging faults. Several experimental results are given to underline properties and advantages of the simulation technique Christoph Scholl, Bernd BeckerEquivalence Checking in the Presence of Incompletely Specified Boxes 2002 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We consider the problem of checking whether an implementation which contains parts with incomplete information is equivalent to a given full specification. We study implementations which are not completely specified, but contain boxes which are associated with incompletely specified functions (called Incompletely Specified Boxes or IS--Boxes). After motivating the use of implementations with Incompletely Specified Boxes we define our notion of equivalence for this kind of implementations and present a method to solve the problem. A series of experimental results demonstrates the effectiveness and feasibility of the methods presented. Ilia Polian, Irith Pomeranz, Bernd BeckerExact Computation of Maximally Dominating Faults and Its Application to n-Detection Tests 2002 IEEE Asian Test Symp. , Seiten : 9 - 14» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung n-detection test sets for stuck-at faults have been shown to be useful in detecting unmodeled defects. It was also shown that a set of faults, called maximally dominating faults, can play an important role in controlling the increase in the size of an n-detection test set as n is increased. In an earlier work, a superset of the maximally dominating fault set was used. In this work, we propose a method to determine exact sets of maximally dominating faults. We also define a new type of n-detection test sets based on the exact set of maximally dominating faults. We present experimental results to demonstrate the usefulness of this exact set in producing high-quality n-detection test sets. Ilia Polian, Irith Pomeranz, Bernd BeckerExact Computation of Maximally Dominating Faults and Its Application to n-Detection Tests 2002 European Test Workshop Ilia Polian, Bernd BeckerOptimal Bandwidth Allocation in Concurrent SoC Test Under Pin Number Constraints 2002 Workshop on RTL and High Level Testing , Seiten : 12 - 17» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung A method for assigning pins to cores in concurrent System-on-Chip testing is proposed. For each core, the number of assigned pins is traded for test application time using multiple scan chains. Given a pin number constraint, the overall test time is minimized. The used algorithm is formally proven to be optimal, although it has low polynomial computational complexity. The approach is applicable to any kind of testing which requires transport of test data from test equipment to the cores, including scan testing and scan-based BIST. J. Bradford, H. Delong, Ilia Polian, Bernd BeckerRealistic Fault Simulation in an Industrial Setting 2002 GI/ITG Workshop “Testmethoden und Zuverlässigkeit von Schaltungen und Systemen” Ilia Polian, Martin Keim, Nicolai Mallig, Bernd BeckerSequential n-Detection Criteria: Keep It Simple! 2002 IEEE Int'l Online Testing Workshop , Seiten : 189 - 190» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung The idea of n-detection is to exposure a target fault in n different ways. To denote several detections as `sufficiently different', formal criteria seem to be necessary. In this article, we study the properties of test sequences with respect to four new criteria, which we call difference types. We try to guide the n-detection test sequence generation process for stuck-at faults by difference types and evaluate coverage of a Surprisingly, we have found out that the effectiveness in detecting non-target faults is not affected beyond statistical noise. In our opinion this result underlines the effectiveness of n-detection without sophisticated differentiation criteria. J. Bradford, H. Delong, Ilia Polian, Bernd BeckerSimulating Realistic Bridging and Crosstalk Faults in an Industrial Setting 2002 European Test Workshop , Seiten : 75 - 80 Ilia Polian, Bernd BeckerStop & Go BIST 2002 IEEE Int'l Online Testing Workshop , Seiten : 147 - 151» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung A BIST method enabling two-pattern testing at-speed without violating thermal constraints by introducing cool down periods is proposed. The application of the method is demonstrated based on a scalable BIST architecture. Applicability on IP cores is given since only a two-pattern test set is required as input. Klaus-Jürgen Englert, Rolf Drechsler, Bernd BeckerVerification of HDLs using Symbolic Set Representation 2002 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” nach oben zur Jahresübersicht Wolfgang Günther, Andreas Hett, Bernd BeckerApplication of Linearly Transformed BDDs in Sequential Verification 2001 ASP Design Automation Conf. , Seiten : 91 - 96» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung The computation of the set of reachable states is the key problem of many applications in sequential verification. Binary Decision Diagrams (BDDs) are extensively used in this domain, but tend to blow up for larger instances. To increase the computational power of BDDs, linearly transformed BDDs (LTBDDs) have been proposed. In this paper we show how this concept can be incorporated into the sequential verification domain by restricting dynamic reordering in a way that the relational product can still be carried out efficiently. Experimental results are given to show the efficiency of our approach. Christoph Scholl, Bernd BeckerChecking Equivalence for Partial Implementations 2001 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” , Seiten : 31 - 43 Christoph Scholl, Bernd BeckerChecking Equivalence for Partial Implementations 2001 IEEE Design Automation Conference , IEEE Computer Society, Seiten : 238 - 243 Bernd Becker, Christoph Meinel, Masahiro Fujita, Fabio SomenziComputer Aided Design and Test, BDDs versus SAT, Dagstuhl-Seminar-Report 297, 28.01.-02.02.01 2001 Saarbrücken: Geschäftsstelle Schloss Dagstuhl Christoph Scholl, Marc Herbstritt, Bernd BeckerDon't Care Minimization of *BMDs: Complexity and Algorithms 2001 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” , Seiten : 45 - 57 Ilia Polian, Wolfgang Günther, Bernd BeckerEfficient Pattern-Based Verification of Connections to Intellectual Property Cores 2001 IEEE Asian Test Symp. , Seiten : 443 - 448» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Verification of designs containing pre-designed cores is a challenging topic in modern IC design, since traditional approaches generally do not use the information that parts of the design are already verified (like IP cores). To verify the connectivity between the surrounding design and IP cores, we propose a method that is based on test patterns. Using only those patterns for simulation, in almost all cases 100 percent of the errors can be detected. Existing test access logic is employed for the application of the patterns. A large set of experimental results is given to demonstrate the efficiency of the approach. Ilia Polian, Wolfgang Günther, Bernd BeckerEfficient Pattern-Based Verification of Connections to Intellectual Property Cores 2001 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” , Seiten : I:111 - 120 Christoph Scholl, Marc Herbstritt, Bernd BeckerExploiting Don't Cares to Minimize *BMDs 2001 IEEE Int'l Symp. on Circuits and Systems , Band : 5, Seiten : 191 - 194 Bernd Becker, Rolf Drechsler, Thomas Eschbach, Wolfgang GüntherGREEDY IIP: Partitioning Large Graphs by Greedy Iterative Improvement 2001 Euromicro Conf. , Seiten : 54 - 60 Ilia Polian, Bernd BeckerMultiple Scan Chain Design for Two-Pattern Testing 2001 VLSI Test Symp. , Seiten : 88 - 93 Ilia Polian, Bernd BeckerMultiple Scan Chain Design for Two-Pattern Testing 2001 Latin-American Test Workshop , Seiten : 156 - 161 Ilia Polian, Bernd BeckerMultiple Scan Chain Design for Two-Pattern Testing 2001 GI/ITG Workshop “Testmethoden und Zuverlässigkeit von Schaltungen und Systemen” Andreas Hett, Bernd BeckerSupervised Dynamic Reordering in Model Checking 2001 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” , Seiten : 21 - 30 Christoph Scholl, Bernd Becker, A. BrogleThe Multiple Variable Order Problem for Binary Decision Diagrams: Theory and Practical Application 2001 ASP Design Automation Conf. , Seiten : 85 - 90» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Reduced Ordered Binary Decision Diagrams (ROBDDs) gained widespread use in logic design verification, test generation, fault simulation, and logic synthesis [MWBS:88,Bry:92]. Since the size of an ROBDD heavily depends on the variable order used, there is a strong need to find variable orders that minimize the number of nodes in an ROBDD. In certain applications we have to cope with ROBDDs with different variable orders, whereas further manipulations of these ROBDDs require common variable orders. In this paper we give a theoretical background for this "Multiple Variable Order problem". Moreover, we solve the problem to transform ROBDDs with different variable orders into a good common variable order using dynamic variable ordering techniques. Frank Schmiedle, Daniel Große, Rolf Drechsler, Bernd BeckerToo Much Knowledge Hurts: Acceleration of Genetic Programs for Learning Heuristics 2001 Int'l Conf. on Computational Intelligence , Band : 2206, Seiten : 479 - 491» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Among many other applications, evolutionary methods have been used to develop heuristics for several optimization problems in VLSI CAD in recent years. Although learning is performed according to a set of training benchmarks, it is most important to generate heuristics that have a good generalization behaviour and hence are well suited to be applied to unknown examples. Besides large runtimes for learning, the major drawback of these approaches is that they are very sensitive to a variety of parameters for the learning process. In this paper, we study the impact of different parameters, like e.g. stopping conditions, on the quality of the results for learning heuristics for BDD minimization. If learning takes too long, the developed heuristics become too specific for the set of training examples and in that case results of application to unknown problem instances deteriorate. It will be demonstrated here that runtime can be saved while even improving the generalization behaviour of the heuristics. Frank Schmiedle, A. Markert, Bernd BeckerXMaDRE: A Routing Environment with Visualization based on Ray-Tracing 2001 Conf. on Design, Automation and Test in Europe nach oben zur Jahresübersicht Christoph Scholl, Bernd BeckerChecking Equivalence for Partial Implementations , Nummer : 145, 2000» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We consider the problem of checking whether a partial implementation can (still) be extended to a complete design which is equivalent to a given full specification. Several algorithms trading off accuracy and computational resources are presented: Starting with a simple 0,1,X-based simulation, which allows approximate solutions, but is not able to find all errors in the partial implementation, we consider more and more exact methods finally covering all errors detectable in the partial implementation. The exact algorithm reports no error if and only if the current partial implementation conforms to the specification, i.e. it can be extended to a full implementation which is equivalent to the specification. We give a series of experimental results demonstrating the effectiveness and feasibility of the methods presented. Christoph Scholl, Marc Herbstritt, Bernd BeckerExploiting Don't Cares to Minimize *BMDs , Nummer : 141, 2000» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We present for the first time methods to minimize *BMDs exploiting don't care conditions. These minimization methods can be used during the verification of circuits by *BMDs. By changing function values for input vectors, which are in the don't care set, smaller *BMDs can be computed to keep peak memory consumption during *BMD construction as low as possible. We determine the complexity of the problem of don't care minimization for *BMDs and thus justify the use of heuristics to approximate the solution. Preliminary experimental results prove our heuristcs to be very effective in minimizing *BMD sizes. Piet Engelke, Bernd Becker, Martin KeimA Parameterizable Fault Simulator for Bridging Faults 2000 European Test Workshop , Seiten : 63 - 68 Martin Keim, Piet Engelke, Bernd BeckerA Parameterizable Fault Simulator for Bridging Faults 2000 GI/ITG Workshop “Testmethoden und Zuverlässigkeit von Schaltungen und Systemen” Rolf Drechsler, Nicole Drechsler, Elke Mackensen, Tobias Schubert, Bernd BeckerDesign Reuse by Modularity: A Scalable Dynamical (Re)Configurable Multiprocessor System 2000 Euromicro Conf. , Seiten : 1:425 - 431 Andreas Hett, Christoph Scholl, Bernd BeckerDistance Driven Finite State Machine Traversal 2000 IEEE Design Automation Conference , Seiten : 39 - 42» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Symbolic techniques have revolutionized reachability analysis in the last years. Extending their applicability to handle large, industrial designs is a key issue, involving the need to focus on memory consumption for BDD representation as well as time consumption to perform symbolic traversals of Finite State Machines (FSMs). We address the problem of reachability analysis for large FSMs, introducing a novel technique that performs reachability analysis using a sequence of "distance driven" partial traversals based on dynamically chosen prunings of the transition relation. Experiments are given to demonstrate the efficiency and robustness of our approach: We succeed in completing reachability problems with significantly smaller memory requirements and improved time performance. Frank Schmiedle, D. Unruh, Bernd BeckerExact Switchbox Routing with Search Space Reduction 2000 Int'l Symp. on Physical Design , Seiten : 26 - 32» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We present an approach for exact switchbox routing that complements traditional routing techniques. It is particularly well suited for an application to dense problem instances and the completion of routing in subregions which turn out to be difficult for routing tools based on heuristic methods. The exact router proposed uses symbolic methods i.e. MDDs (Multi-valued Decision Diagrams) for representation of the routing space. All possible solutions to the routing problem are represented by one single MDD and once this MDD is given, routability can be decided within constant time. To reduce the search space of possible routing solutions, so-called forced cells are computed. Finally, experimental results are given. They show the feasibility and the practicability of the approach. Tobias Schubert, Elke Mackensen, Nicole Drechsler, Rolf Drechsler, Bernd BeckerSpecialized Hardware for Implementation of Evolutionary Algorithms 2000 Int'l Workshop on Boolean Problems , Seiten : 175 - 182 Tobias Schubert, Elke Mackensen, Nicole Drechsler, Rolf Drechsler, Bernd BeckerSpecialized Hardware for Implementation of Evolutionary Algorithms 2000 Conf. on Genetic and Evolutionary Computation , Seite : 369 Andreas Hett, Christoph Scholl, Bernd BeckerState Traversal guided by Hamming Distance Profiles 2000 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” , VDE Verlag, Seiten : 57 - 66 Rolf Drechsler, Wolfgang Günther, Bernd BeckerTestability of Circuits Derived from Lattice Diagrams 2000 Euromicro Conf. , Seiten : 188 - 192» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In this paper the testability of circuits derived from BDDs representing totally symmetric functions is analyzed. A test pattern generation technique is presented that has runtime linear in the size of the BDD. The result is directly applicable to circuits derived from lattice diagrams, a new design style that combines the synthesis and the layout step. Experimental results show that complete test generation for functions with more than 500 variables can be done in less than 1 CPU second. Rolf Drechsler, Wolfgang Günther, Bernd BeckerTestability of Circuits Derived from Lattice Diagrams 2000 Latin-American Test Workshop Wolfgang Günther, Nicole Drechsler, Rolf Drechsler, Bernd BeckerVerification of Designs Containing Black Boxes 2000 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Often modern designs contain regions where the implementation of certain components is not (fully) known. These regions are called black boxes in the following. They occur e.g. if different designers work on a project in parallel or if IP cores are used. In this paper an approach based on a symbolic representation of characteristic functions for verifying circuits with black boxes is presented. We show that by this method more faults can be detected than with pure binary simulation and symbolic simulation using BDDs, respectively, only. This results from the formulation of our algorithm that allows implications over the black box. Experimental results are given to show what parts of a design can be proven to be correct, if black boxes are assumed. Of course, the probability for the detection of a fault in general depends on the size of the unknown regions. But fault injection experiments on benchmarks show that for many circuits even up to 90 percent of the faults are detected, even though large parts of the design are unspecified. Wolfgang Günther, Nicole Drechsler, Rolf Drechsler, Bernd BeckerVerification of Designs Containing Black Boxes 2000 Euromicro Conf. , Seiten : 100 - 105» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Often modern designs contain regions where the implementation of certain components is not (fully) known. These regions are called black boxes in the following. They occur e.g. if different designers work on a project in parallel or if IP cores are used. In this paper an approach based on a symbolic representation of characteristic functions for verifying circuits with black boxes is presented. We show that by this method more faults can be detected than with pure binary simulation and symbolic simulation using BDDs, respectively, only. This results from the formulation of our algorithm that allows implications over the black box. Experimental results are given to show what parts of a design can be proven to be correct, if black boxes are assumed. Of course, the probability for the detection of a fault in general depends on the size of the unknown regions. But fault injection experiments on benchmarks show that for many circuits even up to 90 percent of the faults are detected, even though large parts of the design are unspecified. Wolfgang Günther, R. Schönfeld, Bernd Becker, Paul Molitork-Layer Straightline Crossing Minimization by Speeding up Sifting 2000 Graph Drawing Conf. , Springer Verlag, Band : 1984, Seiten : 253 - 258» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Recently, a technique called sifting, which is a well-known technique applied during formal logic verification and logic synthesis of digital circuits, has been proposed for k-layer straightline crossing minimization. This new approach has been proved to be very efficient. In particular it outperforms the traditional layer by layer sweep based heuristics by far when applied to k-layered graphs with k>=3. In this paper, we present two methods to speed up sifting. First, it is shown how the crossing matrix can be computed and updated efficiently. Then, we study lower bounds which can be incorporated in the sifting algorithm, allowing to prune large parts of the search space. Experimental results show that it is possible to speed up sifting by more than a factor of 20 using the new methods during the minimization process. nach oben zur Jahresübersicht Christoph Scholl, Bernd Becker, A. BrogleSolving the Multiple Variable Order Problem for Binary Decision Diagrams by Use of Dynamic Reordering Techniques , Nummer : 130, 1999» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Reduced Ordered Binary Decision Diagrams (ROBDDs) gained widespread use in logic design verification, test generation, fault simulation, and logic synthesis [MWBS:88,Bry:92]. Since the size of an ROBDD heavily depends on the variable order used, there is a strong need to find variable orders that minimize the number of nodes in an ROBDD. In certain applications we have to cope with ROBDDs with different variable orders, whereas further manipulations of these ROBDDs require common variable orders. In this paper we solve the problem to transform ROBDDs with different variable orders into a good common variable order. To do so, we make use of dynamic variable ordering techniques. Rolf Drechsler, Marc Herbstritt, Bernd BeckerGrouping Heuristics for Word-level Decision Diagrams 1999 IEEE Int'l Symp. on Circuits and Systems , Seiten : 411 - 415 Rolf Drechsler, Bernd BeckerProbabilistic IP Verification 1999 Int'l Workshop on Testing Embedded Core-based System-Chips Nicole Drechsler, Rolf Drechsler, Bernd BeckerA New Model for Multi-Objective Optimization in Evolutionary Algorithms 1999 Int'l Conf. on Computational Intelligence , Springer Verlag, Band : 1625, Seiten : 108 - 117» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Many optimization problems consist of several mutually dependent subproblems, where the resulting solutions must satisfy all requirements. We propose a new model for Multi-Objective Optimization (MOO) in Evolutionary Algorithms (EAs). The search space is partitioned into so-called Satisfiability Classes (SC), where each region represents the quality of the optimization criteria. Applying the SCs to individuals in a population a fitness can be assigned during the EA run. The model also allows the handling of infeasible regions and restrictions in the search space. Additionally, different priorities for optimization objectives can be modeled. Advantages of the model over previous approaches are discussed and an application is given that shows the superiority of the method for modeling MOO problems. Martin Keim, Ilia Polian, Harry Hengster, Bernd BeckerA Scalable BIST Architecture for Delay Faults 1999 European Test Workshop , Seiten : 98 - 103» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In this paper we present a scalable BIST (Built-In Self Test) architecture that provides a tunable trade-off between on-chip area demand and test execution time for delay fault testing. So, the architecture can meet test execution time requirements or available area requirements or any target in between. Experiments show the scalability of our approach, e.g. that considerably shorter test execution time can be achieved by storing only a few additional input vectors of the BIST architecture. The gain of test execution time possible with the proposed method ranges from a factor of 2 up to a factor of more than 800000. Andreas Hett, Christoph Scholl, Bernd BeckerA.MORE - A Multi-Operand BDD Package University of Freiburg, 1999» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Decision Diagrams (DDs) are often used in CAD systems for the efficient representation and manipulation of Boolean functions. The most popular data structure in this context are Ordered Binary Decision Diagrams (OBDDs) that are used in many applications. This package provides a novel approach for synthesizing BDDs using operator nodes instead of procedure calls. Thus, transformations on this data structure are possible as well as the flexibility to adapt the synthesis process in order to execute the 'most primising paths' first, resulting in less superfluous calculations and lower memory usage due to the skipping of unneeded branches. Martin Keim, Nicole Drechsler, Bernd BeckerCombining GAs and Symbolic Methods for High Quality Tests of Sequential Circuits 1999 ASP Design Automation Conf. , Seiten : 315 - 318 Bernd Becker, Christoph Meinel, Shin-Ichi Minato, Fabio SomenziComputer Aided Design and Test, Decision Diagrams - Concepts and Applications, (99041), Dagstuhl-Seminar-Report 229, 24.01.-29.1.1999 1999 Saarbrücken: Geschäftsstelle Schloss Dagstuhl Rolf Drechsler, Marc Herbstritt, Bernd BeckerGrouping Heuristics for Word-level Decision Diagrams 1999 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” , Shaker Verlag, Seiten : 41 - 50 Bernd Becker, Martin Keim, R. KriegerHybrid Fault Simulation for Synchronous Sequential Circuit 1999 Jour. Electronic Testing , Band : 3, Seiten : 219 - 238 Christoph Scholl, Bernd BeckerOn the Generation of Multiplexer Circuits for Pass Transistor Logic 1999 Int'l Workshop on Logic Synth. » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Pass Transistor Logic has attracted more and more interest during last years, since it has proved to be an attractive alternative to static CMOS designs with respect to area, performance and power consumption. Existing automatic PTL synthesis tools use a direct mapping of (decomposed) BDDs to pass transistors. Thereby, structural properties of BDDs like the ordering restriction and the fact that the select signals of the multiplexers (corresponding to BDD nodes) directly depend on input variables, are imposed on PTL circuits although they are not necessary for PTL synthesis. General Multiplexer Circuits can be used instead and should provide a much higher potential for optimization compared to a pure BDD approach. Nevertheless - to the best of our knowledge - an optimization of general Multiplexer Circuits (MCs) for PTL synthesis was not tried so far due to a lack of suitable optimization approaches. In this paper we present such an algorithm which is based on efficient BDD optimization techniques. Our experiments prove that there is indeed a high optimization potential by the use of general MCs - both concerning area and depth of the resulting PTL networks. Christoph Scholl, Bernd Becker, A. BrogleSolving the Multiple Variable Order Problem for Binary Decision Diagram by Use of Dynamic Reordering Techniques 1999 Int'l Workshop on Logic Synth. » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Reduced Ordered Binary Decision Diagrams (ROBDDs) gained widespread use in logic design verification, test generation, fault simulation, and logic synthesis [MWBS:88,Bry:92]. Since the size of an ROBDD heavily depends on the variable order used, there is a strong need to find variable orders that minimize the number of nodes in an ROBDD. In certain applications we have to cope with ROBDDs with different variable orders, whereas further manipulations of these ROBDDs require common variable orders. In this paper we solve the problem to transform ROBDDs with different variable orders into a good common variable order. To do so, we make use of dynamic variable ordering techniques. Christoph Scholl, Bernd Becker, A. BrogleSolving the Multiple Variable Order Problem for Binary Decision Diagram by Use of Dynamic Reordering Techniques , Nummer : 130, 1999» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Reduced Ordered Binary Decision Diagrams (ROBDDs) gained widespread use in logic design verification, test generation, fault simulation, and logic synthesis [MWBS:88,Bry:92]. Since the size of an ROBDD heavily depends on the variable order used, there is a strong need to find variable orders that minimize the number of nodes in an ROBDD. In certain applications we have to cope with ROBDDs with different variable orders, whereas further manipulations of these ROBDDs require common variable orders. In this paper we solve the problem to transform ROBDDs with different variable orders into a good common variable order. To do so, we make use of dynamic variable ordering techniques. Harry Hengster, Bernd BeckerSynthesis of Circuits Derived from Decision Diagrams - Combining Small Delay and Testability - 1999 Int'l Symp. on Defect and Fault Tolerance , Seiten : 268 - 275 Per Lindgren, Rolf Drechsler, Bernd BeckerSynthesis of Pseudo Kronecker Lattice Diagrams 1999 Int'l Conf. on Computer Design , Seiten : 307 - 310 nach oben zur Jahresübersicht Martin Keim, Nicole Göckel, Rolf Drechsler, Bernd BeckerCombining GAs and Symbolic Methods for High Quality Tests of Sequential Circuits , Nummer : 105/98, 1998» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung A symbolic fault simulator is integrated in a Genetic Algorithm (GA) environment to perform {Automatic Test Pattern Generation} (ATPG) for synchronous sequential circuits. In a two phase algorithm test length and fault coverage as well are optimized. However, there are circuits, that are hard to test using random pattern sequences, even if these sequences are genetically optimized. Thus, deterministic aspects are included in the GA environment to improve fault coverage. Experiments demonstrate that both a priori time consuming strategies can be combined at reasonable costs: Tests with higher fault coverages and considerably shorter test sequences than previously presented approaches are obtained. Rolf Drechsler, Bernd BeckerBinary Decision Diagrams - Theory and Implementation Kluwer Academic Publishers, 1998 Martin Keim, Nicole Drechsler, Rolf Drechsler, Bernd BeckerCombining GAs and Symbolic Methods for High Quality Tests of Sequential Circuits 1998 European Test Workshop , Seiten : 141 - 142 Rolf Drechsler, Bernd BeckerGraphenbasierte Funktionsdarstellung B.G. Teubner, 1998 Martin Keim, Bernd BeckerNearly Exact Signal Probabilities for Synchronous Sequential Circuits - An Experimental Analysis , Nummer : 106/98, 1998» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In this article we present a strategy how to estimate the signal probabilities for synchronous sequential circuits. For each line in the circuit an OBDDs is constructed only once. Using this OBDD the signal probabilities in every succeeding time frame is computed. We investigated a large set of the ISCAS'89 benchmark circuits, showing that the proposed strategy estimates 75 percent of all signals considered with a relative error of only 10 percent or less. Harry Hengster, Bernd BeckerSynthesis of Fully Testable High Speed Circuits Derived from Decision Diagrams 1998 GI/ITG Workshop “Testmethoden und Zuverlässigkeit von Schaltungen und Systemen” » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We present an approach to synthesize fully stuck-at fault testable circuits along with complete test sets. Starting from functional descriptions given by Kronecker Functional Decision Diagrams (KFDDs) circuits with inherently small delay are constructed by a composition method based on Boolean Matrix Multiplication. During the construction efficient algorithms working on the KFDD are used to avoid the creation of constant lines. Furthermore, in each composition step tests for the faults at the newly generated lines are computed on the fly. Experimental results are given to underline the efficiency of the methods. Harry Hengster, Bernd BeckerSynthesis of Fully Testable High Speed Circuits Derived from Decision Diagrams 1998 Int'l Workshop on Logic Synth. , Seiten : 341 - 345» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We present an EXOR-based synthesis approach to obtain fully stuck-at fault testable circuits along with complete test sets. Starting from functional descriptions given by Kronecker Functional Decision Diagrams (KFDDs) circuits with inherently small delay are constructed by a composition method based on Boolean Matrix Multiplication. During the construction efficient algorithms working on the KFDD are used to avoid the creation of constant lines. Furthermore, in each composition step tests for the faults at the newly generated lines are computed on the fly. Experimental results are given to underline the efficiency of the methods. Martin Keim, Nicole Drechsler, Rolf Drechsler, Bernd BeckerTest Generation for (Sequential) Multi-Valued Logic Networks based on Genetic Algorithm 1998 Int'l Symp. on Multi-Valued Logic , Seiten : 215 - 220 Martin Keim, Nicole Göckel, Rolf Drechsler, Bernd BeckerTest Generation for (Sequential) Multi-Valued Logic Networks based on Genetic Algorithm 1998 Int'l Symp. on Multi-Valued Logic Christoph Scholl, Bernd Becker, T. M. WeisWord-Level Decision Diagrams, WLCDs and Division 1998 Int'l Conf. on CAD , Seiten : 672 - 677» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Several types of Decision Diagrams (DDs) have been proposed for the verification of Integrated Circuits. Recently, word-level DDs like BMDs, *BMDs, HDDs, K*BMDs and *PHDDs have been attracting more and more interest, e.g., by using *BMDs and *PHDDs it was for the first time possible to formally verify integer multipliers and floating point multipliers of "significant" bitlengths, respectively. On the other hand, it has been unknown, whether division, the operation inverse to multiplication, can be efficiently represented by some type of word-level DDs. In this paper we show that the representational power of any word-level DD is too weak to efficiently represent integer division. Thus, neither a clever choice of the variable ordering, the decomposition type or the edge weights, can lead to a polynomial DD size for division. For the proof we introduce Word-Level Linear Combination Diagrams (WLCDs), a DD, which may be viewed as a "generic" word-level DD. We derive an exponential lower bound on the WLCD representation size for integer dividers and show how this bound transfers to all other word-level DDs. nach oben zur Jahresübersicht Nicole Göckel, Martin Keim, Rolf Drechsler, Bernd BeckerA Genetic Algorithm for Sequential Circuit Test Generation based on Symbolic Fault Simulation 1997 GI/ITG Workshop “Testmethoden und Zuverlässigkeit von Schaltungen und Systemen” » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We present a Genetic Algorithm (GA) for sequential circuit test generation. A Binary Decision Diagram (BDD) based fault simulator, i.e. a fault simulator that uses symbolic methods, is integrated in the GA environment. The fault simulator is used as a more accurate evaluation method. Experiments show that we can generate test patterns for circuits where all previously presented GA approaches fail. Additionally, we reduce the length of the test sequences. A comparison to the pure GA based approach shows the efficiency of this method. Nicole Göckel, Martin Keim, Rolf Drechsler, Bernd BeckerA Genetic Algorithm for Sequential Circuit Test Generation based on Symbolic Fault Simulation 1997 European Test Workshop Nicole Göckel, Rolf Drechsler, Bernd BeckerA Multi-Layer Detailed Routing Approach based on Evolutionary Algorithms 1997 Int'l Conf. on Evolutionary Computation , Seiten : 557 - 562» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In this paper we present an Evolutionary Algorithm (EA) for Detailed Routing Problems (DRPs), like the Channel Routing Problem and the Switchbox Routing Problem. We combine EAs with domain specific knowledge, i.e. the genetic operators make use of the rip-up and reroute technique. The algorithm can work with two-layer and multi-layer problem instances. The efficiency of our algorithm is demonstrated by application to multi-layer channel routing benchmarks. Instances with up to five layers, 130 columns, and more than 60 nets are considered. Rolf Drechsler, Nicole Göckel, Elke Mackensen, Bernd BeckerBEA: Specialized Hardware for Implementation of Evolutionary Algorithms 1997 Genetic Programming Conf. , Seite : 491 Bernd Becker, Randy Bryant, Masahiro Fujita, Christoph MeinelComputer Aided Design and Test, Decision Diagrams - Concepts and Applications, (9705), Dagstuhl-Seminar-Report 166, 27.01.-31.1.1997 1997 Saarbrücken: Geschäftsstelle Schloss Dagstuhl Bernd Becker, Rolf DrechslerDecision Diagrams in Synthesis - Algorithms, Applications and Extensions - 1997 Int'l Conf. on VLSI Design , Seiten : 46 - 50» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung An overview on Decision Diagrams (DDs), the state-of-the-art data structure in computer aided design of integrated circuits, is given. The overview is not complete in the sense that all DDs are considered, but we mention the most important with practical relevance. DDs are widely used and in the meantime have also been integrated in commercial tools. In the following special interest is devoted to the use of DDs in the area of synthesis. We also discuss the influence of DDs in other fields and outline future trends. Andreas Hett, Rolf Drechsler, Bernd BeckerFast and Efficient Construction of BDDs by reordering based Synthesis 1997 European Design and Test Conf. , Seiten : 168 - 175» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We present a new approach to symbolic simulation with BDDs. Our method uses Reordering Based Synthesis (RBS) whichallows the integration of dynamic variable ordering (even) within a single synthesis operation (e.g. an AND-operation). Thus huge peak sizes during the construction often can be avoided, and we obtain a method that, with no penalty in runtime, is more memory efficient than traditional ITE operator based symbolic simulation. The results are confirmed by experiments on a large set of benchmarks: We give a comparison to several previously published approaches and also consider some industrial benchmarks which are known to be hard to handle. Rolf Drechsler, Martin Keim, Bernd BeckerFault Simulation in Sequential Multi-Valued Logic Networks 1997 Int'l Symp. on Multi-Valued Logic , Seiten : 145 - 150» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In this paper we present a fault simulator for Sequential Multi-Valued Logic Networks (SMVLN). With this tool we investigate their Random Pattern Testability (RPT). We discuss a unified approach for fault models in SMVLNs and show, that it is possible to describe all static fault models with a global formalism. A large set of experimental results is given that demonstrates the efficiency of our approach. For the first time fault coverages for the Stuck-At Fault Model (SAFM) and Skew Fault Model (SKFM) for large sequential circuits are reported. Christoph Scholl, Rolf Drechsler, Bernd BeckerFunctional Simulation using Binary Decision Diagrams 1997 GI/ITG/GME Workshop “Methoden des Entwurfs und der Verifikation digitaler Systeme” » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In many verification techniques fast functional evaluation of a Boolean network is needed. We investigate the idea of using Binary Decision Diagrams (BDDs) for functional simulation. The area-time trade-off that results from different minimization techniques of the BDD is discussed. We propose new minimization methods based on dynamic reordering that allow smaller representations with (nearly) no runtime penalty. Christoph Scholl, Rolf Drechsler, Bernd BeckerFunctional Simulation using Binary Decision Diagrams 1997 Int'l Workshop on Logic Synth. » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In many verification techniques fast functional evaluation of a Boolean network is needed. We investigate the idea of using Binary Decision Diagrams (BDDs) for functional simulation. The area-time trade-off that results from different minimization techniques of the BDD is discussed. We propose new minimization methods based on dynamic reordering that allow smaller representations with (nearly) no runtime penalty. Rolf Drechsler, Bernd BeckerGraphenbasierte Funktionsdarstellung B.G. Teubner, 1997 Nicole Göckel, Rolf Drechsler, Bernd BeckerLearning Heuristics for OKFDD Minimization by Evolutionary Algorithms 1997 ASP Design Automation Conf. , Seiten : 469 - 472» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Ordered Kronecker Functional Decision Diagrams (OKFDDs) are a data structure for efficient representation and manipulation of Boolean functions. OKFDDs are very sensitive to the chosen variable ordering and the decomposition type list, i.e. the size may vary from linear to exponential. In this paper we present an Evolutionary Algorithm (EA) that learns good heuristics for OKFDD minimization starting from a given set of basic operations. The difference to other previous approaches to OKFDD minimization is that the EA does not solve the problem directly. Rather, it develops strategies for solving the problem. To demonstrate the efficiency of our approach experimental results are given. The newly developed heuristics combine high quality results with reasonable time overhead. C. Ökmen, Martin Keim, R. Krieger, Bernd BeckerOn Optimizing BIST Architecture by Using OBDD-based Approaches and Genetic Algorithms 1997 VLSI Test Symp. , Seiten : 426 - 431 Martin Keim, M. Martin, Bernd Becker, Rolf Drechsler, Paul MolitorPolynomial Formal Verification of Multipliers 1997 VLSI Test Symp. , Seiten : 150 - 155» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Until recently, verifying multipliers with formal methods was not feasible, even for small input word sizes. About two years ago, a new data structure, called Multiplicative Binary Moment Diagram (*BMD), was introduced for representing arithmetic functions over Boolean variables. Based on this data structure, methods were proposed by which verification of multipliers with input word sizes of up to 256 bits became now feasible. Only experimental data has been provided for these verification methods until now. In this paper we give a formal proof that logic verification using *BMDs is polynomially bounded in both space and time, when applied to the class of Wallace-tree like multipliers. Andreas Hett, Rolf Drechsler, Bernd BeckerReordering Based Synthesis 1997 iwrm » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Reordering Based Synthesis (RBS) as an alternative approach to manipulate Decision Diagrams (DDs) is presented. Based on the concept of operation nodes a single "core" operation, i.e. an extended Level Exchange (LE), is sufficient to perform the usual synthesis operations on several types of DDs. RBS allows the integration of dynamic variable ordering (even) within a single synthesis operation (e.g. an AND-operation) and thus provides the possibility of avoiding huge peak sizes during the construction. The optimization potential is significantly enlarged by allowing LEs even between operation nodes. A large number of experimental results for the Harry Hengster, Bernd BeckerSynthesis of Fully Testable High Speed Circuits Derived from Decision Diagrams , 1997» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We present an approach to synthesize fully stuck-at fault testable circuits along with complete test sets. Starting from functional descriptions given by Kronecker Functional Decision Diagrams (KFDDs) circuits with inherently small delay are constructed by a composition method based on Boolean Matrix Multiplication. During the construction efficient algorithms working on the KFDD are used to avoid the creation of constant lines. Furthermore, in each composition step tests for the faults at the newly generated lines are computed on the fly. Experimental results are given to underline the efficiency of the methods. Rolf Drechsler, Harry Hengster, H. Schäfer, J. Hartmann, Bernd BeckerTestability of 2-Level AND/EXOR Expressions 1997 European Design and Test Conf. , Seiten : 548 - 553» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung It is often stated that AND/EXOR circuits are much easier testable than AND/OR circuits. This statement only holds for restricted classes of AND/EXOR expressions, like positive polarity Reed-Muller expressions and fixed polarity Reed-Muller expressions. For these two classes of circuits good deterministic testability properties are known. In this paper we show that for these circuits also good random pattern testability can be proven. An input probability distribution is given which yields a short expected test length for biased random patterns. This is the first time that theoretical results on random pattern testability are presented for 2-level AND/EXOR circuit realizations of arbitrary Boolean functions. For more general classes of 2-level AND/EXOR circuits analogous results are not proven. We present experimental results that show that in general minimized 2-level AND/OR circuits are as well (or badly) testable as minimized 2-level AND/EXOR circuits. nach oben zur Jahresübersicht Rolf Drechsler, Bernd Becker, Nicole GöckelA Genetic Algorithm for the Construction of Small and Highly Testable OKFDD Circuits 1996 Genetic Programming Conf. , Seiten : 473 - 478» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung A Genetic Algorithm (GA) is applied to derive circuits that combine area efficiency and testability. These circuits are obtained from Ordered Kronecker Functional Decision Diagrams (OKFDDs). Previously a heuristic approach has been presented. In this paper we show how these results can further be improved by GAs. Finally, we apply our minimization algorithm to technology mapping for FPGAs. We present experimental results to show the efficiency of our approach. Nicole Göckel, G. Pudelko, Rolf Drechsler, Bernd BeckerA Hybrid Genetic Algorithm for the Channel Routing Problem 1996 IEEE Int'l Symp. on Circuits and Systems , Seiten : IV:675 - IV:678» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We present a Hybrid Genetic Algorithm (HGA) for the Channel Routing Problem (CRP). To do so we combine a Genetic Algorithm (GA) with domain specific knowledge, i.e. the genetic operators make use of the rip-up and reroute technique. Thereby the execution time of our method is faster than previously presented evolutionary based approaches. Furthermore, concerning space complexity we show by experiments that our HGA can handle large channels (with more than 100 columns). Rolf Drechsler, Andreas Hett, Bernd BeckerA Note on Symbolic Simulation using Desicion Diagrams 1996 ulsi » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung If Decision Diagrams (DDs) are used for the representation of the logical behaviour of a combinational logic circuit it has to be traversed in topological order. At each gate the corresponding synthesis operation is carried out. This traversal process is called symbolic simulation. Obviously the sequence in which the operations are performed at each gate influences the number of nodes needed during the computation. In this paper we consider different traversal strategies for OBDDs and OMDDs. We compare them by means of experiments. Harry Hengster, Rolf Drechsler, S. Eckrich, T. Pfeiffer, Bernd BeckerAND/EXOR based Synthesis of Testable KFDD-Circuits with Small Depth 1996 GI/ITG Workshop “Testmethoden und Zuverlässigkeit von Schaltungen und Systemen” » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Decision diagrams are used in design automation for efficient representation of Boolean functions. But it is also possible to derive circuits directly from decision diagrams. In this paper we present an approach to synthesize circuits from a very general class of decision diagrams, the ordered Kronecker functional decision diagrams. We investigate area, depth and testability of the synthesized circuits and compare them to circuit designs generated by other synthesis tools. Experimental results show that the presented approach is suitable to overcome the trade-off between depth and testability. Harry Hengster, Rolf Drechsler, S. Eckrich, T. Pfeiffer, Bernd BeckerAND/EXOR based Synthesis of Testable KFDD-Circuits with Small Depth 1996 IEEE Asian Test Symp. , Seiten : 148 - 154» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Decision Diagrams are used in design automation for efficient representation of Boolean functions. It is also possible to directly derive circuits from Decision Diagrams. In this paper we present an approach to synthesize circuits from a very general class of Decision Diagrams, the ordered Kronecker Functional Decision Diagrams. These Decision Diagrams make use of Davio decompositions which are based on exclusive-or operations and therefore allow the use of EXOR gates in the synthesized circuits. We investigate area, depth, and testability of these circuits and compare them to circuit designs generated by other synthesis tools. Experimental results show that the presented approach is suitable to overcome the trade-off between depth and testability at the price of reasonable area overhead. Bernd Becker, Rolf DrechslerExact Minimization of Kronecker Expressions for Symmetric Functions 1996 IEEE Int'l Symp. on Circuits and Systems , Seiten : IV:388 - IV:391 Rolf Drechsler, H. Esbensen, Bernd BeckerGenetic Algorithms in Computer Aided Design of Integrated Circuits 1996 Online Workshop on Evolutionary Computation Rolf Drechsler, Nicole Göckel, Bernd BeckerLearning Heuristics for OBDD Minimization by Evolutionary Algorithms 1996 Parallel Problem Solving from Nature , Springer Verlag, Band : 1141, Seiten : 730 - 739» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Ordered Binary Decision Diagrams (OBDDs) are the state-of-the-art data structure in CAD for ICs. OBDDs are very sensitive to the chosen variable ordering, i.e. the size may vary from linear to exponential. In this paper we present an Evolutionary Algorithm (EA) that learns good heuristics for OBDD minimization starting from a given set of basic operations. The difference to other previous approaches to OBDD minimization is that the EA does not solve the problem directly. Rather, it developes strategies for solving the problem. To demonstrate the efficiency of our approach experimental results are given. The newly developed heuristics are more efficient than other previously presented methods. Harry Hengster, U. Sparmann, Bernd Becker, Sudhakar M. ReddyLocal Transformations and Robust Dependent Path Delay Faults 1996 GI/ITG Workshop “Testmethoden und Zuverlässigkeit von Schaltungen und Systemen” » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Local transformations are used in several synthesis approaches. During application of such transformations attention has to be paid to many important properties, e.g. area, speed, power consumption, and testability. In this paper we study relations between local transformations and delay fault testability. In delay testing it is not necessary to test every path in a circuit to ascertain correct timing behavior. For example, a set of robust dependent path delay faults need not to be considered for testing if all paths that are not robust dependent are tested. We will present sufficient conditions for local transformations which ensure that a test set for all non-robust-dependent paths in the original circuit is also a test set for all non-robust-dependent paths in the transformed circuit. These conditions are applied to some local transformations which are often used in logic synthesis and it is shown that they preserve testability. The impact of local transformations on robust dependent testability is demonstrated by experimental results performed on benchmark circuits. Harry Hengster, U. Sparmann, Bernd Becker, Sudhakar M. ReddyLocal Transformations and Robust Dependent Path Delay Faults 1996 European Test Workshop » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Local transformations are used in several synthesis approaches. During application of such transformations attention has to be paid to many important properties, e.g. area, speed, power consumption, and testability. In this paper we study relations between local transformations and delay fault testability. In delay testing it is not necessary to test every path in a circuit to ascertain correct timing behavior. For example, a set of robust dependent path delay faults need not to be considered for testing if all paths that are not robust dependent are tested. We present sufficient conditions for local transformations which ensure that a test set for all non-robust-dependent paths in the original circuit is also a test set for all non-robust-dependent paths in the transformed circuit. These conditions are applied to some local transformations which are often used in logic synthesis and it is shown that they preserve testability. The impact of local transformations on robust dependent testability is demonstrated by experimental results performed on benchmark circuits. Harry Hengster, U. Sparmann, Bernd Becker, Sudhakar M. ReddyLocal Transformations and Robust Dependent Path Delay Faults 1996 Int'l Test Conf. » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Local transformations are used in several synthesis approaches. During application of such transformations attention has to be paid to many important properties, e.g. area, speed, power consumption, and testability. In this paper we study relations between local transformations and delay fault testability. In delay testing it is not necessary to test every path in a circuit to ascertain correct timing behavior. For example, a set of robust dependent path delay faults need not be considered for testing if all paths that are not robust dependent are tested. We present sufficient conditions for local transformations which ensure that a test set for all non-robust-dependent paths in the original circuit is also a test set for all non-robust-dependent paths in the transformed circuit. These conditions are applied to some local transformations which are often used in logic synthesis and it is shown that they preserve testability. The impact of local transformations on robust dependent testability is demonstrated by experimental results performed on benchmark circuits. Andreas Hett, Rolf Drechsler, Bernd BeckerMORE Optimization Techniques. , 1996 Rolf Drechsler, Bernd BeckerOKFDDs - Algorithms, Applications and Extensions Kluwer Academic Publisher, Seiten : 163 - 190, 1996 Bernd Becker, Rolf Drechsler, Reinhard EndersOn the Computational Power of Bit-Level and Word-Level Decision Diagrams 1996 GI/ITG/GME Workshop “Methoden des Entwurfs und der Verifikation digitaler Systeme” » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Several types of Decision Diagrams (DDs) have have been proposed in the area of Computer Aided Design (CAD), among them being bit-level DDs like OBDDs, OFDDs and OKFDDs. While the aforementioned types of DDs are suitable for representing Boolean functions at the bit-level and have proved useful for a lot of applications in CAD, recently DDs to represent integer-valued functions, like MTBDDs (=ADDs), EVBDDs, FEVBDDs, (*)BMDs, HDDs (=KBMDs), and K*BMDs, attract more and more interest, e.g., using *BMDs it was for the first time possible to verify multipliers of bit length up to n=256. In this paper we clarify the computational power of these DD classes. Several (inclusion) relations and (exponential) gaps between specific classes differing in the availability of additive and/or multiplicative edge weights and in the choice of decomposition types are shown. It turns out for example, that K(*)BMDs, a generalization of OKFDDs to the word-level, also "include" OBDDs, MTBDDs and (*)BMDs. On the other hand, it is demonstrated that a restriction of the K(*)BMD concept to subclasses, such as OBDDs, MTBDDs, (*)BMDs as well, results in families of functions which lose their efficient representation. Rolf Drechsler, Harry Hengster, H. Schäfer, Bernd BeckerTestability of AND/EXOR Expressions 1996 European Test Workshop » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung It is often stated that AND/EXOR circuits are much easier testable than AND/OR circuits. In this paper we show that this is not true for all 2-level circuits based on EXOR. The statement only holds for restricted classes of AND/EXOR expressions, like Positive Polarity Reed-Muller Expressions and Fixed Polarity Reed-Muller Expressions. AND/EXOR circuits are studied with respect to deterministic and random pattern testability. We present experimental results that show that in general minimized 2-level AND/OR circuits are as well (or badly) testable as minimized 2-level AND/EXOR circuits. Andreas Hett, Rolf Drechsler, Bernd BeckerThe DD Package PUMA - An Online Documentation https://ira.informatik.uni-freiburg.de/software/puma/, 1996» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Decision Diagrams (DDs) are often used in CAD systems for the efficient representation and manipulation of Boolean functions. The most popular data structure in this context are Ordered Binary Decision Diagrams (OBDDs) that are used in many applications. Nevertheless, some relevant classes of Boolean functions cannot be represented efficiently by OBDDs. As one alternative Ordered Functional Decision Diagrams (OFDDs) have been introduced and in the meantime they are used in various applications of XOR-based logic synthesis. Recently, Ordered Kronecker Functional Decision Diagrams (OKFDDs) have been introduced as a means for efficient representation and manipulation of Boolean functions. OKFDDs are a generaliziation of OBDDs and OFDDs as well and try to combine the advantages of both representations. The data structure allows to dynamically adapt the representation of a Boolean function to a given problem. Using OKFDDs it is possible to represent functions efficiently that only have exponentially sized OBDD and OFDD representations. <BR><BR> PUMA is a DD-Package for the efficient representation and manipulation of Boolean Functions with OKFDDs as well as Zero-Suppressed BDDs. nach oben zur Jahresübersicht Rolf Drechsler, Bernd Becker, Nicole GöckelA Genetic Algorithm for 2-Level AND/EXOR Minimization 1995 SASIMI , Seiten : 49 - 56» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We show that there is a close relation between Ordered Kronecker Functional Decision Diagrams (OKFDDs) and 2-level AND/EXOR Expressions. This relation together with efficient OKFDD algorithms can be utilized for exact and heuristic minimization of these AND/EXOR expressions, called Reduced Kronecker Expressions (RKROs). We propose several (exact and heuristical) minimization algorithms and demonstrate the efficiency of our approach by experimental results. A Genetic Algorithm (GA) is applied to minimize RKROs. Minimized RKROs are determined for benchmark functions with up to 100 variables. Furthermore, we compare our solutions to results obtainable for other classes of 2-level AND/EXOR forms. In particular, AND/EXOR expressions derived from OKFDDs turn out to be much smaller than the well-known class of Fixed-Polarity Reed-Muller Expressions (FPRMs), although the complexity of the minimization algorithms is comparable. Our GA approach is a practical alternative to the exact algorithm. It produced optimal results for all considered benchmarks, but it is also applicable to functions with more than 20 variables due to its short runtimes. Rolf Drechsler, Bernd Becker, Nicole GöckelA Genetic Algorithm for Variable Ordering of OBDDs 1995 Int'l Workshop on Logic Synth. , Seiten : 5c:5.55 - 5.64» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung A Genetic Algorithm (GA) is applied to find a variable ordering that minimizes the size of Ordered Binary Decision Diagrams (OBDDs). OBDDs are a data structure for representation and manipulation of Boolean functions often applied in CAD. The choice of the variable ordering largely influences the size of the OBDD, i.e. its size may vary from polynomial to exponential. Dynamic variable ordering is the state-of-the-art method for finding good variable orderings. In this paper we show by experimental results that better sizes can be obtained using GAs. Our GA approach is a practical alternative to the exact algorithm for variable ordering. It produced optimal results for most considered benchmarks, but it is also applicable to functions with more than 20 variables due to its short runtimes. Rolf Drechsler, Bernd Becker, Nicole GöckelA Genetic Algorithm for Variable Ordering of OBDDs , Nummer : 5/95, 1995 Harry Hengster, Rolf Drechsler, Bernd BeckerAND/OR/EXOR based Synthesis of KFDD-Circuits with Small Depth 1995 Reed-Muller Colloquium UK » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Construction of circuits from Decision Diagrams (DDs) has shown several advantages, e.g. the resulting circuits have nice testability properties. One major drawback of circuits derived from ordered DDs is that their depth is proportional to the number of inputs. In this paper we present an approach to design DD circuits derived from Kronecker Functional DDs (KFDDs) with small depth. Experimental results are given that show the efficiency of our approach. Bernd Becker, Randal Bryant, Olivier Coudert, Christoph MeinelComputer Aided Design and Test, Dagstuhl-Seminar-Report 105 (9507), 13.2.1995 - 17.2.1995 1995 Saarbrücken: Geschäftsstelle Schloss Dagstuhl Rolf Drechsler, Bernd Becker, S. RuppertzDynamic Minimization of K*BMDs , 1995 Rolf Drechsler, Bernd BeckerDynamic Minimization of OKFDDs , Nummer : 5/95, 1995 Bernd Becker, Rolf DrechslerExact Minimization of Kronecker Expressions for Symmetric Functions 1995 IFIP WG 10.5 Workshop on Applications of the Reed-Muller Expansion in Circuit Design , Seiten : 240 - 245 R. Krieger, Bernd Becker, R. SinkovićNecessary Assignments for an Accelerated OBDD-based Computation of Exact Fault Detection Probabilities 1995 GI/ITG Workshop “Testmethoden und Zuverlässigkeit von Schaltungen und Systemen” R. Krieger, Bernd Becker, C. ÖkmenOBDD-based Optimization of Input probabilities for weighted random test 1995 Int'l Symp. on Defect and Fault Tolerance , Seiten : 120 - 129 Bernd Becker, Rolf Drechsler, M. TheobaldOKFDDs versus OBDDs and OFDDs 1995 ICALP , Springer Verlag, Band : 944, Seiten : 475 - 486» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Ordered Decision Diagrams (ODDs) as a means for the representation of Boolean functions are used in many applications in CAD. Depending on the decomposition type, various classes of ODDs have been defined, the most important being the Ordered Binary Decision Diagrams (OBDDs), the Ordered Functional Decision Diagrams (OFDDs) and the Ordered Kronecker Functional Decision Diagrams (OKFDDs). In this paper we clarify the computational power of OKFDDs versus OBDDs and OFDDs from a (more) theoretical point of view. We prove several exponential gaps between specific types of ODDs. Combining these results it follows that a restriction of the OKFDD concept to subclasses, such as OBDDs and OFDDs as well, results in families of functions which lose their efficient representation. Bernd Becker, Rolf Drechsler, Reinhard EndersOn the Computational Power of Bit-Level and Word-Level Decision Diagrams , 1995 Bernd Becker, Rolf Drechsler, R. WerchnerOn the Relation Between BDDs and FDDs 1995 Information and Computation , Band : 123(2), Seiten : 185 - 197 Rolf Drechsler, Bernd BeckerPUMA: An OKFDD-Package and its Implementation 1995 European Design and Test Conf. R. Krieger, Bernd Becker, Martin KeimSymbolic Fault Simulation for Sequential Circuits and the Multiple Observation Time Test Strategy 1995 IEEE Design Automation Conference , Seiten : 339 - 344» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Fault simulation for synchronous sequential circuits is a very time-consuming task. The complexity of the task increases if there is no information about the initial state of the circuit. In this case an unknown initial state is assumed which is usually handled by introducing a three-valued logic. As it is well-known fault simulation based on this logic only determines a lower bound of the fault coverage. Recently it was shown that fault simulation based upon the multiple observation time test strategy can improve the accuracy of the fault coverage. In this paper we describe how this strategy can be successfully implemented based on Ordered Binary Decision Diagrams. Our experiments demonstrate the efficiency of the fault simulation procedure developed. Bernd Becker, Rolf DrechslerSynthesis for Testability: Circuits Derived from Ordered Kronecker Functional Decision Diagrams 1995 European Design and Test Conf. , Seite : 592» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Testability properties of circuits derived from Ordered Kronecker Functional Decision Diagrams (OKFDDs) are studied with respect to the Stuck-At Fault Model (SAFM) and the Cellular Fault Model (CFM). The computation of complete test sets and of all occuring redundancies can be done easily and efficiently and circuits with high testability can be obtained. The full paper including experimental results can be obtained from the authors. nach oben zur Jahresübersicht Rolf Drechsler, M. Theobald, Bernd BeckerFast FDD based Minimization of Generalized Reed-Muller Forms 1994 Workshop über Komplexitätstheorie, Datenstrukturen und effiziente Algorithmen Workshop über Komplexitätstheorie, Datenstrukturen und effiziente Algorithmen Rolf Drechsler, H. Esbensen, Bernd BeckerGenetic Algorithms in Computer Aided Design of Integrated Circuits , Nummer : 17/94, 1994» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung An increasing number of successful applications of Genetic Algorithms (GAs) within Computer Aided Design (CAD) of Integrated Circuits (ICs) is reported in the literature. The problems dealt with in this field consist of sequences of sub-problems, which are characterized by being NP-hard, large and mutually dependent. This very high level of complexity should make the GA a well suited approach, at least in principle. However, the GA is of practical interest to the CAD community if and only if it is competitive to the existing approaches with respect to performance. With this fact as the starting point, the purpose of this paper is to discuss how to develop high-performance GAs for CAD of ICs . After reviewing a number of recent, performance competitive GAs for key problems in CAD of ICs, the common characteristics of these algorithms are discussed. They all exploit problem specific knowledge in various ways or are integrated with other heuristics. The paper also discusses performance evaluation principles. To make an impact, it is crucial that performance is evaluated using the measures commonly applied in the CAD field. The practical implications hereof for GA-based applications are addressed. Bernd Becker, Rolf Drechsler, M. TheobaldMinimization of 2-level AND/XOR Expressions using Ordered Kronecker Functional Decision Diagrams , Nummer : 3/94, 1994 Rolf Drechsler, Bernd Becker, A. JahnkeOn Variable Ordering and Decomposition Type Choice in OKFDDs 1994 Workshop über Komplexitätstheorie, Datenstrukturen und effiziente Algorithmen Rolf Drechsler, Bernd Becker, A. JahnkeOn Variable Ordering and Decomposition Type Choice in OKFDDs , Nummer : 11/94, 1994 Bernd Becker, Rolf Drechsler, M. TheobaldOn Variable Ordering of Functional Decision Diagrams , Nummer : TR-94-006, 1994 Bernd Becker, Rolf Drechsler, M. TheobaldOn Variable Ordering of Ordered Functional Decision Diagrams 1994 GI/GME/ITG-Fachtagung “Rechnergestützter Entwurf und Architektur mikroelektronischer Systeme” , Springer Verlag, Seiten : 62 - 71 Rolf Drechsler, A. Sarabi, M. Theobald, Bernd Becker, M. A. PerkowskiOn the Computational Power of Ordered Kronecker Functional Decision Diagrams , Nummer : 4/94, 1994 Rolf Drechsler, A. Sarabi, M. Theobald, Bernd Becker, M. A. PerkowskiOrdered Kronecker Functional Decision Diagrams: An Efficient Tool for Synthesis and Verification 1994 GI/ITG Workshop “Anwendung formaler Methoden im Systementwurf” Bernd Becker, Rolf DrechslerSynthesis for Testability: Circuits Derived from Ordered Kronecker Functional Decision Diagrams 1994 Int'l Test Synthesis Workshop Bernd Becker, Rolf DrechslerSynthesis for Testability: Circuits Derived from Ordered Kronecker Functional Decision Diagrams , Nummer : 14/94, 1994 Harry Hengster, Rolf Drechsler, Bernd BeckerTestability Properties of Local Circuit Transformations with Respect to the Robust Path-Delay-Fault Model 1994 Int'l Conf. on VLSI Design , Seiten : 123 - 126» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We present a new approach to show that local circuit transformations which improve the area of a circuit preserve or improve robust path-delay-fault testability. In contrast to previously published methods which had to consider the whole circuit we examine only the subcircuits to be transformed. Furthermore, we present some transformations which preserve or improve testability. Bernd Becker, Rolf DrechslerTestability of Circuits Derived from Functional Decision Diagrams 1994 European Design and Test Conf. , Seite : 667» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We investigate the testability properties of Boolean networks derived from a special class of multi-level AND/ EXOR expressions, called ordered functional decicision diagrams (OFDDs). We consider the stuck-at fault model (SAFM) and the cellular fault model (CFM). All occuring redundancies are classified. The resulting circuits are highly testable with nearly 100% fault coverage on average. The full paper including all experimental results can be obtained from the authors. nach oben zur Jahresübersicht Bernd Becker, Rolf Drechsler, Harry Hengster, R. Krieger, R. SinkovićBinary Decision Diagrams and Testing 1993 GI/ITG Workshop “Testmethoden und Zuverlässigkeit von Schaltungen und Systemen” » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Binary Decision Diagrams (BDD's) can be successfully applied to a wide variety of tasks in digital system design, verification and testing. In this paper we focus on the area of testing and demonstrate how two key problems, the computation of signal and fault detection probabilities and the synthesis of testable circuits, can profit from a BDD-based approach. Bernd Becker, Randal Bryant, Christoph MeinelComputer Aided Design and Test: 15.2.1993-19.2.1993 (9307), Dagstuhl Seminar Report 56 1993 Saarbrücken: Geschäftsstelle Schloss Dagstuhl Rolf Drechsler, A. Sarabi, M. Theobald, Bernd Becker, M. A. PerkowskiEfficient Representation and Manipulation of Switching Functions Based on Ordered Kronecker Functional Decision Diagrams , Nummer : 14/93, 1993 Rolf Drechsler, M. Theobald, Bernd BeckerFast FDD based Minimization of Generalized Reed-Muller Forms , Nummer : 15/93, 1993 Bernd Becker, Rolf Drechsler, Harry HengsterLocal Circuit Transformations Preserving Robust Path-Delay-Fault Testability , Nummer : 1/93, 1993 Bernd Becker, Rolf Drechsler, Paul MolitorOn Generation of Area-Time Optimal Testable Adders 1993 Technical Report 3/93 Bernd Becker, Rolf Drechsler, M. TheobaldOn Variable Ordering of Functional Decision Diagrams , 1993 Bernd Becker, Rolf DrechslerOn the Computational Power of Functional Decision Diagrams 1993 Workshop über Komplexitätstheorie, Datenstrukturen und effiziente Algorithmen Workshop über Komplexitätstheorie, Datenstrukturen und effiziente Algorithmen Bernd Becker, Rolf Drechsler, M. TheobaldOn the Implementation of a Package for Efficient Representation and Manipulation of Functional Decision Diagrams 1993 IFIP WG 10.5 Workshop on Applications of the Reed-Muller Expansion in Circuit Design , Seiten : 162 - 169 Bernd Becker, Rolf Drechsler, R. WerchnerOn the Relation between BDDs and FDDs , Nummer : 12/93, 1993 Bernd Becker, Rolf Drechsler, Christoph MeinelOn the Testability of Circuits Derived from Binary Decision Diagrams , Nummer : 9/93, 1993 Rolf Drechsler, Bernd BeckerRapid Prototyping of Fully Testable Multi-Level AND/EXOR Networks 1993 IFIP WG 10.5 Workshop on Applications of the Reed-Muller Expansion in Circuit Design , Seiten : 126 - 133 Bernd Becker, Rolf DrechslerTestability of Circuits Derived from Functional Decision Diagrams , 1993 Ralf Hahn, Bernd Becker, Harry HengsterThe Fault Graph and its Application to Combinational Fault Simulation 1993 GI/ITG Workshop “Testmethoden und Zuverlässigkeit von Schaltungen und Systemen” » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung The fault graph is a data structure to store faults and to manage relations between faults. It allows to exploit these relations for testing purposes and to control the order of faults considered. To demonstrate the effectiveness of the fault graph we developed an algorithm for fault simulation in combinational circuits that is based on this data structure. The algorithm is conceptually simple. Experiments show that it is superior to a sophisticated fanout oriented fault simulation algorithm. R. Krieger, Bernd Becker, Harry Hengsterlgc++: Ein Werkzeug zur Implementierung von Logiken als abstrakte Datentypen in C++ , 1993 R. Krieger, Ralf Hahn, Bernd Beckertest_circ: Ein abstrakter Datentyp zur Repräsentation von hierarchischen Schaltkreisen , 1993 nach oben zur Jahresübersicht Rolf Drechsler, Bernd Becker, Paul MolitorA Performance Oriented Generator for Robust Path-Delay-Fault Testable Adders 1992 GI/ITG Workshop “Testmethoden und Zuverlässigkeit von Schaltungen und Systemen” Bernd Becker, Rolf Drechsler, Paul MolitorOn the Implementation of an Efficient Performance Driven Generator for Conditional-Sum-Adders. 1992 Technical Report 2/93 Rolf Drechsler, Bernd BeckerRapid Prototyping of Robust Path-Delay-Fault Testable Circuits Derived from Binary Decision Diagrams , Nummer : TR-17/92, SFB 124, 1992 nach oben zur Jahresübersicht Bernd Becker, Christoph MeinelEntwerfen, Prüfen, Testen: 18.2.1991-22.2.1991 (9108), Dagstuhl-Seminar-Report 6 1991 Saarbrücken: Geschäftsstelle Schloss Dagstuhl nach oben zur Jahresübersicht Bernd Becker, U. SparmannA Uniform Test Approach for RCC-Adders 1988 Aegean Workshop on Parallel Computation and VLSI Theory , Springer Verlag, Band : 319, Seiten : 288 - 300 nach oben zur Jahresübersicht Bernd BeckerAn Easily Testable Optimal-Time VLSI-Multiplier 1987 Acta Informatica , Band : 24, Seiten : 363 - 380 Bernd Becker, G. Hotz, R. Kolla, Paul Molitor, H. G. OsthofCADIC - Ein System zum hierarchischen Entwurf integrierter Schaltungen 1987 E.I.S.-Workshop , Seiten : 235 - 245 Bernd Becker, H. G. OsthofLayouts with Wires of Balanced Length 1987 Information and Computation , Band : 73(1), Seiten : 45 - 58 nach oben zur Jahresübersicht Bernd Becker, G. Hotz, R. Kolla, Paul MolitorEin logisch-topologischer Kalkül zur Konstruktion von integrierten Schaltkreisen 1986 INFORMATIK Forschung und Entwicklung 1 , Seite : 38--47,72- nach oben zur Jahresübersicht Bernd BeckerOn the Crossing-free, Rectangular Embedding of Weighted Graphs in the Plane 1983 Theor. Comput. Sci., GI-Conf. , Springer Verlag, Band : 145, Seiten : 61 - 72