Approximate reachability with BDDs using overlapping projections

ABSTRACT

Approximate reachability tec hniques trade off accuracy with the capacity to deal with bigger designs. Cho et al [3] proposed approximate FSM traversal algorithms over a partition of the set of state bits. In this paper w egeneralize it by allowing projectionson to a collection of nondisjoint subsets of the state variables. We establish the adv an tageof ha ving overlapping projections and present a new multiple constr ainfunction for BDDs, to compute efficiently the approximate image during symbolic forward propagation using overlapping projections. We demonstrate the effectiveness of this new algorithm by applying it to several control modules from the I/O unit in the Stanford FLASH Multiprocessor. We also present our results on the larger ISCAS 89 benchmarks.

References

1. 1.Bryant, R. E., "Graph-Based Algorithms for Boolean Function Manipulation." IEEE Transactions on Comt?uters, Vol. C-35, No. 8, pp. 677-691, August 1986.
2. 2.Butch, J. R., Clarke, E. M., McMillan, K. L., Dill, D, L, and Hwang, L. J., "Symbolic Model Checking: 1020 States and Beyond ~' Proceedings of the Conference in Logic in Computer Science, pp. 428-439, 1990.
3. 3.Cho, H., Hachtel, G., Macii, E., Pleisser, B., and Somenzi, F., "Algorithms for Approximate FSM Traversal Based on State Space Decomposition," IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol. 15, No. 12, pp. 1465-1478, December 1996.
4. 4.Cho, H., Hachtel, G., Macii, E., Poncino, M., and Somenzi, F., "Automatic State Space Decomposition for Approximate FSM Traversal Based on Circuit Analysis," IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol. 15, No. 12, pp. 1451-1464, December 1996.
5. 5.Coudert, O., and Madre, J. C., "A Unified Framework for the Formal Verification of Sequential Circuits," IEEE International Conference on Computer-Aided Design, pp. 126- 129, 1990.
6. 6.Kuskin, J., Ofelt, D., Heinrich, M., Heinlein, J., Simoni, R., Gharachorloo, K., Chapin, J., Nakahira, D., Baxter, J., Horowitz, M., Gupta, A., Rosenblum, M., and Hennessy, J., "The Stanford FLASH Multiprocessor," Proceedings of the 21st International Symposium on Computer Architecture, pp. 301-313, April 1994.
7. 7.McMillan, K. L., "A Conjunctively Decomposed Boolean Representation for Symbolic Model Checking," In Proceedings of Computer-Aided Verification, pp. 13-25~ 1996.
8. 8.Touati, H. J., Savoj, H., Lin, B., Bra~on, R. K., and Sangiovanni-Vincentelli, A., "Implicit State Enumeration of Finite State Machines using BDDs,' IEEE International Conference on Computer-Aided Design, pp. 130-133, 1990.

Index Terms

• Applied computing

  • Physical sciences and engineering

    • Engineering

• Computer systems organization

  • Dependable and fault-tolerant systems and networks

• General and reference

  • Cross-computing tools and techniques

    • Performance

• Hardware

  • Integrated circuits

  • Robustness

• Mathematics of computing

  • Mathematical software

• Networks

  • Network performance evaluation