nach oben

Erschienen in:

2021 | OriginalPaper | Buchkapitel

8. Enhanced Reliability Using Formal Techniques

verfasst von : Sebastian Huhn, Rolf Drechsler

Erschienen in: Design for Testability, Debug and Reliability

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Several breakthroughs in the field of the design, fabrication, and test of integrated circuits allowed for the implementation of highly complex ICs. These ICs fulfill several mission- or even safety-critical tasks at once while following a highly complex functional behavior.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Embedded Multichannel Test Compression for Low-Pin Count Test

Nächstes Kapitel Conclusion and Outlook

Note that there are many techniques available, which are approximating the reachable state space of digital circuits and, hence, those techniques can significantly improve the run-time [Gru+05, McM03, RS95]. However, they are not considered in this work to keep the presentation clear.

Note that this FF stage introduces a required delay of one clock cycle.

Note that the bound u was not exceeded.

If no bar is shown, a hardware overhead of 0% or close to 0% is measured.

Note that the initial robustness is due to the circuit’s structure and, more precisely, due to the implicitly given redundancies as observed in [TD09].

[Bie+99b]

A. Biere et al., Symbolic model checking without BDDs, in Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (Springer, 1999), pp. 193–207. https://doi.org/10.1007/3540490590_14

[Bla+08]

D. Blaauw et al., Razor II: In situ error detection and correction for PVT and SER tolerance, in Proceedings of the IEEE International Conference on Solid-State Circuits (2008), pp. 400–622. https://doi.org/10.1109/ISSCC.2008.4523226

[Bry86]

R.E. Bryant, Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. C-35(8), 677–691 (1986). https://doi.org/10.1109/TC.1986.1676819 MATH

[BW89]

A.E. Barbour, A.S. Wojcik, A general constructive approach to fault-tolerant design using redundancy. IEEE Trans. Comput. 38(1), 15–29 (1989). https://doi.org/10.1109/12.8727 MathSciNetCrossRef

[Dre+09]

R. Drechsler et al., Test Pattern Generation Using Boolean Proof Engines (Springer, 2009). https://doi.org/10.1007/978-90-481-2360-5

[DS07]

S. Disch, C. Scholl, Combinational equivalence checking using incremental SAT solving, output ordering, and resets, in Proceedings of the ASP Design Automation Conference (2007), pp. 938–943. https://doi.org/10.1109/ASPDAC.2007.358110

[DSF04]

R. Drechsler, J. Shi, G. Fey, Synthesis of fully testable circuits from BDDs. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 23(3), 440–443 (2004). https://doi.org/10.1109/TCAD.2004.823342 CrossRef

[ED10]

S. Eggersglüß, R. Drechsler, Robust algorithms for high quality test pattern generation using Boolean satisfiability, in Proceedings of the International Test Conference (2010), pp. 1–10. https://doi.org/10.1109/TEST.2010.5699289

[Ern+03]

D. Ernst et al., Razor: a low-power pipeline based on circuit-level timing speculation, in Proceedings of the IEEE/ACM International Symposium on Microarchitecture (2003), pp. 7–18. https://doi.org/10.1109/MICRO.2003.1253179

[ES04]

N. Eén, N. Sörensson, An extensible SAT-solver, in Lecture Notes in Computer Science 2919 (2004), pp. 502–518. https://doi.org/10.1007/978-3-540-24605-3_37

[EWD13]

S. Eggersglüß, R. Wille, R. Drechsler, Improved SAT-based ATPG: More constraints, better compaction, in Proceedings of the International Conference on Computer-Aided Design (2013), pp. 85–90. https://doi.org/10.1109/ICCAD.2013.6691102

[Fey+11]

G. Fey et al., Effective robustness analysis using bounded model checking techniques. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 30(8), 1239–1252 (2011) https://doi.org/10.1109/TCAD.2011.2120950 CrossRef

[FFM08]

N. Farazmand, M. Fazeli, S.G. Miremadi, FEDC: Control flow error detection and correction for embedded systems without program interruption, in Third International Conference on Availability, Reliability and Security (2008), pp. 33–38. https://doi.org/10.1109/ARES.2008.199

[FSF14]

A. Finder, A. Sülflow, G. Fey, Latency analysis for sequential circuits. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 33(4), 643–647 (2014). https://doi.org/10.1109/TCAD.2013.2292501 CrossRef

[Gru+05]

O. Grumberg et al., Achieving speedups in distributed symbolic reachability analysis through asynchronous computation, in Proceedings of the Advanced Research Working Conference on Correct Hardware Design and Verification Methods (Springer, 2005), pp. 129–145. https://doi.org/10.1007/11560548_12

[Gru09]

O. Grumberg, 3-valued abstraction for (bounded) model checking, in Proceedings of the International Conference Automated Technology for Verification and Analysis (Springer, 2009), pp. 21–21. https://doi.org/10.1007/978-3-642-04761-9_2

[Ham50]

R.W. Hamming, Error detecting and error correcting codes. Bell Syst. Tech. J. 29(2), 147–160 (1950). https://doi.org/10.1002/j.1538-7305.1950.tb00463.x MathSciNetCrossRef

[HSV13]

S. Hertz, D. Sheridan, S. Vasudevan, Mining hardware assertions with guidance from static analysis. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 32(6), 952–965 (2013). https://doi.org/10.1109/TCAD.2013.2241176 CrossRef

[Inc20]

Verific Design Automation Inc., Verific’s Parser Platform, 02/15/2020 (2020). https://www.verific.com

[KCR06]

F.L. Kastensmidt, L. Carro, R. Reis, Fault-Tolerance Techniques for SRAM-Based FPGAs (Springer, 2006). https://doi.org/10.1007/978-0-387-31069-5

[LA04]

C. Lattner, V. Adve, LLVM: a compilation framework for lifelong program analysis transformation, in Proceedings of the International Symposium on Code Generation and Optimization (2004), pp. 75–86. https://doi.org/10.1109/CGO.2004.1281665

[Lar92]

T. Larrabee, Test pattern generation using Boolean satisfiability. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 11(1), 4–15 (1992). https://doi.org/10.1109/43.108614 CrossRef

[Lee59]

C.Y. Lee, Representation of switching circuits by binary-decision programs. Bell Syst. Tech. J. 38(4), 985–999 (1959). https://doi.org/10.1002/j.1538-7305.1959.tb01585.x MathSciNetCrossRef

[Loi+13]

C. Loiacono et al., Fast Cone-Of-Influence computation and estimation in problems with multiple properties, in Proceedings of the Design, Automation and Test in Europe (2013), pp. 803–806. https://doi.org/10.7873/DATE.2013.170

[Luo89]

Z. Luo, ECC, an extended calculus of constructions, in Proceedings of the International Symposium on Logic in Computer Science (1989), pp. 386–395. https://doi.org/10.1109/LICS.1989.39193

[McM03]

K.L. McMillan, Interpolation and SAT-based model checking, in Proceedings of the International Conference on Computer-Aided Verification (Springer, 2003), pp. 1–13. https://doi.org/10.1007/978-3-540-45069-6_1

[Mic03]

A. Miczo, Digital Logic Testing and Simulation, Vol. 2 (Wiley, 2003)

[Rie+16]

H. Riener et al., metaSMT: focus on your application and not on solver integration. Int. J. Softw. Tool Technol. Trans., 1–17 (2016)

[RS95]

K. Ravi, F. Somenzi, High-density reachability analysis, in Proceedings of the International Conference on Computer-Aided Design (1995), pp. 154–158. https://doi.org/10.1109/ICCAD.1995.480006

[SB89]

C.E. Stroud, A.E. Barbour, Design for testability and test generation for static redundancy system level fault-tolerant circuits, in Proceedings of the International Test Conference (1989), pp. 812–818. https://doi.org/10.1109/TEST.1989.82370

[Som16]

F. Somenzi, CUDD: CU Decision Diagram Package (University of Colorado at Boulder, 2016). ftp://vlsi.colorado.edu/pub/. 2016-04-11

[SRM14]

A. Sanchez-Macian, P. Reviriego, J.A. Maestro, Hamming SEC-DAED and extended hamming SEC-DED-TAED codes through selective shortening and bit placement. IEEE Trans. Device Mater. Reliab. 14(1), 574–576 (2014). https://doi.org/10.1109/TDMR.2012.224753 CrossRef

[TD09]

D. Tille, R. Drechsler, A fast untestability proof for SAT-based ATPG, in Proceedings of the IEEE Symposium on Design and Diag. of Electronic Circuits and Systems (2009), pp. 38–43. https://doi.org/10.1109/DDECS.2009.5012096

[TED10]

D. Tille, S. Eggersgluss, R. Drechsler, Incremental solving techniques for SAT-based ATPG. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 29(7), 1125–1130 (2010). https://doi.org/10.1109/TCAD.2010.2044673 CrossRef

Titel: Enhanced Reliability Using Formal Techniques
verfasst von: Sebastian Huhn
Rolf Drechsler
Verlag: Springer International Publishing
Buch: Design for Testability, Debug and Reliability
Print ISBN: 978-3-030-69208-7

Electronic ISBN: 978-3-030-69209-4

Copyright-Jahr: 2021
DOI: https://doi.org/10.1007/978-3-030-69209-4_8

Neuer Inhalt

Bildnachweise

VDI-Icon, Profil Icon, inhalt2, Springer Professional Modul/© Springer Fachmedien Wiesbaden GmbH, Nachhaltigkeitsaward Key Visual/© Cometis AG/Global ESG Monitor | Daniel Rupp | Generiert mit KI, Search Icon, Banner Hanser, Jonas Klose/© Pine Valley Capital GmbH, Carina Kießling von der Strategieberatung Roland Berger/© Monika Walther Fotografie | ATZ, Beijing Auto Show 2024: Deutsche Hersteller wollen angreifen./© EKH-Pictures / Generated with AI / Stock.adobe.com, Zeitschrift Wissensmanagement Cover, PatentFit-Logo/© Springer Fachmedien Wiesbaden GmbH, Zukunftswerkstatt Sales Excellence 2024/© AndreyPopov / Getty Images / iStock, 2023_Antrieb/© supervisuell, ATZ-Webinar: Prototypenfreie Entwicklung durch Offline- und Driver-in-the-Loop-HiL-Tests /© (c) VI-grade

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Neuer Inhalt

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.