Automated synthesis of crossbars for nanoscale computing using formal methods

Since the fabrication of nanoscale memristors by HP Labs in 2008, there has been a sustained interest in the use of crossbars of nanoscale memristors for digital storage and neuromorphic computing. However, the same success has not been replicated in the use of crossbars for performing generalpurpose computations that can support the existing software infrastructure originally designed for von Neumann architectures. One of the fundamental challenges facing the exploitation of nanoscale memristor crossbars is the existence of sneak paths. It has been shown that sneak paths can be used to perform Boolean computations in crossbars. However, the human mind can be easily overwhelmed by the large number of sneak paths that may arise in a crossbar. It is not surprising that the size of manually-designed crossbars has been too large for practical applications. In this paper, we demonstrate how formal methods can be used to automatically synthesize compact crossbar designs that employ the sneak paths phenomena as a fundamental design primitive to evaluate Boolean formula.