SAT Based Multi Pin Net Detailed Routing for FPGA

Boolean satisfiability based detailed routing is becoming very popular nowadays because of its capability to evaluate all the nets simultaneously. In this approach the geometric FPGA detailed routing problem can be transformed into a single Boolean function. Any satisfying assignment of input Boolean variables in the function denotes that routing is possible. Impossible routing is proved by the absence of any valid satisfying assignment. All the previous SAT based detailed routing solutions executed on two-pin nets. Decomposition is one important job in two-pin net routing as because all the real nets are multi-pin. Working on multi-pin net is more realistic and efficient. Our main concentration is on the question of rout ability of multi-pin net to track assignment formulation by removing the overhead of net decomposition. In this paper we prove the rout ability of MCNC benchmark circuits with multi-pin nets and list the comparison between track-based detailed routing on two-pin nets and track assignment formulation on multi-pin nets.