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.
@article{bwmeta1.element.bwnjournal-article-amcv17i1p113bwm,
author = {Gosti, Wilsin and Villa, Tiziano and Saldanha, Alex and Sangiovanni-Vincentelli, Alberto},
title = {FSM encoding for BDD representations},
journal = {International Journal of Applied Mathematics and Computer Science},
volume = {17},
year = {2007},
pages = {113-128},
zbl = {1153.68553},
language = {en},
url = {http://dml.mathdoc.fr/item/bwmeta1.element.bwnjournal-article-amcv17i1p113bwm}
}
Gosti, Wilsin; Villa, Tiziano; Saldanha, Alex; Sangiovanni-Vincentelli, Alberto. FSM encoding for BDD representations. International Journal of Applied Mathematics and Computer Science, Tome 17 (2007) pp. 113-128. http://gdmltest.u-ga.fr/item/bwmeta1.element.bwnjournal-article-amcv17i1p113bwm/
[000] 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.
[001] Brayton R.K., Hachtel G.D., McMullen C.T. and Sangiovanni-Vincentelli A.L. (1984): Logic Minimization Algorithms for VLSI Synthesis. - Kluwer Academic Publishers. | Zbl 0565.94020
[002] Bryant R.E. (1986): Graph-based algorithms for Boolean function manipulation.- IEEE Trans. Comput., Vol.C(35), No.8, pp.677-691. | Zbl 0593.94022
[003] Bryant R.E. (1992): Symbolic Boolean manipulation with ordered binary-decision diagrams. - ACM Comput. Surveys, Vol.24, No.3.
[004] 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.
[005] 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.
[006] 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.
[007] 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.
[008] 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.
[009] 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. | Zbl 1153.68553
[010] 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.
[011] 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.
[012] 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. | Zbl 0105.32301
[013] 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.
[014] 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.
[015] Lisanke R. (1989): Logic synthesis benchmark circuits for the International Workshop on Logic Synthesis. - Research Triangle Park, North Carolina, Microelectronics Center of North Carolina.
[016] 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.
[017] 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.
[018] 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. | Zbl 0927.68051
[019] 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.
[020] Meinel Ch. and Theobald T. (1996 b): State encodings and OBDD-sizes. - Techn. rep. 96-04, Universat Trier, Germany.
[021] Rudell R. (1993): Dynamic variable ordering for ordered binary decision diagrams. - Proc. Int. Conf. Computer-Aided Design,San Francisco, CA, USA, pp.42-47.
[022] 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.
[023] Villa T., Kam T., Brayton R. and Sangiovanni-Vincentelli A. (1997): Synthesis of FSMs: Logic Optimization. - Boston: Kluwer. | Zbl 0876.94057
[024] 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