Abstract
The combinational logic-level equivalence problem is to determine
whether two given combinational circuits implement the same
Boolean function. This problem arises in a number of CAD
applications, for example when checking the correctness of
incremental design changes (performed either manually or by a
design automation tool).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
Original language | English |
---|---|
Journal | IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems |
Volume | 18 |
Issue number | 7 |
Pages (from-to) | 903 |
Publication status | Published - 1999 |