Verification of arithmetic circuits using binary moment diagrams |
| |
Authors: | Randal E Bryant Yirng-An Chen |
| |
Affiliation: | (1) Department of Computer Science, Carnegie Mellon University, Pittsburgh, PA 15213, USA; E-mail: Randy.Bryant@cs.cmu.edu, US;(2) Department of Computer & Information Science, National Chiao Tung University, Hsinchu, Taiwan 300, ROC; E-mail: yachen@cis.nctu.edu.tw, TW |
| |
Abstract: | Binary moment diagrams (BMDs) provide a canonical representation 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 real, rational, or integer values. BMDs can thus model the functionality of data path circuits operating over word-level
data. Many important functions, including integer multiplication, 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 as a
special case. We propose a hierarchical approach to verifying arithmetic circuits, where component modules are first shown
to 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.
Published online: 15 May 2001 |
| |
Keywords: | : Decision diagrams – Computer arithmetic – Formal verification |
本文献已被 SpringerLink 等数据库收录! |
|