Evaluating coverage of error detection logic for soft errors using formal methods

ABSTRACT

In this paper we describe a methodology to measure exactly the quality of fault-tolerant designs by combining fault-injection in high level design (HLD) descriptions with a formal verification approach. We utilize BDD based symbolic simulation to determine the coverage of online error-detection and - correction logic. We describe an easily portable approach, which can be applied to a wide variety of multi-GHz industrial designs.

REFERENCES

• 1: Robert Baumann, Soft Errors in Advanced Computer Systems, IEEE Design & Test, v.22 n.3, p.258-266, May 2005 [doi>10.1109/MDT.2005.69]
• 2: Marong Phadoongsidhi , Kewal K. Saluja, Event-Centric Simulation of Crosstalk Pulse Faults in Sequential Circuits, Proceedings of the 21st International Conference on Computer Design, p.42, October 13-15, 2003
• 3: P. Folkesson , S. Svensson , J. Karlsson, A Comparison of Simulation Based and Scan Chain Implemented Fault Injection, Proceedings of the The Twenty-Eighth Annual International Symposium on Fault-Tolerant Computing, p.284, June 23-25, 1998
• 4: R. J. Martínez , P. J. Gil , G. Martín , C. Pérez , J. J. Serrano, Experimental Validation of High-Speed Fault-Tolerant Systems Using Physical Fault Injection, Proceedings of the conference on Dependable Computing for Critical Applications, p.249, January 06-08, 1999
• 5: C. Constantinescu, "Experimental evaluation of error detection mechanisms", IEEE Transactions on Reliability, Mar 2003, pp. 53--57
• 6: S. R. Seward, P. K. Lala, "Fault Injection for Verifying Testability at the VHDL Level", Intl. Test Conference, 2003, p. 131--137
• 7: John R. Samson, Jr. , Wilfrido A. Moreno , Fernando J. Falquez, Validating fault tolerant designs using laser fault injection (LFI), 1997 Workshop on Defect and Fault-Tolerance in VLSI Systems, p.175-185, October 20-22, 1997
• 8: R. Velazco, T. Calin, M. Nicolaidis, S. C. Moss, S. D. LaLumondiere, V. T. Tran, R. Koga, "SEU-hardened storage cell validation using a pulsed laser", Nuclear Science, Vol. 43 No. 6 Dec. 1996, pp. 2843--2848
• 9: R. Leveugle, A New Approach for Early Dependability Evaluation Based on Formal Property Checking and Controlled Mutations, Proceedings of the 11th IEEE International On-Line Testing Symposium, p.260-265, July 06-08, 2005 [doi>10.1109/IOLTS.2005.8]
• 10: J.-C. Lo, S. Thanawastien, T. R. N. Rao, M. Nicolaidis, "An SFS Berger Check Prediction ALU and Its Application to Self-Checking Processors Designs", IEEE Trans On CAD, vol. 11, No. 4, April 1992, pp. 525--540
• 11: On-line Error Detection Techniques for Dependable Embedded Processors with High Complexity, Proceedings of the Seventh International On-Line Testing Workshop, p.51, July 09-11, 2001
• 12: Matthias Pflanz, On-line error detection and fast recover techniques for dependable embedded processors, Springer-Verlag New York, Inc., New York, NY, 2002
• 13: Christian Jacobi , Kai Weber , Viresh Paruthi , Jason Baumgartner, Automatic Formal Verification of Fused-Multiply-Add FPUs, Proceedings of the conference on Design, Automation and Test in Europe, p.1298-1303, March 07-11, 2005 [doi>10.1109/DATE.2005.75]
• 14: V. Paruthi, C Jacobi_, K. Weber, "Effcient Symbolic Simulation via Dynamic Scheduling, Don't Caring, and Case Splitting", CHARME 2005

INDEX TERMS

Keywords:
Error Detection and Correction, Fault/Error Coverage, Formal Verification, Soft Error Injection