We address the problem of reducing the size of Craig's interpolants used in SAT-based model checking. Craig's interpolants are AND-OR circuits, generated by post-processing refutation proofs of SAT solvers. Being highly redundant, their compaction is typically tackled by reducing the proof graph and/or by exploiting standard logic synthesis techniques. In this paper, we propose a set of ad-hoc logic synthesis functions that, revisiting known logic synthesis approaches, specifically address speed and scalability. Though general and not restricted to interpolants, these techniques target the main sources of redundancy in combinational circuits. This paper includes an experimental evaluation, showing the benefits of the proposed techniques, on a set of benchmark interpolants arising from hardware model checking problems.
Logic Synthesis for Interpolant Circuit Compaction / Cabodi, G.; Camurati, P. E.; Palena, M.; Pasini, P.; Vendraminetto, D.. - In: IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS. - ISSN 0278-0070. - STAMPA. - 38:2(2019), pp. 380-384.
|Titolo:||Logic Synthesis for Interpolant Circuit Compaction|
|Data di pubblicazione:||2019|
|Digital Object Identifier (DOI):||http://dx.doi.org/10.1109/TCAD.2018.2808229|
|Appare nelle tipologie:||1.1 Articolo in rivista|