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(22 )⋅ k m n ) 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 2n 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 SATbased BM formulation in ⋅n [11]. Moreover, using this improved Boolean matching formulation, we implemented (as a proof of concept) a FPGA resynthes...

• Type: Conference
• Year: 2007
• Where: FPGA
• Authors: Jason Cong, Kirill Minkovich
• Keywords: BM Formulation, Boolean Matching Formulation, FPGA 2007, FPGA Resynthesis, Hardware