DocumentCode :
3163451
Title :
Verification of Arithmetic Circuits with Binary Moment Diagrams
Author :
Randal E. Bryant, Yirng-An Chen
Author_Institution :
Carnegie Mellon University, Pittsburgh, PA
fYear :
1995
fDate :
1995
Firstpage :
535
Lastpage :
541
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 :
Adders; Arithmetic; Binary decision diagrams; Boolean functions; Circuits; Data structures; Digital systems; Electrical capacitance tomography; Encoding; Integer linear programming;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Design Automation, 1995. DAC '95. 32nd Conference on
Conference_Location :
San Francisco, CA
ISSN :
0738-100X
Print_ISBN :
0-89791-725-1
Type :
conf
DOI :
10.1109/DAC.1995.250005
Filename :
1586761
Link To Document :
بازگشت