Application of Axiom System in the Construction Method of BDD

Abstract:

This paper presents a brief introduction of BDD. Through the analysis of the question existing in BDD construction, such as a lot of useless variable nodes, repeated calculation, redundant nodes and calculation, and so on, this paper introduces axiom system and compute-table to the BDD construction and present a new method. This method eliminates the useless node, reduces redundant nodes and lots of repeated computation. It can improve the implementation efficiency and avoid wasting memory.

• Periodical: Applied Mechanics and Materials (Volume 376)
• Pages: 267-271
• DOI: https://doi.org/10.4028/www.scientific.net/AMM.376.267
• Online since: August 2013
• Authors: Xu Zhang, Dong Hua Hu
• Keywords: Axiom System, BDD, Compute-Table, DNF

References

[1] O.P. Kuznetsow. Program realization of logic functions and automata part 1: Analysis and synthesis of binary process[J]. Automata and Remote contr. 1977, 38: 1077-1087.

[2] Malik Shard, Wang Albert R, Brayton Robert. Logic verification using binary decision diagrams in a logic synthesis environment. Proc. ICCAD, California, 1988: 6-9.

DOI: 10.1109/iccad.1988.122451

[3] J. Burch. Using BDDs to verify multipliers[C]. in Proc. 1991 Int. Workshop format methods in Vlsi design. (1991).

[4] Brace Karl S, Rudell Richard L, Brant Randal E. Efficient implementation of a BDD package. 27th ACM/IEEE Design Automation Conference, 1990: 40-45.

DOI: 10.1145/123186.123222

[5] Randal E. Bryant. Symbolic manipulation of Boolean functions using a graphical representation. Proceedings of the 22nd ACM/IEEE conference on Design Automation. 1985, 6: 688-694.

DOI: 10.1109/dac.1985.1586017

[6] Bryant Randal E. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on computers. 1986. C-35(8): 677-619.

DOI: 10.1109/tc.1986.1676819

[7] S. B . Akers. Binary Decision diagrams[J]. IEEE Trans. Comput. 1978, C-27: 509-516.

DOI: 10.1109/tc.1978.1675141

[8] LONG Wangning, MIN Yinghua, BIAN Jinian, YANG Shiyuan, XUE Hongxi. Efficient Heuristic Variable Ordering of OBDDs. TSINGHUA SCIENCE AND TECHNOLIGY. Vol. 5, No. 2, 2006, 6,: 211-216.

[9] Karplus K. Representing Boolean Functions with If-Then-Else DAGs. Computer Engineering UCSC-CRL-88-28, UC Santa Cruz. (1998).

[10] F. Somenzi. CU Decision Diagram Package Release 2. 3. 1, University of Colarado at Boulder, 2002. K. Elissa, Title of paper if known, unpublished.

[11] Shichang Fang. Discrete Dathematics[M]. Xi'An: Xidian Univercity Publishing Hourse, 1996: 53-84.

[12] WANG Ming, Yu Haiibin. Binary Decision Djagram Minimization Algorithm Based on Genetic Tabu Hybrid Strategy. INFORMATION AND CONTROL. V01．34．No．2, Apr．, 2005: 142-146.

[13] Baohong Gao, Yadong Zhu, Yuling Liu, Shengli Wang, Qiang Zhou, Xiaoyan Liu. A Novel Post-CMP Electrochemical Cleaning Process Using the BDD Film Anode Combined with Special Chemical Agents. China Semiconductor Technology International Conference (2010).

DOI: 10.1149/1.3360686

[14] Wang Qiang, Guo Jian, Liu Jianyuan. TimedBinaryDecisionDiagram. JOURNAL OF XI'AN INSTITUTE OF POST AND TELECOMMUNICATIONS. Vol. 4, No. 3, Sep. 1999: 1-6.

[15] L. M. Bartlett and S. Du, New progressive variable ordering for Binary Decision Diagram analysis of fault trees, Quality and Reliability Engineering International, vol. 21, pp.413-425, (2005).

DOI: 10.1002/qre.674

[16] Li Xiangyu, Chen Guangju. Realization and Improvement of Binary Decision Diagram[J]. Journal of UEST of China. Vol28, No. 3, Jun. 199: 516-519.

[17] Suguo Du, Yan Sun. Comparison of Progressive Variable Ordering Methods with Fixed Ordering Heuristics for Binary Decision Diagrams. 1-4244-1312-5/07/$25. 00 © 2007 IEEE.

DOI: 10.1109/wicom.2007.1126