Sciweavers

Share
FPGA
2007
ACM

Improved SAT-based Boolean matching using implicants for LUT-based FPGAs

9 years 3 months ago
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...
Jason Cong, Kirill Minkovich
Added 07 Jun 2010
Updated 07 Jun 2010
Type Conference
Year 2007
Where FPGA
Authors Jason Cong, Kirill Minkovich
Comments (0)
books