FSM encoding for BDD representations

Wilsin Gosti; Tiziano Villa; Alex Saldanha; Alberto Sangiovanni-Vincentelli

International Journal of Applied Mathematics and Computer Science (2007)

  • Volume: 17, Issue: 1, page 113-128
  • ISSN: 1641-876X

Abstract

top
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.

How to cite

top

Gosti, Wilsin, et al. "FSM encoding for BDD representations." International Journal of Applied Mathematics and Computer Science 17.1 (2007): 113-128. <http://eudml.org/doc/207815>.

@article{Gosti2007,
abstract = {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.},
author = {Gosti, Wilsin, Villa, Tiziano, Saldanha, Alex, Sangiovanni-Vincentelli, Alberto},
journal = {International Journal of Applied Mathematics and Computer Science},
keywords = {formal verification; encoding; logic synthesis; binary decision diagram; finite state machine; logic representation},
language = {eng},
number = {1},
pages = {113-128},
title = {FSM encoding for BDD representations},
url = {http://eudml.org/doc/207815},
volume = {17},
year = {2007},
}

TY - JOUR
AU - Gosti, Wilsin
AU - Villa, Tiziano
AU - Saldanha, Alex
AU - Sangiovanni-Vincentelli, Alberto
TI - FSM encoding for BDD representations
JO - International Journal of Applied Mathematics and Computer Science
PY - 2007
VL - 17
IS - 1
SP - 113
EP - 128
AB - 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.
LA - eng
KW - formal verification; encoding; logic synthesis; binary decision diagram; finite state machine; logic representation
UR - http://eudml.org/doc/207815
ER -

References

top
  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. Zbl0565.94020
  3. Bryant R.E. (1986): Graph-based algorithms for Boolean function manipulation.- IEEE Trans. Comput., Vol.C(35), No.8, pp.677-691. Zbl0593.94022
  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. 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. 
  8. 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. 
  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. Zbl1153.68553
  11. 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. 
  12. 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. 
  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. Zbl0105.32301
  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. Zbl0927.68051
  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, Universat 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, pp589-602. 
  24. Villa T., Kam T., Brayton R. and Sangiovanni-Vincentelli A. (1997): Synthesis of FSMs: Logic Optimization. - Boston: Kluwer. Zbl0876.94057
  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 

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.