Several algorithms exists for transforming a BED into a reduced ordered BDD. One closely mimics the BDD Apply-operator while another can exploit the structural information of the Boolean expression. There are also algorithms for determining satisfiability of formulae represented by BEDs.
We have successfully verified all circuits in the ISCAS 85 benchmark suite against their non-redundant version. In particular, we have verified that the two 16-bit multiplication circuits (c6288 and c6288nr) implement the same Boolean function. Using the BED package, this verification problem is solved in a less than a CPU second, while using standard BDD techniques this problem is infeasible.
Using the BED representation, it has been possible to verify that two different implementation of 1024-bits multipliers implement the same functionality. This is believed to be the hitherto largest circuit ever to be formally verified (each multiplier would consist of more than 10 million gates, if build!).
BEDs are useful in applications where the end-result as a reduced ordered BDD is small, for example, for tautology checking or for representing the transition relation when performing a fixed-point iteration in symbolic model checking.
BEDs are a part of the VERIS verification project, aimed at verifying large embedded systems.
The C source code of an efficient BED
package is available. It contains a library (with both C and C++
interfaces) of the core BED data structure and algorithms for
manipulating the BEDs. It also contains a user shell on top of the BED
library. Commands to build, manipulate, inspect and view BEDs can be
issued at a prompt. The BED package (version 2.5) is available
for download here. If you have any
questions or feedback about
the BED package, please send e-mail to Henrik Hulgaard.
More details are available in the paper
"Boolean Expression Diagrams" by
Henrik Reif Andersen and
Henrik Hulgaard. Appears in the proceedings for
LICS '97.
Available as
PostScript (gzip'ed),
PostScript, and
PDF.
The journal version of the above paper is
"Boolean Expression Diagrams" by
Henrik Reif Andersen and
Henrik Hulgaard.
To appear in
Information and Computation.
Available as
PostScript (gzip'ed),
PostScript, and
PDF.
We have verified a large number of
multi-level combinational circuits using the BED package. The
results are reported in the paper "Combinational Logic-Level
Verification using Boolean Expression Diagrams" by Henrik Hulgaard and Poul Frederick Williams and
Henrik Reif Andersen.
Appears in the proceedings for the
3rd International Workshop on Applications of the
Reed-Muller Expansion in Circuit Design, 1997.
Available as
PostScript (gzip'ed),
PostScript, and
PDF.
A more thorough investigation of the use of
the BED data structure in verification of combinational circuits can
be found in "Equivalence Checking of Combinational Circuits using
Boolean Expression Diagrams" by Henrik Hulgaard and Poul Frederick Williams and Henrik Reif Andersen.
Appears in
IEEE Transactions on CAD, July 1999.
Available as
PostScript (gzip'ed),
PostScript, and
PDF.
In a joint effort with researchers at ETH
Zürich and Carnegie Mellon University, we have applied BEDs in
symbolic model checking. For a class of problems with few or no input
variables, our BED model checking algorithm works well. The research
has been reported in "Combining Decision Diagrams and SAT Procedures
for Efficient Symbolic Model Checking" by Poul Frederick Williams and Armin Biere and Edmund M. Clarke and Anubhav Gupta.
Appear in
Proc. Computer Aided Verification (CAV), July 2000,
and as volume 1855 in Lecture Notes in Computer Science.
Copyright 2000 Springer-Verlag.
Available as
PostScript (gzip'ed),
PostScript, and
PDF.
Together with researchers at Bordeaux
University in France, we have extended the BED data structure to
include a p-cut operator suited for fault tree analysis. The research
has been reported in "Bypassing BDD Construction for Reliability Analysis"
by Poul Frederick Williams and Macha Nikolskaia and Antoine Rauzy.
In
Information Processing Letters (IPL). Copyright 2000
Elsevier.
Available as
PostScript (gzip'ed),
PostScript, and
PDF.
Poul Frederick
Williams' PhD dissertation describes how BEDs can be used in
formal verification. The title is "Formal Verification Based on
Boolean Expression Diagrams". It is available
here.