Equivalence checking of combinational circuits using Boolean expression diagrams

Citation
H. Hulgaard et al., Equivalence checking of combinational circuits using Boolean expression diagrams, IEEE COMP A, 18(7), 1999, pp. 903-917
Citations number
46
Categorie Soggetti
Eletrical & Eletronics Engineeing
Journal title
IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS
ISSN journal
02780070 → ACNP
Volume
18
Issue
7
Year of publication
1999
Pages
903 - 917
Database
ISI
SICI code
0278-0070(199907)18:7<903:ECOCCU>2.0.ZU;2-D
Abstract
The combinational logic-level equivalence problem is to determine whether t wo given combinational circuits implement the same Boolean function. This p roblem arises in a number of computer-aided design (CAD) applications, for example when checking the correctness of incremental design changes (Perfor med either manually or by a design automation tool). This paper introduces a data structure called boolean expression diagrams ( BED's) and two algorithms for transforming a BED into a reduced ordered bin ary decision diagram (OBDD), BED's 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 BED's suitable for v erifying the equivalence of combinational circuits. BED's can be seen as an intermediate representation between circuits (which are compact) and OBDD' s (which are canonical). Based on a large number of combinational circuits, we demonstrate that BED' s either outperform or achieve results comparable to both standard OBDD app roaches and the techniques specifically developed to exploit structural sim ilarities for efficiently solving the equivalence problem. Due to the simplicity and generality of BED's, it is to be expected that co mbining them with other approaches to equivalence checking will be both str aightforward and beneficial.