Issue No.05 - May (2010 vol.59)

pp: 579-592

Osman Hasan , Concordia University, Montreal

Sofiène Tahar , Concordia University, Montreal

Naeem Abbasi , Concordia University, Montreal

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TC.2009.165

ABSTRACT

Reliability analysis has become a tool of fundamental importance to virtually all electrical and computer engineers because of the extensive usage of hardware systems in safety and mission critical domains, such as medicine, military, and transportation. Due to the strong relationship between reliability theory and probabilistic notions, computer simulation techniques have been traditionally used to perform reliability analysis. However, simulation provides less accurate results and cannot handle large-scale systems due to its enormous CPU time requirements. To ensure accurate and complete reliability analysis and thus more reliable hardware designs, we propose to conduct a formal reliability analysis of systems within the sound core of a higher order logic theorem prover (HOL). In this paper, we present the higher order logic formalization of some fundamental reliability theory concepts, which can be built upon to precisely analyze the reliability of various engineering systems. The proposed approach and formalization is then utilized to analyze the repairability conditions for a reconfigurable memory array in the presence of stuck-at and coupling faults.

INDEX TERMS

Formal models, performance and reliability, theorem proving, memory structures.

CITATION

Osman Hasan, Sofiène Tahar, Naeem Abbasi, "Formal Reliability Analysis Using Theorem Proving",

*IEEE Transactions on Computers*, vol.59, no. 5, pp. 579-592, May 2010, doi:10.1109/TC.2009.165REFERENCES

- [1] L. Devroye,
Non-Uniform Random Variate Generation. Springer-Verlag, 1986.- [2] D. MacKay, "Introduction to Monte Carlo Methods,"
Learning in Graphical Models, pp. 175-204, Kluwer Academic Press, 1998.- [3] Mars Polar Lander, http://mpfwww.jpl.nasa.govmsp98/, 2008.
- [4] A. Gupta, "Formal Hardware Verification Methods: A Survey,"
Formal Methods in System Design, vol. 1, nos. 2/3, pp. 151-238, 1992.- [5] E. Clarke, O. Grumberg, and D. Long, "Verification Tools for Finite State Concurrent Systems,"
A Decade of Concurrency-Reflections and Perspectives, pp. 124-175, Springer, 1993.- [6] M. Gordon, "Mechanizing Programming Logics in Higher-Order Logic,"
Current Trends in Hardware Verification and Automated Theorem Proving, pp. 387-439, Springer, 1989.- [7] J. Hurd, "Formal Verification of Probabilistic Algorithms," PhD thesis, Univ. of Cambridge, 2002.
- [8] O. Hasan, "Formal Probabilistic Analysis Using Theorem Proving," PhD thesis, Concordia Univ., 2008.
- [9] P. Billingsley,
Probability and Measure. John Wiley, 1995.- [10] A. Miczo,
Digital Logic Testing and Simulation. Wiley Interscience, 2003.- [11] S. Kuo and W. Fuchs, "Efficient Spare Allocation for Reconfigurable Arrays,"
IEEE Design and Test of Computers, vol. 4, no. 1, pp. 24-31, Feb. 1987.- [12] M. Gordon and T. Melham,
Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic. Cambridge Univ. Press, 1993.- [13] S. Krishnaswamy, G.F. Viamonte, I.L. Markov, and J.P. Hayes, "Accurate Reliability Evaluation and Enhancement via Probabilistic Transfer Matrices,"
Proc. Design, Automation and Test in Europe, pp. 282-287, 2005.- [14] J. Han, E. Taylor, J. Gao, and J. Fortes, "Faults, Error Bounds and Reliability of Nanoelectronic Circuits,"
Proc. Application Specific System Architectures and Processors, pp. 247-253, 2005.- [15] M.R. Choudhury and K. Mohanram, "Reliability Analysis of Logic Circuits,"
IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, vol. 28, no. 3, pp. 392-405, Mar. 2009.- [16] D. Bhaduri and S. Shukla, "NANOPRISM: A Tool for Evaluating Granularity versus Reliability Trade Offs in Nano Architectures,"
Proc. Great Lakes Symp. Very Large Scale Integration (VLSI), pp. 109-112, 2004.- [17] G. Norman, D. Parker, M. Kwiatkowska, and S. Shukla, "Evaluating the Reliability of NAND Multiplexing with PRISM,"
IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, vol. 24, no. 10, pp. 1629-1637, Oct. 2005.- [18] E. Clarke, O. Grumberg, and D. Peled,
Model Checking. The MIT Press, 2000.- [19] M. Nicolaidis, N. Achouri, and L. Anghel, "A Diversified Memory Built-in Self-Repair Approach for Nanotechnologies,"
Proc. 22nd IEEE Very Large Scale Integration (VLSI) Test Symp., pp. 313-318, 2004.- [20] A. Sehgal, A. Dubey, E. Marinissen, C. Wouters, H. Vranken, and K. Chakrabarty, "Redundancy Modelling and Array Yield Analysis for Repairable Embedded Memories,"
IEE Proc. Computers and Digital Techniques, vol. 152, no. 1, pp. 97-106, 2005.- [21] W. Shi and W.K. Fuchs, "Probabilistic Analysis and Algorithms for Reconfiguration of Memory Arrays,"
IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, vol. 11, no. 9, pp. 1153-1160, Sept. 1992.- [22] C.P. Low and H.W. Leong, "Probabilistic Analysis of Memory Reconfiguration in the Presence of Coupling Faults,"
Proc. IEEE Int'l Workshop Defect and Fault Tolerance in Very Large Scale Integration (VLSI) Systems, pp. 157-166, 1992.- [23] D. Blough, "Performance Evaluation of a Reconfiguration-Algorithm for Memory Arrays Containing Clustered Faults,"
IEEE Trans. Reliability, vol. 45, no. 2, pp. 274-284, June 1996.- [24] O. Hasan, N. Abbasi, and S. Tahar, "Formal Probabilistic Analysis of Stuck-at Faults in Reconfigurable Memory Arrays,"
Integrated Formal Methods, pp. 277-291, Springer, 2009.- [25] R. Yates and D. Goodman,
Probability and Stochastic Processes: A Friendly Introduction for Electrical and Computer Engineers. Wiley, 2005.- [26] A. Levine,
Theory of Probability. Addison-Wesley, 1971.- [27] J. Harrison,
Theorem Proving with the Real Numbers. Springer, 1998.- [28] S. Richter, "Formalizing Integration Theory, with an Application to Probabilistic Algorithms," Diploma thesis, Dept. of Informatics, Technische Universitat Munchen, 2003.
- [29] K. Tridevi,
Probability and Statistics with Reliability, Queuing and Computer Science Applications. Wiley Interscience, 2002.- [30] M. Choi, N. Park, and F. Lombardi, "Hardware-Software Co-Reliability in Field Reconfigurable Multi-Processor-Memory Systems,"
Proc. Int'l Parallel and Distributed Processing Symp., pp. 170-184, 2002.- [31] J.R. Cavallaro and I.D. Walker, "A Survey of NASA and Military Standards on Fault Tolerance and Reliability Applied to Robotics,"
Proc. AIAA/NASA Conf. Intelligent Robots in Field, Factory, Service, and Space, pp. 282-286, 1994.- [32] M. Chang, W.K. Fuchs, and J.H. Patel, "Diagnosis and Repair of Memory with Coupling Faults,"
IEEE Trans. Computers, vol. 38, no. 4 pp. 493-500, Apr. 1989. |