The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.
Verification of Arithmetic Circuits with Binary Moment Diagrams
From OpenAlex, which stores abstracts as an
index of words and their positions: what is shown is rebuilt from that,
and reads fluently whether or not it is what the author wrote.
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.
@misc{bryant1995verification,
title = {Verification of Arithmetic Circuits with Binary Moment Diagrams},
author = {Randal E. Bryant},
year = {1995},
journal = {Proceedings - ACM IEEE Design Automation Conference},
publisher = {Association for Computing Machinery},
doi = {10.1109/dac.1995.250005},
}