SAT sweeping with local observability don't-cares

SAT sweeping is a method for simplifying an 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 Boolean reasoning 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'tcares (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 ...

• Type: Conference
• Year: 2006
• Where: DAC
• Authors: Qi Zhu, Nathan Kitchen, Andreas Kuehlmann, Alberto L. Sangiovanni-Vincentelli
• Keywords: Boolean Reasoning, Computational Effort, DAC 2006, Design Automation, Graph Vertices