Verification of Arithmetic Functions with Binary Moment Diagrams

From bibtex.

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 arbitary 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 with around the same complexity as BDDs. We propose a hierarchical approach to verifying arithmetic circuits, here basic building blocks are first shown to implement a word-level specification. The overall circuit functionality Is then verified at the word level. Multipliers with word sizes of up to 62 bits have been verified by this technique. Acceslon For NTIS CRA&I uric TAB 03 Unannounced Justification Dist. ibution Availability Codes Dist,7Avail and Ior * 1st A-I Special I1 Verification of Arithmetic Functions with Binary Moment Diagrams* 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 arbitary 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 with around the same complexity as BDDs. We propose a hierarchical approach to verifying arithmetic circuits, here basic building blocks are first shown to implement a word-level specification. The overall circuit functionality is then verified at the word level. Multipliers with word sizes of up to 62 bits have been verified by this technique.