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

Improved SAT-based Boolean matching using implicants for LUT-based FPGAs,10.1145/1216919.1216944,Jason Cong,Kirill Minkovich

Improved SAT-based Boolean matching using implicants for LUT-based FPGAs   (Citations: 18)
BibTex | RIS | RefWorks Download
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 Boo- lean 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(2 2 ) ⋅ 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 impli- cants, which is much smaller than 2n and experimentally found to be around 3 . Using the new BM formulation, and consid- ering 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 ⋅ n
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
    • ...While SAT-based Boolean matching (SAT-BM) offers great flexibility in handling various PLB architectures, expensive computational complexity limits its applications, even with numerous improvements [3] [7] [11]...

    Chun Zhanget al. Building a faster boolean matcher using bloom filter

    • ...IP-BM is based on the SAT-based Boolean matching proposed in [10, 11, 12]...

    Zhe Fenget al. IPR: In-Place Reconfiguration for FPGA fault tolerance

    • ...Unlike the SAT-based matching methods discussed in [10,14,15, 20,26], our technique is based on the conversion of the PLB into an equivalent encoded library of cells which enables faster matching using NPN encoding [1,4] when compared to generic SAT-based methods...
    • ...In particular, those methods based on SAT-based matching [10, 14, 15, 20, 26] have received significant attention in the literature, and have been applied to problems such as architectural design, postmapping area reduction, and technology mapping itself...

    Andrew A. Kenningset al. FPGA technology mapping with encoded libraries andstaged priority cuts

    • ...SAT-based matching [10,14,19] is one option for matching logic functions to topologies of LUTs...
    • ...Finally, the use of SAT-based matching for rewriting topologies defined in terms of LUTs is time-consuming due to the necessity of repeatedly building and solving SAT problems; this remains true despite recent improvements in SAT-based matching for FPGAs [10,12,19]...

    Val Pevzneret al. Physical optimization for FPGAs using post-placement topology rewritin...

    • ...The Boolean matching problem can be formulated as a (quantified) Boolean satisfiability problem in the following way [12, 19, 20]...
    • ...Each satisfying assignment gives an instantiation of the LUT configuration bits that implement the same function F. SAT-based Boolean matching offers high flexibility and, with recent optimizations [21, 19, 20], reasonable performance...
    • ...Recently, [12, 19, 28] proposed combinational resynthesis based on Boolean matching [18] for FPGA area reduction...

    Yu Huet al. Robust FPGA resynthesis based on fault-tolerant Boolean matching

Sort by: