doi:10.1007/978-3-319-40970-2_14
ISI:000387430600014
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
Cham, Springer Int Publishing Ag
http://infoscience.epfl.ch/record/218883/files/2016_sat.pdf
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.
2016-06-21T10:47:55Z
http://infoscience.epfl.ch/record/218883
http://infoscience.epfl.ch/record/218883
Text