Equivalence Checking for Flow-Based Computing

The rapid growth of data-intensive applications has spurred the interest for novel in-memory computing paradigms. With the recent innovations within flow-based computing, complex circuit specification can automatically be compiled into crossbar designs. This has raised the important question of verifying the functional correctness of the synthesized crossbars. Unfortunately, the traditional equivalence checking techniques based on SAT formulations cannot directly be applied to flow-based computing. This explains why the existing techniques are rather naive and have exponential runtime complexity. In this paper, we present a framework called CHECK that casts the equivalence checking problem into a problem of detecting simple paths in an undirected graph, which enables verification to be performed using efficient graph algorithms. Moreover, the scaleability of the equivalence checking is further improved by dynamically shrinking the size of the graph using logic rules. The experimental results demonstrate the proposed graph-based approach is one to two orders of magnitude faster than brute-force enumeration. This translates into that CHECK is capable of verifying 25 designs from the RevLib suite. In contrast, naive enumeration is only capable of verifying 18 out of the 25 designs.