FPGA ROUTING AND ROUTABILITY ESTIMATION VIA BOOLEAN SATISFIABILITY

Guaranteeing or even estimating the routability of a portion of a plac ed field programmable gate array (FPGA) remains difficult or impossibl e in most practical applications. In this paper, we develop a novel fo rmulation of both routing and routability estimation that relies on a rendering of the routing constraints as a single large Boolean equatio n. Any satisfying assignment to this equation specifies a complete det ailed routing. By representing the equation as a binary decision diagr am (BDD), we represent all possible routes for all nets simultaneously . Routability estimation is transformed to Boolean satisfiability, whi ch is trivial for BDD's. We use the technique in the context of a perf ect routability estimator for a global router. Experimental results fr om a standard FPGA benchmark suite suggest the technique is feasible f or realistic circuits, but refinements are needed for very large desig ns.