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.