FSM encoding for BDD representations

Gosti, W. ; Villa, T. ; Saldanha, A. ; Sangiovanni-Vincentelli, A. L.

International Journal of Applied Mathematics and Computer Science, Tome 17 (2007) no. 1, pp. 113-128.

Résumé

We address the problem of encoding the state variables of a finite state machine such that the BDD representing the next state function and the output function has the minimum number of nodes. We present an exact algorithm to solve this problem when only the present state variables are encoded. We provide results on MCNC benchmark circuits.

Détail

Keywords: binary decision diagram, encoding, finite state machine, logic synthesis, formal verification, logic representation
Mots-clés : binarny diagram decyzyjny, kodowanie, automat skończony, synteza logiczna, weryfikacja formalna

Bibliographie

[1] Bern J., Meinel C. and Slobodova A. (1996): Global rebuilding of OBDD's avoiding memory requirement maxima. - IEEE Trans. CAD Int. Circuits Syst., Vol. 15, No. 1, pp. 131-134.

[2] Brayton R.K., Hachtel G.D., McMullen C.T. and Sangiovanni-Vincentelli A.L. (1984): Logic Minimization Algorithms for VLSI Synthesis. - Kluwer Academic Publishers.

[3] Bryant R.E. (1986): Graph-based algorithms for Boolean function manipulation. - IEEE Trans. Comput., Vol. C(35), No. 8, pp. 677-691.

[4] Bryant R.E. (1992): Symbolic Boolean manipulation with ordered binary-decision diagrams. - ACM Comput. Surveys, Vol. 24, No. 3.

[5] Buch P., Narayan A., Richard Newton A. and Sangiovanni-Vincentelli A. (1997): Logic synthesis for large pass transistor circuits. - Proc. 1997 IEEE/ACM Int. Conf. Computer-Aided Design, ICCAD '97, Washington, DC, USA, pp. 663-670.

[6] Cabodi G., Quer S. and Camurati P. (1995): Transforming Boolean relations by symbolic encoding, In: Proc. Correct Hardware Design and Verification CHARME'95, (P. Camurati and P. Eveking, Edi.), LNCS, Vol. 987, pp. 161-170.

[7] Drechsler R., Drechsler N. and Gunther W. (2000): Fast exact minimization of BDD's. - IEEE Trans. CAD Int. Circ. Syst., Vol. 19, No. 3, pp. 384-389.

[8] Drechsler R., Junhao Shi and Görschwin Fey (2004): Synthesis of fully testable circuits from BDDs. - IEEE Trans. CAD Int. Circ. Syst., Vol. 23, No. 3, pp. 440-443.

[9] Gosti W., Villa T., Saldanha A. and Sangiovanni-Vincentelli A. (1998): An exact input encoding algorithm for BDDs representing FSMs. - Proc. 8-th Great Lakes Symp. VLSI, Lafayette, LA, USA, pp. 294-300.

[10] Gosti W., Villa T., Saldanha A. and Sangiovanni-Vincentelli A.L. (1997): Input encoding for minimum BDD size: Theory and experiments.-Techn. rep., University of California at Berkeley, No. UCB/ERL M97/22.

[11] Gunther W. and Drechsler R. (1998): Linear transformations and exact minimization of BDDs.- Proc. 8-thGreat Lakes Symp. VLSI, Lafayette, LA, USA, pp. 325-330.

[12] Gunther W. and Drechsler R. (2000): ACTion: Combining logic synthesis and technology mapping for MUX-based FPGAs. -J. Syst. Archit., Vol. 46, No. 14, pp. 1321-1334.

[13] Hartmanis J. and Stearns R.E. (1962): Some dangers in the state reduction of sequential machines. - Inf. Contr., Vol. 5, No. 3, pp. 252-260.

[14] Lavagno L., McGeer P., Saldanha A. and Sangiovanni-Vincentelli A.L. (1995): Timed Shannon Circuits: A Power-Efficient Design Style and Synthesis Tool. - Proc. 32-th Design Automation Conf., San Francisco, CA, USA, pp. 254-260.

[15] Lee E.B. and Perkowski M. (1984): Concurrent minimization and state assignment of finite state machines. - Proc. IEEE Int. Conf. Syst., Man Cybernetics, Halifax, Nova Scotia, Canada, pp. 248-260.

[16] Lisanke R. (1989): Logic synthesis benchmark circuits for the International Workshop on Logic Synthesis. - Research Triangle Park, North Carolina, Microelectronics Center of North Carolina.

[17] Macchiarulo L., Benini L. and Macii E. (2001): On-the-fly layout generation for PTL macrocells.-Proc. Conf. Design, Automation and Test in Europe, DATE '01, pp. 546-551, Piscataway, NJ, USA, IEEE Press.

[18] Meinel C., Somenzi F. and Theobald T. (2000): Linear sifting of decision diagrams and its application in synthesis. - IEEE Trans. CAD Int. Circ. Syst., Vol. 19, No. 5, pp. 521-533.

[19] Meinel C. and Theobald T. (1999): On the influence of state encoding on OBDD-representations of finite state machines. - Theoret. Inf. Applic., Vol. 33, No. 1, pp. 21-31.

[20] Meinel Ch. and Theobald T. (1996 a): Local encoding transformations for optimizing OBDD-representations of finite state machines. - Proc. Int. Conf. Formal Methods in Computer-Aided Design, London: Springer, No. 1166, pp. 404-418.

[21] Meinel Ch. and Theobald T. (1996 b): State encodings and OBDD-sizes. - Techn. rep. 96-04, Universität Trier, Germany.

[22] Rudell R. (1993): Dynamic variable ordering for ordered binary decision diagrams. - Proc. Int. Conf. Computer-Aided Design, San Francisco, CA, USA, pp. 42-47.

[23] Saldanha A., Villa T., Brayton R. and Sangiovanni-Vincentelli A. (1994): Satisfaction of input and output encoding constraints. - IEEE Trans. CAD Int. Circ. Syst., Vol. 13, No. 5, pp 589-602.

[24] Villa T., Kam T., Brayton R. and Sangiovanni-Vincentelli A. (1997): Synthesis of FSMs: Logic Optimization. - Boston: Kluwer.

[25] Yuan L., Qu G., Villa T. and Sangiovanni-Vincentelli A.L. (2005): FSM re-engineering and its application in low power state encoding. - Proc. 2005 Asia South Pacific Design Automation Conf. (ASP-DAC 2005), Shanghai, China, Vol. 1, pp. 254-259.