Constraint-Based FPGA Detailed Routing

A Field-programmable Gate Array (FPGA) is an integrated circuit designed to be configurable by the customer or designer after manufacturing. The FPGA configuration is generally specified using a hardware description languages (Verilog or VHDL), and then CAD tools convert the HDL designs into flattened netlist consisting of logic gates. After that, through logic optimization, placement and routing, finally, burn to the FPGA for test.This thesis studies constraint-based FPGA detailed routing problems. We will use SAT, SMT and CSP respectively as solution engines to solve this problem.Satisfiability(SAT) is the problem of determining if the variables of a given Boolean formula can be assigned in such a way as to make a formula evaluate to TRUE. Therefore, for a practical FPGA detailed routing problem, we need to write an analysis and conversion program which could transform it into a corresponding SAT problem, while maintain the logical equivalence of these two problems. Then, we could use SAT solver to solve the problem to get a routing solution.Satisfiability Modulo Theories (SMT) problem is a decision problem for logical formulas with respect to combinations of background theories expressed in classical first-order logic with equality. SMT formulas provide a much richer modeling language. For example, an SMT formula allows us to model the datapath operations of a microprocessor at the word level rather than the bit level. A Constraint Satisfaction Problem (CSP) is mathematical problem defined as a set of variables whose values must satisfy a number of constraints or limitations. We also need to write analysis and conversion program for SMT and CSP, while keeping logical equivalence between FPGA detailed routing problem and SMT, CSP formulas respectively.Finally, we used a set of benchmarks for testing performances of above mentioned constraint solving engines and analyze the reasons.