Boolean Satisfiability Methods for Modern Computer-Aided Design Problems in Microelectronics.

The Boolean satisfiability (SAT) methods are one of the efficient approaches used to solve the problems of Boolean matching and the equivalence checking of digital circuits. In combination with classic routing algorithms and optimization techniques, these methods demonstrate better results than the classic routing algorithms in terms of the speed of operation and the quality of the results. In this paper, the modern practice of using the SAT methods in computer-aided design systems for VLSI is analyzed. The examples of modern SAT approaches to the problems of routing and the formal equivalence checking of digital circuits' descriptions within the technological mapping as a part of the FPGA design flow are considered. The algorithm of the detailed routing of the FPGA switching blocks using the satisfiability problem is developed and presented. The results of its work are demonstrated on the example of the programmable logic block of the integrated circuit 5400TP094 made in Russia. The block has the island architecture, where the configurable logic blocks and switching blocks form a regularly repeated layout template. The properties of the chosen classic architecture allow us to expand the region of the presented algorithm to the entire class of island style of FPGA. The algorithm is tested on the project benchmarks ISCAS-85, ISCAS-89, and LGSynth-89. The comparison of the developed SAT-based algorithm with the well-known routing algorithm Pathfinder is presented by the criteria of the elapsed time and the achieved degree of routed nets in the switching blocks. It is specified that the considered Boolean satisfiability methods for the routing problem are capable to prove the circuit's unroutability, unlike the Pathfinder algorithm whose results can only implicitly indicate it. The paper demonstrates that the application of a more efficient SAT solver significantly accelerates the work of the suggested detailed routing algorithm. [ABSTRACT FROM AUTHOR]