Using configurable computing to accelerate Boolean satisfiability

Configurable computing is a novel approach for high performance computing. It uses configurable hardware, such as field programmable logic arrays, as processing elements. The hardware is customized according to the application. High performance is achieved through custom functional units and parallel processing.;This thesis presents a case study of designing and implementing Boolean satisfiability (SAT) in configurable computer. Boolean satisfiability is an important problem that has many applications in VLSI CAD and other areas. In this thesis, an instance-specific approach is used to accelerate the backtrack search algorithm for SAT problem. The clauses of the SAT formula are translated into implication circuits. These clauses are evaluated in parallel. The control circuit is also fully implemented in the configurable hardware. A logic emulation system is used as a proof of concept to implement the design. This leads to run-time speedups of up to several hundred times compared to software approach.;Reviewing the initial implementation shows that the hardware compilation time is a significant overhead in this instance-specific approach. A new modular design is created to expedite the compilation process. Employing an incremental customization approach, the compilation overhead can be reduced from thousands of seconds to a few seconds. Meanwhile, a more efficient algorithm is implemented. Through conflict analysis, more effective backtrack and run-time learning can be implemented. This leads to several orders of magnitude improvement to many problems.;This case study extends the application domain of configurable computing. It demonstrates that configurable computing is very capable of accelerating algorithms with complex control flows.;This work shows the strength of instance-specific approach in configurable computing. By customizing the hardware according to the problem input, the hardware can be efficiently utilized and the circuit is fully tailored according to the problem. This approach exploits large amounts of fine-grained parallelism that is different to exploit by other methods. The work on design style and CAD tools show that the compilation overhead for the instance-specific approach can be reduced to a few seconds. This makes such approach useful to a wide range of difficult problems.;Overall, this work successfully shows the strength of configurable computing in accelerating difficult problems. The methodology and software tools developed for this problem can also be used to accelerate other problems. This work also illustrates the issues in configurable computing, especially in the area of configurable hardware CAD tools. We have proposed a framework to facilitate the design and implementation of configurable computing applications. This serves as an alert to the CAD community for further study in this area.