Equivalence Checking for Flow-Based Computing using Iterative SAT Solving

Processing in-memory is projected to shatter the von Neumann bottleneck and enable acceleration of data-intensive applications. Flow-based computing is an efficient in-memory computing paradigm for accelerating the execution of Boolean logic. While recent synthesis algorithms can map complex functions into flow-based computing circuits, the functional correctness cannot be verified using state-of-the-art equivalence checking techniques. The challenge is that non-volatile memory devices are intrinsically bi-directional, which introduces cycles in the computational graph. These cycles break traditional equivalence checking methods that are based on SAT formulations. In this paper, we propose a framework for equivalence checking of flow-based computing circuits that is called FlowSAT. The framework captures each circuit using an undirected computational graph. The key idea of FlowSAT is to introduce helper variables, in the form of arrows, that dynamically convert the undirected graph into a directed graph. This facilitates equivalence checking to be performed using traditional SAT formulations. However, it is prohibitively expensive to ban all possible cycles using arrow variables. Therefore, we propose to eliminate cycles by iteratively adding constraints to the SAT formulation. Our experimental evaluation demonstrates that FlowSAT is up to an order of magnitude faster than state-of-the-art methods. The framework is capable of verifying all 20/20 benchmark circuits, while the previous state-of-the-art technique is only capable of verifying 12/20 circuits within a time limit of one hour.