SAT sweeping with local observability don't-cares

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

*Corresponding author for this work

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

66 Scopus citations

Abstract

SAT sweeping is a method for simplifying an shape And/Inverter graph (AIG) by systematically merging graph vertices from the inputs towards 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 Booleanreasoning in functional verification and logic synthesis. In previous work, SAT sweeping merges two vertices only if they are functionally equivalent. In this paper 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 ODC-based 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 publication2006 43rd ACM/IEEE Design Automation Conference, DAC'06
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages229-234
Number of pages6
ISBN (Print)1595933816, 1595933816, 9781595933812
DOIs
StatePublished - 2006
Event43rd Annual Design Automation Conference, DAC 2006 - San Francisco, CA, United States
Duration: Jul 24 2006Jul 28 2006

Publication series

NameProceedings - Design Automation Conference
ISSN (Print)0738-100X

Conference

Conference43rd Annual Design Automation Conference, DAC 2006
Country/TerritoryUnited States
CitySan Francisco, CA
Period7/24/067/28/06

Keywords

  • And/inverter graphs
  • Observability
  • SAT sweeping

ASJC Scopus subject areas

  • Hardware and Architecture
  • Control and Systems Engineering

Fingerprint

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

Cite this