Exploiting Symmetries to Speed Up SAT-Based Boolean Matching for Logic Synthesis of FPGAs

Boolean matching is one of the enabling techniques for technology mapping and logic resynthesis of Field Programmable Gate Array (FPGA). SAT-based Boolean matching (SAT-BM) has been proposed, but the computational complexity prohibits its practical deployment. In this paper, we leverage the symmetries in Boolean functions and target FPGA architectures to prune the solution space. Besides the exploration of symmetries, we also propose a few techniques to reduce the replication runtime for SAT instance generation using the incremental SAT reasoning engine. In terms of the overall runtime, our SAT-BM obtains up to 226X speedup compared to the original SAT-BM algorithm, making SAT-BM more practical.

• Type: Journal
• Year: 2008
• Where: TCAD
• Authors: Yu Hu, Victor Shih, Rupak Majumdar, Lei He
• Keywords: Field Programmable Gate Array, Incremental Sat Reasoning, SAT-based Boolean, TCAD 2008