| A Field-Programmable Gate Array (FPGA) is a general-purpose, multi-level programmable logic device that is customized by the end user. This thesis focuses on the final stage of a FPGA design implementation, routing. Considering the increasing complexity and capacity of current FPGA architectures, a modern FPGA router must (1) be flexible for a variety of FPGA architectures, (2) manage more accurate congestion model, and (3) be able to predict (or at least determine) the routability of the design. This thesis presents an “exact” method, called the Boolean Satisfiability (SAT)-based routing approach, that addresses all these constraints.; In Boolean SAT-based routing, a large but still atomic Boolean function is created such that its internal structure represents the geometric routing constraints. Any satisfying assignment of Boolean values to variables in this function corresponds to a legal routing solution. Compared to traditional routers which sequentially consider one net at a time, this approach offers two unique features: (1) simultaneous embedding of all nets regardless of net ordering and (2) the ability to demonstrate routing infeasibility by proving the unsatisfiability of the routing constraint Boolean function.; This Boolean-based routing approach was implemented and applied to both final detailed routing and fault tolerant FPGA reconfiguration, which is a partial routing task. Also, to make this method more practical, a hybrid routing algorithm, which combines a conventional routing approach with our SAT-based routing flow, was devised and tested with industrial-sized circuits. Experimental results show that Boolean SAT-based routing is a viable complement to existing routing approaches. In particular, when integrated within the flow of conventional routers, SAT-based routing solves their non-convergence problem by its ability to prove unroutability of the current set of route alternatives. For reconfiguration applications, SAT-based routing is very competitive, in flexibility, quality and runtime, with conventional approaches. These promising results suggest that SAT-based methods may have a useful role to play in other layout applications. |
