nach oben

Erschienen in:

2021 | OriginalPaper | Buchkapitel

3. 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

This chapter introduces different formal techniques, which are invoked in Part II of this book, and, hence, are required for its comprehension. The described formal techniques include the SAT problem and the BMC. Furthermore, the concept of a FSM as well as a BDD are introduced as a symbolic model.

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 Integrated Circuits

Nächstes Kapitel Embedded Compression Architecture for Test Access Ports

In this book, the negation of a Boolean variable x is written as \(\overline {x}\).

Note that made decisions have no incident edges.

Since a Boolean formula in CNF can be easily transformed into PB constraints and modern PBO solvers typically accept CNFs as input, we use the notion of CNF in this paper if possible.

[Ake78]

S.B. Akers, Binary desicion diagrams. IEEE Trans. Comput. 27 (1978)

[Bie+09]

A. Biere et al., Handbook of Satisfiability, vol. 185. Frontiers in AI and Applications (IOS Press, 2009)

[Bie+99a]

A. Biere et al., Symbolic model checking using SAT procedures instead of BDDs, in Proceedings of the Design Automation Conference (1999), pp. 317–320. https://doi.org/10.1109/DAC.1999.781333

[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

[Bie08]

A. Biere, Adaptive restart strategies for conflict driven SAT solvers, in Proceedings of the International Conference on Theory and Application of Satisfiability Testing (Springer, Berlin, Heidelberg, 2008), pp. 28–33 https://doi.org/10.1007/9783540797197_4 MATH

[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

[BS96]

M. Böhm, E. Speckenmeyer, A fast parallel SAT-solver — efficient workload balancing. Ann. Math. Artif. Intell. 17(2), 381–400 (1996). https://doi.org/10.1007/BF02127976 MathSciNetCrossRef

[Cla+18]

E.M. Clarke et al., Model Checking (MIT press, 2018)

[Coo71]

S.A. Cook, The complexity of theorem-proving procedures, in Proceedings of the ACM International Symposium on the Theory of Computing (Shaker Heights, Ohio, USA, 1971), pp. 151–158. https://doi.org/10.1145/800157.805047

[DAC99]

M.B. Dwyer, G.S. Avrunin, J.C. Corbett, Patterns in property specifications for finite-state verification, in Proceedings of the International Conference on Software Engineering (1999), pp. 411–420. https://doi.org/10.1145/302405.302672

[DDG00]

R. Drechsler, N. Drechsler, W. Gunther, Fast exact minimization of BDD’s. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 19(3), 384–389 (2000). https://doi.org/10.1109/43.833206 CrossRef

[DLL62]

M. Davis, G. Logemann, D. Loveland, A machine program for theorem-proving. Commun. ACM 5(7), 394–397 (1962). https://doi.org/10.1145/368273.368557 MathSciNetCrossRef

[DP60]

M.D. Davis, H. Putnam, A computing procedure for quantification theory. J. Assoc. Comput. Mach. 7, 201–215 (1960)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

[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

[Egg+16a]

S. Eggersglüß et al., Formal test point insertion for region-based low-capture-power compact at-speed scan test, in Proceedings of the IEEE Asian Test Symposium (2016), pp. 173–178. https://doi.org/10.1109/ATS.2016.41

[Egg+16b]

S. Eggersglüß et al., On optimization-based ATPG and its application for highly compacted test sets. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 35(12), 2104–2117 (2016) https://doi.org/10.1109/TCAD.2016.2552822 CrossRef

[EMW16]

S. Eggersglüß, K. Miyase, X. Wen, SAT-based post-processing for regional capture power reduction in at-speed scan test generation, in Proceedings of the IEEE European Test Symposium (2016), pp. 1–6. https://doi.org/10.1109/ETS.2016.7519327

[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

[Geb+07]

M. Gebser et al., Conflict-driven answer set solving, in Proceedings of the International Joint Conference on Artificial Intelligence (2007), pp. 386–392. https://doi.org/10.1016/j.artint.2012.04.001

[GN02]

E. Goldberg, Y. Novikov, BerkMin: A fast and robust SAT-solver, in Proceedings of the Design, Automation and Test in Europe (2002), pp. 142–149. https://doi.org/10.1109/DATE.2002.998262

[JW90]

R.G. Jeroslow, J. Wang, Solving propositional satisfiability problems. Ann. Math. Artif. Intell. 1(1), pp. 167–187 (1990). https://doi.org/10.1007/BF01531077 CrossRef

[KL93]

H. Konuk, T. Larrabee, Explorations of sequential ATPG using Boolean satisfiability, in Proceedings of the VLSI Test Symposium (1993), pp. 85–90. https://doi.org/10.1109/VTEST.1993.313303

[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

[Mic03]

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

[Mos+01]

M.W. Moskewicz et al., Chaff: engineering an efficient SAT solver, in Proceedings of the Design Automation Conference (2001), pp. 530–535. https://doi.org/10.1145/378239.379017

[MS00]

J. Marques-Silva, K. Sakallah, Invited tutorial: Boolean satisfiability algorithms and applications in electronic design automation, in Proceedings of the International Conference on Computer-Aided Verification (Springer, Berlin, Heidelberg, 2000), pp. 3–3. https://doi.org/10.1007/10722167_3

[MS99]

J.P. Marques-Silva, K.A. Sakallah, GRASP: A search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506–521 (1999). https://doi.org/10.1109/12.769433 MathSciNetCrossRef

[SBP16]

M. Sauer, B. Becker, I. Polian, PHAETON: A SAT-based framework for timing-aware path sensitization. IEEE Trans. Comput. 65(6), 1869–1881 (2016). https://doi.org/10.1109/TC.2015.2458869 MathSciNetCrossRef

[SC85]

A.P. Sistla, E.M. Clarke, The complexity of propositional linear temporal logics. J. ACM 32(3), 733–749 (1985). https://doi.org/10.1145/3828.3837 MathSciNetCrossRef

[Sch+99]

C. Scholl et al., BDD minimization using symmetries. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 18(2), 81–100 (1999). https://doi.org/10.1109/43.743706 CrossRef

[Som16]

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

[Tse83]

G. Tseitin, On the complexity of derivation in propositional calculus, in Studies in Constructive Mathematics and Mathematical Logic, Part 2, Vol. 8 (Springer, 1983), pp. 466–483. https://doi.org/10.1007/978-3-642-81955-1_28

[Vel04]

M.N. Velev, Encoding global unobservability for efficient translation to SAT, in Proceedings of the International Conference on Theory and Applications of Satisfiability Testing (2004), pp. 197–204

[Vic+05]

D.W. Victor et al., Functional verification of the POWER5 microprocessor and POWER5 multiprocessor systems. IBM J. Res. Dev. 49(4-5), 541–553 (2005). https://doi.org/10.1147/rd.494.0541 CrossRef

Titel: 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_3

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.