Boolean Expression Diagrams

Research output: Research - peer-reviewJournal article – Annual report year: 2002

View graph of relations

This paper presents a new data structure called boolean expression diagrams (BEDs) for representing and manipulating Boolean functions. BEDs are a generalization of binary decision diagrams (BDDs) which can represent any Boolean circuit in linear space. Two algorithms are described for transforming a BED into a reduced ordered BDD. One is a generalized version of the BDD apply-operator while the other can exploit the structural information of the Boolean expression. This ability is demonstrated by verifying that two different circuit implementations of a 16-bit multiplier implement the same Boolean function. Using BEDs, this verification problem is solved efficiently, while using standard BDD techniques this problem is infeasible. Generally, BEDs are useful in applications, for example tautology checking, where the end-result as a reduced ordered BDD is small. Moreover, using operators for substitution and existential quantification they allow for the verification of large hierarchical circuits.
Original languageEnglish
JournalInformation and Computation
Volume179
Issue number2
Pages (from-to)194-212
ISSN0890-5401
DOIs
StatePublished - 15 Dec 2002
CitationsWeb of Science® Times Cited: 6
Download as:
Download as PDF
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
PDF
Download as HTML
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
HTML
Download as Word
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
Word

ID: 4600713