Fault-Tolerant In-Memory Crossbar Computing using Quantified Constraint Solving

There has been a surge of interest in the effective storage and computation of data using nanoscale crossbars. In this paper, we present a new method for automating the design of fault-tolerant crossbars that can effectively compute Boolean formula. Our approach leverages recent advances in Satisfiability Modulo Theories (SMT) solving for quantified bit-vector formula (QBVF). We demonstrate that our method is well-suited for fault-tolerant computation and can perform Boolean computations despite stuck-open and stuck-closed interconnect defects as well as wire faults. We employ our framework to generate various arithmetic and logical circuits that compute correctly despite the presence of stuck-at faults as well as broken wires.