A new FPGA detailed routing approach via search-based Boolean satisfiability

Abstract

Boolean-based routing methods transform the geometric FPGA routing task into a large but atomic Boolean function with the property that any assignment of input variables that satisfies the function specifies a valid routing solution. Previous attempts at FPGA routing using Boolean methods were based on binary decision diagrams which limited their scopes, because of size limitations, to only individual FPGA channels. Thus, FPGA layouts were decomposed into channel-wise slices that are handled separately, and those individual channel slices were stitched together later. In this paper, we present a new search-based satisfiability (SAT) FPGA detailed routing formulation that handles all channels in an FPGA simultaneously. The formulation has the virtue that it considers all nets concurrently allowing higher degrees of freedom for each net, in contrast to the classical one-net-at-a-time approaches and is able to prove the unroutability of a given circuit by demonstrating the absence of a satisfying assignment to the routing Boolean function. To demonstrate the effectiveness of this method, we first present comparative experimental results between integer linear programming (ILP)-based routing, which is an alternative concurrent method, and SAT-based routing. We also present the first comparisons of search-based Boolean SAT routing results to other conventional routers and offer the first evidence that SAT methods can actually demonstrate the unroutability of a layout. Preliminary experimental results suggest that our approach compares very favorably with both the ILP-based approach and conventional FPGA routers.