SAT sweeping with local observability don't-cares

Qi Zhu*, Nathan B. Kitchen, Andreas Kuehlmann, Alberto Sangiovanni-Vincentelli

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingChapter

Abstract

Boolean reasoning is an essential ingredient of electronic design automation. And-Inverter graphs (AIGs) are often used to represent Boolean functions but have a high degree of structural redundancy. SAT sweeping is a method for simplifying an AIG by systematically merging graph vertices from the inputs toward the outputs using a combination of structural hashing, simulation, and SAT queries. Due to its robustness and efficiency, SAT sweeping provides a solid algorithm for Boolean reasoning in functional verification and logic synthesis. In previous work, SAT sweeping merges two vertices only if they are functionally equivalent. In this chapter we present a significant extension of the SAT-sweeping algorithm that exploits local observability don't-cares (ODCs) to increase the number of vertices merged. We use a novel technique to bound the use of ODCs and thus the computational effort to find them, while still finding a large fraction of them. Our reported results based on a set of industrial benchmark circuits demonstrate that the use of ODCs in SAT sweeping results in significantly more graph simplification with great benefit for Boolean reasoning with a moderate increase in computational effort.

Original languageEnglish (US)
Title of host publicationAdvanced Techniques in Logic Synthesis, Optimizations and Applications
PublisherSpringer New York
Pages129-148
Number of pages20
ISBN (Print)9781441975171
DOIs
StatePublished - Dec 1 2011

ASJC Scopus subject areas

  • Engineering(all)

Fingerprint Dive into the research topics of 'SAT sweeping with local observability don't-cares'. Together they form a unique fingerprint.

Cite this