Efficient construction of binary moment diagrams for verifying arithmetic circuits
- 19 November 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- No. 10636757,p. 78-82
- https://doi.org/10.1109/iccad.1995.479995
Abstract
BDD-based approaches cannot handle some arithmetic functions such as multiplication efficiently, while Binary Moment Diagrams proposed by Bryant and Chen (1994) provide compact representations for those functions. They reported a BMD-based polynomial-time algorithm for verifying multipliers. This approach requires high-level information such as specifications to subcomponents. This paper presents a new technique called backward construction which can construct BMDs directly from circuit descriptions without any high-level information. The experiments show that the computation time for verifying for n-bit multipliers is approximately n/sup 4/. We have successfully verified 64-bit multipliers of several type in 3-6 hours with 46 Mbyte of memory on SPARCstation 10/51. This result outperforms previous BDD-based approaches for verifying multipliers.Keywords
This publication has 11 references indexed in Scilit:
- Edge-valued binary decision for multi-level hierarchical verificationPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Breadth-first manipulation of very large binary-decision diagramsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Indexed BDDs: algorithmic advances in techniques to represent and verify Boolean functionsIEEE Transactions on Computers, 1997
- Residue BDD and its application to the verification of arithmetic circuitsPublished by Association for Computing Machinery (ACM) ,1995
- Verification of arithmetic circuits with binary moment diagramsPublished by Association for Computing Machinery (ACM) ,1995
- Verification of Arithmetic Functions with Binary Moment DiagramsPublished by Defense Technical Information Center (DTIC) ,1994
- Spectral transforms for large boolean functions with applications to technology mappingPublished by Association for Computing Machinery (ACM) ,1993
- Using BDDs to verify multipliersPublished by Association for Computing Machinery (ACM) ,1991
- Sequential circuit verification using symbolic model checkingPublished by Association for Computing Machinery (ACM) ,1990
- Graph-Based Algorithms for Boolean Function ManipulationIEEE Transactions on Computers, 1986