Merging nodes under sequential observability

ABSTRACT

This paper presents a new type of sequential technology independent synthesis. Building on the previous notions of combinational observability and sequential equivalence, sequential observability is introduced and discussed. By considering both the sequential nature of the design and observability simultaneously, better results can be obtained than with either algorithm alone. The experimental results show that this method can reduce the technology-independent gate count up to 10% more than the previously best known synthesis techniques.

REFERENCES

• 1: J. Baumgartner, "Integrating FV Into Main-Stream Verification: The IBM Experience," Tutorial Given at FMCAD 2006.
• 2: S. Chatterjee , A. Mishchenko , R. Brayton , X. Wang , T. Kam, Reducing structural bias in technology mapping, Proceedings of the 2005 IEEE/ACM International conference on Computer-aided design, p.519-526, November 06-10, 2005, San Jose, CA
• 3: Maher N. Mneimneh , Karem A. Sakallah, Principles of Sequential-Equivalence Verification, IEEE Design & Test, v.22 n.3, p.248-257, May 2005 [doi>10.1109/MDT.2005.68]
• 4: 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]
• 5: 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
• 6: 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
• 7: W. Kunz, D. Stoffel, and P. Menon, "Logic optimization and equivalence checking by implication analysis," in ICCAD 1997.
• 8: 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
• 9: 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
• 10: Berkeley Logic Synthesis and Verification Group, ABC: A System for Sequential Synthesis and Verification, http://www.eecs.berkeley.edu/~alanmi/abc/
• 11: C. van Eijk, "Sequential equivalence checking based on structural similarities," in IEEE Trans. Computer-Aided Design, July 2000.
• 12: Srinivas Devadas , Abhijit Ghosh , Kurt Keutzer, Logic synthesis, McGraw-Hill, Inc., New York, NY, 1994
• 13: Qi Zhu , Nathan Kitchen , Andreas Kuehlmann , Alberto Sangiovanni-Vincentelli, SAT sweeping with local observability don't-cares, Proceedings of the 43rd annual conference on Design automation, July 24-28, 2006, San Francisco, CA, USA [doi>10.1145/1146909.1146970]
• 14: Stephen M. Plaza , Kai-hui Chang , Igor L. Markov , Valeria Bertacco, Node Mergers in the Presence of Don't Cares, Proceedings of the 2007 conference on Asia South Pacific design automation, p.414-419, January 23-26, 2007 [doi>10.1109/ASPDAC.2007.358021]
• 15: C. E. Leiserson and J. B. Saxe, "Retiming synchronous circuitry," in Algorithmica 1991.
• 16: Per Bjesse , Koen Claessen, SAT-Based Verification without State Space Traversal, Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design, p.372-389, November 01-03, 2000
• 17: H. K. Ma, S. Devadas, A. R. Newton, and A. Sangiovanni-Vincentelli, "Test generation for sequential circuits," in CAD of Integrated Circuits and Systems 1988.
• 18: Pei Hsin Ho , Thomas Shiple , Kevin Harer , James Kukula , Robert Damiano , Valeria Bertacco , Jerry Taylor , Jiang Long, Smart simulation using collaborative formal and simulation engines, Proceedings of the 2000 IEEE/ACM international conference on Computer-aided design, November 05-09, 2000, San Jose, California
• 19: W. A. Burkhard , R. M. Keller, Some approaches to best-match file searching, Communications of the ACM, v.16 n.4, p.230-236, April 1973 [doi>10.1145/362003.362025]
• 20: L. A. Steen and J. A. Seebach, "Counterexamples in Topology," Courier Dover Publications 1970, Page 34.
• 21: M. R. Prasad, A. Biere, and A. Gupta, "A Survey of Recent Advances in SAT-Based Formal Verification," in Software Tools for Technology Transfer 2005.
• 22: Niklas Een, Niklas Sorensson, MiniSat. http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/
• 23: Sun Microsystems, "Processor Technology Resources - picoJava," http://www.sun.com/software/communitysource/processors/picojava.xml
• 24: Alan Mishchenko , Satrajit Chatterjee , Robert Brayton, DAG-aware AIG rewriting a fresh look at combinational logic synthesis, Proceedings of the 43rd annual conference on Design automation, July 24-28, 2006, San Francisco, CA, USA [doi>10.1145/1146909.1147048]
• 25: P. Bjesse , J. Kukula, Automatic generalized phase abstraction for formal verification, Proceedings of the 2005 IEEE/ACM International conference on Computer-aided design, p.1076-1082, November 06-10, 2005, San Jose, CA

INDEX TERMS

Primary Classification:
  J. Computer Applications
  J.6 COMPUTER-AIDED ENGINEERING

General Terms:
Algorithms, Design, Performance, Verification

Keywords:
merge, observable, sequential, synthesis