STACCATO: disjoint support decompositions from BDDs through symbolic kernels

ABSTRACT

A disjoint support decomposition (DSD) is a representation of a Boolean function F obtained by composing two or more simpler component functions such that the component functions have no common inputs. The decomposition of a function is desirable for several reasons. First, it's a method to obtain a multiple-level implementation of a function. It leads to a partition in simpler blocks that easily results in smaller areas and fewer interconnects. Moreover, it exposes a parallelism in the computation of the function that can be exploited by hardware as well as during simulation.In this paper we present a novel algorithm, STACCATO, that generates a DSD decomposition starting from the BDD of a function. STACCATO is novel because 1) it provides a complete description of each decomposition, that is, it computes the "kernel" function K relating the elements of each decomposition, and 2) it has better performance than previously known algorithms. Experimental results run on both IWLS and industrial test-benches show that STACCATO's performance is in most cases three times as fast or more than previously known solutions.

REFERENCES

• 1: Robert L. Ashenhurst. The decomposition of switching functions. In Proceedings of the International Symposium on the Theory of Switching, Part I 29, pages 74--116, 1957.
• 2: V. Yun-Shen Shen, Archie C. McKellar, and Peter Weiner. A fast algorithm for the disjunctive decomposition of switching functions. IEEE Transactions on Computers, C-20(3):304--309, 1971.
• 3: Valeria Bertacco , Maurizio Damiani, The disjunctive decomposition of logic functions, Proceedings of the 1997 IEEE/ACM international conference on Computer-aided design, p.78-82, November 09-13, 1997, San Jose, California, United States
• 4: Valeria Maria Bertacco , Kunle Olukotun, Achieving scalable hardware verification with symbolic simulation, 2003
• 5: Yusuke Matsunaga. An exact and efficient algorithm for disjunctive decomposition. In SASIMI, pages 44--50, October 1998.
• 6: Kevin Karplus, USING IF-THEN-ELSE DAGS TO DO TECHNOLOGY MAPPING FOR FIELD-PROGRAMMABLE GATE ARRAYS, University of California at Santa Cruz, Santa Cruz, CA, 1990
• 7: Tsutomu Sasao. Multiple-valued decomposition of generalized boolean functions and the complexity of programmable logic arrays. IEEE Transactions on Computers, C-30(9):635--643, September 1981.
• 8: Rajeev Murgai , Yoshihito Nishizaki , Narendra Shenoy , Robert K. Brayton , Alberto Sangiovanni-Vincentelli, Logic synthesis for programmable gate arrays, Proceedings of the 27th ACM/IEEE conference on Design automation, p.620-625, June 24-27, 1990, Orlando, Florida, United States [doi>10.1145/123186.123421]
• 9: T. Kutzschebauch , L. Stok, Layout Driven Decomposition with Congestion Consideration, Proceedings of the conference on Design, automation and test in Europe, p.672, March 04-08, 2002
• 10: Valeria Bertacco , Kunle Olukotun, Efficient state representation for symbolic simulation, Proceedings of the 39th conference on Design automation, June 10-14, 2002, New Orleans, Louisiana, USA [doi>10.1145/513918.513946]
• 11: Gianpiero Cabodi , Paolo Camurati , Luciano Lavagno , Stefano Quer, Disjunctive partitioning and partial iterative squaring: an effective approach for symbolic traversal of large circuits, Proceedings of the 34th annual conference on Design automation, p.728-733, June 09-13, 1997, Anaheim, California, United States [doi>10.1145/266021.266355]
• 12: Tsutomu Sasao and Munehiro Matsuura. DECOMPOS: An integrated system for functional decomposition. In International Workshop on Logic Synthesis, pages 471--477, 1998.
• 13: Robert K. Brayton and Curt McMullen. The decomposition and factorization of boolean expressions. In ISCAS, Proceedings of the International Symposyium on Circuits and Systems, pages 49--54, 1982.
• 14: Kevin Karplus, Using if-then-else DAGs for multi-level logic minimization, Proceedings of the decennial Caltech conference on VLSI on Advanced research in VLSI, p.101-117, June 1989, Cambridge, Massachusetts, United States
• 15: Yung-Te Lai, Kuo-Rueih R. Pan, and Massoud Pedram. Obdd-based functional decomposition: algorithms and implementation. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 15(8):977--990, August 1996.
• 16: Olivier Coudert and Jean Christophe Madre. A unified framework for the formal verification of sequential circuits. In ICCAD, Proceedings of the International Conference on Computer Aided Design, pages 126--129, November 1990.
• 17: Randal E. Bryant, Symbolic Boolean manipulation with ordered binary-decision diagrams, ACM Computing Surveys (CSUR), v.24 n.3, p.293-318, Sept. 1992 [doi>10.1145/136035.136043]
• 18: Sun Microsystems. PicoJava technology. http://www.sun.com-/microelectronics/communitysource/picojava.
• 19: CUDD-2.3.1. http://vlsi.Colorado.edu/~fabio.