SpringerLink
Log in

Post-Silicon Fault Localization with Satisfiability Solvers

  • Chapter
  • First Online:
Post-Silicon Validation and Debug

  • 1080 Accesses

Abstract

This chapter covers techniques to localize faults in integrated circuits by means of automated satisfiability solvers. These techniques aim at identifying fault candidates for an erroneous execution trace by symbolically checking the consistency between the golden gate level model and the faulty behavior of the prototype chip. Contemporary satisfiability checkers, as well as the use of sliding windows, guarantee the scalability of our approach, which provides both spatial and temporal localization for general faults and is not restricted to a specific fault model.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
EUR 32.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or Ebook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
EUR 29.95
Price includes VAT (Germany)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
EUR 93.08
Price includes VAT (Germany)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
EUR 117.69
Price includes VAT (Germany)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free ship** worldwide - see info
Hardcover Book
EUR 160.49
Price includes VAT (Germany)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free ship** worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    Note that \(S_i\) and \(S_{i+1}\) are not necessarily disjoint, as the domain and co-domain of T coincide.

  2. 2.

    The approach of unwinding transition relations into a propositional formula which is then passed to a SAT solver was popularized by the success of Bounded Model Checking (BMC) [13].

References

  1. E. Clarke, O. Grumberg, D. Peled, Model Checking (MIT Press, Cambridge, 1999)

    Google Scholar 

  2. Y. Vizel, G. Weissenbacher, S. Malik, Boolean satisfiability solvers and their applications in model checking. Proc. IEEE 103(11), 2021–2035 (2015)

    Google Scholar 

  3. M. Abramovici, P. Bradley, K. Dwarakanath, P. Levin, G. Memmi, D. Miller, A reconfigurable design-for-debug infrastructure for SoCs, in Design Automation Conference (DAC) (ACM, 2006), pp. 7–12

    Google Scholar 

  4. M. Abramovici, M.A. Breuer, A.D. Friedman, Digital Systems Testing and Testable Design (Computer Science Press, USA, 1990)

    Google Scholar 

  5. A. Biere, M.J.H. Heule, H. van Maaren, T. Walsh (eds.), Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185 (IOS Press, Amsterdam, 2009)

    Google Scholar 

  6. J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, L.J. Hwang, Symbolic model checking: 10\(^{20}\) states and beyond, Logic in Computer Science (LICS) (IEEE, New York, 1990), pp. 428–439

    Google Scholar 

  7. K.L. McMillan, Symbolic Model Checking (Kluwer, Dordrecht, 1993)

    Google Scholar 

  8. R.E. Bryant, Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. 35(8), 677–691 (1986)

    Google Scholar 

  9. J.C. King, A program verifier, Ph.D. thesis, Carnegie Mellon University, Pittsburgh, PA, USA (1970)

    Google Scholar 

  10. T. Ball, B. Cook, V. Levin, S.K. Rajamani, Slam and static driver verifier: technology transfer of formal methods inside microsoft, Integrated Formal Verification (IFM). LNCS, vol. 2999 (Springer, Berlin, 2004)

    Google Scholar 

  11. S. Lee, K.A. Sakallah, Unbounded scalable verification based on approximate property-directed reachability and datapath abstraction, in Computer Aided Verification. LNCS, vol. 8559, ed. by A. Biere, R. Bloem (Springer, Berlin, 2014), pp. 849–865

    Google Scholar 

  12. D. Kroening, O. Strichman, Decision Procedures: An Algorithmic Point of View, Texts in Theoretical Computer Science (EATCS) (Springer, Berlin, 2008)

    Google Scholar 

  13. A. Biere, A. Cimatti, E.M. Clarke, Y. Zhu, Symbolic model checking without BDDs, Tools and Algorithms for the Construction and Analysis of Systems. LNCS, vol. 1579 (Springer, Berlin, 1999), pp. 193–207

    Google Scholar 

  14. R. Reiter, A theory of diagnosis from first principles. Artif. Intell. 32(1), 57–95 (1987)

    Google Scholar 

  15. P. Struss, O. Dressler, Physical negation – integrating fault models into the general diagnostic engine, in International Joint Conference on Artificial Intelligence (IJCAI), ed. by N.S. Sridharan (Morgan Kaufmann, USA, 1989), pp. 1318–1323

    Google Scholar 

  16. J. de Kleer, A.K. Mackworth, R. Reiter, Characterizing diagnoses and systems. Artif. Intell. 56(2–3), 197–222 (1992)

    Google Scholar 

  17. F.M. de Paula, M. Gort, A.J. Hu, S.J.E. Wilton, J. Yang, Backspace: formal analysis for post-silicon debug, Formal Methods in Computer-Aided Design (FMCAD) (IEEE, New York, 2008), pp. 1–10

    Google Scholar 

  18. F.M. de Paula, A. Nahir, Z. Nevo, A. Orni, A.J. Hu, TAB-backspace: unlimited-length trace buffers with zero additional on-chip overhead, in Design Automation Conference (DAC) (ACM, 2011), pp. 411–416

    Google Scholar 

  19. G. Tseitin, On the complexity of proofs in poropositional logics, in Automation of Reasoning: Classical Papers in Computational Logic 1967–1970, vol. 2, ed. by J. Siekmann, G. Wrightson (Springer, Berlin, 1983). Originally published 1970

    Google Scholar 

  20. M.H. Liffiton, K.A. Sakallah, Algorithms for computing minimal unsatisfiable subsets of constraints. J. Autom. Reason. 40(1), 1–33 (2008)

    Google Scholar 

  21. A. Sülflow, G. Fey, R. Bloem, R. Drechsler, Using unsatisfiable cores to debug multiple design errors, in Great Lakes Symposium on VLSI, ed. by V. Narayanan, Z. Yan, E. Macii, S. Bhanja (ACM, New York, 2008), pp. 77–82

    Google Scholar 

  22. A. Ignatiev, A. Previti, M.H. Liffiton, J. Marques-Silva, Smallest MUS extraction with minimal hitting set dualization, in Principles and Practice of Constraint Programming (CP). LNCS, vol. 9255, ed. by G. Pesant (Springer, Berlin, 2015), pp. 173–182

    Google Scholar 

  23. C. Mencía, A. Ignatiev, A. Previti, J. Marques-Silva, MCS extraction with sublinear oracle queries, in Theory and Applications of Satisfiability Testing (SAT). LNCS, vol. 9710, ed. by N. Creignou, D. Le Berre (Springer, Berlin, 2016), pp. 342–360

    Google Scholar 

  24. C. Mencía, A. Previti, J. Marques-Silva, Literal-based MCS extraction, in International Joint Conference on Artificial Intelligence (IJCAI), ed. by Q. Yang, M. Wooldridge (AAAI Press, London, 2015), pp. 1973–1979

    Google Scholar 

  25. D. Lin, T. Hong, Y. Li, S. Eswaran, S. Kumar, F. Fallah, N. Hakim, D.S. Gardner, S. Mitra, Effective post-silicon validation of system-on-chips using quick error detection. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. (TCAD) 33(10), 1573–1590 (2014)

    Google Scholar 

  26. E. Singh, C.W. Barrett, S. Mitra, E-QED: electrical bug localization during post-silicon validation enabled by quick error detection and formal methods, in Computer Aided Verification. LNCS, vol. 10427, ed. by R. Majumdar, V. Kuncak (Springer, Berlin, 2017), pp. 104–125

    Google Scholar 

  27. C.S. Zhu, G. Weissenbacher, S. Malik, Coverage-based trace signal selection for fault localisation in post-silicon validation, Haifa Verification Conference (HVC). LNCS, vol. 7857 (Springer, Berlin, 2012), pp. 132–147

    Google Scholar 

  28. K.-T. Cheng, L.-C. Wang, Automatic test pattern generation, EDA for IC System Design, Verification, and Testing (CRC Press, Boca Raton, 2006)

    Google Scholar 

  29. S.-B. Park, T. Hong, S. Mitra, Post-silicon bug localization in processors using instruction footprint recording and analysis (IFRA). IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. (TCAD) 28(10), 1545–1558 (2009)

    Google Scholar 

  30. C.S. Zhu, G. Weissenbacher, S. Malik, Silicon fault diagnosis using sequence interpolation with backbones, Computer-Aided Design (ICCAD) (IEEE, New York, 2014), pp. 348–355

    Google Scholar 

  31. W. Craig, Linear reasoning. A new form of the Herbrand-Gentzen theorem. J. Symb. Log. 22(3), 250–268 (1957)

    Google Scholar 

  32. K.L. McMillan, Interpolation and SAT-based model checking, Computer Aided Verification. LNCS, vol. 2725 (Springer, Berlin, 2003), pp. 1–13

    Google Scholar 

  33. B. Keng, A.G. Veneris, Scaling VLSI design debugging with interpolation, Formal Methods in Computer-Aided Design (FMCAD) (IEEE, New York, 2009), pp. 144–151

    Google Scholar 

  34. J. Marques-Silva, M. Janota, I. Lynce, On computing backbones of propositional theories, in European Conference on Artificial Intelligence (ECAI) (IOS Press, 2010), pp. 15–20

    Google Scholar 

  35. C.S. Zhu, G. Weissenbacher, D. Sethi, S. Malik, SAT-based techniques for determining backbones for post-silicon fault localisation, High Level Design Validation and Test Workshop (HLDVT) (IEEE, New York, 2011), pp. 84–91

    Google Scholar 

  36. C.S. Zhu, G. Weissenbacher, S. Malik, Post-silicon fault localisation using maximum satisfiability and backbones, Formal Methods in Computer-Aided Design (FMCAD) (IEEE, New York, 2011), pp. 63–66

    Google Scholar 

  37. M.H. Liffiton, A. Previti, A. Malik, J. Marques-Silva, Fast, flexible MUS enumeration. Constraints 21(2), 223–250 (2016)

    Google Scholar 

  38. G. Weissenbacher, Logical methods in automated hardware and software verification, Habilitation thesis at TU Wien (2016)

    Google Scholar 

Download references

Acknowledgements

Parts of this chapter are based on the habilitation of the first author [38] and describe joint work with Charlie Shucheng Zhu [27, 30, 35, 36]. The first author is supported by the Austrian National Research Network S11403-N23 (RiSE) and by the Vienna Science and Technology Fund (WWTF) through grant VRG11-005.

Author information

Authors and Affiliations

  1. TU Wien, Vienna, Austria

    Georg Weissenbacher

  2. Princeton University, Princeton, NJ, USA

    Sharad Malik

Authors
  1. Georg Weissenbacher
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Sharad Malik
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Georg Weissenbacher .

Editor information

Editors and Affiliations

  1. Department of Computer and Information Science and Engineering, University of Florida, Gainesville, FL, USA

    Prabhat Mishra

  2. Department of Computer and Information Science and Engineering, University of Florida, Gainesville, FL, USA

    Farimah Farahmandi

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Weissenbacher, G., Malik, S. (2019). Post-Silicon Fault Localization with Satisfiability Solvers. In: Mishra, P., Farahmandi, F. (eds) Post-Silicon Validation and Debug. Springer, Cham. https://doi.org/10.1007/978-3-319-98116-1_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-98116-1_13

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-98115-4

  • Online ISBN: 978-3-319-98116-1

  • eBook Packages: EngineeringEngineering (R0)

Publish with us

Policies and ethics

Search

Navigation