FSM encoding for BDD representations

• Autorzy: Wilsin Gosti , Tiziano Villa , Alex Saldanha , Alberto L. Sangiovanni-Vincentelli
• Języki publikacji: EN

Abstrakty

EN

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.

Słowa kluczowe

EN

formal verification; encoding; logic synthesis; binary decision diagram; finite state machine; logic representation

• Wydawca: University of Zielona Gora Press
• Czasopismo: International Journal of Applied Mathematics and Computer Science
• Rocznik: 2007
• Tom: 17
• Numer: 1
• Strony: 113-128

Daty

wydano

2007

poprawiono

2006-05-10

otrzymano

2006-05-12

(nieznana)

2006-12-15

Twórcy

autor

Wilsin Gosti

• Cadence Design Systems, 2655 Seely Avenue, San Jose, CA 95134, USA

autor

Tiziano Villa

• DI, Universita' di Verona, Ca' Vignal 2, Strada Le Grazie 15, 37134 Verona, Italy

autor

Alex Saldanha

• Exponential Interactive, Inc., Emeryville, CA 94608, USA

autor

Alberto L. Sangiovanni-Vincentelli

• Department of Electrical Engineering and Computer Sience, University of California, Berkeley, CA 94720, USA

Bibliografia

• 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.
• Brayton R.K., Hachtel G.D., McMullen C.T. and Sangiovanni-Vincentelli A.L. (1984): Logic Minimization Algorithms for VLSI Synthesis. - Kluwer Academic Publishers.
• Bryant R.E. (1986): Graph-based algorithms for Boolean function manipulation.- IEEE Trans. Comput., Vol.C(35), No.8, pp.677-691.
• Bryant R.E. (1992): Symbolic Boolean manipulation with ordered binary-decision diagrams. - ACM Comput. Surveys, Vol.24, No.3.
• 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.
• 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.
• Drecher R., Drecher N. and Gunther W. (2000): Fast exact minimization of BDD's. - IEEE Trans. CAD Int. Circ. Syst., Vol.19, No.3, pp.384-389.
• Drecher R., Junhao Shi and Gorschwin Fey (2004): Synthesis of fully testable circuits from BDDs. - IEEE Trans. CAD Int. Circ. Syst., Vol.23, No.3, pp.440-443.
• 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.
• 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.
• Gunther W. and Drecher R. (1998): Linear transformations and exact minimization of BDDs. - Proc. 8-th Great Lakes Symp. VLSI, Lafayette, LA, USA, pp.325-330.
• Gunther W. and Drecher R. (2000): ACTion: Combining logic synthesis and technology mapping for MUX-based FPGAs. - J. Syst. Archit., Vol.46, No.14, pp.1321-1334.
• 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.
• 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.
• 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.
• Lisanke R. (1989): Logic synthesis benchmark circuits for the International Workshop on Logic Synthesis. - Research Triangle Park, North Carolina, Microelectronics Center of North Carolina.
• 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.
• 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.
• 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.
• 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.
• Meinel Ch. and Theobald T. (1996 b): State encodings and OBDD-sizes. - Techn. rep. 96-04, Universat Trier, Germany.
• Rudell R. (1993): Dynamic variable ordering for ordered binary decision diagrams. - Proc. Int. Conf. Computer-Aided Design,San Francisco, CA, USA, pp.42-47.
• 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, pp589-602.
• Villa T., Kam T., Brayton R. and Sangiovanni-Vincentelli A. (1997): Synthesis of FSMs: Logic Optimization. - Boston: Kluwer.
• 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