Formal Verification of ECCs for Memories Using ACL2 | Journal of Electronic Testing Skip to main content
Springer Nature Link
Log in

Formal Verification of ECCs for Memories Using ACL2

  • Published:
Journal of Electronic Testing Aims and scope Submit manuscript

Abstract

Due to the ever-increasing toll of soft errors in memories, Error Correction Codes (ECCs) like Hamming and Reed-Solomon Codes have been used to protect data in memories, in applications ranging from space to terresterial work stations. In past seven decades, most of the research has focused on providing better ECC strategies for data integrity in memories, but the same pace research efforts have not been made to develop better verification methodologies for the newer ECCs. As the memory sizes keep increasing, exhaustive simulation-based testing of ECCs is no longer practical. Hence, formal verification, particularly theorem proving, provides an efficient, yet scarcely explored, alternative for ECC verification. We propose a framework, with extensible libraries, for the formal verification of ECCs using the ACL2 theorem prover. The framework is easy to use and particularly targets the needs of formally verified ECCs in memories. We also demonstrate the usefulness of the proposed framework by verifying two of the most commonly used ECCs, i.e., Hamming and Convolutional codes. To illustrate that the ECCs verified using our formal framework are practically reliable, we utilized a formal record-based memory model to formally verify that the inherent properties of the ECCs like hamming distance, codeword decoding, and error detection/correction remain consistent even when the ECC is implemented on the memory.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (Japan)

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5

Similar content being viewed by others

References

  1. Affeldt R, Garrigue J (2015) Formalization of Error-Correcting codes: from hamming to modern coding theory. In: Urban C, Zhang X (eds) Proceedings of International conference on interactive theorem proving. Springer, LNCS, vol 9236, pp 17–33

  2. Affeldt R, Garrigue J (2015) Formalization of Error-Correcting Codes using SSReflect. MI Lect Note Ser 61:76–78

    MATH  Google Scholar 

  3. Affeldt R, Garrigue J, Saikawa T (2016) Formalization of Reed-Solomon Codes and progress report on Formalization of LDPC Codes. In: Proceedings of International Symposium on Information Theory and Its Applications. IEEE, pp 532–536

  4. Affeldt R, Garrigue J, Saikawa T (2020) A library for formalization of linear Error-Correcting codes. Journal of Automated Reasoning, pp 1–42

  5. Arbel E, Koyfman S, Kudva P, Moran S (2014) Automated detection and verification of parity-protected memory elements. In: Proceedings of International Conference on Computer-Aided Design. IEEE, pp 1–8

  6. Argyrides C, Pradhan D K, Kocak T (2011) Matrix codes for reliable and cost efficient memory chips. Trans VLSI Syst 19(3):420–428

    Article  Google Scholar 

  7. Argyrides C A, Reviriego P, Pradhan D K, Maestro J A (2010) Matrix-Based Codes for adjacent error correction. Trans Nuclear Sci 57(4):2106–2111

    Article  Google Scholar 

  8. Baarir S, Braunstein C, Encrenaz E, Ilié J M, Mounier I, Poitrenaud D, Younes S (2011) Feasibility analysis for robustness quantification by symbolic model checking. Formal Methods Syst Des 39(2):165–184

    Article  Google Scholar 

  9. Ballarin C, Paulson L C (1999) A Pragmatic Approach to Extending Provers by Computer Algebra—with Applications to Coding Theory. Fund Inf 39(1,2):1–20

    MathSciNet  MATH  Google Scholar 

  10. Baumann R (2005) Soft errors in advanced computer systems. Des Test Comput 22(3):258–266. https://doi.org/10.1109/MDT.2005.69

    Article  Google Scholar 

  11. Berrou C, Glavieux A, Thitimajshima P (1993) Near Shannon limit error-correcting coding and decoding: Turbo-codes 1 In: Proceedings of International conference on communications, vol vol 2. IEEE, pp 1064–1070

  12. Binder D, Smith E C, Holman A B (1975) Satellite anomalies from galactic cosmic rays. Trans Nuclear Sci 22(6):2675–2680. https://doi.org/10.1109/TNS.1975.4328188

    Article  Google Scholar 

  13. Bollig B, Wegener I (1996) Improving the variable ordering of OBDDs is NP-complete. Trans Comput 45(9):993–1002

    Article  Google Scholar 

  14. Boyer R S, Goldschlag D M, Kaufmann M, Moore J S (1991) Functional instantiation in First-Order logic. Academic Press, pp 7–26

  15. Burlyaev D, Fradet P, Girault A (2014) Verification-guided voter minimization in triple-modular redundant circuits. In: Proceedings of Design, Automation & Test in Europe Conference & Exhibition. IEEE, pp 1–6

  16. Cabodi G, Murciano M (2006) BDD-based Hardware Verification. In: Proceedings of International conference on formal methods for the design of computer, Communication, and Software Systems. Springer, pp 78–107

  17. Can B, Yomo H, De Carvalho E (2006) Hybrid Forwarding Scheme for Cooperative Relaying in OFDM based Networks. In: Proceedings of International conference on communications, vol 10, IEEE, pp 4520–4525

  18. Clarke E M (1997) Model checking. In: Proceedings of International Conference on Foundations of Software Technology and Theoretical Computer Science. Springer, pp 54–56

  19. Clarke E M, Wing J M (1996) Formal methods: State of the art and future directions. Comput Surv 28(4):626–643

    Article  Google Scholar 

  20. Cota E, Lima F, Rezgui S, Carro L, Velazco R, Lubaszewski M, Reis R (2001) Synthesis of an 8051-Like Micro-Controller tolerant to transient faults. J Electron Test 17(2):149–161

    Article  Google Scholar 

  21. Das A, Touba NA (2018) Low Complexity Burst Error Correcting Codes to Correct MBUs in SRAMs. In: Proceedings of Great Lakes Symposium on VLSI. ACM, pp 219–224

  22. Davis J (2006) Memories: Array-like records for ACL2. In: Proceedings International workshop on the ACL2 theorem prover and its applications. ACM, pp 57–60

  23. Fey G, Sulflow A, Frehse S, Drechsler R (2011) Effective robustness analysis using bounded model checking techniques. Trans Comput-Aided Des Integr Circ Syst 30(8):1239– 1252

    Article  Google Scholar 

  24. Frehse S, Fey G, Suflow A, Drechsler R (2009) Robustness Check for Multiple Faults using Formal Techniques. In: Proceedings of Euromicro conference on digital system design, architectures, Methods and Tools. IEEE, pp 85–90

  25. Frigerio L, Radaelli M A, Salice F (2008) Convolutional Coding for SEU mitigation In: Proceedings of European Test Symposium. IEEE, pp 191–196

  26. Hagiwara M, Nakano K, Kong J (2016) Formalization of Coding Theory using Lean In: Proceedings of International Symposium on Information Theory and Its Applications. IEEE, pp 522–526

  27. Hamming R W (1950) Error detecting and error correcting codes. Bell Syst Techn J 29(2):147–160

    Article  MathSciNet  Google Scholar 

  28. Han H, Touba N A, Yang J S (2017) Exploiting unused spare columns and replaced columns to enhance memory ECC. Trans Comput-Aided Des Integr Circ Syst 36(9):1580–1591

    Article  Google Scholar 

  29. Hasan O, Tahar S (2015) Formal verification methods In: Encyclopedia of information science and technology, 3 edn. IGI Global, pp 7162–7170

  30. Hentschke R, Marques F, Lima F, Carro L, Susin A, Reis R (2002) Analyzing area and performance penalty of protecting different digital modules with hamming code and triple modular redundancy. In: Proceedings of Integrated Circuits and Systems Design. IEEE, pp 95–100

  31. Höller A, Kajtazovic N, Preschern C, Kreiner C (2014) Formal fault tolerance analysis of algorithms for redundant systems in early design stages. In: Proceedings of Software Engineering for Resilient Systems. Springer, pp 71–85

  32. Hsiao M Y (1970) A class of optimal minimum Odd-Weight-Column SEC-DED codes. J Res Dev 14(4):395–401

    Google Scholar 

  33. Hussein J, Swift G (2015) Mitigating Single-Event Upsets Xilinx White Paper (WP395)(v1. 1). Available at: https://www.xilinx.com/support/documentation/white_papers/wp395-Mitigating-SEUs.pdf

  34. Isabelle Theorem Prover (2020) Available at: https://isabelle.in.tum.de/

  35. Jiang J H R, Lee C C, Mishchenko A, Huang C Y (2010) To SAT or not to SAT: Scalable exploration of functional dependency. Trans Comput 59(4):457–467

    Article  MathSciNet  Google Scholar 

  36. Kaufmann M, Sumners R (2002) Efficient Rewriting of Operations on Finite Structures in ACL2

  37. Kaufmann M, Moore J S, Manolios P (2000) Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers

  38. Kaufmann M, Moore J S, Ray S, Reeber E (2009) Integrating external deduction tools with ACL2. J Appl Log 7(1):3–25

    Article  MathSciNet  Google Scholar 

  39. Kchaou A, Youssef W E H, Tourki R, Bouesse F, Ramos P, Velazco R (2016) A deep analysis of SEU consequences in the internal memory of LEON3 processor. In: Proceedings of Latin-American Test Symposium. IEEE, pp 178–178. https://doi.org/10.1109/LATW.2016.7483358

  40. Kong J, Webb D J, Hagiwara M (2018) Formalization of insertion/deletion codes and the Levenshtein metric in lean. In: Proceedings of Information Theory and Its Applications. IEEE, pp 11–15

  41. Krautz U, Pflanz M, Jacobi C, Tast H W, Weber K, Vierhaus H T (2006) Evaluating Coverage of Error Detection Logic for Soft Errors using Formal Methods. In: Proceedings of Design automation & test in europe conference, vol 1. IEEE, pp 1–6. https://doi.org/10.1109/DATE.2006.244062

  42. Lean Theorem Prover (2020) Available at: https://leanprover.github.io/

  43. Leveugle R (2005) A new approach for early dependability evaluation based on formal property checking and controlled mutations. In: Proceedings of International On-Line Testing Symposium. IEEE, pp 260–265

  44. Lin S, Costello D J (1983) Coding for reliable digital transmission and storage. Prentice-Hall, chap 1, pp 1–14

  45. Lin S, Costello DJ (1983b) Error Control Codin: Fundamentals and Applications. Pearson-Prentice Hall

  46. Lvov A, Lastras-Montano L A, Paruthi V, Shadowen R, El-zein A (2012) Formal verification of error correcting circuits using computational algebraic geometry. In: Proceedings of Formal Methods in Computer-Aided Design. IEEE, pp 141–148

  47. May T C, Woods M H (1979) Alpha-Particle-Induced Soft errors in dynamic memories. Trans Electron Dev 26(1):2–9. https://doi.org/10.1109/T-ED.1979.19370

    Article  Google Scholar 

  48. Nicolaidis M (1999) Time redundancy based soft-error tolerance to rescue nanometer technologies. In: Proceedings VLSI Test Symposium. IEEE, pp 86–94

  49. Pierre L, Clavel R, Leveugle R (2009) ACL2 for the Verification of Fault-tolerance Properties: First Results. In: Proceedings of International Workshop on the ACL2 Theorem Prover and Its Applications. ACM, pp 90–99, https://doi.org/10.1145/1637837.1637852

  50. Radke W H (2011) Fault-tolerant non-volatile integrated circuit memory. US Patent 8,046,542

  51. Rastogi A, Agarawal M, Gupta B (2009) SEU Mitigation-using 1/3 Rate Convolution Coding. In: Proceedings of International Conference on Computer Science and Information Technology. IEEE, pp 180–183

  52. Sanchez-Macian A, Reviriego P, Maestro J A (2012) Enhanced detection of double and triple adjacent errors in hamming codes through selective bit placement. Trans Device Mater Reliab 12(2):357–362

    Article  Google Scholar 

  53. Sanchez-Macian A, Reviriego P, Maestro J A (2014) Hamming SEC-DAED and extended hamming SEC-DED-TAED codes through selective shortening and bit placement. Trans Device Mater Reliab 14 (1):574–576

    Article  Google Scholar 

  54. Sánchez-Macián A, Reviriego P, Maestro J A (2016) Combined SEU and SEFI Protection for Memories using Orthogonal Latin Square Codes. Trans Circ Syst I: Reg Papers 63(11):1933–1943

    Google Scholar 

  55. Seshia S A, Li W, Mitra S (2007) Verification-guided Soft Error Resilience. In: Proceedings of Design, Automation & Test in Europe Conference & Exhibition. IEEE, pp 1–6

  56. Slayman C W (2005) Cache and memory error detection, correction, and reduction techniques for terrestrial servers and workstations. Trans Device Mater Reliab 5(3):397–404. https://doi.org/10.1109/TDMR.2005.856487

    Article  Google Scholar 

  57. Verifi-ECC (2020) Available at: https://github.com/Mahum123/Verifi-ECC.git

  58. Viterbi A (1971) Convolutional Codes and their Performance in Communication Systems. Trans Commun Technol 19(5):751–772

    Article  MathSciNet  Google Scholar 

  59. Zhang P, Muccini H, Li B (2010) A classification and comparison of model checking software architecture techniques. J Syst Softw 83(5):723–744

    Article  Google Scholar 

  60. Ziegler J F, Curtis H W, Muhlfeld H P, Montrose C J, Chin B, Nicewicz M, Russell C A, Wang W Y, Freeman L B, Hosier P, LaFave L E, Walsh J L, Orro J M, Unger G J, Ross J M, O’Gorman T J, Messina B, Sullivan T D, Sykes A J, Yourke H, Enger T A, Tolat V, Scott T S, Taber A H, Sussman R J, Klein W A, Wahaus C W (1996) IBM Experiments in soft fails in computer electronics (1978—1994). IBM J Res Dev 40(1):3–18. https://doi.org/10.1147/rd.401.0003

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Electrical Engineering and Computer Science (SEECS), National University of Sciences and Technology (NUST), Islamabad, Pakistan

    Mahum Naseer, Waqar Ahmad & Osman Hasan

Authors
  1. Mahum Naseer
    View author publications

    You can also search for this author inPubMed Google Scholar

  2. Waqar Ahmad
    View author publications

    You can also search for this author inPubMed Google Scholar

  3. Osman Hasan
    View author publications

    You can also search for this author inPubMed Google Scholar

Corresponding author

Correspondence to Mahum Naseer.

Additional information

Responsible Editor: V. D. Agrawal

Publisher’s Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Naseer, M., Ahmad, W. & Hasan, O. Formal Verification of ECCs for Memories Using ACL2. J Electron Test 36, 643–663 (2020). https://doi.org/10.1007/s10836-020-05904-2

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10836-020-05904-2

Keywords