SAT-based FPGA Detailed Routing

Field Programmable gate arrays (FPGAs)as one kind of the best large logic device, have been used widely in the design of various electronic products. In the course of an FPGA-based development, place and route are the primary factors that affect the whole performance of the system.The thesis has mainly studied how to route a FPGA via Boolean Satisfiability solving.We have designed and realized V-SAT system, which can transfer a detailed routing problem to a formula that will be solved by a Boolean Satisfiability solver. Two prestigious tools VPR and zChaff are the main parts of V-SAT. V-SAT is tested on a set of MCNC benchmarks and obtains favorable results compared with that of VPR alone. In two major factors, V-SAT outperforms VPR.V-SAT accepts global routing files produced by VPR and creates Boolean Satisfiability problem which will be solved by zChaff solver. V-SAT has four mayor functions:file distributor, min-width solver, CNF producer, and zChaff format producer. By these functions, the system achieves two goals:getting the min-width through left-edge algorithm and transferring global routing to Boolean Satisfiability problem.By experiments, we get the time consuming distribution of V-SAT system. And find the bottleneck of the whole system. We then use Lib-Method to optimize the system. With Lib-Theroy involved, the system exploits more reusability and needs less search time, thus gets better performance as expected.