Verification-guided soft error resilience

ABSTRACT

Algorithmic techniques for formal verification can be used not just for bug-finding, but also to estimate vulnerability to reliability problems and to reduce overheads of circuit mechanisms for error resilience. We demonstrate this idea of verification-guided error resilience in the context of soft errors in latches. We show how model checking can be used to identify latches in a circuit that must be protected in order that the circuit satisfies a formal specification. Experimental results on a Verilog implementation of the ESA SpaceWire communication protocol indicate that the power overhead of soft error protection can be reduced by a factor of 4.35 by using our approach rather than protecting all latches.

REFERENCES

• 1: Cadence SMV model checker. http://www.kenmcmil.com/smv.html.
• 2: SpaceWire Verilog. http://www.opencores.org/projects.cgi/web/spacewire/overview, July 2005.
• 3: IEEE P1850 - standard for PSL - property specification language. http://www.eda.org/ieee-1850/, URL circa Sep.'06.
• 4: Hossein Asadi , Mehdi B. Tahoori, Soft Error Modeling and Protection for Sequential Elements, Proceedings of the 20th IEEE International Symposium on Defect and Fault Tolerance in VLSI Systems (DFT'05), p.463-474, October 03-05, 2005 [doi>10.1109/DFTVS.2005.61]
• 5: R. C. Baumann. The impact of technology scaling on soft error rate performance and limits to the efficiency of error correction. In Proc. IEDM, pages 329--332, 2002.
• 6: H. Chockler, O. Kupferman, and M. Y. Vardi. Coverage metrics for formal verification. In Proc. CHARME, LNCS 2860, pages 111--125, 2003.
• 7: E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT Press, 2000.
• 8: European Cooperation for Space Standardization. Space engineering - SpaceWire - links, nodes, routers, and networks (draft ECSS-E-50-12A). http://www.spacewire.esa.int/tech/spacewire/standards/, November 2002.
• 9: Kumar K. Goswami , Ravishankar K. Iyer , Luke Young, DEPEND: A Simulation-Based Environment for System Level Dependability Analysis, IEEE Transactions on Computers, v.46 n.1, p.60-74, January 1997 [doi>10.1109/12.559803]
• 10: Yatin Hoskote , Timothy Kam , Pei-Hsin Ho , Xudong Zhao, Coverage estimation for symbolic model checking, Proceedings of the 36th ACM/IEEE conference on Design automation, p.300-305, June 21-25, 1999, New Orleans, Louisiana, United States [doi>10.1145/309847.309936]
• 11: Mei-Chen Hsueh , Timothy K. Tsai , Ravishankar K. Iyer, Fault Injection Techniques and Tools, Computer, v.30 n.4, p.75-82, April 1997 [doi>10.1109/2.585157]
• 12: Ghani A. Kanawati , Nasser A. Kanawati , Jacob A. Abraham, FERRARI: A Flexible Software-Based Fault and Error Injection System, IEEE Transactions on Computers, v.44 n.2, p.248-260, February 1995 [doi>10.1109/12.364536]
• 13: U. Krautz , M. Pflanz , C. Jacobi , H. W. Tast , K. Weber , H. T. Vierhaus, Evaluating coverage of error detection logic for soft errors using formal methods, Proceedings of the conference on Design, automation and test in Europe: Proceedings, March 06-10, 2006, Munich, Germany
• 14: Smita Krishnaswamy , George F. Viamontes , Igor L. Markov , John P. Hayes, Accurate Reliability Evaluation and Enhancement via Probabilistic Transfer Matrices, Proceedings of the conference on Design, Automation and Test in Europe, p.282-287, March 07-11, 2005 [doi>10.1109/DATE.2005.47]
• 15: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 16: Subhasish Mitra , Tanay Karnik , Norbert Seifert , Ming Zhang, Logic soft errors in sub-65nm technologies design and CAD challenges, Proceedings of the 42nd annual conference on Design automation, June 13-17, 2005, Anaheim, California, USA [doi>10.1145/1065579.1065585]
• 17: M. Nicolaidis. Design for soft error mitigation. IEEE Trans. Device and Matl. Reliability, 5(3):405--418, Sept. 2005.
• 18: Shubhendu S. Mukherjee , Christopher Weaver , Joel Emer , Steven K. Reinhardt , Todd Austin, A Systematic Methodology to Compute the Architectural Vulnerability Factors for a High-Performance Microprocessor, Proceedings of the 36th annual IEEE/ACM International Symposium on Microarchitecture, p.29, December 03-05, 2003
• 19: Nicholas J. Wang , Justin Quek , Todd M. Rafacz , Sanjay J. patel, Characterizing the Effects of Transient Faults on a High-Performance Processor Pipeline, Proceedings of the 2004 International Conference on Dependable Systems and Networks (DSN'04), p.61, June 28-July 01, 2004
• 20: M. Zhang, S. Mitra, T. M. Mak, N. Seifert, Q. Shi, K. Kim, N. Shanbhag, N. Wang, and S. Patel. Sequential element design with built-in soft error resilience. IEEE Transactions on VLSI, Dec. 2006.