Formal Probabilistic Analysis of Stuck-at Faults in Reconfigurable Memory Arrays

摘要

Reconfigurable memory arrays with spare rows and columns are quite frequently used as reliable data storage components in present age System-on-Chips (SoCs). The spare memory rows and columns can be utilized to automatically replace rows or columns that are found to contain a cell fault after fabrication. One of the biggest SoC design challenges is to estimate, prior to the actual fabrication process, the right number of these spare rows and spare columns for meeting the reliability specifications. Traditionally, computer simulation techniques are used to perform probabilistic analysis of reconfigurable memory arrays but they provide inaccurate results. To ensure accurate analysis and thus more reliable SoC designs, we propose, in this paper, a probabilistic theorem proving approach in the domain of reconfigurable memory array analysis. We present a higher-order-logic stuck-at fault model for reconfigurable memory arrays, based on which, we illustrate the formal verification of some key statistical properties related to the number of stuck-at faults and the repairability condition.