RealTest

Laufzeit

2015

 nach oben zur Jahresübersicht

• Matthias Sauer, Bernd Becker, Ilia Polian
  PHAETON: 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.

2013

 nach oben zur Jahresübersicht

• Matthias Sauer, Sven Reimer, Stefan Kupferschmid, Tobias Schubert, Paolo Marin, Bernd Becker
  Applying 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 (flip-flops) 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 flip-flops.
• Matthias Sauer, Sven Reimer, Tobias Schubert, Ilia Polian, Bernd Becker
  Efficient 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.
• Matthias Sauer, Sven Reimer, Ilia Polian, Tobias Schubert, Bernd Becker
  Provably 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.

2012

 nach oben zur Jahresübersicht

• Alexander Czutro, Michael Imhof, Jie Jiang, Abdullah Mumtaz, Matthias Sauer, Bernd Becker, Ilia Polian, Hans-Joachim Wunderlich
  Variation-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.
• Matthias Sauer, Stefan Kupferschmid, Alexander Czutro, Sudhakar M. Reddy, Bernd Becker
  Analysis 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.
• Jie Jiang, Matthias Sauer, Alexander Czutro, Bernd Becker, Ilia Polian
  On 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.
• Alexander Czutro, Matthias Sauer, Tobias Schubert, Ilia Polian, Bernd Becker
  SAT-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 Becker
  Small-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.

2011

 nach oben zur Jahresübersicht

• Matthias Sauer, Alexander Czutro, Ilia Polian, Bernd Becker
  Estimation of Component Criticality in Early Design Steps
  2011 IEEE Int'l Online Testing Symp., Seiten: 104 - 110
• Matthias Sauer, Jie Jiang, Alexander Czutro, Ilia Polian, Bernd Becker
  Efficient 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 Becker
  SAT-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.