000218883 001__ 218883
000218883 005__ 20190317000454.0
000218883 0247_ $$2doi$$a10.1007/978-3-319-40970-2_14
000218883 020__ $$a978-3-319-40970-2
000218883 02470 $$2ISI$$a000387430600014
000218883 020__ $$a978-3-319-40969-6
000218883 037__ $$aCONF
000218883 245__ $$aHeuristic NPN classification for large functions using AIGs and LEXSAT
000218883 269__ $$a2016
000218883 260__ $$bSpringer Int Publishing Ag$$c2016$$aCham
000218883 300__ $$a16
000218883 336__ $$aConference Papers
000218883 490__ $$aLecture Notes in Computer Science
000218883 520__ $$aTwo 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.
000218883 700__ $$0249604$$g263922$$aSoeken, Mathias
000218883 700__ $$aMishchenko, Alan
000218883 700__ $$0245677$$g196536$$aPetkovska, Ana
000218883 700__ $$aSterin, Baruch
000218883 700__ $$0241619$$g101954$$aIenne, Paolo
000218883 700__ $$aBrayton, Robert K.
000218883 700__ $$0240269$$g167918$$aDe Micheli, Giovanni
000218883 7112_ $$dJuly 5-8, 2016$$cBordeaux, France$$a19th International Conference on Theory and Applications of Satisfiability Testing (SAT)
000218883 773__ $$tProceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing (SAT)
000218883 8564_ $$uhttps://infoscience.epfl.ch/record/218883/files/2016_sat.pdf$$zn/a$$s509962$$yn/a
000218883 909C0 $$xU11140$$0252283$$pLSI1
000218883 909C0 $$0252192$$pLAP$$xU10418
000218883 909CO $$qGLOBAL_SET$$pconf$$pSTI$$pIC$$ooai:infoscience.tind.io:218883
000218883 917Z8 $$x112915
000218883 937__ $$aEPFL-CONF-218883
000218883 973__ $$rNON-REVIEWED$$sPUBLISHED$$aEPFL
000218883 980__ $$aCONF