www.prismmodelchecker.org
[NPKS04] Gethin Norman, David Parker, Marta Kwiatkowska and Sandeep Shukla. Evaluating the Reliability of Defect-Tolerant Architectures for Nanotechnology with Probabilistic Model Checking. In Proc. International Conference on VLSI Design, pages 907-914, IEEE CS Press. January 2004. [ps.gz] [pdf] [bib] [Analyses the reliability of defect-tolerant design, NAND multiplexing, using PRISM.]
Downloads:  ps.gz ps.gz (55 KB)  pdf pdf (119 KB)  bib bib
Notes: Further information and verification results are available from this web page.
Links: [Google] [Google Scholar]
Abstract. As we move from deep submicron technology to nanotechnology for device manufacture, the need for defect-tolerant architectures is gaining importance. This is because, at the nanoscale, devices will be prone to errors due to manufacturing defects, ageing, and transient faults. Micro-architects will be required to design their logic around defect tolerance through redundancy. However, measures of reliability must be quantified in order for such design methodologies to be acceptable. We propose a CAD framework based on probabilistic model checking which provides efficient evaluation of the reliability/redundancy trade-off for defect-tolerant architectures. This framework can model probabilistic assumptions about defects, easily compute reliability figures and help designers make the right decisions. We demonstrate the power of our framework by evaluating the reliability/redundancy trade-off of a canonical example, namely NAND multiplexing. We not only find errors in analytically computed bounds published recently, but we also show how to use our framework to evaluate various facets of design trade-off for reliability.

Publications