Matthias Sauer, Dr.
Technische Fakultät Albert-Ludwigs-Universität Georges Köhler Allee, Gebäude 51 79110 Freiburg im Breisgau Deutschland
Gebäude 51, Raum 01..031
++49 +761 203-8143
sauerm@informatik.uni-freiburg.de
Matthias Sauer
Liste filtern : Jahre: 2018 |
2017 |
2016 |
2015 |
2014 |
2013 |
2012 |
2011 | alle anzeigen nach oben zur Jahresübersicht Pascal Raiola, Michael Kochte, Ahmed Atteya, Laura Rodriguez Gomez, Hans-Joachim Wunderlich, Bernd Becker, Matthias SauerDetecting and Resolving Security Violations in Reconfigurable Scan Networks 2018 IEEE Int'l Online Testing Symp 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” 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” nach oben zur Jahresübersicht 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 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 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. nach oben zur Jahresübersicht 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) Mathias Soeken, Pascal Raiola, Baruch Sterin, Matthias SauerSAT-based Functional Dependency Computation 2016 International Workshop on Logic & Synthesis 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 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, 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 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” 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. Linus Feiten, Matthias SauerExtracting the RC4 secret key of the Open Smart Grid Protocol (OSGP) 2015 Industrial Control System Security (ICSS) Workshop » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung The Open Smart Grid Protocol (OSGP) is a widely used industry standard for exchanging sensitive data between devices inside of smart grids. For message confidentiality, OSGP implements a customised form of the RC4 stream cipher. In this work, we show how already known weaknesses of RC4 can be exploited to successfully attack the OSGP implementation as well. The attack modification is able to effectively derive the secret OSGP encryption and decryption key, given that an attacker can accumulate the cipher streams of approximately 90,000 messages. The possession of this key allows the attacker to decrypt all data intercepted on the OSGP smart grid and thereby obtain privacy critical information of its participants. 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. 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. Karina Gitina, Ralf Wimmer, Sven Reimer, Matthias Sauer, Christoph Scholl, Bernd BeckerSolving DQBF Through Quantifier Elimination 2015 Conf. on Design, Automation and Test in Europe nach oben zur Jahresübersicht 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. 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. 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. 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. Der Andere Verlag , Seite : 184Testing Time - Time to Test? -- Using Formal Methods for the Timing Analysis of Digital Circuits -- ISBN : 978-3-86247-451-6 Matthias Sauer 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 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. 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. 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. 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. 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. 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 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. 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. 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. 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%. 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. 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 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. 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. 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.