Boolean matching using binary decision diagrams with applications to logic synthesis and verification
- 2 January 2003
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 452-458
- https://doi.org/10.1109/iccd.1992.276313
Abstract
An algorithm for Boolean matching based on binary decision diagrams using a level-first search strategy is presented. This algorithm is generally not restricted to circuits with just a few inputs and can be used for both technology mapping and logic verification. Unlike depth-first and breadth-first strategies, a level-first strategy permits significant pruning of the search space. A set of filters that further improve the performance of the matching algorithm is described. A method of analyzing the effectiveness of a filter is presented, and the various filters are ranked on the basis of their effect/cost ratio. Experimental results on a number of benchmark circuits are presented, comparing the basic matching algorithm with and without the use of various filters. It is shown how the matching algorithm and the filters can be extended to Boolean functions with don't cares.Keywords
This publication has 10 references indexed in Scilit:
- Proving circuit correctness using formal comparison between expected and extracted behaviourPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Edge-valued binary decision for multi-level hierarchical verificationPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Efficient implementation of a BDD packagePublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Shared binary decision diagram with attributed edges for efficient Boolean function manipulationPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Technology mapping using Boolean matching and don't care setsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Heuristics to compute variable orderings for efficient manipulation of ordered binary decision diagramsPublished by Association for Computing Machinery (ACM) ,1991
- Breadth-first manipulation of SBDD of Boolean functions for vector processingPublished by Association for Computing Machinery (ACM) ,1991
- DAGON: technology binding and local optimization by DAG matchingPublished by Association for Computing Machinery (ACM) ,1987
- Graph-Based Algorithms for Boolean Function ManipulationIEEE Transactions on Computers, 1986
- Hardware VerificationComputer, 1985