Solution Method Of SAT With FPGA Simulation

Since the complexity and size of the integrated circuit design have grown exponentially, the verification becomes the bottleneck of the whole flows of integrated circuit design. The formal verification methods using BDD technique commonly which is efficient for small and medium scale circuit, but for large-scale circuit, it fails. With the recent development of computer science, the SAT solver has a large progress that has been successfully applied in solving many theory and practical problems. However, such as widely used zChaff and DPLL method, the software SAT solver usually hard to deal with the SAT problems with large-scale or large-stochastic.In this paper, the hardware simulation method is used to solve the SAT problem. We package the SAT problem by some innovative supporters and map them to the field programmable gate array(FPGA)chip, then the FPGA chip could do computation and verification by itself.We studied the way of transforming the SAT problem into FPGA, and the supporters that makes FPGA run without control from environment,automatically, and finally, we proposes a whole framework that includes a translator that convert CNF formula and its supporters into FPGA Chip,and FPGA chip simulation, synthesis, verification, configuration,download and calculation. With that framework, we could solve the SAT problem by FPGA fast and conveniently, which may have a far-reaching significance in automated design analysis and verification.