Combinational Logic-Level Verification using Boolean Expression Diagrams
Henrik Hulgaard
Poul Frederick Williams
Henrik Reif Andersen
September 1997
Abstract
Boolean Expression Diagrams
(BEDs) is a new data structure for representing and manipulating
Boolean functions. BEDs are a generalization of Binary Decision
Diagrams (BDDs) that are capable of representing any Boolean circuit
in linear space and still maintain many of the desirable properties of
BDDs.
This paper demonstrates that BEDs are well suited for solving the
combinational logic-level verification problem which is, given two
combinational circuits, to determine whether they implement the same
Boolean functions. Based on all combinational circuits in the
ISCAS 85 and LGSynth 91 benchmarks, we demonstrate that BEDs
outperform both standard BDD approaches and the techniques
specifically developed to exploit structural similarities for
efficiently solving the problem.
In
3rd International Workshop on Applications of the
Reed-Muller Expansion in Circuit Design, September 1997.
Available as
PostScript(gzip'ed),
PostScript,
PDF, and
BibTeX.