TED+: a data structure for microprocessor verification

ABSTRACT

Formal verification of microprocessors requires a mechanism for efficient representation and manipulation of both arithmetic and random Boolean functions. Recently, a new canonical and graph-based representation called TED has been introduced for verification of digital systems. Although TED can be used effectively to represent arithmetic expressions at the word-level, it is not memory efficient in representing bit-level logic expressions. In this paper, we present modifications to TED to improve its ability for bit-level logic representation while maintaining its robustness in arithmetic word-level representation. It will be shown that for random Boolean expressions, the modified TED performs the same as BDD representation.

References

1. R. E. Bryant, "Graph-based algorithms for Boolean function manipulation", IEEE Trans. Comput., vol. C-35, pp. 677--691, Aug. 1986.
2. R. E. Bryant, "Symbolic Boolean manipulation with ordered binary decision diagrams", ACM Comp. Surveys, vol. 24, pp. 293--318, Sep. 1992.
3. B. Becker, R. Drechsler, and R. Werchner, "On the relation between BDD's and FDD's", Inform. Comput., vol. 123, no. 2, pp. 185--197, Dec. 1995.
4. R. Rudell, "Dynamic variable ordering for ordered binary decision diagrams", Int. Conf. CAD, pp. 42--47, Nov. 1993.
5. R. Drechsler, M. Theobald, and B. Becker, "Fast OFDD based minimization of fixed polarity Reed-Muller expressions", Eur. Design Automation Conf., pp. 2--7, Sep. 1994.
6. U. Kebschull, E. Schubert, and W. Rosenstiel, "Multilevel logic synthesis based on functional decision diagrams", Eur. Conf. Design Automation, pp. 43--47, Mar. 1992.
7. R. Drechsler and B. Becker, "Sympathy: Fast exact minimization of fixed polarity Reed-Muller expressions for symmetric functions", IEEE Trans. CAD, vol. 16, #1, pp. 1--5, Jan. 1997.
8. E. M. Clarke, K. L. McMillan, X. Zhao, M. Fujita, and J. Yang, "Spectral Transforms for Large Boolean Functions with Applications to Technology Mapping", DAC, pp. 54--60, 1993.
9. I. Bahar, E. A. Frohm, C. M. Gaona, G. D. Hachtel, E. Macii, A. Pardo, and F. Somenzi, "Algebraic Decision Diagrams and their Applications", ICCAD, pp. 188--191, Nov. 1993.
10. Y-T. Lai, M. Pedram, and S. B. Vrudhula, "FGILP: An ILP Solver based on Function Graphs", ICCAD, pp. 685--689, 1993.
11. R. E. Bryant and Y-A. Chen, "Verification of Arithmetic Functions with Binary Moment Diagrams", DAC, 1995.
12. E. M. Clarke, M. Fujita, and X. Zhao, "Hybrid Decision Diagrams - Overcoming the Limitation of MTBDDs and BMDs", ICCAD, 1995.
13. R. Dreschler, B. Becker, and S. Ruppertz, "The K*BMD: A Verification Data Structure", IEEE Design & Test, pp. 51--59, 1997.
14. P. Kalla, M. Ciesielski, E. Boutillon, E. Martin, "High-level design verification using Taylor Expansion Diagrams: first results", High-Level Design Validation and Test Workshop, pp. 13--17, Oct. 2002.
15. M. J. Ciesielski, P. Kalla, Zhihong Zheng, B. Rouzeyre, "Taylor expansion diagrams: a new representation for RTL verification", High-Level Design Validation and Test Workshop, pp. 70--75, Nov. 2001.
16. M. J. Ciesielski, P. Kalla, Zhihong Zheng, B. Rouzeyre, "Taylor expansion diagrams: a compact, canonical representation with applications to symbolic verification", Design, Automation and Test in Europe, pp. 285--289, Mar. 2002.
17. S. Minato, N. Ishiura, S. Yajima, "Shared binary decision diagram with attributed edges for efficient Boolean function manipulation", DAC, pp. 52--57, Jan. 1991.
18. K. S. Brace, R. L. Rudell, R. E. Bryant, "Efficient implementation of a BDD package", DAC, pp. 40--45, Jun. 1990.
19. F. Somenzi, CUDD: CU Decision Diagram Package Release 2.3.0. University of Colorado at Boulder, 1998.
20. F. Brglez and H. Fujiwara, "A neutral netlist of 10 combinational circuits and a target translator in fortran", Int'l Symp. Circ. and Systems, Special Sess. on ATPG and Fault Simulation, pp. 663--698, 1985.