Equivalence Checking Using Abstract BDDs
The work
| Authors | Somesh Jha; Yuan Lu; Marius Minea; Edmund M. Clarke |
|---|---|
| Editors | |
| Type | techreport |
| Year | 1996 |
| Citekey | jha1996equivalence |
Where it appeared
| Publisher | School of Computer Science, Carnegie Mellon University |
|---|---|
| Number in series | CMU-CS-96-187 |
| School | School of Computer Science, Carnegie Mellon University |
Identifiers
| report_number | CMU-CS-96-187 |
|---|
Access
| Landing page | https://www.cs.cmu.edu/~emc/papers/Conference%20Papers/Equivalence%20Checking%20Using%20Abstract%20BDDs.pdf |
|---|
Empty on purpose
| container |
Related
| Distinct from | bryant1991complexity |
|---|---|
| Distinct from | clarke1996word |
| Distinct from | dai2026guarded |
| Distinct from | pertseva2026automating |
From bibtex.
Abstract
We introduce a new equivalence checking method based on abstract BDDs (aBDDs). The basic idea is the following: given an abstraction function, aBDDs reduce the size of BDDs by merging nodes that have the same abstract value. An aBDD has bounded size and can be constructed without constructing the original BDD. We show that this method of equivalence checking is complete for an important class of arithmetic circuits that includes integer multiplication. The efficiency of this technique is illustrated by experiments on ISCAS'85 benchmark circuits.
A copy is held
pdf, 529.9 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-09-17 18:03 UTC |
| Approved by | a person 2026-10-22 18:07 UTC |
Filed under
Cite it as
@techreport{jha1996equivalence,
title = {Equivalence Checking Using Abstract BDDs},
author = {Somesh Jha and Yuan Lu and Marius Minea and Edmund M. Clarke},
year = {1996},
publisher = {School of Computer Science, Carnegie Mellon University},
school = {School of Computer Science, Carnegie Mellon University},
}
This record lives at https://refs.drheap.org/jha1996equivalence/ and will keep doing so.