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: Randal E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, Aug. 1986 [doi>10.1109/TC.1986.1676819]
• 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: 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: 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: 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: J. Kuskin , D. Ofelt , M. Heinrich , J. Heinlein , R. Simoni , K. Gharachorloo , J. Chapin , D. Nakahira , J. Baxter , M. Horowitz , A. Gupta , M. Rosenblum , J. Hennessy, The Stanford FLASH multiprocessor, Proceedings of the 21ST annual international symposium on Computer architecture, p.302-313, April 18-21, 1994, Chicago, Illinois, United States
• 7: Kenneth L. McMillan, A Conjunctively Decomposed Boolean Representation for Symbolic Model Checking, Proceedings of the 8th International Conference on Computer Aided Verification, p.13-25, August 03, 1996
• 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

Primary Classification:
  B. Hardware
  B.7 INTEGRATED CIRCUITS

Additional Classification:
  B. Hardware
  B.8 Performance and Reliability

  C. Computer Systems Organization

  G. Mathematics of Computing
  G.4 MATHEMATICAL SOFTWARE
      Subjects: Algorithm design and analysis

  J. Computer Applications

General Terms:
Algorithms, Design, Experimentation, Measurement, Performance, Theory

Keywords:
ISM frequency band, RF CMOS, digital radio, spread spectrum communication, transceiver