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.
This work is based on an earlier work: SAT sweeping with local observability don’t-cares, in Proceedings of the 43rd Annual Design Automation Conference, ISBN:1-59593-381-6 (2006) © ACM, 2006. DOI=http://doi.acm.org/10.1145/1146909.1146970.
This chapter is an extended version of [20]. The added content includes examples, a proof, details of the algorithm flow and implementation, discussion of applications, and explanation of the experimental results.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Blanchard, T., Ferreri, R., Whitmore, J.: The OpenAccess coalition: The drive to an open industry standard information model, API, and reference implementation for IC design data. In: Proceedings of the International Symposium on Quality Electronic Design, pp. 69–74. San Jose, CA (2002)
Brand, D.: Verification of large synthesized designs. In: Proceedings of the IEEE/ACM International Conference on Computer Aided Design, pp. 534–537. Santa Clara, CA (1993)
Brayton, R.K.: Compatible observability don’t cares revisited. In: Proceedings of the IEEE/ACM International Conference on Computer Aided Design, pp. 618–623. San Jose, CA (2001)
van Eijk, C.A.J.: Sequential equivalence checking without state space traversal. In: Proceedings of DATE, pp. 618–623. Paris, France (1998)
Fu, Z., Yu, Y., Malik, S.: Considering circuit observability don’t cares in CNF satisfiability. In: Design, Automation and Test in Europe, pp. 1108–1113. Munich, Germany (2005)
Goldberg, E., Prasad, M.R., Brayton, R.K.: Using SAT in combinational equivalence checking. In: Proceedings of IEEE/ACM Design Automation and Test in Europe Conference and Exposition, pp. 114–121. Munich, Germany (2001)
Kuehlmann, A.: Dynamic transition relation simplification for bounded property checking. In: Digest of Technical Papers of the IEEE/ACM International Conference on Computer Aided Design, pp. 50–57. San Jose, CA (2004)
Kuehlmann, A., Krohm, F.: Equivalence checking using cuts and heaps. In: Proceedings of the 34th ACM/IEEE Design Automation Conference, pp. 263–268. Anaheim, CA (1997)
Kuehlmann, A., Paruthi, V., Krohm, F., Ganai, M.K.: Robust Boolean reasoning for equivalence checking and functional property verification. IEEE Transactions on Computer-Aided Design 21(12), 1377–1394 (2002)
Kunz, W.: HANNIBAL: An efficient tool for logic verification based on recursive learning. In: Digest of Technical Papers of the IEEE/ACM International Conference on Computer Aided Design, pp. 538–543. Santa Clara, CA (1993)
Kunz, W., Stoffel, D., Menon, P.: Logic optimization and equivalence checking by implication analysis. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 16(3), 266–281 (1997)
Lu, F., Wang, L.C., Cheng, K.T., Huang, R.C.Y.: A circuit SAT solver with signal correlation guided learning. In: Design Automation and Test in Europe, pp. 892–897. Munich, Germany (2003)
McMillan, K.L.: Don’t-care computation using k-clause approximation. In: International Workshop on Logic Synthesis (IWLS’05). Lake Arrowhead, CA (2005)
Mishchenko, A., Brayton, R.K.: SAT-based complete don’t-care computation for network optimization. In: Design, Automation and Test in Europe, pp. 412–417. Munich, Germany (2005)
Safarpour, S., Veneris, A., Drechsler, R., Lee, J.: Managing don’t cares in Boolean satisfiability. In: Design, Automation and Test in Europe, p. 10260. Paris, France (2004)
Saldanha, A., Wang, A.R., Brayton, R.K., Sangiovanni-Vincentelli, A.L.: Multi-level logic simplification using don’t cares and filters. In: Proceedings of the 26th ACM/IEEE Conference on Design Automation, pp. 277–282. Las Vegas, NV (1989)
Saluja, N., Khatri, S.P.: A robust algorithm for approximate compatible observability don’t care (CODC) computation. In: Proceedings of the 41st Design Automation Conference, pp. 422–427. San Diego, CA (2004)
Savoj, H., Brayton, R.K.: The use of observability and external don’t cares for the simplification of multi-level networks. In: Proceedings of the 27th ACM/IEEE Design Automation Conference, pp. 297–301. Orlando, FL (1990)
Xiu, Z., Papa, D.A., Chong, P., Albrecht, C., Kuehlmann, A., Rutenbar, R.A., Markov, I.L.: Early research experience with OpenAccess Gear: An open source development environment for physical design. In: Proceedings of the ACM International Symposium on Physical Design, pp. 94–100. San Francisco, CA (2005)
Zhu, Q., Kitchen, N., Kuehlmann, A., Sangiovanni-Vincentelli, A.: SAT sweeping with local observability don’t-cares. In: Proceedings of the 43rd Design Automation Conference, pp. 229–234. San Francisco, CA (2006)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer Science+Business Media, LLC
About this chapter
Cite this chapter
Zhu, Q., Kitchen, N.B., Kuehlmann, A., Sangiovanni-Vincentelli, A. (2011). SAT Sweeping with Local Observability Don’t-Cares. In: Gulati, K. (eds) Advanced Techniques in Logic Synthesis, Optimizations and Applications. Springer, New York, NY. https://doi.org/10.1007/978-1-4419-7518-8_8
Download citation
DOI: https://doi.org/10.1007/978-1-4419-7518-8_8
Published:
Publisher Name: Springer, New York, NY
Print ISBN: 978-1-4419-7517-1
Online ISBN: 978-1-4419-7518-8
eBook Packages: EngineeringEngineering (R0)