Improved SAT-Based Boolean Matching Using Implicants for LUT-Based FPGAs

Boolean matching (BM) is a Widely used technique in FPGA resynthesis and architecture evaluation. In this paper we present several improvements to the recently proposed SAT-based Boolean matching formulation (SAT-BM-M) [11]. The principal improvement was achieved by deriving the SAT formulation using the implicant instead of minterm representation of the function to be matched. This enables our BM formulation to create a SAT problem of size O (m . 2(k)) as opposed to O(2 '') in the original formulation, where n is the number of inputs to the function, k is the size of the LUT, and m is the number of implicants, which is much smaller than 2 '' and experimentally found to be around 3 . n. Using the new BM formulation, and considering 10-input functions, we can show an almost 3x run time improvement and can solve 5.6x more problems than the SAT-based BM formulation in [11]. Moreover, using this improved Boolean matching formulation, we implemented (as a proof of concept) a FPGA resynthesis tool, called RIMatch, which was able to reduce the number of LUTs produced by ZMap by 10% on the MCNC benchmarks.