Abstract

Parallelism provides excellent speedup for many different applications in computer science. A key challenge when developing a parallel processor is to ensure the extra circuit area used does not cause excessive routing delays. In general, supercomputer designers must ensure their processors are scalable, and their structures will continue to provide increasing speedup for ever larger problems. An often overlooked limit to scalability is the complexity of the routing resources consumed as the problem is scaled.

This dissertation introduces a scalable superscalar processor that significantly accelerates the calculation of transitive implications for Boolean satisfiability (SAT). SAT is a core computer science problem with important commercial applications, including timing verification, automated layout, logic minimization and test pattern generation.

The described approach completely avoids the inefficient instance-specific placement and routing of previous field-programmable gate array (FPGA) designs, while fully exploiting the advantages of massive, fine-grained parallelism. Given n variables, this approach scalably provides quadratic speedup for some problems, when compared to modern software approaches.

Two prototyped custom Programmable Logic Devices (PLDs) demonstrate the concept. Easily-Loaded Variable Implication Solver (ELVIS) quickly evaluates transitive implications for SAT problems and presents a significant improvement over previous approaches. Partitionable, Reloadable, Implication Solving Clause Independent Logic Array (PRISCILA) is a scalable, regularly partitioned, multi-chip example of the design.

The approach is easily scaled; it grows modestly with formula size and guarantees asymptotically tight area and time complexity for formula loading. Furthermore, unlike previous instance-specific attempts, the ELVIS and PRISCILA prototypes scalably support fast dynamic clause addition, an unbounded number of variables per clause, and easily predetermined circuit timing characteristics.

Complexity Analysis of A Massively Parallel Boolean Satisfiability Implication Circuit (.pdf file)