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 (as opposed to O( m 2 k ) 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 n and experimentally found to be around 3 . 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.
sat boolean matching implicant logic synthesis fpga lookup table