A comparative study of two boolean formulations of FPGA detailed routing constraints

A Boolean-based router expresses the routing constraints as a Boolean function which is satisfiable if and only if the layout is routable. Compared to traditional routers, Boolean-based routers offer two unique features: (1) simultaneous embedding of all nets regardless of net ordering, and (2) ability to demonstrate routing infeasibility by proving the unsatisfiability of the generated routing constraint Boolean function. In this paper, we introduce a new Boolean-based FPGA detailed routing formulation that yields an easy-to-evaluate and more scalable routability Boolean function than the previous methods. The routability constraints are expressed in terms of a set of "route" variables each of which designating a specific detailed route for a given net. Experimental results clearly show the superiority of this formulation over an earlier formulation that expressed the constraints in terms of "track" variables.