SAT sweeping with local observability don't-cares

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.

REFERENCES

• 1: Andreas Kuehlmann , Florian Krohm, Equivalence checking using cuts and heaps, Proceedings of the 34th annual conference on Design automation, p.263-268, June 09-13, 1997, Anaheim, California, United States [doi>10.1145/266021.266090]
• 2: A. Kuehlmann, V. Paruthi, F. Krohm, and M. K. Ganai, "Robust Boolean reasoning for equivalence checking and functional property verification," IEEE Transactions on Computer-Aided Design, vol. 21, pp. 1377--1394, December 2002.
• 3: A. Kuehlmann, Dynamic transition relation simplification for bounded property checking, Proceedings of the 2004 IEEE/ACM International conference on Computer-aided design, p.50-57, November 07-11, 2004 [doi>10.1109/ICCAD.2004.1382542]
• 4: Daniel Brand, Verification of large synthesized designs, Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design, p.534-537, November 07-11, 1993, Santa Clara, California, United States
• 5: Wolfgang Kunz, HANNIBAL: an efficient tool for logic verification based on recursive learning, Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design, p.538-543, November 07-11, 1993, Santa Clara, California, United States
• 6: W. Kunz, D. Stoffel, and P. Menon, "Logic optimization and equivalence checking by implication analysis," IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 16, pp. 266--281, March 1997.
• 7: E. Goldberg , M. Prasad , R. Brayton, Using SAT for combinational equivalence checking, Proceedings of the conference on Design, automation and test in Europe, p.114-121, March 2001, Munich, Germany
• 8: Feng Lu , Li-C. Wang , Kwang-Ting Cheng , Ric C-Y Huang, A Circuit SAT Solver With Signal Correlation Guided Learning, Proceedings of the conference on Design, Automation and Test in Europe, p.10892, March 03-07, 2003
• 9: A. Saldanha , A. R. Wang , R. K. Brayton , A. L. Sangiovanni-Vincentelli, Multi-level logic simplification using don't cares and filters, Proceedings of the 26th ACM/IEEE conference on Design automation, p.277-282, June 25-28, 1989, Las Vegas, Nevada, United States [doi>10.1145/74382.74429]
• 10: Alan Mishchenko , Robert K. Brayton, SAT-Based Complete Don't-Care Computation for Network Optimization, Proceedings of the conference on Design, Automation and Test in Europe, p.412-417, March 07-11, 2005 [doi>10.1109/DATE.2005.264]
• 11: K. L. McMillan, "Don't-care computation using k-clause approximation," in Int'l Workshop on Logic Synthesis (IWLS'05), (Lake Arrowhead, CA), 2005.
• 12: Hamid Savoj , Robert K. Brayton, The use of observability and external don't cares for the simplification of multi-level networks, Proceedings of the 27th ACM/IEEE conference on Design automation, p.297-301, June 24-27, 1990, Orlando, Florida, United States [doi>10.1145/123186.123280]
• 13: R. K. Brayton, Compatible observability don't cares revisited, Proceedings of the 2001 IEEE/ACM international conference on Computer-aided design, November 04-08, 2001, San Jose, California
• 14: Nikhil Saluja , Sunil P. Khatri, A robust algorithm for approximate compatible observability don't care (CODC) computation, Proceedings of the 41st annual conference on Design automation, June 07-11, 2004, San Diego, CA, USA [doi>10.1145/996566.996688]
• 15: Sean Safarpour , Andreas Veneris , Rolf Drechsler , Joanne Lee, Managing Don't Cares in Boolean Satisfiability, Proceedings of the conference on Design, automation and test in Europe, p.10260, February 16-20, 2004
• 16: Zhaohui Fu , Yinlei Yu , Sharad Malik, Considering Circuit Observability Don't Cares in CNF Satisfiability, Proceedings of the conference on Design, Automation and Test in Europe, p.1108-1113, March 07-11, 2005 [doi>10.1109/DATE.2005.102]
• 17: http://openeda.si2.org.
• 18: The OpenAccess Coalition - The Drive to an Open Industry Standard Information Model, API, and Reference Implementation for IC Design Data, Proceedings of the 3rd International Symposium on Quality Electronic Design, p.69, March 18-21, 2002
• 19: Zhong Xiu , David A. Papa , Philip Chong , Christoph Albrecht , Andreas Kuehlmann , Rob A. Rutenbar , Igor L. Markov, Early research experience with OpenAccess gear: an open source development environment for physical design, Proceedings of the 2005 international symposium on Physical design, April 03-06, 2005, San Francisco, California, USA [doi>10.1145/1055137.1055156]
• 20: http://iwls.org/iwls2005/benchmarks.html.
• 21: http://www.opencores.org.

INDEX TERMS

Primary Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.3 Design Aids
          Subjects: Verification

General Terms:
Algorithms, Verification

Keywords:
SAT sweeping, and/inverter graphs, observability