| Boolean Satisfiability (SAT) is the core problem of many applications in Electronic Design Automation (EDA), Artificial Intelligence (AI) and other areas. Any acceleration in solutions to this problem will have direct benefits for these applications.; This thesis presents the design and implementation of an application-specific multiprocessor system for SAT. A review of the current SAT software packages reveals the algorithmic characteristics of SAT and the limitations of the current software packages running on general-purpose processors. Subsequently, a parallel algorithm and a matching multiprocessor architecture are proposed to utilize the fine grain parallelism in SAT. At each node, the system has an application-specific processor, and a communication assist to handle inter-processor communication. All aspects of the system configuration, such as task partitioning, network topology, and communication and synchronization protocol, are determined based on application characteristics, and supported by simulation results.; The application-specific processor at each node is designed and implemented based on a commercial configurable processor core. Through matching the architecture with the characteristics of the target application via specialized instructions to accelerate the common primitive operations, each application specific processor can achieve 2–3x speedup compared with the basic core processor, with little extra hardware cost. In addition, it achieves higher or approximately the same performance as a 336MHz UltraSparc workstation, at a fraction of hardware cost. The small size of this processor enables multiple instances of them to be tightly integrated into a single die.; Designing an application specific multiprocessor system is a very challenging task, with typically a large design space to explore and many tradeoffs to evaluate. A cycle-accurate multiprocessor simulator based on a commercial instruction set simulator (ISS) is developed to explore the design space. To overcome the speed limitation of the cycle accurate simulation, a high level simulator has also been developed, which achieves 50–80x speedup in simulation speed with little loss of accuracy.; The final design consists of complete Verilog descriptions of the processor, as well as the communication assist at each node. Simulation results show that the system developed achieves good load balancing, high processor utilization rate and low communication cost. More importantly, this system achieves a 20–60x speedup over the fastest known SAT solver—Chaff running on a 336MHz UltraSparc workstation, which has a 10–100x speedup over other popular solvers. We believe that this system can be used to significantly expand the practical applicability of SAT in all its application areas.; Recently, several commercial configurable processor cores have been offered, which can greatly cut the development cost and time of custom processors, and thus, provide practical alternatives for application specific processor design. In addition, the rapid progress in IC manufacturing techniques has enabled multiple processors, and even DRAM, to be integrated into a single chip. Thus, multiprocessing solutions with low overhead communication and integrated memory on the same die have become practical. Although these advances have been applied successfully by applications with regular data accesses and operations, so far, SAT has not been able to benefit from them, due to its control intensive data flow and dynamic data structures. Therefore, this work also serves as a case study to extend the application domain of these latest advances in hardware design and manufacturing. |
