Fostering Design and Automation of
Electronic and Embedded Systems

CEDA Newsletter Subscribe

Follow  facebook logo twitter button logo v2 by pixxiepaynee d5sog0x    Share  Affiliate with CEDA

Title: SAT Sweeping with Local Observability Don't-Cares

MSc. Nathan Kitchen

From the University of California at Berkeley, Berkeley, CA

Abstract

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 talk it is presented 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.

The 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.

Biographical sketch

Nathan Kitchen received his B.S. in Computer Engineering from Brigham Young University in 2002. He is currently working toward a Ph.D. in Electrical Engineering from the University of California, Berkeley. His research interests include logic synthesis and verification.

PlayPlay Video