Font Size: a A A

The Study Of Pseudo-Boolean Satisfiability Algorithm And Its Application In FPGA Routing

Posted on:2011-02-23Degree:DoctorType:Dissertation
Country:ChinaCandidate:Y L TangFull Text:PDF
GTID:1118330332471146Subject:Light Industry Information Technology and Engineering
Abstract/Summary:PDF Full Text Request
Field Programmable Gate Array (FPGA) contains reconfigurable logic blocks and routing resources, belongs to digital integrated circuits. FPGA supports programmable reconfiguration, and makes great saving in processing cost and time. Due to its flexibility, low risk, short development cycle and other advantages, FPGA is widely applied in communications, industrial control, automotive electronics, data processing, consumer electronics and other domain. The corresponding computer aided design (CAD) tools need to be upgraded and optimized with the increasing capacity of reconfigurable blocks in FPGA. With the increasing complexity of design, it usually takes long time for CAD tools to map one design to FPGA device to meet the requirements of various parameters. Since nearly 30% of the whole CAD flow time is often consumed in routing stage, it is very import to explore high efficiency routing algorithms to reduce the time of whole FPGA development process.A variety of routing algorithms have been developed and used at present, Boolean Satisfiability (SAT) routing algorithm and geometric search routing algorithms are currently the most popular ones among them. Both of them have advantages and disadvantages. The geometric search routing algorithms, evolving from basic Maze algorithm, can improve routing speed by optimizing. But they can only route one wire once and is difficult to determine routability, so the algorithms normally terminated by setting an upper limit time. Meanwhile, all the other geometric search algorithms developed from Maze algorithm have shortcomings of depending on routing sequence. In contrast, SAT-based algorithms can route all the wires at the same time, proving routability theoretically. But the method makes scalability relatively poor, as a large number of variables and constraint clauses are usually required.Recently, a routing algorithm based on Pseudo-Boolean Satisfiability (PBS) becomes research focus. Similar to common SAT-based algorithms, PBS algorithm can route all the wires at the same time, and prove its routability. The difference is that PBS routing algorithm expresses constraints by simple clauses, so the numbers of variables and clauses are significantly reduced. Therefore, the memory requirement is greatly reduced and the scalability is obviously improved. However, pseudo-Boolean Satisfiability algorithm is not applicable in large routing benchmarks, the transformation cost of which in routing process is large. This paper has made efforts to explore a new algorithm to solve the above problems, and the specific research and results are as follows:(1) Based on the latest comprehensive survey of FPGA architectures, an FPGA routing architectural model is presented, which belongs to symmetrical array (island-style) FPGA architecture grounded on SRAM. Only three appropriate parameters are needed to represent the target routing architecture of this model. A detailed study of Boolean satisfiability algorithm, pseudo-Boolean satisfiability algorithms, and two kinds of geometric search routing algorithm,which include a negotiation-based performance-driven routing algorithm (PathFinder) and a negotiated A* routing algorithm for FPGAs (Frontier) is made in this paper. Frontier, SAT, and PBS are analyzed and compared on the basis of same large benchmark circuits which are consist of global routing instances and Max-SAT routing benchmarks. The results show that encoding of pseudo-Boolean constraints is more simple and compact than pure CNF, and also behaves better tightness and shorter running time. The solver PBS is developed by extension of pseudo-Boolean satisfiability problem. Compared with previous two methods, including early geometric search algorithms and current solver Chaff for pure CNF, the solver PBS aiming at the problem of pseudo-Boolean satisfiability can effectively speed up the solution process, and the required storage space is smaller.(2) Recent work in 0-1 Integer Linear Programming (ILP) offers extensions that can optimize linear objective functions. This is usually achieved by solving a series of SAT or ILP decision problems. But an objective function may complicate the constraints using symmetries, even when the constraints are unsatisfiable and irrelevant with the objective function. Based on symmetry-breaking technology, an adaptive flow is proposed which combines technique of dynamic symmetry-breaking and static symmetry-breaking. The new flow can analyze a given Boolean optimization problem and choose symmetry-breaking technique that is best suited for the problem characteristics. Experiments results show that this approach accelerates problem solving compared to pure static symmetry-breaking or pure dynamic symmetry-breaking.(3) In order to improve the negative effect of increasing transformation cost of pseudo-Boolean Satisfiability algorithm in the routing process, a new routing algorithm is proposed for FPGA routing, which combines advantages of pseudo-Boolean Satisfiability and geometric routing algorithm. In the routing process, one of geometric routing algorithm, Frontier or PathFinder, is chosen firstly. If not successful, then use pseudo-Boolean Satisfiability algorithm. Moreover, technique of static symmetry-breaking is added to carry out pretreatment of pseudo-Boolean constraints, detect and break the symmetries in the routing flow. Consequently, the purpose of reducing the search path is achieved, and the cost is consequently reduced. Results of preliminary experiments show that this approach can reduce the runtime observably, and speed up the solving process.(4) The problem of detailed FPGA routing using sub-SAT formulation methods is studied. In the context of FPGA routing where routing resources are fixed, Boolean formulation methods can prove unroutability of a given circuit, which is a clear advantage over classical one-net-at-a-time approaches. The sub-SAT methods transform a"strict"SAT problem with N constraints into a new,"relaxed"SAT problem which is satisfiable just if not more than k << N of these constraints can not be satisfiabled in the original problem. It has improved SAT-based approach, but introduces too many additional variables and clauses. To solve this problem, two methods are proposed. First, Pseudo-Boolean Satisfiability is employed to offset the disadvantage of additional variables and clauses. Second, sub-SAT introduces additional variables and clauses, and makes the number of symmetries exponential growth in the solving process. In response to this problem, static symmetry-breaking is used to carry out pretreatment of Conjunctive Normal Form (CNF), detect and break the symmetries therein. The purpose of reducing the search path is achieved. The method of reduction to graph automorphism is used to detecting all symmetries. After adding appropriate symmetry-breaking predicates (SBPs), the search space is pruned that confined the search to non-symmetric regions of the space without affecting the satisfiability to the CNF formula. A SAT solver is then applied to the preprocessed CNF formula. Results of preliminary experiments show that the two approaches can reduce the runtime observably, and speed up the solving process.Finally, the work of this dissertation is summarized, and the direction for future research has discussed.
Keywords/Search Tags:Benchmarking, Boolean Satisfiability, Field Programmable Gate Array, Geometric Search Routing Algorithm, Integer Linear Programming, Pseudo-Boolean Satisfiability, Routing algorithms, Symmetry, sub-SAT
PDF Full Text Request
Related items