Jan Burchard, M. Sc.
Georges Köhler Allee 51 79110 Freiburg Deutschland
Gebäude 051, Raum 01-031
+49 (0)761 203-8157
+49 (0)761 203-8142
Liste filtern: Jahre: 2017
2013 | alle anzeigen nach oben zur Jahresübersicht Jan Burchard, Dominik Erb, Sudhakar M. Reddy, Adit D. Singh, Bernd Becker Efficient SAT-Based Generation of Hazard-Activated
TSO Tests 2017 IEEE VLSI Test Symposium (VTS'17) Jan Burchard, Felix Neubauer, Pascal Raiola, Dominik Erb, Bernd Becker Evaluating the Effectiveness of D-Chains in SAT based ATPG 2017 IEEE Latin American Test Symposium (LATS'17) Jan Burchard, Dominik Erb, Adit D. Singh, Sudhakar M. Reddy, Bernd Becker Fast and Waveform-Accurate Hazard-Aware SAT-Based TSOF ATPG 2017 Conference on Design, Automation and Test in Europe 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. Kurzfassung nach oben zur Jahresübersicht Jan Burchard, Tobias Schubert, Bernd Becker Distributed Parallel #SAT Solving 2016 IEEE Cluster 2016 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. Kurzfassung Maël Gay, Jan Burchard, Jan Horáček, Ange-Salomé Messeng Ekossono, Tobias Schubert, Bernd Becker, Ilia Polian, Martin Kreuzer Small Scale AES Toolbox: Algebraic and Propositional
Formulas, Circuit-Implementations and Fault Equations 2016 FCTRU'16 nach oben zur Jahresübersicht Jan Burchard, Tobias Schubert, Bernd Becker Laissez-Faire Caching for Parallel #SAT Solving 2015 International Conference on Theory and Applications of Satisfiability Testing, Band: 9340, Seiten: 46 - 61 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
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. Kurzfassung nach oben zur Jahresübersicht Tobias Schubert, Jan Burchard, Matthias Sauer, Bernd Becker S-Trike: A Mobile Robot Platform for Higher Education 2013 International Conference on Computer Applications in Industry and Engineering, Seiten: 243 - 248 Matthias Sauer, Jan Burchard, Tobias Schubert, Ilia Polian, Bernd Becker Waveform-Guided Fault Injection by Clock Manipulation 2013 TRUDEVICE Workshop