Soeken, Mathias
Mishchenko, Alan
Petkovska, Ana
Sterin, Baruch
Ienne, Paolo
Brayton, Robert K.
De Micheli, Giovanni
Heuristic NPN classification for large functions using AIGs and LEXSAT
Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing (SAT)
Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing (SAT)
Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing (SAT)
Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing (SAT)
16
2016
2016
Two Boolean functions are NPN equivalent if one can be ob- tained from the other by negating inputs, permuting inputs, or negating the output. NPN equivalence is an equivalence relation and the number of equivalence classes is significantly smaller than the number of all Boolean functions. This property has been exploited successfully to in- crease the efficiency of various logic synthesis algorithms. Since computing the NPN representative of a Boolean function is not scalable, heuristics have been proposed that are not guaranteed to find the representative for all functions. So far, these heuristics have been implemented using the functionâ€™s truth table representation, and therefore do not scale for functions exceeding 16 variables. In this paper, we present a symbolic heuristic NPN classification using And-Inverter Graphs and Boolean satisfiability techniques. This allows us to heuristically compute NPN representatives for functions with much larger number of variables; our experiments contain benchmarks with up to 194 variables. A key technique of the symbolic implementation is SAT-based procedure LEXSAT, which finds the lexicographically smallest satisfiable assignment. To our knowledge, LEXSAT has never been used before in logic synthesis algorithms.
Springer Int Publishing Ag
978-3-319-40970-2
Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing (SAT)
Conference Papers
10.1007/978-3-319-40970-2_14