Logic in Computer Science (LICS 1997)

Paper: Boolean Expression Diagrams (at LICS 1997)

Authors: Henrik Reif Andersen Henrik Hulgaard

Abstract

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 and still maintain many of the desirable properties of BDDs. Two algorithms are described for transforming a BED into a reduced ordered BDD. One closely mimics the BDD apply-operator while the other can exploit the structural informa- tion of the Boolean expression. The efficacy of the BED representation is demonstrated by verifying that the redundant and non-redundant versions of the ISCAS 85 benchmark circuits are identical. In particular, it is verified that the two 16-bit multiplication circuits (c6288 and c6288nr) implement the same Boolean functions. Using BEDs, this verification problem is solved in less than a second, while using standard BDD techniques this problem is infeasible. BEDs are useful in applications where the end-result as a reduced ordered BDD is small, for example for tautology checking.

BibTeX

  @InProceedings{AndersenHulgaard-BooleanExpressionDi,
    author = 	 {Henrik Reif Andersen and Henrik Hulgaard},
    title = 	 {Boolean Expression Diagrams},
    booktitle =  {Proceedings of the Twelfth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1997},
    year =	 1997,
    editor =	 {Glynn Winskel},
    month =	 {June}, 
    pages =      {88--98},
    location =   {Warsaw, Poland}, 
    publisher =	 {IEEE Computer Society Press}
  }