Reduction of interpolants for logic synthesis

John D. Backes, Marc D. Riedel

Research output: Chapter in Book/Report/Conference proceedingConference contribution

8 Scopus citations

Abstract

Craig Interpolation is a state-of-the-art technique for logic synthesis and verification, based on Boolean Satisfiability (SAT). Leveraging the efficacy of SAT algorithms, Craig Interpolation produces solutions quickly to challenging problems such as synthesizing functional dependencies and performing bounded model-checking. Unfortunately, the quality of the solutions Is often poor. When interpolants are used to synthesize functional dependencies, the resulting structure of the functions may be unnecessarily complex. In most applications to date, interpolants have been generated directly from the proofs of unsatlsfiablllty that are provided by SAT solvers. In this work, we propose efficient methods based on incremental SAT solving for modifying resolution proofs In order to obtain more compact interpolants. This, In turn, reduces the cost of the logic that is generated for functional dependencies.

Original languageEnglish (US)
Title of host publication2010 IEEE/ACM International Conference on Computer-Aided Design, ICCAD 2010
Pages602-609
Number of pages8
DOIs
StatePublished - Dec 1 2010
Event2010 IEEE/ACM International Conference on Computer-Aided Design, ICCAD 2010 - San Jose, CA, United States
Duration: Nov 7 2010Nov 11 2010

Publication series

NameIEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers, ICCAD
ISSN (Print)1092-3152

Other

Other2010 IEEE/ACM International Conference on Computer-Aided Design, ICCAD 2010
CountryUnited States
CitySan Jose, CA
Period11/7/1011/11/10

Fingerprint Dive into the research topics of 'Reduction of interpolants for logic synthesis'. Together they form a unique fingerprint.

  • Cite this

    Backes, J. D., & Riedel, M. D. (2010). Reduction of interpolants for logic synthesis. In 2010 IEEE/ACM International Conference on Computer-Aided Design, ICCAD 2010 (pp. 602-609). [5654209] (IEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers, ICCAD). https://doi.org/10.1109/ICCAD.2010.5654209