NDLI: Verification of Arithmetic Circuits with Binary Moment Diagrams

Content Provider	IEEE Xplore Digital Library
Author	Randal E. Bryant, Yirng-An Chen
Copyright Year	1995
Description	Author affiliation: Carnegie Mellon University, Pittsburgh, PA (Randal E. Bryant, Yirng-An Chen)
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.
Starting Page	535
Ending Page	541
File Size	167511
Page Count	7
File Format	PDF
ISBN	0897917251
ISSN	0738100X
DOI	10.1109/DAC.1995.250005
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	1995-06-12
Publisher Place	USA
Access Restriction	Subscribed
Rights Holder	Association for Computing Machinery, Inc. (ACM)
Subject Keyword	Arithmetic Circuits Boolean functions Data structures Digital systems Encoding Binary decision diagrams Integer linear programming Electrical capacitance tomography Adders
Content Type	Text
Resource Type	Article

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Ordered binary decision diagrams and circuit structure

Algebraic decision diagrams and their applications

Decision diagrams for linear arithmetic

Integrating SAT with Multiway Decision Graphs for efficient model checking

Assertion-based Verification of Behavioral Descriptions with Non-linear Solver

Verification of Arithmetic Functions with Binary Moment Diagrams (1994)

Using integer equations for high level formal verification property checking

Exploiting don't cares to minimize *BMDs

Edge-valued binary decision for multi-level hierarchical verification

Verification of Arithmetic Circuits with Binary Moment Diagrams

Similar Documents

Ordered binary decision diagrams and circuit structure

Algebraic decision diagrams and their applications

Decision diagrams for linear arithmetic

Integrating SAT with Multiway Decision Graphs for efficient model checking

Assertion-based Verification of Behavioral Descriptions with Non-linear Solver

Verification of Arithmetic Functions with Binary Moment Diagrams (1994)

Using integer equations for high level formal verification property checking

Exploiting don't cares to minimize *BMDs

Edge-valued binary decision for multi-level hierarchical verification

Verification of Arithmetic Circuits with Binary Moment Diagrams