Sciweavers

DAC
2006
ACM

SAT sweeping with local observability don't-cares

14 years 11 months ago
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 ...
Qi Zhu, Nathan Kitchen, Andreas Kuehlmann, Alberto
Added 13 Nov 2009
Updated 13 Nov 2009
Type Conference
Year 2006
Where DAC
Authors Qi Zhu, Nathan Kitchen, Andreas Kuehlmann, Alberto L. Sangiovanni-Vincentelli
Comments (0)