Equivalence Checking of Combinational Circuits using Boolean Expression Diagrams

Henrik Hulgaard
Poul Frederick Williams
Henrik Reif Andersen

July 1999

Abstract

This paper introduces a data structure called Boolean Expression Diagrams (BEDs) and two algorithms for transforming a BED into a Reduced Ordered Binary Decision Diagram (OBDD). BEDs are capable of representing any Boolean circuit in linear space and can exploit structural similarities between the two circuits that are compared. These properties make BEDs suitable for verifying the equivalence of combinational circuits. BEDs can be seen as an intermediate representation between circuits (which are compact) and OBDDs (which are canonical).

Based on a large number of combinational circuits, we demonstrate that BEDs either outperform or achieve results comparable to both standard OBDD approaches and the techniques specifically developed to exploit structural similarities for efficiently solving the equivalence problem.

Due to the simplicity and generality of BEDs, it is to be expected that combining them with other approaches to equivalence checking will be both straightforward and beneficial.

In IEEE Transactions on CAD, July 1999.

Available as PostScript(gzip'ed), PostScript, PDF, (preprints) and BibTeX.

1999 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.