Verification of Arithmetic Circuits with Binary Moment Diagrams
- 1 December 1995
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE) in Proceedings of the 39th conference on Design automation - DAC '02
- No. 0738100X,p. 535-541
- https://doi.org/10.1109/dac.1995.250005
Abstract
Binary Moment Diagrams (BMDs) provide a canonical representations for linear functions similar to the way Binary Decision Diagrams (BDDs) represent Boolean functions. Within the class of linear functions, we can embed arbitrary functions from Boolean variables to integer values. BMDs can thus model the functionality of data path circuits operating over word-level data. Many important functions, including integermultiplication, that cannot be represented efficiently at the bit level with BDDs have simple representations at the word level with BMDs. Furthermore, BMDs can represent Boolean functions with around the same complexity as BDDs. We propose a hierarchical approach to verifying arithmetic circuits, where componentmodules are first shownto implement their word-level specifications. The overall circuit functionality is then verified by composing the component functions and comparing the result to the word-level circuit specification. Multipliers with word sizes of up to 256 bits have been verified by this technique.Keywords
This publication has 9 references indexed in Scilit:
- Edge-valued binary decision for multi-level hierarchical verificationPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Multilevel logic synthesis based on functional decision diagramsPublished 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
- Verification of Arithmetic Functions with Binary Moment DiagramsPublished by Defense Technical Information Center (DTIC) ,1994
- Algebraic decision diagrams and their applicationsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1993
- Zero-suppressed BDDs for set manipulation in combinatorial problemsPublished by Association for Computing Machinery (ACM) ,1993
- 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
- Graph-Based Algorithms for Boolean Function ManipulationIEEE Transactions on Computers, 1986