Comparison of Boolean Satisfiability Encodings on FPGA Detailed Routing Problems

We compare 12 new encodings for representing of FPGA detailed routing problems as equivalent Boolean Satisfiability (SAT) problems against the only 2 previously used encodings. We also consider two symmetry-breaking heuristics. Compared to other methods for FPGA detailed routing, SAT-based approaches have the advantage that they can prove the unroutability of a global routing for a particular number of tracks per channel, and that they consider all nets simultaneously. The experiments were run on the standard MCNC benchmarks. The combination of one new encoding with a new symmetry-breaking heuristic resulted in speedup of 3 orders of magnitude or 1,139× of the total execution time on the collection of benchmarks, when proving the unroutability of FPGA global routings. The maximum obtained speedup was 9,499× on an individual benchmark. On the other hand, most of the encodings had comparable and very efficient performance when finding solutions for configurations that were routable. T...

• Type: Conference
• Year: 2008
• Where: DATE
• Authors: Miroslav N. Velev, Ping Gao 0002
• Keywords: DATE 2008, Equivalent Boolean Satisfiability, Global Routings, Hardware, Symmetry-breaking Heuristics