Sat-based technology mapping framework

Abstract

Valid implementations of functions with programmable logic blocks are efficiently determined by creating an approximation of a hardware configuration of programmable logic blocks to quickly screen out configurations unlikely to provide a valid results. If a configuration passes this first phase, the approximation is refined to search for valid function implementations with the hardware configuration. The approximation and refinement may use a partitioning of function input variables to logic blocks to reduce the search space. Additional conflict clauses may be used to further reduce the search space. Implementations of sample functions or other previously considered functions may be analyzed to identify conflict clauses that are reusable for analyzing other functions. A representation of potential implementations of a function can be subdivided into subsets and analyzed separately. The intersection of the solutions from each subset are valid implementations of the function.