Verification of Flow-Based Computing Systems Using Bounded Model Checking

Flow-based computing is a digital in-memory computing paradigm with tremendous potential. Its favorable characteristics, such as high robustness, low energy consumption and small computational delay make it a strong contender for integration into future computing systems. While most studies on emerging computing paradigms are focused on synthesis, it is crucial to develop methods to verify the functional correctness of the resulting designs. Flow-based computing is based on an undirected computational graph, which prevents equivalence checking to be performed by solving SAT formulations. In this paper, we propose a framework called XSAT for equivalence checking of crossbar designs for flow-based computing. The XSAT framework draws on bounded model checking (BMC) to convert the undirected computational graph into a directed acyclic computational graph (DAG). The conversion allows traditional SAT-based equivalence checking techniques to be used at the expense of increasing the size of the problem. We further introduce a divide-and-conquer technique to accelerate the verification process. The technique divides the main problem into many subproblems of smaller size, which can be executed in parallel using multiple cores or nodes. From the experimental evaluation, it can be observed that the XSAT framework can solve all nineteen MCNC benchmarks whereas previous SOTA techniques can only solve eleven out of the nineteen benchmarks within one hour, i.e., with speed-ups of one to two orders of magnitude. Moreover, the divide-and-conquer technique results in speed-ups of up to 93x on large benchmark circuits.